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