5abd0f5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3037 from david-christiansen/app-utils

5abd0f5David Christiansen11 years ago

src/Idris/Coverage.hs+4−3

compare with master

unifiedsplit

@@ -334,11 +334,12 @@ checkAllCovering fc done top n | not (n `elem` done)

334 x -> return () -- stop if total

335checkAllCovering _ _ _ _ = return ()

336

337−-- Check if, in a given group of type declarations mut_ns,

337+-- | Check if, in a given group of type declarations mut_ns,

338-- the constructor cn : ty is strictly positive,

339-- and update the context accordingly

340−

340+checkPositive :: [Name] -- ^ the group of type declarations

341+ -> (Name, Type) -- ^ the constructor

341−checkPositive :: [Name] -> (Name, Type) -> Idris Totality

342+ -> Idris Totality

342checkPositive mut_ns (cn, ty')

343checkPositive mut_ns (cn, ty')

343 = do i <- getIState

344 = do i <- getIState

344 let ty = delazy' True (normalise (tt_ctxt i) [] ty')

345 let ty = delazy' True (normalise (tt_ctxt i) [] ty')

src/Idris/Elab/Term.hs+8−2

@@ -18,7 +18,7 @@ import Idris.Core.Unify

18import Idris.Core.ProofTerm (getProofTerm)

19import Idris.Core.Typecheck (check, recheck, converts, isType)

20import Idris.Core.WHNF (whnf)

21−import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

21+import Idris.Coverage (buildSCG, checkDeclTotality, checkPositive, genClauses, recoverableCoverage, validCoverageCase)

22import Idris.ErrReverse (errReverse)

23import Idris.Elab.Quasiquote (extractUnquotes)

24import Idris.Elab.Utils

@@ -2647,7 +2647,13 @@ processTacticDecls info steps =

2647 do updateIState $ \i -> i { idris_implicits = addDef cn impls (idris_implicits i) }

2648 addIBC (IBCImp cn)

2649

2650+ for_ ctors $ \(ctorN, _, _) ->

2650− for_ ctors $ \(cn, _, _) -> totcheck (NoFC, cn)

2651+ do totcheck (NoFC, ctorN)

2652+ ctxt <- tt_ctxt <$> getIState

2653+ case lookupTyExact ctorN ctxt of

2654+ Just cty -> do checkPositive (tyn : map cn ctors) (ctorN, cty)

2655+ return ()

2656+ Nothing -> return ()

2651

2657

2652 case ctors of

2658 case ctors of

2653 [ctor] -> do setDetaggable (cn ctor); setDetaggable tyn

2659 [ctor] -> do setDetaggable (cn ctor); setDetaggable tyn