git.iko.soy/Idris-dev
on master help sign in
Look through call graph for mutual recursion when productivity checking
56bd9a1Edwin Brady
src/Idris/Coverage.hs+41−24
compare with master
unifiedsplit
@@ -163,38 +163,55 @@ checkPositive n (cn, ty)
163 posArg t = True
163 posArg t = True
164
164
165calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
165calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
166−calcProd i fc n pats = do patsprod <- mapM prodRec pats
166+calcProd i fc topn pats
167− if (and patsprod)
167+ = cp topn pats []
168− then return Productive
169− else return (Partial NotProductive)
170 where
168 where
171 -- every application of n must be in an argument of a coinductive
169 -- every application of n must be in an argument of a coinductive
172 -- constructor, in every function reachable from here in the
170 -- constructor, in every function reachable from here in the
173 -- call graph.
171 -- call graph.
174−
172+ cp n pats done = do patsprod <- mapM (prodRec n done) pats
173+ if (and patsprod)
174+ then return Productive
175+ else return (Partial NotProductive)
176+
175− prodRec :: ([Name], Term, Term) -> Idris Bool
177+ prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
178+ prodRec n done _ | n `elem` done = return True
176− prodRec (_, _, tm) = prod False tm
179+ prodRec n done (_, _, tm) = prod n done False tm
177−
180+
181+ prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
178− prod ok ap@(App _ _)
182+ prod n done ok ap@(App _ _)
179− | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod ok arg
183+ | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod n done ok arg
180− | (P nt f ty, args) <- unApply ap
184+ | (P nt f _, args) <- unApply ap
185+ = do recOK <- checkProdRec (n:done) f
186+ let ctxt = tt_ctxt i
187+ let [ty] = lookupTy f ctxt -- must exist!
181− = let co = cotype nt ty in
188+ let co = cotype nt f ty in
189+ if (not recOK) then return False else
182− if f == n
190+ if f == topn
183− then do argsprod <- mapM (prod co) args
191+ then do argsprod <- mapM (prod n done co) args
184− return (and (ok : argsprod) )
192+ return (and (ok : argsprod) )
185− else do argsprod <- mapM (prod co) args
193+ else do argsprod <- mapM (prod n done co) args
186− return (and argsprod)
194+ return (and argsprod)
187− prod ok (App f a) = liftM2 (&&) (prod False f) (prod False a)
195+ prod n done ok (App f a) = liftM2 (&&) (prod n done False f)
196+ (prod n done False a)
197+ prod n done ok (Bind _ (Let t v) sc)
188− prod ok (Bind _ (Let t v) sc) = liftM2 (&&) (prod False v) (prod False v)
198+ = liftM2 (&&) (prod n done False v) (prod n done False v)
189− prod ok (Bind _ b sc) = prod ok sc
199+ prod n done ok (Bind _ b sc) = prod n done ok sc
190− prod ok t = return True
200+ prod n done ok t = return True
191−
201+
202+ checkProdRec :: [Name] -> Name -> Idris Bool
203+ checkProdRec done f
204+ = case lookupCtxt f (idris_patdefs i) of
205+ [(def, _)] -> do ok <- mapM (prodRec f done) def
206+ return (and ok)
207+ _ -> return True -- defined elsewhere, can't call topn
208+
192− cotype (DCon _ _) ty
209+ cotype (DCon _ _) n ty
193 | (P _ t _, _) <- unApply (getRetTy ty)
210 | (P _ t _, _) <- unApply (getRetTy ty)
194 = case lookupCtxt t (idris_datatypes i) of
211 = case lookupCtxt t (idris_datatypes i) of
195 [TI _ True _] -> True
212 [TI _ True _] -> True
196 _ -> False
213 _ -> False
197− cotype _ _ = False
214+ cotype nt n ty = False
198
215
199calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
216calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
200 -> Idris Totality
217 -> Idris Totality
test/reg018/expectednew file+3
@@ -0,0 +1,3 @@
1+reg018a.idr:16:conat.minusCoNat is not productive
2+reg018b.idr:8:A.showB is possibly not total due to recursive path A.showB
3+reg018c.idr:19:CodataTest.inf is not productive
test/reg018/reg018a.idrnew file+21
@@ -0,0 +1,21 @@
1+module conat
2+
3+%default total
4+
5+codata CoNat = Z | S CoNat
6+
7+infinity : CoNat
8+infinity = S infinity
9+
10+plusCoNat : CoNat -> CoNat -> CoNat
11+plusCoNat Z x = x
12+plusCoNat (S x) y = S (plusCoNat x y)
13+
14+--I don't think this should be definable
15+minusCoNat : CoNat -> CoNat -> CoNat
16+minusCoNat Z n = Z
17+minusCoNat (S n) Z = S n
18+minusCoNat (S n) (S m) = plusCoNat Z (minusCoNat n m)
19+
20+loopForever : CoNat
21+loopForever = minusCoNat infinity infinity
test/reg018/reg018b.idrnew file+14
@@ -0,0 +1,14 @@
1+module A
2+
3+%default total
4+
5+codata B = O B | I B
6+
7+showB : B -> String
8+showB (I x) = "I" ++ showB x
9+showB (O x) = "O" ++ showB x
10+
11+instance Show B where show = showB
12+
13+os : B
14+os = O os
test/reg018/reg018c.idrnew file+20
@@ -0,0 +1,20 @@
1+module CodataTest
2+%default total
3+
4+codata InfStream a = (::) a (InfStream a)
5+--
6+-- natStream : InfStream Nat
7+-- natStream = natFromStream 0 where
8+-- natFromStream : Nat -> InfStream Nat
9+-- natFromStream n = (::) n (natFromStream (S n))
10+
11+take : (n: Nat) -> InfStream a -> Vect a n
12+take O _ = []
13+take (S n) (x :: xs) = x :: take n xs
14+
15+hdtl : InfStream a -> (a, InfStream a)
16+hdtl (x :: xs) = (x, xs)
17+
18+inf : InfStream a -> InfStream a
19+inf (x :: xs) with (hdtl xs)
20+ | (hd, tl) = inf xs
test/reg018/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris $@ reg018a.idr --check
3+idris $@ reg018b.idr --check
4+idris $@ reg018c.idr --check