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