30e4ed8 · Idris-dev · git.iko.soy

src/Core/Evaluate.hs+2−1

compare with master

unifiedsplit

@@ -607,7 +607,7 @@ data Totality = Total [Int] -- well-founded arguments

607 deriving Eq

608

609data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

610− | Mutual [Name]

610+ | Mutual [Name] | NotProductive

611 deriving (Show, Eq)

612

613instance Show Totality where

@@ -616,6 +616,7 @@ instance Show Totality where

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

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

618 show (Partial NotPositive) = "not strictly positive"

619+ show (Partial NotProductive) = "not productive"

619 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

620 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

620 show (Partial (Mutual ns)) = "possibly not total due to mutual recursive path " ++

621 show (Partial (Mutual ns)) = "possibly not total due to mutual recursive path " ++

621 showSep " --> " (map show ns)

622 showSep " --> " (map show ns)

src/Idris/AbsSyntaxTree.hs+1−1

@@ -248,7 +248,7 @@ expl = Exp False Dynamic

248constraint = Constraint False Dynamic

249tacimpl = TacImp False Dynamic

250

251−data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen

251+data FnOpt = Inlinable | TotalFn | Coinductive | AssertTotal | TCGen

252 | CExport String -- export, with a C name

253 | Specialise [Name] -- specialise it, freeze these names

254 deriving (Show, Eq)

src/Idris/Coverage.hs+42−9

@@ -262,17 +262,50 @@ checkPositive n (cn, ty)

262data LexOrder = LexXX | LexEQ | LexLT

263 deriving (Show, Eq, Ord)

264

265+calcProd :: 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)

269+ where

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

271+

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

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

274+

275+ prod ok ap@(App _ _)

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

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

278+ = 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

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

284+ prod ok t = True

285+

286+ cotype ty

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

288+ = case lookupCtxt Nothing t (idris_datatypes i) of

289+ [TI _ True] -> True

290+ _ -> False

291+ | otherwise = False

292+

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

293calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

266calcTotality path fc n pats

294calcTotality path fc n pats

295+ = do i <- get

296+ let opts = case lookupCtxt Nothing n (idris_flags i) of

297+ [fs] -> fs

298+ _ -> []

299+ if (Coinductive `elem` opts) then calcProd i fc n pats

267− = do orders <- mapM ctot pats

300+ else do orders <- mapM ctot pats

268− let order = sortBy cmpOrd $ concat orders

301+ let order = sortBy cmpOrd $ concat orders

269− let (errs, valid) = partitionEithers order

302+ let (errs, valid) = partitionEithers order

270− let lex = stripNoLT (stripXX valid)

303+ let lex = stripNoLT (stripXX valid)

271− case errs of

304+ case errs of

272− [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex)

305+ [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex)

273− logLvl 10 $ show pats

306+ logLvl 10 $ show pats

274− checkDecreasing lex

307+ checkDecreasing lex

275− (e : _) -> return e -- FIXME: should probably combine them

308+ (e : _) -> return e -- FIXME: should probably combine them

276 where

309 where

277 cmpOrd (Left _) (Left _) = EQ

310 cmpOrd (Left _) (Left _) = EQ

278 cmpOrd (Left _) (Right _) = LT

311 cmpOrd (Left _) (Right _) = LT

src/Idris/ElabDecls.hs+11−10

@@ -60,19 +60,20 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in

60 let nty = cty -- normalise ctxt [] cty

61 -- if the return type is something coinductive, freeze the definition

62 let nty' = normalise ctxt [] nty

