ad016d9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Termination check fix for 'Inf'

It should never consider an argument with an 'Inf' type as smaller, because it might be infinite and this productivity check is done elsewhere. Fixes #2809

commitad016d93d72db2884ef2dbc2c002851c11abb245 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 10 Mar 2017, 14:23 (10 years ago) parentd1f3be2

5 files changed+32−1

compare with master

unifiedsplit

src/Idris/Termination.hs+4 test/TestData.hs+2−1 test/totality021/expected+5 test/totality021/run+3 test/totality021/totality021.idr+18

src/Idris/Termination.hs+4

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

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

456456 (fst (unApply (getRetTy tyt)))

457457 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

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

459463 = let tyn = getType n in

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

test/TestData.hs+2−1

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

281281 ( 17, ANY ),

282282 ( 18, ANY ),

283283 ( 19, ANY ),

284− ( 20, ANY )]),

284+ ( 20, ANY ),

285+ ( 21, ANY )]),

285286 ("tutorial", "Tutorial examples",

286287 [ ( 1, ANY ),

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

3+data Level : Type where

4+ SL : Inf Level -> Level

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

7+ Not (SL level = SL level)

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

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