Skip to content

Commit 3deb4b8

Browse files
spcfoxspcfox
committed
[ WIP ] Use negative information during case tree simplification
1 parent 901e570 commit 3deb4b8

File tree

4 files changed

+30
-45
lines changed

4 files changed

+30
-45
lines changed

‎src/Core/Case/Optimise.idr‎

Lines changed: 29 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -17,14 +17,18 @@ mkSubst [] NilMatch = []
1717
mkSubst (x :: xs) (ConsMatch m) = x :: mkSubst xs m
1818

1919
data MatchResult : Scoped where
20-
ConPat : Name -> (tag : Int) -> List (Var vars) -> MatchResult vars
21-
DelayPat : (ty, arg : Var vars) -> MatchResult vars
22-
ConstPat : Constant -> MatchResult vars
20+
ConMatched : Name -> (tag : Int) -> List (Var vars) -> MatchResult vars
21+
ConUnmatched : List (Name, Int) -> MatchResult vars
22+
DelayMatched : (ty, arg : Var vars) -> MatchResult vars
23+
ConstMatched : Constant -> MatchResult vars
24+
ConstUnmatched : List Constant -> MatchResult vars
2325

2426
Weaken MatchResult where
25-
weakenNs s (ConPat n tag args) = ConPat n tag (weakenNs s <$> args)
26-
weakenNs s (DelayPat ty arg) = DelayPat (weakenNs s ty) (weakenNs s arg)
27-
weakenNs s (ConstPat c) = ConstPat c
27+
weakenNs s (ConMatched n tag args) = ConMatched n tag (weakenNs s <$> args)
28+
weakenNs s (ConUnmatched tags) = ConUnmatched tags
29+
weakenNs s (DelayMatched ty arg) = DelayMatched (weakenNs s ty) (weakenNs s arg)
30+
weakenNs s (ConstMatched c) = ConstMatched c
31+
weakenNs s (ConstUnmatched cs) = ConstUnmatched cs
2832

