85ff9c2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Coverage checker fix

85ff9c2Edwin Brady13 years ago

CONTRIBUTORS+1−1

compare with master

unifiedsplit

@@ -19,11 +19,11 @@ Dominic Mulligan

19Jan de Muijnck-Hughes

20Tom Prince

21raichoo

22+Philip Rasmussen

22Reynir Reynisson

23Reynir Reynisson

23Seo Sanghyeon

24Seo Sanghyeon

24Benjamin Saunders

25Benjamin Saunders

25startling

26startling

26−Philip Rasmussen

27Chetan T

28Matus Tejiscak

29Dirk Ullrich

src/Idris/Core/Unify.hs+2−6

@@ -588,12 +588,8 @@ recoverable t@(App _ _) _

588 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

589recoverable _ t@(App _ _)

590 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

591−recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

591+recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y

592− | x == y = True

593− | otherwise = False

594−recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)

592+recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

595− | x == y = True

596− | otherwise = False

597recoverable (Constant _) (P (DCon _ _) y _) = False

593recoverable (Constant _) (P (DCon _ _) y _) = False

598recoverable (P (DCon _ _) x _) (Constant _) = False

594recoverable (P (DCon _ _) x _) (Constant _) = False

599recoverable (Constant _) (P (TCon _ _) y _) = False

595recoverable (Constant _) (P (TCon _ _) y _) = False

src/Idris/ElabDecls.hs+37−10

@@ -1292,7 +1292,7 @@ checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool

1292checkPossible info fc tcgen fname lhs_in

1293 = do ctxt <- getContext

1294 i <- getIState

1295− let lhs = addImpl i lhs_in

1295+ let lhs = addImplPat i lhs_in

1296 -- if the LHS type checks, it is possible

1297 case elaborate ctxt (sMN 0 "patLHS") infP []

1298 (erun fc (buildTC i info True [] fname (infTerm lhs))) of

@@ -1301,21 +1301,48 @@ checkPossible info fc tcgen fname lhs_in

1301 case recheck ctxt [] (forget lhs_tm) lhs_tm of

1302 OK _ -> return True

1303 err -> return False

1304+ -- if it's a recoverable error, the case may become possible

1304− Error err -> if tcgen then return False

1305+ Error err -> if tcgen then return (recoverable ctxt err)

1305− else return (impossibleError err)

1306+ else return (validCase ctxt err ||

1307+ recoverable ctxt err)

1306− where impossibleError (CantUnify _ topx topy e _ _)

1308+ where validCase ctxt (CantUnify _ topx topy e _ _)

1309+ = let topx' = normalise ctxt [] topx

1310+ topy' = normalise ctxt [] topy in

1307− = not (sameFam topx topy || not (impossibleError e))

1311+ not (sameFam topx' topy' || not (validCase ctxt e))

1308− impossibleError (CantConvert _ _ _) = False

1312+ validCase ctxt (CantConvert _ _ _) = False

1309− impossibleError (At _ e) = impossibleError e

1313+ validCase ctxt (At _ e) = validCase ctxt e

1310− impossibleError (Elaborating _ _ e) = impossibleError e

1314+ validCase ctxt (Elaborating _ _ e) = validCase ctxt e

1311− impossibleError (ElaboratingArg _ _ _ e) = impossibleError e

1315+ validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e

1312− impossibleError _ = True

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

1313

1326

1314 sameFam topx topy

1327 sameFam topx topy

1315 = case (unApply topx, unApply topy) of

1328 = case (unApply topx, unApply topy) of

1316 ((P _ x _, _), (P _ y _, _)) -> x == y

1329 ((P _ x _, _), (P _ y _, _)) -> x == y

1317 _ -> False

1330 _ -> False

1318

1331

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+

1319getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1346getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1320 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1347 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1321getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1348getFixedInType i env (_ : is) (Bind n (Pi t) sc)