git.iko.soy/Idris-dev
on master help sign in
Use elaborated form of cases to check for defaults

Before, the check for a default catch-all case was done using PTerm and the Placeholder constructor. Now, universal cases at the end are found by checking that all arguments are elaborated to pattern variables. This can catch cases where it's not an explicit placeholder, and it avoids confusion with constructors by checking the binders of the elaborated case.

commitaeb703e01511add5d11fa8f3819bd2500f94bf62 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 19 Sep 2015, 12:16 (11 years ago) parent6d7d3bd
1 file changed+13−3
compare with master
unifiedsplit
src/Idris/Elab/Clause.hs+13−3
src/Idris/Elab/Clause.hs+13−3
@@ -162,7 +162,7 @@ elabClauses info' fc opts n_in cs =
162162 simpleCase tcase (UnmatchedCase "Error") reflect CompileTime fc inacc atys pdef erInfo
163163 cov <- coverage
164164 pmissing <-
165− if cov && not (hasDefault cs)
165+ if cov && not (hasDefault pats_raw)
166166 then do missing <- genClauses fc n (map getLHS pdef) cs_full
167167 -- missing <- genMissing n scargs sc
168168 missing' <- filterM (checkPossible info fc True n) missing
@@ -291,10 +291,20 @@ elabClauses info' fc opts n_in cs =
291291 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
292292 depat acc x = (acc, x)
293293
294− hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs
295− , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args
294+
295+ getPVs (Bind x (PVar _) tm) = let (vs, tm') = getPVs tm
296+ in (x:vs, tm')
297+ getPVs tm = ([], tm)
298+
299+ isPatVar vs (P Bound n _) = n `elem` vs
300+ isPatVar _ _ = False
301+
302+ hasDefault cs | (Right (lhs, rhs) : _) <- reverse cs
303+ , (pvs, tm) <- getPVs (explicitNames lhs)
304+ , (f, args) <- unApply tm = all (isPatVar pvs) args
296305 hasDefault _ = False
297306
307+
298308 getLHS (_, l, _) = l
299309
300310 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)