git.iko.soy/Idris-dev
on dfbb3db help sign in
Idris-dev/src/Idris/Coverage.hs
629 lines 26 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
20-- Generate the LHSes which are missing from a case tree
21-- Eliminate the ones which cannot be well typed
23genMissing :: Name -> [Name] -> SC -> Idris [PTerm]
24genMissing fn args sc
25 = do sc' <- expandTree sc
26 logLvl 5 $ "Checking missing cases for " ++
27 show fn ++ "\n" ++ (show sc')
28 (got, missing) <- gm fn (map (\x -> P Bound x Erased) args) sc'
29 return $ filter (\x -> not (x `elem` got)) missing
31-- Make a term to feed to the pattern matcher from a LHS declared impossible
32-- (we can't type check it, but we need the case analysis to check for
33-- covering...)
35mkPatTm :: PTerm -> Idris Term
36mkPatTm t = do i <- getIState
37 let timp = addImpl' True [] [] i t
38 evalStateT (toTT timp) 0
39 where
40 toTT (PRef _ n) = do i <- lift getIState
41 case lookupDef n (tt_ctxt i) of
42 [TyDecl nt _] -> return $ P nt n Erased
43 _ -> return $ P Ref n Erased
44 toTT (PApp _ t args) = do t' <- toTT t
45 args' <- mapM (toTT . getTm) args
46 return $ mkApp t' args'
47 toTT _ = do v <- get
48 put (v + 1)
49 return (P Bound (MN v "imp") Erased)
51mkPTerm :: Name -> [TT Name] -> Idris PTerm
52mkPTerm f args = do i <- getIState
53 let fapp = mkApp (P Bound f Erased) (map eraseName args)
54 return $ delab i fapp
55 where eraseName (App f a) = App (eraseName f) (eraseName a)
56 eraseName (P _ (MN _ _) _) = Erased
57 eraseName t = t
59gm :: Name -> [TT Name] -> SC -> Idris ([PTerm], [PTerm])
60gm fn args (Case n alts) = do m <- mapM (gmAlt fn args n) alts
61 let (got, missing) = unzip m
62 return (concat got, concat missing)
63gm fn args (STerm tm) = do logLvl 3 ("Covered: " ++ show args)
64 t <- mkPTerm fn args
65 return ([t], [])
66gm fn args ImpossibleCase = do logLvl 3 ("Impossible: " ++ show args)
67 t <- mkPTerm fn args
68 return ([], [])
69gm fn args (UnmatchedCase _) = do logLvl 3 ("Missing: " ++ show args)
70 t <- mkPTerm fn args
71 return ([], [t])
73gmAlt fn args n (ConCase cn t cargs sc)
74 = do let args' = map (subst n (mkApp (P Bound cn Erased)
75 (map (\x -> P Bound x Erased) cargs)))
76 args
77 gm fn args' sc
78gmAlt fn args n (ConstCase c sc)
79 = do let args' = map (subst n (Constant c)) args
80 gm fn args' sc
81gmAlt fn args n (DefaultCase sc)
82 = do gm fn args sc
84getDefault (DefaultCase sc : _) = sc
85getDefault (_ : cs) = getDefault cs
86getDefault [] = UnmatchedCase ""
88dropDefault (DefaultCase sc : rest) = dropDefault rest
89dropDefault (c : cs) = c : dropDefault cs
90dropDefault [] = []
92expandTree :: SC -> Idris SC
93expandTree (Case n alts) = do i <- getIState
94 as <- expandAlts i (dropDefault alts)
95 (getDefault alts)
96 alts' <- mapM expandTreeA as
97 return (Case n alts')
98 where expandTreeA (ConCase n i ns sc) = do sc' <- expandTree sc
99 return (ConCase n i ns sc')
100 expandTreeA (ConstCase i sc) = do sc' <- expandTree sc
101 return (ConstCase i sc')
102 expandTreeA (DefaultCase sc) = do sc' <- expandTree sc
103 return (DefaultCase sc')
104expandTree t = return t
106expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]
107expandAlts i all@(ConstCase c _ : alts) def
108 = return $ all ++ [DefaultCase def]
109expandAlts i all@(ConCase n _ _ _ : alts) def
110 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
111 = do let tyn = getTy n (tt_ctxt i)
112 case lookupCtxt tyn (idris_datatypes i) of
113 (TI ns _ _: _) -> do let ps = map mkPat ns
114 return $ addAlts ps (altsFor all) all
115 _ -> return all
116 where
117 altsFor [] = []
118 altsFor (ConCase n _ _ _ : alts) = n : altsFor alts
119 altsFor (_ : alts) = altsFor alts
121 addAlts [] got alts = alts
122 addAlts ((n, arity) : ps) got alts
123 | n `elem` got = addAlts ps got alts
124 | otherwise = addAlts ps got (alts ++
125 [ConCase n (-1) (argList arity) def])
127 argList i = take i (map (\x -> (MN x "ign")) [0..])
129 getTy n ctxt
130 = case lookupTy n ctxt of
131 (t : _) -> case unApply (getRetTy t) of
132 (P _ tyn _, _) -> tyn
133 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
134 _ -> error "Can't happen getTy 2"
136 mkPat x = case lookupCtxt x (idris_implicits i) of
137 (pargs : _)
138 -> (x, length pargs)
139 _ -> error "Can't happen - genAll"
140expandAlts i alts def = return alts
144-- OLD STUFF: probably broken...
146-- Given a list of LHSs, generate a extra clauses which cover the remaining
147-- cases. The ones which haven't been provided are marked 'absurd' so that the
148-- checker will make sure they can't happen.
150-- This will only work after the given clauses have been typechecked and the
151-- names are fully explicit!
153genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm]
154genClauses fc n xs given
155 = do i <- getIState
156 let lhss = map (getLHS i) xs
157 let argss = transpose lhss
158 let all_args = map (genAll i) argss
159 logLvl 7 $ "COVERAGE of " ++ show n
160 logLvl 10 $ show argss ++ "\n" ++ show all_args
161 logLvl 10 $ "Original: \n" ++
162 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
163 let parg = case lookupCtxt n (idris_implicits i) of
164 (p : _) -> p
165 _ -> repeat (pexp Placeholder)
166 let tryclauses = mkClauses parg all_args
167 logLvl 2 $ show (length tryclauses) ++ " initially to check"
168 let new = mnub i $ filter (noMatch i) tryclauses
169 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
170 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
171-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
172 return new
173-- return (map (\t -> PClause n t [] PImpossible []) new)
174 where getLHS i term
175 | (f, args) <- unApply term = map (\t -> delab' i t True) args
176 | otherwise = []
178 lhsApp (PClause _ _ l _ _ _) = l
179 lhsApp (PWith _ _ l _ _ _) = l
181 mnub i [] = []
182 mnub i (x : xs) =
183 if (any (\t -> case matchClause i x t of
184 Right _ -> True
185 Left _ -> False) xs) then mnub i xs
186 else x : mnub i xs
188 noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of
189 Right _ -> False
190 Left miss -> True) xs
193 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
194 mkClauses parg args
195 | all (== [Placeholder]) args = []
196 mkClauses parg args
197 = do args' <- mkArg args
198 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
199 return tm
200 where
201 mkArg :: [[PTerm]] -> [[PTerm]]
202 mkArg [] = return []
203 mkArg (a : as) = do a' <- a
204 as' <- mkArg as
205 return (a':as')
207fnub xs = fnub' [] xs where
208 fnub' acc (x : xs) | x `elem` acc = fnub' acc xs
209 | otherwise = fnub' (x : acc) xs
210 fnub' acc [] = acc
212-- FIXME: Just look for which one is the deepest, then generate all
213-- possibilities up to that depth.
215genAll :: IState -> [PTerm] -> [PTerm]
216genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
217 [] -> [Placeholder]
218 xs -> nub xs
219 where
220 conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
221 conForm (PRef fc n) = isConName n (tt_ctxt i)
222 conForm _ = False
224 otherPats :: PTerm -> [PTerm]
225 otherPats o@(PRef fc n) = ops fc n [] o
226 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
227 otherPats arg = return Placeholder
229 ops fc n xs o
230 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
231 = do xs' <- mapM otherPats (map getTm xs)
232 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
233 let tyn = getTy n (tt_ctxt i)
234 case lookupCtxt tyn (idris_datatypes i) of
235 (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
236 _ -> [p]
237 ops fc n arg o = return Placeholder
239 getTy n ctxt = case lookupTy n ctxt of
240 (t : _) -> case unApply (getRetTy t) of
241 (P _ tyn _, _) -> tyn
242 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
243 _ -> error "Can't happen getTy 2"
245 mkPat fc x = case lookupCtxt x (idris_implicits i) of
246 (pargs : _)
247 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
248 _ -> error "Can't happen - genAll"
250upd p' p = p { getTm = p' }
252-- Check if, in a given type n, the constructor cn : ty is strictly positive,
253-- and update the context accordingly
255checkPositive :: Name -> (Name, Type) -> Idris ()
256checkPositive n (cn, ty)
257 = do let p = cp ty
258 i <- getIState
259 let tot = if p then Total (args ty) else Partial NotPositive
260 let ctxt' = setTotal cn tot (tt_ctxt i)
261 putIState (i { tt_ctxt = ctxt' })
262 logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot
263 addIBC (IBCTotal cn tot)
264 where
265 args t = [0..length (getArgTys t)-1]
267 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
268 cp t = True
270 posArg (Bind _ (Pi nty) sc)
271 | (P _ n' _, args) <- unApply nty
272 = n /= n' && posArg sc
273 posArg t = True
275-- Totality checking - check for structural recursion
276-- (no mutual definitions yet)
278data LexOrder = LexXX | LexEQ | LexLT
279 deriving (Show, Eq, Ord)
281calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
282calcProd i fc n pats = do patsprod <- mapM prodRec pats
283 if (and patsprod)
284 then return Productive
285 else return (Partial NotProductive)
286 where
287 -- every application of n must be in an argument of a coinductive
288 -- constructor
290 prodRec :: ([Name], Term, Term) -> Idris Bool
291 prodRec (_, _, tm) = prod False tm
293 prod ok ap@(App _ _)
294 | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod ok arg
295 | (P _ f ty, args) <- unApply ap
296 = let co = cotype ty in
297 if f == n
298 then do argsprod <- mapM (prod co) args
299 return (and (ok : argsprod) )
300 else do argsprod <- mapM (prod co) args
301 return (and argsprod)
302 prod ok (App f a) = liftM2 (&&) (prod False f) (prod False a)
303 prod ok (Bind _ (Let t v) sc) = liftM2 (&&) (prod False v) (prod False v)
304 prod ok (Bind _ b sc) = prod ok sc
305 prod ok t = return True
307 cotype ty
308 | (P _ t _, _) <- unApply (getRetTy ty)
309 = case lookupCtxt t (idris_datatypes i) of
310 [TI _ True _] -> True
311 _ -> False
312 | otherwise = False
314calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
315 -> Idris Totality
316calcTotality path fc n pats
317 = do i <- getIState
318 let opts = case lookupCtxt n (idris_flags i) of
319 [fs] -> fs
320 _ -> []
321 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
322 (failure : _) -> return failure
323 _ -> if (Coinductive `elem` opts)
324 then calcProd i fc n pats
325 else checkSizeChange n
326 where
327 checkLHS i (P _ fn _)
328 = case lookupTotal fn (tt_ctxt i) of
329 [Partial _] -> return (Partial (Other [fn]))
330 _ -> Nothing
331 checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)
332 checkLHS _ _ = Nothing
334checkTotality :: [Name] -> FC -> Name -> Idris Totality
335checkTotality path fc n
336 | n `elem` path = return (Partial (Mutual (n : path)))
337 | otherwise = do
338 t <- getTotality n
339 updateContext (simplifyCasedef n)
340 ctxt <- getContext
341 i <- getIState
342 let opts = case lookupCtxt n (idris_flags i) of
343 [fs] -> fs
344 _ -> []
345 t' <- case t of
346 Unchecked ->
347 case lookupDef n ctxt of
348 [CaseOp _ _ _ _ pats _ _ _ _] ->
349 do t' <- if AssertTotal `elem` opts
350 then return $ Total []
351 else calcTotality path fc n pats
352 setTotality n t'
353 addIBC (IBCTotal n t')
354 -- if it's not total, it can't reduce, to keep
355 -- typechecking decidable
356 case t' of
357-- FIXME: Put this back when we can handle mutually recursive things
358-- p@(Partial _) ->
359-- do setAccessibility n Frozen
360-- addIBC (IBCAccess n Frozen)
361-- logLvl 5 $ "HIDDEN: "
362-- ++ show n ++ show p
363 _ -> return ()
364 return t'
365 _ -> return $ Total []
366 x -> return x
367 case t' of
368 Total _ -> return t'
369 Productive -> return t'
370 e -> do w <- cmdOptType WarnPartial
371 if TotalFn `elem` opts
372 then totalityError t'
373 else do when (w && not (PartialFn `elem` opts)) $
374 warnPartial n t'
375 return t'
376 where
377 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
379 warnPartial n t
380 = do i <- getIState
381 case lookupDef n (tt_ctxt i) of
382 [x] -> do
383 iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t
384-- ++ "\n" ++ show x
385-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
386-- iputStrLn (show cg)
389checkDeclTotality :: (FC, Name) -> Idris Totality
390checkDeclTotality (fc, n)
391 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
392-- buildSCG (fc, n)
393-- logLvl 2 $ "Built SCG"
394 checkTotality [] fc n
396-- Calculate the size change graph for this definition
398-- SCG for a function f consists of a list of:
399-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
401-- where g is a function called
402-- a1 ... an are the arguments of f in positions 1..n of g
403-- sizechange1 ... sizechange2 is how their size has changed wrt the input
404-- to f
405-- Nothing, if the argument is unrelated to the input
407buildSCG :: (FC, Name) -> Idris ()
408buildSCG (_, n) = do
409 ist <- getIState
410 case lookupCtxt n (idris_callgraph ist) of
411 [cg] -> case lookupDef n (tt_ctxt ist) of
412 [CaseOp _ _ _ _ _ args sc _ _] ->
413 do logLvl 3 $ "Building SCG for " ++ show n ++ " from\n"
414 ++ show sc
415 let newscg = buildSCG' ist sc args
416 logLvl 5 $ show newscg
417 addToCG n ( cg { scg = newscg } )
418 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
419 x -> error $ "buildSCG: " ++ show (n, x)
421buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]
422buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
423 nub $ scg sc (zip args args)
424 (zip args (zip args (repeat Same)))
425 where
426 scg :: SC -> [(Name, Name)] -> -- local var, originating top level var
427 [(Name, (Name, SizeChange))] -> -- orig to new, and relationship
428 [SCGEntry]
429 scg (Case x alts) vars szs
430 = let x' = findTL x vars in
431 concatMap (scgAlt x' vars szs) alts
432 where
433 findTL x vars
434 | Just x' <- lookup x vars
435 = if x' `elem` args then x'
436 else findTL x' vars
437 | otherwise = x
439 scg (STerm tm) vars szs = scgTerm tm vars szs
440 scg _ _ _ = []
442 -- how the arguments relate - either Smaller or Unknown
443 argRels :: Name -> [(Name, SizeChange)]
444 argRels n = let ctxt = tt_ctxt ist
445 [ty] = lookupTy n ctxt -- must exist!
446 P _ nty _ = fst (unApply (getRetTy ty))
447 args = map snd (getArgTys ty) in
448 map (getRel nty) (map (fst . unApply . getRetTy) args)
449 where
450 getRel ty (P _ n' _) | n' == ty = (n, Smaller)
451 getRel ty t = (n, Unknown)
453 scgAlt x vars szs (ConCase n _ args sc)
454 -- all args smaller than top variable of x in sc
455 -- (as long as they are in the same type family)
456 | Just tvar <- lookup x vars
457 = let arel = argRels n
458 szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel
459 ++ szs
460 vars' = nub (zip args (repeat tvar) ++ vars) in
461 scg sc vars' szs'
462 | otherwise = scg sc vars szs
463 scgAlt x vars szs (ConstCase _ sc) = scg sc vars szs
464 scgAlt x vars szs (DefaultCase sc) = scg sc vars szs
466 scgTerm f@(App _ _) vars szs
467 | (P _ (UN "lazy") _, [_, arg]) <- unApply f
468 = scgTerm arg vars szs
469 | (P _ fn _, args) <- unApply f
470 = let rest = concatMap (\x -> scgTerm x vars szs) args in
471 case lookup fn vars of
472 Just _ -> rest
473 Nothing -> nub $ (fn, map (mkChange szs) args) : rest
474 scgTerm (App f a) vars szs
475 = scgTerm f vars szs ++ scgTerm a vars szs
476 scgTerm (Bind n (Let t v) e) vars szs
477 = scgTerm v vars szs ++ scgTerm e vars szs
478 scgTerm (Bind n _ e) vars szs
479 = scgTerm e (nub ((n, n) : vars)) szs
480 scgTerm (P _ fn _) vars szs
481 = case lookup fn vars of
482 Just _ -> []
483 Nothing -> [(fn, [])]
484 scgTerm _ _ _ = []
486 mkChange :: [(Name, (Name, SizeChange))] -> Term
487 -> Maybe (Int, SizeChange)
488 mkChange szs tm
489 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm = mkChange szs arg
490 | (P _ n ty, _) <- unApply tm -- get higher order args too
491 = do sc <- lookup n szs
492 case sc of
493 (_, Unknown) -> Nothing
494 (o, sc) -> do i <- getArgPos 0 o args
495 return (i, sc)
496 mkChange _ _ = Nothing
498 getArgPos :: Int -> Name -> [Name] -> Maybe Int
499 getArgPos i n [] = Nothing
500 getArgPos i n (x : xs) | n == x = Just i
501 | otherwise = getArgPos (i + 1) n xs
503checkSizeChange :: Name -> Idris Totality
504checkSizeChange n = do
505 ist <- getIState
506 case lookupCtxt n (idris_callgraph ist) of
507 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
508 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
509 "from " ++ show (scg cg) ++ "\n" ++
510 show (length ms) ++ "\n" ++
511 showSep "\n" (map show ms))
512 logLvl 6 (show cg)
513 -- every multipath must have an infinitely descending
514 -- thread, then the function terminates
515 -- also need to checks functions called are all total
516 -- (Unchecked is okay as we'll spot problems here)
517 let tot = map (checkMP ist (length (argsdef cg))) ms
518 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"
519 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
520 return (noPartial tot)
521 [] -> do logLvl 5 $ "No paths for " ++ show n
522 return Unchecked
524type MultiPath = [SCGEntry]
526mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
527mkMultiPaths ist path [] = [reverse path]
528mkMultiPaths ist path cg
529 = concat (map extend cg)
530 where extend (nextf, args)
531 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
532 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
533 = case lookupCtxt nextf (idris_callgraph ist) of
534 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
535 _ -> [ reverse ((nextf, args) : path) ]
536 | otherwise = [ reverse ((nextf, args) : path) ]
538-- do (nextf, args) <- cg
539-- if ((nextf, args) `elem` path)
540-- then return (reverse ((nextf, args) : path))
541-- else case lookupCtxt nextf (idris_callgraph ist) of
542-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
543-- _ -> return (reverse ((nextf, args) : path))
545-- If any route along the multipath leads to infinite descent, we're fine.
546-- Try a route beginning with every argument.
547-- If we reach a point we've been to before, but with a smaller value,
548-- that means there is an infinitely descending path from that argument.
550checkMP :: IState -> Int -> MultiPath -> Totality
551checkMP ist i mp = if i > 0
552 then collapse (map (tryPath 0 [] mp) [0..i-1])
553 else tryPath 0 [] mp 0
554 where
555 tryPath' d path mp arg
556 = let res = tryPath d path mp arg in
557 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
559 tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality
560 tryPath desc path [] _ = Total []
561-- tryPath desc path ((UN "believe_me", _) : _) arg
562-- = Partial BelieveMe
563 -- if we get to a constructor, it's fine as long as it's strictly positive
564 tryPath desc path ((f, _) :es) arg
565 | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)
566 = case lookupTotal f (tt_ctxt ist) of
567 [Total _] -> Unchecked -- okay so far
568 [Partial _] -> Partial (Other [f])
569 x -> error (show x)
570 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
571 = Total []
572 tryPath desc path (e@(f, args) : es) arg
573 | e `elem` es && allNothing args = Partial (Mutual [f])
574 tryPath desc path (e@(f, nextargs) : es) arg
575 | Just d <- lookup e path
576 = if desc > 0
577 then -- trace ("Descent " ++ show (desc - d) ++ " "
578 -- ++ show (path, e)) $
579 Total []
580 else Partial (Mutual (map (fst . fst) path ++ [f]))
581 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
582 let argspos = collapseNothing (zip nextargs [0..]) in
583 collapse' Unchecked $
584 do (a, pos) <- argspos
585 case a of
586 Nothing -> -- don't know, but if the
587 -- rest definitely terminates without
588 -- any cycles with route so far,
589 -- then we might yet be total
590 case collapse (map (tryPath (-10000) ((e, 0):path) es)
591 [0..length nextargs - 1]) of
592 Total _ -> return Unchecked
593 x -> return x
594 Just (nextarg, sc) ->
595 if nextarg == arg then
596 case sc of
597 Same -> return $ tryPath desc ((e, desc) : path)
598 es pos
599 Smaller -> return $ tryPath (desc+1)
600 ((e, desc):path)
601 es
602 pos
603 _ -> trace ("Shouldn't happen " ++ show e) $
604 return (Partial Itself)
605 else return Unchecked
606 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
607 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
608 | otherwise = Unchecked
610allNothing xs = null (collapseNothing (zip xs [0..]))
612collapseNothing ((Nothing, _) : xs)
613 = filter (\ (x, _) -> case x of
614 Nothing -> False
615 _ -> True) xs
616collapseNothing (x : xs) = x : collapseNothing xs
617collapseNothing [] = []
619noPartial (Partial p : xs) = Partial p
620noPartial (_ : xs) = noPartial xs
621noPartial [] = Total []
623collapse xs = collapse' Unchecked xs
624collapse' def (Total r : xs) = Total r
625collapse' def (Unchecked : xs) = collapse' def xs
626collapse' def (d : xs) = collapse' d xs
627-- collapse' Unchecked [] = Total []
628collapse' def [] = def