2933
export
3034
optimiseTree : {vars : _} -> List (Var vars, MatchResult vars) -> CaseTree vars -> Maybe (CaseTree vars)
@@ -34,36 +38,43 @@ optimiseAlts : {vars : _} -> List (Var vars, MatchResult vars) ->
3438
(List (Maybe (CaseAlt vars)), Maybe (CaseTree vars))
3539
optimiseAlts ps v [] = ([], Nothing)
3640
optimiseAlts ps v (ConCase n tag args sc :: alts)
37-
= do let sz = mkSizeOf args
41+
= do let Just unmatched : Maybe (MatchResult vars) = ConUnmatched . (::) (n, tag) <$>
42+
case lookup v ps of
43+
Nothing => Just []
44+
Just (ConUnmatched unmatch) =>
45+
toMaybe (not $ (n, tag) `elem` unmatch) unmatch
46+
_ => assert_total $ idris_crash "INTERNAL ERROR: unexpected match"
47+
| _ => optimiseAlts ps v alts
48+
let sz = mkSizeOf args
3849
let v' = weakenNs sz v
3950
let ps' = map (bimap (weakenNs sz) (weakenNs sz)) ps
4051
let args' = allVarsPrefix sz
41-
let alt = ConCase n tag args <$> optimiseTree ((v', ConPat n tag args') :: ps') sc
42-
mapFst (alt ::) (optimiseAlts ps v alts)
52+
let alt = ConCase n tag args <$> optimiseTree ((v', ConMatched n tag args') :: ps') sc
53+
mapFst (alt ::) (optimiseAlts ((v, unmatched) :: ps) v alts)
4354
optimiseAlts ps v (DelayCase ty arg sc :: alts)
4455
= do let sz = mkSizeOf [ty, arg]
4556
let v' = weakenNs sz v
4657
let ps' = map (bimap (weakenNs sz) (weakenNs sz)) ps
47-
let alt = DelayCase ty arg <$> optimiseTree ((v', DelayPat first (later first)) :: ps') sc
58+
let alt = DelayCase ty arg <$> optimiseTree ((v', DelayMatched first (later first)) :: ps') sc
4859
mapFst (alt ::) (optimiseAlts ps v alts)
4960
optimiseAlts ps v (ConstCase c sc :: alts)
50-
= do let alt = ConstCase c <$> optimiseTree ((v, ConstPat c) :: ps) sc
61+
= do let alt = ConstCase c <$> optimiseTree ((v, ConstMatched c) :: ps) sc
5162
mapFst (alt ::) (optimiseAlts ps v alts)
5263
optimiseAlts ps _ (DefaultCase sc :: _)
5364
= ([], optimiseTree ps sc)
5465

5566
pickAlt : {vars : _} -> List (Var vars, MatchResult vars) ->
5667
MatchResult vars -> List (CaseAlt vars) -> Maybe (CaseTree vars)
5768
pickAlt _ _ [] = Nothing
58-
pickAlt ps p@(ConPat n t args) (ConCase n' t' args' sc :: alts)
69+
pickAlt ps p@(ConMatched n t args) (ConCase n' t' args' sc :: alts)
5970
= if t == t' && n == n'
6071
then do match <- checkLengthMatch args args' -- lengths should always match
6172
optimiseTree ps $ substCaseTree zero (mkSizeOf _) (mkSubst args match) sc
6273
else pickAlt ps p alts
63-
pickAlt ps (DelayPat ty arg) (DelayCase ty' arg' sc :: _)
74+
pickAlt ps (DelayMatched ty arg) (DelayCase ty' arg' sc :: _)
6475
= do let subst : Subst Var [ty', arg'] vars = mkSubst [ty, arg] %search
6576
optimiseTree ps $ substCaseTree zero (mkSizeOf _) subst sc
66-
pickAlt ps p@(ConstPat c) (ConstCase c' sc :: alts)
77+
pickAlt ps p@(ConstMatched c) (ConstCase c' sc :: alts)
6778
= if c == c'
6879
then optimiseTree ps sc
6980
else pickAlt ps p alts
@@ -73,8 +84,10 @@ pickAlt ps p (_ :: alts) = pickAlt ps p alts
7384
optimiseTree ps (Case idx el ty alts)
7485
= do let var = MkVar el
7586
case lookup var ps of
76-
Just p => pickAlt ps p alts
77-
Nothing => case mapFst catMaybes $ optimiseAlts ps var alts of
87+
Just p@(ConMatched {}) => pickAlt ps p alts
88+
Just p@(DelayMatched {}) => pickAlt ps p alts
89+
Just p@(ConstMatched {}) => pickAlt ps p alts
90+
_ => case mapFst catMaybes $ optimiseAlts ps var alts of
7891
([], def) => def
7992
(alts, Nothing) => Just $ Case idx el ty alts
8093
(alts, Just def) =>

‎tests/idris2/casetree/casetree006/expected‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -23,13 +23,6 @@ Compile time tree: case {arg:1} of
2323
_ => case {arg:3} of
2424
(::) {e:7} {e:8} {e:9} => case {arg:5} of
2525
Later {e:10} {e:11} {e:12} {e:13} {e:14} {e:15} => 6
26-
_ => case {arg:2} of
27-
Z => case {arg:3} of
28-
(::) {e:1} {e:2} {e:3} => case {arg:5} of
29-
First {e:4} {e:5} {e:6} => 5
30-
S {e:0} => case {arg:3} of
31-
(::) {e:7} {e:8} {e:9} => case {arg:5} of
32-
Later {e:10} {e:11} {e:12} {e:13} {e:14} {e:15} => 6
3326
_ => case {arg:2} of
3427
Z => case {arg:3} of
3528
(::) {e:1} {e:2} {e:3} => case {arg:5} of

‎tests/idris2/casetree/heuristics001/expected‎

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,6 @@ Compile time tree: case {arg:4} of
66
_ => case {arg:2} of
77
Nil {e:1} => case {arg:4} of
88
S {e:2} => {arg:3}
9-
_ => case {arg:3} of
10-
Nil {e:3} => case {arg:4} of
11-
S {e:4} => {arg:2}
129
_ => case {arg:3} of
1310
Nil {e:3} => case {arg:4} of
1411
S {e:4} => {arg:2}
@@ -21,7 +18,7 @@ Inferrable args: [0]
2118
Compiled: \ {arg:2}, {arg:3}, {arg:4} => case {arg:4} of
2219
{ 0 => {arg:2}
2320
; _ => case {arg:2} of
24-
{ _builtin.NIL {tag = 0} [nil] => case {arg:4} of { 0 => case {arg:3} of { _builtin.NIL {tag = 0} [nil] => case {arg:4} of { 0 => crash "Nat case not covered"; _ => {arg:2}}}; _ => {arg:3}}
21+
{ _builtin.NIL {tag = 0} [nil] => case {arg:4} of { 0 => crash "Nat case not covered"; _ => {arg:3}}
2522
; _ => case {arg:3} of
2623
{ _builtin.NIL {tag = 0} [nil] => case {arg:4} of { 0 => crash "Nat case not covered"; _ => {arg:2}}
2724
; _ => case {arg:2} of
@@ -57,9 +54,6 @@ Compile time tree: case {arg:4} of
5754
_ => case {arg:2} of
5855
Nil {e:1} => case {arg:4} of
5956
S {e:2} => {arg:3}
60-
_ => case {arg:3} of
61-
Nil {e:3} => case {arg:4} of
62-
S {e:4} => {arg:2}
6357
_ => case {arg:3} of
6458
Nil {e:3} => case {arg:4} of
6559
S {e:4} => {arg:2}

‎tests/idris2/coverage/coverage032/expected‎

Lines changed: 0 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -8,35 +8,20 @@ Compile time tree: case {arg:2} of
88
_ => case {arg:1} of
99
True => case {arg:2} of
1010
Just {e:2} {e:3} => ()
11-
_ => case {arg:2} of
12-
Just {e:4} {e:5} => case {e:5} of
13-
False => ()
1411
_ => case {arg:2} of
1512
Just {e:4} {e:5} => case {e:5} of
1613
False => ()
1714
_ => case {arg:1} of
1815
False => case {e:5} of
1916
True => ()
20-
_ => case {arg:1} of
21-
False => case {arg:2} of
22-
Just {e:6} {e:7} => case {e:7} of
23-
True => ()
2417
Compiled: \ {arg:1}, {arg:2} => case {arg:2} of
2518
{ _builtin.NOTHING {tag = 0} [nothing] => ___
2619
; _ => case {arg:1} of
2720
{ 1 => case {arg:2} of
2821
{ _builtin.JUST {tag = 1} [just] {e:3} => ___
29-
; _ => case {arg:2} of
30-
{ _builtin.JUST {tag = 1} [just] {e:5} => case {e:5} of { 0 => ___}
31-
}
3222
}
3323
; _ => case {arg:2} of
3424
{ _builtin.JUST {tag = 1} [just] {e:5} => case {e:5} of { 0 => ___; _ => case {arg:1} of { 0 => case {e:5} of { 1 => ___}}}
35-
; _ => case {arg:1} of
36-
{ 0 => case {arg:2} of
37-
{ _builtin.JUST {tag = 1} [just] {e:7} => case {e:7} of { 1 => ___}
38-
}
39-
}
4025
}
4126
}
4227
}

0 commit comments

Comments
 (0)