git.iko.soy/Idris-dev
on master help sign in
Coverage checker fix

If a candidate case fails with a 'recoverable' unification error (i.e. one which could be fixed by allowing more reduction somewhere) then it should be considered valid for coverage checking purposes. Fixes #1069 (and possibly some others, not checked yet!) (There is, I think a better fix, involving better generation of candidate cases, which I will leave for another time)

commit85ff9c293533afe9a831da92aa26a8f88ac495fb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 20 Apr 2014, 21:26 (13 years ago) parent8bf2f8a
3 files changed+40−17
compare with master
unifiedsplit
CONTRIBUTORS+1−1 src/Idris/Core/Unify.hs+2−6 src/Idris/ElabDecls.hs+37−10
CONTRIBUTORS+1−1
@@ -19,11 +19,11 @@ Dominic Mulligan
1919Jan de Muijnck-Hughes
2020Tom Prince
2121raichoo
22+Philip Rasmussen
2223Reynir Reynisson
2324Seo Sanghyeon
2425Benjamin Saunders
2526startling
26−Philip Rasmussen
2727Chetan T
2828Matus Tejiscak
2929Dirk Ullrich
src/Idris/Core/Unify.hs+2−6
@@ -588,12 +588,8 @@ recoverable t@(App _ _) _
588588 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False
589589recoverable _ t@(App _ _)
590590 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False
591−recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)
592− | x == y = True
593− | otherwise = False
594−recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)
595− | x == y = True
596− | otherwise = False
591+recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y
592+recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
597593recoverable (Constant _) (P (DCon _ _) y _) = False
598594recoverable (P (DCon _ _) x _) (Constant _) = False
599595recoverable (Constant _) (P (TCon _ _) y _) = False
src/Idris/ElabDecls.hs+37−10
@@ -1292,7 +1292,7 @@ checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool
12921292checkPossible info fc tcgen fname lhs_in
12931293 = do ctxt <- getContext
12941294 i <- getIState
1295− let lhs = addImpl i lhs_in
1295+ let lhs = addImplPat i lhs_in
12961296 -- if the LHS type checks, it is possible
12971297 case elaborate ctxt (sMN 0 "patLHS") infP []
12981298 (erun fc (buildTC i info True [] fname (infTerm lhs))) of
@@ -1301,21 +1301,48 @@ checkPossible info fc tcgen fname lhs_in
13011301 case recheck ctxt [] (forget lhs_tm) lhs_tm of
13021302 OK _ -> return True
13031303 err -> return False
1304− Error err -> if tcgen then return False
1305− else return (impossibleError err)
1306− where impossibleError (CantUnify _ topx topy e _ _)
1307− = not (sameFam topx topy || not (impossibleError e))
1308− impossibleError (CantConvert _ _ _) = False
1309− impossibleError (At _ e) = impossibleError e
1310− impossibleError (Elaborating _ _ e) = impossibleError e
1311− impossibleError (ElaboratingArg _ _ _ e) = impossibleError e
1312− impossibleError _ = True
1304+ -- if it's a recoverable error, the case may become possible
1305+ Error err -> if tcgen then return (recoverable ctxt err)
1306+ else return (validCase ctxt err ||
1307+ recoverable ctxt err)
1308+ where validCase ctxt (CantUnify _ topx topy e _ _)
1309+ = let topx' = normalise ctxt [] topx
1310+ topy' = normalise ctxt [] topy in
1311+ not (sameFam topx' topy' || not (validCase ctxt e))
1312+ validCase ctxt (CantConvert _ _ _) = False
1313+ validCase ctxt (At _ e) = validCase ctxt e
1314+ validCase ctxt (Elaborating _ _ e) = validCase ctxt e
1315+ validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e
1316+ validCase ctxt _ = True
1317+
1318+ recoverable ctxt (CantUnify r topx topy e _ _)
1319+ = let topx' = normalise ctxt [] topx
1320+ topy' = normalise ctxt [] topy in
1321+ checkRec topx' topy'
1322+ recoverable ctxt (At _ e) = recoverable ctxt e
1323+ recoverable ctxt (Elaborating _ _ e) = recoverable ctxt e
1324+ recoverable ctxt (ElaboratingArg _ _ _ e) = recoverable ctxt e
1325+ recoverable _ _ = False
13131326
13141327 sameFam topx topy
13151328 = case (unApply topx, unApply topy) of
13161329 ((P _ x _, _), (P _ y _, _)) -> x == y
13171330 _ -> False
13181331
1332+ -- different notion of recoverable than in unification, since we
1333+ -- have no metavars -- just looking to see if a constructor is failing
1334+ -- to unify with a function that may be reduced later
1335+
1336+ checkRec (App f a) p@(P _ _ _) = checkRec f p
1337+ checkRec p@(P _ _ _) (App f a) = checkRec p f
1338+ checkRec (App f a) (App f' a') = checkRec f f' && checkRec a a'
1339+ checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
1340+ checkRec _ _ = False
1341+
1342+ ntRec x y | Ref <- x = True
1343+ | Ref <- y = True
1344+ | otherwise = False -- name is different, unrecoverable
1345+
13191346getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
13201347 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
13211348getFixedInType i env (_ : is) (Bind n (Pi t) sc)