    {-# LANGUAGE GADTs                      #-}

    {-# 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 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 (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.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.Utils.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 (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Field {}            -> Result -> TCM Result
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Primitive {}        -> Result -> TCM Result
    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
    _ 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 (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Import {}           -> Result -> TCM Result
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Pragma {}           -> Result -> TCM Result
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Open {}             -> Result -> TCM Result
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.PatternSynDef {}    -> Result -> TCM Result
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.Generalize {}       -> Result -> TCM Result
    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 (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
        A.RecDef DefInfo
    _ QName
    r UniverseCheck
    _ RecordDirectives
    _ DataDefParams
    _ Expr
    _ [Declaration]
    ds -> [Declaration] -> TCM Result
    forall {t :: * -> *}. Traversable t => t Declaration -> TCM Result
    termDecls [Declaration]
    ds
        -- 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__
      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)
    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 Delayed
    delayed [Clause]
    cs)   = [QName
    x]
        getName (A.RecDef DefInfo
    _ QName
    _ UniverseCheck
    _ RecordDirectives
    _ DataDefParams
    _ Expr
    _ [Declaration]
    ds)   = [Declaration] -> [QName]
    getNames [Declaration]
    ds
        getName (A.Mutual MutualInfo
    _ [Declaration]
    ds)             = [Declaration] -> [QName]
    getNames [Declaration]
    ds
        getName (A.Section Range
    _ 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 Expr
    _)    = [QName]
    xs
        getName (A.UnquoteDef [DefInfo]
    _ [QName]
    xs Expr
    _)       = [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 (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.
      MutualId
    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
    mutualBlock <- MutualId -> TCM MutualBlock
    lookupMutualBlock MutualId
    mid
      let allNames :: [QName]
    allNames = (QName -> Bool) -> [QName] -> [QName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (QName -> Bool) -> QName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Bool
    isAbsurdLambdaName) ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ Set QName -> [QName]
    forall a. Set a -> [a]
    Set.elems (Set QName -> [QName]) -> Set QName -> [QName]
    forall a b. (a -> b) -> a -> b
    $ MutualBlock -> Set QName
    mutualNames MutualBlock
    mutualBlock
          names :: [QName]
    names    = if [QName] -> Bool
    forall a. Null a => a -> Bool
    null [QName]
    names0 then [QName]
    allNames else [QName]
    names0
          i :: MutualInfo
    i        = MutualBlock -> MutualInfo
    mutualInfo MutualBlock
    mutualBlock

      -- We set the range to avoid panics when printing error messages.
      MutualInfo -> TCM Result -> TCM Result
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange MutualInfo
    i (TCM Result -> TCM Result) -> TCM Result -> TCM Result
    forall a b. (a -> b) -> a -> b
    $ do

      -- The following debug statement is part of a test case for Issue
      -- #3590.
      [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.mutual.id" Nat
    40 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "Termination checking mutual block " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MutualId -> [Char]
    forall a. Show a => a -> [Char]
    show MutualId
    mid
      [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.mutual" Nat
    10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Termination checking " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [QName] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [QName]
    allNames

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

        -- Trivially terminating (non-recursive)?
        Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([[QName]] -> Bool
    forall a. Null a => a -> Bool
    null [[QName]]
    sccs) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.warn.yes" Nat
    10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Trivially terminating: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [QName] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [QName]
    names

        -- Actual termination checking needed: go through SCCs.
        [Result] -> Result
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([Result] -> Result) -> TCMT IO [Result] -> TCM Result
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
         [[QName]] -> ([QName] -> TCM Result) -> TCMT IO [Result]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [[QName]]
    sccs (([QName] -> TCM Result) -> TCMT IO [Result])
    -> ([QName] -> TCM Result) -> TCMT IO [Result]
    forall a b. (a -> b) -> a -> b
    $ \ [QName]
    allNames -> do

         -- Set the mutual names in the termination environment.
         let namesSCC :: [QName]
    namesSCC = (QName -> Bool) -> [QName] -> [QName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ([QName]
    allNames [QName] -> QName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    `hasElem`) [QName]
    names
         let setNames :: TerEnv -> TerEnv
    setNames TerEnv
    e = TerEnv
    e
               { terMutual :: [QName]
    terMutual    = [QName]
    allNames
               , terUserNames :: [QName]
    terUserNames = [QName]
    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
    cutoff <- TerM CutOff
    terGetCutOff
               [Char] -> Nat -> [Char] -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.top" Nat
    10 ([Char] -> TerM ()) -> [Char] -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Termination checking " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [QName] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [QName]
    namesSCC [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                 [Char]
    " with cutoff=" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ CutOff -> [Char]
    forall a. Show a => a -> [Char]
    show CutOff
    cutoff [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "..."
               (TerEnv -> TerEnv) -> TerM Result -> TerM Result
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal TerEnv -> TerEnv
    setNames TerM Result
    cont

         -- New check currently only makes a difference for copatterns.
         -- Since it is slow, only invoke it if
         -- any of the definitions uses copatterns.
         Result
    res <- TCMT IO Bool -> TCM Result -> TCM Result -> TCM Result
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ([TCMT IO Bool] -> TCMT IO Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    orM ([TCMT IO Bool] -> TCMT IO Bool) -> [TCMT IO Bool] -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ (QName -> TCMT IO Bool) -> [QName] -> [TCMT IO Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCMT IO Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    usesCopatterns [QName]
    allNames)
             -- 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
    $ [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' [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')

         -- Record result of termination check in signature.
         -- If there are some termination errors, we collect them in
         -- the state and mark the definition as non-terminating so
         -- that it does not get unfolded
         let terminates :: Bool
    terminates = Result -> Bool
    forall a. Null a => a -> Bool
    null Result
    res
         [QName] -> (QName -> TCMT IO ()) -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [QName]
    allNames ((QName -> TCMT IO ()) -> TCMT IO ())
    -> (QName -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    q -> QName -> Bool -> TCMT IO ()
    setTerminates QName
    q Bool
    terminates
         Result -> TCM Result
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    res

    -- | @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
      [QName]
    allNames <- TerM [QName]
    terGetMutual
      let collect :: TerM Calls
    collect = [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' [QName]
    allNames QName -> TerM Calls
    termDef

      -- first try to termination check ignoring the dot patterns
      Calls
    calls1 <- TerM Calls
    collect
      [Char] -> Calls -> TerM ()
    reportCalls [Char]
    "no " Calls
    calls1

      CutOff
    cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = ?cutoff::CutOff
    CutOff
    cutoff
      Either CallPath ()
    r <- Either CallPath () -> TerM (Either CallPath ())
    forall a. a -> TerM a
    billToTerGraph (Either CallPath () -> TerM (Either CallPath ()))
    -> Either CallPath () -> TerM (Either CallPath ())
    forall a b. (a -> b) -> a -> b
    $ Calls -> Either CallPath ()
    forall cinfo.
    (Monoid cinfo, ?cutoff::CutOff) =>
    CallGraph cinfo -> Either cinfo ()
    Term.terminates Calls
    calls1
      Either CallPath ()
    r <-
           -- 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.
           TerM Bool
    -> TerM (Either CallPath ())
    -> TerM (Either CallPath ())
    -> TerM (Either CallPath ())
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Maybe Cubical -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Cubical -> Bool)
    -> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe Cubical
    optCubical (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) (Either CallPath () -> TerM (Either CallPath ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return Either CallPath ()
    r) {- else -} (TerM (Either CallPath ()) -> TerM (Either CallPath ()))
    -> TerM (Either CallPath ()) -> TerM (Either CallPath ())
    forall a b. (a -> b) -> a -> b
    $
           case Either CallPath ()
    r of
             r :: Either CallPath ()
    r@Right{} -> Either CallPath () -> TerM (Either CallPath ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return Either CallPath ()
    r
             Left{}    -> do
               -- Try again, but include the dot patterns this time.
               Calls
    calls2 <- Bool -> TerM Calls -> TerM Calls
    forall a. Bool -> TerM a -> TerM a
    terSetUseDotPatterns Bool
    True (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ TerM Calls
    collect
               [Char] -> Calls -> TerM ()
    reportCalls [Char]
    "" Calls
    calls2
               Either CallPath () -> TerM (Either CallPath ())
    forall a. a -> TerM a
    billToTerGraph (Either CallPath () -> TerM (Either CallPath ()))
    -> Either CallPath () -> TerM (Either CallPath ())
    forall a b. (a -> b) -> a -> b
    $ Calls -> Either CallPath ()
    forall cinfo.
    (Monoid cinfo, ?cutoff::CutOff) =>
    CallGraph cinfo -> Either cinfo ()
    Term.terminates Calls
    calls2

      -- @names@ is taken from the 'Abstract' syntax, so it contains only
      -- the names the user has declared.  This is for error reporting.
      [QName]
    names <- TerM [QName]
    terGetUserNames
      case Either CallPath ()
    r of
        Left CallPath
    calls -> Result -> TerM Result
    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
    $ [QName] -> [CallInfo] -> TerminationError
    terminationError [QName]
    names ([CallInfo] -> TerminationError) -> [CallInfo] -> TerminationError
    forall a b. (a -> b) -> a -> b
    $ CallPath -> [CallInfo]
    callInfos CallPath
    calls
        Right{} -> do
          TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.warn.yes" Nat
    2 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            [QName] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ([QName]
    names) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " does termination check"
          Result -> TerM Result
    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 :: [QName] -> [CallInfo] -> TerminationError
    terminationError :: [QName] -> [CallInfo] -> TerminationError
    terminationError [QName]
    names [CallInfo]
    calls = [QName] -> [CallInfo] -> TerminationError
    TerminationError [QName]
    names' [CallInfo]
    calls
      where
      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]
    names
      mentioned :: [QName]
    mentioned = (CallInfo -> QName) -> [CallInfo] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map CallInfo -> QName
    callInfoTarget [CallInfo]
    calls

    billToTerGraph :: a -> TerM a
    billToTerGraph :: forall a. a -> TerM a
    billToTerGraph a
    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 :: [Char] -> Calls -> TerM ()
    reportCalls [Char]
    no Calls
    calls = do
      CutOff
    cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = ?cutoff::CutOff
    CutOff
    cutoff

      -- We work in TCM exclusively.
      TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ do

        [Char] -> Nat -> [[Char]] -> TCMT IO ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Nat -> a -> m ()
    reportS [Char]
    "term.lex" Nat
    20
          [ [Char]
    "Calls (" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    no [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "dot patterns): " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Calls -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Calls
    calls
          ]

        -- Print the whole completion phase.
        [Char] -> Nat -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
    verboseS [Char]
    "term.matrices" Nat
    40 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
          let header :: [Char] -> [Char]
    header [Char]
    s = [[Char]] -> [Char]
    unlines
                [ Nat -> Char -> [Char]
    forall a. Nat -> a -> [a]
    replicate Nat
    n Char
    '='
                , Nat -> Char -> [Char]
    forall a. Nat -> a -> [a]
    replicate Nat
    k Char
    '=' [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> Char -> [Char]
    forall a. Nat -> a -> [a]
    replicate Nat
    k' Char
    '='
                , Nat -> Char -> [Char]
    forall a. Nat -> a -> [a]
    replicate Nat
    n Char
    '='
                ]
                where n :: Nat
    n  = Nat
    70
                      r :: Nat
    r  = Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - [Char] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Char]
    s
                      k :: Nat
    k  = Nat
    r Nat -> Nat -> Nat
    forall a. Integral a => a -> a -> a
    `div` Nat
    2
                      k' :: Nat
    k' = Nat
    r Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    k
          let report :: [Char] -> a -> m ()
    report [Char]
    s a
    cs = [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.matrices" Nat
    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
                [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text   ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    header [Char]
    s
                , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    cs0     = Calls
    calls
              step :: Calls -> TCMT IO (Either () 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
                [Char] -> Calls -> TCMT IO ()
    forall {m :: * -> *} {a}.
    (MonadDebug m, Pretty a) =>
    [Char] -> a -> m ()
    report [Char]
    " New call matrices " Calls
    new
                Either () Calls -> TCMT IO (Either () Calls)
    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'
          [Char] -> Calls -> TCMT IO ()
    forall {m :: * -> *} {a}.
    (MonadDebug m, Pretty a) =>
    [Char] -> a -> m ()
    report [Char]
    " Initial call matrices " Calls
    cs0
          (Calls -> TCMT IO (Either () Calls)) -> Calls -> TCMT IO ()
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m (Either b a)) -> a -> m b
    trampolineM Calls -> TCMT IO (Either () Calls)
    step Calls
    cs0

        -- Print the result of completion.
        let calls' :: Calls
    calls' = Calls -> Calls
    forall cinfo.
    (?cutoff::CutOff, Monoid cinfo) =>
    CallGraph cinfo -> CallGraph cinfo
    CallGraph.complete Calls
    calls
            idems :: [CallMatrixAug CallPath]
    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'
        --   ]
        [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.matrices" Nat
    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
    vcat
          [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Idempotent call matrices (" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    no [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "dot patterns):\n"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    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] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    "\n" ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (CallMatrixAug CallPath -> TCMT IO Doc)
    -> [CallMatrixAug CallPath] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map CallMatrixAug CallPath -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [CallMatrixAug CallPath]
    idems
          ]
        -- reportSDoc "term.matrices" 30 $ vcat
        --   [ text $ "Other call matrices (" ++ no ++ "dot patterns):"
        --   , nest 2 $ pretty $ CallGraph.fromList others
        --   ]
        () -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | @termFunction name@ checks @name@ for termination.

    termFunction :: QName -> TerM Result
    termFunction :: QName -> TerM Result
    termFunction QName
    name = do

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

      [QName]
    allNames <- TerM [QName]
    terGetMutual
      let index :: Nat
    index = Nat -> Maybe Nat -> Nat
    forall a. a -> Maybe a -> a
    fromMaybe Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Nat -> Nat) -> Maybe Nat -> Nat
    forall a b. (a -> b) -> a -> b
    $ QName -> [QName] -> Maybe Nat
    forall a. Eq a => a -> [a] -> Maybe Nat
    List.elemIndex QName
    name [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.
      Maybe QName
    target <- TCM (Maybe QName) -> TerM (Maybe QName)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Maybe QName) -> TerM (Maybe QName))
    -> TCM (Maybe QName) -> TerM (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ do Type -> TCM (Maybe QName)
    forall (tcm :: * -> *). MonadTCM tcm => Type -> tcm (Maybe QName)
    typeEndsInDef (Type -> TCM (Maybe QName))
    -> (Definition -> Type) -> Definition -> TCM (Maybe QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Type
    defType (Definition -> TCM (Maybe QName))
    -> TCMT IO Definition -> TCM (Maybe QName)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name
      Maybe QName -> TerM ()
    forall {tcm :: * -> *} {a}.
    (MonadTCM tcm, Pretty a) =>
    Maybe a -> tcm ()
    reportTarget Maybe QName
    target
      Maybe QName -> TerM Result -> TerM Result
    forall a. Maybe QName -> TerM a -> TerM a
    terSetTarget Maybe QName
    target (TerM Result -> TerM Result) -> TerM Result -> TerM Result
    forall a b. (a -> b) -> a -> b
    $ do

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

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

        -- First try to termination check ignoring the dot patterns
        Calls
    calls1 <- Bool -> TerM Calls -> TerM Calls
    forall a. Bool -> TerM a -> TerM a
    terSetUseDotPatterns Bool
    False (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ TerM Calls
    collect
        [Char] -> Calls -> TerM ()
    reportCalls [Char]
    "no " Calls
    calls1

        Either [CallInfo] ()
    r <- do
         CutOff
    cutoff <- TerM CutOff
    terGetCutOff
         let ?cutoff = ?cutoff::CutOff
    CutOff
    cutoff
         Either CallPath ()
    r <- Either CallPath () -> TerM (Either CallPath ())
    forall a. a -> TerM a
    billToTerGraph (Either CallPath () -> TerM (Either CallPath ()))
    -> Either CallPath () -> TerM (Either CallPath ())
    forall a b. (a -> b) -> a -> b
    $ (Nat -> Bool) -> Calls -> Either CallPath ()
    forall cinfo.
    (Monoid cinfo, ?cutoff::CutOff) =>
    (Nat -> Bool) -> CallGraph cinfo -> Either cinfo ()
    Term.terminatesFilter (Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    index) Calls
    calls1
         case Either CallPath ()
    r of
           Right () -> Either [CallInfo] () -> TerM (Either [CallInfo] ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either [CallInfo] () -> TerM (Either [CallInfo] ()))
    -> Either [CallInfo] () -> TerM (Either [CallInfo] ())
    forall a b. (a -> b) -> a -> b
    $ () -> Either [CallInfo] ()
    forall a b. b -> Either a b
    Right ()
           Left{}    -> do
             -- Try again, but include the dot patterns this time.
             Calls
    calls2 <- Bool -> TerM Calls -> TerM Calls
    forall a. Bool -> TerM a -> TerM a
    terSetUseDotPatterns Bool
    True (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ TerM Calls
    collect
             [Char] -> Calls -> TerM ()
    reportCalls [Char]
    "" Calls
    calls2
             Either [CallInfo] () -> TerM (Either [CallInfo] ())
    forall a. a -> TerM a
    billToTerGraph (Either [CallInfo] () -> TerM (Either [CallInfo] ()))
    -> Either [CallInfo] () -> TerM (Either [CallInfo] ())
    forall a b. (a -> b) -> a -> b
    $ (CallPath -> [CallInfo])
    -> Either CallPath () -> Either [CallInfo] ()
    forall a c b. (a -> c) -> Either a b -> Either c b
    mapLeft CallPath -> [CallInfo]
    callInfos (Either CallPath () -> Either [CallInfo] ())
    -> Either CallPath () -> Either [CallInfo] ()
    forall a b. (a -> b) -> a -> b
    $ (Nat -> Bool) -> Calls -> Either CallPath ()
    forall cinfo.
    (Monoid cinfo, ?cutoff::CutOff) =>
    (Nat -> Bool) -> CallGraph cinfo -> Either cinfo ()
    Term.terminatesFilter (Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    index) Calls
    calls2

        [QName]
    names <- TerM [QName]
    terGetUserNames
        case Either [CallInfo] ()
    r of
          Left [CallInfo]
    calls -> Result -> TerM Result
    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
    $ [QName] -> [CallInfo] -> TerminationError
    terminationError ([QName
    name] [QName] -> [QName] -> [QName]
    forall a. Eq a => [a] -> [a] -> [a]
    `List.intersect` [QName]
    names) [CallInfo]
    calls
          Right () -> do
            TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.warn.yes" Nat
    2 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
              QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    name [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " does termination check"
            Result -> TerM Result
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result
    forall a. Monoid a => a
    mempty
       where
         reportTarget :: Maybe a -> tcm ()
    reportTarget Maybe a
    r = TCMT IO () -> tcm ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> tcm ()) -> TCMT IO () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $
           [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.target" Nat
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  target type " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
             Maybe a -> [Char] -> (a -> [Char]) -> [Char]
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe a
    r [Char]
    "not recognized" (\ a
    q ->
               [Char]
    "ends in " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow a
    q)

    -- | 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 (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 Telescope
    _ Type
    core <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    core of
        Def QName
    d Elims
    vs -> Maybe QName -> TCM (Maybe QName)
    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 (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

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

      TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.def.fun" Nat
    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
    prettyTCM QName
    name
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    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 (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.def.fun" Nat
    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
    prettyTCM QName
    name
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    prettyTCM Type
    t
            ]

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

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

        -- If the result should be disregarded, set all calls to unguarded.
        TerM Bool -> (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall (m :: * -> *) a.
    Monad m =>
    m Bool -> (m a -> m a) -> m a -> m a
    applyWhenM TerM Bool
    terGetMaskResult 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
    $ do

          case Definition -> Defn
    theDef Definition
    def of
            Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cls, funDelayed :: Defn -> Delayed
    funDelayed = Delayed
    delayed } ->
              Delayed -> TerM Calls -> TerM Calls
    forall a. Delayed -> TerM a -> TerM a
    terSetDelayed Delayed
    delayed (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ [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 (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
                  else Clause -> TerM Calls
    termClause Clause
    cl

            Defn
    _ -> Calls -> TerM Calls
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
      where
        hasDefP :: [NamedArg DeBruijnPattern] -> Bool
        hasDefP :: NAPs -> Bool
    hasDefP NAPs
    ps = Any -> Bool
    getAny (Any -> Bool) -> Any -> Bool
    forall a b. (a -> b) -> a -> b
    $ ((DeBruijnPattern -> Any) -> NAPs -> Any)
    -> NAPs -> (DeBruijnPattern -> Any) -> Any
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (DeBruijnPattern -> Any) -> NAPs -> Any
    forall a b m.
    (PatternLike a b, Monoid m) =>
    (Pattern' a -> m) -> b -> m
    foldPattern NAPs
    ps ((DeBruijnPattern -> Any) -> Any)
    -> (DeBruijnPattern -> Any) -> Any
    forall a b. (a -> b) -> a -> b
    $ \ (DeBruijnPattern
    x :: DeBruijnPattern) ->
                      case DeBruijnPattern
    x of
                        DefP{} -> Bool -> Any
    Any Bool
    True
                        DeBruijnPattern
    _      -> Bool -> Any
    Any Bool
    False

    -- | 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 (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 :: Nat -> Type -> TerM Calls
    loop Nat
    n Type
    t = do
        MaskedDeBruijnPatterns
    ps <- Nat -> TerM MaskedDeBruijnPatterns
    forall {f :: * -> *}.
    MonadTCEnv f =>
    Nat -> f MaskedDeBruijnPatterns
    mkPats Nat
    n
        [Char] -> Nat -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.type" Nat
    60 (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
          [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "termType " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [Char]
    forall a. Show a => a -> [Char]
    show Nat
    n [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " with " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [Char]
    forall a. Show a => a -> [Char]
    show (MaskedDeBruijnPatterns -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length MaskedDeBruijnPatterns
    ps) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " patterns"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "looking at type " 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
    prettyTCM Type
    t
          ]
        Telescope
    tel <- TerM Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope  -- Andreas, 2018-11-15, issue #3394, forgotten initialization of terSizeDepth
        MaskedDeBruijnPatterns -> TerM Calls -> TerM Calls
    forall a. MaskedDeBruijnPatterns -> TerM a -> TerM a
    terSetPatterns MaskedDeBruijnPatterns
    ps (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TerM Calls -> TerM Calls
    forall a. Telescope -> TerM a -> TerM a
    terSetSizeDepth Telescope
    tel (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ do
          Type
    -> (Type -> TerM Calls)
    -> (Dom Type -> Abs Type -> TerM Calls)
    -> TerM Calls
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPiType Type
    t {-then-} Type -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract {-else-} ((Dom Type -> Abs Type -> TerM Calls) -> TerM Calls)
    -> (Dom Type -> Abs Type -> TerM Calls) -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ \ Dom Type
    dom Abs Type
    absB -> do
            Dom Type -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Dom Type
    dom TerM Calls -> TerM Calls -> TerM Calls
    forall a. Monoid a => a -> a -> a
    `mappend` Dom Type -> Abs Type -> (Type -> TerM Calls) -> TerM Calls
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs Dom Type
    dom Abs Type
    absB (Nat -> Type -> TerM Calls
    loop (Nat -> Type -> TerM Calls) -> Nat -> Type -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $! Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)

      -- create n variable patterns
      mkPats :: Nat -> f MaskedDeBruijnPatterns
    mkPats Nat
    n  = (Nat -> Name -> Masked DeBruijnPattern)
    -> [Nat] -> [Name] -> MaskedDeBruijnPatterns
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Nat -> Name -> Masked DeBruijnPattern
    forall {a}. Pretty a => Nat -> a -> Masked DeBruijnPattern
    mkPat (Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom Nat
    n) ([Name] -> MaskedDeBruijnPatterns)
    -> f [Name] -> f MaskedDeBruijnPatterns
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f [Name]
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
    getContextNames
      mkPat :: Nat -> a -> Masked DeBruijnPattern
    mkPat Nat
    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
    $ [Char] -> Nat -> DBPatVar
    DBPatVar (a -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow a
    x) Nat
    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
      ([Bool]
    ds, Bool
    d) <- TCM ([Bool], Bool) -> TerM ([Bool], Bool)
    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 Telescope
    tel Type
    core <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
        -- Check argument types
        [Bool]
    ds <- [Dom ([Char], Type)]
    -> (Dom ([Char], Type) -> TCMT IO Bool) -> TCMT IO [Bool]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel) ((Dom ([Char], Type) -> TCMT IO Bool) -> TCMT IO [Bool])
    -> (Dom ([Char], Type) -> TCMT IO Bool) -> TCMT IO [Bool]
    forall a b. (a -> b) -> a -> b
    $ \ Dom ([Char], Type)
    t -> do
          TelV Telescope
    _ Type
    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
    $ ([Char], Type) -> Type
    forall a b. (a, b) -> b
    snd (([Char], Type) -> Type) -> ([Char], Type) -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom ([Char], Type) -> ([Char], Type)
    forall t e. Dom' t e -> e
    unDom Dom ([Char], Type)
    t
          Bool
    d <- (Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe QName -> Bool) -> TCM (Maybe QName) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCM (Maybe QName)
    isDataOrRecord (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t)) TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` (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
    <$> Type -> TCMT IO (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType Type
    t)
          Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    d (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.mask" Nat
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
              TCMT IO Doc
    "argument type "
                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
    prettyTCM Type
    t
                TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " is not data or record type, ignoring structural descent for --without-K"
          Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    d
        -- Check result types
        Bool
    d  <- Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe QName -> Bool)
    -> (Type -> TCM (Maybe QName)) -> Type -> TCMT IO Bool
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Term -> TCM (Maybe QName)
    isDataOrRecord (Term -> TCM (Maybe QName))
    -> (Type -> Term) -> Type -> TCM (Maybe QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> TCMT IO Bool) -> Type -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ Type
    core
        Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    d (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.mask" Nat
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "result type is not data or record type, ignoring guardedness for --without-K"
        ([Bool], Bool) -> TCM ([Bool], Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Bool]
    ds, Bool
    d)
      [Bool] -> TerM a -> TerM a
    forall a. [Bool] -> TerM a -> TerM a
    terSetMaskArgs ([Bool]
    ds [Bool] -> [Bool] -> [Bool]
    forall a. [a] -> [a] -> [a]
    ++ Bool -> [Bool]
    forall a. a -> [a]
    repeat Bool
    True) (TerM a -> TerM a) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ Bool -> TerM a -> TerM a
    forall a. Bool -> TerM a -> TerM a
    terSetMaskResult Bool
    d (TerM a -> TerM a) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ TerM a
    cont

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

    targetElem :: [Target] -> TerM Bool
    targetElem :: [QName] -> TerM Bool
    targetElem [QName]
    ds = Bool -> (QName -> Bool) -> Maybe QName -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False (QName -> [QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    ds) (Maybe QName -> Bool) -> TerM (Maybe QName) -> TerM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TerM (Maybe QName)
    terGetTarget

    {-
    -- | The target type of the considered recursive definition.
    data Target
      = Set        -- ^ Constructing a Set (only meaningful with 'guardingTypeConstructors').
      | Data QName -- ^ Constructing a coinductive or mixed type (could be data or record).
      deriving (Eq, Show)

    -- | Check wether a 'Target" corresponds to the current one.
    matchingTarget :: DBPConf -> Target -> TCM Bool
    matchingTarget conf t = maybe (return True) (match t) (currentTarget conf)
      where
        match Set      Set       = return True
        match (Data d) (Data d') = mutuallyRecursive d d'
        match _ _                = return 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 (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 (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)
    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 (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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        -- Constructors.
        Con ConHead
    c ConInfo
    _ Elims
    args -> 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 (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
          Maybe QName
    suc <- TerM (Maybe QName)
    terGetSizeSuc
          if 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 then ConHead -> ConPatternInfo -> NAPs -> DeBruijnPattern
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    s DataOrRecord
    IsData Induction
    Inductive []) 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 (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
    arg]
           else DeBruijnPattern -> TerM DeBruijnPattern
    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
        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 Nat
    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
    . ([Char] -> Nat -> DBPatVar
    `DBPatVar` Nat
    i) ([Char] -> DBPatVar) -> (Name -> [Char]) -> Name -> DBPatVar
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (Name -> DeBruijnPattern) -> TerM Name -> TerM DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat -> TerM Name
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Nat -> m Name
    nameOfBV Nat
    i
        Lit Literal
    l       -> DeBruijnPattern -> TerM DeBruijnPattern
    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 [Char]
    s Elims
    _   -> [Char] -> TerM DeBruijnPattern
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    s
        Term
    t           -> DeBruijnPattern -> TerM DeBruijnPattern
    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

    -- | Extract recursive calls from one clause.
    termClause :: Clause -> TerM Calls
    termClause :: Clause -> TerM Calls
    termClause Clause
    clause = do
      Clause{ clauseTel :: Clause -> Telescope
    clauseTel = Telescope
    tel, namedClausePats :: Clause -> NAPs
    namedClausePats = NAPs
    ps, clauseBody :: Clause -> Maybe Term
    clauseBody = Maybe Term
    body } <- Clause -> TerM Clause
    forall (tcm :: * -> *). MonadTCM tcm => Clause -> tcm Clause
    etaExpandClause Clause
    clause
      TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.check.clause" Nat
    25 (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
    vcat
        [ TCMT IO Doc
    "termClause"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    tel
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "ps  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ NAPs -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
    prettyTCMPatternList NAPs
    ps
        ]
      Maybe Term -> (Term -> TerM Calls) -> TerM Calls
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    t a -> (a -> m b) -> m b
    forM' Maybe Term
    body ((Term -> TerM Calls) -> TerM Calls)
    -> (Term -> TerM Calls) -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ \ Term
    v -> Telescope -> TerM Calls -> TerM Calls
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> 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.
        NAPs
    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.
        NAPs
    ps <- (DeBruijnPattern -> TerM DeBruijnPattern) -> NAPs -> TerM NAPs
    forall a b (m :: * -> *).
    (PatternLike a b, Monad m) =>
    (Pattern' a -> m (Pattern' a)) -> b -> m b
    preTraversePatternM DeBruijnPattern -> TerM DeBruijnPattern
    stripCoCon NAPs
    ps
        -- Mask non-data arguments.
        MaskedDeBruijnPatterns
    mdbpats <- [DeBruijnPattern] -> TerM MaskedDeBruijnPatterns
    maskNonDataArgs ([DeBruijnPattern] -> TerM MaskedDeBruijnPatterns)
    -> [DeBruijnPattern] -> TerM MaskedDeBruijnPatterns
    forall a b. (a -> b) -> a -> b
    $ (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
    -> NAPs -> [DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg NAPs
    ps
        MaskedDeBruijnPatterns -> TerM Calls -> TerM Calls
    forall a. MaskedDeBruijnPatterns -> TerM a -> TerM a
    terSetPatterns MaskedDeBruijnPatterns
    mdbpats (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ do
          Telescope -> TerM Calls -> TerM Calls
    forall a. Telescope -> TerM a -> TerM a
    terSetSizeDepth Telescope
    tel (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ do
            Term -> TerM ()
    reportBody Term
    v
            Term -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Term
    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 (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    p
        stripCoCon :: DeBruijnPattern -> TerM DeBruijnPattern
    stripCoCon DeBruijnPattern
    p = case DeBruijnPattern
    p of
          ConP (ConHead QName
    c DataOrRecord
    _ Induction
    _ [Arg QName]
    _) ConPatternInfo
    _ NAPs
    _ -> do
            TerM Bool
    -> TerM DeBruijnPattern
    -> TerM DeBruijnPattern
    -> TerM DeBruijnPattern
    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)
    terGetSizeSuc) (DeBruijnPattern -> TerM DeBruijnPattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    p) (TerM DeBruijnPattern -> TerM DeBruijnPattern)
    -> TerM DeBruijnPattern -> TerM DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ {- else -} do
            QName -> TerM Induction
    forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Induction
    whatInduction QName
    c TerM Induction
    -> (Induction -> TerM DeBruijnPattern) -> TerM DeBruijnPattern
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Induction
    Inductive   -> DeBruijnPattern -> TerM DeBruijnPattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    p
              Induction
    CoInductive -> DeBruijnPattern -> TerM DeBruijnPattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    unusedVar
          DeBruijnPattern
    _ -> DeBruijnPattern -> TerM DeBruijnPattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return DeBruijnPattern
    p
        reportBody :: Term -> TerM ()
        reportBody :: Term -> TerM ()
    reportBody Term
    v = [Char] -> Nat -> TerM () -> TerM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
    verboseS [Char]
    "term.check.clause" Nat
    6 (TerM () -> TerM ()) -> TerM () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ do
          QName
    f       <- TerM QName
    terGetCurrent
          Delayed
    delayed <- TerM Delayed
    terGetDelayed
          MaskedDeBruijnPatterns
    pats    <- TerM MaskedDeBruijnPatterns
    terGetPatterns
          TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.check.clause" Nat
    6 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
            [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "termination checking " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                        (if Delayed
    delayed Delayed -> Delayed -> Bool
    forall a. Eq a => a -> a -> Bool
    == Delayed
    Delayed then [Char]
    "delayed " else [Char]
    "") [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                        [Char]
    "clause 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
    prettyTCM QName
    f
                , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "lhs:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((Masked DeBruijnPattern -> TCMT IO Doc)
    -> MaskedDeBruijnPatterns -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Masked DeBruijnPattern -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MaskedDeBruijnPatterns
    pats)
                , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "rhs:" 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
    prettyTCM Term
    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 [Char]
    _ a
    a) = a -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract a
    a
      extract (Abs [Char]
    x a
    a)   = [Char] -> TerM Calls -> TerM Calls
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext [Char]
    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 (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 (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 (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.sort" Nat
    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
    prettyTCM Sort
    s
          [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.sort" Nat
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "s = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Sort -> [Char]
    forall a. Show a => a -> [Char]
    show Sort
    s)
        case Sort
    s of
          Inf IsFibrant
    f Integer
    n    -> Calls -> TerM Calls
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          Sort
    SizeUniv   -> Calls -> TerM Calls
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          Sort
    LockUniv   -> Calls -> TerM Calls
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          Type 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
          Prop 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
          SSet 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
          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 (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          DefS QName
    d Elims
    es  -> Calls -> TerM Calls
    forall (m :: * -> *) a. Monad m => a -> m a
    return Calls
    forall a. Null a => a
    empty
          DummyS{}   -> Calls -> TerM Calls
    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)

    -- | 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
    cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = ?cutoff::CutOff
    CutOff
    cutoff
      [(Arg Term, Bool)]
    -> ((Arg Term, Bool) -> TerM Calls) -> TerM Calls
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    t a -> (a -> m b) -> m b
    forM' [(Arg Term, Bool)]
    args (((Arg Term, Bool) -> TerM Calls) -> TerM Calls)
    -> ((Arg Term, Bool) -> TerM Calls) -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ \ (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

        QName
    f       <- TerM QName
    terGetCurrent
        [QName]
    names   <- TerM [QName]
    terGetMutual
        Order
    guarded <- TerM Order
    terGetGuarded

        -- let gArgs = Def g es0
        TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.function" Nat
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "termination checking function 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
    prettyTCM (QName -> Elims -> Term
    Def QName
    g Elims
    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.
        Bool
    isProj <- QName -> TerM Bool
    forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Bool
    isProjectionButNotCoinductive QName
    g
        let unguards :: [Order]
    unguards = Order -> [Order]
    forall a. a -> [a]
    repeat Order
    Order.unknown
        let guards :: [Order]
    guards = Bool -> ([Order] -> [Order]) -> [Order] -> [Order]
    forall a. Bool -> (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 :: [Term]
    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
    calls <- [(Order, Term)] -> ((Order, Term) -> TerM Calls) -> TerM Calls
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    t a -> (a -> m b) -> m b
    forM' ([Order] -> [Term] -> [(Order, Term)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Order]
    guards [Term]
    args) (((Order, Term) -> TerM Calls) -> TerM Calls)
    -> ((Order, Term) -> TerM Calls) -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ \ (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.

        TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.found.call" Nat
    20 (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
    "found call from" 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
    prettyTCM QName
    f
              , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "to" 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
    prettyTCM QName
    g
              ]

        -- insert this call into the call list
        case QName -> [QName] -> Maybe Nat
    forall a. Eq a => a -> [a] -> Maybe Nat
    List.elemIndex QName
    g [QName]
    names of

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

           -- call is to one of the mutally recursive functions
           Just Nat
    gInd -> do
             Delayed
    delayed <- TerM Delayed
    terGetDelayed
             -- 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.
             Elims
    es <- -- ifM terGetHaveInlinedWith (return es0) {-else-} $
               TCM Elims -> TerM Elims
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Elims -> TerM Elims) -> TCM Elims -> TerM Elims
    forall a b. (a -> b) -> a -> b
    $ Elims -> (Elim -> TCMT IO Elim) -> TCM Elims
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM Elims
    es0 ((Elim -> TCMT IO Elim) -> TCM Elims)
    -> (Elim -> TCMT IO Elim) -> TCM Elims
    forall a b. (a -> b) -> a -> b
    $
                 -- 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.
                 (Term -> TCM Term) -> Elim -> TCMT IO Elim
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Term -> TCM Term
    reduceCon (Elim -> TCMT IO Elim)
    -> (Elim -> TCMT IO Elim) -> Elim -> TCMT IO Elim
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Elim -> TCMT IO Elim
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    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
             (Nat
    nrows, Nat
    ncols, [[Order]]
    matrix) <- Account (BenchPhase TerM)
    -> TerM (Nat, Nat, [[Order]]) -> TerM (Nat, Nat, [[Order]])
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    billTo [BenchPhase TerM
    Phase
    Benchmark.Termination, BenchPhase TerM
    Phase
    Benchmark.Compare] (TerM (Nat, Nat, [[Order]]) -> TerM (Nat, Nat, [[Order]]))
    -> TerM (Nat, Nat, [[Order]]) -> TerM (Nat, Nat, [[Order]])
    forall a b. (a -> b) -> a -> b
    $
               Elims -> TerM (Nat, Nat, [[Order]])
    compareArgs Elims
    es
             -- only a delayed definition can be guarded
             let ifDelayed :: Order -> Order
    ifDelayed Order
    o | Order -> Bool
    Order.decreasing Order
    o Bool -> Bool -> Bool
    && Delayed
    delayed Delayed -> Delayed -> Bool
    forall a. Eq a => a -> a -> Bool
    == Delayed
    NotDelayed = Order
    Order.le
                             | Bool
    otherwise                                  = Order
    o
             TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.guardedness" Nat
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
               [Char]
    "composing with guardedness " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Order -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Order
    guarded [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
               [Char]
    " counting as " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Order -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (Order -> Order
    ifDelayed Order
    guarded)
             CutOff
    cutoff <- TerM CutOff
    terGetCutOff
             let ?cutoff = ?cutoff::CutOff
    CutOff
    cutoff
             let matrix' :: [[Order]]
    matrix' = (?cutoff::CutOff) => Order -> [[Order]] -> [[Order]]
    Order -> [[Order]] -> [[Order]]
    composeGuardedness (Order -> Order
    ifDelayed 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.
             Closure Term
    doc <- TCM (Closure Term) -> TerM (Closure Term)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Closure Term) -> TerM (Closure Term))
    -> TCM (Closure Term) -> TerM (Closure Term)
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TCM (Closure Term) -> TCM (Closure Term)
    forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
    withCurrentModule (QName -> ModuleName
    qnameModule QName
    g) (TCM (Closure Term) -> TCM (Closure Term))
    -> TCM (Closure Term) -> TCM (Closure Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> TCM (Closure Term)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure (Term -> TCM (Closure Term)) -> Term -> TCM (Closure Term)
    forall a b. (a -> b) -> a -> b
    $
               QName -> Elims -> Term
    Def QName
    g (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Elim -> Bool) -> Elims -> Elims
    forall a. (a -> Bool) -> [a] -> [a]
    List.dropWhileEnd ((Origin
    Inserted Origin -> Origin -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Origin -> Bool) -> (Elim -> Origin) -> Elim -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin) Elims
    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 :: Nat
    src  = Nat -> Maybe Nat -> Nat
    forall a. a -> Maybe a -> a
    fromMaybe Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Nat -> Nat) -> Maybe Nat -> Nat
    forall a b. (a -> b) -> a -> b
    $ QName -> [QName] -> Maybe Nat
    forall a. Eq a => a -> [a] -> Maybe Nat
    List.elemIndex QName
    f [QName]
    names
                 tgt :: Nat
    tgt  = Nat
    gInd
                 cm :: CallMatrix
    cm   = Nat -> Nat -> [[Order]] -> CallMatrix
    makeCM Nat
    ncols Nat
    nrows [[Order]]
    matrix'
                 info :: CallPath
    info = [CallInfo] -> CallPath
    CallPath [CallInfo :: QName -> Range -> Closure Term -> CallInfo
    CallInfo
                          { callInfoTarget :: QName
    callInfoTarget = QName
    g
                          , callInfoRange :: Range
    callInfoRange  = QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    g
                          , callInfoCall :: Closure Term
    callInfoCall   = Closure Term
    doc
                          }]
             [Char] -> Nat -> TerM () -> TerM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
    verboseS [Char]
    "term.kept.call" Nat
    5 (TerM () -> TerM ()) -> TerM () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ do
               MaskedDeBruijnPatterns
    pats <- TerM MaskedDeBruijnPatterns
    terGetPatterns
               [Char] -> Nat -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.kept.call" Nat
    5 (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
    "kept call from" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    f) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep ((Masked DeBruijnPattern -> TCMT IO Doc)
    -> MaskedDeBruijnPatterns -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Masked DeBruijnPattern -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MaskedDeBruijnPatterns
    pats)
                 , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "to" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    g) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                             [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (TCMT IO Doc -> TCMT IO Doc)
    -> (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM) [Term]
    args)
                 , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "call matrix (with guardedness): "
                 , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ CallMatrix -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty CallMatrix
    cm
                 ]
             Calls -> TerM Calls
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Calls -> TerM Calls) -> Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ Nat -> Nat -> CallMatrix -> CallPath -> Calls -> Calls
    forall cinfo.
    Nat
    -> Nat -> CallMatrix -> cinfo -> CallGraph cinfo -> CallGraph cinfo
    CallGraph.insert Nat
    src Nat
    tgt CallMatrix
    cm CallPath
    info Calls
    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
    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 (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
      [Char] -> Nat -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.reduce" Nat
    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
    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 -> [QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    notElem QName
    g ([QName] -> Bool) -> TerM [QName] -> TerM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TerM [QName]
    terGetMutual) TerM Calls
    fallback {-else-} (TerM Calls -> TerM Calls) -> TerM Calls -> TerM Calls
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Nat -> [Char] -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.reduce" Nat
    40 ([Char] -> TerM ()) -> [Char] -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "This call is in the current SCC!"

      -- Then, collect its non-recursive clauses.
      [Clause]
    cls <- TCM [Clause] -> TerM [Clause]
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [Clause] -> TerM [Clause]) -> TCM [Clause] -> TerM [Clause]
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM [Clause]
    getNonRecursiveClauses QName
    g
      [Char] -> Nat -> [Char] -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.reduce" Nat
    40 ([Char] -> TerM ()) -> [Char] -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unwords [ [Char]
    "Function has", Nat -> [Char]
    forall a. Show a => a -> [Char]
    show ([Clause] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Clause]
    cls), [Char]
    "non-recursive exact clauses"]
      [Char] -> Nat -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.reduce" Nat
    80 (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
    $ (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NamedClause -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (NamedClause -> TCMT IO Doc)
    -> (Clause -> NamedClause) -> Clause -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Bool -> Clause -> NamedClause
    NamedClause QName
    g Bool
    True) [Clause]
    cls
      [Char] -> Nat -> [Char] -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn  [Char]
    "term.reduce" Nat
    80 ([Char] -> TerM ())
    -> (SmallSet AllowedReduction -> [Char])
    -> SmallSet AllowedReduction
    -> TerM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char]
    "allowed reductions = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++) ([Char] -> [Char])
    -> (SmallSet AllowedReduction -> [Char])
    -> SmallSet AllowedReduction
    -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [AllowedReduction] -> [Char]
    forall a. Show a => a -> [Char]
    show ([AllowedReduction] -> [Char])
    -> (SmallSet AllowedReduction -> [AllowedReduction])
    -> SmallSet AllowedReduction
    -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SmallSet AllowedReduction -> [AllowedReduction]
    forall a. SmallSetElement a => SmallSet a -> [a]
    SmallSet.elems
        (SmallSet AllowedReduction -> TerM ())
    -> TerM (SmallSet AllowedReduction) -> TerM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (TCEnv -> SmallSet AllowedReduction)
    -> TerM (SmallSet AllowedReduction)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> SmallSet AllowedReduction
    envAllowedReductions

      -- Finally, try to reduce with the non-recursive clauses (and no rewrite rules).
      Reduced (Blocked Term) Term
    r <- TCM (Reduced (Blocked Term) Term)
    -> TerM (Reduced (Blocked Term) Term)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Reduced (Blocked Term) Term)
     -> TerM (Reduced (Blocked Term) Term))
    -> TCM (Reduced (Blocked Term) Term)
    -> TerM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ (SmallSet AllowedReduction -> SmallSet AllowedReduction)
    -> TCM (Reduced (Blocked Term) Term)
    -> TCM (Reduced (Blocked Term) Term)
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (SmallSet AllowedReduction -> SmallSet AllowedReduction)
    -> m a -> m a
    modifyAllowedReductions (AllowedReduction
    -> SmallSet AllowedReduction -> SmallSet AllowedReduction
    forall a. SmallSetElement a => a -> SmallSet a -> SmallSet a
    SmallSet.delete AllowedReduction
    UnconfirmedReductions) (TCM (Reduced (Blocked Term) Term)
     -> TCM (Reduced (Blocked Term) Term))
    -> TCM (Reduced (Blocked Term) Term)
    -> TCM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $
        ReduceM (Reduced (Blocked Term) Term)
    -> TCM (Reduced (Blocked Term) Term)
    forall a. ReduceM a -> TCM a
    runReduceM (ReduceM (Reduced (Blocked Term) Term)
     -> TCM (Reduced (Blocked Term) Term))
    -> ReduceM (Reduced (Blocked Term) Term)
    -> TCM (Reduced (Blocked Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Term
    -> [Clause]
    -> RewriteRules
    -> MaybeReducedElims
    -> ReduceM (Reduced (Blocked Term) Term)
    appDefE' Term
    v0 [Clause]
    cls [] ((Elim -> MaybeReduced Elim) -> Elims -> MaybeReducedElims
    forall a b. (a -> b) -> [a] -> [b]
    map Elim -> MaybeReduced Elim
    forall a. a -> MaybeReduced a
    notReduced Elims
    es)
      case Reduced (Blocked Term) Term
    r of
        NoReduction{}    -> TerM Calls
    fallback
        YesReduction Simplification
    _ Term
    v -> do
          [Char] -> Nat -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.reduce" Nat
    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:"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    prettyTCM Term
    v0
            ]
          [Char] -> Nat -> TerM () -> TerM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Nat -> m () -> m ()
    verboseS [Char]
    "term.reduce" Nat
    5 (TerM () -> TerM ()) -> TerM () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TerM ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "termination-checker-reduced-nonrecursive-call"
          Term -> TerM Calls
    continue Term
    v

    getNonRecursiveClauses :: QName -> TCM [Clause]
    getNonRecursiveClauses :: QName -> TCM [Clause]
    getNonRecursiveClauses QName
    q =
      (Clause -> Bool) -> [Clause] -> [Clause]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Bool -> Bool -> Bool)
    -> (Clause -> Bool) -> (Clause -> Bool) -> Clause -> Bool
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 Bool -> Bool -> Bool
    (&&) Clause -> Bool
    nonrec Clause -> Bool
    exact) ([Clause] -> [Clause])
    -> (Definition -> [Clause]) -> Definition -> [Clause]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> [Clause]
    defClauses (Definition -> [Clause]) -> TCMT IO Definition -> TCM [Clause]
    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
    q
      where
      nonrec :: Clause -> Bool
    nonrec = Bool -> (Bool -> Bool) -> Maybe Bool -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False Bool -> Bool
    not (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Bool
    clauseRecursive
      exact :: Clause -> Bool
    exact  = Bool -> Maybe Bool -> Bool
    forall a. a -> Maybe a -> a
    fromMaybe Bool
    False (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Bool
    clauseExact

    -- | Extract recursive calls from a term.

    instance ExtractCalls Term where
      extract :: Term -> TerM Calls
    extract Term
    t = do
        TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.check.term" Nat
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    prettyTCM Term
    t

        -- Instantiate top-level MetaVar.
        Term
    t <- TCM Term -> TerM Term
    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 (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    t
        case Term
    t of

          -- 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.
            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
    True

            -- 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 (m :: * -> *) a. Monad m => a -> m a
    return Induction
    Inductive
                coinductive :: TerM Induction
    coinductive = Induction -> TerM Induction
    forall (m :: * -> *) a. Monad m => a -> m a
    return Induction
    CoInductive
            Induction
    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
              if DataOrRecord
    dataOrRec DataOrRecord -> DataOrRecord -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataOrRecord
    IsData then TerM Induction
    inductive else do
              TerM (Maybe (QName, Defn))
    -> TerM Induction
    -> ((QName, Defn) -> TerM Induction)
    -> TerM Induction
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (TCM (Maybe (QName, Defn)) -> TerM (Maybe (QName, Defn))
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Maybe (QName, Defn)) -> TerM (Maybe (QName, Defn)))
    -> TCM (Maybe (QName, Defn)) -> TerM (Maybe (QName, Defn))
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM (Maybe (QName, Defn))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, Defn))
    isRecordConstructor QName
    c) TerM Induction
    inductive (((QName, Defn) -> TerM Induction) -> TerM Induction)
    -> ((QName, Defn) -> TerM Induction) -> TerM Induction
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    q, Defn
    def) -> do
                [Char] -> Nat -> [Char] -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "term.check.term" Nat
    50 ([Char] -> TerM ()) -> [Char] -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "constructor " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    c [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " has record type " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q
                if Defn -> Maybe Induction
    recInduction Defn
    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
                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
    $ Defn -> Maybe [QName]
    recMutual Defn
    def)
                   {-then-} TerM Induction
    coinductive
                   {-else-} TerM Induction
    inductive
            QName -> Induction -> [(Arg Term, Bool)] -> TerM Calls
    constructor QName
    c Induction
    ind [(Arg Term, Bool)]
    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 Nat
    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. Destroys guardedness.
          Pi Dom Type
    a (Abs [Char]
    x Type
    b) ->
            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
    $
            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 Type -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Dom Type
    a TerM (Calls -> Calls) -> TerM Calls -> TerM Calls
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> do
              Dom Type
    a <- Dom Type -> TerM (Dom Type)
    forall (tcm :: * -> *). MonadTCM tcm => Dom Type -> tcm (Dom Type)
    maskSizeLt Dom Type
    a  -- OR: just do not add a to the context!
              ([Char], Dom Type) -> TerM Calls -> TerM Calls
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext ([Char]
    x, Dom Type
    a) (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
    $ Type -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Type
    b

          -- Non-dependent function space. Destroys guardedness.
          Pi Dom Type
    a (NoAbs [Char]
    _ Type
    b) ->
            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
    $ 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 Type -> TerM Calls
    forall a. ExtractCalls a => a -> TerM Calls
    extract Dom Type
    a TerM (Calls -> Calls) -> TerM Calls -> TerM Calls
    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 (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 (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 (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 Type -> tcm (Dom Type)
    maskSizeLt !Dom Type
    dom = TCM (Dom Type) -> tcm (Dom Type)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Dom Type) -> tcm (Dom Type))
    -> TCM (Dom Type) -> tcm (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ do
      let a :: Type
    a = Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    dom
      (Maybe QName
    msize, Maybe QName
    msizelt) <- TCMT IO (Maybe QName, Maybe QName)
    forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize
      case (Maybe QName
    msize, Maybe QName
    msizelt) of
        (Maybe QName
    _ , Maybe QName
    Nothing) -> Dom Type -> TCM (Dom Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Dom Type
    dom
        (Maybe QName
    Nothing, Maybe QName
    _)  -> TCM (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Just QName
    size, Just QName
    sizelt) -> do
          TelV Telescope
    tel Type
    c <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    a
          case Type
    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 Type -> TCM (Dom Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom Type -> TCM (Dom Type)) -> Dom Type -> TCM (Dom 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 Type -> Dom Type
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom Type
    dom
            Type
    _ -> Dom Type -> TCM (Dom Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Dom 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 (Nat, Nat, [[Order]])
    compareArgs Elims
    es = do
      MaskedDeBruijnPatterns
    pats <- TerM MaskedDeBruijnPatterns
    terGetPatterns
      TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.compareArgs" Nat
    90 (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
    vcat
        [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "comparing " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [Char]
    forall a. Show a => a -> [Char]
    show (Elims -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    es) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " args to " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [Char]
    forall a. Show a => a -> [Char]
    show (MaskedDeBruijnPatterns -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length MaskedDeBruijnPatterns
    pats) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " 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
      [[Order]]
    matrix <- MaskedDeBruijnPatterns -> TerM [[Order]] -> TerM [[Order]]
    forall a b. UsableSizeVars a => a -> TerM b -> TerM b
    withUsableVars MaskedDeBruijnPatterns
    pats (TerM [[Order]] -> TerM [[Order]])
    -> TerM [[Order]] -> TerM [[Order]]
    forall a b. (a -> b) -> a -> b
    $ Elims -> (Elim -> TerM [Order]) -> TerM [[Order]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM Elims
    es ((Elim -> TerM [Order]) -> TerM [[Order]])
    -> (Elim -> TerM [Order]) -> TerM [[Order]]
    forall a b. (a -> b) -> a -> b
    $ \ 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).
      Nat
    projsCaller <- [QName] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length ([QName] -> Nat) -> TerM [QName] -> TerM Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        (QName -> TerM Bool) -> [QName] -> TerM [QName]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (Bool -> QName -> TerM Bool
    forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
    isCoinductiveProjection Bool
    True) ([QName] -> TerM [QName]) -> [QName] -> TerM [QName]
    forall a b. (a -> b) -> a -> b
    $ (Masked DeBruijnPattern -> Maybe QName)
    -> MaskedDeBruijnPatterns -> [QName]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (((ProjOrigin, AmbiguousQName) -> QName)
    -> Maybe (ProjOrigin, AmbiguousQName) -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (AmbiguousQName -> QName
    headAmbQ (AmbiguousQName -> QName)
    -> ((ProjOrigin, AmbiguousQName) -> AmbiguousQName)
    -> (ProjOrigin, AmbiguousQName)
    -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProjOrigin, AmbiguousQName) -> AmbiguousQName
    forall a b. (a, b) -> b
    snd) (Maybe (ProjOrigin, AmbiguousQName) -> Maybe QName)
    -> (Masked DeBruijnPattern -> Maybe (ProjOrigin, AmbiguousQName))
    -> Masked DeBruijnPattern
    -> Maybe QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DeBruijnPattern -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    isProjP (DeBruijnPattern -> Maybe (ProjOrigin, AmbiguousQName))
    -> (Masked DeBruijnPattern -> DeBruijnPattern)
    -> Masked DeBruijnPattern
    -> Maybe (ProjOrigin, AmbiguousQName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Masked DeBruijnPattern -> DeBruijnPattern
    forall a. Masked a -> a
    getMasked) MaskedDeBruijnPatterns
    pats
      Nat
    projsCallee <- [QName] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length ([QName] -> Nat) -> TerM [QName] -> TerM Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        (QName -> TerM Bool) -> [QName] -> TerM [QName]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (Bool -> QName -> TerM Bool
    forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
    isCoinductiveProjection Bool
    True) ([QName] -> TerM [QName]) -> [QName] -> TerM [QName]
    forall a b. (a -> b) -> a -> b
    $ (Elim -> Maybe QName) -> Elims -> [QName]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (((ProjOrigin, QName) -> QName)
    -> Maybe (ProjOrigin, QName) -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ProjOrigin, QName) -> QName
    forall a b. (a, b) -> b
    snd (Maybe (ProjOrigin, QName) -> Maybe QName)
    -> (Elim -> Maybe (ProjOrigin, QName)) -> Elim -> Maybe QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim) Elims
    es
      CutOff
    cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = ?cutoff::CutOff
    CutOff
    cutoff
      Bool
    useGuardedness <- TCMT IO Bool -> TerM Bool
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    guardednessOption
      let guardedness :: Order
    guardedness =
            if Bool
    useGuardedness
            then (?cutoff::CutOff) => Bool -> Nat -> Order
    Bool -> Nat -> Order
    decr Bool
    True (Nat -> Order) -> Nat -> Order
    forall a b. (a -> b) -> a -> b
    $ Nat
    projsCaller Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    projsCallee
            else Order
    Order.Unknown
      TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.guardedness" Nat
    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
    "compareArgs:"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "projsCaller = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Nat
    projsCaller
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "projsCallee = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Nat
    projsCallee
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "guardedness of call: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Order -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Order
    guardedness
        ]
      (Nat, Nat, [[Order]]) -> TerM (Nat, Nat, [[Order]])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Nat, Nat, [[Order]]) -> TerM (Nat, Nat, [[Order]]))
    -> (Nat, Nat, [[Order]]) -> TerM (Nat, Nat, [[Order]])
    forall a b. (a -> b) -> a -> b
    $ Order -> (Nat, Nat, [[Order]]) -> (Nat, Nat, [[Order]])
    addGuardedness Order
    guardedness (Elims -> Nat
    forall a. Sized a => a -> Nat
    size Elims
    es, MaskedDeBruijnPatterns -> Nat
    forall a. Sized a => a -> Nat
    size MaskedDeBruijnPatterns
    pats, [[Order]]
    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 (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.compare" Nat
    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"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    prettyTCM Elim
    e
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    prettyTCM Masked DeBruijnPattern
    p
          ]
        [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.compare" Nat
    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
          [ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "e = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Elim -> [Char]
    forall a. Show a => a -> [Char]
    show Elim
    e
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "p = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Masked DeBruijnPattern -> [Char]
    forall a. Show a => a -> [Char]
    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
          QName
    d  <- QName -> TerM QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getOriginalProjection QName
    d
          QName
    d' <- QName -> TerM QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getOriginalProjection QName
    d'
          Order
    o  <- QName -> QName -> TerM Order
    forall (tcm :: * -> *). MonadTCM tcm => QName -> QName -> tcm Order
    compareProj QName
    d QName
    d'
          [Char] -> Nat -> TCMT IO Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.compare" Nat
    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
    sep
            [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "comparing callee projection " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    d
            , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "against caller projection " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    d'
            , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "yields order " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Order -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Order
    o
            ]
          Order -> TerM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    o
        (Proj{}, DeBruijnPattern
    _)            -> Order -> TerM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown
        (Apply{}, ProjP{})     -> Order -> TerM Order
    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 (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 (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le
      | Bool
    otherwise = TCM Order -> tcm Order
    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
          Maybe QName
    mr  <- QName -> TCM (Maybe QName)
    getRecordOfField QName
    d
          Maybe QName
    mr' <- QName -> TCM (Maybe QName)
    getRecordOfField QName
    d'
          case (Maybe QName
    mr, Maybe QName
    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
              Defn
    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 Defn
    def of
                Record{ recFields :: Defn -> [Dom QName]
    recFields = [Dom QName]
    fs } -> do
                  [QName]
    fs <- [QName] -> TCMT IO [QName]
    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 ((QName -> Bool) -> [QName] -> Maybe QName
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find (QName
    dQName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) [QName]
    fs, (QName -> Bool) -> [QName] -> Maybe QName
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find (QName
    d'QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) [QName]
    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 (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
                         TCM Order
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                      | Bool
    otherwise -> Order -> TCM Order
    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 (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 :: Nat -> Nat -> [[Order]] -> CallMatrix
    makeCM Nat
    ncols Nat
    nrows [[Order]]
    matrix = Matrix Nat Order -> CallMatrix
    forall a. Matrix Nat a -> CallMatrix' a
    CallMatrix (Matrix Nat Order -> CallMatrix) -> Matrix Nat Order -> CallMatrix
    forall a b. (a -> b) -> a -> b
    $
      Size Nat -> [[Order]] -> Matrix Nat Order
    forall i b.
    (Ord i, Num i, Enum i, HasZero b) =>
    Size i -> [[b]] -> Matrix i b
    Matrix.fromLists (Nat -> Nat -> Size Nat
    forall i. i -> i -> Size i
    Matrix.Size Nat
    nrows Nat
    ncols) [[Order]]
    matrix

    -- | 'addGuardedness' adds guardedness flag in the upper left corner
    -- (0,0).
    addGuardedness :: Order -> (Int, Int, [[Order]]) -> (Int, Int, [[Order]])
    addGuardedness :: Order -> (Nat, Nat, [[Order]]) -> (Nat, Nat, [[Order]])
    addGuardedness Order
    o (Nat
    nrows, Nat
    ncols, [[Order]]
    m) =
      (Nat
    nrows Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1, Nat
    ncols Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1,
       (Order
    o Order -> [Order] -> [Order]
    forall a. a -> [a] -> [a]
    : Nat -> Order -> [Order]
    forall a. Nat -> a -> [a]
    replicate Nat
    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 Nat
    offsetFromConstructor QName
    c =
      tcm Bool -> tcm Nat -> tcm Nat -> tcm Nat
    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) (Nat -> tcm Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    0) (Nat -> tcm Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    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
      Term
    t <- TCM Term -> TerM Term
    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
      Order
    o <- Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' Term
    t Masked DeBruijnPattern
    p
      TCMT IO () -> TerM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> TerM ()) -> TCMT IO () -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "term.compare" Nat
    25 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    " comparing term " 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
    prettyTCM Term
    t TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
        TCMT IO Doc
    " to pattern " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Masked DeBruijnPattern -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Masked DeBruijnPattern
    p TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
        [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    " results in " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Order -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Order
    o)
      Order -> TerM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    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)
    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 (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 (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 (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 (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 (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
            Bool
    isP <- QName -> TCMT IO Bool
    forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Bool
    isProjectionButNotCoinductive QName
    p
            Bool -> (Elims -> Elims) -> Elims -> Elims
    forall a. Bool -> (a -> a) -> a -> a
    applyUnless Bool
    isP (ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    p Elim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :) (Elims -> Elims) -> TCM Elims -> TCM Elims
    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

    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)
    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 Nat
    i Elims
    es   -> Nat -> Elims -> Term
    Var Nat
    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 (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 (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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (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
      Maybe QName
    suc  <- TerM (Maybe QName)
    terGetSizeSuc
      CutOff
    cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = ?cutoff::CutOff
    CutOff
    cutoff
      Term
    v <- TCM Term -> TerM Term
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (Term -> TCM Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    v)
      DeBruijnPattern
    p <- TCM DeBruijnPattern -> TerM DeBruijnPattern
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM DeBruijnPattern -> TerM DeBruijnPattern)
    -> TCM DeBruijnPattern -> TerM DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ DeBruijnPattern -> TCM DeBruijnPattern
    reduceConPattern DeBruijnPattern
    p
      case (Term
    v, DeBruijnPattern
    p) of

        -- Andreas, 2013-11-20 do not drop projections,
        -- in any case not coinductive ones!:
        (Var Nat
    i Elims
    es, DeBruijnPattern
    _) | Just{} <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
          Nat -> Masked DeBruijnPattern -> TerM Order
    compareVar Nat
    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 -> Nat -> Order
    Bool -> Nat -> Order
    Order.decr Bool
    True (Nat -> Order) -> (Nat -> Nat) -> Nat -> Order
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    max (if Bool
    m then Nat
    0 else DeBruijnPattern -> Nat
    forall a. Pattern' a -> Nat
    patternDepth DeBruijnPattern
    p) (Nat -> Nat) -> (Nat -> Nat) -> Nat -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Nat
    forall a. Enum a => a -> a
    pred (Nat -> Order) -> TerM Nat -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
           (TerEnv -> Nat) -> TerM Nat
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Nat
    _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
          Nat -> Order -> Order
    increase Nat
    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 (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 (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le
          | Bool
    otherwise   -> Order -> TerM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown

        (Lit Literal
    l, DeBruijnPattern
    _) -> do
          Term
    v <- TCM Term -> TerM Term
    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 Term
    v of
            Lit{}       -> Order -> TerM Order
    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 -> Nat -> Order
    Bool -> Nat -> Order
    decr Bool
    True (Nat -> Order) -> TerM Nat -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TerM Nat
    forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
    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 (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
          Nat -> Order -> Order
    increase (Nat -> Order -> Order) -> TerM Nat -> TerM (Order -> Order)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TerM Nat
    forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
    offsetFromConstructor (ConHead -> QName
    conName ConHead
    c)
                   TerM (Order -> Order) -> TerM Order -> TerM Order
    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)
    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 (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] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Arg Term]
    ts Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == NAPs -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    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 Nat
    i []) (VarP PatternInfo
    _ DBPatVar
    x) = Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == DBPatVar -> Nat
    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
    $ Nat -> Order -> Order
    decrease Nat
    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
    cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = ?cutoff::CutOff
    CutOff
    cutoff
      -- we may assume |ps| >= |ts|, otherwise c ps would be of functional type
      -- which is impossible
      case ([Arg Term] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Arg Term]
    ts, NAPs -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length NAPs
    ps) of
        (Nat
    0,Nat
    0) -> Order -> TerM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le        -- c <= c
        (Nat
    0,Nat
    1) -> Order -> TerM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown   -- c not<= c x
        (Nat
    1,Nat
    0) -> TerM Order
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Nat
    1,Nat
    1) -> Term -> Masked DeBruijnPattern -> TerM Order
    compareTerm' (Arg Term -> Term
    forall e. Arg e -> e
    unArg ([Arg Term] -> Arg Term
    forall a. [a] -> a
    head [Arg Term]
    ts)) (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) -> DeBruijnPattern)
    -> Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ NAPs -> Arg (Named_ DeBruijnPattern)
    forall a. [a] -> a
    head NAPs
    ps)
        (Nat
    _,Nat
    _) -> (Order -> Order -> Order) -> Order -> [Order] -> Order
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    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 :: Nat -> Masked DeBruijnPattern -> TerM Order
    compareVar Nat
    i (Masked Bool
    m DeBruijnPattern
    p) = do
      Maybe QName
    suc    <- TerM (Maybe QName)
    terGetSizeSuc
      CutOff
    cutoff <- TerM CutOff
    terGetCutOff
      let ?cutoff = ?cutoff::CutOff
    CutOff
    cutoff
      let no :: TerM Order
    no = Order -> TerM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown
      case DeBruijnPattern
    p of
        ProjP{}   -> TerM Order
    no
        IApplyP PatternInfo
    _ Term
    _ Term
    _ DBPatVar
    x  -> Nat -> Masked DBPatVar -> TerM Order
    compareVarVar Nat
    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  -> Nat -> Masked DBPatVar -> TerM Order
    compareVarVar Nat
    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
    . Nat -> Order -> Order
    decrease Nat
    1 (Order -> Order) -> TerM Order -> TerM Order
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat -> Masked DeBruijnPattern -> TerM Order
    compareVar Nat
    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
    _ 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
          Nat -> Order -> Order
    decrease (Nat -> Order -> Order) -> TerM Nat -> TerM (Order -> Order)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TerM Nat
    forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
    offsetFromConstructor (ConHead -> QName
    conName ConHead
    c)
                   TerM (Order -> Order) -> TerM Order -> TerM Order
    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)
    mapM (Nat -> Masked DeBruijnPattern -> TerM Order
    compareVar Nat
    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)
        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
          Nat -> Order -> Order
    decrease (Nat -> Order -> Order) -> TerM Nat -> TerM (Order -> Order)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TerM Nat
    forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm Nat
    offsetFromConstructor QName
    c
                   TerM (Order -> Order) -> TerM Order -> TerM Order
    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)
    mapM (Nat -> Masked DeBruijnPattern -> TerM Order
    compareVar Nat
    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 :: Nat -> Masked DBPatVar -> TerM Order
    compareVarVar Nat
    i (Masked Bool
    m x :: DBPatVar
    x@(DBPatVar [Char]
    _ Nat
    j))
      | Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    j = if Bool -> Bool
    not Bool
    m then Order -> TerM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le else TCM Order -> TerM Order
    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)
    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
    =<< Nat -> TCMT IO Type
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Nat -> m Type
    typeOfBV Nat
    j)
            {- then -} (Order -> TCM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.le)
            {- else -} (Order -> TCM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown)
      | Bool
    otherwise = do
          -- record usability of variable
          Bool
    u <- (Nat
    i Nat -> 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 Bool -> Bool
    not Bool
    u then Order -> TerM Order
    forall (m :: * -> *) a. Monad m => a -> m a
    return Order
    Order.unknown else do
          -- Only if usable:
          BoundedSize
    res <- Nat -> TerM BoundedSize
    forall (m :: * -> *). PureTCM m => Nat -> m BoundedSize
    isBounded Nat
    i
          case BoundedSize
    res of
            BoundedSize
    BoundedNo  -> Order -> TerM Order
    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
    . Nat -> Order -> Order
    decrease Nat
    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)