git.iko.soy/Idris-dev
on b87820d help sign in
Idris-dev/src/Idris/Coverage.hs
746 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 return t
464-- | Calculate the size change graph for this definition
465--
466-- SCG for a function f consists of a list of:
467-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
468--
469-- where g is a function called
470-- a1 ... an are the arguments of f in positions 1..n of g
471-- sizechange1 ... sizechange2 is how their size has changed wrt the input
472-- to f
473-- Nothing, if the argument is unrelated to the input
474buildSCG :: (FC, Name) -> Idris ()
475buildSCG (_, n) = do
476 ist <- getIState
477 case lookupCtxt n (idris_callgraph ist) of
478 [cg] -> case lookupDefExact n (tt_ctxt ist) of
479 Just (CaseOp _ _ _ pats _ cd) ->
480 let (args, sc) = cases_totcheck cd in
481 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"
482 ++ show pats ++ "\n" ++ show sc
483 let newscg = buildSCG' ist (rights pats) args
484 logCoverage 5 $ "SCG is: " ++ show newscg
485 addToCG n ( cg { scg = newscg } )
486 _ -> return () -- CG comes from a type declaration only
487 [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"
488 x -> error $ "buildSCG: " ++ show (n, x)
490delazy = delazy' False -- not lazy codata
491delazy' all t@(App _ f a)
492 | (P _ (UN l) _, [_, _, arg]) <- unApply t,
493 l == txt "Force" = delazy' all arg
494 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
495 l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg
496 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
497 l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg
498delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
499delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
500delazy' all t = t
502data Guardedness = Toplevel | Unguarded | Guarded
503 deriving Show
505buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
506buildSCG' ist pats args = nub $ concatMap scgPat pats where
507 scgPat (lhs, rhs) = let lhs' = delazy lhs
508 rhs' = delazy rhs
509 (f, pargs) = unApply (dePat lhs') in
510 findCalls Toplevel (dePat rhs') (patvars lhs') pargs
512 findCalls guarded ap@(App _ f a) pvs pargs
513 -- under a call to "assert_total", don't do any checking, just believe
514 -- that it is total.
515 | (P _ (UN at) _, [_, _]) <- unApply ap,
516 at == txt "assert_total" = []
517 -- under a call to "Delay LazyCodata", don't do any checking of the
518 -- immediate call, as long as the call is guarded.
519 -- Then check its arguments
520 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
521 Guarded <- guarded,
522 del == txt "Delay"
523 = let (capp, args) = unApply arg in
524 concatMap (\x -> findCalls guarded x pvs pargs) args
525 | (P _ n _, args) <- unApply ap
526 = let nguarded = case guarded of
527 Unguarded -> Unguarded
528 _ -> if isConName n (tt_ctxt ist)
529 then Guarded
530 else Unguarded in
531 mkChange n args pargs ++
532 concatMap (\x -> findCalls nguarded x pvs pargs) args
533 findCalls guarded (App _ f a) pvs pargs
534 = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs
535 findCalls guarded (Bind n (Let t v) e) pvs pargs
536 = findCalls Unguarded t pvs pargs ++
537 findCalls Unguarded v pvs pargs ++ findCalls guarded e (n : pvs) pargs
538 findCalls guarded (Bind n t e) pvs pargs
539 = findCalls Unguarded (binderTy t) pvs pargs ++
540 findCalls guarded e (n : pvs) pargs
541 findCalls guarded (P _ f _ ) pvs pargs
542 | not (f `elem` pvs) = [(f, [])]
543 findCalls _ _ _ _ = []
545 expandToArity n args
546 = case lookupTy n (tt_ctxt ist) of
547 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
548 _ -> args
549 where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
550 expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []
551 expand i _ xs = xs
553 mkChange n args pargs = [(n, expandToArity n (sizes args))]
554 where
555 sizes [] = []
556 sizes (a : as) = checkSize a pargs 0 : sizes as
558 -- find which argument in pargs <a> is smaller than, if any
559 checkSize a (p : ps) i
560 | a == p = Just (i, Same)
561 | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
562 as == txt "assert_smaller" && arg == p
563 = Just (i, Smaller)
564 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
565 | otherwise = checkSize a ps (i + 1)
566 checkSize a [] i = Nothing
568 -- the smaller thing we find must be defined in the same group of mutally
569 -- defined types as <a>, and not be coinductive - so carry the type of
570 -- the constructor we've gone under.
572 smaller (Just tyn) a (t, Just tyt)
573 | a == t = isInductive (fst (unApply (getRetTy tyn)))
574 (fst (unApply (getRetTy tyt)))
575 smaller ty a (ap@(App _ f s), _)
576 | (P (DCon _ _ _) n _, args) <- unApply ap
577 = let tyn = getType n in
578 any (smaller (ty `mplus` Just tyn) a)
579 (zip args (map toJust (getArgTys tyn)))
580 -- check higher order recursive arguments
581 smaller ty (App _ f s) a = smaller ty f a
582 smaller _ _ _ = False
584 toJust (n, t) = Just t
586 getType n = case lookupTyExact n (tt_ctxt ist) of
587 Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
589 isInductive (P _ nty _) (P _ nty' _) =
590 let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of
591 [TI _ x _ _ muts] -> (x, muts)
592 _ -> (False, []) in
593 (nty == nty' || any (== nty') muts) && not co
594 isInductive _ _ = False
596 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
597 dePat t = t
599 patvars (Bind x (PVar _) sc) = x : patvars sc
600 patvars _ = []
602checkSizeChange :: Name -> Idris Totality
603checkSizeChange n = do
604 ist <- getIState
605 case lookupCtxt n (idris_callgraph ist) of
606 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
607 logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++
608 "from " ++ show (scg cg) ++ "\n" ++
609 show (length ms) ++ "\n" ++
610 showSep "\n" (map show ms))
611 logCoverage 6 (show cg)
612 -- every multipath must have an infinitely descending
613 -- thread, then the function terminates
614 -- also need to checks functions called are all total
615 -- (Unchecked is okay as we'll spot problems here)
616 let tot = map (checkMP ist (getArity ist n)) ms
617 logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"
618 logCoverage 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
619 return (noPartial tot)
620 [] -> do logCoverage 5 $ "No paths for " ++ show n
621 return Unchecked
622 where getArity ist n
623 = case lookupTy n (tt_ctxt ist) of
624 [ty] -> arity (normalise (tt_ctxt ist) [] ty)
625 _ -> error "Can't happen: checkSizeChange.getArity"
627type MultiPath = [SCGEntry]
629mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
630mkMultiPaths ist path [] = [reverse path]
631mkMultiPaths ist path cg
632 = concat (map extend cg)
633 where extend (nextf, args)
634 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
635 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
636 = case lookupCtxt nextf (idris_callgraph ist) of
637 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
638 _ -> [ reverse ((nextf, args) : path) ]
639 | otherwise = [ reverse ((nextf, args) : path) ]
641-- do (nextf, args) <- cg
642-- if ((nextf, args) `elem` path)
643-- then return (reverse ((nextf, args) : path))
644-- else case lookupCtxt nextf (idris_callgraph ist) of
645-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
646-- _ -> return (reverse ((nextf, args) : path))
648-- If any route along the multipath leads to infinite descent, we're fine.
649-- Try a route beginning with every argument.
650-- If we reach a point we've been to before, but with a smaller value,
651-- that means there is an infinitely descending path from that argument.
653checkMP :: IState -> Int -> MultiPath -> Totality
654checkMP ist i mp = if i > 0
655 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
656-- trace ("Paths " ++ show paths) $
657 collapse paths
658 else tryPath 0 [] mp 0
659 where
660 tryPath' d path mp arg
661 = let res = tryPath d path mp arg in
662 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
664 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
665 tryPath desc path [] _ = Total []
666-- tryPath desc path ((UN "believe_me", _) : _) arg
667-- = Partial BelieveMe
668 -- if we get to a constructor, it's fine as long as it's strictly positive
669 tryPath desc path ((f, _) : es) arg
670 | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
671 = case lookupTotal f (tt_ctxt ist) of
672 [Total _] -> Unchecked -- okay so far
673 [Partial _] -> Partial (Other [f])
674 x -> error $ "CAN'T HAPPEN: " ++ show x ++ " for " ++ show f
675 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
676 = Total []
677 tryPath desc path (e@(f, args) : es) arg
678 | e `elem` es && allNothing args = Partial (Mutual [f])
679 tryPath desc path (e@(f, nextargs) : es) arg
680 | Just d <- lookup (e, arg) path
681 = if desc > 0
682 then -- trace ("Descent " ++ show (desc - d) ++ " "
683 -- ++ show (path, e)) $
684 Total []
685 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
686 | e `elem` map (fst . fst) path
687 && not (f `elem` map fst es)
688 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
689 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
690 let argspos = case collapseNothing (zip nextargs [0..]) of
691 [] -> [(Nothing, 0)]
692 x -> x
693-- trace (show (argspos, nextargs, path)) $
694 pathres =
695 do (a, pos) <- argspos
696 case a of
697 Nothing -> -- don't know, but if the
698 -- rest definitely terminates without
699 -- any cycles with route so far,
700 -- then we might yet be total
701 case collapse (map (tryPath 0 (((e, arg), 0):path) es)
702 [0..length nextargs - 1]) of
703 Total _ -> return Unchecked
704 x -> return x
705 Just (nextarg, sc) ->
706 if nextarg == arg then
707 case sc of
708 Same -> return $ tryPath desc (((e, arg), desc) : path)
709 es pos
710 Smaller -> return $ tryPath (desc+1)
711 (((e, arg), desc) : path)
712 es
713 pos
714 _ -> trace ("Shouldn't happen " ++ show e) $
715 return (Partial Itself)
716 else return Unchecked in
717-- trace (show (desc, argspos, path, es, pathres)) $
718 collapse' Unchecked pathres
720 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
721 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
722 | otherwise = Unchecked
724allNothing :: [Maybe a] -> Bool
725allNothing xs = null (collapseNothing (zip xs [0..]))
727collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
728collapseNothing ((Nothing, _) : xs)
729 = filter (\ (x, _) -> case x of
730 Nothing -> False
731 _ -> True) xs
732collapseNothing (x : xs) = x : collapseNothing xs
733collapseNothing [] = []
735noPartial :: [Totality] -> Totality
736noPartial (Partial p : xs) = Partial p
737noPartial (_ : xs) = noPartial xs
738noPartial [] = Total []
740collapse :: [Totality] -> Totality
741collapse xs = collapse' Unchecked xs
742collapse' def (Total r : xs) = Total r
743collapse' def (Unchecked : xs) = collapse' def xs
744collapse' def (d : xs) = collapse' d xs
745-- collapse' Unchecked [] = Total []
746collapse' def [] = def