Skip to content

Commit 8a27925

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

File tree

4 files changed

+40
-54
lines changed

4 files changed

+40
-54
lines changed

‎src/Core/Case/Optimise.idr‎

Lines changed: 39 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -17,53 +17,65 @@ 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
32+
33+
addUnmatchedCon : (Name, Int) -> Maybe (MatchResult vars) -> Maybe (MatchResult vars)
34+
addUnmatchedCon con Nothing = Just $ ConUnmatched [con]
35+
addUnmatchedCon con (Just (ConUnmatched cs))
36+
= toMaybe (not $ con `elem` cs) $ ConUnmatched (con :: cs)
37+
addUnmatchedCon _ _ = Nothing
2838

2939
export
3040
optimiseTree : {vars : _} -> List (Var vars, MatchResult vars) -> CaseTree vars -> Maybe (CaseTree vars)
3141

3242
optimiseAlts : {vars : _} -> List (Var vars, MatchResult vars) ->
33-
Var vars -> List (CaseAlt vars) ->
43+
Var vars -> Maybe (MatchResult vars) -> List (CaseAlt vars) ->
3444
(List (Maybe (CaseAlt vars)), Maybe (CaseTree vars))
35-
optimiseAlts ps v [] = ([], Nothing)
36-
optimiseAlts ps v (ConCase n tag args sc :: alts)
37-
= do let sz = mkSizeOf args
45+
optimiseAlts ps v _ [] = ([], Nothing)
46+
optimiseAlts ps v p (ConCase n tag args sc :: alts)
47+
= do let p'@(Just _) = addUnmatchedCon (n, tag) p
48+
| _ => optimiseAlts ps v p alts
49+
let sz = mkSizeOf args
3850
let v' = weakenNs sz v
3951
let ps' = map (bimap (weakenNs sz) (weakenNs sz)) ps
4052
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)
43-
optimiseAlts ps v (DelayCase ty arg sc :: alts)
53+
let alt = ConCase n tag args <$> optimiseTree ((v', ConMatched n tag args') :: ps') sc
54+
mapFst (alt ::) (optimiseAlts ps v p' alts)
55+
optimiseAlts ps v p (DelayCase ty arg sc :: alts)
4456
= do let sz = mkSizeOf [ty, arg]
4557
let v' = weakenNs sz v
4658
let ps' = map (bimap (weakenNs sz) (weakenNs sz)) ps
47-
let alt = DelayCase ty arg <$> optimiseTree ((v', DelayPat first (later first)) :: ps') sc
48-
mapFst (alt ::) (optimiseAlts ps v alts)
49-
optimiseAlts ps v (ConstCase c sc :: alts)
50-
= do let alt = ConstCase c <$> optimiseTree ((v, ConstPat c) :: ps) sc
51-
mapFst (alt ::) (optimiseAlts ps v alts)
52-
optimiseAlts ps _ (DefaultCase sc :: _)
53-
= ([], optimiseTree ps sc)
59+
let alt = DelayCase ty arg <$> optimiseTree ((v', DelayMatched first (later first)) :: ps') sc
60+
mapFst (alt ::) (optimiseAlts ps v p alts)
61+
optimiseAlts ps v p (ConstCase c sc :: alts)
62+
= do let alt = ConstCase c <$> optimiseTree ((v, ConstMatched c) :: ps) sc
63+
mapFst (alt ::) (optimiseAlts ps v p alts)
64+
optimiseAlts ps v p (DefaultCase sc :: _)
65+
= ([], optimiseTree (maybe ps (\p => (v, p) :: ps) p) sc)
5466

5567
pickAlt : {vars : _} -> List (Var vars, MatchResult vars) ->
5668
MatchResult vars -> List (CaseAlt vars) -> Maybe (CaseTree vars)
5769
pickAlt _ _ [] = Nothing
58-
pickAlt ps p@(ConPat n t args) (ConCase n' t' args' sc :: alts)
70+
pickAlt ps p@(ConMatched n t args) (ConCase n' t' args' sc :: alts)
5971
= if t == t' && n == n'
6072
then do match <- checkLengthMatch args args' -- lengths should always match
6173
optimiseTree ps $ substCaseTree zero (mkSizeOf _) (mkSubst args match) sc
6274
else pickAlt ps p alts
63-
pickAlt ps (DelayPat ty arg) (DelayCase ty' arg' sc :: _)
75+
pickAlt ps (DelayMatched ty arg) (DelayCase ty' arg' sc :: _)
6476
= do let subst : Subst Var [ty', arg'] vars = mkSubst [ty, arg] %search
6577
optimiseTree ps $ substCaseTree zero (mkSizeOf _) subst sc
66-
pickAlt ps p@(ConstPat c) (ConstCase c' sc :: alts)
78+
pickAlt ps p@(ConstMatched c) (ConstCase c' sc :: alts)
6779
= if c == c'
6880
then optimiseTree ps sc
6981
else pickAlt ps p alts
@@ -73,8 +85,10 @@ pickAlt ps p (_ :: alts) = pickAlt ps p alts
7385
optimiseTree ps (Case idx el ty alts)
7486
= do let var = MkVar el
7587
case lookup var ps of
76-
Just p => pickAlt ps p alts
77-
Nothing => case mapFst catMaybes $ optimiseAlts ps var alts of
88+
Just p@(ConMatched {}) => pickAlt ps p alts
89+
Just p@(DelayMatched {}) => pickAlt ps p alts
90+
Just p@(ConstMatched {}) => pickAlt ps p alts
91+
p => case mapFst catMaybes $ optimiseAlts ps var p alts of
7892
([], def) => def
7993
(alts, Nothing) => Just $ Case idx el ty alts
8094
(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)