git.iko.soy/Idris-dev
on master help sign in
Strip impossible cases when building case trees
edfe5b3Edwin Brady
src/Core/CaseTree.hs+8−2
compare with master
unifiedsplit
@@ -167,9 +167,15 @@ data Phase = CompileTime | RunTime
167
167
168simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] ->
168simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] ->
169 TC CaseDef
169 TC CaseDef
170−simpleCase tc cover phase fc []
170+simpleCase tc cover phase fc cs
171+ = sc' tc cover phase fc (filter (\(_, _, r) ->
172+ case r of
173+ Impossible -> False
174+ _ -> True) cs)
175+ where
176+ sc' tc cover phase fc []
171 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []
177 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []
172−simpleCase tc cover phase fc cs
178+ sc' tc cover phase fc cs
173 = let proj = phase == RunTime
179 = let proj = phase == RunTime
174 pats = map (\ (avs, l, r) ->
180 pats = map (\ (avs, l, r) ->
175 (avs, toPats tc l, (l, r))) cs
181 (avs, toPats tc l, (l, r))) cs