git.iko.soy/Idris-dev
on 5242001 help sign in
Idris-dev/src/Idris/Coverage.hs
607 lines 25 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 7 $ "COVERAGE of " ++ show n
50 logLvl 10 $ show argss ++ "\n" ++ show all_args
51 logLvl 10 $ "Original: \n" ++
52 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
53 let parg = case lookupCtxt n (idris_implicits i) of
54 (p : _) -> p
55 _ -> repeat (pexp Placeholder)
56 let tryclauses = mkClauses parg all_args
57 logLvl 2 $ show (length tryclauses) ++ " initially to check"
58 let new = mnub i $ filter (noMatch i) tryclauses
59 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
60 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
61-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
62 return new
63-- return (map (\t -> PClause n t [] PImpossible []) new)
64 where getLHS i term
65 | (f, args) <- unApply term = map (\t -> delab' i t True) args
66 | otherwise = []
68 lhsApp (PClause _ _ l _ _ _) = l
69 lhsApp (PWith _ _ l _ _ _) = l
71 mnub i [] = []
72 mnub i (x : xs) =
73 if (any (\t -> case matchClause i x t of
74 Right _ -> True
75 Left _ -> False) xs) then mnub i xs
76 else x : mnub i xs
78 noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of
79 Right _ -> False
80 Left miss -> True) xs
83 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
84 mkClauses parg args
85 | all (== [Placeholder]) args = []
86 mkClauses parg args
87 = do args' <- mkArg args
88 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
89 return tm
90 where
91 mkArg :: [[PTerm]] -> [[PTerm]]
92 mkArg [] = return []
93 mkArg (a : as) = do a' <- a
94 as' <- mkArg as
95 return (a':as')
97fnub xs = fnub' [] xs where
98 fnub' acc (x : xs) | x `elem` acc = fnub' acc xs
99 | otherwise = fnub' (x : acc) xs
100 fnub' acc [] = acc
102-- FIXME: Just look for which one is the deepest, then generate all
103-- possibilities up to that depth.
105genAll :: IState -> [PTerm] -> [PTerm]
106genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
107 [] -> [Placeholder]
108 xs -> nub xs
109 where
110 conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
111 conForm (PRef fc n) = isConName n (tt_ctxt i)
112 conForm _ = False
114 otherPats :: PTerm -> [PTerm]
115 otherPats o@(PRef fc n) = ops fc n [] o
116 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
117 otherPats arg = return Placeholder
119 ops fc n xs o
120 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
121 = do xs' <- mapM otherPats (map getTm xs)
122 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
123 let tyn = getTy n (tt_ctxt i)
124 case lookupCtxt tyn (idris_datatypes i) of
125 (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
126 _ -> [p]
127 ops fc n arg o = return Placeholder
129 getTy n ctxt = case lookupTy n ctxt of
130 (t : _) -> case unApply (getRetTy t) of
131 (P _ tyn _, _) -> tyn
132 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
133 _ -> error "Can't happen getTy 2"
135 mkPat fc x = case lookupCtxt x (idris_implicits i) of
136 (pargs : _)
137 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
138 _ -> error "Can't happen - genAll"
140upd p' p = p { getTm = p' }
142-- Check if, in a given type n, the constructor cn : ty is strictly positive,
143-- and update the context accordingly
145checkPositive :: Name -> (Name, Type) -> Idris ()
146checkPositive n (cn, ty)
147 = do let p = cp ty
148 i <- getIState
149 let tot = if p then Total (args ty) else Partial NotPositive
150 let ctxt' = setTotal cn tot (tt_ctxt i)
151 putIState (i { tt_ctxt = ctxt' })
152 logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot
153 addIBC (IBCTotal cn tot)
154 where
155 args t = [0..length (getArgTys t)-1]
157 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
158 cp t = True
160 posArg (Bind _ (Pi nty) sc)
161 | (P _ n' _, args) <- unApply nty
162 = n /= n' && posArg sc
163 posArg t = True
165calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
166calcProd i fc topn pats
167 = cp topn pats []
168 where
169 -- every application of n must be in an argument of a coinductive
170 -- constructor, in every function reachable from here in the
171 -- call graph.
172 cp n pats done = do patsprod <- mapM (prodRec n done) pats
173 if (and patsprod)
174 then return Productive
175 else return (Partial NotProductive)
177 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
178 prodRec n done _ | n `elem` done = return True
179 prodRec n done (_, _, tm) = prod n done False tm
181 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
182 prod n done ok ap@(App _ _)
183 | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod n done ok arg
184 | (P nt f _, args) <- unApply ap
185 = do recOK <- checkProdRec (n:done) f
186 let ctxt = tt_ctxt i
187 let [ty] = lookupTy f ctxt -- must exist!
188 let co = cotype nt f ty in
189 if (not recOK) then return False else
190 if f == topn
191 then do argsprod <- mapM (prod n done co) args
192 return (and (ok : argsprod) )
193 else do argsprod <- mapM (prod n done co) args
194 return (and argsprod)
195 prod n done ok (App f a) = liftM2 (&&) (prod n done False f)
196 (prod n done False a)
197 prod n done ok (Bind _ (Let t v) sc)
198 = liftM2 (&&) (prod n done False v) (prod n done False v)
199 prod n done ok (Bind _ b sc) = prod n done ok sc
200 prod n done ok t = return True
202 checkProdRec :: [Name] -> Name -> Idris Bool
203 checkProdRec done f
204 = case lookupCtxt f (idris_patdefs i) of
205 [(def, _)] -> do ok <- mapM (prodRec f done) def
206 return (and ok)
207 _ -> return True -- defined elsewhere, can't call topn
209 cotype (DCon _ _) n ty
210 | (P _ t _, _) <- unApply (getRetTy ty)
211 = case lookupCtxt t (idris_datatypes i) of
212 [TI _ True _] -> True
213 _ -> False
214 cotype nt n ty = False
216calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
217 -> Idris Totality
218calcTotality path fc n pats
219 = do i <- getIState
220 let opts = case lookupCtxt n (idris_flags i) of
221 [fs] -> fs
222 _ -> []
223 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
224 (failure : _) -> return failure
225 _ -> if (Coinductive `elem` opts)
226 then calcProd i fc n pats
227 else checkSizeChange n
228 where
229 checkLHS i (P _ fn _)
230 = case lookupTotal fn (tt_ctxt i) of
231 [Partial _] -> return (Partial (Other [fn]))
232 _ -> Nothing
233 checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)
234 checkLHS _ _ = Nothing
236checkTotality :: [Name] -> FC -> Name -> Idris Totality
237checkTotality path fc n
238 | n `elem` path = return (Partial (Mutual (n : path)))
239 | otherwise = do
240 t <- getTotality n
241 updateContext (simplifyCasedef n)
242 ctxt <- getContext
243 i <- getIState
244 let opts = case lookupCtxt n (idris_flags i) of
245 [fs] -> fs
246 _ -> []
247 t' <- case t of
248 Unchecked ->
249 case lookupDef n ctxt of
250 [CaseOp _ _ _ _ pats _ _ _ _] ->
251 do t' <- if AssertTotal `elem` opts
252 then return $ Total []
253 else calcTotality path fc n pats
254 setTotality n t'
255 addIBC (IBCTotal n t')
256 -- if it's not total, it can't reduce, to keep
257 -- typechecking decidable
258 case t' of
259-- FIXME: Put this back when we can handle mutually recursive things
260-- p@(Partial _) ->
261-- do setAccessibility n Frozen
262-- addIBC (IBCAccess n Frozen)
263-- logLvl 5 $ "HIDDEN: "
264-- ++ show n ++ show p
265 _ -> return ()
266 return t'
267 _ -> return $ Total []
268 x -> return x
269 case t' of
270 Total _ -> return t'
271 Productive -> return t'
272 e -> do w <- cmdOptType WarnPartial
273 if TotalFn `elem` opts
274 then totalityError t'
275 else do when (w && not (PartialFn `elem` opts)) $
276 warnPartial n t'
277 return t'
278 where
279 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
281 warnPartial n t
282 = do i <- getIState
283 case lookupDef n (tt_ctxt i) of
284 [x] -> do
285 iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t
286-- ++ "\n" ++ show x
287-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
288-- iputStrLn (show cg)
291checkDeclTotality :: (FC, Name) -> Idris Totality
292checkDeclTotality (fc, n)
293 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
294-- buildSCG (fc, n)
295-- logLvl 2 $ "Built SCG"
296 checkTotality [] fc n
298-- Calculate the size change graph for this definition
300-- SCG for a function f consists of a list of:
301-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
303-- where g is a function called
304-- a1 ... an are the arguments of f in positions 1..n of g
305-- sizechange1 ... sizechange2 is how their size has changed wrt the input
306-- to f
307-- Nothing, if the argument is unrelated to the input
309buildSCG :: (FC, Name) -> Idris ()
310buildSCG (_, n) = do
311 ist <- getIState
312 case lookupCtxt n (idris_callgraph ist) of
313 [cg] -> case lookupDef n (tt_ctxt ist) of
314 [CaseOp _ _ _ pats _ args sc _ _] ->
315 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
316 ++ show pats ++ "\n" ++ show sc
317 let newscg = buildSCG' ist (rights pats) args
318 logLvl 5 $ show newscg
319 addToCG n ( cg { scg = newscg } )
320 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
321 x -> error $ "buildSCG: " ++ show (n, x)
323buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
324buildSCG' ist pats args = nub $ concatMap scgPat pats where
325 scgPat (lhs, rhs) = let (f, pargs) = unApply (dePat lhs) in
326 findCalls (dePat rhs) (patvars lhs) pargs
328 findCalls ap@(App f a) pvs pargs
329 | (P _ (UN "lazy") _, [_, arg]) <- unApply ap
330 = findCalls arg pvs pargs
331 | (P _ n _, args) <- unApply ap
332 = mkChange n args pargs ++
333 concatMap (\x -> findCalls x pvs pargs) args
334 findCalls (App f a) pvs pargs
335 = findCalls f pvs pargs ++ findCalls a pvs pargs
336 findCalls (Bind n (Let t v) e) pvs pargs
337 = findCalls v pvs pargs ++ findCalls e (n : pvs) pargs
338 findCalls (Bind n _ e) pvs pargs
339 = findCalls e (n : pvs) pargs
340 findCalls (P _ f _ ) pvs pargs
341 | not (f `elem` pvs) = [(f, [])]
342 findCalls _ _ _ = []
344 mkChange n args pargs = [(n, sizes args)]
345 where
346 sizes [] = []
347 sizes (a : as) = checkSize a pargs 0 : sizes as
349 -- find which argument in pargs <a> is smaller than, if any
350 checkSize a (p : ps) i
351 | a == p = Just (i, Same)
352 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
353 | otherwise = checkSize a ps (i + 1)
354 checkSize a [] i = Nothing
356 -- the smaller thing we find must be the same type as <a>, and
357 -- not be coinductive - so carry the type of the constructor we've
358 -- gone under.
360 smaller (Just tyn) a (t, Just tyt)
361 | a == t = isInductive (fst (unApply (getRetTy tyn)))
362 (fst (unApply (getRetTy tyt)))
363 smaller ty a (ap@(App f s), _)
364 | (P (DCon _ _) n _, args) <- unApply ap
365 = let tyn = getType n in
366 any (smaller (ty `mplus` Just tyn) a)
367 (zip args (map toJust (getArgTys tyn)))
368 -- check higher order recursive arguments
369 smaller ty (App f s) a = smaller ty f a
370 smaller _ _ _ = False
372 toJust (n, t) = Just t
374 getType n = case lookupTy n (tt_ctxt ist) of
375 [ty] -> ty -- must exist
377 isInductive (P _ nty _) (P _ nty' _) =
378 let co = case lookupCtxt nty (idris_datatypes ist) of
379 [TI _ x _] -> x
380 _ -> False in
381 nty == nty' && not co
382 isInductive _ _ = False
384-- getTypeFam t | (P _ n _, _) <- unApply t
386 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
387 dePat t = t
389 patvars (Bind x (PVar _) sc) = x : patvars sc
390 patvars _ = []
392{-
393buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]
394buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
395 nub $ scg sc (zip args args)
396 (zip args (zip args (repeat Same)))
397 where
398 scg :: SC -> [(Name, Name)] -> -- local var, originating top level var
399 [(Name, (Name, SizeChange))] -> -- orig to new, and relationship
400 [SCGEntry]
401 scg (Case x alts) vars szs
402 = let x' = findTL x vars in
403 concatMap (scgAlt x' vars szs) alts
404 where
405 findTL x vars
406 | Just x' <- lookup x vars
407 = if x' `elem` args then x'
408 else findTL x' vars
409 | otherwise = x
411 scg (STerm tm) vars szs = scgTerm tm vars szs
412 scg _ _ _ = []
414 -- how the arguments relate - either Smaller or Unknown
415 argRels :: Name -> [(Name, SizeChange)]
416 argRels n = let ctxt = tt_ctxt ist
417 [ty] = lookupTy n ctxt -- must exist!
418 P _ nty _ = fst (unApply (getRetTy ty))
419 co = case lookupCtxt nty (idris_datatypes ist) of
420 [TI _ x _] -> x
421 _ -> False
422 args = map snd (getArgTys ty) in
423 map (getRel co nty) (map (fst . unApply . getRetTy) args)
424 where
425 getRel True _ _ = (n, Unknown) -- coinductive
426 getRel _ ty (P _ n' _) | n' == ty = (n, Smaller)
427 getRel _ ty t = (n, Unknown)
429 scgAlt x vars szs (ConCase n _ args sc)
430 -- all args smaller than top variable of x in sc
431 -- (as long as they are in the same type family, and it's
432 -- not coinductive)
433 | Just tvar <- lookup x vars
434 = let arel = argRels n
435 szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel
436 ++ szs
437 vars' = nub (zip args (repeat tvar) ++ vars) in
438 scg sc vars' szs'
439 | otherwise = scg sc vars szs
440 scgAlt x vars szs (ConstCase _ sc) = scg sc vars szs
441 scgAlt x vars szs (DefaultCase sc) = scg sc vars szs
443 scgTerm f@(App _ _) vars szs
444 | (P _ (UN "lazy") _, [_, arg]) <- unApply f
445 = scgTerm arg vars szs
446 | (P _ fn _, args) <- unApply f
447 = let rest = concatMap (\x -> scgTerm x vars szs) args in
448 case lookup fn vars of
449 Just _ -> rest
450 Nothing -> nub $ (fn, map (mkChange szs) args) : rest
451 scgTerm (App f a) vars szs
452 = scgTerm f vars szs ++ scgTerm a vars szs
453 scgTerm (Bind n (Let t v) e) vars szs
454 = scgTerm v vars szs ++ scgTerm e vars szs
455 scgTerm (Bind n _ e) vars szs
456 = scgTerm e (nub ((n, n) : vars)) szs
457 scgTerm (P _ fn _) vars szs
458 = case lookup fn vars of
459 Just _ -> []
460 Nothing -> [(fn, [])]
461 scgTerm _ _ _ = []
463 mkChange :: [(Name, (Name, SizeChange))] -> Term
464 -> Maybe (Int, SizeChange)
465 mkChange szs tm
466 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm = mkChange szs arg
467 | (P _ n ty, _) <- unApply tm -- get higher order args too
468 = do sc <- lookup n szs
469 case sc of
470 (_, Unknown) -> Nothing
471 (o, sc) -> do i <- getArgPos 0 o args
472 return (i, sc)
473 mkChange _ _ = Nothing
475 getArgPos :: Int -> Name -> [Name] -> Maybe Int
476 getArgPos i n [] = Nothing
477 getArgPos i n (x : xs) | n == x = Just i
478 | otherwise = getArgPos (i + 1) n xs
479-}
481checkSizeChange :: Name -> Idris Totality
482checkSizeChange n = do
483 ist <- getIState
484 case lookupCtxt n (idris_callgraph ist) of
485 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
486 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
487 "from " ++ show (scg cg) ++ "\n" ++
488 show (length ms) ++ "\n" ++
489 showSep "\n" (map show ms))
490 logLvl 6 (show cg)
491 -- every multipath must have an infinitely descending
492 -- thread, then the function terminates
493 -- also need to checks functions called are all total
494 -- (Unchecked is okay as we'll spot problems here)
495 let tot = map (checkMP ist (length (argsdef cg))) ms
496 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"
497 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
498 return (noPartial tot)
499 [] -> do logLvl 5 $ "No paths for " ++ show n
500 return Unchecked
502type MultiPath = [SCGEntry]
504mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
505mkMultiPaths ist path [] = [reverse path]
506mkMultiPaths ist path cg
507 = concat (map extend cg)
508 where extend (nextf, args)
509 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
510 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
511 = case lookupCtxt nextf (idris_callgraph ist) of
512 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
513 _ -> [ reverse ((nextf, args) : path) ]
514 | otherwise = [ reverse ((nextf, args) : path) ]
516-- do (nextf, args) <- cg
517-- if ((nextf, args) `elem` path)
518-- then return (reverse ((nextf, args) : path))
519-- else case lookupCtxt nextf (idris_callgraph ist) of
520-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
521-- _ -> return (reverse ((nextf, args) : path))
523-- If any route along the multipath leads to infinite descent, we're fine.
524-- Try a route beginning with every argument.
525-- If we reach a point we've been to before, but with a smaller value,
526-- that means there is an infinitely descending path from that argument.
528checkMP :: IState -> Int -> MultiPath -> Totality
529checkMP ist i mp = if i > 0
530 then collapse (map (tryPath 0 [] mp) [0..i-1])
531 else tryPath 0 [] mp 0
532 where
533 tryPath' d path mp arg
534 = let res = tryPath d path mp arg in
535 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
537 tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality
538 tryPath desc path [] _ = Total []
539-- tryPath desc path ((UN "believe_me", _) : _) arg
540-- = Partial BelieveMe
541 -- if we get to a constructor, it's fine as long as it's strictly positive
542 tryPath desc path ((f, _) :es) arg
543 | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)
544 = case lookupTotal f (tt_ctxt ist) of
545 [Total _] -> Unchecked -- okay so far
546 [Partial _] -> Partial (Other [f])
547 x -> error (show x)
548 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
549 = Total []
550 tryPath desc path (e@(f, args) : es) arg
551 | e `elem` es && allNothing args = Partial (Mutual [f])
552 tryPath desc path (e@(f, nextargs) : es) arg
553 | Just d <- lookup e path
554 = if desc > 0
555 then -- trace ("Descent " ++ show (desc - d) ++ " "
556 -- ++ show (path, e)) $
557 Total []
558 else Partial (Mutual (map (fst . fst) path ++ [f]))
559 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
560 let argspos = collapseNothing (zip nextargs [0..]) in
561 collapse' Unchecked $
562 do (a, pos) <- argspos
563 case a of
564 Nothing -> -- don't know, but if the
565 -- rest definitely terminates without
566 -- any cycles with route so far,
567 -- then we might yet be total
568 case collapse (map (tryPath (-10000) ((e, 0):path) es)
569 [0..length nextargs - 1]) of
570 Total _ -> return Unchecked
571 x -> return x
572 Just (nextarg, sc) ->
573 if nextarg == arg then
574 case sc of
575 Same -> return $ tryPath desc ((e, desc) : path)
576 es pos
577 Smaller -> return $ tryPath (desc+1)
578 ((e, desc):path)
579 es
580 pos
581 _ -> trace ("Shouldn't happen " ++ show e) $
582 return (Partial Itself)
583 else return Unchecked
584 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
585 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
586 | otherwise = Unchecked
588allNothing xs = null (collapseNothing (zip xs [0..]))
590collapseNothing ((Nothing, _) : xs)
591 = filter (\ (x, _) -> case x of
592 Nothing -> False
593 _ -> True) xs
594collapseNothing (x : xs) = x : collapseNothing xs
595collapseNothing [] = []
597noPartial (Partial p : xs) = Partial p
598noPartial (_ : xs) = noPartial xs
599noPartial [] = Total []
601collapse xs = collapse' Unchecked xs
602collapse' def (Total r : xs) = Total r
603collapse' def (Unchecked : xs) = collapse' def xs
604collapse' def (d : xs) = collapse' d xs
605-- collapse' Unchecked [] = Total []
606collapse' def [] = def