git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/src/Idris/Coverage.hs
782 lines 34 kB history raw
1{-# LANGUAGE PatternGuards #-}
2{-| The coverage and totality checkers for Idris are in this module.
3-}
4module Idris.Coverage where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.CaseTree
10import Idris.AbsSyntax
11import Idris.Delaborate
12import Idris.Error
13import Idris.Output (iWarn, iputStrLn)
15import Data.List
16import Data.Either
17import Data.Maybe
18import Debug.Trace
20import Control.Monad.State.Strict
22-- | Generate a pattern from an 'impossible' LHS.
23--
24-- We need this to eliminate the pattern clauses which have been
25-- provided explicitly from new clause generation.
26mkPatTm :: PTerm -> Idris Term
27mkPatTm t = do i <- getIState
28 let timp = addImpl' True [] [] [] i t
29 evalStateT (toTT (mapPT deNS timp)) 0
30 where
31 toTT (PRef _ _ n) = do i <- lift getIState
32 case lookupNameDef n (tt_ctxt i) of
33 [(n', TyDecl nt _)] -> return $ P nt n' Erased
34 _ -> return $ P Ref n Erased
35 toTT (PApp _ t args) = do t' <- toTT t
36 args' <- mapM (toTT . getTm) args
37 return $ mkApp t' args'
38 -- For alternatives, pick the first and drop the namespaces. It doesn't
39 -- really matter which is taken since matching will ignore the namespace.
40 toTT (PAlternative _ _ (a : as)) = toTT a
41 toTT _ = do v <- get
42 put (v + 1)
43 return (P Bound (sMN v "imp") Erased)
45 deNS (PRef f hl (NS n _)) = PRef f hl n
46 deNS t = t
48-- | Given a list of LHSs, generate a extra clauses which cover the remaining
49-- cases. The ones which haven't been provided are marked 'absurd' so
50-- that the checker will make sure they can't happen.
51--
52-- This will only work after the given clauses have been typechecked and the
53-- names are fully explicit!
54genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
55genClauses fc n xs given
56 = do i <- getIState
57 let lhs_tms = map (\x -> delab' i x True True) xs
58 -- if a placeholder was given, don't bother generating cases for it
59 let lhs_tms' = zipWith mergePlaceholders lhs_tms
60 (map (stripUnmatchable i) given)
61 let lhss = map pUnApply lhs_tms'
63 let argss = transpose lhss
64 let all_args = map (genAll i) argss
65 logLvl 5 $ "COVERAGE of " ++ show n
66 logLvl 5 $ show lhss
67 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
68 logLvl 10 $ show argss ++ "\n" ++ show all_args
69 logLvl 3 $ "Original: \n" ++
70 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
71 -- add an infinite supply of explicit arguments to update the possible
72 -- cases for (the return type may be variadic, or function type, so
73 -- there may be more case splitting that the idris_implicits record
74 -- suggests)
75 let parg = case lookupCtxt n (idris_implicits i) of
76 (p : _) ->
77 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)
78 _ -> repeat (pexp Placeholder)
79 let tryclauses = mkClauses parg all_args
80 logLvl 3 $ show (length tryclauses) ++ " initially to check"
81 logLvl 2 $ showSep "\n" (map (showTm i) tryclauses)
82 let new = filter (noMatch i) (nub tryclauses)
83 logLvl 2 $ show (length new) ++ " clauses to check for impossibility"
84 logLvl 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
85-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
86 return new
87-- return (map (\t -> PClause n t [] PImpossible []) new)
88 where getLHS i term
89 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
90 | otherwise = []
92 pUnApply (PApp _ _ args) = map getTm args
93 pUnApply _ = []
95 -- Return whether the given clause matches none of the input clauses
96 -- (xs)
97 noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of
98 Right ms -> False
99 Left miss -> True) xs
102 mergePlaceholders :: PTerm -> PTerm -> PTerm
103 mergePlaceholders x Placeholder = Placeholder
104 mergePlaceholders (PApp fc f args) (PApp fc' f' args')
105 = PApp fc' f' (zipWith mergePArg args args')
106 where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in
107 x { getTm = xtm}
108 mergePlaceholders x _ = x
110 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
111 mkClauses parg args
112 | all (== [Placeholder]) args = []
113 mkClauses parg args
114 = do args' <- mkArg args
115 let tm = PApp fc (PRef fc [] n) (zipWith upd args' parg)
116 return tm
117 where
118 mkArg :: [[PTerm]] -> [[PTerm]]
119 mkArg [] = return []
120 mkArg (a : as) = do a' <- a
121 as' <- mkArg as
122 return (a':as')
124-- | Does this error result rule out a case as valid when coverage checking?
125validCoverageCase :: Context -> Err -> Bool
126validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
127 = let topx' = normalise ctxt [] topx
128 topy' = normalise ctxt [] topy in
129 not (sameFam topx' topy' || not (validCoverageCase ctxt e))
130 where sameFam topx topy
131 = case (unApply topx, unApply topy) of
132 ((P _ x _, _), (P _ y _, _)) -> x == y
133 _ -> False
134validCoverageCase ctxt (CantConvert _ _ _) = False
135validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e
136validCoverageCase ctxt (Elaborating _ _ e) = validCoverageCase ctxt e
137validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e
138validCoverageCase ctxt _ = True
140-- | Check whether an error is recoverable in the sense needed for
141-- coverage checking.
142recoverableCoverage :: Context -> Err -> Bool
143recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)
144 = let topx' = normalise ctxt [] topx
145 topy' = normalise ctxt [] topy in
146 r || checkRec topx' topy'
147 where -- different notion of recoverable than in unification, since we
148 -- have no metavars -- just looking to see if a constructor is failing
149 -- to unify with a function that may be reduced later
150 checkRec (App _ f a) p@(P _ _ _) = checkRec f p
151 checkRec p@(P _ _ _) (App _ f a) = checkRec p f
152 checkRec fa@(App _ _ _) fa'@(App _ _ _)
153 | (f, as) <- unApply fa,
154 (f', as') <- unApply fa'
155 = if (length as /= length as')
156 then checkRec f f'
157 else checkRec f f' && and (zipWith checkRec as as')
158 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
159 checkRec _ _ = False
161 ntRec x y | Ref <- x = True
162 | Ref <- y = True
163 | (Bound, Bound) <- (x, y) = True
164 | otherwise = False -- name is different, unrecoverable
165recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e
166recoverableCoverage ctxt (Elaborating _ _ e) = recoverableCoverage ctxt e
167recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
168recoverableCoverage _ _ = False
170-- FIXME: Just look for which one is the deepest, then generate all
171-- possibilities up to that depth.
172-- This and below issues for this function are tracked as Issue #1741 on the issue tracker.
173-- https://github.com/idris-lang/Idris-dev/issues/1741
174genAll :: IState -> [PTerm] -> [PTerm]
175genAll i args
176 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
177 [] -> [Placeholder]
178 xs -> inventConsts xs
179 where
180 -- if they're constants, invent a new one to make sure that
181 -- constants which are not explicitly handled are covered
182 inventConsts cs@(PConstant fc c : _) = map (PConstant NoFC) (ic' (mapMaybe getConst cs))
183 where getConst (PConstant _ c) = Just c
184 getConst _ = Nothing
185 inventConsts xs = xs
187 -- try constants until they're not in the list.
188 -- FIXME: It is, of course, possible that someone has enumerated all
189 -- the constants and matched on them (maybe in generated code) and this
190 -- will be really slow. This is sufficiently unlikely that we won't
191 -- worry for now...
193 ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I)
194 ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)
195 ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl)
196 ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8)
197 ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16)
198 ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32)
199 ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
200 ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
201 ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
202 -- TODO: Bit vectors
203 -- The rest are types with only one case
204 ic' xs = xs
206 firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs
207 | otherwise = x : cs
209 lotsOfNums t = map t [0..]
210 lotsOfChars = map Ch ['a'..]
211 lotsOfStrings = map Str (map (("some string " ++).show) [1..])
213 nubMap f acc [] = acc
214 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
216 otherPats :: PTerm -> [PTerm]
217 otherPats o@(PRef fc hl n) = ops fc n [] o
218 otherPats o@(PApp _ (PRef fc hl n) xs) = ops fc n xs o
219 otherPats o@(PPair fc hls _ l r)
220 = ops fc pairCon
221 ([pimp (sUN "A") Placeholder True,
222 pimp (sUN "B") Placeholder True] ++
223 [pexp l, pexp r]) o
224 otherPats o@(PDPair fc hls p t _ v)
225 = ops fc sigmaCon
226 ([pimp (sUN "a") Placeholder True,
227 pimp (sUN "P") Placeholder True] ++
228 [pexp t,pexp v]) o
229 otherPats o@(PConstant _ c) = inventConsts [o] -- return o
230 otherPats arg = return Placeholder
232 ops fc n xs o
233 | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)
234 = do xs' <- mapM otherPats (map getExpTm xs)
235 let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))
236 let tyn = getTy n (tt_ctxt i)
237 case lookupCtxt tyn (idris_datatypes i) of
238 (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
239 _ -> [p]
240 ops fc n arg o = return Placeholder
242 getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
243 getExpTm t = getTm t
245 -- put it back to its original form
246 resugar (PApp _ (PRef fc hl n) [_,_,t,v])
247 | n == sigmaCon
248 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)
249 resugar (PApp _ (PRef fc hl n) [_,_,l,r])
250 | n == pairCon
251 = PPair fc [] IsTerm (getTm l) (getTm r)
252 resugar t = t
254 dropForce force (x : xs) i | i `elem` force
255 = upd Placeholder x : dropForce force xs (i + 1)
256 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
257 dropForce _ [] _ = []
260 getTy n ctxt = case lookupTy n ctxt of
261 (t : _) -> case unApply (getRetTy t) of
262 (P _ tyn _, _) -> tyn
263 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
264 _ -> error "Can't happen getTy 2"
266 mkPat fc x = case lookupCtxt x (idris_implicits i) of
267 (pargs : _)
268 -> PApp fc (PRef fc [] x) (map (upd Placeholder) pargs)
269 _ -> error "Can't happen - genAll"
271 fnub :: [PTerm] -> [PTerm]
272 fnub xs = fnub' [] xs
274 fnub' :: [PTerm] -> [PTerm] -> [PTerm]
275 fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
276 | otherwise = fnub' (x : acc) xs
277 fnub' acc [] = acc
279 -- quick check for constructor equality
280 quickEq :: PTerm -> PTerm -> Bool
281 quickEq (PConstant _ n) (PConstant _ n') = n == n'
282 quickEq (PRef _ _ n) (PRef _ _ n') = n == n'
283 quickEq (PApp _ t as) (PApp _ t' as')
284 | length as == length as'
285 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
286 quickEq Placeholder Placeholder = True
287 quickEq x y = False
289 qelem :: PTerm -> [PTerm] -> Bool
290 qelem x [] = False
291 qelem x (y : ys) | x `quickEq` y = True
292 | otherwise = qelem x ys
295upd :: t -> PArg' t -> PArg' t
296upd p' p = p { getTm = p' }
298-- Check whether function and all descendants cover all cases (partial is
299-- okay, as long as it's due to recursion)
301checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
302checkAllCovering fc done top n | not (n `elem` done)
303 = do i <- get
304 case lookupTotal n (tt_ctxt i) of
305 [tot@(Partial NotCovering)] ->
306 do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n
307 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }
308 addIBC (IBCTotCheckErr fc msg)
309 [Partial _] ->
310 case lookupCtxt n (idris_callgraph i) of
311 [cg] -> mapM_ (checkAllCovering fc (n : done) top)
312 (map fst (calls cg))
313 _ -> return ()
314 x -> return () -- stop if total
315checkAllCovering _ _ _ _ = return ()
317-- Check if, in a given group of type declarations mut_ns,
318-- the constructor cn : ty is strictly positive,
319-- and update the context accordingly
321checkPositive :: [Name] -> (Name, Type) -> Idris Totality
322checkPositive mut_ns (cn, ty')
323 = do let ty = delazy' True ty'
324 let p = cp ty
325 i <- getIState
326 let tot = if p then Total (args ty) else Partial NotPositive
327 let ctxt' = setTotal cn tot (tt_ctxt i)
328 putIState (i { tt_ctxt = ctxt' })
329 logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns
330 addIBC (IBCTotal cn tot)
331 return tot
332 where
333 args t = [0..length (getArgTys t)-1]
335 cp (Bind n (Pi _ aty _) sc) = posArg aty && cp sc
336 cp t | (P _ n' _, args) <- unApply t,
337 n' `elem` mut_ns = all noRec args
338 cp _ = True
340 posArg (Bind _ (Pi _ nty _) sc)
341 | (P _ n' _, args) <- unApply nty
342 = n' `notElem` mut_ns && all noRec args && posArg sc
343 posArg t | (P _ n' _, args) <- unApply t,
344 n' `elem` mut_ns = all noRec args
345 posArg _ = True
347 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
350calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
351calcProd i fc topn pats
352 = cp topn pats []
353 where
354 -- every application of n must be in an argument of a coinductive
355 -- constructor, in every function reachable from here in the
356 -- call graph.
357 cp n pats done = do patsprod <- mapM (prodRec n done) pats
358 if (and patsprod)
359 then return Productive
360 else return (Partial NotProductive)
362 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
363 prodRec n done _ | n `elem` done = return True
364 prodRec n done (_, _, tm) = prod n done False (delazy' True tm)
366 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
367 prod n done ok ap@(App _ _ _)
368 | (P nt f _, args) <- unApply ap
369 = do recOK <- checkProdRec (n:done) f
370 let ctxt = tt_ctxt i
371 let [ty] = lookupTy f ctxt -- must exist!
372 let co = cotype nt f ty in
373 if (not recOK) then return False else
374 if f == topn
375 then do argsprod <- mapM (prod n done co) args
376 return (and (ok : argsprod) )
377 else do argsprod <- mapM (prod n done co) args
378 return (and argsprod)
379 prod n done ok (App _ f a) = liftM2 (&&) (prod n done False f)
380 (prod n done False a)
381 prod n done ok (Bind _ (Let t v) sc)
382 = liftM2 (&&) (prod n done False v) (prod n done False v)
383 prod n done ok (Bind _ b sc) = prod n done ok sc
384 prod n done ok t = return True
386 checkProdRec :: [Name] -> Name -> Idris Bool
387 checkProdRec done f
388 = case lookupCtxt f (idris_patdefs i) of
389 [(def, _)] -> do ok <- mapM (prodRec f done) def
390 return (and ok)
391 _ -> return True -- defined elsewhere, can't call topn
393 cotype (DCon _ _ _) n ty
394 | (P _ t _, _) <- unApply (getRetTy ty)
395 = case lookupCtxt t (idris_datatypes i) of
396 [TI _ True _ _ _] -> True
397 _ -> False
398 cotype nt n ty = False
400-- | Calculate the totality of a function from its patterns.
401-- Either follow the size change graph (if inductive) or check for
402-- productivity (if coinductive)
403calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
404calcTotality fc n pats
405 = do i <- getIState
406 let opts = case lookupCtxt n (idris_flags i) of
407 [fs] -> fs
408 _ -> []
409 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
410 (failure : _) -> return failure
411 _ -> checkSizeChange n
412 where
413 checkLHS i (P _ fn _)
414 = case lookupTotal fn (tt_ctxt i) of
415 [Partial _] -> return (Partial (Other [fn]))
416 _ -> Nothing
417 checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
418 checkLHS _ _ = Nothing
420checkTotality :: [Name] -> FC -> Name -> Idris Totality
421checkTotality path fc n
422 | n `elem` path = return (Partial (Mutual (n : path)))
423 | otherwise = do
424 t <- getTotality n
425 i <- getIState
426 ctxt' <- do ctxt <- getContext
427 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
428 setContext ctxt'
429 ctxt <- getContext
430 i <- getIState
431 let opts = case lookupCtxt n (idris_flags i) of
432 [fs] -> fs
433 _ -> []
434 t' <- case t of
435 Unchecked ->
436 case lookupDef n ctxt of
437 [CaseOp _ _ _ _ pats _] ->
438 do t' <- if AssertTotal `elem` opts
439 then return $ Total []
440 else calcTotality fc n pats
441 setTotality n t'
442 addIBC (IBCTotal n t')
443 return t'
444 [TyDecl (DCon _ _ _) ty] ->
445 case unApply (getRetTy ty) of
446 (P _ tyn _, _) -> do
447 let ms = case lookupCtxt tyn (idris_datatypes i) of
448 [TI _ _ _ _ xs@(_:_)] -> xs
449 ts -> [tyn]
450 checkPositive ms (n, ty)
451 _-> return $ Total []
452 _ -> return $ Total []
453 x -> return x
454 case t' of
455 Total _ -> return t'
456 Productive -> return t'
457 e -> do w <- cmdOptType WarnPartial
458 if TotalFn `elem` opts
459 then do totalityError t'; return t'
460 else do when (w && not (PartialFn `elem` opts)) $
461 warnPartial n t'
462 return t'
463 where
464 totalityError t = do i <- getIState
465 let msg = show n ++ " is " ++ show t
466 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}
467 addIBC (IBCTotCheckErr fc msg)
469 warnPartial n t
470 = do i <- getIState
471 case lookupDef n (tt_ctxt i) of
472 [x] -> do
473 iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t
474-- ++ "\n" ++ show x
475-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
476-- iputStrLn (show cg)
479checkDeclTotality :: (FC, Name) -> Idris Totality
480checkDeclTotality (fc, n)
481 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
482-- buildSCG (fc, n)
483-- logLvl 2 $ "Built SCG"
484 i <- getIState
485 let opts = case lookupCtxt n (idris_flags i) of
486 [fs] -> fs
487 _ -> []
488 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
489 t <- checkTotality [] fc n
490 case t of
491 -- if it's not total, it can't reduce, to keep
492 -- typechecking decidable
493 p@(Partial _) -> do setAccessibility n Frozen
494 addIBC (IBCAccess n Frozen)
495 logLvl 5 $ "HIDDEN: "
496 ++ show n ++ show p
497 _ -> return ()
498 return t
501-- | Calculate the size change graph for this definition
502--
503-- SCG for a function f consists of a list of:
504-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
505--
506-- where g is a function called
507-- a1 ... an are the arguments of f in positions 1..n of g
508-- sizechange1 ... sizechange2 is how their size has changed wrt the input
509-- to f
510-- Nothing, if the argument is unrelated to the input
511buildSCG :: (FC, Name) -> Idris ()
512buildSCG (_, n) = do
513 ist <- getIState
514 case lookupCtxt n (idris_callgraph ist) of
515 [cg] -> case lookupDefExact n (tt_ctxt ist) of
516 Just (CaseOp _ _ _ pats _ cd) ->
517 let (args, sc) = cases_totcheck cd in
518 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
519 ++ show pats ++ "\n" ++ show sc
520 let newscg = buildSCG' ist (rights pats) args
521 logLvl 5 $ "SCG is: " ++ show newscg
522 addToCG n ( cg { scg = newscg } )
523 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
524 x -> error $ "buildSCG: " ++ show (n, x)
526delazy = delazy' False -- not lazy codata
527delazy' all t@(App _ f a)
528 | (P _ (UN l) _, [_, _, arg]) <- unApply t,
529 l == txt "Force" = delazy' all arg
530 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
531 l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg
532 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
533 l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg
534delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
535delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
536delazy' all t = t
538data Guardedness = Toplevel | Unguarded | Guarded
539 deriving Show
541buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
542buildSCG' ist pats args = nub $ concatMap scgPat pats where
543 scgPat (lhs, rhs) = let lhs' = delazy lhs
544 rhs' = delazy rhs
545 (f, pargs) = unApply (dePat lhs') in
546 findCalls Toplevel (dePat rhs') (patvars lhs') pargs
548 findCalls guarded ap@(App _ f a) pvs pargs
549 -- under a call to "assert_total", don't do any checking, just believe
550 -- that it is total.
551 | (P _ (UN at) _, [_, _]) <- unApply ap,
552 at == txt "assert_total" = []
553 -- under a call to "Delay LazyCodata", don't do any checking of the
554 -- immediate call, as long as the call is guarded.
555 -- Then check its arguments
556 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
557 Guarded <- guarded,
558 del == txt "Delay"
559 = let (capp, args) = unApply arg in
560 concatMap (\x -> findCalls guarded x pvs pargs) args
561 | (P _ n _, args) <- unApply ap
562 = let nguarded = case guarded of
563 Unguarded -> Unguarded
564 _ -> if isConName n (tt_ctxt ist)
565 then Guarded
566 else Unguarded in
567 mkChange n args pargs ++
568 concatMap (\x -> findCalls nguarded x pvs pargs) args
569 findCalls guarded (App _ f a) pvs pargs
570 = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs
571 findCalls guarded (Bind n (Let t v) e) pvs pargs
572 = findCalls Unguarded t pvs pargs ++
573 findCalls Unguarded v pvs pargs ++ findCalls guarded e (n : pvs) pargs
574 findCalls guarded (Bind n t e) pvs pargs
575 = findCalls Unguarded (binderTy t) pvs pargs ++
576 findCalls guarded e (n : pvs) pargs
577 findCalls guarded (P _ f _ ) pvs pargs
578 | not (f `elem` pvs) = [(f, [])]
579 findCalls _ _ _ _ = []
581 expandToArity n args
582 = case lookupTy n (tt_ctxt ist) of
583 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
584 _ -> args
585 where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
586 expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []
587 expand i _ xs = xs
589 mkChange n args pargs = [(n, expandToArity n (sizes args))]
590 where
591 sizes [] = []
592 sizes (a : as) = checkSize a pargs 0 : sizes as
594 -- find which argument in pargs <a> is smaller than, if any
595 checkSize a (p : ps) i
596 | a == p = Just (i, Same)
597 | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
598 as == txt "assert_smaller" && arg == p
599 = Just (i, Smaller)
600 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
601 | otherwise = checkSize a ps (i + 1)
602 checkSize a [] i = Nothing
604 -- the smaller thing we find must be the same type as <a>, and
605 -- not be coinductive - so carry the type of the constructor we've
606 -- gone under.
608 smaller (Just tyn) a (t, Just tyt)
609 | a == t = isInductive (fst (unApply (getRetTy tyn)))
610 (fst (unApply (getRetTy tyt)))
611 smaller ty a (ap@(App _ f s), _)
612 | (P (DCon _ _ _) n _, args) <- unApply ap
613 = let tyn = getType n in
614 any (smaller (ty `mplus` Just tyn) a)
615 (zip args (map toJust (getArgTys tyn)))
616 -- check higher order recursive arguments
617 smaller ty (App _ f s) a = smaller ty f a
618 smaller _ _ _ = False
620 toJust (n, t) = Just t
622 getType n = case lookupTy n (tt_ctxt ist) of
623 [ty] -> delazy ty -- must exist
625 isInductive (P _ nty _) (P _ nty' _) =
626 let co = case lookupCtxt nty (idris_datatypes ist) of
627 [TI _ x _ _ _] -> x
628 _ -> False in
629 nty == nty' && not co
630 isInductive _ _ = False
632 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
633 dePat t = t
635 patvars (Bind x (PVar _) sc) = x : patvars sc
636 patvars _ = []
638checkSizeChange :: Name -> Idris Totality
639checkSizeChange n = do
640 ist <- getIState
641 case lookupCtxt n (idris_callgraph ist) of
642 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
643 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
644 "from " ++ show (scg cg) ++ "\n" ++
645 show (length ms) ++ "\n" ++
646 showSep "\n" (map show ms))
647 logLvl 6 (show cg)
648 -- every multipath must have an infinitely descending
649 -- thread, then the function terminates
650 -- also need to checks functions called are all total
651 -- (Unchecked is okay as we'll spot problems here)
652 let tot = map (checkMP ist (getArity ist n)) ms
653 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"
654 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
655 return (noPartial tot)
656 [] -> do logLvl 5 $ "No paths for " ++ show n
657 return Unchecked
658 where getArity ist n
659 = case lookupTy n (tt_ctxt ist) of
660 [ty] -> arity (normalise (tt_ctxt ist) [] ty)
661 _ -> error "Can't happen: checkSizeChange.getArity"
663type MultiPath = [SCGEntry]
665mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
666mkMultiPaths ist path [] = [reverse path]
667mkMultiPaths ist path cg
668 = concat (map extend cg)
669 where extend (nextf, args)
670 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
671 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
672 = case lookupCtxt nextf (idris_callgraph ist) of
673 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
674 _ -> [ reverse ((nextf, args) : path) ]
675 | otherwise = [ reverse ((nextf, args) : path) ]
677-- do (nextf, args) <- cg
678-- if ((nextf, args) `elem` path)
679-- then return (reverse ((nextf, args) : path))
680-- else case lookupCtxt nextf (idris_callgraph ist) of
681-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
682-- _ -> return (reverse ((nextf, args) : path))
684-- If any route along the multipath leads to infinite descent, we're fine.
685-- Try a route beginning with every argument.
686-- If we reach a point we've been to before, but with a smaller value,
687-- that means there is an infinitely descending path from that argument.
689checkMP :: IState -> Int -> MultiPath -> Totality
690checkMP ist i mp = if i > 0
691 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
692-- trace ("Paths " ++ show paths) $
693 collapse paths
694 else tryPath 0 [] mp 0
695 where
696 tryPath' d path mp arg
697 = let res = tryPath d path mp arg in
698 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
700 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
701 tryPath desc path [] _ = Total []
702-- tryPath desc path ((UN "believe_me", _) : _) arg
703-- = Partial BelieveMe
704 -- if we get to a constructor, it's fine as long as it's strictly positive
705 tryPath desc path ((f, _) : es) arg
706 | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
707 = case lookupTotal f (tt_ctxt ist) of
708 [Total _] -> Unchecked -- okay so far
709 [Partial _] -> Partial (Other [f])
710 x -> error $ "CAN'T HAPPEN: " ++ show x ++ " for " ++ show f
711 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
712 = Total []
713 tryPath desc path (e@(f, args) : es) arg
714 | e `elem` es && allNothing args = Partial (Mutual [f])
715 tryPath desc path (e@(f, nextargs) : es) arg
716 | Just d <- lookup (e, arg) path
717 = if desc > 0
718 then -- trace ("Descent " ++ show (desc - d) ++ " "
719 -- ++ show (path, e)) $
720 Total []
721 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
722 | e `elem` map (fst . fst) path
723 && not (f `elem` map fst es)
724 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
725 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
726 let argspos = case collapseNothing (zip nextargs [0..]) of
727 [] -> [(Nothing, 0)]
728 x -> x
729-- trace (show (argspos, nextargs, path)) $
730 pathres =
731 do (a, pos) <- argspos
732 case a of
733 Nothing -> -- don't know, but if the
734 -- rest definitely terminates without
735 -- any cycles with route so far,
736 -- then we might yet be total
737 case collapse (map (tryPath 0 (((e, arg), 0):path) es)
738 [0..length nextargs - 1]) of
739 Total _ -> return Unchecked
740 x -> return x
741 Just (nextarg, sc) ->
742 if nextarg == arg then
743 case sc of
744 Same -> return $ tryPath desc (((e, arg), desc) : path)
745 es pos
746 Smaller -> return $ tryPath (desc+1)
747 (((e, arg), desc) : path)
748 es
749 pos
750 _ -> trace ("Shouldn't happen " ++ show e) $
751 return (Partial Itself)
752 else return Unchecked in
753-- trace (show (desc, argspos, path, es, pathres)) $
754 collapse' Unchecked pathres
756 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
757 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
758 | otherwise = Unchecked
760allNothing :: [Maybe a] -> Bool
761allNothing xs = null (collapseNothing (zip xs [0..]))
763collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
764collapseNothing ((Nothing, _) : xs)
765 = filter (\ (x, _) -> case x of
766 Nothing -> False
767 _ -> True) xs
768collapseNothing (x : xs) = x : collapseNothing xs
769collapseNothing [] = []
771noPartial :: [Totality] -> Totality
772noPartial (Partial p : xs) = Partial p
773noPartial (_ : xs) = noPartial xs
774noPartial [] = Total []
776collapse :: [Totality] -> Totality
777collapse xs = collapse' Unchecked xs
778collapse' def (Total r : xs) = Total r
779collapse' def (Unchecked : xs) = collapse' def xs
780collapse' def (d : xs) = collapse' d xs
781-- collapse' Unchecked [] = Total []
782collapse' def [] = def