ef954e1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix the new totality test

This makes one of the isDConName calls less specific, due to unresolved names coming out of impossible patterns.

commitef954e1fac8d77e6036accafe3abae7712620ca7 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 11 Feb 2015, 17:50 (12 years ago) parent54451e4

3 files changed+16−3

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+5−1 src/Idris/Core/Evaluate.hs+10−1 src/Idris/Delaborate.hs+1−1

src/Idris/AbsSyntax.hs+5−1

@@ -1734,7 +1734,11 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

17341734 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)

17351735 = Placeholder

17361736 su (PApp fc f@(PRef _ fn) args)

1737− | isDConName fn ctxt

1737+ -- here we use canBeDConName because the impossible pattern

1738+ -- check will not necessarily fully resolve constructor names,

1739+ -- and these bare names will otherwise get in the way of

1740+ -- impossbility checking.

1741+ | canBeDConName fn ctxt

17381742 = PApp fc f (fmap (fmap su) args)

17391743 su (PApp fc f args)

17401744 = PHidden (PApp fc f args)

src/Idris/Core/Evaluate.hs+10−1

@@ -11,7 +11,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

1111 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

1212 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

1313 mapDefCtxt,

14− lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,

14+ lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

1515 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

1616 isUniverse) where

1717

@@ -975,12 +975,21 @@ isTConName n ctxt

975975 Just (TyDecl (TCon _ _) _) -> True

976976 _ -> False

977977

978+-- | Check whether a resolved name is certainly a data constructor

978979isDConName :: Name -> Context -> Bool

979980isDConName n ctxt

980981 = case lookupDefExact n ctxt of

981982 Just (TyDecl (DCon _ _ _) _) -> True

982983 _ -> False

983984

985+-- | Check whether any overloading of a name is a data constructor

986+canBeDConName :: Name -> Context -> Bool

987+canBeDConName n ctxt

988+ = or $ do def <- lookupCtxt n (definitions ctxt)

989+ case tfst def of

990+ (TyDecl (DCon _ _ _) _) -> return True

991+ _ -> return False

992+

984993isFnName :: Name -> Context -> Bool

985994isFnName n ctxt

986995 = case lookupDefExact n ctxt of

src/Idris/Delaborate.hs+1−1

@@ -308,7 +308,7 @@ pprintErr' i (ElaboratingArg f x _ e)

308308 where whatIsName = let ctxt = tt_ctxt i

309309 in if isTConName f ctxt

310310 then text "type constructor" <> space

311− else if isConName f ctxt

311+ else if isDConName f ctxt

312312 then text "constructor" <> space

313313 else if isFnName f ctxt

314314 then text "function" <> space