@@ -0,0 +1,649 @@
1+{-|
2+Module : Idris.Coverage
3+Description : The coverage and totality checkers for Idris are in this module.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+-}
8+{-# LANGUAGE PatternGuards #-}
9+module Idris.Termination where
10+
11+import Idris.AbsSyntax
12+import Idris.Core.CaseTree
13+import Idris.Core.Evaluate
14+import Idris.Core.TT
15+import Idris.Delaborate
16+import Idris.Error
17+import Idris.Output (iWarn, iputStrLn)
18+
19+import Control.Monad.State.Strict
20+import Data.Char
21+import Data.Either
22+import Data.List
23+import Data.Maybe
24+import Debug.Trace
25+
26+-- | Check whether function and all descendants cover all cases
27+-- (partial is okay, as long as it's due to recursion)
28+checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
29+checkAllCovering fc done top n | not (n `elem` done)
30+ = do i <- get
31+ case lookupTotal n (tt_ctxt i) of
32+ [tot@(Partial NotCovering)] ->
33+ do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n
34+ putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }
35+ addIBC (IBCTotCheckErr fc msg)
36+ [Partial _] ->
37+ case lookupCtxt n (idris_callgraph i) of
38+ [cg] -> mapM_ (checkAllCovering fc (n : done) top)
39+ (calls cg)
40+ _ -> return ()
41+ x -> return () -- stop if total
42+checkAllCovering _ _ _ _ = return ()
43+
44+-- | Check whether all 'Inf' arguments to the name end up guaranteed to be
45+-- guarded by constructors (conservatively... maybe this can do better later).
46+-- Essentially, all it does is check that every branch is a constructor application
47+-- with no other function applications.
48+--
49+-- If so, set the 'AllGuarded' flag which can be used by the productivity check
50+checkIfGuarded :: Name -> Idris ()
51+checkIfGuarded n
52+ = do i <- get
53+ let ctxt = tt_ctxt i
54+ case lookupDefExact n ctxt of
55+ Just (CaseOp _ ty _ _ _ cases) ->
56+ let gnames = fst (cases_compiletime cases) in
57+ if allGuarded gnames i (snd (cases_compiletime cases))
58+ then -- trace (show (n, gnames, ty, cases_compiletime cases)) $
59+ addFnOpt n AllGuarded
60+ else return ()
61+ _ -> return ()
62+ where
63+ guard n ist = isConName n (tt_ctxt ist) || guardFlag n ist
64+ guardFlag n ist = case lookupCtxtExact n (idris_flags ist) of
65+ Nothing -> False
66+ Just fs -> AllGuarded `elem` fs
67+
68+ -- Top level thing always needs to be a constructor application if
69+ -- the delayed things are going to be definitely guarded by this definition
70+ allGuarded names i (STerm t)
71+ | (P _ fn _, args) <- unApply t,
72+ guard fn i
73+ = and (map (guardedTerm names i) args)
74+ | otherwise = False
75+ allGuarded names i (ProjCase _ alts) = and (map (guardedAlt names i) alts)
76+ allGuarded names i (Case _ _ alts) = and (map (guardedAlt names i) alts)
77+ allGuarded names i _ = True
78+
79+ guardedTerm names i (P _ v _) = v `elem` names || guard v i
80+ guardedTerm names i (Bind n (Let t v) sc)
81+ = guardedTerm names i v && guardedTerm names i sc
82+ guardedTerm names i (Bind n b sc) = False
83+ guardedTerm names i ap@(App _ _ _)
84+ | (P _ fn _, args) <- unApply ap,
85+ guard fn i || fn `elem` names
86+ = and (map (guardedTerm names i) args)
87+ guardedTerm names i (App _ f a) = False
88+ guardedTerm names i tm = True
89+
90+ guardedAlt names i (ConCase _ _ _ t) = allGuarded names i t
91+ guardedAlt names i (FnCase _ _ t) = allGuarded names i t
92+ guardedAlt names i (ConstCase _ t) = allGuarded names i t
93+ guardedAlt names i (SucCase _ t) = allGuarded names i t
94+ guardedAlt names i (DefaultCase t) = allGuarded names i t
95+
96+-- | Check if, in a given group of type declarations mut_ns, the
97+-- constructor cn : ty is strictly positive, and update the context
98+-- accordingly
99+checkPositive :: [Name] -- ^ the group of type declarations
100+ -> (Name, Type) -- ^ the constructor
101+ -> Idris Totality
102+checkPositive mut_ns (cn, ty')
103+ = do i <- getIState
104+ let ty = delazy' True (normalise (tt_ctxt i) [] ty')
105+ let p = cp i ty
106+ let tot = if p then Total (args ty) else Partial NotPositive
107+ let ctxt' = setTotal cn tot (tt_ctxt i)
108+ putIState (i { tt_ctxt = ctxt' })
109+ logCoverage 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns
110+ addIBC (IBCTotal cn tot)
111+ return tot
112+ where
113+ args t = [0..length (getArgTys t)-1]
114+
115+ cp i (Bind n (Pi _ aty _) sc)
116+ = posArg i aty && cp i sc
117+ cp i t | (P _ n' _ , args) <- unApply t,
118+ n' `elem` mut_ns = all noRec args
119+ cp i _ = True
120+
121+ posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc
122+ posArg ist t = posParams ist t
123+
124+ noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
125+
126+ -- If the type appears recursively in a parameter argument, that's
127+ -- fine, otherwise if it appears in an argument it's not fine.
128+ posParams ist t | (P _ n _, args) <- unApply t
129+ = case lookupCtxtExact n (idris_datatypes ist) of
130+ Just ti -> checkParamsOK (param_pos ti) 0 args
131+ Nothing -> and (map (posParams ist) args)
132+ posParams ist t = noRec t
133+
134+ checkParamsOK ppos i [] = True
135+ checkParamsOK ppos i (p : ps)
136+ | i `elem` ppos = checkParamsOK ppos (i + 1) ps
137+ | otherwise = noRec p && checkParamsOK ppos (i + 1) ps
138+
139+-- | Calculate the totality of a function from its patterns. Either
140+-- follow the size change graph (if inductive) or check for
141+-- productivity (if coinductive)
142+calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
143+calcTotality fc n pats
144+ = do i <- getIState
145+ let opts = case lookupCtxt n (idris_flags i) of
146+ [fs] -> fs
147+ _ -> []
148+ case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
149+ (failure : _) -> return failure
150+ _ -> checkSizeChange n
151+ where
152+ checkLHS i (P _ fn _)
153+ = case lookupTotalExact fn (tt_ctxt i) of
154+ Just (Partial _) -> return (Partial (Other [fn]))
155+ _ -> Nothing
156+ checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
157+ checkLHS _ _ = Nothing
158+
159+checkTotality :: [Name] -> FC -> Name -> Idris Totality
160+checkTotality path fc n
161+ | n `elem` path = return (Partial (Mutual (n : path)))
162+ | otherwise = do
163+ t <- getTotality n
164+ i <- getIState
165+ ctxt' <- do ctxt <- getContext
166+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt
167+ setContext ctxt'
168+ ctxt <- getContext
169+ i <- getIState
170+ let opts = case lookupCtxt n (idris_flags i) of
171+ [fs] -> fs
172+ _ -> []
173+ t' <- case t of
174+ Unchecked ->
175+ case lookupDef n ctxt of
176+ [CaseOp _ _ _ _ pats _] ->
177+ do t' <- if AssertTotal `elem` opts
178+ then return $ Total []
179+ else calcTotality fc n pats
180+ logCoverage 2 $ "Set to " ++ show t'
181+ setTotality n t'
182+ addIBC (IBCTotal n t')
183+ return t'
184+ [TyDecl (DCon _ _ _) ty] ->
185+ case unApply (getRetTy ty) of
186+ (P _ tyn _, _) -> do
187+ let ms = case lookupCtxt tyn (idris_datatypes i) of
188+ [TI _ _ _ _ xs@(_:_)] -> xs
189+ ts -> [tyn]
190+ checkPositive ms (n, ty)
191+ _-> return $ Total []
192+ _ -> return $ Total []
193+ x -> return x
194+ case t' of
195+ Total _ -> return t'
196+ Productive -> return t'
197+ e -> do w <- cmdOptType WarnPartial
198+ if TotalFn `elem` opts
199+ then do totalityError t'; return t'
200+ else do when (w && not (PartialFn `elem` opts)) $
201+ warnPartial n t'
202+ return t'
203+ where
204+ totalityError t = do i <- getIState
205+ let msg = show n ++ " is " ++ show t
206+ putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}
207+ addIBC (IBCTotCheckErr fc msg)
208+
209+ warnPartial n t
210+ = do i <- getIState
211+ case lookupDef n (tt_ctxt i) of
212+ [x] -> do
213+ iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t
214+-- ++ "\n" ++ show x
215+-- let cg = lookupCtxtName Nothing n (idris_callgraph i)
216+-- iputStrLn (show cg)
217+
218+
219+checkDeclTotality :: (FC, Name) -> Idris Totality
220+checkDeclTotality (fc, n)
221+ = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"
222+ i <- getIState
223+ let opts = case lookupCtxtExact n (idris_flags i) of
224+ Just fs -> fs
225+ _ -> []
226+ when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
227+ t <- checkTotality [] fc n
228+ return t
229+
230+-- If the name calls something which is partial, set it as partial
231+verifyTotality :: (FC, Name) -> Idris ()
232+verifyTotality (fc, n)
233+ = do logCoverage 2 $ "Checking " ++ show n ++ "'s descendents are total"
234+ ist <- getIState
235+ case lookupTotalExact n (tt_ctxt ist) of
236+ Just (Total _) -> do
237+ let ns = getNames (tt_ctxt ist)
238+
239+ case getPartial ist [] ns of
240+ Nothing -> return ()
241+ Just bad -> do let t' = Partial (Other bad)
242+ logCoverage 2 $ "Set to " ++ show t'
243+ setTotality n t'
244+ addIBC (IBCTotal n t')
245+ _ -> return ()
246+ where
247+ getNames ctxt = case lookupDefExact n ctxt of
248+ Just (CaseOp _ _ _ _ _ defs)
249+ -> let (top, def) = cases_compiletime defs in
250+ map fst (findCalls' True def top)
251+ _ -> []
252+
253+ getPartial ist [] [] = Nothing
254+ getPartial ist bad [] = Just bad
255+ getPartial ist bad (n : ns)
256+ = case lookupTotalExact n (tt_ctxt ist) of
257+ Just (Partial _) -> getPartial ist (n : bad) ns
258+ _ -> getPartial ist bad ns
259+
260+-- | Calculate the size change graph for this definition
261+--
262+-- SCG for a function f consists of a list of:
263+-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
264+--
265+-- where g is a function called
266+-- a1 ... an are the arguments of f in positions 1..n of g
267+-- sizechange1 ... sizechange2 is how their size has changed wrt the input
268+-- to f
269+-- Nothing, if the argument is unrelated to the input
270+buildSCG :: (FC, Name) -> Idris ()
271+buildSCG (_, n) = do
272+ ist <- getIState
273+ case lookupCtxt n (idris_callgraph ist) of
274+ [cg] -> case lookupDefExact n (tt_ctxt ist) of
275+ Just (CaseOp _ _ _ pats _ cd) ->
276+ let (args, sc) = cases_compiletime cd in
277+ do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"
278+ ++ show pats ++ "\n" ++ show sc
279+ let newscg = buildSCG' ist n (rights pats) args
280+ logCoverage 5 $ "SCG is: " ++ show newscg
281+ addToCG n ( cg { scg = newscg } )
282+ _ -> return () -- CG comes from a type declaration only
283+ [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"
284+ x -> error $ "buildSCG: " ++ show (n, x)
285+
286+delazy = delazy' False -- not lazy codata
287+delazy' all t@(App _ f a)
288+ | (P _ (UN l) _, [_, _, arg]) <- unApply t,
289+ l == txt "Force" = delazy' all arg
290+ | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
291+ l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg
292+ | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
293+ l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg
294+delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
295+delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
296+delazy' all t = t
297+
298+data Guardedness = Toplevel | Unguarded | Guarded | Delayed
299+ deriving Show
300+
301+buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
302+buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
303+ scgPat (lhs, rhs) = let lhs' = delazy lhs
304+ rhs' = delazy rhs
305+ (f, pargs) = unApply (dePat lhs') in
306+ findCalls [] Toplevel (dePat rhs') (patvars lhs')
307+ (zip pargs [0..])
308+
309+ -- Under a delay, calls are excluded from the graph - if it's a call to a
310+ -- non-total function we'll find that in the final totality check
311+ findCalls cases Delayed ap@(P _ n _) pvs args = []
312+ findCalls cases guarded ap@(App _ f a) pvs pargs
313+ -- under a call to "assert_total", don't do any checking, just believe
314+ -- that it is total.
315+ | (P _ (UN at) _, [_, _]) <- unApply ap,
316+ at == txt "assert_total" = []
317+ -- don't go under calls to functions which are asserted total
318+ | (P _ n _, _) <- unApply ap,
319+ Just opts <- lookupCtxtExact n (idris_flags ist),
320+ AssertTotal `elem` opts = []
321+ -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't
322+ -- check under guarded constructors.
323+ | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
324+ Guarded <- guarded,
325+ del == txt "Delay"
326+ = findCalls cases Delayed arg pvs pargs
327+ | (P _ n _, args) <- unApply ap,
328+ Delayed <- guarded,
329+ isConName n (tt_ctxt ist) || allGuarded n ist
330+ = -- Still under a 'Delay' and constructor guarded, so check
331+ -- just the arguments to the constructor, remaining Delayed
332+ concatMap (\x -> findCalls cases guarded x pvs pargs) args
333+ | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,
334+ ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]
335+ -- Continue look inside if...then...else blocks
336+ -- TODO: Consider whether we should do this for user defined ifThenElse
337+ -- rather than just the one in the Prelude as a special case
338+ = findCalls cases guarded t pvs pargs ++
339+ findCalls cases guarded e pvs pargs
340+ | (P _ n _, args) <- unApply ap,
341+ caseName n && n /= topfn,
342+ notPartial (lookupTotalExact n (tt_ctxt ist))
343+ -- case block - look inside the block, as long as it was covering
344+ -- (i.e. not currently set at Partial) to get a more accurate size
345+ -- change result from the top level patterns (also to help pass
346+ -- information through from guarded corecursion accurately)
347+ = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args ++
348+ if n `notElem` cases
349+ then findCallsCase (n : cases) guarded n args pvs pargs
350+ else []
351+ | (P _ n _, args) <- unApply ap,
352+ Delayed <- guarded
353+ -- Under a delayed recursive call just check the arguments
354+ = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args
355+ | (P _ n _, args) <- unApply ap
356+ -- Ordinary call, not under a delay.
357+ -- If n is a constructor, set 'args' as Guarded
358+ = let nguarded = case guarded of
359+ Unguarded -> Unguarded
360+ x -> if isConName n (tt_ctxt ist)
361+ || allGuarded n ist
362+ then Guarded
363+ else Unguarded in
364+ mkChange n args pargs ++
365+ concatMap (\x -> findCalls cases nguarded x pvs pargs) args
366+ where notPartial (Just (Partial NotCovering)) = False
367+ notPartial _ = True
368+ findCalls cases guarded (App _ f a) pvs pargs
369+ = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs
370+ findCalls cases guarded (Bind n (Let t v) e) pvs pargs
371+ = findCalls cases Unguarded t pvs pargs ++
372+ findCalls cases Unguarded v pvs pargs ++
373+ -- Substitute in the scope since this might reveal some useful
374+ -- structure
375+ findCalls cases guarded (substV v e) pvs pargs
376+ findCalls cases guarded (Bind n t e) pvs pargs
377+ = findCalls cases Unguarded (binderTy t) pvs pargs ++
378+ findCalls cases guarded e (n : pvs) pargs
379+ findCalls cases guarded (P _ f _ ) pvs pargs
380+ | not (f `elem` pvs) = [(f, [])]
381+ findCalls _ _ _ _ _ = []
382+
383+ -- Assumption is that names are preserved in the case block (shadowing
384+ -- dealt with by the elaborator) so we can just assume the top level names
385+ -- are okay for building the size change
386+ findCallsCase cases guarded n args pvs pargs
387+ = case lookupDefExact n (tt_ctxt ist) of
388+ Just (CaseOp _ _ _ pats _ cd) ->
389+ concatMap (fccPat cases pvs pargs args guarded) (rights pats)
390+ Nothing -> []
391+
392+ fccPat cases pvs pargs args g (lhs, rhs)
393+ = let lhs' = delazy lhs
394+ rhs' = delazy rhs
395+ (f, pargs_case) = unApply (dePat lhs')
396+ -- pargs is a pair of a term, and the argument position that
397+ -- term appears in. If any of the arguments to the case block
398+ -- are also on the lhs, we also want those patterns to appear
399+ -- in the parg list so that we'll spot patterns which are
400+ -- smaller than then
401+ newpargs = newPArg args pargs
402+ -- Now need to update the rhs of the case with the names in the
403+ -- outer definition: In rhs', wherever we see what's in pargs_case,
404+ -- replace it with the corresponding thing in pargs
405+ csubs = zip pargs_case args
406+ newrhs = doCaseSubs csubs (dePat rhs')
407+ pargs' = pargs ++ addPArg newpargs pargs_case in
408+ findCalls cases g newrhs pvs pargs'
409+ where
410+ doCaseSubs [] tm = tm
411+ doCaseSubs ((x, x') : cs) tm
412+ = doCaseSubs (subIn x x' cs) (substTerm x x' tm)
413+
414+ subIn x x' [] = []
415+ subIn x x' ((l, r) : cs)
416+ = (substTerm x x' l, substTerm x x' r) : subIn x x' cs
417+
418+ addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'
419+ addPArg (Nothing : ts) (t' : ts') = addPArg ts ts'
420+ addPArg _ _ = []
421+
422+ newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
423+ newPArg (t : ts) pargs = case lookup t pargs of
424+ Just i -> Just (t, i) : newPArg ts pargs
425+ Nothing -> Nothing : newPArg ts pargs
426+ newPArg [] pargs = []
427+
428+ expandToArity n args
429+ = case lookupTy n (tt_ctxt ist) of
430+ [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
431+ _ -> args
432+ where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
433+ expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []
434+ expand i _ xs = xs
435+
436+ mkChange n args pargs = [(n, expandToArity n (sizes args))]
437+ where
438+ sizes [] = []
439+ sizes (a : as) = checkSize a pargs : sizes as
440+
441+ -- find which argument in pargs <a> is smaller than, if any
442+ checkSize a ((p, i) : ps)
443+ | a == p = Just (i, Same)
444+ | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
445+ as == txt "assert_smaller" && arg == p
446+ = Just (i, Smaller)
447+ | smaller Nothing a (p, Nothing) = Just (i, Smaller)
448+ | otherwise = checkSize a ps
449+ checkSize a [] = Nothing
450+
451+ -- the smaller thing we find must be defined in the same group of mutally
452+ -- defined types as <a>, and not be coinductive - so carry the type of
453+ -- the constructor we've gone under.
454+
455+ smaller (Just tyn) a (t, Just tyt)
456+ | a == t = isInductive (fst (unApply (getRetTy tyn)))
457+ (fst (unApply (getRetTy tyt)))
458+ smaller ty a (ap@(App _ f s), _)
459+ | (P (DCon _ _ _) n _, args) <- unApply ap
460+ = let tyn = getType n in
461+ any (smaller (ty `mplus` Just tyn) a)
462+ (zip args (map toJust (getArgTys tyn)))
463+ -- check higher order recursive arguments
464+ smaller ty (App _ f s) a = smaller ty f a
465+ smaller _ _ _ = False
466+
467+ toJust (n, t) = Just t
468+
469+ getType n = case lookupTyExact n (tt_ctxt ist) of
470+ Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
471+
472+ isInductive (P _ nty _) (P _ nty' _) =
473+ let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of
474+ [TI _ x _ _ muts] -> (x, muts)
475+ _ -> (False, []) in
476+ (nty == nty' || any (== nty') muts) && not co
477+ isInductive _ _ = False
478+
479+ dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
480+ dePat t = t
481+
482+ patvars (Bind x (PVar _) sc) = x : patvars sc
483+ patvars _ = []
484+
485+ allGuarded n ist = case lookupCtxtExact n (idris_flags ist) of
486+ Nothing -> False
487+ Just fs -> AllGuarded `elem` fs
488+
489+checkSizeChange :: Name -> Idris Totality
490+checkSizeChange n = do
491+ ist <- getIState
492+ case lookupCtxt n (idris_callgraph ist) of
493+ [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
494+ logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++
495+ "from " ++ show (scg cg) ++ "\n" ++
496+ show (length ms) ++ "\n" ++
497+ showSep "\n" (map show ms))
498+ logCoverage 6 (show cg)
499+ -- every multipath must have an infinitely descending
500+ -- thread, then the function terminates
501+ -- also need to checks functions called are all total
502+ -- (Unchecked is okay as we'll spot problems here)
503+ let tot = map (checkMP ist n (getArity ist n)) ms
504+ logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"
505+ logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++
506+ (showSep "\n" (map show (zip ms tot)))
507+ return (noPartial tot)
508+ [] -> do logCoverage 5 $ "No paths for " ++ show n
509+ return Unchecked
510+ where getArity ist n
511+ = case lookupTy n (tt_ctxt ist) of
512+ [ty] -> arity (normalise (tt_ctxt ist) [] ty)
513+ _ -> error "Can't happen: checkSizeChange.getArity"
514+
515+type MultiPath = [SCGEntry]
516+
517+mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
518+mkMultiPaths ist path [] = [reverse path]
519+mkMultiPaths ist path cg = concatMap extend cg
520+ where extend (nextf, args)
521+ | (nextf, args) `inPath` path = [ reverse ((nextf, args) : path) ]
522+ | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
523+ = case lookupCtxt nextf (idris_callgraph ist) of
524+ [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
525+ _ -> [ reverse ((nextf, args) : path) ]
526+ | otherwise = [ reverse ((nextf, args) : path) ]
527+
528+ inPath :: SCGEntry -> [SCGEntry] -> Bool
529+ inPath f [] = False
530+ inPath f (g : gs) = smallerEq f g || f == g || inPath f gs
531+
532+ smallerEq :: SCGEntry -> SCGEntry -> Bool
533+ smallerEq (f, args) (g, args')
534+ = f == g && not (null (filter smallers args))
535+ && filter smallers args == filter smallers args'
536+ smallers (Just (_, Smaller)) = True
537+ smallers _ = False
538+
539+-- If any route along the multipath leads to infinite descent, we're fine.
540+-- Try a route beginning with every argument.
541+-- If we reach a point we've been to before, but with a smaller value,
542+-- that means there is an infinitely descending path from that argument.
543+
544+checkMP :: IState -> Name -> Int -> MultiPath -> Totality
545+checkMP ist topfn i mp = if i > 0
546+ then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
547+-- trace ("Paths " ++ show paths) $
548+ collapse paths
549+ else tryPath 0 [] mp 0
550+ where
551+ tryPath' d path mp arg
552+ = let res = tryPath d path mp arg in
553+ trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
554+
555+ mkBig (e, d) = (e, 10000)
556+
557+ tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
558+ tryPath desc path [] _ = Total []
559+-- tryPath desc path ((UN "believe_me", _) : _) arg
560+-- = Partial BelieveMe
561+ -- if we get to a constructor, it's fine as long as it's strictly positive
562+ tryPath desc path ((f, _) : es) arg
563+ | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
564+ = case lookupTotalExact f (tt_ctxt ist) of
565+ Just (Total _) -> Unchecked -- okay so far
566+ Just (Partial _) -> Partial (Other [f])
567+ x -> Unchecked -- An error elsewhere, set as Unchecked to make
568+ -- some progress
569+ | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
570+ = Total []
571+ tryPath desc path (e@(f, args) : es) arg
572+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
573+ | e `elem` es && allNothing args = Partial (Mutual [f])
574+ tryPath desc path (e@(f, nextargs) : es) arg
575+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
576+ | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
577+ | Just d <- lookup (e, arg) path
578+ = if desc - d > 0 -- Now lower than when we were last here
579+ then -- trace ("Descent " ++ show (desc - d) ++ " "
580+ -- ++ show (path, e)) $
581+ Total []
582+ else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
583+ | e `elem` map (fst . fst) path
584+ && not (f `elem` map fst es)
585+ = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
586+ | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
587+ let argspos = zip nextargs [0..]
588+ pathres =
589+ do (a, pos) <- argspos
590+ case a of
591+ Nothing -> -- gone up, but if the
592+ -- rest definitely terminates without any
593+ -- cycles (including the path so far, which
594+ -- we take as inaccessible) the path is fine
595+ return $ tryPath 0 (map mkBig (((e, arg), desc) : path)) es pos
596+ Just (nextarg, sc) ->
597+ if nextarg == arg then
598+ case sc of
599+ Same -> return $ tryPath desc (((e, arg), desc) : path)
600+ es pos
601+ Smaller -> return $ tryPath (desc+1)
602+ (((e, arg), desc) : path)
603+ es
604+ pos
605+ _ -> trace ("Shouldn't happen " ++ show e) $
606+ return (Partial Itself)
607+ else return Unchecked in
608+-- trace (show (desc, argspos, path, es, pathres)) $
609+ collapse pathres
610+
611+ | otherwise = Unchecked
612+
613+allNothing :: [Maybe a] -> Bool
614+allNothing xs = null (collapseNothing (zip xs [0..]))
615+
616+collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
617+collapseNothing ((Nothing, t) : xs)
618+ = (Nothing, t) : filter (\ (x, _) -> case x of
619+ Nothing -> False
620+ _ -> True) xs
621+collapseNothing (x : xs) = x : collapseNothing xs
622+collapseNothing [] = []
623+
624+noPartial :: [Totality] -> Totality
625+noPartial (Partial p : xs) = Partial p
626+noPartial (_ : xs) = noPartial xs
627+noPartial [] = Total []
628+
629+collapse :: [Totality] -> Totality
630+collapse xs = collapse' Unchecked xs
631+collapse' def (Total r : xs) = Total r
632+collapse' def (Unchecked : xs) = collapse' def xs
633+collapse' def (d : xs) = collapse' d xs
634+-- collapse' Unchecked [] = Total []
635+collapse' def [] = def
636+
637+totalityCheckBlock :: Idris ()
638+totalityCheckBlock = do
639+ ist <- getIState
640+ -- Do totality checking after entire mutual block
641+ mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n
642+ ctxt' <- do ctxt <- getContext
643+ tclift $ simplifyCasedef n (getErasureInfo ist) ctxt
644+ setContext ctxt')
645+ (map snd (idris_totcheck ist))
646+ mapM_ buildSCG (idris_totcheck ist)
647+ mapM_ checkDeclTotality (idris_totcheck ist)
648+ clear_totcheck
649+