9abed6a · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

401 test/totality005/run

402 test/totality005/*.idr

403 test/totality005/expected

404+ test/totality006/run

405+ test/totality006/*.idr

406+ test/totality006/expected

404

407

405 test/tutorial001/run

408 test/tutorial001/run

406 test/tutorial001/*.idr

409 test/tutorial001/*.idr

src/Idris/ElabDecls.hs+6−1

@@ -1335,7 +1335,12 @@ checkPossible info fc tcgen fname lhs_in

1335

1336 checkRec (App f a) p@(P _ _ _) = checkRec f p

1337 checkRec p@(P _ _ _) (App f a) = checkRec p f

1338+ checkRec fa@(App _ _) fa'@(App _ _)

1339+ | (f, as) <- unApply fa,

1340+ (f', as') <- unApply fa'

1341+ = if (length as /= length as')

1342+ then checkRec f f'

1338− checkRec (App f a) (App f' a') = checkRec f f' && checkRec a a'

1343+ else checkRec f f' && and (zipWith checkRec as as')

1339 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt

1344 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt

1340 checkRec _ _ = False

1345 checkRec _ _ = False

1341

1346

test/totality006/expectednew file+2

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

1+totality006.idr:6:1:Main.prf is not total as there are missing cases

2+totality006a.idr:9:6:prf' (S _) (S _) oh is a valid case

test/totality006/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ totality006.idr --check

3+idris $@ totality006a.idr --check

4+rm -f *.ibc

test/totality006/totality006.idrnew file+11

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

1+antitrue : so False -> a

2+antitrue oh impossible

3+

4+total

5+prf : (a:Nat) -> (b:Nat) -> so (a > b) -> GT a b

6+prf Z Z oh impossible

7+prf Z (S k) um = antitrue um

8+prf (S k) Z um = lteSucc lteZero

9+-- prf (S _) (S _) oh impossible

10+

11+

test/totality006/totality006a.idrnew file+10

@@ -0,0 +1,10 @@

1+antitrue : so False -> a

2+antitrue oh impossible

3+

4+total

5+prf' : (a:Nat) -> (b:Nat) -> so (a > b) -> GT a b

6+prf' Z Z oh impossible

7+prf' Z (S k) um = antitrue um

8+prf' (S k) Z um = lteSucc lteZero

9+prf' (S _) (S _) oh impossible

10+