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

git.iko.soy/Idris-dev

Added simple productivity checker for coinductive definitions

Recursive calls must be an argument to a coinductive constructor

commit30e4ed8ea61bd32e3e9490d91dda70eec590518e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 23 Oct 2012, 00:37 (14 years ago) parent5692e48

9 files changed+86−21

compare with master

unifiedsplit

src/Core/Evaluate.hs+2−1 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Coverage.hs+42−9 src/Idris/ElabDecls.hs+11−10 src/Idris/IBC.hs+4 test/README+1 test/test016/expected+1 test/test016/run+4 test/test016/test016.idr+20

src/Core/Evaluate.hs+2−1

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

607607 deriving Eq

608608

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

610− | Mutual [Name]

610+ | Mutual [Name] | NotProductive

611611 deriving (Show, Eq)

612612

613613instance Show Totality where

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

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

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

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+1−1

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

248248constraint = Constraint False Dynamic

249249tacimpl = TacImp False Dynamic

250250

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

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

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

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

254254 deriving (Show, Eq)

src/Idris/Coverage.hs+42−9

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

262262data LexOrder = LexXX | LexEQ | LexLT

263263 deriving (Show, Eq, Ord)

264264

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+

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

266294calcTotality path fc n pats

267− = do orders <- mapM ctot pats

268− let order = sortBy cmpOrd $ concat orders

269− let (errs, valid) = partitionEithers order

270− let lex = stripNoLT (stripXX valid)

271− case errs of

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

273− logLvl 10 $ show pats

274− checkDecreasing lex

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

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

300+ else do orders <- mapM ctot pats

301+ let order = sortBy cmpOrd $ concat orders

302+ let (errs, valid) = partitionEithers order

303+ let lex = stripNoLT (stripXX valid)

304+ case errs of

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

306+ logLvl 10 $ show pats

307+ checkDecreasing lex

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

276309 where

277310 cmpOrd (Left _) (Left _) = EQ

278311 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

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

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

6262 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

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

6471 addIBC (IBCDef n)

6572 addDeferred ds

66− setFlags n opts

67− 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

72− addIBC (IBCAccess n Frozen)

73− iputStrLn $ "Co " ++ show n

74− _ -> return ()

75− _ -> return ()

73+ setFlags n opts'

74+ addIBC (IBCFlags n opts')

75+ when corec $ do setAccessibility n Frozen

76+ addIBC (IBCAccess n Frozen)

7677

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

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

src/Idris/IBC.hs+4

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

649649 NotPositive -> putWord8 3

650650 Mutual x1 -> do putWord8 4

651651 put x1

652+ NotProductive -> putWord8 5

652653 get

653654 = do i <- getWord8

654655 case i of

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

659660 3 -> return NotPositive

660661 4 -> do x1 <- get

661662 return (Mutual x1)

663+ 5 -> return NotProductive

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

663665

664666instance Binary Totality where

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

737739 AssertTotal -> putWord8 3

738740 Specialise x -> do putWord8 4

739741 put x

742+ Coinductive -> putWord8 5

740743 get

741744 = do i <- getWord8

742745 case i of

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

746749 3 -> return AssertTotal

747750 4 -> do x <- get

748751 return (Specialise x)

752+ 5 -> return Coinductive

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

750754

751755instance Binary Fixity where

test/README+1

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

1515013: binding syntax

1616014: resource DSL

1717015: verified binary adder

18+016: codata

1819

1920regxxx: 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

3+%default total

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

7+countFrom : Int -> Stream Int

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

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+