aa0abbc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Pay attention to 'Force' in totality checking

If we ignore it, non-terminating and non-productive functions might accidentally be thought to be total. Fixes #3746

commitaa0abbc782c38f227a39c450da0c29386a9723e9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 4 May 2017, 12:25 (9 years ago) parentf5bae6b

5 files changed+20−3

compare with master

unifiedsplit

src/Idris/Termination.hs+2−2 test/TestData.hs+2−1 test/totality023/expected+2 test/totality023/run+3 test/totality023/totality023.idr+11

src/Idris/Termination.hs+2−2

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

284284

285285delazy = delazy' False -- not lazy codata

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

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

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

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

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

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

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

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

test/TestData.hs+2−1

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

290290 ( 19, ANY ),

291291 ( 20, ANY ),

292292 ( 21, ANY ),

293− ( 22, ANY )]),

293+ ( 22, ANY ),

294+ ( 23, ANY )]),

294295 ("tutorial", "Tutorial examples",

295296 [ ( 1, ANY ),

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

4+foo : InfIO

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

7+total

8+run : InfIO -> IO ()

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

10+ run (f r)

11+