@@ -163,38 +163,55 @@ checkPositive n (cn, ty)
163163 posArg t = True
164164
165165calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
166−calcProd i fc n pats = do patsprod <- mapM prodRec pats
167− if (and patsprod)
168− then return Productive
169− else return (Partial NotProductive)
166+calcProd i fc topn pats
167+ = cp topn pats []
170168 where
171169 -- every application of n must be in an argument of a coinductive
172170 -- constructor, in every function reachable from here in the
173171 -- call graph.
174−
175− prodRec :: ([Name], Term, Term) -> Idris Bool
176− prodRec (_, _, tm) = prod False tm
177−
178− prod ok ap@(App _ _)
179− | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod ok arg
180− | (P nt f ty, args) <- unApply ap
181− = let co = cotype nt ty in
182− if f == n
183− then do argsprod <- mapM (prod co) args
184− return (and (ok : argsprod) )
185− else do argsprod <- mapM (prod co) args
186− return (and argsprod)
187− prod ok (App f a) = liftM2 (&&) (prod False f) (prod False a)
188− prod ok (Bind _ (Let t v) sc) = liftM2 (&&) (prod False v) (prod False v)
189− prod ok (Bind _ b sc) = prod ok sc
190− prod ok t = return True
191−
192− cotype (DCon _ _) ty
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+
177+ prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
178+ prodRec n done _ | n `elem` done = return True
179+ prodRec n done (_, _, tm) = prod n done False tm
180+
181+ prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
182+ prod n done ok ap@(App _ _)
183+ | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod n done ok arg
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!
188+ let co = cotype nt f ty in
189+ if (not recOK) then return False else
190+ if f == topn
191+ then do argsprod <- mapM (prod n done co) args
192+ return (and (ok : argsprod) )
193+ else do argsprod <- mapM (prod n done co) args
194+ return (and argsprod)
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)
198+ = liftM2 (&&) (prod n done False v) (prod n done False v)
199+ prod n done ok (Bind _ b sc) = prod n done ok sc
200+ prod n done ok t = return True
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+
209+ cotype (DCon _ _) n ty
193210 | (P _ t _, _) <- unApply (getRetTy ty)
194211 = case lookupCtxt t (idris_datatypes i) of
195212 [TI _ True _] -> True
196213 _ -> False
197− cotype _ _ = False
214+ cotype nt n ty = False
198215
199216calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
200217 -> Idris Totality