bf8685e · Idris-dev · git.iko.soy

idris.cabal+2

compare with master

unifiedsplit

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

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

28 tuples, dependent pairs

29 .

30+ * Coinductive types

31+ .

30 * Indentation significant syntax, extensible syntax

32 * Indentation significant syntax, extensible syntax

31 .

33 .

32 * Tactic based theorem proving (influenced by Coq)

34 * Tactic based theorem proving (influenced by Coq)

lib/io.idr+1−1

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

2

3%access public

4

5−abstract data IO a = prim__IO a

5+abstract codata IO a = prim__IO a

6

7abstract

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

src/Core/Evaluate.hs+2

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

602 deriving (Show, Eq)

603

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

605+ | Productive

605 | Partial PReason

606 | Partial PReason

606 | Unchecked

607 | Unchecked

607 deriving Eq

608 deriving Eq

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

612

613

613instance Show Totality where

614instance Show Totality where

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

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

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

615 show Unchecked = "not yet checked for totality"

617 show Unchecked = "not yet checked for totality"

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

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

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

619 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

263 deriving (Show, Eq, Ord)

264

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

266−calcProd i fc n pats

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

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

267+ if (and patsprod)

268+ then return Productive

268− | otherwise = return (Partial NotProductive)

269+ else return (Partial NotProductive)

269 where

270 where

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

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

271

272

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

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

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

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

274

275

275 prod ok ap@(App _ _)

276 prod ok ap@(App _ _)

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

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

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

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

278 = let co = cotype ty in

279 = let co = cotype ty in

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

280+ if f == n

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

282+ return (and (ok : argsprod) )

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

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

284+ return (and argsprod)

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

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

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

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

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

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

284− prod ok t = True

288+ prod ok t = return True

285

289

286 cotype ty

290 cotype ty

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

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

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

407 if TotalFn `elem` opts

411 if TotalFn `elem` opts

408 then case t' of

412 then case t' of

409 Total _ -> return t'

413 Total _ -> return t'

414+ Productive -> return t'

410 e -> totalityError t'

415 e -> totalityError t'

411 else return t'

416 else return t'

412 where

417 where

src/Idris/IBC.hs+2

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

671 Partial x1 -> do putWord8 1

672 put x1

673 Unchecked -> do putWord8 2

674+ Productive -> do putWord8 3

674 get

675 get

675 = do i <- getWord8

676 = do i <- getWord8

676 case i of

677 case i of

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

679 1 -> do x1 <- get

680 1 -> do x1 <- get

680 return (Partial x1)

681 return (Partial x1)

681 2 -> return Unchecked

682 2 -> return Unchecked

683+ 3 -> return Productive

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

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

683

685

684instance Binary IBCFile where

686instance Binary IBCFile where