git.iko.soy/Idris-dev
on ff7ea9d help sign in
Idris-dev/src/Idris/Coverage.hs
880 lines 40 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.Core.TT
12import Idris.Core.Evaluate
13import Idris.Core.CaseTree
15import Idris.AbsSyntax
16import Idris.Delaborate
17import Idris.Error
18import Idris.Output (iWarn, iputStrLn)
20import Data.List
21import Data.Either
22import Data.Maybe
23import Debug.Trace
25import Control.Monad.State.Strict
27-- | Generate a pattern from an 'impossible' LHS.
28--
29-- We need this to eliminate the pattern clauses which have been
30-- provided explicitly from new clause generation.
31mkPatTm :: PTerm -> Idris Term
32mkPatTm t = do i <- getIState
33 let timp = addImpl' True [] [] [] i t
34 evalStateT (toTT (mapPT deNS timp)) 0
35 where
36 toTT (PRef _ _ n) = do i <- lift getIState
37 case lookupNameDef n (tt_ctxt i) of
38 [(n', TyDecl nt _)] -> return $ P nt n' Erased
39 _ -> return $ P Ref n Erased
40 toTT (PApp _ t args) = do t' <- toTT t
41 args' <- mapM (toTT . getTm) args
42 return $ mkApp t' args'
43 toTT (PDPair _ _ _ l _ r) = do l' <- toTT l
44 r' <- toTT r
45 return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
46 toTT (PPair _ _ _ l r) = do l' <- toTT l
47 r' <- toTT r
48 return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
49 -- For alternatives, pick the first and drop the namespaces. It doesn't
50 -- really matter which is taken since matching will ignore the namespace.
51 toTT (PAlternative _ _ (a : as)) = toTT a
52 toTT _ = do v <- get
53 put (v + 1)
54 return (P Bound (sMN v "imp") Erased)
56 deNS (PRef f hl (NS n _)) = PRef f hl n
57 deNS t = t
59-- | Given a list of LHSs, generate a extra clauses which cover the remaining
60-- cases. The ones which haven't been provided are marked 'absurd' so
61-- that the checker will make sure they can't happen.
62--
63-- This will only work after the given clauses have been typechecked and the
64-- names are fully explicit!
65genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
66genClauses fc n xs given
67 = do i <- getIState
68 let lhs_tms = map (\x -> flattenArgs $ delab' i x True True) xs
69 -- if a placeholder was given, don't bother generating cases for it
70 let lhs_tms' = zipWith mergePlaceholders lhs_tms
71 (map (stripUnmatchable i) (map flattenArgs given))
72 let lhss = map pUnApply lhs_tms'
73 nty <- case lookupTyExact n (tt_ctxt i) of
74 Just t -> return (normalise (tt_ctxt i) [] t)
75 _ -> fail "Can't happen - genClauses, lookupTyExact"
77 let argss = transpose lhss
78 let all_args = map (genAll i) (zip (genPH i nty) argss)
79 logCoverage 5 $ "COVERAGE of " ++ show n
80 logCoverage 5 $ "using type " ++ show nty
81 logCoverage 5 $ "non-concrete args " ++ show (genPH i nty)
83 logCoverage 5 $ show (lhs_tms, lhss)
84 logCoverage 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
85 logCoverage 10 $ show argss ++ "\n" ++ 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 (concatMap otherPats (fnub args)) of
207 [] -> [Placeholder]
208 xs -> ph $ inventConsts xs
209 where
210 ph ts = if addPH then Placeholder : ts else ts
212 -- if they're constants, invent a new one to make sure that
213 -- constants which are not explicitly handled are covered
214 inventConsts cs@(PConstant fc c : _) = map (PConstant NoFC) (ic' (mapMaybe getConst cs))
215 where getConst (PConstant _ c) = Just c
216 getConst _ = Nothing
217 inventConsts xs = xs
219 -- try constants until they're not in the list.
220 -- FIXME: It is, of course, possible that someone has enumerated all
221 -- the constants and matched on them (maybe in generated code) and this
222 -- will be really slow. This is sufficiently unlikely that we won't
223 -- worry for now...
225 ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I)
226 ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)
227 ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl)
228 ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8)
229 ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16)
230 ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32)
231 ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
232 ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
233 ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
234 -- The rest are types with only one case
235 ic' xs = xs
237 firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs
238 | otherwise = x : cs
240 lotsOfNums t = map t [0..]
241 lotsOfChars = map Ch ['a'..]
242 lotsOfStrings = map Str (map (("some string " ++).show) [1..])
244 nubMap f acc [] = acc
245 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
247 otherPats :: PTerm -> [PTerm]
248 otherPats o@(PRef fc hl n) = ph $ ops fc n [] o
249 otherPats o@(PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs o
250 otherPats o@(PPair fc hls _ l r)
251 = ph $ ops fc pairCon
252 ([pimp (sUN "A") Placeholder True,
253 pimp (sUN "B") Placeholder True] ++
254 [pexp l, pexp r]) o
255 otherPats o@(PDPair fc hls p t _ v)
256 = ph $ ops fc sigmaCon
257 ([pimp (sUN "a") Placeholder True,
258 pimp (sUN "P") Placeholder True] ++
259 [pexp t,pexp v]) o
260 otherPats o@(PConstant _ c) = ph $ inventConsts [o] -- return o
261 otherPats arg = return Placeholder
263 ops fc n xs o
264 | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)
265 = do xs' <- mapM otherPats (map getExpTm xs)
266 let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))
267 let tyn = getTy n (tt_ctxt i)
268 case lookupCtxt tyn (idris_datatypes i) of
269 (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
270 _ -> [p]
271 ops fc n arg o = return Placeholder
273 getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
274 getExpTm t = getTm t
276 -- put it back to its original form
277 resugar (PApp _ (PRef fc hl n) [_,_,t,v])
278 | n == sigmaCon
279 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)
280 resugar (PApp _ (PRef fc hl n) [_,_,l,r])
281 | n == pairCon
282 = PPair fc [] IsTerm (getTm l) (getTm r)
283 resugar t = t
285 dropForce force (x : xs) i | i `elem` force
286 = upd Placeholder x : dropForce force xs (i + 1)
287 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
288 dropForce _ [] _ = []
291 getTy n ctxt = case lookupTy n ctxt of
292 (t : _) -> case unApply (getRetTy t) of
293 (P _ tyn _, _) -> tyn
294 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
295 _ -> error "Can't happen getTy 2"
297 mkPat fc x = case lookupCtxt x (idris_implicits i) of
298 (pargs : _)
299 -> PApp fc (PRef fc [] x) (map (upd Placeholder) pargs)
300 _ -> error "Can't happen - genAll"
302 fnub :: [PTerm] -> [PTerm]
303 fnub xs = fnub' [] xs
305 fnub' :: [PTerm] -> [PTerm] -> [PTerm]
306 fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
307 | otherwise = fnub' (x : acc) xs
308 fnub' acc [] = acc
310 -- quick check for constructor equality
311 quickEq :: PTerm -> PTerm -> Bool
312 quickEq (PConstant _ n) (PConstant _ n') = n == n'
313 quickEq (PRef _ _ n) (PRef _ _ n') = n == n'
314 quickEq (PApp _ t as) (PApp _ t' as')
315 | length as == length as'
316 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
317 quickEq Placeholder Placeholder = True
318 quickEq x y = False
320 qelem :: PTerm -> [PTerm] -> Bool
321 qelem x [] = False
322 qelem x (y : ys) | x `quickEq` y = True
323 | otherwise = qelem x ys
326upd :: t -> PArg' t -> PArg' t
327upd p' p = p { getTm = p' }
329-- | Check whether function and all descendants cover all cases
330-- (partial is okay, as long as it's due to recursion)
331checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
332checkAllCovering fc done top n | not (n `elem` done)
333 = do i <- get
334 case lookupTotal n (tt_ctxt i) of
335 [tot@(Partial NotCovering)] ->
336 do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n
337 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }
338 addIBC (IBCTotCheckErr fc msg)
339 [Partial _] ->
340 case lookupCtxt n (idris_callgraph i) of
341 [cg] -> mapM_ (checkAllCovering fc (n : done) top)
342 (calls cg)
343 _ -> return ()
344 x -> return () -- stop if total
345checkAllCovering _ _ _ _ = return ()
347-- | Check if, in a given group of type declarations mut_ns, the
348-- constructor cn : ty is strictly positive, and update the context
349-- accordingly
350checkPositive :: [Name] -- ^ the group of type declarations
351 -> (Name, Type) -- ^ the constructor
352 -> Idris Totality
353checkPositive mut_ns (cn, ty')
354 = do i <- getIState
355 let ty = delazy' True (normalise (tt_ctxt i) [] ty')
356 let p = cp i ty
357 let tot = if p then Total (args ty) else Partial NotPositive
358 let ctxt' = setTotal cn tot (tt_ctxt i)
359 putIState (i { tt_ctxt = ctxt' })
360 logCoverage 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns
361 addIBC (IBCTotal cn tot)
362 return tot
363 where
364 args t = [0..length (getArgTys t)-1]
366 cp i (Bind n (Pi _ aty _) sc)
367 = posArg i aty && cp i sc
368 cp i t | (P _ n' _ , args) <- unApply t,
369 n' `elem` mut_ns = all noRec args
370 cp i _ = True
372 posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc
373 posArg ist t = posParams ist t
375 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
377 -- If the type appears recursively in a parameter argument, that's
378 -- fine, otherwise if it appears in an argument it's not fine.
379 posParams ist t | (P _ n _, args) <- unApply t
380 = case lookupCtxtExact n (idris_datatypes ist) of
381 Just ti -> checkParamsOK (param_pos ti) 0 args
382 Nothing -> and (map (posParams ist) args)
383 posParams ist t = noRec t
385 checkParamsOK ppos i [] = True
386 checkParamsOK ppos i (p : ps)
387 | i `elem` ppos = checkParamsOK ppos (i + 1) ps
388 | otherwise = noRec p && checkParamsOK ppos (i + 1) ps
390-- | Calculate the totality of a function from its patterns. Either
391-- follow the size change graph (if inductive) or check for
392-- productivity (if coinductive)
393calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
394calcTotality fc n pats
395 = do i <- getIState
396 let opts = case lookupCtxt n (idris_flags i) of
397 [fs] -> fs
398 _ -> []
399 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
400 (failure : _) -> return failure
401 _ -> checkSizeChange n
402 where
403 checkLHS i (P _ fn _)
404 = case lookupTotalExact fn (tt_ctxt i) of
405 Just (Partial _) -> return (Partial (Other [fn]))
406 _ -> Nothing
407 checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
408 checkLHS _ _ = Nothing
410checkTotality :: [Name] -> FC -> Name -> Idris Totality
411checkTotality path fc n
412 | n `elem` path = return (Partial (Mutual (n : path)))
413 | otherwise = do
414 t <- getTotality n
415 i <- getIState
416 ctxt' <- do ctxt <- getContext
417 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
418 setContext ctxt'
419 ctxt <- getContext
420 i <- getIState
421 let opts = case lookupCtxt n (idris_flags i) of
422 [fs] -> fs
423 _ -> []
424 t' <- case t of
425 Unchecked ->
426 case lookupDef n ctxt of
427 [CaseOp _ _ _ _ pats _] ->
428 do t' <- if AssertTotal `elem` opts
429 then return $ Total []
430 else calcTotality fc n pats
431 logCoverage 2 $ "Set to " ++ show t'
432 setTotality n t'
433 addIBC (IBCTotal n t')
434 return t'
435 [TyDecl (DCon _ _ _) ty] ->
436 case unApply (getRetTy ty) of
437 (P _ tyn _, _) -> do
438 let ms = case lookupCtxt tyn (idris_datatypes i) of
439 [TI _ _ _ _ xs@(_:_)] -> xs
440 ts -> [tyn]
441 checkPositive ms (n, ty)
442 _-> return $ Total []
443 _ -> return $ Total []
444 x -> return x
445 case t' of
446 Total _ -> return t'
447 Productive -> return t'
448 e -> do w <- cmdOptType WarnPartial
449 if TotalFn `elem` opts
450 then do totalityError t'; return t'
451 else do when (w && not (PartialFn `elem` opts)) $
452 warnPartial n t'
453 return t'
454 where
455 totalityError t = do i <- getIState
456 let msg = show n ++ " is " ++ show t
457 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}
458 addIBC (IBCTotCheckErr fc msg)
460 warnPartial n t
461 = do i <- getIState
462 case lookupDef n (tt_ctxt i) of
463 [x] -> do
464 iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t
465-- ++ "\n" ++ show x
466-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
467-- iputStrLn (show cg)
470checkDeclTotality :: (FC, Name) -> Idris Totality
471checkDeclTotality (fc, n)
472 = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"
473 i <- getIState
474 let opts = case lookupCtxtExact n (idris_flags i) of
475 Just fs -> fs
476 _ -> []
477 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
478 t <- checkTotality [] fc n
479 return t
481-- If the name calls something which is partial, set it as partial
482verifyTotality :: (FC, Name) -> Idris ()
483verifyTotality (fc, n)
484 = do logCoverage 2 $ "Checking " ++ show n ++ "'s descendents are total"
485 ist <- getIState
486 case lookupTotalExact n (tt_ctxt ist) of
487 Just (Total _) -> do
488 let ns = getNames (tt_ctxt ist)
490 case getPartial ist [] ns of
491 Nothing -> return ()
492 Just bad -> do let t' = Partial (Other bad)
493 logCoverage 2 $ "Set to " ++ show t'
494 setTotality n t'
495 addIBC (IBCTotal n t')
496 _ -> return ()
497 where
498 getNames ctxt = case lookupDefExact n ctxt of
499 Just (CaseOp _ _ _ _ _ defs)
500 -> let (top, def) = cases_compiletime defs in
501 map fst (findCalls' True def top)
502 _ -> []
504 getPartial ist [] [] = Nothing
505 getPartial ist bad [] = Just bad
506 getPartial ist bad (n : ns)
507 = case lookupTotalExact n (tt_ctxt ist) of
508 Just (Partial _) -> getPartial ist (n : bad) ns
509 _ -> getPartial ist bad ns
511-- | Calculate the size change graph for this definition
512--
513-- SCG for a function f consists of a list of:
514-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
515--
516-- where g is a function called
517-- a1 ... an are the arguments of f in positions 1..n of g
518-- sizechange1 ... sizechange2 is how their size has changed wrt the input
519-- to f
520-- Nothing, if the argument is unrelated to the input
521buildSCG :: (FC, Name) -> Idris ()
522buildSCG (_, n) = do
523 ist <- getIState
524 case lookupCtxt n (idris_callgraph ist) of
525 [cg] -> case lookupDefExact n (tt_ctxt ist) of
526 Just (CaseOp _ _ _ pats _ cd) ->
527 let (args, sc) = cases_totcheck cd in
528 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"
529 ++ show pats ++ "\n" ++ show sc
530 let newscg = buildSCG' ist n (rights pats) args
531 logCoverage 5 $ "SCG is: " ++ show newscg
532 addToCG n ( cg { scg = newscg } )
533 _ -> return () -- CG comes from a type declaration only
534 [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"
535 x -> error $ "buildSCG: " ++ show (n, x)
537delazy = delazy' False -- not lazy codata
538delazy' all t@(App _ f a)
539 | (P _ (UN l) _, [_, _, arg]) <- unApply t,
540 l == txt "Force" = delazy' all arg
541 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
542 l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg
543 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
544 l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg
545delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
546delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
547delazy' all t = t
549data Guardedness = Toplevel | Unguarded | Guarded | Delayed
550 deriving Show
552buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
553buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
554 scgPat (lhs, rhs) = let lhs' = delazy lhs
555 rhs' = delazy rhs
556 (f, pargs) = unApply (dePat lhs') in
557 findCalls [] Toplevel (dePat rhs') (patvars lhs')
558 (zip pargs [0..])
560 -- Under a delay, calls are excluded from the graph - if it's a call to a
561 -- non-total function we'll find that in the final totality check
562 findCalls cases Delayed ap@(P _ n _) pvs args = []
563 findCalls cases guarded ap@(App _ f a) pvs pargs
564 -- under a call to "assert_total", don't do any checking, just believe
565 -- that it is total.
566 | (P _ (UN at) _, [_, _]) <- unApply ap,
567 at == txt "assert_total" = []
568 -- don't go under calls to functions which are asserted total
569 | (P _ n _, _) <- unApply ap,
570 Just opts <- lookupCtxtExact n (idris_flags ist),
571 AssertTotal `elem` opts = []
572 -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't
573 -- check under guarded constructors.
574 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
575 Guarded <- guarded,
576 del == txt "Delay"
577 = findCalls cases Delayed arg pvs pargs
578 | (P _ n _, args) <- unApply ap,
579 Delayed <- guarded,
580 isConName n (tt_ctxt ist)
581 = -- Still under a 'Delay' and constructor guarded, so check
582 -- just the arguments to the constructor, remaining Delayed
583 concatMap (\x -> findCalls cases guarded x pvs pargs) args
584 | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,
585 ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]
586 -- Continue look inside if...then...else blocks
587 -- TODO: Consider whether we should do this for user defined ifThenElse
588 -- rather than just the one in the Prelude as a special case
589 = findCalls cases guarded t pvs pargs ++
590 findCalls cases guarded e pvs pargs
591 | (P _ n _, args) <- unApply ap,
592 caseName n && n /= topfn,
593 notPartial (lookupTotalExact n (tt_ctxt ist))
594 -- case block - look inside the block, as long as it was covering
595 -- (i.e. not currently set at Partial) to get a more accurate size
596 -- change result from the top level patterns (also to help pass
597 -- information through from guarded corecursion accurately)
598 = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args ++
599 if n `notElem` cases
600 then findCallsCase (n : cases) guarded n args pvs pargs
601 else []
602 | (P _ n _, args) <- unApply ap,
603 Delayed <- guarded
604 -- Under a delayed recursive call just check the arguments
605 = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args
606 | (P _ n _, args) <- unApply ap
607 -- Ordinary call, not under a delay.
608 -- If n is a constructor, set 'args' as Guarded
609 = let nguarded = case guarded of
610 Unguarded -> Unguarded
611 x -> if isConName n (tt_ctxt ist)
612 then Guarded
613 else Unguarded in
614 mkChange n args pargs ++
615 concatMap (\x -> findCalls cases nguarded x pvs pargs) args
616 where notPartial (Just (Partial NotCovering)) = False
617 notPartial _ = True
618 findCalls cases guarded (App _ f a) pvs pargs
619 = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs
620 findCalls cases guarded (Bind n (Let t v) e) pvs pargs
621 = findCalls cases Unguarded t pvs pargs ++
622 findCalls cases Unguarded v pvs pargs ++ findCalls cases guarded e (n : pvs) pargs
623 findCalls cases guarded (Bind n t e) pvs pargs
624 = findCalls cases Unguarded (binderTy t) pvs pargs ++
625 findCalls cases guarded e (n : pvs) pargs
626 findCalls cases guarded (P _ f _ ) pvs pargs
627 | not (f `elem` pvs) = [(f, [])]
628 findCalls _ _ _ _ _ = []
630 -- Assumption is that names are preserved in the case block (shadowing
631 -- dealt with by the elaborator) so we can just assume the top level names
632 -- are okay for building the size change
633 findCallsCase cases guarded n args pvs pargs
634 = case lookupDefExact n (tt_ctxt ist) of
635 Just (CaseOp _ _ _ pats _ cd) ->
636 concatMap (fccPat cases pvs pargs args guarded) (rights pats)
637 Nothing -> []
639 fccPat cases pvs pargs args g (lhs, rhs)
640 = let lhs' = delazy lhs
641 rhs' = delazy rhs
642 (f, pargs_case) = unApply (dePat lhs')
643 -- pargs is a pair of a term, and the argument position that
644 -- term appears in. If any of the arguments to the case block
645 -- are also on the lhs, we also want those patterns to appear
646 -- in the parg list so that we'll spot patterns which are
647 -- smaller than then
648 newpargs = newPArg args pargs
649 -- Now need to update the rhs of the case with the names in the
650 -- outer definition: In rhs', wherever we see what's in pargs_case,
651 -- replace it with the corresponding thing in pargs
652 csubs = zip pargs_case args
653 newrhs = doCaseSubs csubs (dePat rhs')
654 pargs' = pargs ++ addPArg newpargs pargs_case in
655 findCalls cases g newrhs pvs pargs'
656 where
657 doCaseSubs [] tm = tm
658 doCaseSubs ((x, x') : cs) tm
659 = doCaseSubs (subIn x x' cs) (substTerm x x' tm)
661 subIn x x' [] = []
662 subIn x x' ((l, r) : cs)
663 = (substTerm x x' l, substTerm x x' r) : subIn x x' cs
665 addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'
666 addPArg (Nothing : ts) (t' : ts') = addPArg ts ts'
667 addPArg _ _ = []
669 newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
670 newPArg (t : ts) pargs = case lookup t pargs of
671 Just i -> Just (t, i) : newPArg ts pargs
672 Nothing -> Nothing : newPArg ts pargs
673 newPArg [] pargs = []
675 expandToArity n args
676 = case lookupTy n (tt_ctxt ist) of
677 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
678 _ -> args
679 where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
680 expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []
681 expand i _ xs = xs
683 mkChange n args pargs = [(n, expandToArity n (sizes args))]
684 where
685 sizes [] = []
686 sizes (a : as) = checkSize a pargs : sizes as
688 -- find which argument in pargs <a> is smaller than, if any
689 checkSize a ((p, i) : ps)
690 | a == p = Just (i, Same)
691 | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
692 as == txt "assert_smaller" && arg == p
693 = Just (i, Smaller)
694 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
695 | otherwise = checkSize a ps
696 checkSize a [] = Nothing
698 -- the smaller thing we find must be defined in the same group of mutally
699 -- defined types as <a>, and not be coinductive - so carry the type of
700 -- the constructor we've gone under.
702 smaller (Just tyn) a (t, Just tyt)
703 | a == t = isInductive (fst (unApply (getRetTy tyn)))
704 (fst (unApply (getRetTy tyt)))
705 smaller ty a (ap@(App _ f s), _)
706 | (P (DCon _ _ _) n _, args) <- unApply ap
707 = let tyn = getType n in
708 any (smaller (ty `mplus` Just tyn) a)
709 (zip args (map toJust (getArgTys tyn)))
710 -- check higher order recursive arguments
711 smaller ty (App _ f s) a = smaller ty f a
712 smaller _ _ _ = False
714 toJust (n, t) = Just t
716 getType n = case lookupTyExact n (tt_ctxt ist) of
717 Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
719 isInductive (P _ nty _) (P _ nty' _) =
720 let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of
721 [TI _ x _ _ muts] -> (x, muts)
722 _ -> (False, []) in
723 (nty == nty' || any (== nty') muts) && not co
724 isInductive _ _ = False
726 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
727 dePat t = t
729 patvars (Bind x (PVar _) sc) = x : patvars sc
730 patvars _ = []
732checkSizeChange :: Name -> Idris Totality
733checkSizeChange n = do
734 ist <- getIState
735 case lookupCtxt n (idris_callgraph ist) of
736 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
737 logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++
738 "from " ++ show (scg cg) ++ "\n" ++
739 show (length ms) ++ "\n" ++
740 showSep "\n" (map show ms))
741 logCoverage 6 (show cg)
742 -- every multipath must have an infinitely descending
743 -- thread, then the function terminates
744 -- also need to checks functions called are all total
745 -- (Unchecked is okay as we'll spot problems here)
746 let tot = map (checkMP ist n (getArity ist n)) ms
747 logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"
748 logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++
749 (showSep "\n" (map show (zip ms tot)))
750 return (noPartial tot)
751 [] -> do logCoverage 5 $ "No paths for " ++ show n
752 return Unchecked
753 where getArity ist n
754 = case lookupTy n (tt_ctxt ist) of
755 [ty] -> arity (normalise (tt_ctxt ist) [] ty)
756 _ -> error "Can't happen: checkSizeChange.getArity"
758type MultiPath = [SCGEntry]
760mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
761mkMultiPaths ist path [] = [reverse path]
762mkMultiPaths ist path cg = concatMap extend cg
763 where extend (nextf, args)
764 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
765 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
766 = case lookupCtxt nextf (idris_callgraph ist) of
767 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
768 _ -> [ reverse ((nextf, args) : path) ]
769 | otherwise = [ reverse ((nextf, args) : path) ]
771-- If any route along the multipath leads to infinite descent, we're fine.
772-- Try a route beginning with every argument.
773-- If we reach a point we've been to before, but with a smaller value,
774-- that means there is an infinitely descending path from that argument.
776checkMP :: IState -> Name -> Int -> MultiPath -> Totality
777checkMP ist topfn i mp = if i > 0
778 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
779-- trace ("Paths " ++ show paths) $
780 collapse paths
781 else tryPath 0 [] mp 0
782 where
783 tryPath' d path mp arg
784 = let res = tryPath d path mp arg in
785 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
787 mkBig (e, d) = (e, 10000)
789 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
790 tryPath desc path [] _ = Total []
791-- tryPath desc path ((UN "believe_me", _) : _) arg
792-- = Partial BelieveMe
793 -- if we get to a constructor, it's fine as long as it's strictly positive
794 tryPath desc path ((f, _) : es) arg
795 | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
796 = case lookupTotalExact f (tt_ctxt ist) of
797 Just (Total _) -> Unchecked -- okay so far
798 Just (Partial _) -> Partial (Other [f])
799 x -> Unchecked -- An error elsewhere, set as Unchecked to make
800 -- some progress
801 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
802 = Total []
803 tryPath desc path (e@(f, args) : es) arg
804 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
805 | e `elem` es && allNothing args = Partial (Mutual [f])
806 tryPath desc path (e@(f, nextargs) : es) arg
807 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
808 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
809 | Just d <- lookup (e, arg) path
810 = if desc - d > 0 -- Now lower than when we were last here
811 then -- trace ("Descent " ++ show (desc - d) ++ " "
812 -- ++ show (path, e)) $
813 Total []
814 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
815 | e `elem` map (fst . fst) path
816 && not (f `elem` map fst es)
817 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
818 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
819 let argspos = zip nextargs [0..]
820 pathres =
821 do (a, pos) <- argspos
822 case a of
823 Nothing -> -- gone up, but if the
824 -- rest definitely terminates without any
825 -- cycles (including the path so far, which
826 -- we take as inaccessible) the path is fine
827 return $ tryPath 0 (map mkBig (((e, arg), desc) : path)) es pos
828 Just (nextarg, sc) ->
829 if nextarg == arg then
830 case sc of
831 Same -> return $ tryPath desc (((e, arg), desc) : path)
832 es pos
833 Smaller -> return $ tryPath (desc+1)
834 (((e, arg), desc) : path)
835 es
836 pos
837 _ -> trace ("Shouldn't happen " ++ show e) $
838 return (Partial Itself)
839 else return Unchecked in
840-- trace (show (desc, argspos, path, es, pathres)) $
841 collapse pathres
843 | otherwise = Unchecked
845allNothing :: [Maybe a] -> Bool
846allNothing xs = null (collapseNothing (zip xs [0..]))
848collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
849collapseNothing ((Nothing, t) : xs)
850 = (Nothing, t) : filter (\ (x, _) -> case x of
851 Nothing -> False
852 _ -> True) xs
853collapseNothing (x : xs) = x : collapseNothing xs
854collapseNothing [] = []
856noPartial :: [Totality] -> Totality
857noPartial (Partial p : xs) = Partial p
858noPartial (_ : xs) = noPartial xs
859noPartial [] = Total []
861collapse :: [Totality] -> Totality
862collapse xs = collapse' Unchecked xs
863collapse' def (Total r : xs) = Total r
864collapse' def (Unchecked : xs) = collapse' def xs
865collapse' def (d : xs) = collapse' d xs
866-- collapse' Unchecked [] = Total []
867collapse' def [] = def
869totalityCheckBlock :: Idris ()
870totalityCheckBlock = do
871 ist <- getIState
872 -- Do totality checking after entire mutual block
873 mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n
874 ctxt' <- do ctxt <- getContext
875 tclift $ simplifyCasedef n (getErasureInfo ist) ctxt
876 setContext ctxt')
877 (map snd (idris_totcheck ist))
878 mapM_ buildSCG (idris_totcheck ist)
879 mapM_ checkDeclTotality (idris_totcheck ist)
880 clear_totcheck