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