git.iko.soy/Idris-dev
on master help sign in
Fix silly error in totality checker
2392716Edwin Brady
src/Idris/Core/Evaluate.hs+5−1
compare with master
unifiedsplit
@@ -13,7 +13,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
13 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
13 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
14 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
14 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
15 mapDefCtxt,
15 mapDefCtxt,
16− lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
16+ lookupTotal, lookupTotalExact, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
17 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
17 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
18 isUniverse) where
18 isUniverse) where
19
19
@@ -1084,6 +1084,10 @@ lookupTotal :: Name -> Context -> [Totality]
1084lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
1084lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
1085 where mkt (d, a, t, m) = t
1085 where mkt (d, a, t, m) = t
1086
1086
1087+lookupTotalExact :: Name -> Context -> Maybe Totality
1088+lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1089+ where mkt (d, a, t, m) = t
1090+
1087lookupMetaInformation :: Name -> Context -> [MetaInformation]
1091lookupMetaInformation :: Name -> Context -> [MetaInformation]
1088lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)
1092lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)
1089 where mkm (d, a, t, m) = m
1093 where mkm (d, a, t, m) = m
src/Idris/Coverage.hs+4−4
@@ -381,8 +381,8 @@ calcTotality fc n pats
381 _ -> checkSizeChange n
381 _ -> checkSizeChange n
382 where
382 where
383 checkLHS i (P _ fn _)
383 checkLHS i (P _ fn _)
384− = case lookupTotal fn (tt_ctxt i) of
384+ = case lookupTotalExact fn (tt_ctxt i) of
385− [Partial _] -> return (Partial (Other [fn]))
385+ Just (Partial _) -> return (Partial (Other [fn]))
386 _ -> Nothing
386 _ -> Nothing
387 checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
387 checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
388 checkLHS _ _ = Nothing
388 checkLHS _ _ = Nothing
@@ -596,8 +596,8 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
596
596
597 toJust (n, t) = Just t
597 toJust (n, t) = Just t
598
598
599− getType n = case lookupTy n (tt_ctxt ist) of
599+ getType n = case lookupTyExact n (tt_ctxt ist) of
600− [ty] -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
600+ Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
601
601
602 isInductive (P _ nty _) (P _ nty' _) =
602 isInductive (P _ nty _) (P _ nty' _) =
603 let co = case lookupCtxt nty (idris_datatypes ist) of
603 let co = case lookupCtxt nty (idris_datatypes ist) of