git.iko.soy/Idris-dev
on 4dddfaf help sign in
Idris-dev/src/Idris/Coverage.hs
647 lines 27 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Coverage where
5import Core.TT
6import Core.Evaluate
7import Core.CaseTree
9import Idris.AbsSyntax
10import Idris.Delaborate
11import Idris.Error
13import Data.List
14import Data.Either
15import Data.Maybe
16import Debug.Trace
18import Control.Monad.State
20mkPatTm :: PTerm -> Idris Term
21mkPatTm t = do i <- getIState
22 let timp = addImpl' True [] [] i t
23 evalStateT (toTT timp) 0
24 where
25 toTT (PRef _ n) = do i <- lift getIState
26 case lookupDef n (tt_ctxt i) of
27 [TyDecl nt _] -> return $ P nt n Erased
28 _ -> return $ P Ref n Erased
29 toTT (PApp _ t args) = do t' <- toTT t
30 args' <- mapM (toTT . getTm) args
31 return $ mkApp t' args'
32 toTT _ = do v <- get
33 put (v + 1)
34 return (P Bound (MN v "imp") Erased)
36-- Given a list of LHSs, generate a extra clauses which cover the remaining
37-- cases. The ones which haven't been provided are marked 'absurd' so that the
38-- checker will make sure they can't happen.
40-- This will only work after the given clauses have been typechecked and the
41-- names are fully explicit!
43genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm]
44genClauses fc n xs given
45 = do i <- getIState
46 let lhss = map (getLHS i) xs
47 let argss = transpose lhss
48 let all_args = map (genAll i) argss
49 logLvl 5 $ "COVERAGE of " ++ show n
50 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
51 logLvl 10 $ show argss ++ "\n" ++ show all_args
52 logLvl 10 $ "Original: \n" ++
53 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
54 -- add an infinite supply of explicit arguments to update the possible
55 -- cases for (the return type may be variadic, or function type, sp
56 -- there may be more case splitting that the idris_implicits record
57 -- suggests)
58 let parg = case lookupCtxt n (idris_implicits i) of
59 (p : _) -> p ++ repeat (PExp 0 False Placeholder "")
60 _ -> repeat (pexp Placeholder)
61 let tryclauses = mkClauses parg all_args
62 logLvl 2 $ show (length tryclauses) ++ " initially to check"
63 let new = filter (noMatch i) (mnub i tryclauses)
64 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
65 logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
66-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
67 return new
68-- return (map (\t -> PClause n t [] PImpossible []) new)
69 where getLHS i term
70 | (f, args) <- unApply term = map (\t -> delab' i t True) args
71 | otherwise = []
73 lhsApp (PClause _ _ l _ _ _) = l
74 lhsApp (PWith _ _ l _ _ _) = l
76 mnub i [] = []
77 mnub i (x : xs) =
78 let xs' = filter (\t -> case matchClause i x t of
79 Right _ -> False
80 Left _ -> True) xs in
81 x : mnub i xs'
83-- if (any (\t -> case matchClause i x t of
84-- Right _ -> True
85-- Left _ -> False) xs) then mnub i xs
86-- else x : mnub i xs
88 noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of
89 Right _ -> False
90 Left miss -> True) xs
93 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
94 mkClauses parg args
95 | all (== [Placeholder]) args = []
96 mkClauses parg args
97 = do args' <- mkArg args
98 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
99 return tm
100 where
101 mkArg :: [[PTerm]] -> [[PTerm]]
102 mkArg [] = return []
103 mkArg (a : as) = do a' <- a
104 as' <- mkArg as
105 return (a':as')
107fnub xs = fnub' [] xs
109fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
110 | otherwise = fnub' (x : acc) xs
111fnub' acc [] = acc
113-- quick check for constructor equality
114quickEq :: PTerm -> PTerm -> Bool
115quickEq (PRef _ n) (PRef _ n') = n == n'
116quickEq (PApp _ t as) (PApp _ t' as')
117 | length as == length as'
118 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
119quickEq Placeholder Placeholder = True
120quickEq _ _ = False
122qelem x [] = False
123qelem x (y : ys) | x `quickEq` y = True
124 | otherwise = qelem x ys
126-- FIXME: Just look for which one is the deepest, then generate all
127-- possibilities up to that depth.
129genAll :: IState -> [PTerm] -> [PTerm]
130genAll i args
131 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
132 [] -> [Placeholder]
133 xs -> xs
134 where
135 conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
136 conForm (PRef fc n) = isConName n (tt_ctxt i)
137 conForm _ = False
139 nubMap f acc [] = acc
140 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
142 otherPats :: PTerm -> [PTerm]
143 otherPats o@(PRef fc n) = ops fc n [] o
144 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
145 otherPats arg = return Placeholder
147 ops fc n xs_in o
148 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
149 = do let force = getForceable i n -- no need to generate forceable positions
150 let xs = dropForce force xs_in 0
151 xs' <- mapM otherPats (map getTm xs)
152 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
153 let tyn = getTy n (tt_ctxt i)
154 case lookupCtxt tyn (idris_datatypes i) of
155 (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
156 _ -> [p]
157 ops fc n arg o = return Placeholder
159 getForceable i n = case lookupCtxt n (idris_optimisation i) of
160 [Optimise _ fs _] -> fs
161 _ -> []
163 dropForce force (x : xs) i | i `elem` force
164 = upd Placeholder x : dropForce force xs (i + 1)
165 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
166 dropForce _ [] _ = []
169 getTy n ctxt = case lookupTy n ctxt of
170 (t : _) -> case unApply (getRetTy t) of
171 (P _ tyn _, _) -> tyn
172 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
173 _ -> error "Can't happen getTy 2"
175 mkPat fc x = case lookupCtxt x (idris_implicits i) of
176 (pargs : _)
177 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
178 _ -> error "Can't happen - genAll"
180upd p' p = p { getTm = p' }
182-- Check if, in a given type n, the constructor cn : ty is strictly positive,
183-- and update the context accordingly
185checkPositive :: Name -> (Name, Type) -> Idris ()
186checkPositive n (cn, ty)
187 = do let p = cp ty
188 i <- getIState
189 let tot = if p then Total (args ty) else Partial NotPositive
190 let ctxt' = setTotal cn tot (tt_ctxt i)
191 putIState (i { tt_ctxt = ctxt' })
192 logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot
193 addIBC (IBCTotal cn tot)
194 where
195 args t = [0..length (getArgTys t)-1]
197 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
198 cp t = True
200 posArg (Bind _ (Pi nty) sc)
201 | (P _ n' _, args) <- unApply nty
202 = n /= n' && posArg sc
203 posArg t = True
205calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
206calcProd i fc topn pats
207 = cp topn pats []
208 where
209 -- every application of n must be in an argument of a coinductive
210 -- constructor, in every function reachable from here in the
211 -- call graph.
212 cp n pats done = do patsprod <- mapM (prodRec n done) pats
213 if (and patsprod)
214 then return Productive
215 else return (Partial NotProductive)
217 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
218 prodRec n done _ | n `elem` done = return True
219 prodRec n done (_, _, tm) = prod n done False tm
221 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
222 prod n done ok ap@(App _ _)
223 | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod n done ok arg
224 | (P nt f _, args) <- unApply ap
225 = do recOK <- checkProdRec (n:done) f
226 let ctxt = tt_ctxt i
227 let [ty] = lookupTy f ctxt -- must exist!
228 let co = cotype nt f ty in
229 if (not recOK) then return False else
230 if f == topn
231 then do argsprod <- mapM (prod n done co) args
232 return (and (ok : argsprod) )
233 else do argsprod <- mapM (prod n done co) args
234 return (and argsprod)
235 prod n done ok (App f a) = liftM2 (&&) (prod n done False f)
236 (prod n done False a)
237 prod n done ok (Bind _ (Let t v) sc)
238 = liftM2 (&&) (prod n done False v) (prod n done False v)
239 prod n done ok (Bind _ b sc) = prod n done ok sc
240 prod n done ok t = return True
242 checkProdRec :: [Name] -> Name -> Idris Bool
243 checkProdRec done f
244 = case lookupCtxt f (idris_patdefs i) of
245 [(def, _)] -> do ok <- mapM (prodRec f done) def
246 return (and ok)
247 _ -> return True -- defined elsewhere, can't call topn
249 cotype (DCon _ _) n ty
250 | (P _ t _, _) <- unApply (getRetTy ty)
251 = case lookupCtxt t (idris_datatypes i) of
252 [TI _ True _] -> True
253 _ -> False
254 cotype nt n ty = False
256calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
257 -> Idris Totality
258calcTotality path fc n pats
259 = do i <- getIState
260 let opts = case lookupCtxt n (idris_flags i) of
261 [fs] -> fs
262 _ -> []
263 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
264 (failure : _) -> return failure
265 _ -> if (Coinductive `elem` opts)
266 then calcProd i fc n pats
267 else checkSizeChange n
268 where
269 checkLHS i (P _ fn _)
270 = case lookupTotal fn (tt_ctxt i) of
271 [Partial _] -> return (Partial (Other [fn]))
272 _ -> Nothing
273 checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)
274 checkLHS _ _ = Nothing
276checkTotality :: [Name] -> FC -> Name -> Idris Totality
277checkTotality path fc n
278 | n `elem` path = return (Partial (Mutual (n : path)))
279 | otherwise = do
280 t <- getTotality n
281 updateContext (simplifyCasedef n)
282 ctxt <- getContext
283 i <- getIState
284 let opts = case lookupCtxt n (idris_flags i) of
285 [fs] -> fs
286 _ -> []
287 t' <- case t of
288 Unchecked ->
289 case lookupDef n ctxt of
290 [CaseOp _ _ _ _ pats _ _ _ _] ->
291 do t' <- if AssertTotal `elem` opts
292 then return $ Total []
293 else calcTotality path fc n pats
294 setTotality n t'
295 addIBC (IBCTotal n t')
296 -- if it's not total, it can't reduce, to keep
297 -- typechecking decidable
298 case t' of
299-- FIXME: Put this back when we can handle mutually recursive things
300-- p@(Partial _) ->
301-- do setAccessibility n Frozen
302-- addIBC (IBCAccess n Frozen)
303-- logLvl 5 $ "HIDDEN: "
304-- ++ show n ++ show p
305 _ -> return ()
306 return t'
307 _ -> return $ Total []
308 x -> return x
309 case t' of
310 Total _ -> return t'
311 Productive -> return t'
312 e -> do w <- cmdOptType WarnPartial
313 if TotalFn `elem` opts
314 then totalityError t'
315 else do when (w && not (PartialFn `elem` opts)) $
316 warnPartial n t'
317 return t'
318 where
319 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
321 warnPartial n t
322 = do i <- getIState
323 case lookupDef n (tt_ctxt i) of
324 [x] -> do
325 iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t
326-- ++ "\n" ++ show x
327-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
328-- iputStrLn (show cg)
331checkDeclTotality :: (FC, Name) -> Idris Totality
332checkDeclTotality (fc, n)
333 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
334-- buildSCG (fc, n)
335-- logLvl 2 $ "Built SCG"
336 checkTotality [] fc n
338-- Calculate the size change graph for this definition
340-- SCG for a function f consists of a list of:
341-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
343-- where g is a function called
344-- a1 ... an are the arguments of f in positions 1..n of g
345-- sizechange1 ... sizechange2 is how their size has changed wrt the input
346-- to f
347-- Nothing, if the argument is unrelated to the input
349buildSCG :: (FC, Name) -> Idris ()
350buildSCG (_, n) = do
351 ist <- getIState
352 case lookupCtxt n (idris_callgraph ist) of
353 [cg] -> case lookupDef n (tt_ctxt ist) of
354 [CaseOp _ _ _ pats _ args sc _ _] ->
355 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
356 ++ show pats ++ "\n" ++ show sc
357 let newscg = buildSCG' ist (rights pats) args
358 logLvl 5 $ show newscg
359 addToCG n ( cg { scg = newscg } )
360 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
361 x -> error $ "buildSCG: " ++ show (n, x)
363buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
364buildSCG' ist pats args = nub $ concatMap scgPat pats where
365 scgPat (lhs, rhs) = let (f, pargs) = unApply (dePat lhs) in
366 findCalls (dePat rhs) (patvars lhs) pargs
368 findCalls ap@(App f a) pvs pargs
369 | (P _ (UN "lazy") _, [_, arg]) <- unApply ap
370 = findCalls arg pvs pargs
371 | (P _ n _, args) <- unApply ap
372 = mkChange n args pargs ++
373 concatMap (\x -> findCalls x pvs pargs) args
374 findCalls (App f a) pvs pargs
375 = findCalls f pvs pargs ++ findCalls a pvs pargs
376 findCalls (Bind n (Let t v) e) pvs pargs
377 = findCalls v pvs pargs ++ findCalls e (n : pvs) pargs
378 findCalls (Bind n _ e) pvs pargs
379 = findCalls e (n : pvs) pargs
380 findCalls (P _ f _ ) pvs pargs
381 | not (f `elem` pvs) = [(f, [])]
382 findCalls _ _ _ = []
384 mkChange n args pargs = [(n, sizes args)]
385 where
386 sizes [] = []
387 sizes (a : as) = checkSize a pargs 0 : sizes as
389 -- find which argument in pargs <a> is smaller than, if any
390 checkSize a (p : ps) i
391 | a == p = Just (i, Same)
392 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
393 | otherwise = checkSize a ps (i + 1)
394 checkSize a [] i = Nothing
396 -- the smaller thing we find must be the same type as <a>, and
397 -- not be coinductive - so carry the type of the constructor we've
398 -- gone under.
400 smaller (Just tyn) a (t, Just tyt)
401 | a == t = isInductive (fst (unApply (getRetTy tyn)))
402 (fst (unApply (getRetTy tyt)))
403 smaller ty a (ap@(App f s), _)
404 | (P (DCon _ _) n _, args) <- unApply ap
405 = let tyn = getType n in
406 any (smaller (ty `mplus` Just tyn) a)
407 (zip args (map toJust (getArgTys tyn)))
408 -- check higher order recursive arguments
409 smaller ty (App f s) a = smaller ty f a
410 smaller _ _ _ = False
412 toJust (n, t) = Just t
414 getType n = case lookupTy n (tt_ctxt ist) of
415 [ty] -> ty -- must exist
417 isInductive (P _ nty _) (P _ nty' _) =
418 let co = case lookupCtxt nty (idris_datatypes ist) of
419 [TI _ x _] -> x
420 _ -> False in
421 nty == nty' && not co
422 isInductive _ _ = False
424-- getTypeFam t | (P _ n _, _) <- unApply t
426 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
427 dePat t = t
429 patvars (Bind x (PVar _) sc) = x : patvars sc
430 patvars _ = []
432{-
433buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]
434buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
435 nub $ scg sc (zip args args)
436 (zip args (zip args (repeat Same)))
437 where
438 scg :: SC -> [(Name, Name)] -> -- local var, originating top level var
439 [(Name, (Name, SizeChange))] -> -- orig to new, and relationship
440 [SCGEntry]
441 scg (Case x alts) vars szs
442 = let x' = findTL x vars in
443 concatMap (scgAlt x' vars szs) alts
444 where
445 findTL x vars
446 | Just x' <- lookup x vars
447 = if x' `elem` args then x'
448 else findTL x' vars
449 | otherwise = x
451 scg (STerm tm) vars szs = scgTerm tm vars szs
452 scg _ _ _ = []
454 -- how the arguments relate - either Smaller or Unknown
455 argRels :: Name -> [(Name, SizeChange)]
456 argRels n = let ctxt = tt_ctxt ist
457 [ty] = lookupTy n ctxt -- must exist!
458 P _ nty _ = fst (unApply (getRetTy ty))
459 co = case lookupCtxt nty (idris_datatypes ist) of
460 [TI _ x _] -> x
461 _ -> False
462 args = map snd (getArgTys ty) in
463 map (getRel co nty) (map (fst . unApply . getRetTy) args)
464 where
465 getRel True _ _ = (n, Unknown) -- coinductive
466 getRel _ ty (P _ n' _) | n' == ty = (n, Smaller)
467 getRel _ ty t = (n, Unknown)
469 scgAlt x vars szs (ConCase n _ args sc)
470 -- all args smaller than top variable of x in sc
471 -- (as long as they are in the same type family, and it's
472 -- not coinductive)
473 | Just tvar <- lookup x vars
474 = let arel = argRels n
475 szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel
476 ++ szs
477 vars' = nub (zip args (repeat tvar) ++ vars) in
478 scg sc vars' szs'
479 | otherwise = scg sc vars szs
480 scgAlt x vars szs (ConstCase _ sc) = scg sc vars szs
481 scgAlt x vars szs (DefaultCase sc) = scg sc vars szs
483 scgTerm f@(App _ _) vars szs
484 | (P _ (UN "lazy") _, [_, arg]) <- unApply f
485 = scgTerm arg vars szs
486 | (P _ fn _, args) <- unApply f
487 = let rest = concatMap (\x -> scgTerm x vars szs) args in
488 case lookup fn vars of
489 Just _ -> rest
490 Nothing -> nub $ (fn, map (mkChange szs) args) : rest
491 scgTerm (App f a) vars szs
492 = scgTerm f vars szs ++ scgTerm a vars szs
493 scgTerm (Bind n (Let t v) e) vars szs
494 = scgTerm v vars szs ++ scgTerm e vars szs
495 scgTerm (Bind n _ e) vars szs
496 = scgTerm e (nub ((n, n) : vars)) szs
497 scgTerm (P _ fn _) vars szs
498 = case lookup fn vars of
499 Just _ -> []
500 Nothing -> [(fn, [])]
501 scgTerm _ _ _ = []
503 mkChange :: [(Name, (Name, SizeChange))] -> Term
504 -> Maybe (Int, SizeChange)
505 mkChange szs tm
506 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm = mkChange szs arg
507 | (P _ n ty, _) <- unApply tm -- get higher order args too
508 = do sc <- lookup n szs
509 case sc of
510 (_, Unknown) -> Nothing
511 (o, sc) -> do i <- getArgPos 0 o args
512 return (i, sc)
513 mkChange _ _ = Nothing
515 getArgPos :: Int -> Name -> [Name] -> Maybe Int
516 getArgPos i n [] = Nothing
517 getArgPos i n (x : xs) | n == x = Just i
518 | otherwise = getArgPos (i + 1) n xs
519-}
521checkSizeChange :: Name -> Idris Totality
522checkSizeChange n = do
523 ist <- getIState
524 case lookupCtxt n (idris_callgraph ist) of
525 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
526 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
527 "from " ++ show (scg cg) ++ "\n" ++
528 show (length ms) ++ "\n" ++
529 showSep "\n" (map show ms))
530 logLvl 6 (show cg)
531 -- every multipath must have an infinitely descending
532 -- thread, then the function terminates
533 -- also need to checks functions called are all total
534 -- (Unchecked is okay as we'll spot problems here)
535 let tot = map (checkMP ist (length (argsdef cg))) ms
536 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"
537 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
538 return (noPartial tot)
539 [] -> do logLvl 5 $ "No paths for " ++ show n
540 return Unchecked
542type MultiPath = [SCGEntry]
544mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
545mkMultiPaths ist path [] = [reverse path]
546mkMultiPaths ist path cg
547 = concat (map extend cg)
548 where extend (nextf, args)
549 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
550 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
551 = case lookupCtxt nextf (idris_callgraph ist) of
552 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
553 _ -> [ reverse ((nextf, args) : path) ]
554 | otherwise = [ reverse ((nextf, args) : path) ]
556-- do (nextf, args) <- cg
557-- if ((nextf, args) `elem` path)
558-- then return (reverse ((nextf, args) : path))
559-- else case lookupCtxt nextf (idris_callgraph ist) of
560-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
561-- _ -> return (reverse ((nextf, args) : path))
563-- If any route along the multipath leads to infinite descent, we're fine.
564-- Try a route beginning with every argument.
565-- If we reach a point we've been to before, but with a smaller value,
566-- that means there is an infinitely descending path from that argument.
568checkMP :: IState -> Int -> MultiPath -> Totality
569checkMP ist i mp = if i > 0
570 then collapse (map (tryPath 0 [] mp) [0..i-1])
571 else tryPath 0 [] mp 0
572 where
573 tryPath' d path mp arg
574 = let res = tryPath d path mp arg in
575 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
577 tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality
578 tryPath desc path [] _ = Total []
579-- tryPath desc path ((UN "believe_me", _) : _) arg
580-- = Partial BelieveMe
581 -- if we get to a constructor, it's fine as long as it's strictly positive
582 tryPath desc path ((f, _) :es) arg
583 | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)
584 = case lookupTotal f (tt_ctxt ist) of
585 [Total _] -> Unchecked -- okay so far
586 [Partial _] -> Partial (Other [f])
587 x -> error (show x)
588 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
589 = Total []
590 tryPath desc path (e@(f, args) : es) arg
591 | e `elem` es && allNothing args = Partial (Mutual [f])
592 tryPath desc path (e@(f, nextargs) : es) arg
593 | Just d <- lookup e path
594 = if desc > 0
595 then -- trace ("Descent " ++ show (desc - d) ++ " "
596 -- ++ show (path, e)) $
597 Total []
598 else Partial (Mutual (map (fst . fst) path ++ [f]))
599 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
600 let argspos = collapseNothing (zip nextargs [0..]) in
601 collapse' Unchecked $
602 do (a, pos) <- argspos
603 case a of
604 Nothing -> -- don't know, but if the
605 -- rest definitely terminates without
606 -- any cycles with route so far,
607 -- then we might yet be total
608 case collapse (map (tryPath (-10000) ((e, 0):path) es)
609 [0..length nextargs - 1]) of
610 Total _ -> return Unchecked
611 x -> return x
612 Just (nextarg, sc) ->
613 if nextarg == arg then
614 case sc of
615 Same -> return $ tryPath desc ((e, desc) : path)
616 es pos
617 Smaller -> return $ tryPath (desc+1)
618 ((e, desc):path)
619 es
620 pos
621 _ -> trace ("Shouldn't happen " ++ show e) $
622 return (Partial Itself)
623 else return Unchecked
624 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
625 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
626 | otherwise = Unchecked
628allNothing xs = null (collapseNothing (zip xs [0..]))
630collapseNothing ((Nothing, _) : xs)
631 = filter (\ (x, _) -> case x of
632 Nothing -> False
633 _ -> True) xs
634collapseNothing (x : xs) = x : collapseNothing xs
635collapseNothing [] = []
637noPartial (Partial p : xs) = Partial p
638noPartial (_ : xs) = noPartial xs
639noPartial [] = Total []
641collapse xs = collapse' Unchecked xs
642collapse' def (Total r : xs) = Total r
643collapse' def (Unchecked : xs) = collapse' def xs
644collapse' def (d : xs) = collapse' d xs
645-- collapse' Unchecked [] = Total []
646collapse' def [] = def