git.iko.soy/Idris-dev
on master help sign in
Tweak notion of recoverability in coverage checker

Fixes #970

commit9abed6a7e59ef54be06ac4c4a2ba3004d20458ac authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 20 Apr 2014, 21:51 (13 years ago) parent2820945
6 files changed+36−1
compare with master
unifiedsplit
idris.cabal+3 src/Idris/ElabDecls.hs+6−1 test/totality006/expected+2 test/totality006/run+4 test/totality006/totality006.idr+11 test/totality006/totality006a.idr+10
idris.cabal+3
@@ -401,6 +401,9 @@ Extra-source-files:
401401 test/totality005/run
402402 test/totality005/*.idr
403403 test/totality005/expected
404+ test/totality006/run
405+ test/totality006/*.idr
406+ test/totality006/expected
404407
405408 test/tutorial001/run
406409 test/tutorial001/*.idr
src/Idris/ElabDecls.hs+6−1
@@ -1335,7 +1335,12 @@ checkPossible info fc tcgen fname lhs_in
13351335
13361336 checkRec (App f a) p@(P _ _ _) = checkRec f p
13371337 checkRec p@(P _ _ _) (App f a) = checkRec p f
1338− checkRec (App f a) (App f' a') = checkRec f f' && checkRec a a'
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'
1343+ else checkRec f f' && and (zipWith checkRec as as')
13391344 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
13401345 checkRec _ _ = False
13411346
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+