git.iko.soy/Idris-dev
on dcdebfc help sign in
Idris-dev/src/Idris/Coverage.hs
702 lines 30 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
12import Idris.Output (iputStrLn)
14import Data.List
15import Data.Either
16import Data.Maybe
17import Debug.Trace
19import Control.Monad.State.Strict
21-- Generate a pattern from an 'impossible' LHS. (Need this to eliminate the
22-- pattern clauses which have been provided explicitly from new clause
23-- generation.)
25mkPatTm :: PTerm -> Idris Term
26mkPatTm t = do i <- getIState
27 let timp = addImpl' True [] [] i t
28 evalStateT (toTT (mapPT deNS timp)) 0
29 where
30 toTT (PRef _ n) = do i <- lift getIState
31 case lookupDef n (tt_ctxt i) of
32 [TyDecl nt _] -> return $ P nt n Erased
33 _ -> return $ P Ref n Erased
34 toTT (PApp _ t args) = do t' <- toTT t
35 args' <- mapM (toTT . getTm) args
36 return $ mkApp t' args'
37 -- For alternatives, pick the first and drop the namespaces. It doesn't
38 -- really matter which is taken since matching will ignore the namespace.
39 toTT (PAlternative _ (a : as)) = toTT a
40 toTT _ = do v <- get
41 put (v + 1)
42 return (P Bound (sMN v "imp") Erased)
44 deNS (PRef f (NS n _)) = PRef f n
45 deNS t = t
47-- Given a list of LHSs, generate a extra clauses which cover the remaining
48-- cases. The ones which haven't been provided are marked 'absurd' so that the
49-- checker will make sure they can't happen.
51-- This will only work after the given clauses have been typechecked and the
52-- names are fully explicit!
54genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
55genClauses fc n xs given
56 = do i <- getIState
57 let lhs_tms = map (\x -> delab' i x True True) xs
58 -- if a placeholder was given, don't bother generating cases for it
59 let lhs_tms' = zipWith mergePlaceholders lhs_tms given
60 let lhss = map pUnApply lhs_tms'
62 let argss = transpose lhss
63 let all_args = map (genAll i) argss
64 logLvl 5 $ "COVERAGE of " ++ show n
65 logLvl 5 $ show lhss
66 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
67 logLvl 10 $ show argss ++ "\n" ++ show all_args
68 logLvl 1 $ "Original: \n" ++
69 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
70 -- add an infinite supply of explicit arguments to update the possible
71 -- cases for (the return type may be variadic, or function type, so
72 -- there may be more case splitting that the idris_implicits record
73 -- suggests)
74 let parg = case lookupCtxt n (idris_implicits i) of
75 (p : _) ->
76 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)
77 _ -> repeat (pexp Placeholder)
78 let tryclauses = mkClauses parg all_args
79 logLvl 2 $ show (length tryclauses) ++ " initially to check"
80 logLvl 1 $ showSep "\n" (map (showTm i) tryclauses)
81 let new = filter (noMatch i) (nub tryclauses)
82 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
83 logLvl 3 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
84-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
85 return new
86-- return (map (\t -> PClause n t [] PImpossible []) new)
87 where getLHS i term
88 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
89 | otherwise = []
91 pUnApply (PApp _ _ args) = map getTm args
92 pUnApply _ = []
94 -- Return whether the given clause matches none of the input clauses
95 -- (xs)
96 noMatch i tm = all (\x -> case matchClause i (delab' i x True True) tm of
97 Right ms -> False
98 Left miss -> True) xs
101 mergePlaceholders :: PTerm -> PTerm -> PTerm
102 mergePlaceholders x Placeholder = Placeholder
103 mergePlaceholders (PApp fc f args) (PApp fc' f' args')
104 = PApp fc' f' (zipWith mergePArg args args')
105 where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in
106 x { getTm = xtm}
107 mergePlaceholders x _ = x
109 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
110 mkClauses parg args
111 | all (== [Placeholder]) args = []
112 mkClauses parg args
113 = do args' <- mkArg args
114 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
115 return tm
116 where
117 mkArg :: [[PTerm]] -> [[PTerm]]
118 mkArg [] = return []
119 mkArg (a : as) = do a' <- a
120 as' <- mkArg as
121 return (a':as')
123fnub xs = fnub' [] xs
125fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
126 | otherwise = fnub' (x : acc) xs
127fnub' acc [] = acc
129-- quick check for constructor equality
130quickEq :: PTerm -> PTerm -> Bool
131quickEq (PConstant n) (PConstant n') = n == n'
132quickEq (PRef _ n) (PRef _ n') = n == n'
133quickEq (PApp _ t as) (PApp _ t' as')
134 | length as == length as'
135 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
136quickEq Placeholder Placeholder = True
137quickEq x y = False
139qelem x [] = False
140qelem x (y : ys) | x `quickEq` y = True
141 | otherwise = qelem x ys
143-- FIXME: Just look for which one is the deepest, then generate all
144-- possibilities up to that depth.
146genAll :: IState -> [PTerm] -> [PTerm]
147genAll i args
148 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
149 [] -> [Placeholder]
150 xs -> inventConsts xs
151 where
152 -- if they're constants, invent a new one to make sure that
153 -- constants which are not explicitly handled are covered
154 inventConsts cs@(PConstant c : _) = map PConstant (ic' (mapMaybe getConst cs))
155 where getConst (PConstant c) = Just c
156 getConst _ = Nothing
157 inventConsts xs = xs
159 -- try constants until they're not in the list.
160 -- FIXME: It is, of course, possible that someone has enumerated all
161 -- the constants and matched on them (maybe in generated code) and this
162 -- will be really slow. This is sufficiently unlikely that we won't
163 -- worry for now...
165 ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I)
166 ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)
167 ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl)
168 ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8)
169 ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16)
170 ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32)
171 ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
172 ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
173 ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
174 -- TODO: Bit vectors
175 -- The rest are types with only one case
176 ic' xs = xs
178 firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs
179 | otherwise = x : cs
181 lotsOfNums t = map t [0..]
182 lotsOfChars = map Ch ['a'..]
183 lotsOfStrings = map Str (map (("some string " ++).show) [1..])
185 conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
186 conForm (PRef fc n) = isConName n (tt_ctxt i)
187 conForm _ = False
189 nubMap f acc [] = acc
190 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
192 otherPats :: PTerm -> [PTerm]
193 otherPats o@(PRef fc n) = ops fc n [] o
194 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
195 otherPats o@(PPair fc _ l r)
196 = ops fc pairCon
197 ([pimp (sUN "A") Placeholder True,
198 pimp (sUN "B") Placeholder True] ++
199 [pexp l, pexp r]) o
200 otherPats o@(PDPair fc p t _ v)
201 = ops fc (sUN "Ex_intro")
202 ([pimp (sUN "a") Placeholder True,
203 pimp (sUN "P") Placeholder True] ++
204 [pexp t,pexp v]) o
205 otherPats o@(PConstant c) = return o
206 otherPats arg = return Placeholder
208 ops fc n xs o
209 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
210 = do xs' <- mapM otherPats (map getExpTm xs)
211 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))
212 let tyn = getTy n (tt_ctxt i)
213 case lookupCtxt tyn (idris_datatypes i) of
214 (TI ns _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
215 _ -> [p]
216 ops fc n arg o = return Placeholder
218 getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!
219 getExpTm t = getTm t
221 -- put it back to its original form
222 resugar (PApp _ (PRef fc (UN ei)) [_,_,t,v])
223 | ei == txt "Ex_intro"
224 = PDPair fc TypeOrTerm (getTm t) Placeholder (getTm v)
225 resugar (PApp _ (PRef fc n) [_,_,l,r])
226 | n == pairCon
227 = PPair fc IsTerm (getTm l) (getTm r)
228 resugar t = t
230 dropForce force (x : xs) i | i `elem` force
231 = upd Placeholder x : dropForce force xs (i + 1)
232 dropForce force (x : xs) i = x : dropForce force xs (i + 1)
233 dropForce _ [] _ = []
236 getTy n ctxt = case lookupTy n ctxt of
237 (t : _) -> case unApply (getRetTy t) of
238 (P _ tyn _, _) -> tyn
239 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
240 _ -> error "Can't happen getTy 2"
242 mkPat fc x = case lookupCtxt x (idris_implicits i) of
243 (pargs : _)
244 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
245 _ -> error "Can't happen - genAll"
247upd p' p = p { getTm = p' }
249-- Check whether function and all descendants cover all cases (partial is
250-- okay, as long as it's due to recursion)
252checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
253checkAllCovering fc done top n | not (n `elem` done)
254 = do i <- get
255 case lookupTotal n (tt_ctxt i) of
256 [tot@(Partial NotCovering)] ->
257 tclift $ tfail (At fc (Msg (show top ++ " is " ++ show tot
258 ++ " due to " ++ show n)))
259 _ -> return ()
260 case lookupCtxt n (idris_callgraph i) of
261 [cg] -> mapM_ (checkAllCovering fc (n : done) top)
262 (map fst (calls cg))
263 _ -> return ()
264checkAllCovering _ _ _ _ = return ()
266-- Check if, in a given type n, the constructor cn : ty is strictly positive,
267-- and update the context accordingly
269checkPositive :: Name -> (Name, Type) -> Idris ()
270checkPositive n (cn, ty')
271 = do let ty = delazy ty'
272 let p = cp ty
273 i <- getIState
274 let tot = if p then Total (args ty) else Partial NotPositive
275 let ctxt' = setTotal cn tot (tt_ctxt i)
276 putIState (i { tt_ctxt = ctxt' })
277 logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot
278 addIBC (IBCTotal cn tot)
279 where
280 args t = [0..length (getArgTys t)-1]
282 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
283 cp t = True
285 posArg (Bind _ (Pi nty) sc)
286 | (P _ n' _, args) <- unApply nty
287 = n /= n' && posArg sc
288 posArg t = True
290calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
291calcProd i fc topn pats
292 = cp topn pats []
293 where
294 -- every application of n must be in an argument of a coinductive
295 -- constructor, in every function reachable from here in the
296 -- call graph.
297 cp n pats done = do patsprod <- mapM (prodRec n done) pats
298 if (and patsprod)
299 then return Productive
300 else return (Partial NotProductive)
302 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
303 prodRec n done _ | n `elem` done = return True
304 prodRec n done (_, _, tm) = prod n done False (delazy' True tm)
306 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
307 prod n done ok ap@(App _ _)
308 | (P nt f _, args) <- unApply ap
309 = do recOK <- checkProdRec (n:done) f
310 let ctxt = tt_ctxt i
311 let [ty] = lookupTy f ctxt -- must exist!
312 let co = cotype nt f ty in
313 if (not recOK) then return False else
314 if f == topn
315 then do argsprod <- mapM (prod n done co) args
316 return (and (ok : argsprod) )
317 else do argsprod <- mapM (prod n done co) args
318 return (and argsprod)
319 prod n done ok (App f a) = liftM2 (&&) (prod n done False f)
320 (prod n done False a)
321 prod n done ok (Bind _ (Let t v) sc)
322 = liftM2 (&&) (prod n done False v) (prod n done False v)
323 prod n done ok (Bind _ b sc) = prod n done ok sc
324 prod n done ok t = return True
326 checkProdRec :: [Name] -> Name -> Idris Bool
327 checkProdRec done f
328 = case lookupCtxt f (idris_patdefs i) of
329 [(def, _)] -> do ok <- mapM (prodRec f done) def
330 return (and ok)
331 _ -> return True -- defined elsewhere, can't call topn
333 cotype (DCon _ _) n ty
334 | (P _ t _, _) <- unApply (getRetTy ty)
335 = case lookupCtxt t (idris_datatypes i) of
336 [TI _ True _ _] -> True
337 _ -> False
338 cotype nt n ty = False
340-- Calculate the totality of a function from its patterns.
341-- Either follow the size change graph (if inductive) or check for
342-- productivity (if coinductive)
344calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
345calcTotality fc n pats
346 = do i <- getIState
347 let opts = case lookupCtxt n (idris_flags i) of
348 [fs] -> fs
349 _ -> []
350 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
351 (failure : _) -> return failure
352 _ -> if (Coinductive `elem` opts)
353 then calcProd i fc n pats
354 else checkSizeChange n
355 where
356 checkLHS i (P _ fn _)
357 = case lookupTotal fn (tt_ctxt i) of
358 [Partial _] -> return (Partial (Other [fn]))
359 _ -> Nothing
360 checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)
361 checkLHS _ _ = Nothing
363checkTotality :: [Name] -> FC -> Name -> Idris Totality
364checkTotality path fc n
365 | n `elem` path = return (Partial (Mutual (n : path)))
366 | otherwise = do
367 t <- getTotality n
368 updateContext (simplifyCasedef n)
369 ctxt <- getContext
370 i <- getIState
371 let opts = case lookupCtxt n (idris_flags i) of
372 [fs] -> fs
373 _ -> []
374 t' <- case t of
375 Unchecked ->
376 case lookupDef n ctxt of
377 [CaseOp _ _ _ _ pats _] ->
378 do t' <- if AssertTotal `elem` opts
379 then return $ Total []
380 else calcTotality fc n pats
381 setTotality n t'
382 addIBC (IBCTotal n t')
383 return t'
384 _ -> return $ Total []
385 x -> return x
386 case t' of
387 Total _ -> return t'
388 Productive -> return t'
389 e -> do w <- cmdOptType WarnPartial
390 if TotalFn `elem` opts
391 then totalityError t'
392 else do when (w && not (PartialFn `elem` opts)) $
393 warnPartial n t'
394 return t'
395 where
396 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
398 warnPartial n t
399 = do i <- getIState
400 case lookupDef n (tt_ctxt i) of
401 [x] -> do
402 iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t
403-- ++ "\n" ++ show x
404-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
405-- iputStrLn (show cg)
408checkDeclTotality :: (FC, Name) -> Idris Totality
409checkDeclTotality (fc, n)
410 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
411-- buildSCG (fc, n)
412-- logLvl 2 $ "Built SCG"
413 i <- getIState
414 t <- checkTotality [] fc n
415 case t of
416 -- if it's not total, it can't reduce, to keep
417 -- typechecking decidable
418 p@(Partial _) -> do setAccessibility n Frozen
419 addIBC (IBCAccess n Frozen)
420 logLvl 5 $ "HIDDEN: "
421 ++ show n ++ show p
422 _ -> return ()
423 return t
426-- Calculate the size change graph for this definition
428-- SCG for a function f consists of a list of:
429-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
431-- where g is a function called
432-- a1 ... an are the arguments of f in positions 1..n of g
433-- sizechange1 ... sizechange2 is how their size has changed wrt the input
434-- to f
435-- Nothing, if the argument is unrelated to the input
437buildSCG :: (FC, Name) -> Idris ()
438buildSCG (_, n) = do
439 ist <- getIState
440 case lookupCtxt n (idris_callgraph ist) of
441 [cg] -> case lookupDef n (tt_ctxt ist) of
442 [CaseOp _ _ _ pats _ cd] ->
443 let (args, sc) = cases_totcheck cd in
444 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
445 ++ show pats ++ "\n" ++ show sc
446 let newscg = buildSCG' ist (rights pats) args
447 logLvl 5 $ show newscg
448 addToCG n ( cg { scg = newscg } )
449 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
450 x -> error $ "buildSCG: " ++ show (n, x)
452delazy = delazy' False -- not lazy codata
453delazy' all t@(App f a)
454 | (P _ (UN l) _, [_, _, arg]) <- unApply t,
455 l == txt "Force" = delazy' all arg
456 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
457 l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg
458 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
459 l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg
460delazy' all (App f a) = App (delazy' all f) (delazy' all a)
461delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
462delazy' all t = t
464data Guardedness = Toplevel | Unguarded | Guarded
466buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
467buildSCG' ist pats args = nub $ concatMap scgPat pats where
468 scgPat (lhs, rhs) = let lhs' = delazy lhs
469 rhs' = delazy rhs
470 (f, pargs) = unApply (dePat lhs') in
471 findCalls Toplevel (dePat rhs') (patvars lhs') pargs
473 findCalls guarded ap@(App f a) pvs pargs
474 -- under a call to "assert_total", don't do any checking, just believe
475 -- that it is total.
476 | (P _ (UN at) _, [_, _]) <- unApply ap,
477 at == txt "assert_total" = []
478 -- under a call to "Delay LazyCodata", don't do any checking of the
479 -- immediate call, as long as the call is guarded.
480 -- Then check its arguments
481 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
482 guarded <- Guarded,
483 del == txt "Delay"
484 = let (capp, args) = unApply arg in
485 concatMap (\x -> findCalls Toplevel x pvs pargs) args
486 | (P _ n _, args) <- unApply ap
487 = let nguarded = case guarded of
488 Unguarded -> Unguarded
489 _ -> if isConName n (tt_ctxt ist)
490 then Guarded
491 else Unguarded in
492 mkChange n args pargs ++
493 concatMap (\x -> findCalls nguarded x pvs pargs) args
494 findCalls guarded (App f a) pvs pargs
495 = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs
496 findCalls guarded (Bind n (Let t v) e) pvs pargs
497 = findCalls Unguarded v pvs pargs ++ findCalls guarded e (n : pvs) pargs
498 findCalls guarded (Bind n _ e) pvs pargs
499 = findCalls guarded e (n : pvs) pargs
500 findCalls guarded (P _ f _ ) pvs pargs
501 | not (f `elem` pvs) = [(f, [])]
502 findCalls _ _ _ _ = []
504 expandToArity n args
505 = case lookupTy n (tt_ctxt ist) of
506 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
507 _ -> args
508 where expand i (Bind n (Pi _) sc) (x : xs) = x : expand (i + 1) sc xs
509 expand i (Bind n (Pi _) sc) [] = Just (i, Same) : expand (i + 1) sc []
510 expand i _ xs = xs
512 mkChange n args pargs = [(n, expandToArity n (sizes args))]
513 where
514 sizes [] = []
515 sizes (a : as) = checkSize a pargs 0 : sizes as
517 -- find which argument in pargs <a> is smaller than, if any
518 checkSize a (p : ps) i
519 | a == p = Just (i, Same)
520 | (P _ (UN as) _, [_,arg,_]) <- unApply a,
521 as == txt "assert_smaller" && arg == p
522 = Just (i, Smaller)
523 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
524 | otherwise = checkSize a ps (i + 1)
525 checkSize a [] i = Nothing
527 -- the smaller thing we find must be the same type as <a>, and
528 -- not be coinductive - so carry the type of the constructor we've
529 -- gone under.
531 smaller (Just tyn) a (t, Just tyt)
532 | a == t = isInductive (fst (unApply (getRetTy tyn)))
533 (fst (unApply (getRetTy tyt)))
534 smaller ty a (ap@(App f s), _)
535 | (P (DCon _ _) n _, args) <- unApply ap
536 = let tyn = getType n in
537 any (smaller (ty `mplus` Just tyn) a)
538 (zip args (map toJust (getArgTys tyn)))
539 -- check higher order recursive arguments
540 smaller ty (App f s) a = smaller ty f a
541 smaller _ _ _ = False
543 toJust (n, t) = Just t
545 getType n = case lookupTy n (tt_ctxt ist) of
546 [ty] -> delazy ty -- must exist
548 isInductive (P _ nty _) (P _ nty' _) =
549 let co = case lookupCtxt nty (idris_datatypes ist) of
550 [TI _ x _ _] -> x
551 _ -> False in
552 nty == nty' && not co
553 isInductive _ _ = False
555 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
556 dePat t = t
558 patvars (Bind x (PVar _) sc) = x : patvars sc
559 patvars _ = []
561checkSizeChange :: Name -> Idris Totality
562checkSizeChange n = do
563 ist <- getIState
564 case lookupCtxt n (idris_callgraph ist) of
565 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
566 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
567 "from " ++ show (scg cg) ++ "\n" ++
568 show (length ms) ++ "\n" ++
569 showSep "\n" (map show ms))
570 logLvl 6 (show cg)
571 -- every multipath must have an infinitely descending
572 -- thread, then the function terminates
573 -- also need to checks functions called are all total
574 -- (Unchecked is okay as we'll spot problems here)
575 let tot = map (checkMP ist (getArity ist n)) ms
576 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"
577 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
578 return (noPartial tot)
579 [] -> do logLvl 5 $ "No paths for " ++ show n
580 return Unchecked
581 where getArity ist n
582 = case lookupTy n (tt_ctxt ist) of
583 [ty] -> arity (normalise (tt_ctxt ist) [] ty)
584 _ -> error "Can't happen: checkSizeChange.getArity"
586type MultiPath = [SCGEntry]
588mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
589mkMultiPaths ist path [] = [reverse path]
590mkMultiPaths ist path cg
591 = concat (map extend cg)
592 where extend (nextf, args)
593 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
594 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
595 = case lookupCtxt nextf (idris_callgraph ist) of
596 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
597 _ -> [ reverse ((nextf, args) : path) ]
598 | otherwise = [ reverse ((nextf, args) : path) ]
600-- do (nextf, args) <- cg
601-- if ((nextf, args) `elem` path)
602-- then return (reverse ((nextf, args) : path))
603-- else case lookupCtxt nextf (idris_callgraph ist) of
604-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
605-- _ -> return (reverse ((nextf, args) : path))
607-- If any route along the multipath leads to infinite descent, we're fine.
608-- Try a route beginning with every argument.
609-- If we reach a point we've been to before, but with a smaller value,
610-- that means there is an infinitely descending path from that argument.
612checkMP :: IState -> Int -> MultiPath -> Totality
613checkMP ist i mp = if i > 0
614 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
615-- trace ("Paths " ++ show paths) $
616 collapse paths
617 else tryPath 0 [] mp 0
618 where
619 tryPath' d path mp arg
620 = let res = tryPath d path mp arg in
621 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
623 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
624 tryPath desc path [] _ = Total []
625-- tryPath desc path ((UN "believe_me", _) : _) arg
626-- = Partial BelieveMe
627 -- if we get to a constructor, it's fine as long as it's strictly positive
628 tryPath desc path ((f, _) : es) arg
629 | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)
630 = case lookupTotal f (tt_ctxt ist) of
631 [Total _] -> Unchecked -- okay so far
632 [Partial _] -> Partial (Other [f])
633 x -> error (show x)
634 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
635 = Total []
636 tryPath desc path (e@(f, args) : es) arg
637 | e `elem` es && allNothing args = Partial (Mutual [f])
638 tryPath desc path (e@(f, nextargs) : es) arg
639 | Just d <- lookup (e, arg) path
640 = if desc > 0
641 then -- trace ("Descent " ++ show (desc - d) ++ " "
642 -- ++ show (path, e)) $
643 Total []
644 else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
645 | e `elem` map (fst . fst) path
646 && not (f `elem` map fst es)
647 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
648 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
649 let argspos = case collapseNothing (zip nextargs [0..]) of
650 [] -> [(Nothing, 0)]
651 x -> x
652-- trace (show (argspos, nextargs, path)) $
653 pathres =
654 do (a, pos) <- argspos
655 case a of
656 Nothing -> -- don't know, but if the
657 -- rest definitely terminates without
658 -- any cycles with route so far,
659 -- then we might yet be total
660 case collapse (map (tryPath 0 (((e, arg), 0):path) es)
661 [0..length nextargs - 1]) of
662 Total _ -> return Unchecked
663 x -> return x
664 Just (nextarg, sc) ->
665 if nextarg == arg then
666 case sc of
667 Same -> return $ tryPath desc (((e, arg), desc) : path)
668 es pos
669 Smaller -> return $ tryPath (desc+1)
670 (((e, arg), desc) : path)
671 es
672 pos
673 _ -> trace ("Shouldn't happen " ++ show e) $
674 return (Partial Itself)
675 else return Unchecked in
676-- trace (show (desc, argspos, path, es, pathres)) $
677 collapse' Unchecked pathres
679 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
680 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
681 | otherwise = Unchecked
683allNothing xs = null (collapseNothing (zip xs [0..]))
685collapseNothing ((Nothing, _) : xs)
686 = filter (\ (x, _) -> case x of
687 Nothing -> False
688 _ -> True) xs
689collapseNothing (x : xs) = x : collapseNothing xs
690collapseNothing [] = []
692noPartial (Partial p : xs) = Partial p
693noPartial (_ : xs) = noPartial xs
694noPartial [] = Total []
696collapse xs = collapse' Unchecked xs
697collapse' def (Total r : xs) = Total r
698collapse' def (Unchecked : xs) = collapse' def xs
699collapse' def (d : xs) = collapse' d xs
700-- collapse' Unchecked [] = Total []
701collapse' def [] = def