b0720b0 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

381 test/totality003/run

382 test/totality003/*.idr

383 test/totality003/expected

384+ test/totality004/run

385+ test/totality004/*.idr

386+ test/totality004/expected

384

387

385 test/tutorial001/run

388 test/tutorial001/run

386 test/tutorial001/*.idr

389 test/tutorial001/*.idr

libs/prelude/Prelude/Stream.idr+3

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

10codata Stream : Type -> Type where

11 (::) : a -> Stream a -> Stream a

12

13+-- Hints for interactive editing

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

15+

13instance Functor Stream where

16instance Functor Stream where

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

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

15

18

src/Idris/Coverage.hs+14−7

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

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

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

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

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

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

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

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

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

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

417delazy' all t = t

418

419+data Guardedness = Toplevel | Unguarded | Guarded

420+

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

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

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

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

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

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

422 rhs' = delazy rhs

424 rhs' = delazy rhs

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

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

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

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

425

427

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

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

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

429 -- 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

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

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

432 -- as the call is guarded

434 -- as the call is guarded

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

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

436+ guarded <- Guarded,

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

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

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

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

439+ = let nguarded = case guarded of

440+ Unguarded -> Unguarded

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

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

442+ then Guarded

443+ else Unguarded in

437 mkChange n args pargs ++

444 mkChange n args pargs ++

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

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

439 findCalls guarded (App f a) pvs pargs

446 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

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

448 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

443 findCalls guarded (Bind n _ e) pvs pargs

450 findCalls guarded (Bind n _ e) pvs pargs

444 = findCalls guarded e (n : pvs) pargs

451 = findCalls guarded e (n : pvs) pargs

445 findCalls guarded (P _ f _ ) pvs pargs

452 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

117 _ -> False

118 _ -> False

119 -- 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

121 let usety = if norm then nty' else nty

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

123 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

2reg018b.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}

4reg018d.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

2+

3+%default total

4+

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

8+

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