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

git.iko.soy/Idris-dev

Finish guardedness check

Also needs to check under 'Delay' that any further corecursive call is properly guarded.

commit678fc8695f80dfb48f2987344a087bb2856e9b77 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 23 Mar 2014, 15:07 (13 years ago) parent303e100

6 files changed+27−5

compare with master

unifiedsplit

idris.cabal+3 src/Idris/Core/Evaluate.hs+1−1 src/Idris/Coverage.hs+7−4 test/totality005/expected+2 test/totality005/run+5 test/totality005/totality005.idr+9

idris.cabal+3

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

384384 test/totality004/run

385385 test/totality004/*.idr

386386 test/totality004/expected

387+ test/totality005/run

388+ test/totality005/*.idr

389+ test/totality005/expected

387390

388391 test/tutorial001/run

389392 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

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

266266 ev ntimes stk top env

267267 (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

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

270270 let ntimes' = case f of

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

src/Idris/Coverage.hs+7−4

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

430430 -- that it is total.

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

432432 at == txt "assert_total" = []

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

434− -- as the call is guarded

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

433+ -- under a call to "Delay LazyCodata", don't do any checking of the

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

435+ -- Then check its arguments

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

436437 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

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

439442 = let nguarded = case guarded of

440443 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 @@

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

5+fib : Stream Nat

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

8+main : IO ()

9+main = print (take 15 fib)