678fc86 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

384 test/totality004/run

385 test/totality004/*.idr

386 test/totality004/expected

387+ test/totality005/run

388+ test/totality005/*.idr

389+ test/totality005/expected

387

390

388 test/tutorial001/run

391 test/tutorial001/run

389 test/tutorial001/*.idr

392 test/tutorial001/*.idr

src/Idris/Core/Evaluate.hs+1−1

@@ -265,7 +265,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

265 -- block reduction immediately under codata (and not forced)

266 ev ntimes stk top env

267 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

268− | dly == txt "Delay" && lco == txt "LazyCodata"

268+ | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl

269 = do let (f, _) = unApply arg

270 let ntimes' = case f of

271 P _ fn _ -> (fn, 0) : ntimes

src/Idris/Coverage.hs+7−4

@@ -430,11 +430,14 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

430 -- that it is total.

431 | (P _ (UN at) _, [_, _]) <- unApply ap,

432 at == txt "assert_total" = []

433− -- 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 of the

434− -- as the call is guarded

434+ -- immediate call, as long as the call is guarded.

435+ -- Then check its arguments

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

436+ | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

436 guarded <- Guarded,

437 guarded <- Guarded,

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

438+ del == txt "Delay"

439+ = let (capp, args) = unApply arg in

440+ concatMap (\x -> findCalls Toplevel x pvs pargs) args

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

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

439 = let nguarded = case guarded of

442 = let nguarded = case guarded of

440 Unguarded -> Unguarded

443 Unguarded -> Unguarded

test/totality005/expectednew file+2

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

1+totality005.idr:6:1:Main.fib is possibly not total due to recursive path Main.fib

2+[0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377]

test/totality005/runnew file+5

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

1+#!/usr/bin/env bash

2+idris $@ totality005.idr --total --check

3+idris $@ totality005.idr -o totality005

4+./totality005

5+rm -f totality005 *.ibc

test/totality005/totality005.idrnew file+9

@@ -0,0 +1,9 @@

1+

2+zipWithS : (f : a -> b -> c) -> Stream a -> Stream b -> Stream c

3+zipWithS f (x :: xs) (y :: ys) = f x y :: zipWithS f xs ys

4+

5+fib : Stream Nat

6+fib = 0 :: zipWithS (+) fib (1 :: fib)

7+

8+main : IO ()

9+main = print (take 15 fib)