@@ -535,13 +535,17 @@ mkMultiPaths ist path cg
535535-- If any route along the multipath leads to infinite descent, we're fine.
536536-- Try a route beginning with every argument.
537537-- If we reach a point we've been to before, but with a smaller value,
538−-- that means there is an infinitely descending path.
538+-- that means there is an infinitely descending path from that argument.
539539
540540checkMP :: IState -> Int -> MultiPath -> Totality
541541checkMP ist i mp = if i > 0
542542 then collapse (map (tryPath 0 [] mp) [0..i-1])
543543 else tryPath 0 [] mp 0
544544 where
545+ tryPath' d path mp arg
546+ = let res = tryPath d path mp arg in
547+ trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
548+
545549 tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality
546550 tryPath desc path [] _ = Total []
547551-- tryPath desc path ((UN "believe_me", _) : _) arg
@@ -550,7 +554,7 @@ checkMP ist i mp = if i > 0
550554 tryPath desc path ((f, _) :es) arg
551555 | [TyDecl (DCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
552556 = case lookupTotal f (tt_ctxt ist) of
553− [Total _] -> Total []
557+ [Total _] -> Unchecked -- okay so far
554558 [Partial _] -> Partial (Other [f])
555559 x -> error (show x)
556560 | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
@@ -561,39 +565,48 @@ checkMP ist i mp = if i > 0
561565 tryPath desc path (e@(f, nextargs) : es) arg
562566 | Just d <- lookup e path
563567 = if (desc - d) > 0
564− then Total []
568+ then -- trace ("Descent " ++ show (desc - d) ++ " "
569+ -- ++ show (path, e)) $
570+ Total []
565571 else Partial (Mutual (map (fst . fst) path ++ [f]))
566572 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
567573 let argspos = zip nextargs [0..] in
568− collapse' (Partial (Mutual (map (fst . fst) path ++ [f]))) $
569− do (arg, pos) <- argspos
570− case arg of
571− Nothing -> -- don't know, but it's okay if the
574+ collapse' Unchecked $
575+ do (a, pos) <- argspos
576+ case a of
577+ Nothing -> -- don't know, but if the
572578 -- rest definitely terminates without
573− -- any cycles with route so far
574− map (tryPath (-10000) ((e, desc):path) es)
575− [0..length nextargs - 1]
579+ -- any cycles with route so far,
580+ -- then we might yet be total
581+ case collapse (map (tryPath (-10000) ((e, desc):path) es)
582+ [0..length nextargs - 1]) of
583+ Total _ -> return Unchecked
584+ x -> return x
576585 Just (nextarg, sc) ->
577− case sc of
578− Same -> return $ tryPath desc ((e, desc):path)
579− es
580− nextarg
581− Smaller -> return $ tryPath (desc+1)
582− ((e, desc):path)
583− es
584− nextarg
585− _ -> trace ("Shouldn't happen " ++ show e) $
586− return (Partial Itself)
587− | [Total _] <- lookupTotal f (tt_ctxt ist) = Total []
586+ if nextarg == arg then
587+ case sc of
588+ Same -> return $ tryPath desc ((e, desc):path)
589+ es
590+ pos
591+ Smaller -> return $ tryPath (desc+1)
592+ ((e, desc):path)
593+ es
594+ pos
595+ _ -> trace ("Shouldn't happen " ++ show e) $
596+ return (Partial Itself)
597+ else return Unchecked
598+ | [Total _] <- lookupTotal f (tt_ctxt ist) = Unchecked
588599 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
589− | otherwise = Total []
600+ | otherwise = Unchecked
590601
591602noPartial (Partial p : xs) = Partial p
592603noPartial (_ : xs) = noPartial xs
593604noPartial [] = Total []
594605
595−collapse xs = collapse' (Partial Itself) xs
596−collapse' def (Total r : xs) = Total r
606+collapse xs = collapse' Unchecked xs
607+collapse' def (Total r : xs) = Total r
608+collapse' def (Unchecked : xs) = collapse' def xs
597609collapse' def (d : xs) = collapse' d xs
610+collapse' Unchecked [] = Total []
598611collapse' def [] = def
599612