git.iko.soy/Idris-dev
on cb005bc help sign in
Idris-dev/src/Idris/Coverage.hs
736 lines 32 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Coverage where
5import Idris.Core.TT
6import Idris.Core.Evaluate
7import Idris.Core.CaseTree
9import Idris.AbsSyntax
10import Idris.Delaborate
11import Idris.Error
12import Idris.Output (iWarn, iputStrLn)
14import Data.List
15import Data.Either
16import Data.Maybe
17import Debug.Trace
19import Control.Monad.State.Strict
21-- Generate a pattern from an 'impossible' LHS. (Need this to eliminate the
22-- pattern clauses which have been provided explicitly from new clause
23-- generation.)
25mkPatTm :: PTerm -> Idris Term
26mkPatTm t = do i <- getIState
27 let timp = addImpl' True [] [] i t
28 evalStateT (toTT (mapPT deNS timp)) 0
29 where
30 toTT (PRef _ n) = do i <- lift getIState
31 case lookupDef n (tt_ctxt i) of
32 [TyDecl nt _] -> return $ P nt n Erased
33 _ -> return $ P Ref n Erased
34 toTT (PApp _ t args) = do t' <- toTT t
35 args' <- mapM (toTT . getTm) args
36 return $ mkApp t' args'
37 -- For alternatives, pick the first and drop the namespaces. It doesn't
38 -- really matter which is taken since matching will ignore the namespace.
39 toTT (PAlternative _ (a : as)) = toTT a
40 toTT _ = do v <- get
41 put (v + 1)
42 return (P Bound (sMN v "imp") Erased)
44 deNS (PRef f (NS n _)) = PRef f n
45 deNS t = t
47-- Given a list of LHSs, generate a extra clauses which cover the remaining
48-- cases. The ones which haven't been provided are marked 'absurd' so that the
49-- checker will make sure they can't happen.
51-- This will only work after the given clauses have been typechecked and the
52-- names are fully explicit!
54genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
55genClauses fc n xs given
56 = do i <- getIState
57 let lhs_tms = map (\x -> delab' i x True True) xs
58 -- if a placeholder was given, don't bother generating cases for it
59 let lhs_tms' = zipWith mergePlaceholders lhs_tms
60 (map (stripUnmatchable i) given)
61 let lhss = map pUnApply lhs_tms'
63 let argss = transpose lhss
64 let all_args = map (genAll i) argss
65 logLvl 5 $ "COVERAGE of " ++ show n
66 logLvl 5 $ show lhss
67 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
68 logLvl 10 $ show argss ++ "\n" ++ show all_args
69 logLvl 3 $ "Original: \n" ++
70 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
71 -- add an infinite supply of explicit arguments to update the possible
72 -- cases for (the return type may be variadic, or function type, so
73 -- there may be more case splitting that the idris_implicits record
74 -- suggests)
75 let parg = case lookupCtxt n (idris_implicits i) of
76 (p : _) ->
77 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)
78 _ -> repeat (pexp Placeholder)
79 let tryclauses = mkClauses parg all_args
80 logLvl 3 $ show (length tryclauses) ++ " initially to check"
81 logLvl 2 $ showSep "\n" (map (showTm i) tryclauses)
82 let new = filter (noMatch i) (nub tryclauses)
83 logLvl 2 $ show (length new) ++ " clauses to check for impossibility"
84 logLvl 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
85-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
86 return new
87-- return (map (\t -> PClause n t [] PImpossible []) new)
88 where getLHS i term
89 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
90 | otherwise = []
92 pUnApply (PApp _ _ args) = map getTm args
93 pUnApply _ = []
95 -- Return whether the given clause matches none of the input clauses
96 -- (xs)
97 noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of
98 Right ms -> False
99 Left miss -> True) xs
102 mergePlaceholders :: PTerm -> PTerm -> PTerm
103 mergePlaceholders x Placeholder = Placeholder
104 mergePlaceholders (PApp fc f args) (PApp fc' f' args')
105 = PApp fc' f' (zipWith mergePArg args args')
106 where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in
107 x { getTm = xtm}
108 mergePlaceholders x _ = x
110 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
111 mkClauses parg args
112 | all (== [Placeholder]) args = []
113 mkClauses parg args
114 = do args' <- mkArg args
115 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
116 return tm
117 where
118 mkArg :: [[PTerm]] -> [[PTerm]]
119 mkArg [] = return []
120 mkArg (a : as) = do a' <- a
121 as' <- mkArg as
122 return (a':as')
124-- FIXME: Just look for which one is the deepest, then generate all
125-- possibilities up to that depth.
126-- This and below issues for this function are tracked as Issue #1741 on the issue tracker.
127-- https://github.com/idris-lang/Idris-dev/issues/1741
128genAll :: IState -> [PTerm] -> [PTerm]
129genAll i args
130 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
131 [] -> [Placeholder]
132 xs -> inventConsts xs
133 where
134 -- if they're constants, invent a new one to make sure that
135 -- constants which are not explicitly handled are covered
136 inventConsts cs@(PConstant c : _) = map PConstant (ic' (mapMaybe getConst cs))
137 where getConst (PConstant c) = Just c
138 getConst _ = Nothing
139 inventConsts xs = xs
141 -- try constants until they're not in the list.
142 -- FIXME: It is, of course, possible that someone has enumerated all
143 -- the constants and matched on them (maybe in generated code) and this
144 -- will be really slow. This is sufficiently unlikely that we won't
145 -- worry for now...
147 ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I)
148 ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)
149 ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl)
150 ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8)
151 ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16)
152 ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32)
153 ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
154 ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
155 ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
156 -- TODO: Bit vectors
157 -- The rest are types with only one case
158 ic' xs = xs
160 firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs
161 | otherwise = x : cs
163 lotsOfNums t = map t [0..]
164 lotsOfChars = map Ch ['a'..]
165 lotsOfStrings = map Str (map (("some string " ++).show) [1..])
167 nubMap f acc [] = acc
168 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
170 otherPats :: PTerm -> [PTerm]
171 otherPats o@(PRef fc n) = ops fc n [] o
172 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
173 otherPats o@(PPair fc _ l r)
174 = ops fc pairCon
175 ([pimp (sUN "A") Placeholder True,
176 pimp (sUN "B") Placeholder True] ++
177 [pexp l, pexp r]) o
178 otherPats o@(PDPair fc p t _ v)
179 = ops fc (sUN "Ex_intro")
180 ([pimp (sUN "a") Placeholder True,
181 pimp (sUN "P") Placeholder True] ++
182 [pexp t,pexp v]) o
183 otherPats o@(PConstant c) = inventConsts [o] -- return o
184 otherPats arg = return Placeholder
186 ops fc n xs o
187 | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)
188 = do xs' <- mapM otherPats (map getExpTm xs)
189 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))
190 let tyn = getTy n (tt_ctxt i)
191 case lookupCtxt tyn (idris_datatypes i) of
192 (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
193 _ -> [p]
194 ops fc n arg o = return Placeholder
196 getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
197 getExpTm t = getTm t
199 -- put it back to its original form
200 resugar (PApp _ (PRef fc (UN ei)) [_,_,t,v])
201 | ei == txt "Ex_intro"
202 = PDPair fc TypeOrTerm (getTm t) Placeholder (getTm v)
203 resugar (PApp _ (PRef fc n) [_,_,l,r])
204 | n == pairCon
205 = PPair fc IsTerm (getTm l) (getTm r)
206 resugar t = t
208 dropForce force (x : xs) i | i `elem` force
209 = upd Placeholder x : dropForce force xs (i + 1)
210 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
211 dropForce _ [] _ = []
214 getTy n ctxt = case lookupTy n ctxt of
215 (t : _) -> case unApply (getRetTy t) of
216 (P _ tyn _, _) -> tyn
217 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
218 _ -> error "Can't happen getTy 2"
220 mkPat fc x = case lookupCtxt x (idris_implicits i) of
221 (pargs : _)
222 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
223 _ -> error "Can't happen - genAll"
225 fnub :: [PTerm] -> [PTerm]
226 fnub xs = fnub' [] xs
228 fnub' :: [PTerm] -> [PTerm] -> [PTerm]
229 fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
230 | otherwise = fnub' (x : acc) xs
231 fnub' acc [] = acc
233 -- quick check for constructor equality
234 quickEq :: PTerm -> PTerm -> Bool
235 quickEq (PConstant n) (PConstant n') = n == n'
236 quickEq (PRef _ n) (PRef _ n') = n == n'
237 quickEq (PApp _ t as) (PApp _ t' as')
238 | length as == length as'
239 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
240 quickEq Placeholder Placeholder = True
241 quickEq x y = False
243 qelem :: PTerm -> [PTerm] -> Bool
244 qelem x [] = False
245 qelem x (y : ys) | x `quickEq` y = True
246 | otherwise = qelem x ys
249upd :: t -> PArg' t -> PArg' t
250upd p' p = p { getTm = p' }
252-- Check whether function and all descendants cover all cases (partial is
253-- okay, as long as it's due to recursion)
255checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
256checkAllCovering fc done top n | not (n `elem` done)
257 = do i <- get
258 case lookupTotal n (tt_ctxt i) of
259 [tot@(Partial NotCovering)] ->
260 do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n
261 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }
262 addIBC (IBCTotCheckErr fc msg)
263 [Partial _] ->
264 case lookupCtxt n (idris_callgraph i) of
265 [cg] -> mapM_ (checkAllCovering fc (n : done) top)
266 (map fst (calls cg))
267 _ -> return ()
268 x -> return () -- stop if total
269checkAllCovering _ _ _ _ = return ()
271-- Check if, in a given group of type declarations mut_ns,
272-- the constructor cn : ty is strictly positive,
273-- and update the context accordingly
275checkPositive :: [Name] -> (Name, Type) -> Idris Totality
276checkPositive mut_ns (cn, ty')
277 = do let ty = delazy' True ty'
278 let p = cp ty
279 i <- getIState
280 let tot = if p then Total (args ty) else Partial NotPositive
281 let ctxt' = setTotal cn tot (tt_ctxt i)
282 putIState (i { tt_ctxt = ctxt' })
283 logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns
284 addIBC (IBCTotal cn tot)
285 return tot
286 where
287 args t = [0..length (getArgTys t)-1]
289 cp (Bind n (Pi _ aty _) sc) = posArg aty && cp sc
290 cp t | (P _ n' _, args) <- unApply t,
291 n' `elem` mut_ns = all noRec args
292 cp _ = True
294 posArg (Bind _ (Pi _ nty _) sc)
295 | (P _ n' _, args) <- unApply nty
296 = n' `notElem` mut_ns && all noRec args && posArg sc
297 posArg t | (P _ n' _, args) <- unApply t,
298 n' `elem` mut_ns = all noRec args
299 posArg _ = True
301 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
304calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
305calcProd i fc topn pats
306 = cp topn pats []
307 where
308 -- every application of n must be in an argument of a coinductive
309 -- constructor, in every function reachable from here in the
310 -- call graph.
311 cp n pats done = do patsprod <- mapM (prodRec n done) pats
312 if (and patsprod)
313 then return Productive
314 else return (Partial NotProductive)
316 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
317 prodRec n done _ | n `elem` done = return True
318 prodRec n done (_, _, tm) = prod n done False (delazy' True tm)
320 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
321 prod n done ok ap@(App _ _)
322 | (P nt f _, args) <- unApply ap
323 = do recOK <- checkProdRec (n:done) f
324 let ctxt = tt_ctxt i
325 let [ty] = lookupTy f ctxt -- must exist!
326 let co = cotype nt f ty in
327 if (not recOK) then return False else
328 if f == topn
329 then do argsprod <- mapM (prod n done co) args
330 return (and (ok : argsprod) )
331 else do argsprod <- mapM (prod n done co) args
332 return (and argsprod)
333 prod n done ok (App f a) = liftM2 (&&) (prod n done False f)
334 (prod n done False a)
335 prod n done ok (Bind _ (Let t v) sc)
336 = liftM2 (&&) (prod n done False v) (prod n done False v)
337 prod n done ok (Bind _ b sc) = prod n done ok sc
338 prod n done ok t = return True
340 checkProdRec :: [Name] -> Name -> Idris Bool
341 checkProdRec done f
342 = case lookupCtxt f (idris_patdefs i) of
343 [(def, _)] -> do ok <- mapM (prodRec f done) def
344 return (and ok)
345 _ -> return True -- defined elsewhere, can't call topn
347 cotype (DCon _ _ _) n ty
348 | (P _ t _, _) <- unApply (getRetTy ty)
349 = case lookupCtxt t (idris_datatypes i) of
350 [TI _ True _ _ _] -> True
351 _ -> False
352 cotype nt n ty = False
354-- Calculate the totality of a function from its patterns.
355-- Either follow the size change graph (if inductive) or check for
356-- productivity (if coinductive)
358calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
359calcTotality fc n pats
360 = do i <- getIState
361 let opts = case lookupCtxt n (idris_flags i) of
362 [fs] -> fs
363 _ -> []
364 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
365 (failure : _) -> return failure
366 _ -> checkSizeChange n
367 where
368 checkLHS i (P _ fn _)
369 = case lookupTotal fn (tt_ctxt i) of
370 [Partial _] -> return (Partial (Other [fn]))
371 _ -> Nothing
372 checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)
373 checkLHS _ _ = Nothing
375checkTotality :: [Name] -> FC -> Name -> Idris Totality
376checkTotality path fc n
377 | n `elem` path = return (Partial (Mutual (n : path)))
378 | otherwise = do
379 t <- getTotality n
380 i <- getIState
381 updateContext (simplifyCasedef n $ getErasureInfo i)
382 ctxt <- getContext
383 i <- getIState
384 let opts = case lookupCtxt n (idris_flags i) of
385 [fs] -> fs
386 _ -> []
387 t' <- case t of
388 Unchecked ->
389 case lookupDef n ctxt of
390 [CaseOp _ _ _ _ pats _] ->
391 do t' <- if AssertTotal `elem` opts
392 then return $ Total []
393 else calcTotality fc n pats
394 setTotality n t'
395 addIBC (IBCTotal n t')
396 return t'
397 [TyDecl (DCon _ _ _) ty] ->
398 case unApply (getRetTy ty) of
399 (P _ tyn _, _) -> do
400 let ms = case lookupCtxt tyn (idris_datatypes i) of
401 [TI _ _ _ _ xs@(_:_)] -> xs
402 ts -> [tyn]
403 checkPositive ms (n, ty)
404 _-> return $ Total []
405 _ -> return $ Total []
406 x -> return x
407 case t' of
408 Total _ -> return t'
409 Productive -> return t'
410 e -> do w <- cmdOptType WarnPartial
411 if TotalFn `elem` opts
412 then do totalityError t'; return t'
413 else do when (w && not (PartialFn `elem` opts)) $
414 warnPartial n t'
415 return t'
416 where
417 totalityError t = do i <- getIState
418 let msg = show n ++ " is " ++ show t
419 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}
420 addIBC (IBCTotCheckErr fc msg)
422 warnPartial n t
423 = do i <- getIState
424 case lookupDef n (tt_ctxt i) of
425 [x] -> do
426 iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t
427-- ++ "\n" ++ show x
428-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
429-- iputStrLn (show cg)
432checkDeclTotality :: (FC, Name) -> Idris Totality
433checkDeclTotality (fc, n)
434 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
435-- buildSCG (fc, n)
436-- logLvl 2 $ "Built SCG"
437 i <- getIState
438 let opts = case lookupCtxt n (idris_flags i) of
439 [fs] -> fs
440 _ -> []
441 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
442 t <- checkTotality [] fc n
443 case t of
444 -- if it's not total, it can't reduce, to keep
445 -- typechecking decidable
446 p@(Partial _) -> do setAccessibility n Frozen
447 addIBC (IBCAccess n Frozen)
448 logLvl 5 $ "HIDDEN: "
449 ++ show n ++ show p
450 _ -> return ()
451 return t
454-- Calculate the size change graph for this definition
456-- SCG for a function f consists of a list of:
457-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
459-- where g is a function called
460-- a1 ... an are the arguments of f in positions 1..n of g
461-- sizechange1 ... sizechange2 is how their size has changed wrt the input
462-- to f
463-- Nothing, if the argument is unrelated to the input
465buildSCG :: (FC, Name) -> Idris ()
466buildSCG (_, n) = do
467 ist <- getIState
468 case lookupCtxt n (idris_callgraph ist) of
469 [cg] -> case lookupDefExact n (tt_ctxt ist) of
470 Just (CaseOp _ _ _ pats _ cd) ->
471 let (args, sc) = cases_totcheck cd in
472 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
473 ++ show pats ++ "\n" ++ show sc
474 let newscg = buildSCG' ist (rights pats) args
475 logLvl 5 $ "SCG is: " ++ show newscg
476 addToCG n ( cg { scg = newscg } )
477 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
478 x -> error $ "buildSCG: " ++ show (n, x)
480delazy = delazy' False -- not lazy codata
481delazy' all t@(App f a)
482 | (P _ (UN l) _, [_, _, arg]) <- unApply t,
483 l == txt "Force" = delazy' all arg
484 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
485 l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg
486 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
487 l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg
488delazy' all (App f a) = App (delazy' all f) (delazy' all a)
489delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
490delazy' all t = t
492data Guardedness = Toplevel | Unguarded | Guarded
493 deriving Show
495buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
496buildSCG' ist pats args = nub $ concatMap scgPat pats where
497 scgPat (lhs, rhs) = let lhs' = delazy lhs
498 rhs' = delazy rhs
499 (f, pargs) = unApply (dePat lhs') in
500 findCalls Toplevel (dePat rhs') (patvars lhs') pargs
502 findCalls guarded ap@(App f a) pvs pargs
503 -- under a call to "assert_total", don't do any checking, just believe
504 -- that it is total.
505 | (P _ (UN at) _, [_, _]) <- unApply ap,
506 at == txt "assert_total" = []
507 -- under a call to "Delay LazyCodata", don't do any checking of the
508 -- immediate call, as long as the call is guarded.
509 -- Then check its arguments
510 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
511 Guarded <- guarded,
512 del == txt "Delay"
513 = let (capp, args) = unApply arg in
514 concatMap (\x -> findCalls guarded x pvs pargs) args
515 | (P _ n _, args) <- unApply ap
516 = let nguarded = case guarded of
517 Unguarded -> Unguarded
518 _ -> if isConName n (tt_ctxt ist)
519 then Guarded
520 else Unguarded in
521 mkChange n args pargs ++
522 concatMap (\x -> findCalls nguarded x pvs pargs) args
523 findCalls guarded (App f a) pvs pargs
524 = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs
525 findCalls guarded (Bind n (Let t v) e) pvs pargs
526 = findCalls Unguarded t pvs pargs ++
527 findCalls Unguarded v pvs pargs ++ findCalls guarded e (n : pvs) pargs
528 findCalls guarded (Bind n t e) pvs pargs
529 = findCalls Unguarded (binderTy t) pvs pargs ++
530 findCalls guarded e (n : pvs) pargs
531 findCalls guarded (P _ f _ ) pvs pargs
532 | not (f `elem` pvs) = [(f, [])]
533 findCalls _ _ _ _ = []
535 expandToArity n args
536 = case lookupTy n (tt_ctxt ist) of
537 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
538 _ -> args
539 where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
540 expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []
541 expand i _ xs = xs
543 mkChange n args pargs = [(n, expandToArity n (sizes args))]
544 where
545 sizes [] = []
546 sizes (a : as) = checkSize a pargs 0 : sizes as
548 -- find which argument in pargs <a> is smaller than, if any
549 checkSize a (p : ps) i
550 | a == p = Just (i, Same)
551 | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
552 as == txt "assert_smaller" && arg == p
553 = Just (i, Smaller)
554 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
555 | otherwise = checkSize a ps (i + 1)
556 checkSize a [] i = Nothing
558 -- the smaller thing we find must be the same type as <a>, and
559 -- not be coinductive - so carry the type of the constructor we've
560 -- gone under.
562 smaller (Just tyn) a (t, Just tyt)
563 | a == t = isInductive (fst (unApply (getRetTy tyn)))
564 (fst (unApply (getRetTy tyt)))
565 smaller ty a (ap@(App f s), _)
566 | (P (DCon _ _ _) n _, args) <- unApply ap
567 = let tyn = getType n in
568 any (smaller (ty `mplus` Just tyn) a)
569 (zip args (map toJust (getArgTys tyn)))
570 -- check higher order recursive arguments
571 smaller ty (App f s) a = smaller ty f a
572 smaller _ _ _ = False
574 toJust (n, t) = Just t
576 getType n = case lookupTy n (tt_ctxt ist) of
577 [ty] -> delazy ty -- must exist
579 isInductive (P _ nty _) (P _ nty' _) =
580 let co = case lookupCtxt nty (idris_datatypes ist) of
581 [TI _ x _ _ _] -> x
582 _ -> False in
583 nty == nty' && not co
584 isInductive _ _ = False
586 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
587 dePat t = t
589 patvars (Bind x (PVar _) sc) = x : patvars sc
590 patvars _ = []
592checkSizeChange :: Name -> Idris Totality
593checkSizeChange n = do
594 ist <- getIState
595 case lookupCtxt n (idris_callgraph ist) of
596 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
597 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
598 "from " ++ show (scg cg) ++ "\n" ++
599 show (length ms) ++ "\n" ++
600 showSep "\n" (map show ms))
601 logLvl 6 (show cg)
602 -- every multipath must have an infinitely descending
603 -- thread, then the function terminates
604 -- also need to checks functions called are all total
605 -- (Unchecked is okay as we'll spot problems here)
606 let tot = map (checkMP ist (getArity ist n)) ms
607 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"
608 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
609 return (noPartial tot)
610 [] -> do logLvl 5 $ "No paths for " ++ show n
611 return Unchecked
612 where getArity ist n
613 = case lookupTy n (tt_ctxt ist) of
614 [ty] -> arity (normalise (tt_ctxt ist) [] ty)
615 _ -> error "Can't happen: checkSizeChange.getArity"
617type MultiPath = [SCGEntry]
619mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
620mkMultiPaths ist path [] = [reverse path]
621mkMultiPaths ist path cg
622 = concat (map extend cg)
623 where extend (nextf, args)
624 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
625 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
626 = case lookupCtxt nextf (idris_callgraph ist) of
627 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
628 _ -> [ reverse ((nextf, args) : path) ]
629 | otherwise = [ reverse ((nextf, args) : path) ]
631-- do (nextf, args) <- cg
632-- if ((nextf, args) `elem` path)
633-- then return (reverse ((nextf, args) : path))
634-- else case lookupCtxt nextf (idris_callgraph ist) of
635-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
636-- _ -> return (reverse ((nextf, args) : path))
638-- If any route along the multipath leads to infinite descent, we're fine.
639-- Try a route beginning with every argument.
640-- If we reach a point we've been to before, but with a smaller value,
641-- that means there is an infinitely descending path from that argument.
643checkMP :: IState -> Int -> MultiPath -> Totality
644checkMP ist i mp = if i > 0
645 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
646-- trace ("Paths " ++ show paths) $
647 collapse paths
648 else tryPath 0 [] mp 0
649 where
650 tryPath' d path mp arg
651 = let res = tryPath d path mp arg in
652 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
654 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
655 tryPath desc path [] _ = Total []
656-- tryPath desc path ((UN "believe_me", _) : _) arg
657-- = Partial BelieveMe
658 -- if we get to a constructor, it's fine as long as it's strictly positive
659 tryPath desc path ((f, _) : es) arg
660 | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
661 = case lookupTotal f (tt_ctxt ist) of
662 [Total _] -> Unchecked -- okay so far
663 [Partial _] -> Partial (Other [f])
664 x -> error $ "CAN'T HAPPEN: " ++ (show x)
665 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
666 = Total []
667 tryPath desc path (e@(f, args) : es) arg
668 | e `elem` es && allNothing args = Partial (Mutual [f])
669 tryPath desc path (e@(f, nextargs) : es) arg
670 | Just d <- lookup (e, arg) path
671 = if desc > 0
672 then -- trace ("Descent " ++ show (desc - d) ++ " "
673 -- ++ show (path, e)) $
674 Total []
675 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
676 | e `elem` map (fst . fst) path
677 && not (f `elem` map fst es)
678 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
679 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
680 let argspos = case collapseNothing (zip nextargs [0..]) of
681 [] -> [(Nothing, 0)]
682 x -> x
683-- trace (show (argspos, nextargs, path)) $
684 pathres =
685 do (a, pos) <- argspos
686 case a of
687 Nothing -> -- don't know, but if the
688 -- rest definitely terminates without
689 -- any cycles with route so far,
690 -- then we might yet be total
691 case collapse (map (tryPath 0 (((e, arg), 0):path) es)
692 [0..length nextargs - 1]) of
693 Total _ -> return Unchecked
694 x -> return x
695 Just (nextarg, sc) ->
696 if nextarg == arg then
697 case sc of
698 Same -> return $ tryPath desc (((e, arg), desc) : path)
699 es pos
700 Smaller -> return $ tryPath (desc+1)
701 (((e, arg), desc) : path)
702 es
703 pos
704 _ -> trace ("Shouldn't happen " ++ show e) $
705 return (Partial Itself)
706 else return Unchecked in
707-- trace (show (desc, argspos, path, es, pathres)) $
708 collapse' Unchecked pathres
710 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
711 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
712 | otherwise = Unchecked
714allNothing :: [Maybe a] -> Bool
715allNothing xs = null (collapseNothing (zip xs [0..]))
717collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
718collapseNothing ((Nothing, _) : xs)
719 = filter (\ (x, _) -> case x of
720 Nothing -> False
721 _ -> True) xs
722collapseNothing (x : xs) = x : collapseNothing xs
723collapseNothing [] = []
725noPartial :: [Totality] -> Totality
726noPartial (Partial p : xs) = Partial p
727noPartial (_ : xs) = noPartial xs
728noPartial [] = Total []
730collapse :: [Totality] -> Totality
731collapse xs = collapse' Unchecked xs
732collapse' def (Total r : xs) = Total r
733collapse' def (Unchecked : xs) = collapse' def xs
734collapse' def (d : xs) = collapse' d xs
735-- collapse' Unchecked [] = Total []
736collapse' def [] = def