git.iko.soy/Idris-dev
on ff01a4c help sign in
Idris-dev/src/Idris/Coverage.hs
979 lines 44 kB history raw
1{-|
2Module : Idris.Coverage
3Description : The coverage and totality checkers for Idris are in this module.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards #-}
9module Idris.Coverage where
11import Idris.AbsSyntax
12import Idris.Core.CaseTree
13import Idris.Core.Evaluate
14import Idris.Core.TT
15import Idris.Delaborate
16import Idris.Error
17import Idris.Output (iWarn, iputStrLn)
19import Control.Monad.State.Strict
20import Data.Char
21import Data.Either
22import Data.List
23import Data.Maybe
24import Debug.Trace
26-- | Generate a pattern from an 'impossible' LHS.
27--
28-- We need this to eliminate the pattern clauses which have been
29-- provided explicitly from new clause generation.
30mkPatTm :: PTerm -> Idris Term
31mkPatTm t = do i <- getIState
32 let timp = addImpl' True [] [] [] i t
33 evalStateT (toTT (mapPT deNS timp)) 0
34 where
35 toTT (PRef _ _ n) = do i <- lift getIState
36 case lookupNameDef n (tt_ctxt i) of
37 [(n', TyDecl nt _)] -> return $ P nt n' Erased
38 _ -> return $ P Ref n Erased
39 toTT (PApp _ t args) = do t' <- toTT t
40 args' <- mapM (toTT . getTm) args
41 return $ mkApp t' args'
42 toTT (PDPair _ _ _ l _ r) = do l' <- toTT l
43 r' <- toTT r
44 return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
45 toTT (PPair _ _ _ l r) = do l' <- toTT l
46 r' <- toTT r
47 return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
48 -- For alternatives, pick the first and drop the namespaces. It doesn't
49 -- really matter which is taken since matching will ignore the namespace.
50 toTT (PAlternative _ _ (a : as)) = toTT a
51 toTT _ = do v <- get
52 put (v + 1)
53 return (P Bound (sMN v "imp") Erased)
55 deNS (PRef f hl (NS n _)) = PRef f hl n
56 deNS t = t
58-- | Given a list of LHSs, generate a extra clauses which cover the remaining
59-- cases. The ones which haven't been provided are marked 'absurd' so
60-- that the checker will make sure they can't happen.
61--
62-- This will only work after the given clauses have been typechecked and the
63-- names are fully explicit!
64genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
65genClauses fc n xs given
66 = do i <- getIState
67 let lhs_tms = map (\x -> flattenArgs $ delab' i x True True) xs
68 -- if a placeholder was given, don't bother generating cases for it
69 let lhs_tms' = zipWith mergePlaceholders lhs_tms
70 (map (stripUnmatchable i) (map flattenArgs given))
71 let lhss = map pUnApply lhs_tms'
72 nty <- case lookupTyExact n (tt_ctxt i) of
73 Just t -> return (normalise (tt_ctxt i) [] t)
74 _ -> fail "Can't happen - genClauses, lookupTyExact"
76 let argss = transpose lhss
77 let all_args = map (genAll i) (zip (genPH i nty) argss)
78 logCoverage 5 $ "COVERAGE of " ++ show n
79 logCoverage 5 $ "using type " ++ show nty
80 logCoverage 5 $ "non-concrete args " ++ show (genPH i nty)
82 logCoverage 5 $ show (lhs_tms, lhss)
83 logCoverage 5 $ "Args are: " ++ show argss
84 logCoverage 5 $ show (map length argss) ++ "\nAll args:\n" ++ show (map length all_args)
85 logCoverage 10 $ "All args are: " ++ show all_args
86 logCoverage 3 $ "Original: \n" ++
87 showSep "\n" (map (\t -> showTmImpls (delab' i t True True)) xs)
88 -- add an infinite supply of explicit arguments to update the possible
89 -- cases for (the return type may be variadic, or function type, so
90 -- there may be more case splitting that the idris_implicits record
91 -- suggests)
92 let parg = case lookupCtxt n (idris_implicits i) of
93 (p : _) ->
94 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)
95 _ -> repeat (pexp Placeholder)
96 let tryclauses = mkClauses parg all_args
97 logCoverage 3 $ show (length tryclauses) ++ " initially to check"
98 logCoverage 2 $ showSep "\n" (map (showTm i) tryclauses)
99 let new = filter (noMatch i) (nub tryclauses)
100 logCoverage 2 $ show (length new) ++ " clauses to check for impossibility"
101 logCoverage 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
102-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
103 return new
104-- return (map (\t -> PClause n t [] PImpossible []) new)
105 where getLHS i term
106 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
107 | otherwise = []
109 -- if an argument has a non-concrete type (i.e. it's a function
110 -- that calculates something from a previous argument) we'll also
111 -- need to generate a placeholder pattern for it since it could be
112 -- anything based on earlier values
113 genPH :: IState -> Type -> [Bool]
114 genPH ist (Bind n (Pi _ ty _) sc) = notConcrete ist ty : genPH ist sc
115 genPH ist ty = []
117 notConcrete ist t | (P _ n _, args) <- unApply t,
118 not (isConName n (tt_ctxt ist)) = True
119 notConcrete _ _ = False
121 pUnApply (PApp _ f args) = map getTm args
122 pUnApply _ = []
124 flattenArgs (PApp fc (PApp _ f as) as')
125 = flattenArgs (PApp fc f (as ++ as'))
126 flattenArgs t = t
128 -- Return whether the given clause matches none of the input clauses
129 -- (xs)
130 noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of
131 Right ms -> False
132 Left miss -> True) xs
135 mergePlaceholders :: PTerm -> PTerm -> PTerm
136 mergePlaceholders x Placeholder = Placeholder
137 mergePlaceholders (PApp fc f args) (PApp fc' f' args')
138 = PApp fc' f' (zipWith mergePArg args args')
139 where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in
140 x { getTm = xtm}
141 mergePlaceholders x _ = x
143 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
144 mkClauses parg args
145 | all (== [Placeholder]) args = []
146 mkClauses parg args
147 = do args' <- mkArg args
148 let tm = PApp fc (PRef fc [] n) (zipWith upd args' parg)
149 return tm
150 where
151 mkArg :: [[PTerm]] -> [[PTerm]]
152 mkArg [] = return []
153 mkArg (a : as) = do a' <- a
154 as' <- mkArg as
155 return (a':as')
157-- | Does this error result rule out a case as valid when coverage checking?
158validCoverageCase :: Context -> Err -> Bool
159validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
160 = let topx' = normalise ctxt [] topx
161 topy' = normalise ctxt [] topy in
162 not (sameFam topx' topy' || not (validCoverageCase ctxt e))
163 where sameFam topx topy
164 = case (unApply topx, unApply topy) of
165 ((P _ x _, _), (P _ y _, _)) -> x == y
166 _ -> False
167validCoverageCase ctxt (InfiniteUnify _ _ _) = False
168validCoverageCase ctxt (CantConvert _ _ _) = False
169validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e
170validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e
171validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e
172validCoverageCase ctxt _ = True
174-- | Check whether an error is recoverable in the sense needed for
175-- coverage checking.
176recoverableCoverage :: Context -> Err -> Bool
177recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)
178 = let topx' = normalise ctxt [] topx
179 topy' = normalise ctxt [] topy in
180 r || checkRec topx' topy'
181 where -- different notion of recoverable than in unification, since we
182 -- have no metavars -- just looking to see if a constructor is failing
183 -- to unify with a function that may be reduced later
184 checkRec (App _ f a) p@(P _ _ _) = checkRec f p
185 checkRec p@(P _ _ _) (App _ f a) = checkRec p f
186 checkRec fa@(App _ _ _) fa'@(App _ _ _)
187 | (f, as) <- unApply fa,
188 (f', as') <- unApply fa'
189 = if (length as /= length as')
190 then checkRec f f'
191 else checkRec f f' && and (zipWith checkRec as as')
192 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
193 checkRec _ _ = False
195 ntRec x y | Ref <- x = True
196 | Ref <- y = True
197 | (Bound, Bound) <- (x, y) = True
198 | otherwise = False -- name is different, unrecoverable
199recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e
200recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e
201recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
202recoverableCoverage _ _ = False
204genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
205genAll i (addPH, args)
206 = case filter (/=Placeholder) $ fnub $ mergePHs $ fnub (concatMap otherPats (fnub args)) of
207 [] -> [Placeholder]
208 xs -> ph xs
209 where
210 ph ts = if addPH then Placeholder : ts else ts
212 -- Merge patterns with placeholders in other patterns, to ensure we've
213 -- covered all possible generated cases
214 -- e.g. if we have (True, _) (False, _) (_, True) (_, False)
215 -- we should merge these to get (True, True), (False, False)
216 -- (False, True) and (True, False)
217 mergePHs :: [PTerm] -> [PTerm]
218 mergePHs xs = mergePHs' xs xs
220 mergePHs' [] all = []
221 mergePHs' (x : xs) all = mergePH x all ++ mergePHs' xs all
223 mergePH :: PTerm -> [PTerm] -> [PTerm]
224 mergePH tm [] = []
225 mergePH tm (x : xs)
226 | Just merged <- mergePTerm tm x = merged : mergePH tm xs
227 | otherwise = mergePH tm xs
229 mergePTerm :: PTerm -> PTerm -> Maybe PTerm
230 mergePTerm x Placeholder = Just x
231 mergePTerm Placeholder x = Just x
232 mergePTerm tm@(PRef fc1 hl1 n1) (PRef fc2 hl2 n2)
233 | n1 == n2 = Just tm
234 mergePTerm (PPair fc1 hl1 p1 x1 y1) (PPair fc2 hl2 p2 x2 y2)
235 = do x <- mergePTerm x1 x2
236 y <- mergePTerm y1 y2
237 Just (PPair fc1 hl1 p1 x y)
238 mergePTerm (PDPair fc1 hl1 p1 x1 t1 y1) (PDPair fc2 hl2 p2 x2 t2 y2)
239 = do x <- mergePTerm x1 x2
240 y <- mergePTerm y1 y2
241 t <- mergePTerm t1 t2
242 Just (PDPair fc1 hl1 p1 x t y)
243 mergePTerm (PApp fc1 f1 args1) (PApp fc2 f2 args2)
244 = do fm <- mergePTerm f1 f2
245 margs <- mergeArgs args1 args2
246 Just (PApp fc1 fm margs)
247 where
248 mergeArgs [] [] = Just []
249 mergeArgs (a : as) (b : bs)
250 = do ma_in <- mergePTerm (getTm a) (getTm b)
251 let ma = a { getTm = ma_in }
252 mas <- mergeArgs as bs
253 Just (ma : mas)
254 mergeArgs _ _ = Nothing
255 mergePTerm x y | x == y = Just x
256 | otherwise = Nothing
258 -- for every constant in a term (at any level) take next one to make sure
259 -- that constants which are not explicitly handled are covered
260 nextConst (PConstant fc c) = PConstant NoFC (nc' c)
261 nextConst o = o
263 nc' (I c) = I (c + 1)
264 nc' (BI c) = BI (c + 1)
265 nc' (Fl c) = Fl (c + 1)
266 nc' (B8 c) = B8 (c + 1)
267 nc' (B16 c) = B16 (c + 1)
268 nc' (B32 c) = B32 (c + 1)
269 nc' (B64 c) = B64 (c + 1)
270 nc' (Ch c) = Ch (chr $ ord c + 1)
271 nc' (Str c) = Str (c ++ "'")
272 nc' o = o
274 otherPats :: PTerm -> [PTerm]
275 otherPats o@(PRef fc hl n) = ph $ ops fc n [] o
276 otherPats o@(PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs o
277 otherPats o@(PPair fc hls _ l r)
278 = ph $ ops fc pairCon
279 ([pimp (sUN "A") Placeholder True,
280 pimp (sUN "B") Placeholder True] ++
281 [pexp l, pexp r]) o
282 otherPats o@(PDPair fc hls p t _ v)
283 = ph $ ops fc sigmaCon
284 ([pimp (sUN "a") Placeholder True,
285 pimp (sUN "P") Placeholder True] ++
286 [pexp t,pexp v]) o
287 otherPats o@(PConstant _ c) = ph [o, nextConst o]
288 otherPats arg = return Placeholder
290 ops fc n xs o
291 | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)
292 = do xs' <- mapM otherPats (map getExpTm xs)
293 let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))
294 let tyn = getTy n (tt_ctxt i)
295 case lookupCtxt tyn (idris_datatypes i) of
296 (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
297 _ -> [p]
298 ops fc n arg o = return Placeholder
300 getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
301 getExpTm t = getTm t
303 -- put it back to its original form
304 resugar (PApp _ (PRef fc hl n) [_,_,t,v])
305 | n == sigmaCon
306 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)
307 resugar (PApp _ (PRef fc hl n) [_,_,l,r])
308 | n == pairCon
309 = PPair fc [] IsTerm (getTm l) (getTm r)
310 resugar t = t
312 dropForce force (x : xs) i | i `elem` force
313 = upd Placeholder x : dropForce force xs (i + 1)
314 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
315 dropForce _ [] _ = []
318 getTy n ctxt = case lookupTy n ctxt of
319 (t : _) -> case unApply (getRetTy t) of
320 (P _ tyn _, _) -> tyn
321 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
322 _ -> error "Can't happen getTy 2"
324 mkPat fc x = case lookupCtxt x (idris_implicits i) of
325 (pargs : _)
326 -> PApp fc (PRef fc [] x) (map (upd Placeholder) pargs)
327 _ -> error "Can't happen - genAll"
329 fnub :: [PTerm] -> [PTerm]
330 fnub xs = fnub' [] xs
332 fnub' :: [PTerm] -> [PTerm] -> [PTerm]
333 fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
334 | otherwise = fnub' (x : acc) xs
335 fnub' acc [] = acc
337 -- quick check for constructor equality
338 quickEq :: PTerm -> PTerm -> Bool
339 quickEq (PConstant _ n) (PConstant _ n') = n == n'
340 quickEq (PRef _ _ n) (PRef _ _ n') = n == n'
341 quickEq (PPair _ _ _ l r) (PPair _ _ _ l' r') = quickEq l l' && quickEq r r'
342 quickEq (PApp _ t as) (PApp _ t' as')
343 | length as == length as'
344 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
345 quickEq Placeholder Placeholder = True
346 quickEq x y = False
348 qelem :: PTerm -> [PTerm] -> Bool
349 qelem x [] = False
350 qelem x (y : ys) | x `quickEq` y = True
351 | otherwise = qelem x ys
354upd :: t -> PArg' t -> PArg' t
355upd p' p = p { getTm = p' }
357-- | Check whether function and all descendants cover all cases
358-- (partial is okay, as long as it's due to recursion)
359checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
360checkAllCovering fc done top n | not (n `elem` done)
361 = do i <- get
362 case lookupTotal n (tt_ctxt i) of
363 [tot@(Partial NotCovering)] ->
364 do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n
365 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }
366 addIBC (IBCTotCheckErr fc msg)
367 [Partial _] ->
368 case lookupCtxt n (idris_callgraph i) of
369 [cg] -> mapM_ (checkAllCovering fc (n : done) top)
370 (calls cg)
371 _ -> return ()
372 x -> return () -- stop if total
373checkAllCovering _ _ _ _ = return ()
375-- | Check whether all 'Inf' arguments to the name end up guaranteed to be
376-- guarded by constructors (conservatively... maybe this can do better later).
377-- Essentially, all it does is check that every branch is a constructor application
378-- with no other function applications.
379--
380-- If so, set the 'AllGuarded' flag which can be used by the productivity check
381checkIfGuarded :: Name -> Idris ()
382checkIfGuarded n
383 = do i <- get
384 let ctxt = tt_ctxt i
385 case lookupDefExact n ctxt of
386 Just (CaseOp _ ty _ _ _ cases) ->
387 let gnames = fst (cases_compiletime cases) in
388 if allGuarded gnames i (snd (cases_compiletime cases))
389 then -- trace (show (n, gnames, ty, cases_compiletime cases)) $
390 addFnOpt n AllGuarded
391 else return ()
392 _ -> return ()
393 where
394 guard n ist = isConName n (tt_ctxt ist) || guardFlag n ist
395 guardFlag n ist = case lookupCtxtExact n (idris_flags ist) of
396 Nothing -> False
397 Just fs -> AllGuarded `elem` fs
399 -- Top level thing always needs to be a constructor application if
400 -- the delayed things are going to be definitely guarded by this definition
401 allGuarded names i (STerm t)
402 | (P _ fn _, args) <- unApply t,
403 guard fn i
404 = and (map (guardedTerm names i) args)
405 | otherwise = False
406 allGuarded names i (ProjCase _ alts) = and (map (guardedAlt names i) alts)
407 allGuarded names i (Case _ _ alts) = and (map (guardedAlt names i) alts)
408 allGuarded names i _ = True
410 guardedTerm names i (P _ v _) = v `elem` names || guard v i
411 guardedTerm names i (Bind n (Let t v) sc)
412 = guardedTerm names i v && guardedTerm names i sc
413 guardedTerm names i (Bind n b sc) = False
414 guardedTerm names i ap@(App _ _ _)
415 | (P _ fn _, args) <- unApply ap,
416 guard fn i || fn `elem` names
417 = and (map (guardedTerm names i) args)
418 guardedTerm names i (App _ f a) = False
419 guardedTerm names i tm = True
421 guardedAlt names i (ConCase _ _ _ t) = allGuarded names i t
422 guardedAlt names i (FnCase _ _ t) = allGuarded names i t
423 guardedAlt names i (ConstCase _ t) = allGuarded names i t
424 guardedAlt names i (SucCase _ t) = allGuarded names i t
425 guardedAlt names i (DefaultCase t) = allGuarded names i t
427-- | Check if, in a given group of type declarations mut_ns, the
428-- constructor cn : ty is strictly positive, and update the context
429-- accordingly
430checkPositive :: [Name] -- ^ the group of type declarations
431 -> (Name, Type) -- ^ the constructor
432 -> Idris Totality
433checkPositive mut_ns (cn, ty')
434 = do i <- getIState
435 let ty = delazy' True (normalise (tt_ctxt i) [] ty')
436 let p = cp i ty
437 let tot = if p then Total (args ty) else Partial NotPositive
438 let ctxt' = setTotal cn tot (tt_ctxt i)
439 putIState (i { tt_ctxt = ctxt' })
440 logCoverage 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns
441 addIBC (IBCTotal cn tot)
442 return tot
443 where
444 args t = [0..length (getArgTys t)-1]
446 cp i (Bind n (Pi _ aty _) sc)
447 = posArg i aty && cp i sc
448 cp i t | (P _ n' _ , args) <- unApply t,
449 n' `elem` mut_ns = all noRec args
450 cp i _ = True
452 posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc
453 posArg ist t = posParams ist t
455 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
457 -- If the type appears recursively in a parameter argument, that's
458 -- fine, otherwise if it appears in an argument it's not fine.
459 posParams ist t | (P _ n _, args) <- unApply t
460 = case lookupCtxtExact n (idris_datatypes ist) of
461 Just ti -> checkParamsOK (param_pos ti) 0 args
462 Nothing -> and (map (posParams ist) args)
463 posParams ist t = noRec t
465 checkParamsOK ppos i [] = True
466 checkParamsOK ppos i (p : ps)
467 | i `elem` ppos = checkParamsOK ppos (i + 1) ps
468 | otherwise = noRec p && checkParamsOK ppos (i + 1) ps
470-- | Calculate the totality of a function from its patterns. Either
471-- follow the size change graph (if inductive) or check for
472-- productivity (if coinductive)
473calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
474calcTotality fc n pats
475 = do i <- getIState
476 let opts = case lookupCtxt n (idris_flags i) of
477 [fs] -> fs
478 _ -> []
479 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
480 (failure : _) -> return failure
481 _ -> checkSizeChange n
482 where
483 checkLHS i (P _ fn _)
484 = case lookupTotalExact fn (tt_ctxt i) of
485 Just (Partial _) -> return (Partial (Other [fn]))
486 _ -> Nothing
487 checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
488 checkLHS _ _ = Nothing
490checkTotality :: [Name] -> FC -> Name -> Idris Totality
491checkTotality path fc n
492 | n `elem` path = return (Partial (Mutual (n : path)))
493 | otherwise = do
494 t <- getTotality n
495 i <- getIState
496 ctxt' <- do ctxt <- getContext
497 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
498 setContext ctxt'
499 ctxt <- getContext
500 i <- getIState
501 let opts = case lookupCtxt n (idris_flags i) of
502 [fs] -> fs
503 _ -> []
504 t' <- case t of
505 Unchecked ->
506 case lookupDef n ctxt of
507 [CaseOp _ _ _ _ pats _] ->
508 do t' <- if AssertTotal `elem` opts
509 then return $ Total []
510 else calcTotality fc n pats
511 logCoverage 2 $ "Set to " ++ show t'
512 setTotality n t'
513 addIBC (IBCTotal n t')
514 return t'
515 [TyDecl (DCon _ _ _) ty] ->
516 case unApply (getRetTy ty) of
517 (P _ tyn _, _) -> do
518 let ms = case lookupCtxt tyn (idris_datatypes i) of
519 [TI _ _ _ _ xs@(_:_)] -> xs
520 ts -> [tyn]
521 checkPositive ms (n, ty)
522 _-> return $ Total []
523 _ -> return $ Total []
524 x -> return x
525 case t' of
526 Total _ -> return t'
527 Productive -> return t'
528 e -> do w <- cmdOptType WarnPartial
529 if TotalFn `elem` opts
530 then do totalityError t'; return t'
531 else do when (w && not (PartialFn `elem` opts)) $
532 warnPartial n t'
533 return t'
534 where
535 totalityError t = do i <- getIState
536 let msg = show n ++ " is " ++ show t
537 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}
538 addIBC (IBCTotCheckErr fc msg)
540 warnPartial n t
541 = do i <- getIState
542 case lookupDef n (tt_ctxt i) of
543 [x] -> do
544 iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t
545-- ++ "\n" ++ show x
546-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
547-- iputStrLn (show cg)
550checkDeclTotality :: (FC, Name) -> Idris Totality
551checkDeclTotality (fc, n)
552 = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"
553 i <- getIState
554 let opts = case lookupCtxtExact n (idris_flags i) of
555 Just fs -> fs
556 _ -> []
557 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
558 t <- checkTotality [] fc n
559 return t
561-- If the name calls something which is partial, set it as partial
562verifyTotality :: (FC, Name) -> Idris ()
563verifyTotality (fc, n)
564 = do logCoverage 2 $ "Checking " ++ show n ++ "'s descendents are total"
565 ist <- getIState
566 case lookupTotalExact n (tt_ctxt ist) of
567 Just (Total _) -> do
568 let ns = getNames (tt_ctxt ist)
570 case getPartial ist [] ns of
571 Nothing -> return ()
572 Just bad -> do let t' = Partial (Other bad)
573 logCoverage 2 $ "Set to " ++ show t'
574 setTotality n t'
575 addIBC (IBCTotal n t')
576 _ -> return ()
577 where
578 getNames ctxt = case lookupDefExact n ctxt of
579 Just (CaseOp _ _ _ _ _ defs)
580 -> let (top, def) = cases_compiletime defs in
581 map fst (findCalls' True def top)
582 _ -> []
584 getPartial ist [] [] = Nothing
585 getPartial ist bad [] = Just bad
586 getPartial ist bad (n : ns)
587 = case lookupTotalExact n (tt_ctxt ist) of
588 Just (Partial _) -> getPartial ist (n : bad) ns
589 _ -> getPartial ist bad ns
591-- | Calculate the size change graph for this definition
592--
593-- SCG for a function f consists of a list of:
594-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
595--
596-- where g is a function called
597-- a1 ... an are the arguments of f in positions 1..n of g
598-- sizechange1 ... sizechange2 is how their size has changed wrt the input
599-- to f
600-- Nothing, if the argument is unrelated to the input
601buildSCG :: (FC, Name) -> Idris ()
602buildSCG (_, n) = do
603 ist <- getIState
604 case lookupCtxt n (idris_callgraph ist) of
605 [cg] -> case lookupDefExact n (tt_ctxt ist) of
606 Just (CaseOp _ _ _ pats _ cd) ->
607 let (args, sc) = cases_totcheck cd in
608 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"
609 ++ show pats ++ "\n" ++ show sc
610 let newscg = buildSCG' ist n (rights pats) args
611 logCoverage 5 $ "SCG is: " ++ show newscg
612 addToCG n ( cg { scg = newscg } )
613 _ -> return () -- CG comes from a type declaration only
614 [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"
615 x -> error $ "buildSCG: " ++ show (n, x)
617delazy = delazy' False -- not lazy codata
618delazy' all t@(App _ f a)
619 | (P _ (UN l) _, [_, _, arg]) <- unApply t,
620 l == txt "Force" = delazy' all arg
621 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
622 l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg
623 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
624 l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg
625delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
626delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
627delazy' all t = t
629data Guardedness = Toplevel | Unguarded | Guarded | Delayed
630 deriving Show
632buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
633buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
634 scgPat (lhs, rhs) = let lhs' = delazy lhs
635 rhs' = delazy rhs
636 (f, pargs) = unApply (dePat lhs') in
637 findCalls [] Toplevel (dePat rhs') (patvars lhs')
638 (zip pargs [0..])
640 -- Under a delay, calls are excluded from the graph - if it's a call to a
641 -- non-total function we'll find that in the final totality check
642 findCalls cases Delayed ap@(P _ n _) pvs args = []
643 findCalls cases guarded ap@(App _ f a) pvs pargs
644 -- under a call to "assert_total", don't do any checking, just believe
645 -- that it is total.
646 | (P _ (UN at) _, [_, _]) <- unApply ap,
647 at == txt "assert_total" = []
648 -- don't go under calls to functions which are asserted total
649 | (P _ n _, _) <- unApply ap,
650 Just opts <- lookupCtxtExact n (idris_flags ist),
651 AssertTotal `elem` opts = []
652 -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't
653 -- check under guarded constructors.
654 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
655 Guarded <- guarded,
656 del == txt "Delay"
657 = findCalls cases Delayed arg pvs pargs
658 | (P _ n _, args) <- unApply ap,
659 Delayed <- guarded,
660 isConName n (tt_ctxt ist) || allGuarded n ist
661 = -- Still under a 'Delay' and constructor guarded, so check
662 -- just the arguments to the constructor, remaining Delayed
663 concatMap (\x -> findCalls cases guarded x pvs pargs) args
664 | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,
665 ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]
666 -- Continue look inside if...then...else blocks
667 -- TODO: Consider whether we should do this for user defined ifThenElse
668 -- rather than just the one in the Prelude as a special case
669 = findCalls cases guarded t pvs pargs ++
670 findCalls cases guarded e pvs pargs
671 | (P _ n _, args) <- unApply ap,
672 caseName n && n /= topfn,
673 notPartial (lookupTotalExact n (tt_ctxt ist))
674 -- case block - look inside the block, as long as it was covering
675 -- (i.e. not currently set at Partial) to get a more accurate size
676 -- change result from the top level patterns (also to help pass
677 -- information through from guarded corecursion accurately)
678 = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args ++
679 if n `notElem` cases
680 then findCallsCase (n : cases) guarded n args pvs pargs
681 else []
682 | (P _ n _, args) <- unApply ap,
683 Delayed <- guarded
684 -- Under a delayed recursive call just check the arguments
685 = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args
686 | (P _ n _, args) <- unApply ap
687 -- Ordinary call, not under a delay.
688 -- If n is a constructor, set 'args' as Guarded
689 = let nguarded = case guarded of
690 Unguarded -> Unguarded
691 x -> if isConName n (tt_ctxt ist)
692 || allGuarded n ist
693 then Guarded
694 else Unguarded in
695 mkChange n args pargs ++
696 concatMap (\x -> findCalls cases nguarded x pvs pargs) args
697 where notPartial (Just (Partial NotCovering)) = False
698 notPartial _ = True
699 findCalls cases guarded (App _ f a) pvs pargs
700 = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs
701 findCalls cases guarded (Bind n (Let t v) e) pvs pargs
702 = findCalls cases Unguarded t pvs pargs ++
703 findCalls cases Unguarded v pvs pargs ++
704 -- Substitute in the scope since this might reveal some useful
705 -- structure
706 findCalls cases guarded (substV v e) pvs pargs
707 findCalls cases guarded (Bind n t e) pvs pargs
708 = findCalls cases Unguarded (binderTy t) pvs pargs ++
709 findCalls cases guarded e (n : pvs) pargs
710 findCalls cases guarded (P _ f _ ) pvs pargs
711 | not (f `elem` pvs) = [(f, [])]
712 findCalls _ _ _ _ _ = []
714 -- Assumption is that names are preserved in the case block (shadowing
715 -- dealt with by the elaborator) so we can just assume the top level names
716 -- are okay for building the size change
717 findCallsCase cases guarded n args pvs pargs
718 = case lookupDefExact n (tt_ctxt ist) of
719 Just (CaseOp _ _ _ pats _ cd) ->
720 concatMap (fccPat cases pvs pargs args guarded) (rights pats)
721 Nothing -> []
723 fccPat cases pvs pargs args g (lhs, rhs)
724 = let lhs' = delazy lhs
725 rhs' = delazy rhs
726 (f, pargs_case) = unApply (dePat lhs')
727 -- pargs is a pair of a term, and the argument position that
728 -- term appears in. If any of the arguments to the case block
729 -- are also on the lhs, we also want those patterns to appear
730 -- in the parg list so that we'll spot patterns which are
731 -- smaller than then
732 newpargs = newPArg args pargs
733 -- Now need to update the rhs of the case with the names in the
734 -- outer definition: In rhs', wherever we see what's in pargs_case,
735 -- replace it with the corresponding thing in pargs
736 csubs = zip pargs_case args
737 newrhs = doCaseSubs csubs (dePat rhs')
738 pargs' = pargs ++ addPArg newpargs pargs_case in
739 findCalls cases g newrhs pvs pargs'
740 where
741 doCaseSubs [] tm = tm
742 doCaseSubs ((x, x') : cs) tm
743 = doCaseSubs (subIn x x' cs) (substTerm x x' tm)
745 subIn x x' [] = []
746 subIn x x' ((l, r) : cs)
747 = (substTerm x x' l, substTerm x x' r) : subIn x x' cs
749 addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'
750 addPArg (Nothing : ts) (t' : ts') = addPArg ts ts'
751 addPArg _ _ = []
753 newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
754 newPArg (t : ts) pargs = case lookup t pargs of
755 Just i -> Just (t, i) : newPArg ts pargs
756 Nothing -> Nothing : newPArg ts pargs
757 newPArg [] pargs = []
759 expandToArity n args
760 = case lookupTy n (tt_ctxt ist) of
761 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
762 _ -> args
763 where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
764 expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []
765 expand i _ xs = xs
767 mkChange n args pargs = [(n, expandToArity n (sizes args))]
768 where
769 sizes [] = []
770 sizes (a : as) = checkSize a pargs : sizes as
772 -- find which argument in pargs <a> is smaller than, if any
773 checkSize a ((p, i) : ps)
774 | a == p = Just (i, Same)
775 | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
776 as == txt "assert_smaller" && arg == p
777 = Just (i, Smaller)
778 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
779 | otherwise = checkSize a ps
780 checkSize a [] = Nothing
782 -- the smaller thing we find must be defined in the same group of mutally
783 -- defined types as <a>, and not be coinductive - so carry the type of
784 -- the constructor we've gone under.
786 smaller (Just tyn) a (t, Just tyt)
787 | a == t = isInductive (fst (unApply (getRetTy tyn)))
788 (fst (unApply (getRetTy tyt)))
789 smaller ty a (ap@(App _ f s), _)
790 | (P (DCon _ _ _) n _, args) <- unApply ap
791 = let tyn = getType n in
792 any (smaller (ty `mplus` Just tyn) a)
793 (zip args (map toJust (getArgTys tyn)))
794 -- check higher order recursive arguments
795 smaller ty (App _ f s) a = smaller ty f a
796 smaller _ _ _ = False
798 toJust (n, t) = Just t
800 getType n = case lookupTyExact n (tt_ctxt ist) of
801 Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
803 isInductive (P _ nty _) (P _ nty' _) =
804 let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of
805 [TI _ x _ _ muts] -> (x, muts)
806 _ -> (False, []) in
807 (nty == nty' || any (== nty') muts) && not co
808 isInductive _ _ = False
810 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
811 dePat t = t
813 patvars (Bind x (PVar _) sc) = x : patvars sc
814 patvars _ = []
816 allGuarded n ist = case lookupCtxtExact n (idris_flags ist) of
817 Nothing -> False
818 Just fs -> AllGuarded `elem` fs
820checkSizeChange :: Name -> Idris Totality
821checkSizeChange n = do
822 ist <- getIState
823 case lookupCtxt n (idris_callgraph ist) of
824 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
825 logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++
826 "from " ++ show (scg cg) ++ "\n" ++
827 show (length ms) ++ "\n" ++
828 showSep "\n" (map show ms))
829 logCoverage 6 (show cg)
830 -- every multipath must have an infinitely descending
831 -- thread, then the function terminates
832 -- also need to checks functions called are all total
833 -- (Unchecked is okay as we'll spot problems here)
834 let tot = map (checkMP ist n (getArity ist n)) ms
835 logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"
836 logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++
837 (showSep "\n" (map show (zip ms tot)))
838 return (noPartial tot)
839 [] -> do logCoverage 5 $ "No paths for " ++ show n
840 return Unchecked
841 where getArity ist n
842 = case lookupTy n (tt_ctxt ist) of
843 [ty] -> arity (normalise (tt_ctxt ist) [] ty)
844 _ -> error "Can't happen: checkSizeChange.getArity"
846type MultiPath = [SCGEntry]
848mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
849mkMultiPaths ist path [] = [reverse path]
850mkMultiPaths ist path cg = concatMap extend cg
851 where extend (nextf, args)
852 | (nextf, args) `inPath` path = [ reverse ((nextf, args) : path) ]
853 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
854 = case lookupCtxt nextf (idris_callgraph ist) of
855 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
856 _ -> [ reverse ((nextf, args) : path) ]
857 | otherwise = [ reverse ((nextf, args) : path) ]
859 inPath :: SCGEntry -> [SCGEntry] -> Bool
860 inPath f [] = False
861 inPath f (g : gs) = smallerEq f g || f == g || inPath f gs
863 smallerEq :: SCGEntry -> SCGEntry -> Bool
864 smallerEq (f, args) (g, args')
865 = f == g && not (null (filter smallers args))
866 && filter smallers args == filter smallers args'
867 smallers (Just (_, Smaller)) = True
868 smallers _ = False
870-- If any route along the multipath leads to infinite descent, we're fine.
871-- Try a route beginning with every argument.
872-- If we reach a point we've been to before, but with a smaller value,
873-- that means there is an infinitely descending path from that argument.
875checkMP :: IState -> Name -> Int -> MultiPath -> Totality
876checkMP ist topfn i mp = if i > 0
877 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
878-- trace ("Paths " ++ show paths) $
879 collapse paths
880 else tryPath 0 [] mp 0
881 where
882 tryPath' d path mp arg
883 = let res = tryPath d path mp arg in
884 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
886 mkBig (e, d) = (e, 10000)
888 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
889 tryPath desc path [] _ = Total []
890-- tryPath desc path ((UN "believe_me", _) : _) arg
891-- = Partial BelieveMe
892 -- if we get to a constructor, it's fine as long as it's strictly positive
893 tryPath desc path ((f, _) : es) arg
894 | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
895 = case lookupTotalExact f (tt_ctxt ist) of
896 Just (Total _) -> Unchecked -- okay so far
897 Just (Partial _) -> Partial (Other [f])
898 x -> Unchecked -- An error elsewhere, set as Unchecked to make
899 -- some progress
900 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
901 = Total []
902 tryPath desc path (e@(f, args) : es) arg
903 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
904 | e `elem` es && allNothing args = Partial (Mutual [f])
905 tryPath desc path (e@(f, nextargs) : es) arg
906 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
907 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
908 | Just d <- lookup (e, arg) path
909 = if desc - d > 0 -- Now lower than when we were last here
910 then -- trace ("Descent " ++ show (desc - d) ++ " "
911 -- ++ show (path, e)) $
912 Total []
913 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
914 | e `elem` map (fst . fst) path
915 && not (f `elem` map fst es)
916 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
917 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
918 let argspos = zip nextargs [0..]
919 pathres =
920 do (a, pos) <- argspos
921 case a of
922 Nothing -> -- gone up, but if the
923 -- rest definitely terminates without any
924 -- cycles (including the path so far, which
925 -- we take as inaccessible) the path is fine
926 return $ tryPath 0 (map mkBig (((e, arg), desc) : path)) es pos
927 Just (nextarg, sc) ->
928 if nextarg == arg then
929 case sc of
930 Same -> return $ tryPath desc (((e, arg), desc) : path)
931 es pos
932 Smaller -> return $ tryPath (desc+1)
933 (((e, arg), desc) : path)
934 es
935 pos
936 _ -> trace ("Shouldn't happen " ++ show e) $
937 return (Partial Itself)
938 else return Unchecked in
939-- trace (show (desc, argspos, path, es, pathres)) $
940 collapse pathres
942 | otherwise = Unchecked
944allNothing :: [Maybe a] -> Bool
945allNothing xs = null (collapseNothing (zip xs [0..]))
947collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
948collapseNothing ((Nothing, t) : xs)
949 = (Nothing, t) : filter (\ (x, _) -> case x of
950 Nothing -> False
951 _ -> True) xs
952collapseNothing (x : xs) = x : collapseNothing xs
953collapseNothing [] = []
955noPartial :: [Totality] -> Totality
956noPartial (Partial p : xs) = Partial p
957noPartial (_ : xs) = noPartial xs
958noPartial [] = Total []
960collapse :: [Totality] -> Totality
961collapse xs = collapse' Unchecked xs
962collapse' def (Total r : xs) = Total r
963collapse' def (Unchecked : xs) = collapse' def xs
964collapse' def (d : xs) = collapse' d xs
965-- collapse' Unchecked [] = Total []
966collapse' def [] = def
968totalityCheckBlock :: Idris ()
969totalityCheckBlock = do
970 ist <- getIState
971 -- Do totality checking after entire mutual block
972 mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n
973 ctxt' <- do ctxt <- getContext
974 tclift $ simplifyCasedef n (getErasureInfo ist) ctxt
975 setContext ctxt')
976 (map snd (idris_totcheck ist))
977 mapM_ buildSCG (idris_totcheck ist)
978 mapM_ checkDeclTotality (idris_totcheck ist)
979 clear_totcheck