git.iko.soy/Idris-dev
on 751a6ee help sign in
Idris-dev/src/Idris/Coverage.hs
675 lines 28 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Coverage where
5import Idris.Core.TT
6import Idris.Core.Evaluate
7import Idris.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.Strict
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 (sMN 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 -> showTm i (delab' i t True 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 : _) ->
60 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)
61 _ -> repeat (pexp Placeholder)
62 let tryclauses = mkClauses parg all_args
63 logLvl 2 $ show (length tryclauses) ++ " initially to check"
64 logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)
65 let new = filter (noMatch i) (nub tryclauses)
66 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
67 logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
68-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
69 return new
70-- return (map (\t -> PClause n t [] PImpossible []) new)
71 where getLHS i term
72 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
73 | otherwise = []
75 lhsApp (PClause _ _ l _ _ _) = l
76 lhsApp (PWith _ _ l _ _ _) = l
78 noMatch i tm = all (\x -> case matchClause i (delab' i x True 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
99fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
100 | otherwise = fnub' (x : acc) xs
101fnub' acc [] = acc
103-- quick check for constructor equality
104quickEq :: PTerm -> PTerm -> Bool
105quickEq (PRef _ n) (PRef _ n') = n == n'
106quickEq (PApp _ t as) (PApp _ t' as')
107 | length as == length as'
108 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
109quickEq Placeholder Placeholder = True
110quickEq x y = False
112qelem x [] = False
113qelem x (y : ys) | x `quickEq` y = True
114 | otherwise = qelem x ys
116-- FIXME: Just look for which one is the deepest, then generate all
117-- possibilities up to that depth.
119genAll :: IState -> [PTerm] -> [PTerm]
120genAll i args
121 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
122 [] -> [Placeholder]
123 xs -> inventConsts xs
124 where
125 -- if they're constants, invent a new one to make sure that
126 -- constants which are not explicitly handled are covered
127 inventConsts cs@(PConstant c : _) = map PConstant (ic' (mapMaybe getConst cs))
128 where getConst (PConstant c) = Just c
129 getConst _ = Nothing
130 inventConsts xs = xs
132 -- try constants until they're not in the list.
133 -- FIXME: It is, of course, possible that someone has enumerated all
134 -- the constants and matched on them (maybe in generated code) and this
135 -- will be really slow. This is sufficiently unlikely that we won't
136 -- worry for now...
138 ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I)
139 ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)
140 ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl)
141 ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8)
142 ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16)
143 ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32)
144 ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
145 ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
146 ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
147 -- TODO: Bit vectors
148 -- The rest are types with only one case
149 ic' xs = xs
151 firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs
152 | otherwise = x : cs
154 lotsOfNums t = map t [0..]
155 lotsOfChars = map Ch ['a'..]
156 lotsOfStrings = map Str (map (("some string " ++).show) [1..])
158 conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
159 conForm (PRef fc n) = isConName n (tt_ctxt i)
160 conForm _ = False
162 nubMap f acc [] = acc
163 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
165 otherPats :: PTerm -> [PTerm]
166 otherPats o@(PRef fc n) = ops fc n [] o
167 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
168 otherPats o@(PPair fc _ l r)
169 = ops fc pairCon
170 ([pimp (sUN "A") Placeholder True,
171 pimp (sUN "B") Placeholder True] ++
172 [pexp l, pexp r]) o
173 otherPats o@(PDPair fc p t _ v)
174 = ops fc (sUN "Ex_intro")
175 ([pimp (sUN "a") Placeholder True,
176 pimp (sUN "P") Placeholder True] ++
177 [pexp t,pexp v]) o
178 otherPats o@(PConstant c) = return o
179 otherPats arg = return Placeholder
181 ops fc n xs o
182 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
183 = do xs' <- mapM otherPats (map getExpTm xs)
184 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))
185 let tyn = getTy n (tt_ctxt i)
186 case lookupCtxt tyn (idris_datatypes i) of
187 (TI ns _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
188 _ -> [p]
189 ops fc n arg o = return Placeholder
191 getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
192 getExpTm t = getTm t
194 -- put it back to its original form
195 resugar (PApp _ (PRef fc (UN ei)) [_,_,t,v])
196 | ei == txt "Ex_intro"
197 = PDPair fc TypeOrTerm (getTm t) Placeholder (getTm v)
198 resugar (PApp _ (PRef fc n) [_,_,l,r])
199 | n == pairCon
200 = PPair fc IsTerm (getTm l) (getTm r)
201 resugar t = t
203 dropForce force (x : xs) i | i `elem` force
204 = upd Placeholder x : dropForce force xs (i + 1)
205 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
206 dropForce _ [] _ = []
209 getTy n ctxt = case lookupTy n ctxt of
210 (t : _) -> case unApply (getRetTy t) of
211 (P _ tyn _, _) -> tyn
212 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
213 _ -> error "Can't happen getTy 2"
215 mkPat fc x = case lookupCtxt x (idris_implicits i) of
216 (pargs : _)
217 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
218 _ -> error "Can't happen - genAll"
220upd p' p = p { getTm = p' }
222-- Check whether function and all descendants cover all cases (partial is
223-- okay, as long as it's due to recursion)
225checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
226checkAllCovering fc done top n | not (n `elem` done)
227 = do i <- get
228 case lookupTotal n (tt_ctxt i) of
229 [tot@(Partial NotCovering)] ->
230 tclift $ tfail (At fc (Msg (show top ++ " is " ++ show tot
231 ++ " due to " ++ show n)))
232 _ -> return ()
233 case lookupCtxt n (idris_callgraph i) of
234 [cg] -> mapM_ (checkAllCovering fc (n : done) top)
235 (map fst (calls cg))
236 _ -> return ()
237checkAllCovering _ _ _ _ = return ()
239-- Check if, in a given type n, the constructor cn : ty is strictly positive,
240-- and update the context accordingly
242checkPositive :: Name -> (Name, Type) -> Idris ()
243checkPositive n (cn, ty')
244 = do let ty = delazy ty'
245 let p = cp ty
246 i <- getIState
247 let tot = if p then Total (args ty) else Partial NotPositive
248 let ctxt' = setTotal cn tot (tt_ctxt i)
249 putIState (i { tt_ctxt = ctxt' })
250 logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot
251 addIBC (IBCTotal cn tot)
252 where
253 args t = [0..length (getArgTys t)-1]
255 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
256 cp t = True
258 posArg (Bind _ (Pi nty) sc)
259 | (P _ n' _, args) <- unApply nty
260 = n /= n' && posArg sc
261 posArg t = True
263calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
264calcProd i fc topn pats
265 = cp topn pats []
266 where
267 -- every application of n must be in an argument of a coinductive
268 -- constructor, in every function reachable from here in the
269 -- call graph.
270 cp n pats done = do patsprod <- mapM (prodRec n done) pats
271 if (and patsprod)
272 then return Productive
273 else return (Partial NotProductive)
275 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
276 prodRec n done _ | n `elem` done = return True
277 prodRec n done (_, _, tm) = prod n done False (delazy' True tm)
279 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
280 prod n done ok ap@(App _ _)
281 | (P nt f _, args) <- unApply ap
282 = do recOK <- checkProdRec (n:done) f
283 let ctxt = tt_ctxt i
284 let [ty] = lookupTy f ctxt -- must exist!
285 let co = cotype nt f ty in
286 if (not recOK) then return False else
287 if f == topn
288 then do argsprod <- mapM (prod n done co) args
289 return (and (ok : argsprod) )
290 else do argsprod <- mapM (prod n done co) args
291 return (and argsprod)
292 prod n done ok (App f a) = liftM2 (&&) (prod n done False f)
293 (prod n done False a)
294 prod n done ok (Bind _ (Let t v) sc)
295 = liftM2 (&&) (prod n done False v) (prod n done False v)
296 prod n done ok (Bind _ b sc) = prod n done ok sc
297 prod n done ok t = return True
299 checkProdRec :: [Name] -> Name -> Idris Bool
300 checkProdRec done f
301 = case lookupCtxt f (idris_patdefs i) of
302 [(def, _)] -> do ok <- mapM (prodRec f done) def
303 return (and ok)
304 _ -> return True -- defined elsewhere, can't call topn
306 cotype (DCon _ _) n ty
307 | (P _ t _, _) <- unApply (getRetTy ty)
308 = case lookupCtxt t (idris_datatypes i) of
309 [TI _ True _ _] -> True
310 _ -> False
311 cotype nt n ty = False
313-- Calculate the totality of a function from its patterns.
314-- Either follow the size change graph (if inductive) or check for
315-- productivity (if coinductive)
317calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
318calcTotality fc n pats
319 = do i <- getIState
320 let opts = case lookupCtxt n (idris_flags i) of
321 [fs] -> fs
322 _ -> []
323 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
324 (failure : _) -> return failure
325 _ -> if (Coinductive `elem` opts)
326 then calcProd i fc n pats
327 else checkSizeChange n
328 where
329 checkLHS i (P _ fn _)
330 = case lookupTotal fn (tt_ctxt i) of
331 [Partial _] -> return (Partial (Other [fn]))
332 _ -> Nothing
333 checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)
334 checkLHS _ _ = Nothing
336checkTotality :: [Name] -> FC -> Name -> Idris Totality
337checkTotality path fc n
338 | n `elem` path = return (Partial (Mutual (n : path)))
339 | otherwise = do
340 t <- getTotality n
341 updateContext (simplifyCasedef n)
342 ctxt <- getContext
343 i <- getIState
344 let opts = case lookupCtxt n (idris_flags i) of
345 [fs] -> fs
346 _ -> []
347 t' <- case t of
348 Unchecked ->
349 case lookupDef n ctxt of
350 [CaseOp _ _ _ _ pats _] ->
351 do t' <- if AssertTotal `elem` opts
352 then return $ Total []
353 else calcTotality fc n pats
354 setTotality n t'
355 addIBC (IBCTotal n t')
356 return t'
357 _ -> return $ Total []
358 x -> return x
359 case t' of
360 Total _ -> return t'
361 Productive -> return t'
362 e -> do w <- cmdOptType WarnPartial
363 if TotalFn `elem` opts
364 then totalityError t'
365 else do when (w && not (PartialFn `elem` opts)) $
366 warnPartial n t'
367 return t'
368 where
369 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
371 warnPartial n t
372 = do i <- getIState
373 case lookupDef n (tt_ctxt i) of
374 [x] -> do
375 iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t
376-- ++ "\n" ++ show x
377-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
378-- iputStrLn (show cg)
381checkDeclTotality :: (FC, Name) -> Idris Totality
382checkDeclTotality (fc, n)
383 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
384-- buildSCG (fc, n)
385-- logLvl 2 $ "Built SCG"
386 i <- getIState
387 t <- checkTotality [] fc n
388 case t of
389 -- if it's not total, it can't reduce, to keep
390 -- typechecking decidable
391 p@(Partial _) -> do setAccessibility n Frozen
392 addIBC (IBCAccess n Frozen)
393 logLvl 5 $ "HIDDEN: "
394 ++ show n ++ show p
395 _ -> return ()
396 return t
399-- Calculate the size change graph for this definition
401-- SCG for a function f consists of a list of:
402-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
404-- where g is a function called
405-- a1 ... an are the arguments of f in positions 1..n of g
406-- sizechange1 ... sizechange2 is how their size has changed wrt the input
407-- to f
408-- Nothing, if the argument is unrelated to the input
410buildSCG :: (FC, Name) -> Idris ()
411buildSCG (_, n) = do
412 ist <- getIState
413 case lookupCtxt n (idris_callgraph ist) of
414 [cg] -> case lookupDef n (tt_ctxt ist) of
415 [CaseOp _ _ _ pats _ cd] ->
416 let (args, sc) = cases_totcheck cd in
417 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
418 ++ show pats ++ "\n" ++ show sc
419 let newscg = buildSCG' ist (rights pats) args
420 logLvl 5 $ show newscg
421 addToCG n ( cg { scg = newscg } )
422 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
423 x -> error $ "buildSCG: " ++ show (n, x)
425delazy = delazy' False -- not lazy codata
426delazy' all t@(App f a)
427 | (P _ (UN l) _, [_, _, arg]) <- unApply t,
428 l == txt "Force" = delazy' all arg
429 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
430 l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg
431 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
432 l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg
433delazy' all (App f a) = App (delazy' all f) (delazy' all a)
434delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
435delazy' all t = t
437data Guardedness = Toplevel | Unguarded | Guarded
439buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
440buildSCG' ist pats args = nub $ concatMap scgPat pats where
441 scgPat (lhs, rhs) = let lhs' = delazy lhs
442 rhs' = delazy rhs
443 (f, pargs) = unApply (dePat lhs') in
444 findCalls Toplevel (dePat rhs') (patvars lhs') pargs
446 findCalls guarded ap@(App f a) pvs pargs
447 -- under a call to "assert_total", don't do any checking, just believe
448 -- that it is total.
449 | (P _ (UN at) _, [_, _]) <- unApply ap,
450 at == txt "assert_total" = []
451 -- under a call to "Delay LazyCodata", don't do any checking of the
452 -- immediate call, as long as the call is guarded.
453 -- Then check its arguments
454 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
455 guarded <- Guarded,
456 del == txt "Delay"
457 = let (capp, args) = unApply arg in
458 concatMap (\x -> findCalls Toplevel x pvs pargs) args
459 | (P _ n _, args) <- unApply ap
460 = let nguarded = case guarded of
461 Unguarded -> Unguarded
462 _ -> if isConName n (tt_ctxt ist)
463 then Guarded
464 else Unguarded in
465 mkChange n args pargs ++
466 concatMap (\x -> findCalls nguarded x pvs pargs) args
467 findCalls guarded (App f a) pvs pargs
468 = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs
469 findCalls guarded (Bind n (Let t v) e) pvs pargs
470 = findCalls Unguarded v pvs pargs ++ findCalls guarded e (n : pvs) pargs
471 findCalls guarded (Bind n _ e) pvs pargs
472 = findCalls guarded e (n : pvs) pargs
473 findCalls guarded (P _ f _ ) pvs pargs
474 | not (f `elem` pvs) = [(f, [])]
475 findCalls _ _ _ _ = []
477 expandToArity n args
478 = case lookupTy n (tt_ctxt ist) of
479 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
480 _ -> args
481 where expand i (Bind n (Pi _) sc) (x : xs) = x : expand (i + 1) sc xs
482 expand i (Bind n (Pi _) sc) [] = Just (i, Same) : expand (i + 1) sc []
483 expand i _ xs = xs
485 mkChange n args pargs = [(n, expandToArity n (sizes args))]
486 where
487 sizes [] = []
488 sizes (a : as) = checkSize a pargs 0 : sizes as
490 -- find which argument in pargs <a> is smaller than, if any
491 checkSize a (p : ps) i
492 | a == p = Just (i, Same)
493 | (P _ (UN as) _, [_,arg,_]) <- unApply a,
494 as == txt "assert_smaller" && arg == p
495 = Just (i, Smaller)
496 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
497 | otherwise = checkSize a ps (i + 1)
498 checkSize a [] i = Nothing
500 -- the smaller thing we find must be the same type as <a>, and
501 -- not be coinductive - so carry the type of the constructor we've
502 -- gone under.
504 smaller (Just tyn) a (t, Just tyt)
505 | a == t = isInductive (fst (unApply (getRetTy tyn)))
506 (fst (unApply (getRetTy tyt)))
507 smaller ty a (ap@(App f s), _)
508 | (P (DCon _ _) n _, args) <- unApply ap
509 = let tyn = getType n in
510 any (smaller (ty `mplus` Just tyn) a)
511 (zip args (map toJust (getArgTys tyn)))
512 -- check higher order recursive arguments
513 smaller ty (App f s) a = smaller ty f a
514 smaller _ _ _ = False
516 toJust (n, t) = Just t
518 getType n = case lookupTy n (tt_ctxt ist) of
519 [ty] -> delazy ty -- must exist
521 isInductive (P _ nty _) (P _ nty' _) =
522 let co = case lookupCtxt nty (idris_datatypes ist) of
523 [TI _ x _ _] -> x
524 _ -> False in
525 nty == nty' && not co
526 isInductive _ _ = False
528 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
529 dePat t = t
531 patvars (Bind x (PVar _) sc) = x : patvars sc
532 patvars _ = []
534checkSizeChange :: Name -> Idris Totality
535checkSizeChange n = do
536 ist <- getIState
537 case lookupCtxt n (idris_callgraph ist) of
538 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
539 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
540 "from " ++ show (scg cg) ++ "\n" ++
541 show (length ms) ++ "\n" ++
542 showSep "\n" (map show ms))
543 logLvl 6 (show cg)
544 -- every multipath must have an infinitely descending
545 -- thread, then the function terminates
546 -- also need to checks functions called are all total
547 -- (Unchecked is okay as we'll spot problems here)
548 let tot = map (checkMP ist (getArity ist n)) ms
549 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"
550 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
551 return (noPartial tot)
552 [] -> do logLvl 5 $ "No paths for " ++ show n
553 return Unchecked
554 where getArity ist n
555 = case lookupTy n (tt_ctxt ist) of
556 [ty] -> arity (normalise (tt_ctxt ist) [] ty)
557 _ -> error "Can't happen: checkSizeChange.getArity"
559type MultiPath = [SCGEntry]
561mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
562mkMultiPaths ist path [] = [reverse path]
563mkMultiPaths ist path cg
564 = concat (map extend cg)
565 where extend (nextf, args)
566 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
567 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
568 = case lookupCtxt nextf (idris_callgraph ist) of
569 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
570 _ -> [ reverse ((nextf, args) : path) ]
571 | otherwise = [ reverse ((nextf, args) : path) ]
573-- do (nextf, args) <- cg
574-- if ((nextf, args) `elem` path)
575-- then return (reverse ((nextf, args) : path))
576-- else case lookupCtxt nextf (idris_callgraph ist) of
577-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
578-- _ -> return (reverse ((nextf, args) : path))
580-- If any route along the multipath leads to infinite descent, we're fine.
581-- Try a route beginning with every argument.
582-- If we reach a point we've been to before, but with a smaller value,
583-- that means there is an infinitely descending path from that argument.
585checkMP :: IState -> Int -> MultiPath -> Totality
586checkMP ist i mp = if i > 0
587 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
588-- trace ("Paths " ++ show paths) $
589 collapse paths
590 else tryPath 0 [] mp 0
591 where
592 tryPath' d path mp arg
593 = let res = tryPath d path mp arg in
594 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
596 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
597 tryPath desc path [] _ = Total []
598-- tryPath desc path ((UN "believe_me", _) : _) arg
599-- = Partial BelieveMe
600 -- if we get to a constructor, it's fine as long as it's strictly positive
601 tryPath desc path ((f, _) : es) arg
602 | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)
603 = case lookupTotal f (tt_ctxt ist) of
604 [Total _] -> Unchecked -- okay so far
605 [Partial _] -> Partial (Other [f])
606 x -> error (show x)
607 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
608 = Total []
609 tryPath desc path (e@(f, args) : es) arg
610 | e `elem` es && allNothing args = Partial (Mutual [f])
611 tryPath desc path (e@(f, nextargs) : es) arg
612 | Just d <- lookup (e, arg) path
613 = if desc > 0
614 then -- trace ("Descent " ++ show (desc - d) ++ " "
615 -- ++ show (path, e)) $
616 Total []
617 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
618 | e `elem` map (fst . fst) path
619 && not (f `elem` map fst es)
620 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
621 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
622 let argspos = case collapseNothing (zip nextargs [0..]) of
623 [] -> [(Nothing, 0)]
624 x -> x
625-- trace (show (argspos, nextargs, path)) $
626 pathres =
627 do (a, pos) <- argspos
628 case a of
629 Nothing -> -- don't know, but if the
630 -- rest definitely terminates without
631 -- any cycles with route so far,
632 -- then we might yet be total
633 case collapse (map (tryPath 0 (((e, arg), 0):path) es)
634 [0..length nextargs - 1]) of
635 Total _ -> return Unchecked
636 x -> return x
637 Just (nextarg, sc) ->
638 if nextarg == arg then
639 case sc of
640 Same -> return $ tryPath desc (((e, arg), desc) : path)
641 es pos
642 Smaller -> return $ tryPath (desc+1)
643 (((e, arg), desc) : path)
644 es
645 pos
646 _ -> trace ("Shouldn't happen " ++ show e) $
647 return (Partial Itself)
648 else return Unchecked in
649-- trace (show (desc, argspos, path, es, pathres)) $
650 collapse' Unchecked pathres
652 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
653 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
654 | otherwise = Unchecked
656allNothing xs = null (collapseNothing (zip xs [0..]))
658collapseNothing ((Nothing, _) : xs)
659 = filter (\ (x, _) -> case x of
660 Nothing -> False
661 _ -> True) xs
662collapseNothing (x : xs) = x : collapseNothing xs
663collapseNothing [] = []
665noPartial (Partial p : xs) = Partial p
666noPartial (_ : xs) = noPartial xs
667noPartial [] = Total []
669collapse xs = collapse' Unchecked xs
670collapse' def (Total r : xs) = Total r
671collapse' def (Unchecked : xs) = collapse' def xs
672collapse' def (d : xs) = collapse' d xs
673-- collapse' Unchecked [] = Total []
674collapse' def [] = def