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