aa0abbc · Idris-dev · git.iko.soy

src/Idris/Termination.hs+2−2

compare with master

unifiedsplit

@@ -284,8 +284,8 @@ buildSCG (_, n) = do

284

285delazy = delazy' False -- not lazy codata

286delazy' all t@(App _ f a)

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

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

288− l == txt "Force" = delazy' all arg

288+ l == txt "Force" && (all || lty /= txt "Infinite") = delazy' all arg

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

290 l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg

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

test/TestData.hs+2−1

@@ -290,7 +290,8 @@ testFamiliesData = [

290 ( 19, ANY ),

291 ( 20, ANY ),

292 ( 21, ANY ),

293− ( 22, ANY )]),

293+ ( 22, ANY ),

294+ ( 23, ANY )]),

294 ("tutorial", "Tutorial examples",

295 ("tutorial", "Tutorial examples",

295 [ ( 1, ANY ),

296 [ ( 1, ANY ),

296 ( 2, ANY ),

297 ( 2, ANY ),

test/totality023/expectednew file+2

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

1+totality023.idr:9:1:

2+Main.run is possibly not total due to recursive path Main.run --> Main.run

test/totality023/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ totality023.idr --check

3+rm -f *.ibc

test/totality023/totality023.idrnew file+11

@@ -0,0 +1,11 @@

1+data InfIO : Type where

2+ Do : IO a -> (a -> Inf InfIO) -> InfIO

3+

4+foo : InfIO

5+foo = Do (putStr "Foo") (\x => foo)

6+

7+total

8+run : InfIO -> IO ()

9+run (Do x f) = do r <- x

10+ run (f r)

11+