63+ let (t, _) = unApply (getRetTy nty')

64+ let corec = case t of

65+ P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of

66+ [TI _ True] -> True

67+ _ -> False

68+ _ -> False

69+ let opts' = if corec then (Coinductive : opts) else opts

63 ds <- checkDef fc [(n, nty)]

70 ds <- checkDef fc [(n, nty)]

64 addIBC (IBCDef n)

71 addIBC (IBCDef n)

65 addDeferred ds

72 addDeferred ds

66− setFlags n opts

73+ setFlags n opts'

67− addIBC (IBCFlags n opts)

74+ addIBC (IBCFlags n opts')

68− let (t, _) = unApply (getRetTy nty')

69− case t of

70− P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of

71− [TI _ True] -> do setAccessibility n Frozen

75+ when corec $ do setAccessibility n Frozen

72− addIBC (IBCAccess n Frozen)

76+ addIBC (IBCAccess n Frozen)

73− iputStrLn $ "Co " ++ show n

74− _ -> return ()

75− _ -> return ()

76

77

77elabData :: ElabInfo -> SyntaxInfo -> FC -> Bool -> PData -> Idris ()

78elabData :: ElabInfo -> SyntaxInfo -> FC -> Bool -> PData -> Idris ()

78elabData info syn fc codata (PDatadecl n t_in dcons)

79elabData info syn fc codata (PDatadecl n t_in dcons)

src/Idris/IBC.hs+4

@@ -649,6 +649,7 @@ instance Binary PReason where

649 NotPositive -> putWord8 3

650 Mutual x1 -> do putWord8 4

651 put x1

652+ NotProductive -> putWord8 5

652 get

653 get

653 = do i <- getWord8

654 = do i <- getWord8

654 case i of

655 case i of

@@ -659,6 +660,7 @@ instance Binary PReason where

659 3 -> return NotPositive

660 3 -> return NotPositive

660 4 -> do x1 <- get

661 4 -> do x1 <- get

661 return (Mutual x1)

662 return (Mutual x1)

663+ 5 -> return NotProductive

662 _ -> error "Corrupted binary data for PReason"

664 _ -> error "Corrupted binary data for PReason"

663

665

664instance Binary Totality where

666instance Binary Totality where

@@ -737,6 +739,7 @@ instance Binary FnOpt where

737 AssertTotal -> putWord8 3

739 AssertTotal -> putWord8 3

738 Specialise x -> do putWord8 4

740 Specialise x -> do putWord8 4

739 put x

741 put x

742+ Coinductive -> putWord8 5

740 get

743 get

741 = do i <- getWord8

744 = do i <- getWord8

742 case i of

745 case i of

@@ -746,6 +749,7 @@ instance Binary FnOpt where

746 3 -> return AssertTotal

749 3 -> return AssertTotal

747 4 -> do x <- get

750 4 -> do x <- get

748 return (Specialise x)

751 return (Specialise x)

752+ 5 -> return Coinductive

749 _ -> error "Corrupted binary data for FnOpt"

753 _ -> error "Corrupted binary data for FnOpt"

750

754

751instance Binary Fixity where

755instance Binary Fixity where

test/README+1

@@ -15,5 +15,6 @@ Tests:

15013: binding syntax

16014: resource DSL

17015: verified binary adder

18+016: codata

18

19

19regxxx: various regression tests

20regxxx: various regression tests

test/test016/expectednew file+1

@@ -0,0 +1 @@

1+[10, 11, 12, 13, 14, 15, 16, 17, 18, 19]

test/test016/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris test016.idr -o test016

3+./test016

4+rm -f test016 *.ibc

test/test016/test016.idrnew file+20

@@ -0,0 +1,20 @@

1+module main

2+

3+%default total

4+

5+codata Stream a = Nil | (::) a (Stream a)

6+

7+countFrom : Int -> Stream Int

8+countFrom x = x :: countFrom (x + 1)

9+

10+take : Int -> Stream a -> List a

11+take 0 _ = []

12+take n (x :: xs) = x :: take (n - 1) xs

13+take n [] = []

14+

15+-- foo : main.countFrom 4 = 4 :: main.countFrom 5

16+-- foo = refl

17+

18+main : IO ()

19+main = do print (take 10 (main.countFrom 10))

20+