git.iko.soy/Idris-dev
on master help sign in
Productivity check fix
0a4f002Edwin Brady
idris.cabal+1
compare with master
unifiedsplit
@@ -56,6 +56,7 @@ Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h
56Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
56Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
57 lib/Network/*.idr lib/Control/*.idr
57 lib/Network/*.idr lib/Control/*.idr
58 lib/Control/Monad/*.idr lib/Language/*.idr
58 lib/Control/Monad/*.idr lib/Language/*.idr
59+ lib/Language/Reflection/*.idr
59 lib/System/Concurrency/*.idr
60 lib/System/Concurrency/*.idr
60 lib/Data/*.idr lib/Debug/*.idr
61 lib/Data/*.idr lib/Debug/*.idr
61 lib/Data/Vect/*.idr
62 lib/Data/Vect/*.idr
src/Idris/Coverage.hs+6−11
@@ -162,12 +162,6 @@ checkPositive n (cn, ty)
162 = n /= n' && posArg sc
162 = n /= n' && posArg sc
163 posArg t = True
163 posArg t = True
164
164
165−-- Totality checking - check for structural recursion
166−-- (no mutual definitions yet)
167−
168−data LexOrder = LexXX | LexEQ | LexLT
169− deriving (Show, Eq, Ord)
170−
171calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
165calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
172calcProd i fc n pats = do patsprod <- mapM prodRec pats
166calcProd i fc n pats = do patsprod <- mapM prodRec pats
173 if (and patsprod)
167 if (and patsprod)
@@ -175,15 +169,16 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats
175 else return (Partial NotProductive)
169 else return (Partial NotProductive)
176 where
170 where
177 -- every application of n must be in an argument of a coinductive
171 -- every application of n must be in an argument of a coinductive
178− -- constructor
172+ -- constructor, in every function reachable from here in the
173+ -- call graph.
179
174
180 prodRec :: ([Name], Term, Term) -> Idris Bool
175 prodRec :: ([Name], Term, Term) -> Idris Bool
181 prodRec (_, _, tm) = prod False tm
176 prodRec (_, _, tm) = prod False tm
182
177
183 prod ok ap@(App _ _)
178 prod ok ap@(App _ _)
184 | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod ok arg
179 | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod ok arg
185− | (P _ f ty, args) <- unApply ap
180+ | (P nt f ty, args) <- unApply ap
186− = let co = cotype ty in
181+ = let co = cotype nt ty in
187 if f == n
182 if f == n
188 then do argsprod <- mapM (prod co) args
183 then do argsprod <- mapM (prod co) args
189 return (and (ok : argsprod) )
184 return (and (ok : argsprod) )
@@ -194,12 +189,12 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats
194 prod ok (Bind _ b sc) = prod ok sc
189 prod ok (Bind _ b sc) = prod ok sc
195 prod ok t = return True
190 prod ok t = return True
196
191
197− cotype ty
192+ cotype (DCon _ _) ty
198 | (P _ t _, _) <- unApply (getRetTy ty)
193 | (P _ t _, _) <- unApply (getRetTy ty)
199 = case lookupCtxt t (idris_datatypes i) of
194 = case lookupCtxt t (idris_datatypes i) of
200 [TI _ True _] -> True
195 [TI _ True _] -> True
201 _ -> False
196 _ -> False
202− | otherwise = False
197+ cotype _ _ = False
203
198
204calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
199calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
205 -> Idris Totality
200 -> Idris Totality