git.iko.soy/Idris-dev
on master help sign in
Deal with higher order recursive arguments in size change graphs
f8920a0Edwin Brady
src/Idris/Coverage.hs+3−2
compare with master
unifiedsplit
@@ -408,7 +408,7 @@ buildSCG ist sc args = scg sc (zip args args)
408 [ty] = lookupTy Nothing n ctxt -- must exist!
408 [ty] = lookupTy Nothing n ctxt -- must exist!
409 P _ nty _ = fst (unApply (getRetTy ty))
409 P _ nty _ = fst (unApply (getRetTy ty))
410 args = map snd (getArgTys ty) in
410 args = map snd (getArgTys ty) in
411− map (getRel nty) (map (fst . unApply) args)
411+ map (getRel nty) (map (fst . unApply . getRetTy) args)
412 where
412 where
413 getRel ty (P _ n' _) | n' == ty = (n, Smaller)
413 getRel ty (P _ n' _) | n' == ty = (n, Smaller)
414 getRel ty _ = (n, Unknown)
414 getRel ty _ = (n, Unknown)
@@ -446,7 +446,8 @@ buildSCG ist sc args = scg sc (zip args args)
446
446
447 mkChange :: [(Name, (Name, SizeChange))] -> Term
447 mkChange :: [(Name, (Name, SizeChange))] -> Term
448 -> Maybe (Int, SizeChange)
448 -> Maybe (Int, SizeChange)
449− mkChange szs (P _ n ty)
449+ mkChange szs tm
450+ | (P _ n ty, _) <- unApply tm -- get higher order args too
450 = do sc <- lookup n szs
451 = do sc <- lookup n szs
451 case sc of
452 case sc of
452 (_, Unknown) -> Nothing
453 (_, Unknown) -> Nothing
test/README+1
@@ -16,5 +16,6 @@ Tests:
16014: resource DSL
16014: resource DSL
17015: verified binary adder
17015: verified binary adder
18016: codata
18016: codata
19+017: mutually recursive totality checking
19
20
20regxxx: various regression tests
21regxxx: various regression tests
test/test017/expectednew file+1
@@ -0,0 +1 @@
1+test017a.idr:5:scg.vtrans is possibly not total as it is not well founded
test/test017/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris --check test017.idr
3+idris --check test017a.idr
4+rm -f *.ibc
test/test017/test017.idrnew file+96
@@ -0,0 +1,96 @@
1+module scg
2+
3+%default total
4+
5+data Ord = Zero | Suc Ord | Sup (Nat -> Ord)
6+
7+natElim : (n : Nat) -> (P : Nat -> Set) ->
8+ (P O) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)
9+natElim O P mO mS = mO
10+natElim (S k) P mO mS = mS k (natElim k P mO mS)
11+
12+ordElim : (x : Ord) ->
13+ (P : Ord -> Set) ->
14+ (P Zero) ->
15+ ((x : Ord) -> P x -> P (Suc x)) ->
16+ ((f : Nat -> Ord) -> ((n : Nat) -> P (f n)) ->
17+ P (Sup f)) -> P x
18+ordElim Zero P mZ mSuc mSup = mZ
19+ordElim (Suc o) P mZ mSuc mSup = mSuc o (ordElim o P mZ mSuc mSup)
20+ordElim (Sup f) P mZ mSuc mSup =
21+ mSup f (\n => ordElim (f n) P mZ mSuc mSup)
22+
23+myplus' : Nat -> Nat -> Nat
24+myplus : Nat -> Nat -> Nat
25+
26+myplus O y = y
27+myplus (S k) y = S (myplus' k y)
28+
29+myplus' O y = y
30+myplus' (S k) y = S (myplus y k)
31+
32+mnubBy : (a -> a -> Bool) -> List a -> List a
33+mnubBy = nubBy' []
34+ where
35+ nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
36+ nubBy' acc p [] = []
37+ nubBy' acc p (x::xs) =
38+ if elemBy p x acc then
39+ nubBy' acc p xs
40+ else
41+ x :: nubBy' (x::acc) p xs
42+
43+partial
44+vtrans : Vect a n -> Vect a n -> List a
45+vtrans [] _ = []
46+vtrans (x :: xs) ys = x :: vtrans ys ys
47+
48+even : Nat -> Bool
49+even O = True
50+even (S k) = odd k
51+ where
52+ odd : Nat -> Bool
53+ odd O = False
54+ odd (S k) = even k
55+
56+ack : Nat -> Nat -> Nat
57+ack O n = S n
58+ack (S m) O = ack m (S O)
59+ack (S m) (S n) = ack m (ack (S m) n)
60+
61+data Bin = eps | c0 Bin | c1 Bin
62+
63+foo : Bin -> Nat
64+foo eps = O
65+foo (c0 eps) = O
66+foo (c0 (c1 x)) = S (foo (c1 x))
67+foo (c0 (c0 x)) = foo (c0 x)
68+foo (c1 x) = S (foo x)
69+
70+bar : Nat -> Nat -> Nat
71+bar x y = mp x y where
72+ mp : Nat -> Nat -> Nat
73+ mp O y = y
74+ mp (S k) y = S (bar k y)
75+
76+total mfib : Nat -> Nat
77+mfib O = O
78+mfib (S O) = S O
79+mfib (S (S n)) = mfib (S n) + mfib n
80+
81+maxCommutative : (left : Nat) -> (right : Nat) ->
82+ maximum left right = maximum right left
83+maxCommutative O O = refl
84+maxCommutative (S left) O = refl
85+maxCommutative O (S right) = refl
86+maxCommutative (S left) (S right) =
87+ let inductiveHypothesis = maxCommutative left right in
88+ ?maxCommutativeStepCase
89+
90+maxCommutativeStepCase = proof {
91+ intros;
92+ rewrite (boolElimSuccSucc (lte left right) right left);
93+ rewrite (boolElimSuccSucc (lte right left) left right);
94+ rewrite inductiveHypothesis;
95+ trivial;
96+}
test/test017/test017a.idrnew file+7
@@ -0,0 +1,7 @@
1+module scg
2+
3+total
4+vtrans : Vect a n -> Vect a n -> List a
5+vtrans [] _ = []
6+vtrans (x :: xs) ys = x :: vtrans ys ys
7+