git.iko.soy/Idris-dev
on 5cf643e help sign in
Idris-dev/src/Idris/Coverage.hs
919 lines 41 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 if, in a given group of type declarations mut_ns, the
376-- constructor cn : ty is strictly positive, and update the context
377-- accordingly
378checkPositive :: [Name] -- ^ the group of type declarations
379 -> (Name, Type) -- ^ the constructor
380 -> Idris Totality
381checkPositive mut_ns (cn, ty')
382 = do i <- getIState
383 let ty = delazy' True (normalise (tt_ctxt i) [] ty')
384 let p = cp i ty
385 let tot = if p then Total (args ty) else Partial NotPositive
386 let ctxt' = setTotal cn tot (tt_ctxt i)
387 putIState (i { tt_ctxt = ctxt' })
388 logCoverage 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns
389 addIBC (IBCTotal cn tot)
390 return tot
391 where
392 args t = [0..length (getArgTys t)-1]
394 cp i (Bind n (Pi _ aty _) sc)
395 = posArg i aty && cp i sc
396 cp i t | (P _ n' _ , args) <- unApply t,
397 n' `elem` mut_ns = all noRec args
398 cp i _ = True
400 posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc
401 posArg ist t = posParams ist t
403 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
405 -- If the type appears recursively in a parameter argument, that's
406 -- fine, otherwise if it appears in an argument it's not fine.
407 posParams ist t | (P _ n _, args) <- unApply t
408 = case lookupCtxtExact n (idris_datatypes ist) of
409 Just ti -> checkParamsOK (param_pos ti) 0 args
410 Nothing -> and (map (posParams ist) args)
411 posParams ist t = noRec t
413 checkParamsOK ppos i [] = True
414 checkParamsOK ppos i (p : ps)
415 | i `elem` ppos = checkParamsOK ppos (i + 1) ps
416 | otherwise = noRec p && checkParamsOK ppos (i + 1) ps
418-- | Calculate the totality of a function from its patterns. Either
419-- follow the size change graph (if inductive) or check for
420-- productivity (if coinductive)
421calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
422calcTotality fc n pats
423 = do i <- getIState
424 let opts = case lookupCtxt n (idris_flags i) of
425 [fs] -> fs
426 _ -> []
427 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
428 (failure : _) -> return failure
429 _ -> checkSizeChange n
430 where
431 checkLHS i (P _ fn _)
432 = case lookupTotalExact fn (tt_ctxt i) of
433 Just (Partial _) -> return (Partial (Other [fn]))
434 _ -> Nothing
435 checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
436 checkLHS _ _ = Nothing
438checkTotality :: [Name] -> FC -> Name -> Idris Totality
439checkTotality path fc n
440 | n `elem` path = return (Partial (Mutual (n : path)))
441 | otherwise = do
442 t <- getTotality n
443 i <- getIState
444 ctxt' <- do ctxt <- getContext
445 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
446 setContext ctxt'
447 ctxt <- getContext
448 i <- getIState
449 let opts = case lookupCtxt n (idris_flags i) of
450 [fs] -> fs
451 _ -> []
452 t' <- case t of
453 Unchecked ->
454 case lookupDef n ctxt of
455 [CaseOp _ _ _ _ pats _] ->
456 do t' <- if AssertTotal `elem` opts
457 then return $ Total []
458 else calcTotality fc n pats
459 logCoverage 2 $ "Set to " ++ show t'
460 setTotality n t'
461 addIBC (IBCTotal n t')
462 return t'
463 [TyDecl (DCon _ _ _) ty] ->
464 case unApply (getRetTy ty) of
465 (P _ tyn _, _) -> do
466 let ms = case lookupCtxt tyn (idris_datatypes i) of
467 [TI _ _ _ _ xs@(_:_)] -> xs
468 ts -> [tyn]
469 checkPositive ms (n, ty)
470 _-> return $ Total []
471 _ -> return $ Total []
472 x -> return x
473 case t' of
474 Total _ -> return t'
475 Productive -> return t'
476 e -> do w <- cmdOptType WarnPartial
477 if TotalFn `elem` opts
478 then do totalityError t'; return t'
479 else do when (w && not (PartialFn `elem` opts)) $
480 warnPartial n t'
481 return t'
482 where
483 totalityError t = do i <- getIState
484 let msg = show n ++ " is " ++ show t
485 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}
486 addIBC (IBCTotCheckErr fc msg)
488 warnPartial n t
489 = do i <- getIState
490 case lookupDef n (tt_ctxt i) of
491 [x] -> do
492 iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t
493-- ++ "\n" ++ show x
494-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
495-- iputStrLn (show cg)
498checkDeclTotality :: (FC, Name) -> Idris Totality
499checkDeclTotality (fc, n)
500 = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"
501 i <- getIState
502 let opts = case lookupCtxtExact n (idris_flags i) of
503 Just fs -> fs
504 _ -> []
505 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
506 t <- checkTotality [] fc n
507 return t
509-- If the name calls something which is partial, set it as partial
510verifyTotality :: (FC, Name) -> Idris ()
511verifyTotality (fc, n)
512 = do logCoverage 2 $ "Checking " ++ show n ++ "'s descendents are total"
513 ist <- getIState
514 case lookupTotalExact n (tt_ctxt ist) of
515 Just (Total _) -> do
516 let ns = getNames (tt_ctxt ist)
518 case getPartial ist [] ns of
519 Nothing -> return ()
520 Just bad -> do let t' = Partial (Other bad)
521 logCoverage 2 $ "Set to " ++ show t'
522 setTotality n t'
523 addIBC (IBCTotal n t')
524 _ -> return ()
525 where
526 getNames ctxt = case lookupDefExact n ctxt of
527 Just (CaseOp _ _ _ _ _ defs)
528 -> let (top, def) = cases_compiletime defs in
529 map fst (findCalls' True def top)
530 _ -> []
532 getPartial ist [] [] = Nothing
533 getPartial ist bad [] = Just bad
534 getPartial ist bad (n : ns)
535 = case lookupTotalExact n (tt_ctxt ist) of
536 Just (Partial _) -> getPartial ist (n : bad) ns
537 _ -> getPartial ist bad ns
539-- | Calculate the size change graph for this definition
540--
541-- SCG for a function f consists of a list of:
542-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
543--
544-- where g is a function called
545-- a1 ... an are the arguments of f in positions 1..n of g
546-- sizechange1 ... sizechange2 is how their size has changed wrt the input
547-- to f
548-- Nothing, if the argument is unrelated to the input
549buildSCG :: (FC, Name) -> Idris ()
550buildSCG (_, n) = do
551 ist <- getIState
552 case lookupCtxt n (idris_callgraph ist) of
553 [cg] -> case lookupDefExact n (tt_ctxt ist) of
554 Just (CaseOp _ _ _ pats _ cd) ->
555 let (args, sc) = cases_totcheck cd in
556 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"
557 ++ show pats ++ "\n" ++ show sc
558 let newscg = buildSCG' ist n (rights pats) args
559 logCoverage 5 $ "SCG is: " ++ show newscg
560 addToCG n ( cg { scg = newscg } )
561 _ -> return () -- CG comes from a type declaration only
562 [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"
563 x -> error $ "buildSCG: " ++ show (n, x)
565delazy = delazy' False -- not lazy codata
566delazy' all t@(App _ f a)
567 | (P _ (UN l) _, [_, _, arg]) <- unApply t,
568 l == txt "Force" = delazy' all arg
569 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
570 l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg
571 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
572 l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg
573delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
574delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
575delazy' all t = t
577data Guardedness = Toplevel | Unguarded | Guarded | Delayed
578 deriving Show
580buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
581buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
582 scgPat (lhs, rhs) = let lhs' = delazy lhs
583 rhs' = delazy rhs
584 (f, pargs) = unApply (dePat lhs') in
585 findCalls [] Toplevel (dePat rhs') (patvars lhs')
586 (zip pargs [0..])
588 -- Under a delay, calls are excluded from the graph - if it's a call to a
589 -- non-total function we'll find that in the final totality check
590 findCalls cases Delayed ap@(P _ n _) pvs args = []
591 findCalls cases guarded ap@(App _ f a) pvs pargs
592 -- under a call to "assert_total", don't do any checking, just believe
593 -- that it is total.
594 | (P _ (UN at) _, [_, _]) <- unApply ap,
595 at == txt "assert_total" = []
596 -- don't go under calls to functions which are asserted total
597 | (P _ n _, _) <- unApply ap,
598 Just opts <- lookupCtxtExact n (idris_flags ist),
599 AssertTotal `elem` opts = []
600 -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't
601 -- check under guarded constructors.
602 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
603 Guarded <- guarded,
604 del == txt "Delay"
605 = findCalls cases Delayed arg pvs pargs
606 | (P _ n _, args) <- unApply ap,
607 Delayed <- guarded,
608 isConName n (tt_ctxt ist)
609 = -- Still under a 'Delay' and constructor guarded, so check
610 -- just the arguments to the constructor, remaining Delayed
611 concatMap (\x -> findCalls cases guarded x pvs pargs) args
612 | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,
613 ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]
614 -- Continue look inside if...then...else blocks
615 -- TODO: Consider whether we should do this for user defined ifThenElse
616 -- rather than just the one in the Prelude as a special case
617 = findCalls cases guarded t pvs pargs ++
618 findCalls cases guarded e pvs pargs
619 | (P _ n _, args) <- unApply ap,
620 caseName n && n /= topfn,
621 notPartial (lookupTotalExact n (tt_ctxt ist))
622 -- case block - look inside the block, as long as it was covering
623 -- (i.e. not currently set at Partial) to get a more accurate size
624 -- change result from the top level patterns (also to help pass
625 -- information through from guarded corecursion accurately)
626 = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args ++
627 if n `notElem` cases
628 then findCallsCase (n : cases) guarded n args pvs pargs
629 else []
630 | (P _ n _, args) <- unApply ap,
631 Delayed <- guarded
632 -- Under a delayed recursive call just check the arguments
633 = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args
634 | (P _ n _, args) <- unApply ap
635 -- Ordinary call, not under a delay.
636 -- If n is a constructor, set 'args' as Guarded
637 = let nguarded = case guarded of
638 Unguarded -> Unguarded
639 x -> if isConName n (tt_ctxt ist)
640 then Guarded
641 else Unguarded in
642 mkChange n args pargs ++
643 concatMap (\x -> findCalls cases nguarded x pvs pargs) args
644 where notPartial (Just (Partial NotCovering)) = False
645 notPartial _ = True
646 findCalls cases guarded (App _ f a) pvs pargs
647 = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs
648 findCalls cases guarded (Bind n (Let t v) e) pvs pargs
649 = findCalls cases Unguarded t pvs pargs ++
650 findCalls cases Unguarded v pvs pargs ++ findCalls cases guarded e (n : pvs) pargs
651 findCalls cases guarded (Bind n t e) pvs pargs
652 = findCalls cases Unguarded (binderTy t) pvs pargs ++
653 findCalls cases guarded e (n : pvs) pargs
654 findCalls cases guarded (P _ f _ ) pvs pargs
655 | not (f `elem` pvs) = [(f, [])]
656 findCalls _ _ _ _ _ = []
658 -- Assumption is that names are preserved in the case block (shadowing
659 -- dealt with by the elaborator) so we can just assume the top level names
660 -- are okay for building the size change
661 findCallsCase cases guarded n args pvs pargs
662 = case lookupDefExact n (tt_ctxt ist) of
663 Just (CaseOp _ _ _ pats _ cd) ->
664 concatMap (fccPat cases pvs pargs args guarded) (rights pats)
665 Nothing -> []
667 fccPat cases pvs pargs args g (lhs, rhs)
668 = let lhs' = delazy lhs
669 rhs' = delazy rhs
670 (f, pargs_case) = unApply (dePat lhs')
671 -- pargs is a pair of a term, and the argument position that
672 -- term appears in. If any of the arguments to the case block
673 -- are also on the lhs, we also want those patterns to appear
674 -- in the parg list so that we'll spot patterns which are
675 -- smaller than then
676 newpargs = newPArg args pargs
677 -- Now need to update the rhs of the case with the names in the
678 -- outer definition: In rhs', wherever we see what's in pargs_case,
679 -- replace it with the corresponding thing in pargs
680 csubs = zip pargs_case args
681 newrhs = doCaseSubs csubs (dePat rhs')
682 pargs' = pargs ++ addPArg newpargs pargs_case in
683 findCalls cases g newrhs pvs pargs'
684 where
685 doCaseSubs [] tm = tm
686 doCaseSubs ((x, x') : cs) tm
687 = doCaseSubs (subIn x x' cs) (substTerm x x' tm)
689 subIn x x' [] = []
690 subIn x x' ((l, r) : cs)
691 = (substTerm x x' l, substTerm x x' r) : subIn x x' cs
693 addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'
694 addPArg (Nothing : ts) (t' : ts') = addPArg ts ts'
695 addPArg _ _ = []
697 newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
698 newPArg (t : ts) pargs = case lookup t pargs of
699 Just i -> Just (t, i) : newPArg ts pargs
700 Nothing -> Nothing : newPArg ts pargs
701 newPArg [] pargs = []
703 expandToArity n args
704 = case lookupTy n (tt_ctxt ist) of
705 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
706 _ -> args
707 where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
708 expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []
709 expand i _ xs = xs
711 mkChange n args pargs = [(n, expandToArity n (sizes args))]
712 where
713 sizes [] = []
714 sizes (a : as) = checkSize a pargs : sizes as
716 -- find which argument in pargs <a> is smaller than, if any
717 checkSize a ((p, i) : ps)
718 | a == p = Just (i, Same)
719 | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
720 as == txt "assert_smaller" && arg == p
721 = Just (i, Smaller)
722 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
723 | otherwise = checkSize a ps
724 checkSize a [] = Nothing
726 -- the smaller thing we find must be defined in the same group of mutally
727 -- defined types as <a>, and not be coinductive - so carry the type of
728 -- the constructor we've gone under.
730 smaller (Just tyn) a (t, Just tyt)
731 | a == t = isInductive (fst (unApply (getRetTy tyn)))
732 (fst (unApply (getRetTy tyt)))
733 smaller ty a (ap@(App _ f s), _)
734 | (P (DCon _ _ _) n _, args) <- unApply ap
735 = let tyn = getType n in
736 any (smaller (ty `mplus` Just tyn) a)
737 (zip args (map toJust (getArgTys tyn)))
738 -- check higher order recursive arguments
739 smaller ty (App _ f s) a = smaller ty f a
740 smaller _ _ _ = False
742 toJust (n, t) = Just t
744 getType n = case lookupTyExact n (tt_ctxt ist) of
745 Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
747 isInductive (P _ nty _) (P _ nty' _) =
748 let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of
749 [TI _ x _ _ muts] -> (x, muts)
750 _ -> (False, []) in
751 (nty == nty' || any (== nty') muts) && not co
752 isInductive _ _ = False
754 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
755 dePat t = t
757 patvars (Bind x (PVar _) sc) = x : patvars sc
758 patvars _ = []
760checkSizeChange :: Name -> Idris Totality
761checkSizeChange n = do
762 ist <- getIState
763 case lookupCtxt n (idris_callgraph ist) of
764 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
765 logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++
766 "from " ++ show (scg cg) ++ "\n" ++
767 show (length ms) ++ "\n" ++
768 showSep "\n" (map show ms))
769 logCoverage 6 (show cg)
770 -- every multipath must have an infinitely descending
771 -- thread, then the function terminates
772 -- also need to checks functions called are all total
773 -- (Unchecked is okay as we'll spot problems here)
774 let tot = map (checkMP ist n (getArity ist n)) ms
775 logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"
776 logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++
777 (showSep "\n" (map show (zip ms tot)))
778 return (noPartial tot)
779 [] -> do logCoverage 5 $ "No paths for " ++ show n
780 return Unchecked
781 where getArity ist n
782 = case lookupTy n (tt_ctxt ist) of
783 [ty] -> arity (normalise (tt_ctxt ist) [] ty)
784 _ -> error "Can't happen: checkSizeChange.getArity"
786type MultiPath = [SCGEntry]
788mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
789mkMultiPaths ist path [] = [reverse path]
790mkMultiPaths ist path cg = concatMap extend cg
791 where extend (nextf, args)
792 | (nextf, args) `inPath` path = [ reverse ((nextf, args) : path) ]
793 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
794 = case lookupCtxt nextf (idris_callgraph ist) of
795 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
796 _ -> [ reverse ((nextf, args) : path) ]
797 | otherwise = [ reverse ((nextf, args) : path) ]
799 inPath :: SCGEntry -> [SCGEntry] -> Bool
800 inPath f [] = False
801 inPath f (g : gs) = smallerEq f g || f == g || inPath f gs
803 smallerEq :: SCGEntry -> SCGEntry -> Bool
804 smallerEq (f, args) (g, args')
805 = f == g && not (null (filter smallers args))
806 && filter smallers args == filter smallers args'
807 smallers (Just (_, Smaller)) = True
808 smallers _ = False
810-- If any route along the multipath leads to infinite descent, we're fine.
811-- Try a route beginning with every argument.
812-- If we reach a point we've been to before, but with a smaller value,
813-- that means there is an infinitely descending path from that argument.
815checkMP :: IState -> Name -> Int -> MultiPath -> Totality
816checkMP ist topfn i mp = if i > 0
817 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
818-- trace ("Paths " ++ show paths) $
819 collapse paths
820 else tryPath 0 [] mp 0
821 where
822 tryPath' d path mp arg
823 = let res = tryPath d path mp arg in
824 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
826 mkBig (e, d) = (e, 10000)
828 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
829 tryPath desc path [] _ = Total []
830-- tryPath desc path ((UN "believe_me", _) : _) arg
831-- = Partial BelieveMe
832 -- if we get to a constructor, it's fine as long as it's strictly positive
833 tryPath desc path ((f, _) : es) arg
834 | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
835 = case lookupTotalExact f (tt_ctxt ist) of
836 Just (Total _) -> Unchecked -- okay so far
837 Just (Partial _) -> Partial (Other [f])
838 x -> Unchecked -- An error elsewhere, set as Unchecked to make
839 -- some progress
840 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
841 = Total []
842 tryPath desc path (e@(f, args) : es) arg
843 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
844 | e `elem` es && allNothing args = Partial (Mutual [f])
845 tryPath desc path (e@(f, nextargs) : es) arg
846 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
847 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
848 | Just d <- lookup (e, arg) path
849 = if desc - d > 0 -- Now lower than when we were last here
850 then -- trace ("Descent " ++ show (desc - d) ++ " "
851 -- ++ show (path, e)) $
852 Total []
853 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
854 | e `elem` map (fst . fst) path
855 && not (f `elem` map fst es)
856 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
857 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
858 let argspos = zip nextargs [0..]
859 pathres =
860 do (a, pos) <- argspos
861 case a of
862 Nothing -> -- gone up, but if the
863 -- rest definitely terminates without any
864 -- cycles (including the path so far, which
865 -- we take as inaccessible) the path is fine
866 return $ tryPath 0 (map mkBig (((e, arg), desc) : path)) es pos
867 Just (nextarg, sc) ->
868 if nextarg == arg then
869 case sc of
870 Same -> return $ tryPath desc (((e, arg), desc) : path)
871 es pos
872 Smaller -> return $ tryPath (desc+1)
873 (((e, arg), desc) : path)
874 es
875 pos
876 _ -> trace ("Shouldn't happen " ++ show e) $
877 return (Partial Itself)
878 else return Unchecked in
879-- trace (show (desc, argspos, path, es, pathres)) $
880 collapse pathres
882 | otherwise = Unchecked
884allNothing :: [Maybe a] -> Bool
885allNothing xs = null (collapseNothing (zip xs [0..]))
887collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
888collapseNothing ((Nothing, t) : xs)
889 = (Nothing, t) : filter (\ (x, _) -> case x of
890 Nothing -> False
891 _ -> True) xs
892collapseNothing (x : xs) = x : collapseNothing xs
893collapseNothing [] = []
895noPartial :: [Totality] -> Totality
896noPartial (Partial p : xs) = Partial p
897noPartial (_ : xs) = noPartial xs
898noPartial [] = Total []
900collapse :: [Totality] -> Totality
901collapse xs = collapse' Unchecked xs
902collapse' def (Total r : xs) = Total r
903collapse' def (Unchecked : xs) = collapse' def xs
904collapse' def (d : xs) = collapse' d xs
905-- collapse' Unchecked [] = Total []
906collapse' def [] = def
908totalityCheckBlock :: Idris ()
909totalityCheckBlock = do
910 ist <- getIState
911 -- Do totality checking after entire mutual block
912 mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n
913 ctxt' <- do ctxt <- getContext
914 tclift $ simplifyCasedef n (getErasureInfo ist) ctxt
915 setContext ctxt')
916 (map snd (idris_totcheck ist))
917 mapM_ buildSCG (idris_totcheck ist)
918 mapM_ checkDeclTotality (idris_totcheck ist)
919 clear_totcheck