bf8685e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Separate "productive" and "total" in totality checker

Productive can call Total, but not vice versa. This is still a temporary solution - don't rely on anything yet!

commitbf8685e7a9fcba5467d592c3e6fff7b5bc0cf8db authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 23 Oct 2012, 11:53 (14 years ago) parent30e4ed8

5 files changed+21−10

compare with master

unifiedsplit

idris.cabal+2 lib/io.idr+1−1 src/Core/Evaluate.hs+2 src/Idris/Coverage.hs+14−9 src/Idris/IBC.hs+2

idris.cabal+2

@@ -27,6 +27,8 @@ Description: Idris is a general purpose language with full dependent types.

2727 * do notation, idiom brackets, syntactic conveniences for lists,

2828 tuples, dependent pairs

2929 .

30+ * Coinductive types

31+ .

3032 * Indentation significant syntax, extensible syntax

3133 .

3234 * Tactic based theorem proving (influenced by Coq)

lib/io.idr+1−1

@@ -2,7 +2,7 @@ import prelude.list

33%access public

5−abstract data IO a = prim__IO a

5+abstract codata IO a = prim__IO a

77abstract

88io_bind : IO a -> (a -> IO b) -> IO b

src/Core/Evaluate.hs+2

@@ -602,6 +602,7 @@ data Accessibility = Public | Frozen | Hidden

602602 deriving (Show, Eq)

603603

604604data Totality = Total [Int] -- well-founded arguments

605+ | Productive

605606 | Partial PReason

606607 | Unchecked

607608 deriving Eq

@@ -612,6 +613,7 @@ data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

612613

613614instance Show Totality where

614615 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"

616+ show Productive = "Productive" -- ++ show args ++ " decreasing arguments"

615617 show Unchecked = "not yet checked for totality"

616618 show (Partial Itself) = "possibly not total as it is not well founded"

617619 show (Partial NotCovering) = "not total as there are missing cases"

src/Idris/Coverage.hs+14−9

@@ -263,25 +263,29 @@ data LexOrder = LexXX | LexEQ | LexLT

263263 deriving (Show, Eq, Ord)

264264

265265calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

266−calcProd i fc n pats

267− | and (map prodRec pats) = return (Total [])

268− | otherwise = return (Partial NotProductive)

266+calcProd i fc n pats = do patsprod <- mapM prodRec pats

267+ if (and patsprod)

268+ then return Productive

269+ else return (Partial NotProductive)

269270 where

270271 -- every application of n must be in an argument of a coinductive constructor

271272

272− prodRec :: ([Name], Term, Term) -> Bool

273+ prodRec :: ([Name], Term, Term) -> Idris Bool

273274 prodRec (_, _, tm) = prod False tm

274275

275276 prod ok ap@(App _ _)

276277 | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod ok arg

277278 | (P _ f ty, args) <- unApply ap

278279 = let co = cotype ty in

279− if f == n then and (ok : map (prod co) args)

280− else and (map (prod co) args)

281− prod ok (App f a) = prod False f && prod False a

282− prod ok (Bind _ (Let t v) sc) = prod False v && prod False v

280+ if f == n

281+ then do argsprod <- mapM (prod co) args

282+ return (and (ok : argsprod) )

283+ else do argsprod <- mapM (prod co) args

284+ return (and argsprod)

285+ prod ok (App f a) = liftM2 (&&) (prod False f) (prod False a)

286+ prod ok (Bind _ (Let t v) sc) = liftM2 (&&) (prod False v) (prod False v)

283287 prod ok (Bind _ b sc) = prod False sc

284− prod ok t = True

288+ prod ok t = return True

285289

286290 cotype ty

287291 | (P _ t _, _) <- unApply (getRetTy ty)

@@ -407,6 +411,7 @@ checkTotality path fc n

407411 if TotalFn `elem` opts

408412 then case t' of

409413 Total _ -> return t'

414+ Productive -> return t'

410415 e -> totalityError t'

411416 else return t'

412417 where

src/Idris/IBC.hs+2

@@ -671,6 +671,7 @@ instance Binary Totality where

671671 Partial x1 -> do putWord8 1

672672 put x1

673673 Unchecked -> do putWord8 2

674+ Productive -> do putWord8 3

674675 get

675676 = do i <- getWord8

676677 case i of

@@ -679,6 +680,7 @@ instance Binary Totality where

679680 1 -> do x1 <- get

680681 return (Partial x1)

681682 2 -> return Unchecked

683+ 3 -> return Productive

682684 _ -> error "Corrupted binary data for Totality"

683685

684686instance Binary IBCFile where