git.iko.soy/Idris-dev
on master help sign in
Skip unnecessary coverage checking

If the last clause in a definition contains only _, we don't need to coverage check it. This vastly, vastly improves the speed of this defn: fourTupleElems : TT -> Maybe (TT, (TT, (TT, TT))) fourTupleElems (App (App (App (App p ty1) ty2) tm1) (App (App (App (App p ty3) ty4) tm2) (App (App (App (App p ty1) ty2) tm3) tm4))) = Just (tm1, tm2, tm3, tm4) fourTupleElems _ = Nothing

commit756b44fbffadd93b2aacec0b0fd922ee74b73ce4 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 7 Mar 2014, 14:42 (13 years ago) parentd0edb70
1 file changed+5−1
compare with master
unifiedsplit
src/Idris/ElabDecls.hs+5−1
src/Idris/ElabDecls.hs+5−1
@@ -988,7 +988,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
988988 simpleCase tcase False reflect CompileTime fc atys pdef
989989 cov <- coverage
990990 pmissing <-
991− if cov
991+ if cov && not (hasDefault cs)
992992 then do missing <- genClauses fc n (map getLHS pdef) cs
993993 -- missing <- genMissing n scargs sc
994994 missing' <- filterM (checkPossible info fc True n) missing
@@ -1092,6 +1092,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10921092 depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
10931093 depat acc x = (acc, x)
10941094
1095+ hasDefault cs | (PClause _ _ last _ _ _ :_) <- reverse cs
1096+ , (PApp fn s args) <- last = all ((==Placeholder) . getTm) args
1097+ hasDefault _ = False
1098+
10951099 getLHS (_, l, _) = l
10961100
10971101 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,