git.iko.soy/Idris-dev
on master help sign in
Coverage checker fix
fcba396Edwin Brady
idris.cabal+3
compare with master
unifiedsplit
@@ -708,6 +708,9 @@ Extra-source-files:
708 test/totality009/run
708 test/totality009/run
709 test/totality009/*.idr
709 test/totality009/*.idr
710 test/totality009/expected
710 test/totality009/expected
711+ test/totality010/run
712+ test/totality010/*.idr
713+ test/totality010/expected
711
714
712 test/tutorial001/run
715 test/tutorial001/run
713 test/tutorial001/*.idr
716 test/tutorial001/*.idr
src/Idris/Coverage.hs+8−4
@@ -54,16 +54,16 @@ mkPatTm t = do i <- getIState
54genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
54genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
55genClauses fc n xs given
55genClauses fc n xs given
56 = do i <- getIState
56 = do i <- getIState
57− let lhs_tms = map (\x -> delab' i x True True) xs
57+ let lhs_tms = map (\x -> flattenArgs $ delab' i x True True) xs
58 -- if a placeholder was given, don't bother generating cases for it
58 -- if a placeholder was given, don't bother generating cases for it
59 let lhs_tms' = zipWith mergePlaceholders lhs_tms
59 let lhs_tms' = zipWith mergePlaceholders lhs_tms
60− (map (stripUnmatchable i) given)
60+ (map (stripUnmatchable i) (map flattenArgs given))
61 let lhss = map pUnApply lhs_tms'
61 let lhss = map pUnApply lhs_tms'
62
62
63 let argss = transpose lhss
63 let argss = transpose lhss
64 let all_args = map (genAll i) argss
64 let all_args = map (genAll i) argss
65 logLvl 5 $ "COVERAGE of " ++ show n
65 logLvl 5 $ "COVERAGE of " ++ show n
66− logLvl 5 $ show lhss
66+ logLvl 5 $ show (lhs_tms, lhss)
67 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
67 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
68 logLvl 10 $ show argss ++ "\n" ++ show all_args
68 logLvl 10 $ show argss ++ "\n" ++ show all_args
69 logLvl 3 $ "Original: \n" ++
69 logLvl 3 $ "Original: \n" ++
@@ -89,9 +89,13 @@ genClauses fc n xs given
89 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
89 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
90 | otherwise = []
90 | otherwise = []
91
91
92− pUnApply (PApp _ _ args) = map getTm args
92+ pUnApply (PApp _ f args) = map getTm args
93 pUnApply _ = []
93 pUnApply _ = []
94
94
95+ flattenArgs (PApp fc (PApp _ f as) as')
96+ = flattenArgs (PApp fc f (as ++ as'))
97+ flattenArgs t = t
98+
95 -- Return whether the given clause matches none of the input clauses
99 -- Return whether the given clause matches none of the input clauses
96 -- (xs)
100 -- (xs)
97 noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of
101 noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of
test/totality010/expectednew file+4
@@ -0,0 +1,4 @@
1+totality010.idr:27:1:
2+Main.evenNotS is not total as there are missing cases
3+totality010.idr:30:1:
4+Main.bad is possibly not total due to: Main.evenNotS
test/totality010/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ totality010.idr --check
3+rm -f *.ibc
test/totality010/totality010.idrnew file+31
@@ -0,0 +1,31 @@
1+%default total
2+
3+%default total
4+succNotLTE' : (LTE (S x) x) -> Void
5+succNotLTE' {x = Z} prf = succNotLTEzero prf
6+succNotLTE' {x = (S k)} (LTESucc prf) = succNotLTE' prf
7+
8+succNotLTE : Not (LTE (S x) x)
9+succNotLTE = succNotLTE'
10+
11+succNotLTE2 : Not (LTE (S x) x)
12+succNotLTE2 {x = Z} prf = succNotLTEzero prf
13+succNotLTE2 {x = (S k)} (LTESucc prf) = succNotLTE prf
14+
15+-- a defective even-odd definition allows me to prove bottom
16+
17+mutual
18+ data Even : Nat -> Type where
19+ ZeroEven : Even Z
20+ MkEven : Odd n -> Even (S n)
21+ MkBad : Even n -> Even (S n)
22+
23+ data Odd : Nat -> Type where
24+ MkOdd : Even n -> Odd (S n)
25+
26+evenNotS : Even n -> Not (Even (S n))
27+evenNotS MkEven ZeroEven impossible
28+
29+bad : Void
30+bad = evenNotS ZeroEven $ MkBad ZeroEven
31+