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

git.iko.soy/Idris-dev

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

Perform positivity checking for Elab-defined datatypes

commit5abd0f52476c449f7750a6b0a813572db4b1af31 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 14 Mar 2016, 19:21 (11 years ago) parentce81494 749ecee

2 files changed+12−5

compare with master

unifiedsplit

src/Idris/Coverage.hs+4−3 src/Idris/Elab/Term.hs+8−2

src/Idris/Coverage.hs+4−3

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

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

335335checkAllCovering _ _ _ _ = return ()

336336

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

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

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

339339-- and update the context accordingly

340−

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

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

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

342+ -> Idris Totality

342343checkPositive mut_ns (cn, ty')

343344 = do i <- getIState

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

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

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

1818import Idris.Core.ProofTerm (getProofTerm)

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

2020import Idris.Core.WHNF (whnf)

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

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

2222import Idris.ErrReverse (errReverse)

2323import Idris.Elab.Quasiquote (extractUnquotes)

2424import Idris.Elab.Utils

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

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

26482648 addIBC (IBCImp cn)

26492649

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

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

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 ()

26512657

26522658 case ctors of

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