ad016d9 · Idris-dev · git.iko.soy

src/Idris/Termination.hs+4

compare with master

unifiedsplit

@@ -455,6 +455,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

455 | a == t = isInductive (fst (unApply (getRetTy tyn)))

456 (fst (unApply (getRetTy tyt)))

457 smaller ty a (ap@(App _ f s), _)

458+ -- Nothing can be smaller than a delayed infinite thing...

459+ | (P (DCon _ _ _) (UN d) _, [P _ (UN reason) _, _, _]) <- unApply ap,

460+ d == txt "Delay" && reason == txt "Infinite"

461+ = False

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

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

459 = let tyn = getType n in

463 = let tyn = getType n in

460 any (smaller (ty `mplus` Just tyn) a)

464 any (smaller (ty `mplus` Just tyn) a)

test/TestData.hs+2−1

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

281 ( 17, ANY ),

282 ( 18, ANY ),

283 ( 19, ANY ),

284− ( 20, ANY )]),

284+ ( 20, ANY ),

285+ ( 21, ANY )]),

285 ("tutorial", "Tutorial examples",

286 ("tutorial", "Tutorial examples",

286 [ ( 1, ANY ),

287 [ ( 1, ANY ),

287 ( 2, ANY ),

288 ( 2, ANY ),

test/totality021/expectednew file+5

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

1+totality021.idr:8:1:

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

3+totality021.idr:12:1:

4+Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'

5+totality021.idr:18:1:Main.v is possibly not total due to: Main.sLevelNotSLevel

test/totality021/runnew file+3

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

1+#!/usr/bin/env bash

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

3+rm -f *.ibc

test/totality021/totality021.idrnew file+18

@@ -0,0 +1,18 @@

1+%default total

2+

3+data Level : Type where

4+ SL : Inf Level -> Level

5+

6+sLevelNotSLevel' : (level : Inf Level) ->

7+ Not (SL level = SL level)

8+sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl

9+

10+sLevelNotSLevel : (level : Level) ->

11+ Not (SL (Delay level) = SL (Delay level))

12+sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl

13+

14+l : Level

15+l = SL l

16+

17+v : Void

18+v = sLevelNotSLevel l Refl