content: {-|
  Module      : Idris.Termination
  Description : The termination checker for Idris
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  {-# LANGUAGE PatternGuards #-}
  module Idris.Termination (buildSCG, checkAllCovering, checkDeclTotality,
                            checkIfGuarded, checkPositive, checkSizeChange,
                            verifyTotality) where
  
  import Idris.AbsSyntax
  import Idris.Core.CaseTree
  import Idris.Core.Evaluate
  import Idris.Core.TT
  import Idris.Delaborate
  import Idris.Error
  import Idris.Options
  import Idris.Output (iWarn)
  
  import Control.Monad
  import Control.Monad.State.Strict
  import Data.Either
  import Data.List
  import Data.Maybe
  import Debug.Trace
  
  -- | Check whether function and all descendants cover all cases
  -- (partial is okay, as long as it's due to recursion)
  checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
  checkAllCovering fc done top n | not (n `elem` done)
     = do i <- get
          case lookupTotal n (tt_ctxt i) of
               [tot@(Partial NotCovering)] ->
                      do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n
                         putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }
                         addIBC (IBCTotCheckErr fc msg)
               [Partial (Other ns)] ->
                       -- Check that none of the partial functions it relies
                       -- on are partial due to missing cases
                       mapM_ (checkAllCovering fc (n : done) top) ns
               x -> return () -- stop if total, or partial due to recursion
  checkAllCovering _ _ _ _ = return ()
  
  -- | Check whether all 'Inf' arguments to the name end up guaranteed to be
  -- guarded by constructors (conservatively... maybe this can do better later).
  -- Essentially, all it does is check that every branch is a constructor application
  -- with no other function applications.
  --
  -- If so, set the 'AllGuarded' flag which can be used by the productivity check
  checkIfGuarded :: Name -> Idris ()
  checkIfGuarded n
     = do i <- get
          let ctxt = tt_ctxt i
          case lookupDefExact n ctxt of
               Just (CaseOp _ ty _ _ _ cases) ->
                    let gnames = fst (cases_compiletime cases) in
                        if allGuarded gnames i (snd (cases_compiletime cases))
                           then -- trace (show (n, gnames, ty, cases_compiletime cases)) $
                                addFnOpt n AllGuarded
                           else return ()
               _ -> return ()
    where
      guard n ist = isConName n (tt_ctxt ist) || guardFlag n ist
      guardFlag n ist = case lookupCtxtExact n (idris_flags ist) of
                             Nothing -> False
                             Just fs -> AllGuarded `elem` fs
  
      -- Top level thing always needs to be a constructor application if
      -- the delayed things are going to be definitely guarded by this definition
      allGuarded names i (STerm t)
            | (P _ fn _, args) <- unApply t,
              guard fn i
              = and (map (guardedTerm names i) args)
            | otherwise = False
      allGuarded names i (ProjCase _ alts) = and (map (guardedAlt names i) alts)
      allGuarded names i (Case _ _ alts) = and (map (guardedAlt names i) alts)
      allGuarded names i _ = True
  
      guardedTerm names i (P _ v _) = v `elem` names || guard v i
      guardedTerm names i (Bind n (Let rig t v) sc)
            = guardedTerm names i v && guardedTerm names i sc
      guardedTerm names i (Bind n b sc) = False
      guardedTerm names i ap@(App _ _ _)
            | (P _ fn _, args) <- unApply ap,
              guard fn i || fn `elem` names
                  = and (map (guardedTerm names i) args)
      guardedTerm names i (App _ f a) = False
      guardedTerm names i tm = True
  
      guardedAlt names i (ConCase _ _ _ t) = allGuarded names i t
      guardedAlt names i (FnCase _ _ t) = allGuarded names i t
      guardedAlt names i (ConstCase _ t) = allGuarded names i t
      guardedAlt names i (SucCase _ t) = allGuarded names i t
      guardedAlt names i (DefaultCase t) = allGuarded names i t
  
  -- | Check if, in a given group of type declarations mut_ns, the
  -- constructor cn : ty is strictly positive, and update the context
  -- accordingly
  checkPositive :: [Name]       -- ^ the group of type declarations
                -> (Name, Type) -- ^ the constructor
                -> Idris Totality
  checkPositive mut_ns (cn, ty')
      = do i <- getIState
           let ty = delazy' True (normalise (tt_ctxt i) [] ty')
           let p = cp i ty
           let tot = if p then Total (args ty) else Partial NotPositive
           let ctxt' = setTotal cn tot (tt_ctxt i)
           putIState (i { tt_ctxt = ctxt' })
           logCoverage 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns
           addIBC (IBCTotal cn tot)
           return tot
    where
      args t = [0..length (getArgTys t)-1]
  
      cp i (Bind n (Pi _ _ aty _) sc)
           = posArg i aty && cp i sc
      cp i t | (P _ n' _ , args) <- unApply t,
               n' `elem` mut_ns = all noRec args
      cp i _ = True
  
      posArg ist (Bind _ (Pi _ _ nty _) sc) = noRec nty && posArg ist sc
      posArg ist t = posParams ist t
  
      noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
  
      -- If the type appears recursively in a parameter argument, that's
      -- fine, otherwise if it appears in an argument it's not fine.
      posParams ist t | (P _ n _, args) <- unApply t
         = case lookupCtxtExact n (idris_datatypes ist) of
                Just ti -> checkParamsOK (param_pos ti) 0 args
                Nothing -> and (map (posParams ist) args)
      posParams ist t = noRec t
  
      checkParamsOK ppos i [] = True
      checkParamsOK ppos i (p : ps)
            | i `elem` ppos = checkParamsOK ppos (i + 1) ps
            | otherwise = noRec p && checkParamsOK ppos (i + 1) ps
  
  -- | Calculate the totality of a function from its patterns.  Either
  -- follow the size change graph (if inductive) or check for
  -- productivity (if coinductive)
  calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
  calcTotality fc n pats
      = do i <- getIState
           case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
              (failure : _) -> return failure
              _ -> checkSizeChange n
    where
      checkLHS i (P _ fn _)
          = case lookupTotalExact fn (tt_ctxt i) of
                 Just (Partial _) -> return (Partial (Other [fn]))
                 _ -> Nothing
      checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
      checkLHS _ _ = Nothing
  
  checkTotality :: [Name] -> FC -> Name -> Idris Totality
  checkTotality path fc n
      | n `elem` path = return (Partial (Mutual (n : path)))
      | otherwise = do
          t <- getTotality n
          i <- getIState
          ctxt' <- do ctxt <- getContext
                      tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt
          setContext ctxt'
          ctxt <- getContext
          i <- getIState
          let opts = case lookupCtxt n (idris_flags i) of
                              [fs] -> fs
                              _ -> []
          t' <- case t of
                  Unchecked ->
                      case lookupDef n ctxt of
                          [CaseOp _ _ _ _ pats _] ->
                              do t' <- if AssertTotal `elem` opts
                                          then return $ Total []
                                          else calcTotality fc n pats
                                 logCoverage 2 $ "Set to " ++ show t'
                                 setTotality n t'
                                 addIBC (IBCTotal n t')
                                 return t'
                          [TyDecl (DCon _ _ _) ty] ->
                              case unApply (getRetTy ty) of
                                (P _ tyn _, _) -> do
                                   let ms = case lookupCtxt tyn (idris_datatypes i) of
                                         [TI _ _ _ _ xs@(_:_) _] -> xs
                                         ts -> [tyn]
                                   checkPositive ms (n, ty)
                                _-> return $ Total []
                          _ -> return $ Total []
                  x -> return x
          case t' of
              Total _ -> return t'
              Productive -> return t'
              e -> do w <- cmdOptType WarnPartial
                      if TotalFn `elem` opts
                         then do totalityError t'; return t'
                         else do when (w && not (PartialFn `elem` opts)) $
                                     warnPartial n t'
                                 return t'
    where
      totalityError t = do i <- getIState
                           let msg = show n ++ " is " ++ show t
                           putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}
                           addIBC (IBCTotCheckErr fc msg)
  
      warnPartial n t
         = do i <- getIState
              case lookupDef n (tt_ctxt i) of
                 [x] -> do
                    iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t
  --                                ++ "\n" ++ show x
  --                   let cg = lookupCtxtName Nothing n (idris_callgraph i)
  --                   iputStrLn (show cg)
  
  
  checkDeclTotality :: (FC, Name) -> Idris Totality
  checkDeclTotality (fc, n)
      = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"
           i <- getIState
           let opts = case lookupCtxtExact n (idris_flags i) of
                                Just fs -> fs
                                _ -> []
           when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
           t <- checkTotality [] fc n
           return t
  
  -- If the name calls something which is partial, set it as partial
  verifyTotality :: (FC, Name) -> Idris ()
  verifyTotality (fc, n)
      = do logCoverage 2 $ "Checking " ++ show n ++ "'s descendents are total"
           ist <- getIState
           case lookupTotalExact n (tt_ctxt ist) of
                Just (Total _) -> do
                   let ns = getNames (tt_ctxt ist)
  
                   case getPartial ist [] ns of
                        Nothing -> return ()
                        Just bad -> do let t' = Partial (Other bad)
                                       logCoverage 2 $ "Set in verify to " ++ show t'
                                       setTotality n t'
                                       addIBC (IBCTotal n t')
                _ -> return ()
    where
      getNames ctxt = case lookupDefExact n ctxt of
                           Just (CaseOp  _ _ _ _ _ defs)
                             -> let (top, def) = cases_compiletime defs in
                                    map fst (findCalls' True def top)
                           _ -> []
  
      getPartial ist [] [] = Nothing
      getPartial ist bad [] = Just bad
      getPartial ist bad (n : ns)
          = case lookupTotalExact n (tt_ctxt ist) of
                 Just (Partial _) -> getPartial ist (n : bad) ns
                 _ -> getPartial ist bad ns
  
  -- | Calculate the size change graph for this definition
  --
  -- SCG for a function f consists of a list of:
  --    (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
  --
  -- where g is a function called
  -- a1 ... an are the arguments of f in positions 1..n of g
  -- sizechange1 ... sizechange2 is how their size has changed wrt the input
  -- to f
  --    Nothing, if the argument is unrelated to the input
  buildSCG :: (FC, Name) -> Idris ()
  buildSCG (_, n) = do
     ist <- getIState
     case lookupCtxtExact n (idris_callgraph ist) of
         Just cg -> case lookupDefExact n (tt_ctxt ist) of
             Just (CaseOp _ _ _ pats _ cd) ->
               let (args, sc) = cases_compiletime cd in
                 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"
                                  ++ show pats ++ "\n" ++ show sc
                    let newscg = buildSCG' ist n (rights pats) args
                    logCoverage 5 $ "SCG is: " ++ show newscg
                    addToCG n ( cg { scg = newscg } )
             _ -> return () -- CG comes from a type declaration only
         _ -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"
  
  delazy = delazy' False -- not lazy codata
  delazy' all t@(App _ f a)
       | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
         l == txt "Force" && (all || lty /= txt "Infinite") = delazy' all arg
       | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
         l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg
       | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
         l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg
  delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
  delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
  delazy' all t = t
  
  data Guardedness = Toplevel | Unguarded | Guarded | Delayed
    deriving Show
  
  buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
  buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
    scgPat (lhs, rhs) = let lhs' = delazy lhs
                            rhs' = delazy rhs
                            (_, pargs) = unApply (dePat lhs') in
                              findCalls [] Toplevel (dePat rhs') (patvars lhs')
                                        (zip pargs [0..])
  
    -- Under a delay, calls are excluded from the graph - if it's a call to a
    -- non-total function we'll find that in the final totality check
    findCalls cases Delayed ap@(P _ n _) pvs args = []
    findCalls cases guarded ap@(App _ f a) pvs pargs
       -- under a call to "assert_total", don't do any checking, just believe
       -- that it is total.
       | (P _ (UN at) _, [_, _]) <- unApply ap,
         at == txt "assert_total" = []
       -- don't go under calls to functions which are asserted total
       | (P _ n _, _) <- unApply ap,
         Just opts <- lookupCtxtExact n (idris_flags ist),
         AssertTotal `elem` opts = []
       -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't
       -- check under guarded constructors.
       | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
         Guarded <- guarded,
         del == txt "Delay"
             = findCalls cases Delayed arg pvs pargs
       | (P _ n _, args) <- unApply ap,
         Delayed <- guarded,
         isConName n (tt_ctxt ist) || allGuarded n ist
             = -- Still under a 'Delay' and constructor guarded, so check
               -- just the arguments to the constructor, remaining Delayed
               concatMap (\x -> findCalls cases guarded x pvs pargs) args
       | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,
         ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]
         -- Continue look inside if...then...else blocks
         -- TODO: Consider whether we should do this for user defined ifThenElse
         -- rather than just the one in the Prelude as a special case
         = findCalls cases guarded t pvs pargs ++
           findCalls cases guarded e pvs pargs
       | (P _ n _, args) <- unApply ap,
         caseName n && n /= topfn,
         notPartial (lookupTotalExact n (tt_ctxt ist))
         -- case block - look inside the block, as long as it was covering
         -- (i.e. not currently set at Partial) to get a more accurate size
         -- change result from the top level patterns (also to help pass
         -- information through from guarded corecursion accurately)
         = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args ++
               if n `notElem` cases
                  then findCallsCase (n : cases) guarded n args pvs pargs
                  else []
       | (P _ n _, args) <- unApply ap,
         Delayed <- guarded
         -- Under a delayed recursive call just check the arguments
             = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args
       | (P _ n _, args) <- unApply ap,
         not (n `elem` pvs)
          -- Ordinary call, not under a delay.
          -- If n is a constructor, set 'args' as Guarded
          = let nguarded = case guarded of
                                Unguarded -> Unguarded
                                x -> if isConName n (tt_ctxt ist)
                                         || allGuarded n ist
                                        then Guarded
                                        else Unguarded in
                mkChange n args pargs ++
                   concatMap (\x -> findCalls cases nguarded x pvs pargs) args
      where notPartial (Just (Partial NotCovering)) = False
            notPartial _ = True
    findCalls cases guarded (App _ f a) pvs pargs
          = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs
    findCalls cases guarded (Bind n (Let rig t v) e) pvs pargs
          = findCalls cases Unguarded t pvs pargs ++
            findCalls cases Unguarded v pvs pargs ++
            -- Substitute in the scope since this might reveal some useful
            -- structure
            findCalls cases guarded (substV v e) pvs pargs
    findCalls cases guarded (Bind n t e) pvs pargs
          = findCalls cases Unguarded (binderTy t) pvs pargs ++
            findCalls cases guarded e (n : pvs) pargs
    findCalls cases guarded (P _ f _ ) pvs pargs
        | not (f `elem` pvs) = [(f, [])]
    findCalls _ _ _ _ _ = []
  
    -- Assumption is that names are preserved in the case block (shadowing
    -- dealt with by the elaborator) so we can just assume the top level names
    -- are okay for building the size change
    findCallsCase cases guarded n args pvs pargs
        = case lookupDefExact n (tt_ctxt ist) of
             Just (CaseOp _ _ _ pats _ cd) ->
                  concatMap (fccPat cases pvs pargs args guarded) (rights pats)
             Nothing -> []
  
    fccPat cases pvs pargs args g (lhs, rhs)
        = let lhs' = delazy lhs
              rhs' = delazy rhs
              (_, pargs_case) = unApply (dePat lhs')
              -- pargs is a pair of a term, and the argument position that
              -- term appears in. If any of the arguments to the case block
              -- are also on the lhs, we also want those patterns to appear
              -- in the parg list so that we'll spot patterns which are
              -- smaller than then
              newpargs = newPArg args pargs
              -- Now need to update the rhs of the case with the names in the
              -- outer definition: In rhs', wherever we see what's in pargs_case,
              -- replace it with the corresponding thing in pargs
              csubs = zip pargs_case args
              newrhs = doCaseSubs csubs (dePat rhs')
              pargs' = pargs ++ addPArg newpargs pargs_case in
                 findCalls cases g newrhs pvs pargs'
      where
        doCaseSubs [] tm = tm
        doCaseSubs ((x, x') : cs) tm
             = doCaseSubs (subIn x x' cs) (substTerm x x' tm)
  
        subIn x x' [] = []
        subIn x x' ((l, r) : cs)
            = (substTerm x x' l, substTerm x x' r) : subIn x x' cs
  
    addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'
    addPArg (Nothing : ts) (t' : ts') = addPArg ts ts'
    addPArg _ _ = []
  
    newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]
    newPArg (t : ts) pargs = case lookup t pargs of
                                  Just i -> Just (t, i) : newPArg ts pargs
                                  Nothing -> Nothing : newPArg ts pargs
    newPArg [] pargs = []
  
    expandToArity n args
       = case lookupTy n (tt_ctxt ist) of
              [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
              _ -> args
       where expand i (Bind n (Pi _ _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
             expand i (Bind n (Pi _ _ _ _) sc) [] = Nothing : expand (i + 1) sc []
             expand i _ xs = xs
  
    mkChange n args pargs = [(n, expandToArity n (sizes args))]
      where
        sizes [] = []
        sizes (a : as) = checkSize a pargs : sizes as
  
        -- find which argument in pargs <a> is smaller than, if any
        checkSize a ((p, i) : ps)
            | a == p = Just (i, Same)
            | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
              as == txt "assert_smaller" && arg == p
                    = Just (i, Smaller)
            | smaller Nothing a (p, Nothing) = Just (i, Smaller)
            | otherwise = checkSize a ps
        checkSize a [] = Nothing
  
        -- Can't be smaller than an erased thing (need to be careful here
        -- because Erased equals everything)
        smaller _ _ (Erased, _) = False -- never smaller than an erased thing
        -- If a == t, and we're under a cosntructor, we've found something
        -- smaller
        smaller (Just tyn) a (t, Just tyt) | a == t = True
        smaller ty a (ap@(App _ f s), _)
            -- Nothing can be smaller than a delayed infinite thing...
            | (P (DCon _ _ _) (UN d) _, [P _ (UN reason) _, _, _]) <- unApply ap,
              d == txt "Delay" && reason == txt "Infinite"
                 = False
            | (P (DCon _ _ _) n _, args) <- unApply ap
                 = let tyn = getType n in
                       any (smaller (ty `mplus` Just tyn) a)
                           (zip args (map toJust (getArgTys tyn)))
        -- check higher order recursive arguments
        smaller ty (App _ f s) a = smaller ty f a
        smaller _ _ _ = False
  
        toJust (n, t) = Just t
  
        getType n = case lookupTyExact n (tt_ctxt ist) of
                         Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
  
    dePat (Bind x (PVar _ ty) sc) = dePat (instantiate (P Bound x ty) sc)
    dePat t = t
  
    patvars (Bind x (PVar _ _) sc) = x : patvars sc
    patvars _ = []
  
    allGuarded n ist = case lookupCtxtExact n (idris_flags ist) of
                            Nothing -> False
                            Just fs -> AllGuarded `elem` fs
  
  checkSizeChange :: Name -> Idris Totality
  checkSizeChange n = do
     ist <- getIState
     case lookupCtxt n (idris_callgraph ist) of
         [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
                    logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++
                              "from " ++ show (scg cg) ++ "\n" ++
                              show (length ms) ++ "\n" ++
                              showSep "\n" (map show ms))
                    logCoverage 6 (show cg)
                    -- every multipath must have an infinitely descending
                    -- thread, then the function terminates
                    -- also need to checks functions called are all total
                    -- (Unchecked is okay as we'll spot problems here)
                    let tot = map (checkMP ist n (getArity ist n)) ms
                    logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"
                    logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++
                         (showSep "\n" (map show (zip ms tot)))
                    return (noPartial tot)
         [] -> do logCoverage 5 $ "No paths for " ++ show n
                  return Unchecked
    where getArity ist n
            = case lookupTy n (tt_ctxt ist) of
                   [ty] -> arity (normalise (tt_ctxt ist) [] ty)
                   _ -> error "Can't happen: checkSizeChange.getArity"
  
  type MultiPath = [SCGEntry]
  
  mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
  mkMultiPaths ist path [] = [reverse path]
  mkMultiPaths ist path cg = concatMap extend cg
    where extend (nextf, args)
             | (nextf, args) `inPath` path = [ reverse ((nextf, args) : path) ]
             | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
                 = case lookupCtxt nextf (idris_callgraph ist) of
                      [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
                      _ -> [ reverse ((nextf, args) : path) ]
             | otherwise = [ reverse ((nextf, args) : path) ]
  
          inPath :: SCGEntry -> [SCGEntry] -> Bool
          inPath f [] = False
          inPath f (g : gs) = smallerEq f g || f == g || inPath f gs
  
          smallerEq :: SCGEntry -> SCGEntry -> Bool
          smallerEq (f, args) (g, args')
              = f == g && not (null (filter smallers args))
                       && filter smallers args == filter smallers args'
          smallers (Just (_, Smaller)) = True
          smallers _ = False
  
  -- If any route along the multipath leads to infinite descent, we're fine.
  -- Try a route beginning with every argument.
  --   If we reach a point we've been to before, but with a smaller value,
  --   that means there is an infinitely descending path from that argument.
  
  checkMP :: IState -> Name -> Int -> MultiPath -> Totality
  checkMP ist topfn i mp = if i > 0
                       then let paths = (map (tryPath 0 [] mp) [0..i-1]) in
  --                               trace ("Paths " ++ show paths) $
                                 collapse paths
                       else tryPath 0 [] mp 0
    where
      mkBig (e, d) = (e, 10000)
  
      tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
      tryPath desc path [] _ = Total []
  --     tryPath desc path ((UN "believe_me", _) : _) arg
  --             = Partial BelieveMe
      -- if we get to a constructor, it's fine as long as it's strictly positive
      tryPath desc path ((f, _) : es) arg
          | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
              = case lookupTotalExact f (tt_ctxt ist) of
                     Just (Total _) -> Unchecked -- okay so far
                     Just (Partial _) -> Partial (Other [f])
                     x -> Unchecked -- An error elsewhere, set as Unchecked to make
                                    -- some progress
          | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
              = Total []
      tryPath desc path (e@(f, args) : es) arg
          | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
          | e `elem` es && allNothing args = Partial (Mutual [f])
      tryPath desc path (e@(f, nextargs) : es) arg
          | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
          | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
          | Just d <- lookup (e, arg) path
              = if desc - d > 0 -- Now lower than when we were last here
                     then -- trace ("Descent " ++ show (desc - d) ++ " "
                          --      ++ show (path, e)) $
                          Total []
                     else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
          | e `elem` map (fst . fst) path
             && not (f `elem` map fst es)
                = Partial (Mutual (map (fst . fst . fst) path ++ [f]))
          | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
              let argspos = zip nextargs [0..]
                  pathres =
                    do (a, pos) <- argspos
                       case a of
                          Nothing -> -- gone up, but if the
                                     -- rest definitely terminates without any
                                     -- cycles (including the path so far, which
                                     -- we take as inaccessible) the path is fine
                              return $ tryPath 0 (map mkBig (((e, arg), desc) : path)) es pos
                          Just (nextarg, sc) ->
                            if nextarg == arg then
                              case sc of
                                Same -> return $ tryPath desc (((e, arg), desc) : path)
                                                         es pos
                                Smaller -> return $ tryPath (desc+1)
                                                            (((e, arg), desc) : path)
                                                            es
                                                            pos
                                _ -> trace ("Shouldn't happen " ++ show e) $
                                        return (Partial Itself)
                              else return Unchecked in
  --                   trace (show (desc, argspos, path, es, pathres)) $
                     collapse pathres
  
          | otherwise = Unchecked
  
  allNothing :: [Maybe a] -> Bool
  allNothing xs = null (collapseNothing (zip xs [0..]))
  
  collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
  collapseNothing ((Nothing, t) : xs)
     = (Nothing, t) : filter (\ (x, _) -> case x of
                                               Nothing -> False
                                               _ -> True) xs
  collapseNothing (x : xs) = x : collapseNothing xs
  collapseNothing [] = []
  
  noPartial :: [Totality] -> Totality
  noPartial (Partial p : xs) = Partial p
  noPartial (_ : xs)         = noPartial xs
  noPartial []               = Total []
  
  collapse :: [Totality] -> Totality
  collapse xs = collapse' Unchecked xs
  collapse' def (Total r : xs)   = Total r
  collapse' def (Unchecked : xs) = collapse' def xs
  collapse' def (d : xs)         = collapse' d xs
  -- collapse' Unchecked []         = Total []
  collapse' def []               = def
  
  -- totalityCheckBlock :: Idris ()
  -- totalityCheckBlock = do
  --          ist <- getIState
  --          -- Do totality checking after entire mutual block
  --          mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n
  --                          ctxt' <- do ctxt <- getContext
  --                                      tclift $ simplifyCasedef n (getErasureInfo ist) ctxt
  --                          setContext ctxt')
  --                  (map snd (idris_totcheck ist))
  --          mapM_ buildSCG (idris_totcheck ist)
  --          mapM_ checkDeclTotality (idris_totcheck ist)
  --          clear_totcheck
  
  