b0720b0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change guardedness check for new-style coinduction

Now checks that 'Delay LazyCodata' appears constructor guarded for *all* coinductive definitions, not just mixed inductive/coinductive. Added stream processor test.

commitb0720b0155f7953ad4015464547e40888d28f264 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 22 Mar 2014, 21:32 (13 years ago) parent71a968c

9 files changed+80−10

compare with master

unifiedsplit

idris.cabal+3 libs/prelude/Prelude/Stream.idr+3 src/Idris/Coverage.hs+14−7 src/Idris/ElabDecls.hs+1−1 test/reg018/expected+2−2 test/totality004/expected+2 test/totality004/run+5 test/totality004/totality004.idr+25 test/totality004/totality004a.idr+25

idris.cabal+3

@@ -381,6 +381,9 @@ Extra-source-files:

381381 test/totality003/run

382382 test/totality003/*.idr

383383 test/totality003/expected

384+ test/totality004/run

385+ test/totality004/*.idr

386+ test/totality004/expected

384387

385388 test/tutorial001/run

386389 test/tutorial001/*.idr

libs/prelude/Prelude/Stream.idr+3

@@ -10,6 +10,9 @@ import Prelude.Vect

1010codata Stream : Type -> Type where

1111 (::) : a -> Stream a -> Stream a

1212

13+-- Hints for interactive editing

14+%name Stream xs,ys,zs,ws

15+

1316instance Functor Stream where

1417 map f (x::xs) = f x :: map f xs

1518

src/Idris/Coverage.hs+14−7

@@ -410,18 +410,20 @@ delazy' all t@(App f a)

410410 l == txt "Force" = delazy' all arg

411411 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,

412412 l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg

413− | (P _ (UN l) _, [_, arg]) <- unApply t,

414− l == txt "Lazy'" = delazy' all arg

413+ | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,

414+ l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg

415415delazy' all (App f a) = App (delazy' all f) (delazy' all a)

416416delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)

417417delazy' all t = t

418418

419+data Guardedness = Toplevel | Unguarded | Guarded

420+

419421buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]

420422buildSCG' ist pats args = nub $ concatMap scgPat pats where

421423 scgPat (lhs, rhs) = let lhs' = delazy lhs

422424 rhs' = delazy rhs

423425 (f, pargs) = unApply (dePat lhs') in

424− findCalls True (dePat rhs') (patvars lhs') pargs

426+ findCalls Toplevel (dePat rhs') (patvars lhs') pargs

425427

426428 findCalls guarded ap@(App f a) pvs pargs

427429 -- under a call to "assert_total", don't do any checking, just believe

@@ -431,15 +433,20 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

431433 -- under a call to "Delay LazyCodata", don't do any checking as long

432434 -- as the call is guarded

433435 | (P _ (UN del) _, [_,_,_]) <- unApply ap,

434− guarded && del == txt "Delay" = []

436+ guarded <- Guarded,

437+ del == txt "Delay" = []

435438 | (P _ n _, args) <- unApply ap

436− = let nguarded = isConName n (tt_ctxt ist) in

439+ = let nguarded = case guarded of

440+ Unguarded -> Unguarded

441+ _ -> if isConName n (tt_ctxt ist)

442+ then Guarded

443+ else Unguarded in

437444 mkChange n args pargs ++

438445 concatMap (\x -> findCalls nguarded x pvs pargs) args

439446 findCalls guarded (App f a) pvs pargs

440− = findCalls False f pvs pargs ++ findCalls False a pvs pargs

447+ = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs

441448 findCalls guarded (Bind n (Let t v) e) pvs pargs

442− = findCalls False v pvs pargs ++ findCalls guarded e (n : pvs) pargs

449+ = findCalls Unguarded v pvs pargs ++ findCalls guarded e (n : pvs) pargs

443450 findCalls guarded (Bind n _ e) pvs pargs

444451 = findCalls guarded e (n : pvs) pargs

445452 findCalls guarded (P _ f _ ) pvs pargs

src/Idris/ElabDecls.hs+1−1

@@ -117,7 +117,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

117117 _ -> False

118118 _ -> False

119119 -- Productivity checking now via checking for guarded 'Delay'

120− let opts' = if corec then (Coinductive : opts) else opts

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

121121 let usety = if norm then nty' else nty

122122 ds <- checkDef fc [(n, (-1, Nothing, usety))]

123123 addIBC (IBCDef n)

test/reg018/expected+2−2

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

1−reg018a.idr:16:1:conat.minusCoNat is not productive

1+reg018a.idr:16:1:conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

22reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

3−reg018c.idr:19:1:CodataTest.inf is not productive

3+reg018c.idr:19:1:CodataTest.inf is possibly not total due to: {CodataTest.inf19}

44reg018d.idr:5:1:Main.pull is not total as there are missing cases

test/totality004/expectednew file+2

@@ -0,0 +1,2 @@

1+[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]

2+totality004a.idr:13:1:Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

test/totality004/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+idris $@ totality004.idr -o totality004

3+./totality004

4+idris $@ --check totality004a.idr

5+rm -f totality004 *.ibc

test/totality004/totality004.idrnew file+25

@@ -0,0 +1,25 @@

1+module Main

3+%default total

5+data SP : Type -> Type -> Type where

6+ get : (a -> SP a b) -> SP a b

7+ put : b -> Inf (SP a b) -> SP a b

9+copy : SP a a

10+copy = get (\x => put x copy)

11+

12+process : SP a b -> Stream a -> Stream b

13+process (get f) (x :: xs) = process (f x) xs

14+process (put b sp) xs = b :: process sp xs

15+

16+doubleInt : SP Nat Int

17+doubleInt = get (\x => put (the Int (cast x))

18+ (put (the Int (cast x) * 2) doubleInt))

19+

20+countStream : Nat -> Stream Nat

21+countStream x = x :: countStream (x + 1)

22+

23+main : IO ()

24+main = print (take 10 (process doubleInt (countStream 1)))

25+

test/totality004/totality004a.idrnew file+25