git.iko.soy/Idris-dev
on master help sign in
Fix silly error in totality checker

On the left hand side, make sure the name that's being checked is actually being used as a global name rather than a pattern bound variable

commit2392716762902468cb22916a8eafeaefd76eb2d1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 9 Mar 2016, 11:40 (11 years ago) parent0cb9b4e
2 files changed+9−5
compare with master
unifiedsplit
src/Idris/Core/Evaluate.hs+5−1 src/Idris/Coverage.hs+4−4
src/Idris/Core/Evaluate.hs+5−1
@@ -13,7 +13,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
1313 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
1414 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
1515 mapDefCtxt,
16− lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
16+ lookupTotal, lookupTotalExact, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
1717 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
1818 isUniverse) where
1919
@@ -1084,6 +1084,10 @@ lookupTotal :: Name -> Context -> [Totality]
10841084lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
10851085 where mkt (d, a, t, m) = t
10861086
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+
10871091lookupMetaInformation :: Name -> Context -> [MetaInformation]
10881092lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)
10891093 where mkm (d, a, t, m) = m
src/Idris/Coverage.hs+4−4
@@ -381,8 +381,8 @@ calcTotality fc n pats
381381 _ -> checkSizeChange n
382382 where
383383 checkLHS i (P _ fn _)
384− = case lookupTotal fn (tt_ctxt i) of
385− [Partial _] -> return (Partial (Other [fn]))
384+ = case lookupTotalExact fn (tt_ctxt i) of
385+ Just (Partial _) -> return (Partial (Other [fn]))
386386 _ -> Nothing
387387 checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
388388 checkLHS _ _ = Nothing
@@ -596,8 +596,8 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
596596
597597 toJust (n, t) = Just t
598598
599− getType n = case lookupTy n (tt_ctxt ist) of
600− [ty] -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
599+ getType n = case lookupTyExact n (tt_ctxt ist) of
600+ Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
601601
602602 isInductive (P _ nty _) (P _ nty' _) =
603603 let co = case lookupCtxt nty (idris_datatypes ist) of