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