git.iko.soy/Idris-dev
on da672ec help sign in
Idris-dev/src/Idris/Coverage.hs
786 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 -> flattenArgs $ 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) (map flattenArgs 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 (lhs_tms, 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 _ f args) = map getTm args
93 pUnApply _ = []
95 flattenArgs (PApp fc (PApp _ f as) as')
96 = flattenArgs (PApp fc f (as ++ as'))
97 flattenArgs t = t
99 -- Return whether the given clause matches none of the input clauses
100 -- (xs)
101 noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of
102 Right ms -> False
103 Left miss -> True) xs
106 mergePlaceholders :: PTerm -> PTerm -> PTerm
107 mergePlaceholders x Placeholder = Placeholder
108 mergePlaceholders (PApp fc f args) (PApp fc' f' args')
109 = PApp fc' f' (zipWith mergePArg args args')
110 where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in
111 x { getTm = xtm}
112 mergePlaceholders x _ = x
114 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
115 mkClauses parg args
116 | all (== [Placeholder]) args = []
117 mkClauses parg args
118 = do args' <- mkArg args
119 let tm = PApp fc (PRef fc [] n) (zipWith upd args' parg)
120 return tm
121 where
122 mkArg :: [[PTerm]] -> [[PTerm]]
123 mkArg [] = return []
124 mkArg (a : as) = do a' <- a
125 as' <- mkArg as
126 return (a':as')
128-- | Does this error result rule out a case as valid when coverage checking?
129validCoverageCase :: Context -> Err -> Bool
130validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
131 = let topx' = normalise ctxt [] topx
132 topy' = normalise ctxt [] topy in
133 not (sameFam topx' topy' || not (validCoverageCase ctxt e))
134 where sameFam topx topy
135 = case (unApply topx, unApply topy) of
136 ((P _ x _, _), (P _ y _, _)) -> x == y
137 _ -> False
138validCoverageCase ctxt (CantConvert _ _ _) = False
139validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e
140validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e
141validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e
142validCoverageCase ctxt _ = True
144-- | Check whether an error is recoverable in the sense needed for
145-- coverage checking.
146recoverableCoverage :: Context -> Err -> Bool
147recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)
148 = let topx' = normalise ctxt [] topx
149 topy' = normalise ctxt [] topy in
150 r || checkRec topx' topy'
151 where -- different notion of recoverable than in unification, since we
152 -- have no metavars -- just looking to see if a constructor is failing
153 -- to unify with a function that may be reduced later
154 checkRec (App _ f a) p@(P _ _ _) = checkRec f p
155 checkRec p@(P _ _ _) (App _ f a) = checkRec p f
156 checkRec fa@(App _ _ _) fa'@(App _ _ _)
157 | (f, as) <- unApply fa,
158 (f', as') <- unApply fa'
159 = if (length as /= length as')
160 then checkRec f f'
161 else checkRec f f' && and (zipWith checkRec as as')
162 checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt
163 checkRec _ _ = False
165 ntRec x y | Ref <- x = True
166 | Ref <- y = True
167 | (Bound, Bound) <- (x, y) = True
168 | otherwise = False -- name is different, unrecoverable
169recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e
170recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e
171recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
172recoverableCoverage _ _ = False
174-- FIXME: Just look for which one is the deepest, then generate all
175-- possibilities up to that depth.
176-- This and below issues for this function are tracked as Issue #1741 on the issue tracker.
177-- https://github.com/idris-lang/Idris-dev/issues/1741
178genAll :: IState -> [PTerm] -> [PTerm]
179genAll i args
180 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
181 [] -> [Placeholder]
182 xs -> inventConsts xs
183 where
184 -- if they're constants, invent a new one to make sure that
185 -- constants which are not explicitly handled are covered
186 inventConsts cs@(PConstant fc c : _) = map (PConstant NoFC) (ic' (mapMaybe getConst cs))
187 where getConst (PConstant _ c) = Just c
188 getConst _ = Nothing
189 inventConsts xs = xs
191 -- try constants until they're not in the list.
192 -- FIXME: It is, of course, possible that someone has enumerated all
193 -- the constants and matched on them (maybe in generated code) and this
194 -- will be really slow. This is sufficiently unlikely that we won't
195 -- worry for now...
197 ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I)
198 ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)
199 ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl)
200 ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8)
201 ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16)
202 ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32)
203 ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
204 ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
205 ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
206 -- TODO: Bit vectors
207 -- The rest are types with only one case
208 ic' xs = xs
210 firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs
211 | otherwise = x : cs
213 lotsOfNums t = map t [0..]
214 lotsOfChars = map Ch ['a'..]
215 lotsOfStrings = map Str (map (("some string " ++).show) [1..])
217 nubMap f acc [] = acc
218 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
220 otherPats :: PTerm -> [PTerm]
221 otherPats o@(PRef fc hl n) = ops fc n [] o
222 otherPats o@(PApp _ (PRef fc hl n) xs) = ops fc n xs o
223 otherPats o@(PPair fc hls _ l r)
224 = ops fc pairCon
225 ([pimp (sUN "A") Placeholder True,
226 pimp (sUN "B") Placeholder True] ++
227 [pexp l, pexp r]) o
228 otherPats o@(PDPair fc hls p t _ v)
229 = ops fc sigmaCon
230 ([pimp (sUN "a") Placeholder True,
231 pimp (sUN "P") Placeholder True] ++
232 [pexp t,pexp v]) o
233 otherPats o@(PConstant _ c) = inventConsts [o] -- return o
234 otherPats arg = return Placeholder
236 ops fc n xs o
237 | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)
238 = do xs' <- mapM otherPats (map getExpTm xs)
239 let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))
240 let tyn = getTy n (tt_ctxt i)
241 case lookupCtxt tyn (idris_datatypes i) of
242 (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
243 _ -> [p]
244 ops fc n arg o = return Placeholder
246 getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
247 getExpTm t = getTm t
249 -- put it back to its original form
250 resugar (PApp _ (PRef fc hl n) [_,_,t,v])
251 | n == sigmaCon
252 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)
253 resugar (PApp _ (PRef fc hl n) [_,_,l,r])
254 | n == pairCon
255 = PPair fc [] IsTerm (getTm l) (getTm r)
256 resugar t = t
258 dropForce force (x : xs) i | i `elem` force
259 = upd Placeholder x : dropForce force xs (i + 1)
260 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
261 dropForce _ [] _ = []
264 getTy n ctxt = case lookupTy n ctxt of
265 (t : _) -> case unApply (getRetTy t) of
266 (P _ tyn _, _) -> tyn
267 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
268 _ -> error "Can't happen getTy 2"
270 mkPat fc x = case lookupCtxt x (idris_implicits i) of
271 (pargs : _)
272 -> PApp fc (PRef fc [] x) (map (upd Placeholder) pargs)
273 _ -> error "Can't happen - genAll"
275 fnub :: [PTerm] -> [PTerm]
276 fnub xs = fnub' [] xs
278 fnub' :: [PTerm] -> [PTerm] -> [PTerm]
279 fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
280 | otherwise = fnub' (x : acc) xs
281 fnub' acc [] = acc
283 -- quick check for constructor equality
284 quickEq :: PTerm -> PTerm -> Bool
285 quickEq (PConstant _ n) (PConstant _ n') = n == n'
286 quickEq (PRef _ _ n) (PRef _ _ n') = n == n'
287 quickEq (PApp _ t as) (PApp _ t' as')
288 | length as == length as'
289 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
290 quickEq Placeholder Placeholder = True
291 quickEq x y = False
293 qelem :: PTerm -> [PTerm] -> Bool
294 qelem x [] = False
295 qelem x (y : ys) | x `quickEq` y = True
296 | otherwise = qelem x ys
299upd :: t -> PArg' t -> PArg' t
300upd p' p = p { getTm = p' }
302-- Check whether function and all descendants cover all cases (partial is
303-- okay, as long as it's due to recursion)
305checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
306checkAllCovering fc done top n | not (n `elem` done)
307 = do i <- get
308 case lookupTotal n (tt_ctxt i) of
309 [tot@(Partial NotCovering)] ->
310 do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n
311 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }
312 addIBC (IBCTotCheckErr fc msg)
313 [Partial _] ->
314 case lookupCtxt n (idris_callgraph i) of
315 [cg] -> mapM_ (checkAllCovering fc (n : done) top)
316 (map fst (calls cg))
317 _ -> return ()
318 x -> return () -- stop if total
319checkAllCovering _ _ _ _ = return ()
321-- Check if, in a given group of type declarations mut_ns,
322-- the constructor cn : ty is strictly positive,
323-- and update the context accordingly
325checkPositive :: [Name] -> (Name, Type) -> Idris Totality
326checkPositive mut_ns (cn, ty')
327 = do let ty = delazy' True ty'
328 let p = cp ty
329 i <- getIState
330 let tot = if p then Total (args ty) else Partial NotPositive
331 let ctxt' = setTotal cn tot (tt_ctxt i)
332 putIState (i { tt_ctxt = ctxt' })
333 logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns
334 addIBC (IBCTotal cn tot)
335 return tot
336 where
337 args t = [0..length (getArgTys t)-1]
339 cp (Bind n (Pi _ aty _) sc) = posArg aty && cp sc
340 cp t | (P _ n' _, args) <- unApply t,
341 n' `elem` mut_ns = all noRec args
342 cp _ = True
344 posArg (Bind _ (Pi _ nty _) sc)
345 | (P _ n' _, args) <- unApply nty
346 = n' `notElem` mut_ns && all noRec args && posArg sc
347 posArg t | (P _ n' _, args) <- unApply t,
348 n' `elem` mut_ns = all noRec args
349 posArg _ = True
351 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
354calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
355calcProd i fc topn pats
356 = cp topn pats []
357 where
358 -- every application of n must be in an argument of a coinductive
359 -- constructor, in every function reachable from here in the
360 -- call graph.
361 cp n pats done = do patsprod <- mapM (prodRec n done) pats
362 if (and patsprod)
363 then return Productive
364 else return (Partial NotProductive)
366 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
367 prodRec n done _ | n `elem` done = return True
368 prodRec n done (_, _, tm) = prod n done False (delazy' True tm)
370 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
371 prod n done ok ap@(App _ _ _)
372 | (P nt f _, args) <- unApply ap
373 = do recOK <- checkProdRec (n:done) f
374 let ctxt = tt_ctxt i
375 let [ty] = lookupTy f ctxt -- must exist!
376 let co = cotype nt f ty in
377 if (not recOK) then return False else
378 if f == topn
379 then do argsprod <- mapM (prod n done co) args
380 return (and (ok : argsprod) )
381 else do argsprod <- mapM (prod n done co) args
382 return (and argsprod)
383 prod n done ok (App _ f a) = liftM2 (&&) (prod n done False f)
384 (prod n done False a)
385 prod n done ok (Bind _ (Let t v) sc)
386 = liftM2 (&&) (prod n done False v) (prod n done False v)
387 prod n done ok (Bind _ b sc) = prod n done ok sc
388 prod n done ok t = return True
390 checkProdRec :: [Name] -> Name -> Idris Bool
391 checkProdRec done f
392 = case lookupCtxt f (idris_patdefs i) of
393 [(def, _)] -> do ok <- mapM (prodRec f done) def
394 return (and ok)
395 _ -> return True -- defined elsewhere, can't call topn
397 cotype (DCon _ _ _) n ty
398 | (P _ t _, _) <- unApply (getRetTy ty)
399 = case lookupCtxt t (idris_datatypes i) of
400 [TI _ True _ _ _] -> True
401 _ -> False
402 cotype nt n ty = False
404-- | Calculate the totality of a function from its patterns.
405-- Either follow the size change graph (if inductive) or check for
406-- productivity (if coinductive)
407calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
408calcTotality fc n pats
409 = do i <- getIState
410 let opts = case lookupCtxt n (idris_flags i) of
411 [fs] -> fs
412 _ -> []
413 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
414 (failure : _) -> return failure
415 _ -> checkSizeChange n
416 where
417 checkLHS i (P _ fn _)
418 = case lookupTotal fn (tt_ctxt i) of
419 [Partial _] -> return (Partial (Other [fn]))
420 _ -> Nothing
421 checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
422 checkLHS _ _ = Nothing
424checkTotality :: [Name] -> FC -> Name -> Idris Totality
425checkTotality path fc n
426 | n `elem` path = return (Partial (Mutual (n : path)))
427 | otherwise = do
428 t <- getTotality n
429 i <- getIState
430 ctxt' <- do ctxt <- getContext
431 tclift $ simplifyCasedef n (getErasureInfo i) ctxt
432 setContext ctxt'
433 ctxt <- getContext
434 i <- getIState
435 let opts = case lookupCtxt n (idris_flags i) of
436 [fs] -> fs
437 _ -> []
438 t' <- case t of
439 Unchecked ->
440 case lookupDef n ctxt of
441 [CaseOp _ _ _ _ pats _] ->
442 do t' <- if AssertTotal `elem` opts
443 then return $ Total []
444 else calcTotality fc n pats
445 setTotality n t'
446 addIBC (IBCTotal n t')
447 return t'
448 [TyDecl (DCon _ _ _) ty] ->
449 case unApply (getRetTy ty) of
450 (P _ tyn _, _) -> do
451 let ms = case lookupCtxt tyn (idris_datatypes i) of
452 [TI _ _ _ _ xs@(_:_)] -> xs
453 ts -> [tyn]
454 checkPositive ms (n, ty)
455 _-> return $ Total []
456 _ -> return $ Total []
457 x -> return x
458 case t' of
459 Total _ -> return t'
460 Productive -> return t'
461 e -> do w <- cmdOptType WarnPartial
462 if TotalFn `elem` opts
463 then do totalityError t'; return t'
464 else do when (w && not (PartialFn `elem` opts)) $
465 warnPartial n t'
466 return t'
467 where
468 totalityError t = do i <- getIState
469 let msg = show n ++ " is " ++ show t
470 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}
471 addIBC (IBCTotCheckErr fc msg)
473 warnPartial n t
474 = do i <- getIState
475 case lookupDef n (tt_ctxt i) of
476 [x] -> do
477 iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t
478-- ++ "\n" ++ show x
479-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
480-- iputStrLn (show cg)
483checkDeclTotality :: (FC, Name) -> Idris Totality
484checkDeclTotality (fc, n)
485 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
486-- buildSCG (fc, n)
487-- logLvl 2 $ "Built SCG"
488 i <- getIState
489 let opts = case lookupCtxt n (idris_flags i) of
490 [fs] -> fs
491 _ -> []
492 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
493 t <- checkTotality [] fc n
494 case t of
495 -- if it's not total, it can't reduce, to keep
496 -- typechecking decidable
497 p@(Partial _) -> do setAccessibility n Frozen
498 addIBC (IBCAccess n Frozen)
499 logLvl 5 $ "HIDDEN: "
500 ++ show n ++ show p
501 _ -> return ()
502 return t
505-- | Calculate the size change graph for this definition
506--
507-- SCG for a function f consists of a list of:
508-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
509--
510-- where g is a function called
511-- a1 ... an are the arguments of f in positions 1..n of g
512-- sizechange1 ... sizechange2 is how their size has changed wrt the input
513-- to f
514-- Nothing, if the argument is unrelated to the input
515buildSCG :: (FC, Name) -> Idris ()
516buildSCG (_, n) = do
517 ist <- getIState
518 case lookupCtxt n (idris_callgraph ist) of
519 [cg] -> case lookupDefExact n (tt_ctxt ist) of
520 Just (CaseOp _ _ _ pats _ cd) ->
521 let (args, sc) = cases_totcheck cd in
522 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
523 ++ show pats ++ "\n" ++ show sc
524 let newscg = buildSCG' ist (rights pats) args
525 logLvl 5 $ "SCG is: " ++ show newscg
526 addToCG n ( cg { scg = newscg } )
527 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
528 x -> error $ "buildSCG: " ++ show (n, x)
530delazy = delazy' False -- not lazy codata
531delazy' all t@(App _ f a)
532 | (P _ (UN l) _, [_, _, arg]) <- unApply t,
533 l == txt "Force" = delazy' all arg
534 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
535 l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg
536 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
537 l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg
538delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
539delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
540delazy' all t = t
542data Guardedness = Toplevel | Unguarded | Guarded
543 deriving Show
545buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
546buildSCG' ist pats args = nub $ concatMap scgPat pats where
547 scgPat (lhs, rhs) = let lhs' = delazy lhs
548 rhs' = delazy rhs
549 (f, pargs) = unApply (dePat lhs') in
550 findCalls Toplevel (dePat rhs') (patvars lhs') pargs
552 findCalls guarded ap@(App _ f a) pvs pargs
553 -- under a call to "assert_total", don't do any checking, just believe
554 -- that it is total.
555 | (P _ (UN at) _, [_, _]) <- unApply ap,
556 at == txt "assert_total" = []
557 -- under a call to "Delay LazyCodata", don't do any checking of the
558 -- immediate call, as long as the call is guarded.
559 -- Then check its arguments
560 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
561 Guarded <- guarded,
562 del == txt "Delay"
563 = let (capp, args) = unApply arg in
564 concatMap (\x -> findCalls guarded x pvs pargs) args
565 | (P _ n _, args) <- unApply ap
566 = let nguarded = case guarded of
567 Unguarded -> Unguarded
568 _ -> if isConName n (tt_ctxt ist)
569 then Guarded
570 else Unguarded in
571 mkChange n args pargs ++
572 concatMap (\x -> findCalls nguarded x pvs pargs) args
573 findCalls guarded (App _ f a) pvs pargs
574 = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs
575 findCalls guarded (Bind n (Let t v) e) pvs pargs
576 = findCalls Unguarded t pvs pargs ++
577 findCalls Unguarded v pvs pargs ++ findCalls guarded e (n : pvs) pargs
578 findCalls guarded (Bind n t e) pvs pargs
579 = findCalls Unguarded (binderTy t) pvs pargs ++
580 findCalls guarded e (n : pvs) pargs
581 findCalls guarded (P _ f _ ) pvs pargs
582 | not (f `elem` pvs) = [(f, [])]
583 findCalls _ _ _ _ = []
585 expandToArity n args
586 = case lookupTy n (tt_ctxt ist) of
587 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
588 _ -> args
589 where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
590 expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []
591 expand i _ xs = xs
593 mkChange n args pargs = [(n, expandToArity n (sizes args))]
594 where
595 sizes [] = []
596 sizes (a : as) = checkSize a pargs 0 : sizes as
598 -- find which argument in pargs <a> is smaller than, if any
599 checkSize a (p : ps) i
600 | a == p = Just (i, Same)
601 | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
602 as == txt "assert_smaller" && arg == p
603 = Just (i, Smaller)
604 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
605 | otherwise = checkSize a ps (i + 1)
606 checkSize a [] i = Nothing
608 -- the smaller thing we find must be the same type as <a>, and
609 -- not be coinductive - so carry the type of the constructor we've
610 -- gone under.
612 smaller (Just tyn) a (t, Just tyt)
613 | a == t = isInductive (fst (unApply (getRetTy tyn)))
614 (fst (unApply (getRetTy tyt)))
615 smaller ty a (ap@(App _ f s), _)
616 | (P (DCon _ _ _) n _, args) <- unApply ap
617 = let tyn = getType n in
618 any (smaller (ty `mplus` Just tyn) a)
619 (zip args (map toJust (getArgTys tyn)))
620 -- check higher order recursive arguments
621 smaller ty (App _ f s) a = smaller ty f a
622 smaller _ _ _ = False
624 toJust (n, t) = Just t
626 getType n = case lookupTy n (tt_ctxt ist) of
627 [ty] -> delazy ty -- must exist
629 isInductive (P _ nty _) (P _ nty' _) =
630 let co = case lookupCtxt nty (idris_datatypes ist) of
631 [TI _ x _ _ _] -> x
632 _ -> False in
633 nty == nty' && not co
634 isInductive _ _ = False
636 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
637 dePat t = t
639 patvars (Bind x (PVar _) sc) = x : patvars sc
640 patvars _ = []
642checkSizeChange :: Name -> Idris Totality
643checkSizeChange n = do
644 ist <- getIState
645 case lookupCtxt n (idris_callgraph ist) of
646 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
647 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
648 "from " ++ show (scg cg) ++ "\n" ++
649 show (length ms) ++ "\n" ++
650 showSep "\n" (map show ms))
651 logLvl 6 (show cg)
652 -- every multipath must have an infinitely descending
653 -- thread, then the function terminates
654 -- also need to checks functions called are all total
655 -- (Unchecked is okay as we'll spot problems here)
656 let tot = map (checkMP ist (getArity ist n)) ms
657 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"
658 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
659 return (noPartial tot)
660 [] -> do logLvl 5 $ "No paths for " ++ show n
661 return Unchecked
662 where getArity ist n
663 = case lookupTy n (tt_ctxt ist) of
664 [ty] -> arity (normalise (tt_ctxt ist) [] ty)
665 _ -> error "Can't happen: checkSizeChange.getArity"
667type MultiPath = [SCGEntry]
669mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
670mkMultiPaths ist path [] = [reverse path]
671mkMultiPaths ist path cg
672 = concat (map extend cg)
673 where extend (nextf, args)
674 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
675 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
676 = case lookupCtxt nextf (idris_callgraph ist) of
677 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
678 _ -> [ reverse ((nextf, args) : path) ]
679 | otherwise = [ reverse ((nextf, args) : path) ]
681-- do (nextf, args) <- cg
682-- if ((nextf, args) `elem` path)
683-- then return (reverse ((nextf, args) : path))
684-- else case lookupCtxt nextf (idris_callgraph ist) of
685-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
686-- _ -> return (reverse ((nextf, args) : path))
688-- If any route along the multipath leads to infinite descent, we're fine.
689-- Try a route beginning with every argument.
690-- If we reach a point we've been to before, but with a smaller value,
691-- that means there is an infinitely descending path from that argument.
693checkMP :: IState -> Int -> MultiPath -> Totality
694checkMP ist i mp = if i > 0
695 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
696-- trace ("Paths " ++ show paths) $
697 collapse paths
698 else tryPath 0 [] mp 0
699 where
700 tryPath' d path mp arg
701 = let res = tryPath d path mp arg in
702 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
704 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
705 tryPath desc path [] _ = Total []
706-- tryPath desc path ((UN "believe_me", _) : _) arg
707-- = Partial BelieveMe
708 -- if we get to a constructor, it's fine as long as it's strictly positive
709 tryPath desc path ((f, _) : es) arg
710 | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
711 = case lookupTotal f (tt_ctxt ist) of
712 [Total _] -> Unchecked -- okay so far
713 [Partial _] -> Partial (Other [f])
714 x -> error $ "CAN'T HAPPEN: " ++ show x ++ " for " ++ show f
715 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
716 = Total []
717 tryPath desc path (e@(f, args) : es) arg
718 | e `elem` es && allNothing args = Partial (Mutual [f])
719 tryPath desc path (e@(f, nextargs) : es) arg
720 | Just d <- lookup (e, arg) path
721 = if desc > 0
722 then -- trace ("Descent " ++ show (desc - d) ++ " "
723 -- ++ show (path, e)) $
724 Total []
725 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
726 | e `elem` map (fst . fst) path
727 && not (f `elem` map fst es)
728 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
729 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
730 let argspos = case collapseNothing (zip nextargs [0..]) of
731 [] -> [(Nothing, 0)]
732 x -> x
733-- trace (show (argspos, nextargs, path)) $
734 pathres =
735 do (a, pos) <- argspos
736 case a of
737 Nothing -> -- don't know, but if the
738 -- rest definitely terminates without
739 -- any cycles with route so far,
740 -- then we might yet be total
741 case collapse (map (tryPath 0 (((e, arg), 0):path) es)
742 [0..length nextargs - 1]) of
743 Total _ -> return Unchecked
744 x -> return x
745 Just (nextarg, sc) ->
746 if nextarg == arg then
747 case sc of
748 Same -> return $ tryPath desc (((e, arg), desc) : path)
749 es pos
750 Smaller -> return $ tryPath (desc+1)
751 (((e, arg), desc) : path)
752 es
753 pos
754 _ -> trace ("Shouldn't happen " ++ show e) $
755 return (Partial Itself)
756 else return Unchecked in
757-- trace (show (desc, argspos, path, es, pathres)) $
758 collapse' Unchecked pathres
760 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
761 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
762 | otherwise = Unchecked
764allNothing :: [Maybe a] -> Bool
765allNothing xs = null (collapseNothing (zip xs [0..]))
767collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
768collapseNothing ((Nothing, _) : xs)
769 = filter (\ (x, _) -> case x of
770 Nothing -> False
771 _ -> True) xs
772collapseNothing (x : xs) = x : collapseNothing xs
773collapseNothing [] = []
775noPartial :: [Totality] -> Totality
776noPartial (Partial p : xs) = Partial p
777noPartial (_ : xs) = noPartial xs
778noPartial [] = Total []
780collapse :: [Totality] -> Totality
781collapse xs = collapse' Unchecked xs
782collapse' def (Total r : xs) = Total r
783collapse' def (Unchecked : xs) = collapse' def xs
784collapse' def (d : xs) = collapse' d xs
785-- collapse' Unchecked [] = Total []
786collapse' def [] = def