    {-# LANGUAGE ImplicitParams             #-}
    {-# LANGUAGE NondecreasingIndentation   #-}

    {- Checking for Structural recursion
       Authors: Andreas Abel, Nils Anders Danielsson, Ulf Norell,
                  Karl Mehltretter and others
       Created: 2007-05-28
       Source : TypeCheck.Rules.Decl
     -}

    module Agda.Termination.TermCheck
        ( termDecl
        , termMutual
        , Result
        ) where

    import Prelude hiding ( null )

    import Control.Applicative  ( liftA2 )
    import Control.Monad        ( (<=<), filterM, forM, forM_, zipWithM )

    import Data.Foldable (toList)
    import qualified Data.List as List
    import Data.Monoid hiding ((<>))
    import Data.Set (Set)
    import qualified Data.Set as Set

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.Pattern as I
    import Agda.Syntax.Internal.Generic
    import qualified Agda.Syntax.Info as Info
    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Translation.InternalToAbstract (NamedClause(..))

    import Agda.Termination.CutOff
    import Agda.Termination.Monad
    import Agda.Termination.CallGraph hiding (toList)
    import qualified Agda.Termination.CallGraph as CallGraph
    import Agda.Termination.CallMatrix hiding (toList)
    import Agda.Termination.Order     as Order
    import qualified Agda.Termination.SparseMatrix as Matrix
    import Agda.Termination.Termination (Terminates(..), GuardednessHelps(..), endos, idempotent)
    import qualified Agda.Termination.Termination  as Term
    import Agda.Termination.RecCheck

    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Functions
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Forcing
    import Agda.TypeChecking.Records -- (isRecordConstructor, isInductiveRecord)
    import Agda.TypeChecking.Reduce (reduce, normalise, instantiate, instantiateFull, appDefE')
    import Agda.TypeChecking.SizedTypes
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope

    import qualified Agda.Benchmarking as Benchmark
    import Agda.TypeChecking.Monad.Benchmark (billTo, billPureTo)

    import Agda.Interaction.Options

    import Agda.Utils.Either
    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad -- (mapM', forM', ifM, or2M, and2M)
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import qualified Agda.Utils.SmallSet as SmallSet
    import qualified Agda.Utils.VarSet as VarSet

    import Agda.Utils.Impossible

    -- | Call graph with call info for composed calls.

    type Calls = CallGraph CallPath

    -- | The result of termination checking a module.
    --   Must be a 'Monoid' and have 'Singleton'.

    type Result = [TerminationError]

    -- | Entry point: Termination check a single declaration.
    --
    --   Precondition: 'envMutualBlock' must be set correctly.

    termDecl :: A.Declaration -> TCM Result
    termDecl :: Declaration -> TCM Result
    termDecl Declaration
    d = TCM Result -> TCM Result
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM Result -> TCM Result) -> TCM Result -> TCM Result
    forall a b. (a -> b) -> a -> b
    $ Declaration -> TCM Result
    termDecl' Declaration
    d

    -- | Termination check a single declaration
    --   (without necessarily ignoring @abstract@).

    termDecl' :: A.Declaration -> TCM Result
    termDecl' :: Declaration -> TCM Result
    termDecl' = \case
        A.Axiom {}            -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Field {}            -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Primitive {}        -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Mutual MutualInfo
    i [Declaration]
    ds         -> [QName] -> TCM Result
    termMutual ([QName] -> TCM Result) -> [QName] -> TCM Result
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [QName]
    getNames [Declaration]
    ds
        A.Section Range
    _ Erased
    _ ModuleName
    _ GeneralizeTelescope
    _ [Declaration]
    ds  -> [Declaration] -> TCM Result
    forall {t :: * -> *}. Traversable t => t Declaration -> TCM Result
    termDecls [Declaration]
    ds
            -- section structure can be ignored as we are termination checking
            -- definitions lifted to the top-level
        A.Apply {}            -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Import {}           -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Pragma {}           -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Open {}             -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.PatternSynDef {}    -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.UnfoldingDecl{}     -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Generalize {}       -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
            -- open, pattern synonym and generalize defs are just artifacts from the concrete syntax
        A.ScopedDecl ScopeInfo
    scope [Declaration]
    ds -> {- withScope_ scope $ -} [Declaration] -> TCM Result
    forall {t :: * -> *}. Traversable t => t Declaration -> TCM Result
    termDecls [Declaration]
    ds
            -- scope is irrelevant as we are termination checking Syntax.Internal
        A.RecSig{}            -> Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.RecDef DefInfo
    _ QName
    x UniverseCheck
    _ RecordDirectives
    _ DataDefParams
    _ Type
    _ [Declaration]
    ds -> [QName] -> TCM Result
    termMutual [QName
    x] TCM Result -> TCM Result -> TCM Result
    forall a. Semigroup a => a -> a -> a
    <> [Declaration] -> TCM Result
    forall {t :: * -> *}. Traversable t => t Declaration -> TCM Result
    termDecls [Declaration]
    ds
            -- Andreas, 2022-10-23, issue #5823
            -- Also check record types for termination.
            -- They are unfolded during construction of unique inhabitants of eta-records.
        -- These should all be wrapped in mutual blocks:
        A.FunDef{}      -> TCM Result
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.DataSig{}     -> TCM Result
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.DataDef{}     -> TCM Result
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.UnquoteDecl{} -> TCM Result
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.UnquoteDef{}  -> TCM Result
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.UnquoteData{} -> TCM Result
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        termDecls :: t Declaration -> TCM Result
    termDecls t Declaration
    ds = t Result -> Result
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat (t Result -> Result) -> TCMT IO (t Result) -> TCM Result
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> TCM Result) -> t Declaration -> TCMT IO (t Result)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
    mapM Declaration -> TCM Result
    termDecl' t Declaration
    ds

        -- The mutual names mentioned in the abstract syntax
        -- for symbols that need to be termination-checked.
        getNames :: [Declaration] -> [QName]
    getNames = (Declaration -> [QName]) -> [Declaration] -> [QName]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Declaration -> [QName]
    getName
        getName :: Declaration -> [QName]
    getName (A.FunDef DefInfo
    i QName
    x [Clause]
    cs)   = [QName
    x]
        getName (A.RecDef DefInfo
    _ QName
    x UniverseCheck
    _ RecordDirectives
    _ DataDefParams
    _ Type
    _ [Declaration]
    ds)   = QName
    x QName -> [QName] -> [QName]
    forall a. a -> [a] -> [a]
    : [Declaration] -> [QName]
    getNames [Declaration]
    ds
        getName (A.Mutual MutualInfo
    _ [Declaration]
    ds)             = [Declaration] -> [QName]
    getNames [Declaration]
    ds
        getName (A.Section Range
    _ Erased
    _ ModuleName
    _ GeneralizeTelescope
    _ [Declaration]
    ds)      = [Declaration] -> [QName]
    getNames [Declaration]
    ds
        getName (A.ScopedDecl ScopeInfo
    _ [Declaration]
    ds)         = [Declaration] -> [QName]
    getNames [Declaration]
    ds
        getName (A.UnquoteDecl MutualInfo
    _ [DefInfo]
    _ [QName]
    xs Type
    _)    = [QName]
    xs
        getName (A.UnquoteDef [DefInfo]
    _ [QName]
    xs Type
    _)       = [QName]
    xs
        getName Declaration
    _                           = []

    -- | Entry point: Termination check the current mutual block.

    termMutual
      :: [QName]
         -- ^ The function names defined in this block on top-level.
         --   (For error-reporting only.)
      -> TCM Result
    termMutual :: [QName] -> TCM Result
    termMutual [QName]
    names0 = TCMT IO Bool -> TCM Result -> TCM Result -> TCM Result
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (PragmaOptions -> Bool
    optTerminationCheck (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (Result -> TCM Result
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty) (TCM Result -> TCM Result) -> TCM Result -> TCM Result
    forall a b. (a -> b) -> a -> b
    $ {-else-}
     TCM Result -> TCM Result
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM Result -> TCM Result) -> TCM Result -> TCM Result
    forall a b. (a -> b) -> a -> b
    $ do

      -- Get set of mutually defined names from the TCM.
      -- This includes local and auxiliary functions introduced
      -- during type-checking.
      mid <- MutualId -> Maybe MutualId -> MutualId
    forall a. a -> Maybe a -> a
    fromMaybe MutualId
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe MutualId -> MutualId)
    -> TCMT IO (Maybe MutualId) -> TCMT IO MutualId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe MutualId
    envMutualBlock
      mutualBlock <- lookupMutualBlock mid
      let allNames = (QName -> Bool) -> Set QName -> Set QName
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (Bool -> Bool
    not (Bool -> Bool) -> (QName -> Bool) -> QName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Bool
    isAbsurdLambdaName) (Set QName -> Set QName) -> Set QName -> Set QName
    forall a b. (a -> b) -> a -> b
    $
                     MutualBlock -> Set QName
    mutualNames MutualBlock
    mutualBlock
          names    = if [QName] -> Bool
    forall a. Null a => a -> Bool
    null [QName]
    names0 then Set QName
    allNames else [QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList [QName]
    names0
          i        = MutualBlock -> MutualInfo
    mutualInfo MutualBlock
    mutualBlock

      -- We set the range to avoid panics when printing error messages.
      setCurrentRange i $ do

      -- The following debug statement is part of a test case for Issue
      -- #3590.
      reportSLn "term.mutual.id" 40 $
        "Termination checking mutual block " ++ prettyShow mid
      reportSLn "term.mutual" 10 $ "Termination checking " ++ prettyShow allNames

      -- NO_TERMINATION_CHECK
      if (Info.mutualTerminationCheck i `elem` [ NoTerminationCheck, Terminating ]) then do
          reportSLn "term.warn.yes" 10 $ "Skipping termination check for " ++ prettyShow names
          forM_ allNames $ \ QName
    q -> QName -> Bool -> TCMT IO ()
    forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
    setTerminates QName
    q Bool
    True -- considered terminating!
          return mempty
      -- NON_TERMINATING
      else if (Info.mutualTerminationCheck i == NonTerminating) then do
          reportSLn "term.warn.yes" 10 $ "Considering as non-terminating: " ++ prettyShow names
          forM_ allNames $ \ QName
    q -> QName -> Bool -> TCMT IO ()
    forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
    setTerminates QName
    q Bool
    False
          return mempty
      else do
        sccs <- do
          -- Andreas, 2016-10-01 issue #2231
          -- Recursivity checker has to see through abstract definitions!
          ignoreAbstractMode $ do
            billTo [Benchmark.Termination, Benchmark.RecCheck] $ recursive allNames
          -- -- Andreas, 2017-03-24, use positivity info to skip non-recursive functions
          -- skip = ignoreAbstractMode $ forallM allNames $ \ x -> do
          --   null <$> getMutual x
          -- PROBLEMS with test/Succeed/AbstractCoinduction.agda

        -- Trivially terminating (non-recursive)?
        when (null sccs) $
          reportSLn "term.warn.yes" 10 $ "Trivially terminating: " ++ prettyShow names

        -- Actual termination checking needed: go through SCCs.
        concat <$> do
         forM sccs $ \ Set QName
    allNames -> do

         -- Set the mutual names in the termination environment.
         let namesSCC :: Set QName
    namesSCC = (QName -> Bool) -> Set QName -> Set QName
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set QName
    allNames) Set QName
    names
         let setNames :: TerEnv -> TerEnv
    setNames TerEnv
    e = TerEnv
    e
               { terMutual    = allNames
               , terUserNames = namesSCC
               }
             runTerm :: TerM Result -> TCM Result
    runTerm TerM Result
    cont = TerM Result -> TCM Result
    forall a. TerM a -> TCM a
    runTerDefault (TerM Result -> TCM Result) -> TerM Result -> TCM Result
    forall a b. (a -> b) -> a -> b
    $ do
               cutoff <- TerM CutOff
    terGetCutOff
               reportSLn "term.top" 10 $ "Termination checking " ++ prettyShow namesSCC ++
                 " with cutoff=" ++ show cutoff ++ "..."
               terLocal setNames cont

         -- New check currently only makes a difference for copatterns and record types.
         -- Since it is slow, only invoke it if
         -- any of the definitions uses copatterns or is a record type.
         TCMT IO Bool -> TCM Result -> TCM Result -> TCM Result
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Set QName -> (QName -> TCMT IO Bool) -> TCMT IO Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Foldable f, Monad m) =>
    f a -> (a -> m Bool) -> m Bool
    existsM Set QName
    allNames ((QName -> TCMT IO Bool) -> TCMT IO Bool)
    -> (QName -> TCMT IO Bool) -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ \ QName
    q -> QName -> TCMT IO Bool
    forall (m :: * -> *).
    (HasConstInfo m, HasBuiltins m) =>
    QName -> m Bool
    usesCopatterns QName
    q TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` (Maybe RecordData -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe RecordData -> Bool)
    -> TCMT IO (Maybe RecordData) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    q))
             -- Then: New check, one after another.
             (TerM Result -> TCM Result
    runTerm (TerM Result -> TCM Result) -> TerM Result -> TCM Result
    forall a b. (a -> b) -> a -> b
    $ Set QName -> (QName -> TerM Result) -> TerM Result
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    t a -> (a -> m b) -> m b
    forM' Set QName
    allNames ((QName -> TerM Result) -> TerM Result)
    -> (QName -> TerM Result) -> TerM Result
    forall a b. (a -> b) -> a -> b
    $ QName -> TerM Result
    termFunction)
             -- Else: Old check, all at once.
             (TerM Result -> TCM Result
    runTerm (TerM Result -> TCM Result) -> TerM Result -> TCM Result
    forall a b. (a -> b) -> a -> b
    $ TerM Result
    termMutual')

    -- | Run the termination checker possibly twice and take the best result.
    --   Run it first without extracting descent information from dot patterns.
    --   If this proves termination, we are done.
    --   If this did not manage to prove termination, try with dot patterns.
    --   If this did not manage to prove termination either, return the offending paths.
    --   Otherwise, if the first run proved termination subject to (deactivated) guardedness,
    --   return this result.
    --   Otherwise, return the second result.
    withOrWithoutDotPatterns ::
         (Node -> Bool)
      -> TerM Calls
      -> TerM (Terminates CallPath)
    withOrWithoutDotPatterns :: (Int -> Bool) -> TerM Calls -> TerM (Terminates CallPath)
    withOrWithoutDotPatterns Int -> Bool
    filt TerM Calls
    collect = do
        useGuardedness <- TCMT IO Bool -> TerM Bool
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    guardednessOption
        cutoff <- terGetCutOff
        let ?cutoff = cutoff
        -- Run the continuation @k@ with the result of @m@ unless @m@ already certifies termination.
        let unlessTerminates TerM (Terminates CallPath)
    m Terminates CallPath -> TerM (Terminates CallPath)
    k = TerM (Terminates CallPath)
    m TerM (Terminates CallPath)
    -> (Terminates CallPath -> TerM (Terminates CallPath))
    -> TerM (Terminates CallPath)
    forall a b. TerM a -> (a -> TerM b) -> TerM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Terminates CallPath
    Terminates
                -> Terminates CallPath -> TerM (Terminates CallPath)
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Terminates CallPath
    forall cinfo. Terminates cinfo
    Terminates
              TerminatesNot GuardednessHelps
    GuardednessHelpsYes CallPath
    _ | Bool
    useGuardedness
                -> Terminates CallPath -> TerM (Terminates CallPath)
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Terminates CallPath
    forall cinfo. Terminates cinfo
    Terminates
              Terminates CallPath
    r -> Terminates CallPath -> TerM (Terminates CallPath)
    k Terminates CallPath
    r

        -- First try to termination check ignoring the dot patterns
        calls1 <- terSetUseDotPatterns False collect
        reportCalls "no " calls1
        unlessTerminates (billToTerGraph $ Term.terminatesFilter filt calls1) \ Terminates CallPath
    r1 -> do
          -- Try again, but include the dot patterns this time.
          calls2 <- Bool -> TerM Calls -> TerM Calls
    forall a. Bool -> TerM a -> TerM a
    terSetUseDotPatterns Bool
    True TerM Calls
    collect
          reportCalls "" calls2
          unlessTerminates (billToTerGraph $ Term.terminatesFilter filt calls2) \ Terminates CallPath
    r2 -> do
            case Terminates CallPath
    r1 of
              TerminatesNot GuardednessHelps
    GuardednessHelpsNot CallPath
    _ -> Terminates CallPath -> TerM (Terminates CallPath)
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Terminates CallPath
    r2
                -- We might terminate with guardedness and dot patterns (r2).
              Terminates CallPath
    _              -> Terminates CallPath -> TerM (Terminates CallPath)
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Terminates CallPath
    r1
                -- Since r2 did not certify termination, the simpler r1 is preferable.

    -- | @termMutual'@ checks all names of the current mutual block,
    --   henceforth called @allNames@, for termination.
    --
    --   @allNames@ is taken from 'Internal' syntax, it contains also
    --   the definitions created by the type checker (e.g., with-functions).

    termMutual' :: TerM Result
    termMutual' :: TerM Result
    termMutual' = do

      -- collect all recursive calls in the block
      allNames <- TerM (Set QName)
    terGetMutual
      let collect :: TerM Calls
          collect = Set QName -> (QName -> TerM Calls) -> TerM Calls
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    t a -> (a -> m b) -> m b
    forM' Set QName
    allNames QName -> TerM Calls
    termDef

      r <- withOrWithoutDotPatterns (const True) collect

      -- @names@ is taken from the 'Abstract' syntax, so it contains only
      -- the names the user has declared.  This is for error reporting.
      names <- terGetUserNames
      case r of

        TerminatesNot GuardednessHelps
    guardednessHelps CallPath
    calls -> do
          (QName -> TerM ()) -> Set QName -> TerM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (QName -> Bool -> TerM ()
    forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
    `setTerminates` Bool
    False) Set QName
    allNames
          Result -> TerM Result
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Result -> TerM Result) -> Result -> TerM Result
    forall a b. (a -> b) -> a -> b
    $ TerminationError -> Result
    forall el coll. Singleton el coll => el -> coll
    singleton (TerminationError -> Result) -> TerminationError -> Result
    forall a b. (a -> b) -> a -> b
    $ Set QName -> CallPath -> GuardednessHelps -> TerminationError
    terminationError Set QName
    names CallPath
    calls GuardednessHelps
    guardednessHelps

        Terminates CallPath
    Terminates -> do
          TCMT IO () -> TerM ()
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.warn.yes" Int
    2 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            Set QName -> String
    forall a. Pretty a => a -> String
    prettyShow (Set QName
    names) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " does termination check"
          (QName -> TerM ()) -> Set QName -> TerM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (QName -> Bool -> TerM ()
    forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
    `setTerminates` Bool
    True) Set QName
    allNames
          Result -> TerM Result
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty

    -- | Smart constructor for 'TerminationError'.
    --   Removes 'termErrFunctions' that are not mentioned in 'termErrCalls'.
    terminationError :: Set QName -> CallPath -> GuardednessHelps -> TerminationError
    terminationError :: Set QName -> CallPath -> GuardednessHelps -> TerminationError
    terminationError Set QName
    names CallPath
    calls GuardednessHelps
    guardednessHelps = [QName] -> [CallInfo] -> GuardednessHelps -> TerminationError
    TerminationError [QName]
    names' [CallInfo]
    calls' GuardednessHelps
    guardednessHelps
      where
      calls' :: [CallInfo]
    calls'    = CallPath -> [CallInfo]
    callInfos CallPath
    calls
      mentioned :: [QName]
    mentioned = (CallInfo -> QName) -> [CallInfo] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map CallInfo -> QName
    callInfoTarget [CallInfo]
    calls'
      names' :: [QName]
    names'    = (QName -> Bool) -> [QName] -> [QName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ([QName] -> QName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem [QName]
    mentioned) ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ Set QName -> [QName]
    forall a. Set a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList Set QName
    names

    billToTerGraph :: a -> TerM a
    billToTerGraph :: forall a. a -> TerM a
    billToTerGraph a
    a = TCM a -> TerM a
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM a -> TerM a) -> TCM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ Account (BenchPhase (TCMT IO)) -> a -> TCM a
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> c -> m c
    billPureTo [BenchPhase (TCMT IO)
    Phase
    Benchmark.Termination, BenchPhase (TCMT IO)
    Phase
    Benchmark.Graph] a
    a

    -- | @reportCalls@ for debug printing.
    --
    --   Replays the call graph completion for debugging.

    reportCalls :: String -> Calls -> TerM ()
    reportCalls :: String -> Calls -> TerM ()
    reportCalls String
    no Calls
    calls = do
      cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = cutoff

      -- We work in TCM exclusively.
      liftTCM $ do

        reportS "term.lex" 20
          [ "Calls (" ++ no ++ "dot patterns): " ++ prettyShow calls
          ]

        -- Print the whole completion phase.
        verboseS "term.matrices" 40 $ do
          let header String
    s = [String] -> String
    unlines
                [ Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    n Char
    '='
                , Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    k Char
    '=' String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    k' Char
    '='
                , Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    n Char
    '='
                ]
                where n :: Int
    n  = Int
    70
                      r :: Int
    r  = Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    s
                      k :: Int
    k  = Int
    r Int -> Int -> Int
    forall a. Integral a => a -> a -> a
    `div` Int
    2
                      k' :: Int
    k' = Int
    r Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    k
          let report String
    s a
    cs = String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.matrices" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                [ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text   (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String -> String
    header String
    s
                , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ a -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty a
    cs
                ]
              cs0     = Calls
    calls
              step Calls
    cs = do
                let (Calls
    new, Calls
    cs') = Calls -> Calls -> (Calls, Calls)
    forall cinfo.
    (?cutoff::CutOff, Monoid cinfo) =>
    CallGraph cinfo
    -> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)
    completionStep Calls
    cs0 Calls
    cs
                String -> Calls -> TCMT IO ()
    forall {m :: * -> *} {a}.
    (MonadDebug m, Pretty a) =>
    String -> a -> m ()
    report String
    " New call matrices " Calls
    new
                Either () Calls -> TCMT IO (Either () Calls)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either () Calls -> TCMT IO (Either () Calls))
    -> Either () Calls -> TCMT IO (Either () Calls)
    forall a b. (a -> b) -> a -> b
    $ if Calls -> Bool
    forall a. Null a => a -> Bool
    null Calls
    new then () -> Either () Calls
    forall a b. a -> Either a b
    Left () else Calls -> Either () Calls
    forall a b. b -> Either a b
    Right Calls
    cs'
          report " Initial call matrices " cs0
          trampolineM step cs0

        -- Print the result of completion.
        let calls' = Calls -> Calls
    forall cinfo.
    (?cutoff::CutOff, Monoid cinfo) =>
    CallGraph cinfo -> CallGraph cinfo
    CallGraph.complete Calls
    calls
            idems = (CallMatrixAug CallPath -> Bool)
    -> [CallMatrixAug CallPath] -> [CallMatrixAug CallPath]
    forall a. (a -> Bool) -> [a] -> [a]
    filter CallMatrixAug CallPath -> Bool
    forall cinfo. (?cutoff::CutOff) => CallMatrixAug cinfo -> Bool
    idempotent ([CallMatrixAug CallPath] -> [CallMatrixAug CallPath])
    -> [CallMatrixAug CallPath] -> [CallMatrixAug CallPath]
    forall a b. (a -> b) -> a -> b
    $ [Call CallPath] -> [CallMatrixAug CallPath]
    forall cinfo. [Call cinfo] -> [CallMatrixAug cinfo]
    endos ([Call CallPath] -> [CallMatrixAug CallPath])
    -> [Call CallPath] -> [CallMatrixAug CallPath]
    forall a b. (a -> b) -> a -> b
    $ Calls -> [Call CallPath]
    forall cinfo. CallGraph cinfo -> [Call cinfo]
    CallGraph.toList Calls
    calls'
        -- TODO
        -- reportSDoc "term.behaviours" 20 $ vcat
        --   [ text $ "Recursion behaviours (" ++ no ++ "dot patterns):"
        --   , nest 2 $ return $ Term.prettyBehaviour calls'
        --   ]
        reportSDoc "term.matrices" 30 $ vcat
          [ text $ "Idempotent call matrices (" ++ no ++ "dot patterns):\n"
          , nest 2 $ vcat $ punctuate "\n" $ map pretty idems
          ]
        -- reportSDoc "term.matrices" 30 $ vcat
        --   [ text $ "Other call matrices (" ++ no ++ "dot patterns):"
        --   , nest 2 $ pretty $ CallGraph.fromList others
        --   ]
        return ()

    -- | @termFunction name@ checks @name@ for termination.
    -- If it passes the termination check it is marked as "terminates" in the signature.

    termFunction :: QName -> TerM Result
    termFunction :: QName -> TerM Result
    termFunction QName
    name = QName -> (Definition -> TerM Result) -> TerM Result
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    name ((Definition -> TerM Result) -> TerM Result)
    -> (Definition -> TerM Result) -> TerM Result
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    def -> do

      -- Function @name@ is henceforth referred to by its @index@
      -- in the list of @allNames@ of the mutual block.

      allNames <- TerM (Set QName)
    terGetMutual
      let index = Int -> Maybe Int -> Int
    forall a. a -> Maybe a -> a
    fromMaybe Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ QName -> Set QName -> Maybe Int
    forall a. Ord a => a -> Set a -> Maybe Int
    Set.lookupIndex QName
    name Set QName
    allNames

      -- Retrieve the target type of the function to check.
      -- #4256: Don't use typeOfConst (which instantiates type with module params), since termination
      -- checking is running in the empty context, but with the current module unchanged.
      target <- case theDef def of
        -- We are termination-checking a record (calls to record will not be guarding):
        Record{} -> Target -> TerM Target
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Target
    TargetRecord
        -- We are termination-checking a definition:
        Defn
    _ -> Type -> TerM (Maybe QName)
    forall (tcm :: * -> *). MonadTCM tcm => Type -> tcm (Maybe QName)
    typeEndsInDef (Definition -> Type
    defType Definition
    def) TerM (Maybe QName) -> (Maybe QName -> Target) -> TerM Target
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
               Just QName
    d  -> QName -> Target
    TargetDef QName
    d
               Maybe QName
    Nothing -> Target
    TargetOther
      reportTarget target
      terSetTarget target $ do

        -- Collect the recursive calls in the block which (transitively)
        -- involve @name@,
        -- taking the target of @name@ into account for computing guardedness.

        let collect = (((Set Int, Set Int, Calls)
     -> TerM (Either Calls (Set Int, Set Int, Calls)))
    -> (Set Int, Set Int, Calls) -> TerM Calls
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m (Either b a)) -> a -> m b
    `trampolineM` (Int -> Set Int
    forall a. a -> Set a
    Set.singleton Int
    index, Set Int
    forall a. Monoid a => a
    mempty, Calls
    forall a. Monoid a => a
    mempty)) (((Set Int, Set Int, Calls)
      -> TerM (Either Calls (Set Int, Set Int, Calls)))
     -> TerM Calls)
    -> ((Set Int, Set Int, Calls)
        -> TerM (Either Calls (Set Int, Set Int, Calls)))
    -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ \ (Set Int
    todo, Set Int
    done, Calls
    calls) -> do
              if Set Int -> Bool
    forall a. Null a => a -> Bool
    null Set Int
    todo then Either Calls (Set Int, Set Int, Calls)
    -> TerM (Either Calls (Set Int, Set Int, Calls))
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Calls (Set Int, Set Int, Calls)
     -> TerM (Either Calls (Set Int, Set Int, Calls)))
    -> Either Calls (Set Int, Set Int, Calls)
    -> TerM (Either Calls (Set Int, Set Int, Calls))
    forall a b. (a -> b) -> a -> b
    $ Calls -> Either Calls (Set Int, Set Int, Calls)
    forall a b. a -> Either a b
    Left Calls
    calls else do
                -- Extract calls originating from indices in @todo@.
                new <- Set Int -> (Int -> TerM Calls) -> TerM Calls
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    t a -> (a -> m b) -> m b
    forM' Set Int
    todo ((Int -> TerM Calls) -> TerM Calls)
    -> (Int -> TerM Calls) -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ \ Int
    i ->
                  QName -> TerM Calls
    termDef (QName -> TerM Calls) -> QName -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $
                  if Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0 Bool -> Bool -> Bool
    || Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Set QName -> Int
    forall a. Set a -> Int
    Set.size Set QName
    allNames
                  then QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  else Int -> Set QName -> QName
    forall a. Int -> Set a -> a
    Set.elemAt Int
    i Set QName
    allNames
                -- Mark those functions as processed and add the calls to the result.
                let done'  = Set Int
    done Set Int -> Set Int -> Set Int
    forall a. Monoid a => a -> a -> a
    `mappend` Set Int
    todo
                    calls' = Calls
    new  Calls -> Calls -> Calls
    forall a. Monoid a => a -> a -> a
    `mappend` Calls
    calls
                -- Compute the new todo list:
                    todo' = Calls -> Set Int
    forall cinfo. CallGraph cinfo -> Set Int
    CallGraph.targetNodes Calls
    new Set Int -> Set Int -> Set Int
    forall a. Ord a => Set a -> Set a -> Set a
    Set.\\ Set Int
    done'
                -- Jump the trampoline.
                return $ Right (todo', done', calls')

        r <- withOrWithoutDotPatterns (== index) collect

        names <- terGetUserNames
        case r of

          TerminatesNot GuardednessHelps
    guardednessHelps CallPath
    callpaths -> do
            let calls :: [CallInfo]
    calls = CallPath -> [CallInfo]
    callInfos CallPath
    callpaths
            -- Mark as non-terminating.
            QName -> Bool -> TerM ()
    forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
    setTerminates QName
    name Bool
    False

            -- Functions must be terminating, records types need not...
            case Definition -> Defn
    theDef Definition
    def of

              -- Records need not terminate, so we just put the error on the debug log.
              Record{} -> do
                String -> Int -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.warn.no" Int
    10 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
                  [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep [ TCMT IO Doc
    "Record type", QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    name, TCMT IO Doc
    "does not termination check.", TCMT IO Doc
    "Problematic calls:" ] TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    :
                  (CallInfo -> TCMT IO Doc) -> [CallInfo] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc)
    -> (CallInfo -> TCMT IO Doc) -> CallInfo -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallInfo -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => CallInfo -> m Doc
    prettyTCM) ((CallInfo -> Range) -> [CallInfo] -> [CallInfo]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    List.sortOn CallInfo -> Range
    forall a. HasRange a => a -> Range
    getRange [CallInfo]
    calls)
                TerM Result
    forall a. Monoid a => a
    mempty

              -- Functions must terminate, so we report the error.
              Defn
    _ -> do
                let err :: TerminationError
    err = [QName] -> [CallInfo] -> GuardednessHelps -> TerminationError
    TerminationError [QName
    name | QName
    name QName -> Set QName -> Bool
    forall a. Eq a => a -> Set a -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` Set QName
    names] [CallInfo]
    calls GuardednessHelps
    guardednessHelps
                Result -> TerM Result
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Result -> TerM Result) -> Result -> TerM Result
    forall a b. (a -> b) -> a -> b
    $ TerminationError -> Result
    forall el coll. Singleton el coll => el -> coll
    singleton TerminationError
    err

          Terminates CallPath
    Terminates -> do
            String -> Int -> String -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.warn.yes" Int
    2 (String -> TerM ()) -> String -> TerM ()
    forall a b. (a -> b) -> a -> b
    $
              QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    name String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " does termination check"
            QName -> Bool -> TerM ()
    forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
    setTerminates QName
    name Bool
    True
            Result -> TerM Result
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
       where
         reportTarget :: MonadDebug m => Target -> m ()
         reportTarget :: forall (m :: * -> *). MonadDebug m => Target -> m ()
    reportTarget Target
    tgt = String -> Int -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.target" Int
    20 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ (String
    "  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $
           case Target
    tgt of
             Target
    TargetRecord -> String
    "termination checking a record type"
             TargetDef QName
    q  -> [String] -> String
    unwords [ String
    "target type ends in", QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q ]
             Target
    TargetOther  -> String
    "target type not recognized"

    -- | To process the target type.
    typeEndsInDef :: MonadTCM tcm => Type -> tcm (Maybe QName)
    typeEndsInDef :: forall (tcm :: * -> *). MonadTCM tcm => Type -> tcm (Maybe QName)
    typeEndsInDef Type
    t = TCM (Maybe QName) -> tcm (Maybe QName)
    forall a. TCM a -> tcm a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Maybe QName) -> tcm (Maybe QName))
    -> TCM (Maybe QName) -> tcm (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ do
      TelV _ core <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
      case unEl core of
        Def QName
    d Elims
    vs -> Maybe QName -> TCM (Maybe QName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe QName -> TCM (Maybe QName))
    -> Maybe QName -> TCM (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    d
        Term
    _        -> Maybe QName -> TCM (Maybe QName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing

    -- | Termination check a definition by pattern matching.
    --
    --   TODO: Refactor!
    --   As this function may be called twice,
    --   once disregarding dot patterns,
    --   the second time regarding dot patterns,
    --   it is better if we separated bare call extraction
    --   from computing the change in structural order.
    --   Only the latter depends on the choice whether we
    --   consider dot patterns or not.
    termDef :: QName -> TerM Calls
    termDef :: QName -> TerM Calls
    termDef QName
    name = QName -> TerM Calls -> TerM Calls
    forall a. QName -> TerM a -> TerM a
    terSetCurrent QName
    name (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> TerM Calls) -> TerM Calls
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    name ((Definition -> TerM Calls) -> TerM Calls)
    -> (Definition -> TerM Calls) -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    def -> do

     -- Skip calls to record types unless we are checking a record type in the first place.
     let isRecord_ :: Bool
    isRecord_ = case Definition -> Defn
    theDef Definition
    def of { Record{} -> Bool
    True; Defn
    _ -> Bool
    False }
     let notTargetRecord :: TerM Bool
    notTargetRecord = TerM Target
    terGetTarget TerM Target -> (Target -> Bool) -> TerM Bool
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
           Target
    TargetRecord -> Bool
    False
           Target
    _ -> Bool
    True
     TerM Bool -> TerM Calls -> TerM Calls -> TerM Calls
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Bool -> TerM Bool
    forall a. a -> TerM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    isRecord_ TerM Bool -> TerM Bool -> TerM Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` TerM Bool
    notTargetRecord) TerM Calls
    forall a. Monoid a => a
    mempty {-else-} (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ do

      -- Retrieve definition
      let t :: Type
    t = Definition -> Type
    defType Definition
    def

      TCMT IO () -> TerM ()
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.def.fun" Int
    5 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "termination checking type of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    name
            , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
            ]

      Type -> TerM Calls
    termType Type
    t TerM Calls -> TerM Calls -> TerM Calls
    forall a. Monoid a => a -> a -> a
    `mappend` do

      TCMT IO () -> TerM ()
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.def.fun" Int
    5 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "termination checking body of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    name
            , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
            ]

      -- If --without-K, we disregard all arguments (and result)
      -- which are not of data or record type.

      withoutKEnabled <- TCMT IO Bool -> TerM Bool
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    withoutKOption
      applyWhen withoutKEnabled (setMasks t) $ do

        -- If the result should be disregarded, set all calls to unguarded.
        applyWhenM terGetMaskResult terUnguarded $ do

          case theDef def of
            Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cls  } -> [Clause] -> (Clause -> TerM Calls) -> TerM Calls
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    t a -> (a -> m b) -> m b
    forM' [Clause]
    cls ((Clause -> TerM Calls) -> TerM Calls)
    -> (Clause -> TerM Calls) -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ \ Clause
    cl -> do
              if NAPs -> Bool
    hasDefP (Clause -> NAPs
    namedClausePats Clause
    cl) -- generated hcomp clause, should be safe.
                                              -- TODO find proper strategy.
                then Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
                else Clause -> TerM Calls
    termClause Clause
    cl

            -- @record R pars : Set where field tel@
            -- is treated like function @R pars = tel@.
            Record{ Int
    recPars :: Int
    recPars :: Defn -> Int
    recPars, Telescope
    recTel :: Telescope
    recTel :: Defn -> Telescope
    recTel } -> Int -> Telescope -> TerM Calls
    termRecTel Int
    recPars Telescope
    recTel

            Defn
    _ -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty

    -- | Extract "calls" to the field types from a record constructor telescope.
    -- Does not extract from the parameters, but treats these as the "pattern variables"
    -- (the lhs of the "function").
    termRecTel :: Nat -> Telescope -> TerM Calls
    termRecTel :: Int -> Telescope -> TerM Calls
    termRecTel Int
    npars Telescope
    tel = do
      -- Set up the record parameters like function parameters.
      let ([Dom (String, Type)]
    pars, [Dom (String, Type)]
    fields) = Int
    -> [Dom (String, Type)]
    -> ([Dom (String, Type)], [Dom (String, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    npars ([Dom (String, Type)]
     -> ([Dom (String, Type)], [Dom (String, Type)]))
    -> [Dom (String, Type)]
    -> ([Dom (String, Type)], [Dom (String, Type)])
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel
      [Dom (String, Type)] -> TerM Calls -> TerM Calls
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    [Dom (String, Type)] -> m a -> m a
    addContext [Dom (String, Type)]
    pars (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ do
        ps <- Int -> TerM MaskedDeBruijnPatterns
    forall {f :: * -> *} {p}.
    MonadTCEnv f =>
    p -> f MaskedDeBruijnPatterns
    mkPats Int
    npars
        terSetPatterns ps $ terSetSizeDepth pars $ do
          -- Treat the record fields like the body of a function.
          extract $ telFromList fields
      where
      -- create n variable patterns
      mkPats :: p -> f MaskedDeBruijnPatterns
    mkPats p
    n  = ((Int, Dom Name) -> Masked DeBruijnPattern)
    -> [(Int, Dom Name)] -> MaskedDeBruijnPatterns
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, Dom Name) -> Masked DeBruijnPattern
    forall {a}. Pretty a => (Int, a) -> Masked DeBruijnPattern
    mkPat ([(Int, Dom Name)] -> MaskedDeBruijnPatterns)
    -> f [(Int, Dom Name)] -> f MaskedDeBruijnPatterns
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f [(Int, Dom Name)]
    forall (m :: * -> *). MonadTCEnv m => m [(Int, Dom Name)]
    getContextVars
      mkPat :: (Int, a) -> Masked DeBruijnPattern
    mkPat (Int
    i, a
    x) = DeBruijnPattern -> Masked DeBruijnPattern
    forall a. a -> Masked a
    notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
    -> DeBruijnPattern -> Masked DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ PatternInfo -> DBPatVar -> DeBruijnPattern
    forall x. PatternInfo -> x -> Pattern' x
    VarP PatternInfo
    defaultPatternInfo (DBPatVar -> DeBruijnPattern) -> DBPatVar -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> DBPatVar
    DBPatVar (a -> String
    forall a. Pretty a => a -> String
    prettyShow a
    x) Int
    i

    -- | Collect calls in type signature @f : (x1:A1)...(xn:An) -> B@.
    --   It is treated as if there were the additional function clauses.
    --   @@
    --      f = A1
    --      f x1 = A2
    --      f x1 x2 = A3
    --      ...
    --      f x1 ... xn = B
    --   @@

    termType :: Type -> TerM Calls
    termType :: Type -> TerM Calls
    termType = TerM Calls -> Type -> TerM Calls
    forall a. a -> Type -> a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerM Calls
    forall a. Monoid a => a
    mempty
    -- termType = loop 0  -- Andreas, 2019-04-10 deactivate for backwards-compatibility in 2.6.0 #1556
      where
      loop :: a -> Type -> TerM Calls
    loop a
    n Type
    t = do
        ps <- a -> TerM MaskedDeBruijnPatterns
    forall {f :: * -> *} {p}.
    MonadTCEnv f =>
    p -> f MaskedDeBruijnPatterns
    mkPats a
    n
        reportSDoc "term.type" 60 $ vcat
          [ text $ "termType " ++ show n ++ " with " ++ show (length ps) ++ " patterns"
          , nest 2 $ "looking at type " <+> prettyTCM t
          ]
        tel <- getContextTelescope  -- Andreas, 2018-11-15, issue #3394, forgotten initialization of terSizeDepth
        terSetPatterns ps $ terSetSizeDepth tel $ do
          ifNotPiType t {-then-} extract {-else-} $ \ Dom' Term Type
    dom Abs Type
    absB -> do
            Dom' Term Type -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Dom' Term Type
    dom TerM Calls -> TerM Calls -> TerM Calls
    forall a. Monoid a => a -> a -> a
    `mappend` Dom' Term Type -> Abs Type -> (Type -> TerM Calls) -> TerM Calls
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom' Term Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs Dom' Term Type
    dom Abs Type
    absB (a -> Type -> TerM Calls
    loop (a -> Type -> TerM Calls) -> a -> Type -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $! a
    n a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1)

      -- create n variable patterns
      mkPats :: p -> f MaskedDeBruijnPatterns
    mkPats p
    n  = ((Int, Dom Name) -> Masked DeBruijnPattern)
    -> [(Int, Dom Name)] -> MaskedDeBruijnPatterns
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, Dom Name) -> Masked DeBruijnPattern
    forall {a}. Pretty a => (Int, a) -> Masked DeBruijnPattern
    mkPat ([(Int, Dom Name)] -> MaskedDeBruijnPatterns)
    -> f [(Int, Dom Name)] -> f MaskedDeBruijnPatterns
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f [(Int, Dom Name)]
    forall (m :: * -> *). MonadTCEnv m => m [(Int, Dom Name)]
    getContextVars
      mkPat :: (Int, a) -> Masked DeBruijnPattern
    mkPat (Int
    i, a
    x) = DeBruijnPattern -> Masked DeBruijnPattern
    forall a. a -> Masked a
    notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
    -> DeBruijnPattern -> Masked DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ PatternInfo -> DBPatVar -> DeBruijnPattern
    forall x. PatternInfo -> x -> Pattern' x
    VarP PatternInfo
    defaultPatternInfo (DBPatVar -> DeBruijnPattern) -> DBPatVar -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> DBPatVar
    DBPatVar (a -> String
    forall a. Pretty a => a -> String
    prettyShow a
    x) Int
    i

    -- | Mask arguments and result for termination checking
    --   according to type of function.
    --   Only arguments of types ending in data/record or Size are counted in.
    setMasks :: Type -> TerM a -> TerM a
    setMasks :: forall a. Type -> TerM a -> TerM a
    setMasks Type
    t TerM a
    cont = do
      (ds, d) <- TCM ([Bool], Bool) -> TerM ([Bool], Bool)
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM ([Bool], Bool) -> TerM ([Bool], Bool))
    -> TCM ([Bool], Bool) -> TerM ([Bool], Bool)
    forall a b. (a -> b) -> a -> b
    $ do
        TelV tel core <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
        -- Check argument types
        ds <- checkArgumentTypes tel
        -- Check result types
        d  <- addContext tel $ isNothing <.> isDataOrRecord . unEl $ core
        when d $
          reportSLn "term.mask" 20 $ "result type is not data or record type, ignoring guardedness for --without-K"
        return (ds, d)
      terSetMaskArgs (ds ++ repeat True) $ terSetMaskResult d $ cont

      where
        checkArgumentTypes :: Telescope -> TCM [Bool]
        checkArgumentTypes :: Telescope -> TCM [Bool]
    checkArgumentTypes Telescope
    EmptyTel = [Bool] -> TCM [Bool]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        checkArgumentTypes (ExtendTel Dom' Term Type
    dom Abs Telescope
    atel) = do
          TelV tel2 t <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom' Term Type
    dom
          d <- addContext tel2 $
            (isNothing <$> isDataOrRecord (unEl t)) `or2M` (isJust <$> isSizeType t)
          when d $
            reportSDoc "term.mask" 20 $ do
              "argument type "
                <+> prettyTCM t
                <+> " is not data or record type, ignoring structural descent for --without-K"
          underAbstraction dom atel $ \Telescope
    tel -> (Bool
    dBool -> [Bool] -> [Bool]
    forall a. a -> [a] -> [a]
    :) ([Bool] -> [Bool]) -> TCM [Bool] -> TCM [Bool]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> TCM [Bool]
    checkArgumentTypes Telescope
    tel

    -- | Is the current target type among the given ones?

    targetElem :: [QName] -> TerM Bool
    targetElem :: [QName] -> TerM Bool
    targetElem [QName]
    ds = TerM Target
    terGetTarget TerM Target -> (Target -> Bool) -> TerM Bool
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
      TargetDef QName
    d  -> QName
    d QName -> [QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    ds
      Target
    TargetRecord -> Bool
    False
      Target
    TargetOther  -> Bool
    False

    -- | Convert a term (from a dot pattern) to a DeBruijn pattern.
    --
    --   The term is first normalized and stripped of all non-coinductive projections.

    termToDBP :: Term -> TerM DeBruijnPattern
    termToDBP :: Term -> TerM DeBruijnPattern
    termToDBP Term
    t = TerM Bool
    -> TerM DeBruijnPattern
    -> TerM DeBruijnPattern
    -> TerM DeBruijnPattern
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM TerM Bool
    terGetUseDotPatterns (DeBruijnPattern -> TerM DeBruijnPattern
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    unusedVar) (TerM DeBruijnPattern -> TerM DeBruijnPattern)
    -> TerM DeBruijnPattern -> TerM DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ {- else -} do
      Term -> TerM DeBruijnPattern
    forall a b. TermToPattern a b => a -> TerM b
    termToPattern (Term -> TerM DeBruijnPattern) -> TerM Term -> TerM DeBruijnPattern
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do TCM Term -> TerM Term
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Term -> TerM Term) -> TCM Term -> TerM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> TCM Term
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections (Term -> TCM Term) -> TCM Term -> TCM Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> TCM Term
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise Term
    t

    -- | Convert a term (from a dot pattern) to a pattern for the purposes of the termination checker.
    --
    --   @SIZESUC@ is treated as a constructor.

    class TermToPattern a b where
      termToPattern :: a -> TerM b

      default termToPattern :: (TermToPattern a' b', Traversable f, a ~ f a', b ~ f b') => a -> TerM b
      termToPattern = (a' -> TerM b') -> f a' -> TerM (f b')
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> f a -> f (f b)
    traverse a' -> TerM b'
    forall a b. TermToPattern a b => a -> TerM b
    termToPattern

    instance TermToPattern a b => TermToPattern [a] [b] where
    instance TermToPattern a b => TermToPattern (Arg a) (Arg b) where
    instance TermToPattern a b => TermToPattern (Named c a) (Named c b) where

    -- OVERLAPPING
    -- instance TermToPattern a b => TermToPattern a (Named c b) where
    --   termToPattern t = unnamed <$> termToPattern t

    instance TermToPattern Term DeBruijnPattern where
      termToPattern :: Term -> TerM DeBruijnPattern
    termToPattern Term
    t = TCM Term -> TerM Term
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (Term -> TCM Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm Term
    t) TerM Term -> (Term -> TerM DeBruijnPattern) -> TerM DeBruijnPattern
    forall a b. TerM a -> (a -> TerM b) -> TerM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        -- Constructors.
        Con ConHead
    c ConInfo
    _ Elims
    args -> ConHead -> TerM DeBruijnPattern -> TerM DeBruijnPattern
    ifNotConsOfHIT ConHead
    c (TerM DeBruijnPattern -> TerM DeBruijnPattern)
    -> TerM DeBruijnPattern -> TerM DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $
          ConHead -> ConPatternInfo -> NAPs -> DeBruijnPattern
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    noConPatternInfo (NAPs -> DeBruijnPattern)
    -> ([Arg DeBruijnPattern] -> NAPs)
    -> [Arg DeBruijnPattern]
    -> DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg DeBruijnPattern -> Arg (Named_ DeBruijnPattern))
    -> [Arg DeBruijnPattern] -> NAPs
    forall a b. (a -> b) -> [a] -> [b]
    map ((DeBruijnPattern -> Named_ DeBruijnPattern)
    -> Arg DeBruijnPattern -> Arg (Named_ DeBruijnPattern)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DeBruijnPattern -> Named_ DeBruijnPattern
    forall a name. a -> Named name a
    unnamed) ([Arg DeBruijnPattern] -> DeBruijnPattern)
    -> TerM [Arg DeBruijnPattern] -> TerM DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg Term] -> TerM [Arg DeBruijnPattern]
    forall a b. TermToPattern a b => a -> TerM b
    termToPattern ([Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    args)
        Def QName
    s [Apply Arg Term
    arg] -> do
          suc <- TerM (Maybe QName)
    terGetSizeSuc
          if Just s == suc then ConP (ConHead s IsData Inductive []) noConPatternInfo . map (fmap unnamed) <$> termToPattern [arg]
           else fallback
        DontCare Term
    t  -> Term -> TerM DeBruijnPattern
    forall a b. TermToPattern a b => a -> TerM b
    termToPattern Term
    t -- OR: __IMPOSSIBLE__  -- removed by stripAllProjections
        -- Leaves.
        Var Int
    i []    -> DBPatVar -> DeBruijnPattern
    forall a. a -> Pattern' a
    varP (DBPatVar -> DeBruijnPattern)
    -> (Name -> DBPatVar) -> Name -> DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> Int -> DBPatVar
    `DBPatVar` Int
    i) (String -> DBPatVar) -> (Name -> String) -> Name -> DBPatVar
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> DeBruijnPattern) -> TerM Name -> TerM DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TerM Name
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Name
    nameOfBV Int
    i
        Lit Literal
    l       -> DeBruijnPattern -> TerM DeBruijnPattern
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DeBruijnPattern -> TerM DeBruijnPattern)
    -> DeBruijnPattern -> TerM DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ Literal -> DeBruijnPattern
    forall a. Literal -> Pattern' a
    litP Literal
    l
        Dummy String
    s Elims
    _   -> String -> TerM DeBruijnPattern
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ String
    s
        Term
    t           -> TerM DeBruijnPattern
    fallback
        where
        -- Andrea: 22/04/2020.
        -- With cubical we will always have a clause where the dot
        -- patterns are instead replaced with a variable, so they
        -- cannot be relied on for termination.
        -- See issue #4606 for a counterexample involving HITs.
        --
        -- Without the presence of HITs I conjecture that dot patterns
        -- could be turned into actual splits, because no-confusion
        -- would make the other cases impossible, so I do not disable
        -- this for --without-K entirely.
        --
        -- Szumi, 2025-03-11:
        -- Instead of completely turning off dot-pattern termination for cubical,
        -- it should be enough to only ignore constructors of HITs in dot patterns.
        -- This way, the issues #5953 and #4725 are also avoided.
        ifNotConsOfHIT :: ConHead -> TerM DeBruijnPattern -> TerM DeBruijnPattern
    ifNotConsOfHIT ConHead
    c    = TerM Bool
    -> TerM DeBruijnPattern
    -> TerM DeBruijnPattern
    -> TerM DeBruijnPattern
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> TerM Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    consOfHIT (ConHead -> QName
    conName ConHead
    c)) TerM DeBruijnPattern
    fallback
        fallback :: TerM DeBruijnPattern
    fallback            = DeBruijnPattern -> TerM DeBruijnPattern
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DeBruijnPattern -> TerM DeBruijnPattern)
    -> DeBruijnPattern -> TerM DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ Term -> DeBruijnPattern
    forall a. Term -> Pattern' a
    dotP Term
    t

    -- | Masks all non-data/record type patterns if --without-K.
    --   See issue #1023.
    maskNonDataArgs :: [DeBruijnPattern] -> TerM [Masked DeBruijnPattern]
    maskNonDataArgs :: [DeBruijnPattern] -> TerM MaskedDeBruijnPatterns
    maskNonDataArgs [DeBruijnPattern]
    ps = (DeBruijnPattern -> Bool -> Masked DeBruijnPattern)
    -> [DeBruijnPattern] -> [Bool] -> MaskedDeBruijnPatterns
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith DeBruijnPattern -> Bool -> Masked DeBruijnPattern
    forall {x}. Pattern' x -> Bool -> Masked (Pattern' x)
    mask [DeBruijnPattern]
    ps ([Bool] -> MaskedDeBruijnPatterns)
    -> TerM [Bool] -> TerM MaskedDeBruijnPatterns
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TerM [Bool]
    terGetMaskArgs
      where
        mask :: Pattern' x -> Bool -> Masked (Pattern' x)
    mask p :: Pattern' x
    p@ProjP{} Bool
    _ = Bool -> Pattern' x -> Masked (Pattern' x)
    forall a. Bool -> a -> Masked a
    Masked Bool
    False Pattern' x
    p
        mask Pattern' x
    p         Bool
    d = Bool -> Pattern' x -> Masked (Pattern' x)
    forall a. Bool -> a -> Masked a
    Masked Bool
    d     Pattern' x
    p

    -- | Drop elements of the list which correspond to arguments forced by
    -- the constructor with the given QName.
    mapForcedArguments :: QName -> [a] -> (IsForced -> a -> Maybe b) -> TerM [b]
    mapForcedArguments :: forall a b. QName -> [a] -> (IsForced -> a -> Maybe b) -> TerM [b]
    mapForcedArguments QName
    c [a]
    xs IsForced -> a -> Maybe b
    k = do
      forcedArgs <- QName -> TerM [IsForced]
    forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
    getForcedArgs QName
    c
      let go [IsForced]
    xs (a
    p:[a]
    ps) = do
            let (IsForced
    f, [IsForced]
    xs') = [IsForced] -> (IsForced, [IsForced])
    nextIsForced [IsForced]
    xs
            case IsForced -> a -> Maybe b
    k IsForced
    f a
    p of
              Just b
    b  -> b
    bb -> [b] -> [b]
    forall a. a -> [a] -> [a]
    :[IsForced] -> [a] -> [b]
    go [IsForced]
    xs' [a]
    ps
              Maybe b
    Nothing -> [IsForced] -> [a] -> [b]
    go [IsForced]
    xs' [a]
    ps
          go [IsForced]
    _ [] = []
      pure $ go forcedArgs xs

    -- | Extract recursive calls from one clause.
    termClause :: Clause -> TerM Calls
    termClause :: Clause -> TerM Calls
    termClause Clause
    clause = do
      Clause{ clauseTel = tel, namedClausePats = ps, clauseBody = body } <- Clause -> TerM Clause
    forall (tcm :: * -> *). PureTCM tcm => Clause -> tcm Clause
    etaExpandClause Clause
    clause
      liftTCM $ reportSDoc "term.check.clause" 25 $ vcat
        [ "termClause"
        , nest 2 $ "tel =" <+> prettyTCM tel
        , nest 2 $ "ps  =" <+> do addContext tel $ prettyTCMPatternList ps
        ]
      forM' body $ \ Term
    v -> Telescope -> TerM Calls -> TerM Calls
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ do
        -- TODO: combine the following two traversals, avoid full normalisation.
        -- Parse dot patterns as patterns as far as possible.
        ps <- (DeBruijnPattern -> TerM DeBruijnPattern) -> NAPs -> TerM NAPs
    forall a b (m :: * -> *).
    (PatternLike a b, Monad m) =>
    (Pattern' a -> m (Pattern' a)) -> b -> m b
    postTraversePatternM DeBruijnPattern -> TerM DeBruijnPattern
    parseDotP NAPs
    ps
        -- Blank out coconstructors.
        ps <- preTraversePatternM stripCoCon ps
        -- Mask non-data arguments.
        mdbpats <- maskNonDataArgs $ map namedArg ps
        terSetPatterns mdbpats $ do
          terSetSizeDepth tel $ do
            reportBody v
            extract v

      where
        parseDotP :: DeBruijnPattern -> TerM DeBruijnPattern
    parseDotP = \case
          DotP PatternInfo
    o Term
    t -> Term -> TerM DeBruijnPattern
    termToDBP Term
    t
          DeBruijnPattern
    p        -> DeBruijnPattern -> TerM DeBruijnPattern
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    p
        stripCoCon :: DeBruijnPattern -> TerM DeBruijnPattern
    stripCoCon = \case
          ConP (ConHead QName
    c DataOrRecord
    _ Induction
    CoInductive [Arg QName]
    _) ConPatternInfo
    _ NAPs
    _ -> DeBruijnPattern -> TerM DeBruijnPattern
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    unusedVar
          DeBruijnPattern
    p -> DeBruijnPattern -> TerM DeBruijnPattern
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    p
        reportBody :: Term -> TerM ()
        reportBody :: Term -> TerM ()
    reportBody Term
    v = String -> Int -> TerM () -> TerM ()
    forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
    verboseS String
    "term.check.clause" Int
    6 (TerM () -> TerM ()) -> TerM () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ do
          f       <- TerM QName
    terGetCurrent
          pats    <- terGetPatterns
          liftTCM $ reportSDoc "term.check.clause" 6 $ do
            sep [ text ("termination checking clause of")
                    <+> prettyTCM f
                , nest 2 $ "lhs:" <+> sep (map prettyTCM pats)
                , nest 2 $ "rhs:" <+> prettyTCM v
                ]

    -- | Extract recursive calls from expressions.
    class ExtractCalls a where
      extract :: a -> TerM Calls

    instance ExtractCalls a => ExtractCalls (Abs a) where
      extract :: Abs a -> TerM Calls
    extract (NoAbs String
    _ a
    a) = a -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract a
    a
      extract (Abs String
    x a
    a)   = String -> TerM Calls -> TerM Calls
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => String -> m a -> m a
    addContext String
    x (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ TerM Calls -> TerM Calls
    forall a. TerM a -> TerM a
    terRaise (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ a -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract a
    a

    instance ExtractCalls a => ExtractCalls (Arg a) where
      extract :: Arg a -> TerM Calls
    extract = a -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract (a -> TerM Calls) -> (Arg a -> a) -> Arg a -> TerM Calls
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg a -> a
    forall e. Arg e -> e
    unArg

    instance ExtractCalls a => ExtractCalls (Dom a) where
      extract :: Dom a -> TerM Calls
    extract = a -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract (a -> TerM Calls) -> (Dom a -> a) -> Dom a -> TerM Calls
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom a -> a
    forall t e. Dom' t e -> e
    unDom

    instance ExtractCalls a => ExtractCalls (Elim' a) where
      extract :: Elim' a -> TerM Calls
    extract Proj{}    = Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
      extract (Apply Arg a
    a) = a -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract (a -> TerM Calls) -> a -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    a
      extract (IApply a
    x a
    y a
    a) = (a, (a, a)) -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract (a
    x,(a
    y,a
    a)) -- TODO Andrea: conservative

    instance ExtractCalls a => ExtractCalls [a] where
      extract :: [a] -> TerM Calls
    extract = (a -> TerM Calls) -> [a] -> TerM Calls
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    (a -> m b) -> t a -> m b
    mapM' a -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract

    instance (ExtractCalls a, ExtractCalls b) => ExtractCalls (a,b) where
      extract :: (a, b) -> TerM Calls
    extract (a
    a, b
    b) = Calls -> Calls -> Calls
    forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
    CallGraph.union (Calls -> Calls -> Calls) -> TerM Calls -> TerM (Calls -> Calls)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract a
    a TerM (Calls -> Calls) -> TerM Calls -> TerM Calls
    forall a b. TerM (a -> b) -> TerM a -> TerM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract b
    b

    instance (ExtractCalls a, ExtractCalls b, ExtractCalls c) => ExtractCalls (a,b,c) where
      extract :: (a, b, c) -> TerM Calls
    extract (a
    a, b
    b, c
    c) = (a, (b, c)) -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract (a
    a, (b
    b, c
    c))

    -- | Sorts can contain arbitrary terms of type @Level@,
    --   so look for recursive calls also in sorts.
    --   Ideally, 'Sort' would not be its own datatype but just
    --   a subgrammar of 'Term', then we would not need this boilerplate.

    instance ExtractCalls Sort where
      extract :: Sort -> TerM Calls
    extract Sort
    s = do
        TCMT IO () -> TerM ()
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ do
          String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.sort" Int
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "extracting calls from sort" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Sort -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Sort -> m Doc
    prettyTCM Sort
    s
          String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.sort" Int
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String
    "s = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Sort -> String
    forall a. Show a => a -> String
    show Sort
    s)
        case Sort
    s of
          Inf Univ
    _ Integer
    _    -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          Sort
    SizeUniv   -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          Sort
    LockUniv   -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          Sort
    LevelUniv  -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          Sort
    IntervalUniv -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          Univ Univ
    _ Level' Term
    t       -> TerM Calls -> TerM Calls
    forall a. TerM a -> TerM a
    terUnguarded (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ Level' Term -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Level' Term
    t  -- no guarded levels
          PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> (Dom' Term Term, Sort, Abs Sort) -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract (Dom' Term Term
    a, Sort
    s1, Abs Sort
    s2)
          FunSort Sort
    s1 Sort
    s2 -> (Sort, Sort) -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract (Sort
    s1, Sort
    s2)
          UnivSort Sort
    s -> Sort -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Sort
    s
          MetaS MetaId
    x Elims
    es -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          DefS QName
    d Elims
    es  -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          DummyS{}   -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty

    -- | Extract recursive calls from a type.

    instance ExtractCalls Type where
      extract :: Type -> TerM Calls
    extract (El Sort
    s Term
    t) = (Sort, Term) -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract (Sort
    s, Term
    t)

    instance ExtractCalls a => ExtractCalls (Tele a) where
      extract :: Tele a -> TerM Calls
    extract = \case
        Tele a
    EmptyTel        -> TerM Calls
    forall a. Monoid a => a
    mempty
        ExtendTel a
    a Abs (Tele a)
    tel -> a -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract a
    a TerM Calls -> TerM Calls -> TerM Calls
    forall a. Semigroup a => a -> a -> a
    <> Abs (Tele a) -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Abs (Tele a)
    tel

    -- | Extract recursive calls from a constructor application.

    constructor
      :: QName
        -- ^ Constructor name.
      -> Induction
        -- ^ Should the constructor be treated as inductive or coinductive?
      -> [(Arg Term, Bool)]
        -- ^ All the arguments,
        --   and for every argument a boolean which is 'True' iff the
        --   argument should be viewed as preserving guardedness.
      -> TerM Calls
    constructor :: QName -> Induction -> [(Arg Term, Bool)] -> TerM Calls
    constructor QName
    c Induction
    ind [(Arg Term, Bool)]
    args = do
      cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = cutoff
      forM' args $ \ (Arg Term
    arg, Bool
    preserves) -> do
        let g' :: Order -> Order
    g' = case (Bool
    preserves, Induction
    ind) of
                 (Bool
    True,  Induction
    Inductive)   -> Order -> Order
    forall a. a -> a
    id
                 (Bool
    True,  Induction
    CoInductive) -> (Order
    Order.lt (?cutoff::CutOff) => Order -> Order -> Order
    Order -> Order -> Order
    .*.)
                 (Bool
    False, Induction
    _)           -> Order -> Order -> Order
    forall a b. a -> b -> a
    const Order
    Order.unknown
        (Order -> Order) -> TerM Calls -> TerM Calls
    forall a. (Order -> Order) -> TerM a -> TerM a
    terModifyGuarded Order -> Order
    g' (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Arg Term
    arg

    -- | Handles function applications @g es@.

    function :: QName -> Elims -> TerM Calls
    function :: QName -> Elims -> TerM Calls
    function QName
    g Elims
    es0 = do

        f       <- TerM QName
    terGetCurrent
        names   <- terGetMutual
        guarded <- terGetGuarded

        -- let gArgs = Def g es0
        liftTCM $ reportSDoc "term.function" 30 $
          "termination checking function call " <+> prettyTCM (Def g es0)

        -- First, look for calls in the arguments of the call gArgs.

        -- If the function is a projection but not for a coinductive record,
        -- then preserve guardedness for its principal argument.
        isProj <- isProjectionButNotCoinductive g
        let unguards = Order -> [Order]
    forall a. a -> [a]
    repeat Order
    Order.unknown
        let guards = Bool -> ([Order] -> [Order]) -> [Order] -> [Order]
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen Bool
    isProj (Order
    guarded Order -> [Order] -> [Order]
    forall a. a -> [a] -> [a]
    :) [Order]
    unguards
        -- Collect calls in the arguments of this call.
        let args = (Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> [Arg Term]
    forall t. [Elim' t] -> [Arg t]
    argsFromElims Elims
    es0
        calls <- forM' (zip guards args) $ \ (Order
    guard, Term
    a) -> do
          Order -> TerM Calls -> TerM Calls
    forall a. Order -> TerM a -> TerM a
    terSetGuarded Order
    guard (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ Term -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Term
    a

        -- Then, consider call gArgs itself.

        liftTCM $ reportSDoc "term.found.call" 20 $
          sep [ "found call from" <+> prettyTCM f
              , nest 2 $ "to" <+> prettyTCM g
              ]

        -- insert this call into the call list
        case Set.lookupIndex g names of

           -- call leads outside the mutual block and can be ignored
           Maybe Int
    Nothing   -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    calls

           -- call is to one of the mutally recursive functions/record
           Just Int
    gInd -> do
             cutoff <- TerM CutOff
    terGetCutOff
             let ?cutoff = cutoff

             -- Andreas, 2017-02-14, issue #2458:
             -- If we have inlined with-functions, we could be illtyped,
             -- hence, do not reduce anything.
             -- Andreas, 2017-06-20 issue #2613:
             -- We still need to reduce constructors, even when with-inlining happened.
             es <- -- ifM terGetHaveInlinedWith (return es0) {-else-} $
               liftTCM $ forM es0 $
                 -- 2017-09-09, re issue #2732
                 -- The eta-contraction that was here does not seem necessary to make structural order
                 -- comparison not having to worry about eta.
                 -- Maybe we thought an eta redex could come from a meta instantiation.
                 -- However, eta-contraction is already performed by instantiateFull.
                 -- See test/Succeed/Issue2732-termination.agda.
                 traverse reduceCon <=< instantiateFull

               -- 2017-05-16, issue #2403: Argument normalization is too expensive,
               -- even if we only expand non-recursive functions.
               -- Argument normalization TURNED OFF.
               -- liftTCM $ billTo [Benchmark.Termination, Benchmark.Reduce] $ do
               --  -- Andreas, 2017-01-13, issue #2403, normalize arguments for the structural ordering.
               --  -- Andreas, 2017-03-25, issue #2495, restrict this to non-recursive functions
               --  -- otherwise, the termination checking may run forever.
               --  reportSLn "term.reduce" 90 $ "normalizing call arguments"
               --  modifyAllowedReductions (List.\\ [UnconfirmedReductions,RecursiveReductions]) $
               --    forM es0 $ \ e -> do
               --      reportSDoc "term.reduce" 95 $ "normalizing " <+> prettyTCM e
               --      etaContract =<< normalise e

             -- Compute the call matrix.

             -- Andreas, 2014-03-26 only 6% of termination time for library test
             -- spent on call matrix generation
             (nrows, ncols, matrix) <- billTo [Benchmark.Termination, Benchmark.Compare] $
               compareArgs es

             -- Andreas, 2022-03-21, #5823:
             -- If we are "calling" a record type we are guarded unless the origin
             -- of the termination analysis is itself a record.
             -- This is because we usually do not "unfold" record types into their
             -- field telescope.  We only do so when trying to construct the
             -- unique inhabitant of record type (singleton analysis).
             -- In the latter case, a call to a record type is not guarding.
             guarded' <- isRecord g >>= \case
               Just{} -> TerM Target
    terGetTarget TerM Target -> (Target -> TerM Order) -> TerM Order
    forall a b. TerM a -> (a -> TerM b) -> TerM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                 Target
    TargetRecord
                   -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    guarded
                 Target
    _ -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Order
    guarded (?cutoff::CutOff) => Order -> Order -> Order
    Order -> Order -> Order
    .*. Order
    Order.lt)
                        -- guarding when we call a record and not termination checking a record
               Maybe RecordData
    Nothing
                 -- only a delayed definition can be guarded
                 | Order -> Bool
    Order.decreasing Order
    guarded
                   -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le
                 | Bool
    otherwise
                   -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    guarded
             liftTCM $ reportSLn "term.guardedness" 20 $
               "composing with guardedness " ++ prettyShow guarded ++
               " counting as " ++ prettyShow guarded'
             let matrix' = (?cutoff::CutOff) => Order -> [[Order]] -> [[Order]]
    Order -> [[Order]] -> [[Order]]
    composeGuardedness Order
    guarded' [[Order]]
    matrix

             -- Andreas, 2013-04-26 FORBIDDINGLY expensive!
             -- This PrettyTCM QName cost 50% of the termination time for std-lib!!
             -- gPretty <-liftTCM $ billTo [Benchmark.Termination, Benchmark.Level] $
             --   render <$> prettyTCM g

             -- Andreas, 2013-05-19 as pointed out by Andrea Vezzosi,
             -- printing the call eagerly is forbiddingly expensive.
             -- So we build a closure such that we can print the call
             -- whenever we really need to.
             -- This saves 30s (12%) on the std-lib!
             -- Andreas, 2015-01-21 Issue 1410: Go to the module where g is defined
             -- otherwise its free variables with be prepended to the call
             -- in the error message.
             doc <- liftTCM $ withCurrentModule (qnameModule g) $ buildClosure $
               Def g $ List.dropWhileEnd ((Inserted ==) . getOrigin) es0
               -- Andreas, 2018-07-22, issue #3136
               -- Dropping only inserted arguments at the end, since
               -- dropping arguments in the middle might make the printer crash.
               -- Def g $ filter ((/= Inserted) . getOrigin) es0
               -- Andreas, 2017-01-05, issue #2376
               -- Remove arguments inserted by etaExpandClause.

             let src  = Int -> Maybe Int -> Int
    forall a. a -> Maybe a -> a
    fromMaybe Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ QName -> Set QName -> Maybe Int
    forall a. Ord a => a -> Set a -> Maybe Int
    Set.lookupIndex QName
    f Set QName
    names
                 tgt  = Int
    gInd
                 cm   = Int -> Int -> [[Order]] -> CallMatrix
    makeCM Int
    ncols Int
    nrows [[Order]]
    matrix'
                 info = DList CallInfo -> CallPath
    CallPath (DList CallInfo -> CallPath) -> DList CallInfo -> CallPath
    forall a b. (a -> b) -> a -> b
    $ CallInfo -> DList CallInfo
    forall el coll. Singleton el coll => el -> coll
    singleton (CallInfo -> DList CallInfo) -> CallInfo -> DList CallInfo
    forall a b. (a -> b) -> a -> b
    $
                        CallInfo
                          { callInfoTarget :: QName
    callInfoTarget = QName
    g
                          , callInfoCall :: Closure Term
    callInfoCall   = Closure Term
    doc
                          }
             verboseS "term.kept.call" 5 $ do
               pats <- terGetPatterns
               reportSDoc "term.kept.call" 5 $ vcat
                 [ "kept call from" <+> text (prettyShow f) <+> hsep (map prettyTCM pats)
                 , nest 2 $ "to" <+> text (prettyShow g) <+>
                             hsep (map (parens . prettyTCM) args)
                 , nest 2 $ "call matrix (with guardedness): "
                 , nest 2 $ pretty cm
                 ]
             return $ CallGraph.insert src tgt cm info calls

      where
        -- We have to reduce constructors in case they're reexported.
        -- Andreas, Issue 1530: constructors have to be reduced deep inside terms,
        -- thus, we need to use traverseTermM.
        reduceCon :: Term -> TCM Term
        reduceCon :: Term -> TCM Term
    reduceCon = (Term -> TCM Term) -> Term -> TCM Term
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    forall (m :: * -> *). Monad m => (Term -> m Term) -> Term -> m Term
    traverseTermM ((Term -> TCM Term) -> Term -> TCM Term)
    -> (Term -> TCM Term) -> Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ \case
          Con ConHead
    c ConInfo
    ci Elims
    vs -> (Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    vs) (Term -> Term) -> TCM Term -> TCM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCM Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci [])  -- make sure we don't reduce the arguments
          Term
    t -> Term -> TCM Term
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    t

    -- | Try to get rid of a function call targeting the current SCC
    --   using a non-recursive clause.
    --
    --   This can help copattern definitions of dependent records.
    tryReduceNonRecursiveClause
      :: QName                 -- ^ Function
      -> Elims                 -- ^ Arguments
      -> (Term -> TerM Calls)  -- ^ Continue here if we managed to reduce.
      -> TerM Calls            -- ^ Otherwise, continue here.
      -> TerM Calls
    tryReduceNonRecursiveClause :: QName -> Elims -> (Term -> TerM Calls) -> TerM Calls -> TerM Calls
    tryReduceNonRecursiveClause QName
    g Elims
    es Term -> TerM Calls
    continue TerM Calls
    fallback = do
      -- Andreas, 2020-02-06, re: issue #906
      let v0 :: Term
    v0 = QName -> Elims -> Term
    Def QName
    g Elims
    es
      String -> Int -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.reduce" Int
    40 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Trying to reduce away call: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v0

      -- First, make sure the function is in the current SCC.
      TerM Bool -> TerM Calls -> TerM Calls -> TerM Calls
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> Set QName -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    notElem QName
    g (Set QName -> Bool) -> TerM (Set QName) -> TerM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TerM (Set QName)
    terGetMutual) TerM Calls
    fallback {-else-} (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ do
      String -> Int -> String -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.reduce" Int
    40 (String -> TerM ()) -> String -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ String
    "This call is in the current SCC!"

      -- Then, collect its clauses.
      cls <- Definition -> [Clause]
    defClauses (Definition -> [Clause]) -> TerM Definition -> TerM [Clause]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TerM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    g
      reportSLn "term.reduce" 40 $ unwords [ "Function has", show (length cls), "clauses"]
      reportSDoc "term.reduce" 80 $ vcat $ map (prettyTCM . NamedClause g True) cls
      reportSLn  "term.reduce" 80 . ("allowed reductions = " ++) . show . SmallSet.elems
        =<< asksTC envAllowedReductions

      -- Finally, try to reduce with the non-recursive clauses (and no rewrite rules).
      r <- liftTCM $
        modifyAllowedReductions (SmallSet.delete UnconfirmedReductions) $
        localTC (\TCEnv
    e -> TCEnv
    e { envTermCheckReducing = True }) $
        runReduceM $ appDefE' g v0 cls [] (map notReduced es)
      case r of
        NoReduction{}    -> TerM Calls
    fallback
        YesReduction Simplification
    _ Term
    v -> do
          String -> Int -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.reduce" Int
    30 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "Termination checker: Successfully reduced away call:"
            , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v0
            ]
          String -> Int -> TerM () -> TerM ()
    forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
    verboseS String
    "term.reduce" Int
    5 (TerM () -> TerM ()) -> TerM () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ String -> TerM ()
    forall (m :: * -> *). MonadStatistics m => String -> m ()
    tick String
    "termination-checker-reduced-nonrecursive-call"
          Term -> TerM Calls
    continue Term
    v

    -- | Extract recursive calls from a term.

    instance ExtractCalls Term where
      extract :: Term -> TerM Calls
    extract Term
    t = do
        String -> Int -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.check.term" Int
    50 (TCMT IO Doc -> TerM ()) -> TCMT IO Doc -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ do
          TCMT IO Doc
    "looking for calls in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    t

        -- Instantiate top-level MetaVar.
        Term -> TerM Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    t TerM Term -> (Term -> TerM Calls) -> TerM Calls
    forall a b. TerM a -> (a -> TerM b) -> TerM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case

          -- Constructed value.
          Con ConHead{conName :: ConHead -> QName
    conName = QName
    c, conDataRecord :: ConHead -> DataOrRecord
    conDataRecord = DataOrRecord
    dataOrRec} ConInfo
    _ Elims
    es -> do
            let args :: [Arg Term]
    args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
            -- A constructor preserves the guardedness of all its arguments.
            -- Andreas, 2022-09-19, issue #6108:
            -- A higher constructor does not.  So check if there is an @IApply@ amoung @es@.
            let argsg :: [(Arg Term, Bool)]
    argsg = [Arg Term] -> [Bool] -> [(Arg Term, Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Arg Term]
    args ([Bool] -> [(Arg Term, Bool)]) -> [Bool] -> [(Arg Term, Bool)]
    forall a b. (a -> b) -> a -> b
    $ Bool -> [Bool]
    forall a. a -> [a]
    repeat (Bool -> [Bool]) -> Bool -> [Bool]
    forall a b. (a -> b) -> a -> b
    $ (Elim -> Bool) -> Elims -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Elim -> Bool
    forall a. Elim' a -> Bool
    isProperApplyElim Elims
    es

            -- If we encounter a coinductive record constructor
            -- in a type mutual with the current target
            -- then we count it as guarding.
            let inductive :: TerM Induction
    inductive   = Induction -> TerM Induction
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Induction
    Inductive    -- not guarding, but preserving
                coinductive :: TerM Induction
    coinductive = Induction -> TerM Induction
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Induction
    CoInductive  -- guarding
            -- ♯ is guarding
            ind <- TerM Bool -> TerM Induction -> TerM Induction -> TerM Induction
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ((QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    c Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe QName -> Bool) -> TerM (Maybe QName) -> TerM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TerM (Maybe QName)
    terGetSharp) TerM Induction
    coinductive (TerM Induction -> TerM Induction)
    -> TerM Induction -> TerM Induction
    forall a b. (a -> b) -> a -> b
    $ {-else-} do
              -- data constructors are not guarding
              if DataOrRecord
    dataOrRec DataOrRecord -> DataOrRecord -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataOrRecord
    forall p. DataOrRecord' p
    IsData then TerM Induction
    inductive else do
              -- abstract constructors are not guarding
              TerM (Maybe (QName, RecordData))
    -> TerM Induction
    -> ((QName, RecordData) -> TerM Induction)
    -> TerM Induction
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> TerM (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isRecordConstructor QName
    c) TerM Induction
    inductive (((QName, RecordData) -> TerM Induction) -> TerM Induction)
    -> ((QName, RecordData) -> TerM Induction) -> TerM Induction
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    q, RecordData
    def) -> do
                String -> Int -> String -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.check.term" Int
    50 (String -> TerM ()) -> String -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ String
    "constructor " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    c String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " has record type " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q
                -- inductive record constructors are not guarding
                if RecordData -> Maybe Induction
    _recInduction RecordData
    def Maybe Induction -> Maybe Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Induction -> Maybe Induction
    forall a. a -> Maybe a
    Just Induction
    CoInductive then TerM Induction
    inductive else do
                -- coinductive constructors unrelated to the mutually
                -- constructed inhabitants of coinductive types are not guarding
                TerM Bool -> TerM Induction -> TerM Induction -> TerM Induction
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ([QName] -> TerM Bool
    targetElem ([QName] -> TerM Bool)
    -> (Maybe [QName] -> [QName]) -> Maybe [QName] -> TerM Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [QName] -> Maybe [QName] -> [QName]
    forall a. a -> Maybe a -> a
    fromMaybe [QName]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [QName] -> TerM Bool) -> Maybe [QName] -> TerM Bool
    forall a b. (a -> b) -> a -> b
    $ RecordData -> Maybe [QName]
    _recMutual RecordData
    def)
                   {-then-} TerM Induction
    coinductive
                   {-else-} TerM Induction
    inductive
            constructor c ind argsg

          -- Function, data, or record type.
          Def QName
    g Elims
    es -> QName -> Elims -> (Term -> TerM Calls) -> TerM Calls -> TerM Calls
    tryReduceNonRecursiveClause QName
    g Elims
    es Term -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> TerM Calls
    function QName
    g Elims
    es

          -- Abstraction. Preserves guardedness.
          Lam ArgInfo
    h Abs Term
    b -> Abs Term -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Abs Term
    b

          -- Neutral term. Destroys guardedness.
          Var Int
    i Elims
    es -> TerM Calls -> TerM Calls
    forall a. TerM a -> TerM a
    terUnguarded (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ Elims -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Elims
    es

          -- Dependent function space.
          Pi Dom' Term Type
    a (Abs String
    x Type
    b) ->
            Calls -> Calls -> Calls
    forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
    CallGraph.union (Calls -> Calls -> Calls) -> TerM Calls -> TerM (Calls -> Calls)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
            Dom' Term Type -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Dom' Term Type
    a TerM (Calls -> Calls) -> TerM Calls -> TerM Calls
    forall a b. TerM (a -> b) -> TerM a -> TerM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> do
              a <- Dom' Term Type -> TerM (Dom' Term Type)
    forall (tcm :: * -> *).
    MonadTCM tcm =>
    Dom' Term Type -> tcm (Dom' Term Type)
    maskSizeLt Dom' Term Type
    a  -- OR: just do not add a to the context!
              addContext (x, a) $ terRaise $ extract b

          -- Non-dependent function space.
          Pi Dom' Term Type
    a (NoAbs String
    _ Type
    b) ->
            Calls -> Calls -> Calls
    forall cinfo. CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo
    CallGraph.union (Calls -> Calls -> Calls) -> TerM Calls -> TerM (Calls -> Calls)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term Type -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Dom' Term Type
    a TerM (Calls -> Calls) -> TerM Calls -> TerM Calls
    forall a b. TerM (a -> b) -> TerM a -> TerM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Type
    b

          -- Literal.
          Lit Literal
    l -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty

          -- Sort.
          Sort Sort
    s -> Sort -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Sort
    s

          -- Unsolved metas are not considered termination problems, there
          -- will be a warning for them anyway.
          MetaV MetaId
    x Elims
    args -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty

          -- Erased and not-yet-erased proof.
          DontCare Term
    t -> Term -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Term
    t

          -- Level.
          Level Level' Term
    l -> -- billTo [Benchmark.Termination, Benchmark.Level] $ do
            -- Andreas, 2014-03-26 Benchmark discontinued, < 0.3% spent on levels.
            Level' Term -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Level' Term
    l

          -- Dummy.
          Dummy{} -> Calls -> TerM Calls
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty

    -- | Extract recursive calls from level expressions.

    instance ExtractCalls Level where
      extract :: Level' Term -> TerM Calls
    extract (Max Integer
    n [PlusLevel' Term]
    as) = [PlusLevel' Term] -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract [PlusLevel' Term]
    as

    instance ExtractCalls PlusLevel where
      extract :: PlusLevel' Term -> TerM Calls
    extract (Plus Integer
    n Term
    l) = Term -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Term
    l

    -- | Rewrite type @tel -> Size< u@ to @tel -> Size@.
    maskSizeLt :: MonadTCM tcm => Dom Type -> tcm (Dom Type)
    maskSizeLt :: forall (tcm :: * -> *).
    MonadTCM tcm =>
    Dom' Term Type -> tcm (Dom' Term Type)
    maskSizeLt !Dom' Term Type
    dom = TCM (Dom' Term Type) -> tcm (Dom' Term Type)
    forall a. TCM a -> tcm a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Dom' Term Type) -> tcm (Dom' Term Type))
    -> TCM (Dom' Term Type) -> tcm (Dom' Term Type)
    forall a b. (a -> b) -> a -> b
    $ do
      let a :: Type
    a = Dom' Term Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom' Term Type
    dom
      (msize, msizelt) <- TCMT IO (Maybe QName, Maybe QName)
    forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize
      case (msize, msizelt) of
        (Maybe QName
    _ , Maybe QName
    Nothing) -> Dom' Term Type -> TCM (Dom' Term Type)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Dom' Term Type
    dom
        (Maybe QName
    Nothing, Maybe QName
    _)  -> TCM (Dom' Term Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Just QName
    size, Just QName
    sizelt) -> do
          TelV tel c <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    a
          case a of
            El Sort
    s (Def QName
    d [Elim
    v]) | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    sizelt -> Dom' Term Type -> TCM (Dom' Term Type)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom' Term Type -> TCM (Dom' Term Type))
    -> Dom' Term Type -> TCM (Dom' Term Type)
    forall a b. (a -> b) -> a -> b
    $
              Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    size []) Type -> Dom' Term Type -> Dom' Term Type
    forall a b. a -> Dom' Term b -> Dom' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom' Term Type
    dom
            Type
    _ -> Dom' Term Type -> TCM (Dom' Term Type)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Dom' Term Type
    dom

    {- | @compareArgs es@

         Compare the list of de Bruijn patterns (=parameters) @pats@
         with a list of arguments @es@ and create a call maxtrix
         with |es| rows and |pats| columns.

         The guardedness is the number of projection patterns in @pats@
         minus the number of projections in @es@.
     -}
    compareArgs :: [Elim] -> TerM (Int, Int, [[Order]])
    compareArgs :: Elims -> TerM (Int, Int, [[Order]])
    compareArgs Elims
    es = do
      pats <- TerM MaskedDeBruijnPatterns
    terGetPatterns
      liftTCM $ reportSDoc "term.compareArgs" 90 $ vcat
        [ text $ "comparing " ++ show (length es) ++ " args to " ++ show (length pats) ++ " patterns"
        ]
      -- apats <- annotatePatsWithUseSizeLt pats
      -- reportSDoc "term.compare" 20 $
      --   "annotated patterns = " <+> sep (map prettyTCM apats)
      -- matrix <- forM es $ \ e -> forM apats $ \ (b, p) -> terSetUseSizeLt b $ compareElim e p
      matrix <- withUsableVars pats $ forM es $ \ Elim
    e -> MaskedDeBruijnPatterns
    -> (Masked DeBruijnPattern -> TerM Order) -> TerM [Order]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM MaskedDeBruijnPatterns
    pats ((Masked DeBruijnPattern -> TerM Order) -> TerM [Order])
    -> (Masked DeBruijnPattern -> TerM Order) -> TerM [Order]
    forall a b. (a -> b) -> a -> b
    $ \ Masked DeBruijnPattern
    p -> Elim -> Masked DeBruijnPattern -> TerM Order
    compareElim Elim
    e Masked DeBruijnPattern
    p

      -- Count the number of coinductive projection(pattern)s in caller and callee.
      -- Only recursive coinductive projections are eligible (Issue 1209).
      projsCaller <- length <$> do
        filterM (isCoinductiveProjection True) $ mapMaybe (fmap (headAmbQ . snd) . isProjP . getMasked) pats
      projsCallee <- length <$> do
        filterM (isCoinductiveProjection True) $ mapMaybe (fmap snd . isProjElim) es
      cutoff <- terGetCutOff
      let ?cutoff = cutoff
      let guardedness = (?cutoff::CutOff) => Bool -> Int -> Order
    Bool -> Int -> Order
    decr Bool
    True (Int -> Order) -> Int -> Order
    forall a b. (a -> b) -> a -> b
    $ Int
    projsCaller Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    projsCallee
      liftTCM $ reportSDoc "term.guardedness" 30 $ sep
        [ "compareArgs:"
        , nest 2 $ text $ "projsCaller = " ++ prettyShow projsCaller
        , nest 2 $ text $ "projsCallee = " ++ prettyShow projsCallee
        , nest 2 $ text $ "guardedness of call: " ++ prettyShow guardedness
        ]
      return $ addGuardedness guardedness (size es, size pats, matrix)

    -- | Traverse patterns from left to right.
    --   When we come to a projection pattern,
    --   switch usage of SIZELT constraints:
    --   on, if coinductive,
    --   off, if inductive.
    --
    --   UNUSED
    --annotatePatsWithUseSizeLt :: [DeBruijnPattern] -> TerM [(Bool,DeBruijnPattern)]
    --annotatePatsWithUseSizeLt = loop where
    --  loop [] = return []
    --  loop (p@(ProjP _ q) : pats) = ((False,p) :) <$> do projUseSizeLt q $ loop pats
    --  loop (p : pats) = (\ b ps -> (b,p) : ps) <$> terGetUseSizeLt <*> loop pats

    -- | @compareElim e dbpat@

    compareElim :: Elim -> Masked DeBruijnPattern -> TerM Order
    compareElim :: Elim -> Masked DeBruijnPattern -> TerM Order
    compareElim Elim
    e Masked DeBruijnPattern
    p = do
      TCMT IO () -> TerM ()
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ do
        String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.compare" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ TCMT IO Doc
    "compareElim"
          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "e = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> Elim -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim -> m Doc
    prettyTCM Elim
    e
          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "p = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> Masked DeBruijnPattern -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *).
    MonadPretty m =>
    Masked DeBruijnPattern -> m Doc
    prettyTCM Masked DeBruijnPattern
    p
          ]
        String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "term.compare" Int
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "e = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Elim -> String
    forall a. Show a => a -> String
    show Elim
    e
          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "p = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Masked DeBruijnPattern -> String
    forall a. Show a => a -> String
    show Masked DeBruijnPattern
    p
          ]
      case (Elim
    e, Masked DeBruijnPattern -> DeBruijnPattern
    forall a. Masked a -> a
    getMasked Masked DeBruijnPattern
    p) of
        (Proj ProjOrigin
    _ QName
    d, ProjP ProjOrigin
    _ QName
    d') -> do
          d  <- QName -> TerM QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getOriginalProjection QName
    d
          d' <- getOriginalProjection d'
          o  <- compareProj d d'
          reportSDoc "term.compare" 30 $ sep
            [ text $ "comparing callee projection " ++ prettyShow d
            , text $ "against caller projection " ++ prettyShow d'
            , text $ "yields order " ++ prettyShow o
            ]
          return o
        (Proj{}, DeBruijnPattern
    _)            -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown
        (Apply{}, ProjP{})     -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown
        (Apply Arg Term
    arg, DeBruijnPattern
    _)         -> Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg) Masked DeBruijnPattern
    p
        -- TODO Andrea: making sense?
        (IApply{}, ProjP{})  -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown
        (IApply Term
    _ Term
    _ Term
    arg, DeBruijnPattern
    _)    -> Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm Term
    arg Masked DeBruijnPattern
    p

    -- | In dependent records, the types of later fields may depend on the
    --   values of earlier fields.  Thus when defining an inhabitant of a
    --   dependent record type such as Σ by copattern matching,
    --   a recursive call eliminated by an earlier projection (proj₁) might
    --   occur in the definition at a later projection (proj₂).
    --   Thus, earlier projections are considered "smaller" when
    --   comparing copattern spines.  This is an ok approximation
    --   of the actual dependency order.
    --   See issues 906, 942.
    compareProj :: MonadTCM tcm => QName -> QName -> tcm Order
    compareProj :: forall (tcm :: * -> *). MonadTCM tcm => QName -> QName -> tcm Order
    compareProj QName
    d QName
    d'
      | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d' = Order -> tcm Order
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le
      | Bool
    otherwise = TCM Order -> tcm Order
    forall a. TCM a -> tcm a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Order -> tcm Order) -> TCM Order -> tcm Order
    forall a b. (a -> b) -> a -> b
    $ do
          -- different projections
          mr  <- QName -> TCM (Maybe QName)
    getRecordOfField QName
    d
          mr' <- getRecordOfField d'
          case (mr, mr') of
            (Just QName
    r, Just QName
    r') | QName
    r QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    r' -> do
              -- of same record
              def <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    r
              case def of
                Record{ recFields :: Defn -> [Dom QName]
    recFields = [Dom QName]
    fs } -> do
                  fs <- [QName] -> TCMT IO [QName]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([QName] -> TCMT IO [QName]) -> [QName] -> TCMT IO [QName]
    forall a b. (a -> b) -> a -> b
    $ (Dom QName -> QName) -> [Dom QName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom QName -> QName
    forall t e. Dom' t e -> e
    unDom [Dom QName]
    fs
                  case (List.find (d ==) fs, List.find (d' ==) fs) of
                    (Just QName
    i, Just QName
    i')
                      -- earlier field is smaller
                      | QName
    i QName -> QName -> Bool
    forall a. Ord a => a -> a -> Bool
    < QName
    i'    -> Order -> TCM Order
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.lt
                      | QName
    i QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    i'   -> do
                         __IMPOSSIBLE__
                      | Bool
    otherwise -> Order -> TCM Order
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown
                    (Maybe QName, Maybe QName)
    _ -> TCM Order
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                Defn
    _ -> TCM Order
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            (Maybe QName, Maybe QName)
    _ -> Order -> TCM Order
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown

    -- | 'makeCM' turns the result of 'compareArgs' into a proper call matrix
    makeCM :: Int -> Int -> [[Order]] -> CallMatrix
    makeCM :: Int -> Int -> [[Order]] -> CallMatrix
    makeCM Int
    ncols Int
    nrows [[Order]]
    matrix = Matrix Int Order -> CallMatrix
    forall a. Matrix Int a -> CallMatrix' a
    CallMatrix (Matrix Int Order -> CallMatrix) -> Matrix Int Order -> CallMatrix
    forall a b. (a -> b) -> a -> b
    $
      Size Int -> [[Order]] -> Matrix Int Order
    forall i b.
    (Ord i, Num i, Enum i, HasZero b) =>
    Size i -> [[b]] -> Matrix i b
    Matrix.fromLists (Int -> Int -> Size Int
    forall i. i -> i -> Size i
    Matrix.Size Int
    nrows Int
    ncols) [[Order]]
    matrix

    -- | 'addGuardedness' adds guardedness flag in the upper left corner
    -- (0,0).
    addGuardedness :: Order -> (Int, Int, [[Order]]) -> (Int, Int, [[Order]])
    addGuardedness :: Order -> (Int, Int, [[Order]]) -> (Int, Int, [[Order]])
    addGuardedness Order
    o (Int
    nrows, Int
    ncols, [[Order]]
    m) =
      (Int
    nrows Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1, Int
    ncols Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1,
       (Order
    o Order -> [Order] -> [Order]
    forall a. a -> [a] -> [a]
    : Int -> Order -> [Order]
    forall a. Int -> a -> [a]
    replicate Int
    ncols Order
    Order.unknown) [Order] -> [[Order]] -> [[Order]]
    forall a. a -> [a] -> [a]
    : ([Order] -> [Order]) -> [[Order]] -> [[Order]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Order
    Order.unknown Order -> [Order] -> [Order]
    forall a. a -> [a] -> [a]
    :) [[Order]]
    m)

    -- | Compose something with the upper-left corner of a call matrix
    composeGuardedness :: (?cutoff :: CutOff) => Order -> [[Order]] -> [[Order]]
    composeGuardedness :: (?cutoff::CutOff) => Order -> [[Order]] -> [[Order]]
    composeGuardedness Order
    o ((Order
    corner : [Order]
    row) : [[Order]]
    rows) = ((Order
    o (?cutoff::CutOff) => Order -> Order -> Order
    Order -> Order -> Order
    .*. Order
    corner) Order -> [Order] -> [Order]
    forall a. a -> [a] -> [a]
    : [Order]
    row) [Order] -> [[Order]] -> [[Order]]
    forall a. a -> [a] -> [a]
    : [[Order]]
    rows
    composeGuardedness Order
    _ [[Order]]
    _ = [[Order]]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Stripping off a record constructor is not counted as decrease, in
    --   contrast to a data constructor.
    --   A record constructor increases/decreases by 0, a data constructor by 1.
    offsetFromConstructor :: HasConstInfo tcm => QName -> tcm Int
    offsetFromConstructor :: forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Int
    offsetFromConstructor QName
    c =
      tcm Bool -> tcm Int -> tcm Int -> tcm Int
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> tcm Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaOrCoinductiveRecordConstructor QName
    c) (Int -> tcm Int
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    0) (Int -> tcm Int
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    1)

    --UNUSED Liang-Ting 2019-07-16
    ---- | Compute the proper subpatterns of a 'DeBruijnPattern'.
    --subPatterns :: DeBruijnPattern -> [DeBruijnPattern]
    --subPatterns = foldPattern $ \case
    --  ConP _ _ ps -> map namedArg ps
    --  DefP _ _ ps -> map namedArg ps -- TODO check semantics
    --  VarP _ _    -> mempty
    --  LitP _      -> mempty
    --  DotP _ _    -> mempty
    --  ProjP _ _   -> mempty
    --  IApplyP{}   -> mempty

    compareTerm :: Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm :: Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm Term
    t Masked DeBruijnPattern
    p = do
    --   reportSDoc "term.compare" 25 $
    --     " comparing term " <+> prettyTCM t <+>
    --     " to pattern " <+> prettyTCM p
      t <- TCM Term -> TerM Term
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Term -> TerM Term) -> TCM Term -> TerM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> TCM Term
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Term
    t
      o <- compareTerm' t p
      liftTCM $ reportSDoc "term.compare" 25 $
        " comparing term " <+> prettyTCM t <+>
        " to pattern " <+> prettyTCM p <+>
        text (" results in " ++ prettyShow o)
      return o

    -- | Remove all non-coinductive projections from an algebraic term
    --   (not going under binders).
    --   Also, remove 'DontCare's.
    --
    class StripAllProjections a where
      stripAllProjections :: a -> TCM a

    instance StripAllProjections a => StripAllProjections (Arg a) where
      stripAllProjections :: Arg a -> TCM (Arg a)
    stripAllProjections = (a -> TCMT IO a) -> Arg a -> TCM (Arg a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse a -> TCMT IO a
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections

    instance StripAllProjections Elims where
      stripAllProjections :: Elims -> TCM Elims
    stripAllProjections Elims
    es =
        case Elims
    es of
          []             -> Elims -> TCM Elims
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          (Apply Arg Term
    a : Elims
    es) -> do
            (:) (Elim -> Elims -> Elims)
    -> TCMT IO Elim -> TCMT IO (Elims -> Elims)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> TCMT IO (Arg Term) -> TCMT IO Elim
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> TCMT IO (Arg Term)
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Arg Term
    a) TCMT IO (Elims -> Elims) -> TCM Elims -> TCM Elims
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Elims -> TCM Elims
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Elims
    es
          (IApply Term
    x Term
    y Term
    a : Elims
    es) -> do
            -- TODO Andrea: are we doind extra work?
            (:) (Elim -> Elims -> Elims)
    -> TCMT IO Elim -> TCMT IO (Elims -> Elims)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> Term -> Term -> Elim
    forall a. a -> a -> a -> Elim' a
    IApply (Term -> Term -> Term -> Elim)
    -> TCM Term -> TCMT IO (Term -> Term -> Elim)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCM Term
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Term
    x
                            TCMT IO (Term -> Term -> Elim)
    -> TCM Term -> TCMT IO (Term -> Elim)
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> TCM Term
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Term
    y
                            TCMT IO (Term -> Elim) -> TCM Term -> TCMT IO Elim
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> TCM Term
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Term
    a)
                TCMT IO (Elims -> Elims) -> TCM Elims -> TCM Elims
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Elims -> TCM Elims
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Elims
    es
          (Proj ProjOrigin
    o QName
    p  : Elims
    es) -> do
            isP <- QName -> TCMT IO Bool
    forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Bool
    isProjectionButNotCoinductive QName
    p
            applyUnless isP (Proj o p :) <$> stripAllProjections es

    instance StripAllProjections Args where
      stripAllProjections :: [Arg Term] -> TCM [Arg Term]
    stripAllProjections = (Arg Term -> TCMT IO (Arg Term)) -> [Arg Term] -> TCM [Arg Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Arg Term -> TCMT IO (Arg Term)
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections

    instance StripAllProjections Term where
      stripAllProjections :: Term -> TCM Term
    stripAllProjections Term
    t = do
        case Term
    t of
          Var Int
    i Elims
    es   -> Int -> Elims -> Term
    Var Int
    i (Elims -> Term) -> TCM Elims -> TCM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> TCM Elims
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Elims
    es
          Con ConHead
    c ConInfo
    ci Elims
    ts -> do
            -- Andreas, 2019-02-23, re #2613.  This is apparently not necessary:
            -- c <- fromRightM (\ err -> return c) $ getConForm (conName c)
            ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term) -> TCM Elims -> TCM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> TCM Elims
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Elims
    ts
          Def QName
    d Elims
    es   -> QName -> Elims -> Term
    Def QName
    d (Elims -> Term) -> TCM Elims -> TCM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> TCM Elims
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Elims
    es
          DontCare Term
    t -> Term -> TCM Term
    forall a. StripAllProjections a => a -> TCM a
    stripAllProjections Term
    t
          Term
    _ -> Term -> TCM Term
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    t

    -- | Normalize outermost constructor name in a pattern.

    reduceConPattern :: DeBruijnPattern -> TCM DeBruijnPattern
    reduceConPattern :: DeBruijnPattern -> TCM DeBruijnPattern
    reduceConPattern = \case
      ConP ConHead
    c ConPatternInfo
    i NAPs
    ps -> (SigError -> TCMT IO ConHead)
    -> TCMT IO (Either SigError ConHead) -> TCMT IO ConHead
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> m (Either a b) -> m b
    fromRightM (\ SigError
    err -> ConHead -> TCMT IO ConHead
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ConHead
    c) (QName -> TCMT IO (Either SigError ConHead)
    getConForm (ConHead -> QName
    conName ConHead
    c)) TCMT IO ConHead
    -> (ConHead -> DeBruijnPattern) -> TCM DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ ConHead
    c' ->
        ConHead -> ConPatternInfo -> NAPs -> DeBruijnPattern
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c' ConPatternInfo
    i NAPs
    ps
      DeBruijnPattern
    p -> DeBruijnPattern -> TCM DeBruijnPattern
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    p

    -- | @compareTerm' t dbpat@

    compareTerm' :: Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' :: Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' Term
    v mp :: Masked DeBruijnPattern
    mp@(Masked Bool
    m DeBruijnPattern
    p) = do
      suc  <- TerM (Maybe QName)
    terGetSizeSuc
      cutoff <- terGetCutOff
      let ?cutoff = cutoff
      v <- liftTCM (instantiate v)
      p <- liftTCM $ reduceConPattern p
      case (v, p) of

        -- Andreas, 2013-11-20 do not drop projections,
        -- in any case not coinductive ones!:
        (Var Int
    i Elims
    es, DeBruijnPattern
    _) | Just{} <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
          Int -> Masked DeBruijnPattern -> TerM Order
    compareVar Int
    i Masked DeBruijnPattern
    mp

        (DontCare Term
    t, DeBruijnPattern
    _) ->
          Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' Term
    t Masked DeBruijnPattern
    mp

        -- Andreas, 2014-09-22, issue 1281:
        -- For metas, termination checking should be optimistic.
        -- If there is any instance of the meta making termination
        -- checking succeed, then we should not fail.
        -- Thus, we assume the meta will be instantiated with the
        -- deepest variable in @p@.
        -- For sized types, the depth is maximally
        -- the number of SIZELT hypotheses one can have in a context.
        (MetaV{}, DeBruijnPattern
    p) -> (?cutoff::CutOff) => Bool -> Int -> Order
    Bool -> Int -> Order
    Order.decr Bool
    True (Int -> Order) -> (Int -> Int) -> Int -> Order
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max (if Bool
    m then Int
    0 else DeBruijnPattern -> Int
    forall a. Pattern' a -> Int
    patternDepth DeBruijnPattern
    p) (Int -> Int) -> (Int -> Int) -> Int -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int
    forall a. Enum a => a -> a
    pred (Int -> Order) -> TerM Int -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
           (TerEnv -> Int) -> TerM Int
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Int
    _terSizeDepth

        -- Successor on both sides cancel each other.
        -- We ignore the mask for sizes.
        (Def QName
    s [Apply Arg Term
    t], ConP ConHead
    s' ConPatternInfo
    _ [Arg (Named_ DeBruijnPattern)
    p]) | QName
    s QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead -> QName
    conName ConHead
    s' Bool -> Bool -> Bool
    && QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    s Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    suc ->
          Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t) (DeBruijnPattern -> Masked DeBruijnPattern
    forall a. a -> Masked a
    notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
    -> DeBruijnPattern -> Masked DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg Arg (Named_ DeBruijnPattern)
    p)

        -- Register also size increase.
        (Def QName
    s [Apply Arg Term
    t], DeBruijnPattern
    p) | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    s Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    suc ->
          -- Andreas, 2012-10-19 do not cut off here
          Int -> Order -> Order
    increase Int
    1 (Order -> Order) -> TerM Order -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t) Masked DeBruijnPattern
    mp

        -- In all cases that do not concern sizes,
        -- we cannot continue if pattern is masked.

        (Term, DeBruijnPattern)
    _ | Bool
    m -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown

        (Lit Literal
    l, LitP PatternInfo
    _ Literal
    l')
          | Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l'     -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le
          | Bool
    otherwise   -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown

        (Lit Literal
    l, DeBruijnPattern
    _) -> do
          v <- TCM Term -> TerM Term
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Term -> TerM Term) -> TCM Term -> TerM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> TCM Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm Term
    v
          case v of
            Lit{}       -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown
            Term
    v           -> Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' Term
    v Masked DeBruijnPattern
    mp

        -- Andreas, 2011-04-19 give subterm priority over matrix order

        (Con{}, ConP ConHead
    c ConPatternInfo
    _ NAPs
    ps) | (Arg (Named_ DeBruijnPattern) -> Bool) -> NAPs -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ((?cutoff::CutOff) => Term -> DeBruijnPattern -> Bool
    Term -> DeBruijnPattern -> Bool
    isSubTerm Term
    v (DeBruijnPattern -> Bool)
    -> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
    -> Arg (Named_ DeBruijnPattern)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) NAPs
    ps ->
          (?cutoff::CutOff) => Bool -> Int -> Order
    Bool -> Int -> Order
    decr Bool
    True (Int -> Order) -> TerM Int -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TerM Int
    forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Int
    offsetFromConstructor (ConHead -> QName
    conName ConHead
    c)

        (Con ConHead
    c ConInfo
    _ Elims
    es, ConP ConHead
    c' ConPatternInfo
    _ NAPs
    ps) | ConHead -> QName
    conName ConHead
    c QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead -> QName
    conName ConHead
    c'->
          let ts :: [Arg Term]
    ts = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es in
          [Arg Term] -> NAPs -> TerM Order
    compareConArgs [Arg Term]
    ts NAPs
    ps

        (Con ConHead
    _ ConInfo
    _ [], DeBruijnPattern
    _) -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le

        -- new case for counting constructors / projections
        -- register also increase
        (Con ConHead
    c ConInfo
    _ Elims
    es, DeBruijnPattern
    _) -> do
          let ts :: [Arg Term]
    ts = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
          Int -> Order -> Order
    increase (Int -> Order -> Order) -> TerM Int -> TerM (Order -> Order)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TerM Int
    forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Int
    offsetFromConstructor (ConHead -> QName
    conName ConHead
    c)
                   TerM (Order -> Order) -> TerM Order -> TerM Order
    forall a b. TerM (a -> b) -> TerM a -> TerM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ((?cutoff::CutOff) => [Order] -> Order
    [Order] -> Order
    infimum ([Order] -> Order) -> TerM [Order] -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Arg Term -> TerM Order) -> [Arg Term] -> TerM [Order]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\ Arg Term
    t -> Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t) Masked DeBruijnPattern
    mp) [Arg Term]
    ts)

        (Term
    t, DeBruijnPattern
    p) -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Order -> TerM Order) -> Order -> TerM Order
    forall a b. (a -> b) -> a -> b
    $ (?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
    Term -> DeBruijnPattern -> Order
    subTerm Term
    t DeBruijnPattern
    p

    -- | @subTerm@ computes a size difference (Order)
    subTerm :: (?cutoff :: CutOff) => Term -> DeBruijnPattern -> Order
    subTerm :: (?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
    subTerm Term
    t DeBruijnPattern
    p = if Term -> DeBruijnPattern -> Bool
    equal Term
    t DeBruijnPattern
    p then Order
    Order.le else (?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
    Term -> DeBruijnPattern -> Order
    properSubTerm Term
    t DeBruijnPattern
    p
      where
        equal :: Term -> DeBruijnPattern -> Bool
    equal (Con ConHead
    c ConInfo
    _ Elims
    es) (ConP ConHead
    c' ConPatternInfo
    _ NAPs
    ps) =
          let ts :: [Arg Term]
    ts = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es in
          [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ([Bool] -> Bool) -> [Bool] -> Bool
    forall a b. (a -> b) -> a -> b
    $ (ConHead -> QName
    conName ConHead
    c QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead -> QName
    conName ConHead
    c')
              Bool -> [Bool] -> [Bool]
    forall a. a -> [a] -> [a]
    : ([Arg Term] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg Term]
    ts Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == NAPs -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length NAPs
    ps)
              Bool -> [Bool] -> [Bool]
    forall a. a -> [a] -> [a]
    : (Arg Term -> Arg (Named_ DeBruijnPattern) -> Bool)
    -> [Arg Term] -> NAPs -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Arg Term
    t Arg (Named_ DeBruijnPattern)
    p -> Term -> DeBruijnPattern -> Bool
    equal (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t) (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg Arg (Named_ DeBruijnPattern)
    p)) [Arg Term]
    ts NAPs
    ps
        equal (Var Int
    i []) (VarP PatternInfo
    _ DBPatVar
    x) = Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x
        equal (Lit Literal
    l)    (LitP PatternInfo
    _ Literal
    l') = Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l'
        -- Terms.
        -- Checking for identity here is very fragile.
        -- However, we cannot do much more, as we are not allowed to normalize t.
        -- (It might diverge, and we are just in the process of termination checking.)
        equal Term
    t         (DotP PatternInfo
    _ Term
    t') = Term
    t Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    t'
        equal Term
    _ DeBruijnPattern
    _ = Bool
    False

        properSubTerm :: Term -> DeBruijnPattern -> Order
    properSubTerm Term
    t (ConP ConHead
    _ ConPatternInfo
    _ NAPs
    ps) =
          Bool -> Order -> Order
    setUsability Bool
    True (Order -> Order) -> Order -> Order
    forall a b. (a -> b) -> a -> b
    $ Int -> Order -> Order
    decrease Int
    1 (Order -> Order) -> Order -> Order
    forall a b. (a -> b) -> a -> b
    $ (?cutoff::CutOff) => [Order] -> Order
    [Order] -> Order
    supremum ([Order] -> Order) -> [Order] -> Order
    forall a b. (a -> b) -> a -> b
    $ (Arg (Named_ DeBruijnPattern) -> Order) -> NAPs -> [Order]
    forall a b. (a -> b) -> [a] -> [b]
    map ((?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
    Term -> DeBruijnPattern -> Order
    subTerm Term
    t (DeBruijnPattern -> Order)
    -> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
    -> Arg (Named_ DeBruijnPattern)
    -> Order
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) NAPs
    ps
        properSubTerm Term
    _ DeBruijnPattern
    _ = Order
    Order.unknown

    isSubTerm :: (?cutoff :: CutOff) => Term -> DeBruijnPattern -> Bool
    isSubTerm :: (?cutoff::CutOff) => Term -> DeBruijnPattern -> Bool
    isSubTerm Term
    t DeBruijnPattern
    p = Order -> Bool
    nonIncreasing (Order -> Bool) -> Order -> Bool
    forall a b. (a -> b) -> a -> b
    $ (?cutoff::CutOff) => Term -> DeBruijnPattern -> Order
    Term -> DeBruijnPattern -> Order
    subTerm Term
    t DeBruijnPattern
    p

    compareConArgs :: Args -> [NamedArg DeBruijnPattern] -> TerM Order
    compareConArgs :: [Arg Term] -> NAPs -> TerM Order
    compareConArgs [Arg Term]
    ts NAPs
    ps = do
      cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = cutoff
      case compare (length ts) (length ps) of

        -- We may assume |ps| >= |ts|, otherwise c ps would be of functional type
        -- which is impossible.
        Ordering
    GT -> TerM Order
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Andreas, 2022-08-31, issue #6059: doing anything smarter than
        -- @unknown@ here can lead to non-termination.
        Ordering
    LT -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown

        Ordering
    EQ -> (Order -> Order -> Order) -> Order -> [Order] -> Order
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    List.foldl' (?cutoff::CutOff) => Order -> Order -> Order
    Order -> Order -> Order
    (Order..*.) Order
    Order.le ([Order] -> Order) -> TerM [Order] -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                   (Term -> Masked DeBruijnPattern -> TerM Order)
    -> [Term] -> MaskedDeBruijnPatterns -> TerM [Order]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' ((Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg [Arg Term]
    ts) ((Arg (Named_ DeBruijnPattern) -> Masked DeBruijnPattern)
    -> NAPs -> MaskedDeBruijnPatterns
    forall a b. (a -> b) -> [a] -> [b]
    map (DeBruijnPattern -> Masked DeBruijnPattern
    forall a. a -> Masked a
    notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
    -> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
    -> Arg (Named_ DeBruijnPattern)
    -> Masked DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) NAPs
    ps)
           -- corresponds to taking the size, not the height
           -- allows examples like (x, y) < (Succ x, y)
    {- version which does an "order matrix"
       -- Andreas, 2013-02-18 disabled because it is unclear
       -- how to scale idempotency test to matrix-shaped orders (need thinking/researcH)
       -- Trigges issue 787.
            (_,_) -> do -- build "call matrix"
              m <- mapM (\t -> mapM (compareTerm' suc (unArg t)) ps) ts
              let m2 = makeCM (length ps) (length ts) m
              return $ Order.orderMat (Order.mat m2)
    -}
    {- version which takes height
    --    if null ts then Order.Le
    --               else Order.infimum (zipWith compareTerm' (map unArg ts) ps)
    -}

    compareVar :: Nat -> Masked DeBruijnPattern -> TerM Order
    compareVar :: Int -> Masked DeBruijnPattern -> TerM Order
    compareVar Int
    i (Masked Bool
    m DeBruijnPattern
    p) = do
      suc    <- TerM (Maybe QName)
    terGetSizeSuc
      cutoff <- terGetCutOff
      let ?cutoff = cutoff
      let no = Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown
      case p of
        ProjP{}   -> TerM Order
    no
        IApplyP PatternInfo
    _ Term
    _ Term
    _ DBPatVar
    x  -> Int -> Masked DBPatVar -> TerM Order
    compareVarVar Int
    i (Bool -> DBPatVar -> Masked DBPatVar
    forall a. Bool -> a -> Masked a
    Masked Bool
    m DBPatVar
    x)
        LitP{}    -> TerM Order
    no
        DotP{}   -> TerM Order
    no
        VarP PatternInfo
    _ DBPatVar
    x  -> Int -> Masked DBPatVar -> TerM Order
    compareVarVar Int
    i (Bool -> DBPatVar -> Masked DBPatVar
    forall a. Bool -> a -> Masked a
    Masked Bool
    m DBPatVar
    x)

        ConP ConHead
    s ConPatternInfo
    _ [Arg (Named_ DeBruijnPattern)
    p] | QName -> Maybe QName
    forall a. a -> Maybe a
    Just (ConHead -> QName
    conName ConHead
    s) Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    suc ->
          Bool -> Order -> Order
    setUsability Bool
    True (Order -> Order) -> (Order -> Order) -> Order -> Order
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Order -> Order
    decrease Int
    1 (Order -> Order) -> TerM Order -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> Masked DeBruijnPattern -> TerM Order
    compareVar Int
    i (DeBruijnPattern -> Masked DeBruijnPattern
    forall a. a -> Masked a
    notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
    -> DeBruijnPattern -> Masked DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg Arg (Named_ DeBruijnPattern)
    p)

        ConP ConHead
    c ConPatternInfo
    pi NAPs
    ps -> if Bool
    m then TerM Order
    no else Bool -> Order -> Order
    setUsability Bool
    True (Order -> Order) -> TerM Order -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          let
            dropit :: IsForced -> a -> Maybe a
    dropit IsForced
    Forced a
    _ = Maybe a
    forall a. Maybe a
    Nothing
            dropit IsForced
    NotForced a
    x = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x
          ps <- TerM Bool -> TerM NAPs -> TerM NAPs -> TerM NAPs
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (PragmaOptions -> Bool
    optForcedArgumentRecursion (PragmaOptions -> Bool) -> TerM PragmaOptions -> TerM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TerM PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)
            {- then -} (NAPs -> TerM NAPs
    forall a. a -> TerM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure NAPs
    ps)
            {- else -} (QName
    -> NAPs
    -> (IsForced
        -> Arg (Named_ DeBruijnPattern)
        -> Maybe (Arg (Named_ DeBruijnPattern)))
    -> TerM NAPs
    forall a b. QName -> [a] -> (IsForced -> a -> Maybe b) -> TerM [b]
    mapForcedArguments (ConHead -> QName
    conName ConHead
    c) NAPs
    ps IsForced
    -> Arg (Named_ DeBruijnPattern)
    -> Maybe (Arg (Named_ DeBruijnPattern))
    forall {a}. IsForced -> a -> Maybe a
    dropit)
          decrease <$> offsetFromConstructor (conName c)
                   <*> (Order.supremum <$> mapM (compareVar i . notMasked . namedArg) ps)
        DefP PatternInfo
    _ QName
    c NAPs
    ps -> if Bool
    m then TerM Order
    no else Bool -> Order -> Order
    setUsability Bool
    True (Order -> Order) -> TerM Order -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          Int -> Order -> Order
    decrease (Int -> Order -> Order) -> TerM Int -> TerM (Order -> Order)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TerM Int
    forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Int
    offsetFromConstructor QName
    c
                   TerM (Order -> Order) -> TerM Order -> TerM Order
    forall a b. TerM (a -> b) -> TerM a -> TerM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ((?cutoff::CutOff) => [Order] -> Order
    [Order] -> Order
    Order.supremum ([Order] -> Order) -> TerM [Order] -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Arg (Named_ DeBruijnPattern) -> TerM Order)
    -> NAPs -> TerM [Order]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Int -> Masked DeBruijnPattern -> TerM Order
    compareVar Int
    i (Masked DeBruijnPattern -> TerM Order)
    -> (Arg (Named_ DeBruijnPattern) -> Masked DeBruijnPattern)
    -> Arg (Named_ DeBruijnPattern)
    -> TerM Order
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DeBruijnPattern -> Masked DeBruijnPattern
    forall a. a -> Masked a
    notMasked (DeBruijnPattern -> Masked DeBruijnPattern)
    -> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
    -> Arg (Named_ DeBruijnPattern)
    -> Masked DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) NAPs
    ps)
          -- This should be fine for c == hcomp

    -- | Compare two variables.
    --
    --   The first variable comes from a term, the second from a pattern.
    compareVarVar :: Nat -> Masked DBPatVar -> TerM Order
    compareVarVar :: Int -> Masked DBPatVar -> TerM Order
    compareVarVar Int
    i (Masked Bool
    m x :: DBPatVar
    x@(DBPatVar String
    _ Int
    j))
      | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j = if Bool -> Bool
    not Bool
    m then Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le else TCM Order -> TerM Order
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Order -> TerM Order) -> TCM Order -> TerM Order
    forall a b. (a -> b) -> a -> b
    $
          -- If j is a size, we ignore the mask.
          TCMT IO Bool -> TCM Order -> TCM Order -> TCM Order
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Maybe BoundedSize -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe BoundedSize -> Bool)
    -> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do Type -> TCMT IO (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    Type -> m (Maybe BoundedSize)
    isSizeType (Type -> TCMT IO (Maybe BoundedSize))
    -> TCMT IO Type -> TCMT IO (Maybe BoundedSize)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Int -> TCMT IO Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    j)
            {- then -} (Order -> TCM Order
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le)
            {- else -} (Order -> TCM Order
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown)
      | Bool
    otherwise = do
          -- record usability of variable
          u <- (Int
    i Int -> IntSet -> Bool
    `VarSet.member`) (IntSet -> Bool) -> TerM IntSet -> TerM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TerM IntSet
    terGetUsableVars
          -- Andreas, 2017-07-26, issue #2331.
          -- The usability logic is refuted by bounded size quantification in terms.
          -- Thus, it is switched off (the infrastructure remains in place for now).
          if not u then return Order.unknown else do
          -- Only if usable:
          res <- isBounded i
          case res of
            BoundedSize
    BoundedNo  -> Order -> TerM Order
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown
            BoundedLt Term
    v -> Bool -> Order -> Order
    setUsability Bool
    u (Order -> Order) -> (Order -> Order) -> Order -> Order
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Order -> Order
    decrease Int
    1 (Order -> Order) -> TerM Order -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' Term
    v (Bool -> DeBruijnPattern -> Masked DeBruijnPattern
    forall a. Bool -> a -> Masked a
    Masked Bool
    m (DeBruijnPattern -> Masked DeBruijnPattern)
    -> DeBruijnPattern -> Masked DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> DeBruijnPattern
    forall a. a -> Pattern' a
    varP DBPatVar
    x)