    -- | The monad for the termination checker.
    --
    --   The termination monad @TerM@ is an extension of
    --   the type checking monad 'TCM' by an environment
    --   with information needed by the termination checker.

    module Agda.Termination.Monad where

    import Prelude hiding (null)

    import Control.Applicative hiding (empty)

    import Control.Monad.IO.Class ( MonadIO(..) )
    import Control.Monad.Except   ( MonadError(..) )
    import Control.Monad.Reader   ( MonadReader(..), ReaderT(..) )

    import Data.DList (DList)
    import qualified Data.DList as DL
    import Data.Semigroup ( Semigroup(..) )
    import Data.Set (Set)
    import qualified Data.Set as Set

    import Agda.Interaction.Options (optTerminationDepth)

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern
    import Agda.Syntax.Literal

    import Agda.Termination.CutOff
    import Agda.Termination.Order (Order,le,unknown)
    import Agda.Termination.RecCheck (MutualNames, anyDefs)

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Monad.Benchmark
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Benchmark as B
    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List   ( hasElem )
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Monoid
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty (Pretty, prettyShow)
    import qualified Agda.Syntax.Common.Pretty as P
    import Agda.Utils.VarSet (VarSet)
    import qualified Agda.Utils.VarSet as VarSet

    import Agda.Utils.Impossible

    -- | The target of the function we are checking.

    data Target
      = TargetDef QName
          -- ^ The target of recursion is a @record@, @data@, or unreducible @Def@.
      | TargetRecord
          -- ^ We are termination-checking a record.
      | TargetOther
          -- ^ None of the above two or unknown.
      deriving (Target -> Target -> Bool
    (Target -> Target -> Bool)
    -> (Target -> Target -> Bool) -> Eq Target
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Target -> Target -> Bool
    == :: Target -> Target -> Bool
    $c/= :: Target -> Target -> Bool
    /= :: Target -> Target -> Bool
    Eq, Int -> Target -> ShowS
    [Target] -> ShowS
    Target -> String
    (Int -> Target -> ShowS)
    -> (Target -> String) -> ([Target] -> ShowS) -> Show Target
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Target -> ShowS
    showsPrec :: Int -> Target -> ShowS
    $cshow :: Target -> String
    show :: Target -> String
    $cshowList :: [Target] -> ShowS
    showList :: [Target] -> ShowS
    Show)

    -- | The current guardedness level.

    type Guarded = Order

    -- | The termination environment.

    data TerEnv = TerEnv

      -- First part: options, configuration.

      { TerEnv -> Bool
    terUseDotPatterns :: Bool
        -- ^ Are we mining dot patterns to find evindence of structal descent?
      , TerEnv -> Maybe QName
    terSizeSuc :: Maybe QName
        -- ^ The name of size successor, if any.
      , TerEnv -> Maybe QName
    terSharp   :: Maybe QName
        -- ^ The name of the delay constructor (sharp), if any.
      , TerEnv -> CutOff
    terCutOff  :: CutOff
        -- ^ Depth at which to cut off the structural order.

      -- Second part: accumulated info during descent into decls./term.

      , TerEnv -> QName
    terCurrent :: QName
        -- ^ The name of the function we are currently checking.
      , TerEnv -> MutualNames
    terMutual  :: MutualNames
        -- ^ The names of the functions in the mutual block we are checking.
        --   This includes the internally generated functions
        --   (with, extendedlambda, coinduction).
      , TerEnv -> MutualNames
    terUserNames :: Set QName
        -- ^ The list of name actually appearing in the file (abstract syntax).
        --   Excludes the internally generated functions.
      , TerEnv -> Bool
    terHaveInlinedWith :: Bool
        -- ^ Does the actual clause result from with-inlining?
        --   (If yes, it may be ill-typed.)
      , TerEnv -> Target
    terTarget  :: Target
        -- ^ Target type of the function we are currently termination checking.
        --   Only the constructors of 'Target' are considered guarding.
      , TerEnv -> [Bool]
    terMaskArgs :: [Bool]
        -- ^ Only consider the 'notMasked' 'False' arguments for establishing termination.
        --   See issue #1023.
      , TerEnv -> Bool
    terMaskResult :: Bool
        -- ^ Only consider guardedness if 'False' (not masked).
      , TerEnv -> Int
    _terSizeDepth :: Int  -- lazy by intention!
        -- ^ How many @SIZELT@ relations do we have in the context
        --   (= clause telescope).  Used to approximate termination
        --   for metas in call args.
      , TerEnv -> MaskedDeBruijnPatterns
    terPatterns :: MaskedDeBruijnPatterns
        -- ^ The patterns of the clause we are checking.
      , TerEnv -> Int
    terPatternsRaise :: !Int
        -- ^ Number of additional binders we have gone under
        --   (and consequently need to raise the patterns to compare to terms).
        --   Updated during call graph extraction, hence strict.
      , TerEnv -> Guarded
    terGuarded :: !Guarded
        -- ^ The current guardedness status.  Changes as we go deeper into the term.
        --   Updated during call graph extraction, hence strict.
      , TerEnv -> Bool
    terUseSizeLt :: Bool
        -- ^ When extracting usable size variables during construction of the call
        --   matrix, can we take the variable for use with SIZELT constraints from the context?
        --   Yes, if we are under an inductive constructor.
        --   No, if we are under a record constructor.
        --   (See issue #1015).
      , TerEnv -> VarSet
    terUsableVars :: VarSet
        -- ^ Pattern variables that can be compared to argument variables using SIZELT.
      }

    -- | An empty termination environment.
    --
    --   Values are set to a safe default meaning that with these
    --   initial values the termination checker will not miss
    --   termination errors it would have seen with better settings
    --   of these values.
    --
    --   Values that do not have a safe default are set to
    --   @__IMPOSSIBLE__@.

    defaultTerEnv :: TerEnv
    defaultTerEnv :: TerEnv
    defaultTerEnv = TerEnv
      { terUseDotPatterns :: Bool
    terUseDotPatterns           = Bool
    False -- must be False initially!
      , terSizeSuc :: Maybe QName
    terSizeSuc                  = Maybe QName
    forall a. Maybe a
    Nothing
      , terSharp :: Maybe QName
    terSharp                    = Maybe QName
    forall a. Maybe a
    Nothing
      , terCutOff :: CutOff
    terCutOff                   = CutOff
    defaultCutOff
      , terUserNames :: MutualNames
    terUserNames                = MutualNames
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- needs to be set!
      , terMutual :: MutualNames
    terMutual                   = MutualNames
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- needs to be set!
      , terCurrent :: QName
    terCurrent                  = QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- needs to be set!
      , terHaveInlinedWith :: Bool
    terHaveInlinedWith          = Bool
    False
      , terTarget :: Target
    terTarget                   = Target
    TargetOther
      , terMaskArgs :: [Bool]
    terMaskArgs                 = Bool -> [Bool]
    forall a. a -> [a]
    repeat Bool
    False   -- use all arguments (mask none)
      , terMaskResult :: Bool
    terMaskResult               = Bool
    False          -- use result (do not mask)
      , _terSizeDepth :: Int
    _terSizeDepth               = Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- needs to be set!
      , terPatterns :: MaskedDeBruijnPatterns
    terPatterns                 = MaskedDeBruijnPatterns
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- needs to be set!
      , terPatternsRaise :: Int
    terPatternsRaise            = Int
    0
      , terGuarded :: Guarded
    terGuarded                  = Guarded
    le -- not initially guarded
      , terUseSizeLt :: Bool
    terUseSizeLt                = Bool
    False -- initially, not under data constructor
      , terUsableVars :: VarSet
    terUsableVars               = VarSet
    VarSet.empty
      }

    -- | Termination monad service class.

    class (Functor m, Monad m) => MonadTer m where
      terAsk   :: m TerEnv
      terLocal :: (TerEnv -> TerEnv) -> m a -> m a

      terAsks :: (TerEnv -> a) -> m a
      terAsks TerEnv -> a
    f = TerEnv -> a
    f (TerEnv -> a) -> m TerEnv -> m a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m TerEnv
    forall (m :: * -> *). MonadTer m => m TerEnv
    terAsk

    -- | Termination monad.

    newtype TerM a = TerM { forall a. TerM a -> ReaderT TerEnv TCM a
    terM :: ReaderT TerEnv TCM a }
      deriving ( (forall a b. (a -> b) -> TerM a -> TerM b)
    -> (forall a b. a -> TerM b -> TerM a) -> Functor TerM
    forall a b. a -> TerM b -> TerM a
    forall a b. (a -> b) -> TerM a -> TerM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> TerM a -> TerM b
    fmap :: forall a b. (a -> b) -> TerM a -> TerM b
    $c<$ :: forall a b. a -> TerM b -> TerM a
    <$ :: forall a b. a -> TerM b -> TerM a
    Functor
               , Functor TerM
    Functor TerM =>
    (forall a. a -> TerM a)
    -> (forall a b. TerM (a -> b) -> TerM a -> TerM b)
    -> (forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c)
    -> (forall a b. TerM a -> TerM b -> TerM b)
    -> (forall a b. TerM a -> TerM b -> TerM a)
    -> Applicative TerM
    forall a. a -> TerM a
    forall a b. TerM a -> TerM b -> TerM a
    forall a b. TerM a -> TerM b -> TerM b
    forall a b. TerM (a -> b) -> TerM a -> TerM b
    forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall a. a -> TerM a
    pure :: forall a. a -> TerM a
    $c<*> :: forall a b. TerM (a -> b) -> TerM a -> TerM b
    <*> :: forall a b. TerM (a -> b) -> TerM a -> TerM b
    $cliftA2 :: forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
    liftA2 :: forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
    $c*> :: forall a b. TerM a -> TerM b -> TerM b
    *> :: forall a b. TerM a -> TerM b -> TerM b
    $c<* :: forall a b. TerM a -> TerM b -> TerM a
    <* :: forall a b. TerM a -> TerM b -> TerM a
    Applicative
               , Applicative TerM
    Applicative TerM =>
    (forall a b. TerM a -> (a -> TerM b) -> TerM b)
    -> (forall a b. TerM a -> TerM b -> TerM b)
    -> (forall a. a -> TerM a)
    -> Monad TerM
    forall a. a -> TerM a
    forall a b. TerM a -> TerM b -> TerM b
    forall a b. TerM a -> (a -> TerM b) -> TerM b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall a b. TerM a -> (a -> TerM b) -> TerM b
    >>= :: forall a b. TerM a -> (a -> TerM b) -> TerM b
    $c>> :: forall a b. TerM a -> TerM b -> TerM b
    >> :: forall a b. TerM a -> TerM b -> TerM b
    $creturn :: forall a. a -> TerM a
    return :: forall a. a -> TerM a
    Monad
               , MonadError TCErr
               , ReadTCState TerM
    String -> (Integer -> Integer) -> TerM ()
    ReadTCState TerM =>
    (String -> (Integer -> Integer) -> TerM ()) -> MonadStatistics TerM
    forall (m :: * -> *).
    ReadTCState m =>
    (String -> (Integer -> Integer) -> m ()) -> MonadStatistics m
    $cmodifyCounter :: String -> (Integer -> Integer) -> TerM ()
    modifyCounter :: String -> (Integer -> Integer) -> TerM ()
    MonadStatistics
               , Monad TerM
    Functor TerM
    Applicative TerM
    TerM PragmaOptions
    TerM CommandLineOptions
    (Functor TerM, Applicative TerM, Monad TerM) =>
    TerM PragmaOptions -> TerM CommandLineOptions -> HasOptions TerM
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    m PragmaOptions -> m CommandLineOptions -> HasOptions m
    $cpragmaOptions :: TerM PragmaOptions
    pragmaOptions :: TerM PragmaOptions
    $ccommandLineOptions :: TerM CommandLineOptions
    commandLineOptions :: TerM CommandLineOptions
    HasOptions
               , Monad TerM
    Functor TerM
    Applicative TerM
    (Functor TerM, Applicative TerM, Monad TerM) =>
    (SomeBuiltin -> TerM (Maybe (Builtin PrimFun))) -> HasBuiltins TerM
    SomeBuiltin -> TerM (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    (SomeBuiltin -> m (Maybe (Builtin PrimFun))) -> HasBuiltins m
    $cgetBuiltinThing :: SomeBuiltin -> TerM (Maybe (Builtin PrimFun))
    getBuiltinThing :: SomeBuiltin -> TerM (Maybe (Builtin PrimFun))
    HasBuiltins
               , Monad TerM
    Functor TerM
    Applicative TerM
    TerM Bool
    TerM Verbosity
    TerM ProfileOptions
    (Functor TerM, Applicative TerM, Monad TerM) =>
    (String -> Int -> TCM Doc -> TerM String)
    -> (forall a. String -> Int -> String -> TerM a -> TerM a)
    -> (forall a. String -> Int -> String -> TerM a -> TerM a)
    -> TerM Verbosity
    -> TerM ProfileOptions
    -> TerM Bool
    -> (forall a. TerM a -> TerM a)
    -> MonadDebug TerM
    String -> Int -> TCM Doc -> TerM String
    forall a. String -> Int -> String -> TerM a -> TerM a
    forall a. TerM a -> TerM a
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    (String -> Int -> TCM Doc -> m String)
    -> (forall a. String -> Int -> String -> m a -> m a)
    -> (forall a. String -> Int -> String -> m a -> m a)
    -> m Verbosity
    -> m ProfileOptions
    -> m Bool
    -> (forall a. m a -> m a)
    -> MonadDebug m
    $cformatDebugMessage :: String -> Int -> TCM Doc -> TerM String
    formatDebugMessage :: String -> Int -> TCM Doc -> TerM String
    $ctraceDebugMessage :: forall a. String -> Int -> String -> TerM a -> TerM a
    traceDebugMessage :: forall a. String -> Int -> String -> TerM a -> TerM a
    $cverboseBracket :: forall a. String -> Int -> String -> TerM a -> TerM a
    verboseBracket :: forall a. String -> Int -> String -> TerM a -> TerM a
    $cgetVerbosity :: TerM Verbosity
    getVerbosity :: TerM Verbosity
    $cgetProfileOptions :: TerM ProfileOptions
    getProfileOptions :: TerM ProfileOptions
    $cisDebugPrinting :: TerM Bool
    isDebugPrinting :: TerM Bool
    $cnowDebugPrinting :: forall a. TerM a -> TerM a
    nowDebugPrinting :: forall a. TerM a -> TerM a
    MonadDebug
               , Functor TerM
    Applicative TerM
    HasOptions TerM
    MonadTCEnv TerM
    MonadDebug TerM
    (Functor TerM, Applicative TerM, HasOptions TerM, MonadDebug TerM,
     MonadTCEnv TerM) =>
    (QName -> TerM Definition)
    -> (QName -> TerM (Either SigError Definition))
    -> (QName -> TerM RewriteRules)
    -> HasConstInfo TerM
    QName -> TerM RewriteRules
    QName -> TerM (Either SigError Definition)
    QName -> TerM Definition
    forall (m :: * -> *).
    (Functor m, Applicative m, HasOptions m, MonadDebug m,
     MonadTCEnv m) =>
    (QName -> m Definition)
    -> (QName -> m (Either SigError Definition))
    -> (QName -> m RewriteRules)
    -> HasConstInfo m
    $cgetConstInfo :: QName -> TerM Definition
    getConstInfo :: QName -> TerM Definition
    $cgetConstInfo' :: QName -> TerM (Either SigError Definition)
    getConstInfo' :: QName -> TerM (Either SigError Definition)
    $cgetRewriteRulesFor :: QName -> TerM RewriteRules
    getRewriteRulesFor :: QName -> TerM RewriteRules
    HasConstInfo
               , Monad TerM
    Monad TerM => (forall a. IO a -> TerM a) -> MonadIO TerM
    forall a. IO a -> TerM a
    forall (m :: * -> *).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    $cliftIO :: forall a. IO a -> TerM a
    liftIO :: forall a. IO a -> TerM a
    MonadIO
               , Monad TerM
    TerM TCEnv
    Monad TerM =>
    TerM TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a)
    -> MonadTCEnv TerM
    forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
    forall (m :: * -> *).
    Monad m =>
    m TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
    $caskTC :: TerM TCEnv
    askTC :: TerM TCEnv
    $clocalTC :: forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
    localTC :: forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
    MonadTCEnv
               , Monad TerM
    TerM TCState
    Monad TerM =>
    TerM TCState
    -> (TCState -> TerM ())
    -> ((TCState -> TCState) -> TerM ())
    -> MonadTCState TerM
    TCState -> TerM ()
    (TCState -> TCState) -> TerM ()
    forall (m :: * -> *).
    Monad m =>
    m TCState
    -> (TCState -> m ())
    -> ((TCState -> TCState) -> m ())
    -> MonadTCState m
    $cgetTC :: TerM TCState
    getTC :: TerM TCState
    $cputTC :: TCState -> TerM ()
    putTC :: TCState -> TerM ()
    $cmodifyTC :: (TCState -> TCState) -> TerM ()
    modifyTC :: (TCState -> TCState) -> TerM ()
    MonadTCState
               , Applicative TerM
    MonadIO TerM
    HasOptions TerM
    MonadTCState TerM
    MonadTCEnv TerM
    (Applicative TerM, MonadIO TerM, MonadTCEnv TerM,
     MonadTCState TerM, HasOptions TerM) =>
    (forall a. TCM a -> TerM a) -> MonadTCM TerM
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *).
    (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm,
     HasOptions tcm) =>
    (forall a. TCM a -> tcm a) -> MonadTCM tcm
    $cliftTCM :: forall a. TCM a -> TerM a
    liftTCM :: forall a. TCM a -> TerM a
    MonadTCM
               , Monad TerM
    TerM TCState
    Monad TerM =>
    TerM TCState
    -> (forall a b. Lens' TCState a -> (a -> a) -> TerM b -> TerM b)
    -> (forall a. (TCState -> TCState) -> TerM a -> TerM a)
    -> ReadTCState TerM
    forall a. (TCState -> TCState) -> TerM a -> TerM a
    forall a b. Lens' TCState a -> (a -> a) -> TerM b -> TerM b
    forall (m :: * -> *).
    Monad m =>
    m TCState
    -> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
    -> (forall a. (TCState -> TCState) -> m a -> m a)
    -> ReadTCState m
    $cgetTCState :: TerM TCState
    getTCState :: TerM TCState
    $clocallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> TerM b -> TerM b
    locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> TerM b -> TerM b
    $cwithTCState :: forall a. (TCState -> TCState) -> TerM a -> TerM a
    withTCState :: forall a. (TCState -> TCState) -> TerM a -> TerM a
    ReadTCState
               , Applicative TerM
    HasOptions TerM
    MonadTCEnv TerM
    ReadTCState TerM
    (Applicative TerM, MonadTCEnv TerM, ReadTCState TerM,
     HasOptions TerM) =>
    (forall a. ReduceM a -> TerM a) -> MonadReduce TerM
    forall a. ReduceM a -> TerM a
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) =>
    (forall a. ReduceM a -> m a) -> MonadReduce m
    $cliftReduce :: forall a. ReduceM a -> TerM a
    liftReduce :: forall a. ReduceM a -> TerM a
    MonadReduce
               , MonadTCEnv TerM
    MonadTCEnv TerM =>
    (forall a. Name -> Dom Type -> TerM a -> TerM a)
    -> (forall a.
        Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a)
    -> (forall a.
        Substitution -> (Context -> Context) -> TerM a -> TerM a)
    -> (forall a. Range -> String -> (Name -> TerM a) -> TerM a)
    -> MonadAddContext TerM
    forall a. Range -> String -> (Name -> TerM a) -> TerM a
    forall a. Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a
    forall a. Name -> Dom Type -> TerM a -> TerM a
    forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
    forall (m :: * -> *).
    MonadTCEnv m =>
    (forall a. Name -> Dom Type -> m a -> m a)
    -> (forall a. Origin -> Name -> Term -> Dom Type -> m a -> m a)
    -> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
    -> (forall a. Range -> String -> (Name -> m a) -> m a)
    -> MonadAddContext m
    $caddCtx :: forall a. Name -> Dom Type -> TerM a -> TerM a
    addCtx :: forall a. Name -> Dom Type -> TerM a -> TerM a
    $caddLetBinding' :: forall a. Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a
    addLetBinding' :: forall a. Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a
    $cupdateContext :: forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
    updateContext :: forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
    $cwithFreshName :: forall a. Range -> String -> (Name -> TerM a) -> TerM a
    withFreshName :: forall a. Range -> String -> (Name -> TerM a) -> TerM a
    MonadAddContext
               , MonadTCEnv TerM
    MonadReduce TerM
    ReadTCState TerM
    HasBuiltins TerM
    MonadAddContext TerM
    MonadDebug TerM
    HasConstInfo TerM
    (HasBuiltins TerM, HasConstInfo TerM, MonadAddContext TerM,
     MonadDebug TerM, MonadReduce TerM, MonadTCEnv TerM,
     ReadTCState TerM) =>
    PureTCM TerM
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m,
     MonadReduce m, MonadTCEnv m, ReadTCState m) =>
    PureTCM m
    PureTCM
               )

    -- This could be derived automatically, but the derived type family becomes `BenchPhase (ReaderT TerEnv TCM)` which
    -- is *fine* but triggers complaints that the "type family application is no smaller than the instance head, why not
    -- nuke everything with UndecidableInstances".
    instance MonadBench TerM where
      type BenchPhase TerM = Phase
      getBenchmark :: TerM (Benchmark (BenchPhase TerM))
    getBenchmark              = ReaderT TerEnv TCM (Benchmark (BenchPhase TerM))
    -> TerM (Benchmark (BenchPhase TerM))
    forall a. ReaderT TerEnv TCM a -> TerM a
    TerM (ReaderT TerEnv TCM (Benchmark (BenchPhase TerM))
     -> TerM (Benchmark (BenchPhase TerM)))
    -> ReaderT TerEnv TCM (Benchmark (BenchPhase TerM))
    -> TerM (Benchmark (BenchPhase TerM))
    forall a b. (a -> b) -> a -> b
    $ ReaderT TerEnv TCM (Benchmark (BenchPhase (ReaderT TerEnv TCM)))
    ReaderT TerEnv TCM (Benchmark (BenchPhase TerM))
    forall (m :: * -> *). MonadBench m => m (Benchmark (BenchPhase m))
    B.getBenchmark
      putBenchmark :: Benchmark (BenchPhase TerM) -> TerM ()
    putBenchmark              = ReaderT TerEnv TCM () -> TerM ()
    forall a. ReaderT TerEnv TCM a -> TerM a
    TerM (ReaderT TerEnv TCM () -> TerM ())
    -> (Benchmark Phase -> ReaderT TerEnv TCM ())
    -> Benchmark Phase
    -> TerM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Benchmark (BenchPhase (ReaderT TerEnv TCM))
    -> ReaderT TerEnv TCM ()
    Benchmark Phase -> ReaderT TerEnv TCM ()
    forall (m :: * -> *).
    MonadBench m =>
    Benchmark (BenchPhase m) -> m ()
    B.putBenchmark
      modifyBenchmark :: (Benchmark (BenchPhase TerM) -> Benchmark (BenchPhase TerM))
    -> TerM ()
    modifyBenchmark           = ReaderT TerEnv TCM () -> TerM ()
    forall a. ReaderT TerEnv TCM a -> TerM a
    TerM (ReaderT TerEnv TCM () -> TerM ())
    -> ((Benchmark Phase -> Benchmark Phase) -> ReaderT TerEnv TCM ())
    -> (Benchmark Phase -> Benchmark Phase)
    -> TerM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Benchmark (BenchPhase (ReaderT TerEnv TCM))
     -> Benchmark (BenchPhase (ReaderT TerEnv TCM)))
    -> ReaderT TerEnv TCM ()
    (Benchmark Phase -> Benchmark Phase) -> ReaderT TerEnv TCM ()
    forall (m :: * -> *).
    MonadBench m =>
    (Benchmark (BenchPhase m) -> Benchmark (BenchPhase m)) -> m ()
    B.modifyBenchmark
      finally :: forall a b. TerM a -> TerM b -> TerM a
    finally (TerM ReaderT TerEnv TCM b
    m) (TerM ReaderT TerEnv TCM c
    f) = ReaderT TerEnv TCM b -> TerM b
    forall a. ReaderT TerEnv TCM a -> TerM a
    TerM (ReaderT TerEnv TCM b -> TerM b) -> ReaderT TerEnv TCM b -> TerM b
    forall a b. (a -> b) -> a -> b
    $ (ReaderT TerEnv TCM b
    -> ReaderT TerEnv TCM c -> ReaderT TerEnv TCM b
    forall b c.
    ReaderT TerEnv TCM b
    -> ReaderT TerEnv TCM c -> ReaderT TerEnv TCM b
    forall (m :: * -> *) b c. MonadBench m => m b -> m c -> m b
    B.finally ReaderT TerEnv TCM b
    m ReaderT TerEnv TCM c
    f)

    instance MonadTer TerM where
      terAsk :: TerM TerEnv
    terAsk     = ReaderT TerEnv TCM TerEnv -> TerM TerEnv
    forall a. ReaderT TerEnv TCM a -> TerM a
    TerM (ReaderT TerEnv TCM TerEnv -> TerM TerEnv)
    -> ReaderT TerEnv TCM TerEnv -> TerM TerEnv
    forall a b. (a -> b) -> a -> b
    $ ReaderT TerEnv TCM TerEnv
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      terLocal :: forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    terLocal TerEnv -> TerEnv
    f = ReaderT TerEnv TCM a -> TerM a
    forall a. ReaderT TerEnv TCM a -> TerM a
    TerM (ReaderT TerEnv TCM a -> TerM a)
    -> (TerM a -> ReaderT TerEnv TCM a) -> TerM a -> TerM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TerEnv -> TerEnv) -> ReaderT TerEnv TCM a -> ReaderT TerEnv TCM a
    forall a.
    (TerEnv -> TerEnv) -> ReaderT TerEnv TCM a -> ReaderT TerEnv TCM a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local TerEnv -> TerEnv
    f (ReaderT TerEnv TCM a -> ReaderT TerEnv TCM a)
    -> (TerM a -> ReaderT TerEnv TCM a)
    -> TerM a
    -> ReaderT TerEnv TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TerM a -> ReaderT TerEnv TCM a
    forall a. TerM a -> ReaderT TerEnv TCM a
    terM

    -- | Generic run method for termination monad.
    runTer :: TerEnv -> TerM a -> TCM a
    runTer :: forall a. TerEnv -> TerM a -> TCM a
    runTer TerEnv
    tenv (TerM ReaderT TerEnv TCM a
    m) = ReaderT TerEnv TCM a -> TerEnv -> TCMT IO a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT TerEnv TCM a
    m TerEnv
    tenv

    -- | Run TerM computation in default environment (created from options).

    runTerDefault :: TerM a -> TCM a
    runTerDefault :: forall a. TerM a -> TCM a
    runTerDefault TerM a
    cont = do

      -- Assemble then initial configuration of the termination environment.

      cutoff <- PragmaOptions -> CutOff
    optTerminationDepth (PragmaOptions -> CutOff)
    -> TCMT IO PragmaOptions -> TCMT IO CutOff
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions

      -- Get the name of size suc (if sized types are enabled)
      suc <- sizeSucName

      -- The name of sharp (if available).
      sharp <- fmap nameOfSharp <$> coinductionKit

      let tenv = TerEnv
    defaultTerEnv
            { terSizeSuc                  = suc
            , terSharp                    = sharp
            , terCutOff                   = cutoff
            }

      runTer tenv cont

    -- -- * Termination monad is a 'MonadTCM'.

    -- instance MonadError TCErr TerM where
    --   throwError = liftTCM . throwError
    --   catchError m handler = TerM $ ReaderT $ \ tenv -> do
    --     runTer tenv m `catchError` (\ err -> runTer tenv $ handler err)

    instance Semigroup m => Semigroup (TerM m) where
      <> :: TerM m -> TerM m -> TerM m
    (<>) = (m -> m -> m) -> TerM m -> TerM m -> TerM m
    forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 m -> m -> m
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance (Semigroup m, Monoid m) => Monoid (TerM m) where
      mempty :: TerM m
    mempty  = m -> TerM m
    forall a. a -> TerM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure m
    forall a. Monoid a => a
    mempty
      mappend :: TerM m -> TerM m -> TerM m
    mappend = TerM m -> TerM m -> TerM m
    forall a. Semigroup a => a -> a -> a
    (<>)
      mconcat :: [TerM m] -> TerM m
    mconcat = [m] -> m
    forall a. Monoid a => [a] -> a
    mconcat ([m] -> m) -> ([TerM m] -> TerM [m]) -> [TerM m] -> TerM m
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> [TerM m] -> TerM [m]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence

    -- * Modifiers and accessors for the termination environment in the monad.

    terGetUseDotPatterns :: TerM Bool
    terGetUseDotPatterns :: TerM Bool
    terGetUseDotPatterns = (TerEnv -> Bool) -> TerM Bool
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Bool
    terUseDotPatterns

    terSetUseDotPatterns :: Bool -> TerM a -> TerM a
    terSetUseDotPatterns :: forall a. Bool -> TerM a -> TerM a
    terSetUseDotPatterns Bool
    b = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terUseDotPatterns = b }

    terGetSizeSuc :: TerM (Maybe QName)
    terGetSizeSuc :: TerM (Maybe QName)
    terGetSizeSuc = (TerEnv -> Maybe QName) -> TerM (Maybe QName)
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Maybe QName
    terSizeSuc

    terGetCurrent :: TerM QName
    terGetCurrent :: TerM QName
    terGetCurrent = (TerEnv -> QName) -> TerM QName
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> QName
    terCurrent

    terSetCurrent :: QName -> TerM a -> TerM a
    terSetCurrent :: forall a. QName -> TerM a -> TerM a
    terSetCurrent QName
    q = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terCurrent = q }

    terGetSharp :: TerM (Maybe QName)
    terGetSharp :: TerM (Maybe QName)
    terGetSharp = (TerEnv -> Maybe QName) -> TerM (Maybe QName)
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Maybe QName
    terSharp

    terGetCutOff :: TerM CutOff
    terGetCutOff :: TerM CutOff
    terGetCutOff = (TerEnv -> CutOff) -> TerM CutOff
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> CutOff
    terCutOff

    terGetMutual :: TerM MutualNames
    terGetMutual :: TerM MutualNames
    terGetMutual = (TerEnv -> MutualNames) -> TerM MutualNames
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> MutualNames
    terMutual

    terGetUserNames :: TerM (Set QName)
    terGetUserNames :: TerM MutualNames
    terGetUserNames = (TerEnv -> MutualNames) -> TerM MutualNames
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> MutualNames
    terUserNames

    terGetTarget :: TerM Target
    terGetTarget :: TerM Target
    terGetTarget = (TerEnv -> Target) -> TerM Target
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Target
    terTarget

    terSetTarget :: Target -> TerM a -> TerM a
    terSetTarget :: forall a. Target -> TerM a -> TerM a
    terSetTarget Target
    t = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terTarget = t }

    terGetHaveInlinedWith :: TerM Bool
    terGetHaveInlinedWith :: TerM Bool
    terGetHaveInlinedWith = (TerEnv -> Bool) -> TerM Bool
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Bool
    terHaveInlinedWith

    terSetHaveInlinedWith :: TerM a -> TerM a
    terSetHaveInlinedWith :: forall a. TerM a -> TerM a
    terSetHaveInlinedWith = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terHaveInlinedWith = True }

    terGetMaskArgs :: TerM [Bool]
    terGetMaskArgs :: TerM [Bool]
    terGetMaskArgs = (TerEnv -> [Bool]) -> TerM [Bool]
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> [Bool]
    terMaskArgs

    terSetMaskArgs :: [Bool] -> TerM a -> TerM a
    terSetMaskArgs :: forall a. [Bool] -> TerM a -> TerM a
    terSetMaskArgs [Bool]
    b = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terMaskArgs = b }

    terGetMaskResult :: TerM Bool
    terGetMaskResult :: TerM Bool
    terGetMaskResult = (TerEnv -> Bool) -> TerM Bool
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Bool
    terMaskResult

    terSetMaskResult :: Bool -> TerM a -> TerM a
    terSetMaskResult :: forall a. Bool -> TerM a -> TerM a
    terSetMaskResult Bool
    b = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terMaskResult = b }

    terGetPatterns :: TerM (MaskedDeBruijnPatterns)
    terGetPatterns :: TerM MaskedDeBruijnPatterns
    terGetPatterns = do
      n   <- (TerEnv -> Int) -> TerM Int
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Int
    terPatternsRaise
      mps <- terAsks terPatterns
      return $ if n == 0 then mps else map (fmap (raise n)) mps

    terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a
    terSetPatterns :: forall a. MaskedDeBruijnPatterns -> TerM a -> TerM a
    terSetPatterns MaskedDeBruijnPatterns
    ps = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terPatterns = ps }

    terRaise :: TerM a -> TerM a
    terRaise :: forall a. TerM a -> TerM a
    terRaise = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terPatternsRaise = terPatternsRaise e + 1 }

    terGetGuarded :: TerM Guarded
    terGetGuarded :: TerM Guarded
    terGetGuarded = (TerEnv -> Guarded) -> TerM Guarded
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Guarded
    terGuarded

    terModifyGuarded :: (Order -> Order) -> TerM a -> TerM a
    terModifyGuarded :: forall a. (Guarded -> Guarded) -> TerM a -> TerM a
    terModifyGuarded Guarded -> Guarded
    f = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terGuarded = f $ terGuarded e }

    terSetGuarded :: Order -> TerM a -> TerM a
    terSetGuarded :: forall a. Guarded -> TerM a -> TerM a
    terSetGuarded = (Guarded -> Guarded) -> TerM a -> TerM a
    forall a. (Guarded -> Guarded) -> TerM a -> TerM a
    terModifyGuarded ((Guarded -> Guarded) -> TerM a -> TerM a)
    -> (Guarded -> Guarded -> Guarded) -> Guarded -> TerM a -> TerM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Guarded -> Guarded -> Guarded
    forall a b. a -> b -> a
    const

    terUnguarded :: TerM a -> TerM a
    terUnguarded :: forall a. TerM a -> TerM a
    terUnguarded = Guarded -> TerM a -> TerM a
    forall a. Guarded -> TerM a -> TerM a
    terSetGuarded Guarded
    unknown

    -- | Lens for '_terSizeDepth'.

    terSizeDepth :: Lens' TerEnv Int
    terSizeDepth :: Lens' TerEnv Int
    terSizeDepth Int -> f Int
    f TerEnv
    e = Int -> f Int
    f (TerEnv -> Int
    _terSizeDepth TerEnv
    e) f Int -> (Int -> TerEnv) -> f TerEnv
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Int
    i -> TerEnv
    e { _terSizeDepth = i }

    -- | Lens for 'terUsableVars'.

    terGetUsableVars :: TerM VarSet
    terGetUsableVars :: TerM VarSet
    terGetUsableVars = (TerEnv -> VarSet) -> TerM VarSet
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> VarSet
    terUsableVars

    terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a
    terModifyUsableVars :: forall a. (VarSet -> VarSet) -> TerM a -> TerM a
    terModifyUsableVars VarSet -> VarSet
    f = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terUsableVars = f $ terUsableVars e }

    terSetUsableVars :: VarSet -> TerM a -> TerM a
    terSetUsableVars :: forall a. VarSet -> TerM a -> TerM a
    terSetUsableVars = (VarSet -> VarSet) -> TerM a -> TerM a
    forall a. (VarSet -> VarSet) -> TerM a -> TerM a
    terModifyUsableVars ((VarSet -> VarSet) -> TerM a -> TerM a)
    -> (VarSet -> VarSet -> VarSet) -> VarSet -> TerM a -> TerM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VarSet -> VarSet -> VarSet
    forall a b. a -> b -> a
    const

    -- | Lens for 'terUseSizeLt'.

    terGetUseSizeLt :: TerM Bool
    terGetUseSizeLt :: TerM Bool
    terGetUseSizeLt = (TerEnv -> Bool) -> TerM Bool
    forall a. (TerEnv -> a) -> TerM a
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Bool
    terUseSizeLt

    terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a
    terModifyUseSizeLt :: forall a. (Bool -> Bool) -> TerM a -> TerM a
    terModifyUseSizeLt Bool -> Bool
    f = (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a. (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal ((TerEnv -> TerEnv) -> TerM a -> TerM a)
    -> (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall a b. (a -> b) -> a -> b
    $ \ TerEnv
    e -> TerEnv
    e { terUseSizeLt = f $ terUseSizeLt e }

    terSetUseSizeLt :: Bool -> TerM a -> TerM a
    terSetUseSizeLt :: forall a. Bool -> TerM a -> TerM a
    terSetUseSizeLt = (Bool -> Bool) -> TerM a -> TerM a
    forall a. (Bool -> Bool) -> TerM a -> TerM a
    terModifyUseSizeLt ((Bool -> Bool) -> TerM a -> TerM a)
    -> (Bool -> Bool -> Bool) -> Bool -> TerM a -> TerM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const

    -- | Compute usable vars from patterns and run subcomputation.
    withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b
    withUsableVars :: forall a b. UsableSizeVars a => a -> TerM b -> TerM b
    withUsableVars a
    pats TerM b
    m = do
      vars <- a -> TerM VarSet
    forall a. UsableSizeVars a => a -> TerM VarSet
    usableSizeVars a
    pats
      reportSLn "term.size" 70 $ "usableSizeVars = " ++ show vars
      reportSDoc "term.size" 20 $ if null vars then "no usuable size vars" else
        "the size variables amoung these variables are usable: " <+>
          sep (map (prettyTCM . var) $ VarSet.toList vars)
      terSetUsableVars vars $ m

    -- | Set 'terUseSizeLt' when going under constructor @c@.
    conUseSizeLt :: QName -> TerM a -> TerM a
    conUseSizeLt :: forall a. QName -> TerM a -> TerM a
    conUseSizeLt QName
    c TerM a
    m = do
      TerM Bool -> TerM a -> TerM a -> TerM a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (TCM Bool -> TerM Bool
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Bool -> TerM Bool) -> TCM Bool -> TerM Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaOrCoinductiveRecordConstructor QName
    c)  -- Non-eta inductive records are the same as datatypes
        (Bool -> TerM a -> TerM a
    forall a. Bool -> TerM a -> TerM a
    terSetUseSizeLt Bool
    False TerM a
    m)
        (Bool -> TerM a -> TerM a
    forall a. Bool -> TerM a -> TerM a
    terSetUseSizeLt Bool
    True TerM a
    m)

    -- | Set 'terUseSizeLt' for arguments following projection @q@.
    --   We disregard j<i after a non-coinductive projection.
    --   However, the projection need not be recursive (Issue 1470).
    projUseSizeLt :: QName -> TerM a -> TerM a
    projUseSizeLt :: forall a. QName -> TerM a -> TerM a
    projUseSizeLt QName
    q TerM a
    m = do
      co <- Bool -> QName -> TerM Bool
    forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
    isCoinductiveProjection Bool
    False QName
    q
      reportSLn "term.size" 20 $ applyUnless co ("not " ++) $
        "using SIZELT vars after projection " ++ prettyShow q
      terSetUseSizeLt co m

    -- | For termination checking purposes flat should not be considered a
    --   projection. That is, it flat doesn't preserve either structural order
    --   or guardedness like other projections do.
    --   Andreas, 2012-06-09: the same applies to projections of recursive records.
    isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool
    isProjectionButNotCoinductive :: forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Bool
    isProjectionButNotCoinductive QName
    qn = TCM Bool -> tcm Bool
    forall a. TCM a -> tcm a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Bool -> tcm Bool) -> TCM Bool -> tcm Bool
    forall a b. (a -> b) -> a -> b
    $ do
      b <- QName -> TCM Bool
    isProjectionButNotCoinductive' QName
    qn
      reportSDoc "term.proj" 60 $ do
        "identifier" <+> prettyTCM qn <+> do
          text $
            if b then "is an inductive projection"
              else "is either not a projection or coinductive"
      return b
      where
        isProjectionButNotCoinductive' :: QName -> TCM Bool
    isProjectionButNotCoinductive' QName
    qn = do
          flat <- (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CoinductionKit -> QName
    nameOfFlat (Maybe CoinductionKit -> Maybe QName)
    -> TCMT IO (Maybe CoinductionKit) -> TCMT IO (Maybe QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe CoinductionKit)
    coinductionKit
          if Just qn == flat
            then return False
            else do
              mp <- isProjection qn
              case mp of
                Just Projection{ projProper :: Projection -> Maybe QName
    projProper = Just{}, projFromType :: Projection -> Arg QName
    projFromType = Arg QName
    t }
                  -> QName -> TCM Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isInductiveRecord (Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    t)
                Maybe Projection
    _ -> Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | Check whether a projection belongs to a coinductive record
    --   and is actually recursive.
    --   E.g.
    --   @
    --      isCoinductiveProjection (Stream.head) = return False
    --
    --      isCoinductiveProjection (Stream.tail) = return True
    --   @
    isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool
    isCoinductiveProjection :: forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
    isCoinductiveProjection Bool
    mustBeRecursive QName
    q = TCM Bool -> tcm Bool
    forall a. TCM a -> tcm a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Bool -> tcm Bool) -> TCM Bool -> tcm Bool
    forall a b. (a -> b) -> a -> b
    $ do
      String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.guardedness" Int
    40 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "checking isCoinductiveProjection " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q
      flat <- (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CoinductionKit -> QName
    nameOfFlat (Maybe CoinductionKit -> Maybe QName)
    -> TCMT IO (Maybe CoinductionKit) -> TCMT IO (Maybe QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe CoinductionKit)
    coinductionKit
      -- yes for ♭
      if Just q == flat then return True else do
        pdef <- getConstInfo q
        case isProjection_ (theDef pdef) of
          Just Projection{ projProper :: Projection -> Maybe QName
    projProper = Just{}, projFromType :: Projection -> Arg QName
    projFromType = Arg ArgInfo
    _ QName
    r, projIndex :: Projection -> Int
    projIndex = Int
    n } ->
            TCMT IO (Maybe RecordData)
    -> TCM Bool -> (RecordData -> TCM Bool) -> TCM Bool
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> TCMT IO (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    r) TCM Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((RecordData -> TCM Bool) -> TCM Bool)
    -> (RecordData -> TCM Bool) -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ \ RecordData
    rdef -> do
              -- no for inductive or non-recursive record
              if RecordData -> Maybe Induction
    _recInduction RecordData
    rdef Maybe Induction -> Maybe Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Induction -> Maybe Induction
    forall a. a -> Maybe a
    Just Induction
    CoInductive then Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False else do
                String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.guardedness" Int
    40 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " is coinductive; record type is " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    r
                if Bool -> Bool
    not Bool
    mustBeRecursive then Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True else do
                  String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.guardedness" Int
    40 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " must be recursive"
                  if RecordData -> Bool
    notSafeRecRecursive RecordData
    rdef then Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False else do
                    String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.guardedness" Int
    40 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " has been declared recursive, doing actual check now..."
                    -- TODO: the following test for recursiveness of a projection should be cached.
                    -- E.g., it could be stored in the @Projection@ component.
                    -- Now check if type of field mentions mutually recursive symbol.
                    -- Get the type of the field by dropping record parameters and record argument.
                    let TelV Telescope
    tel Type
    core = Type -> TelV Type
    telView' (Definition -> Type
    defType Definition
    pdef)
                        ([Dom (String, Type)]
    pars, [Dom (String, Type)]
    tel') = Int
    -> [Dom (String, Type)]
    -> ([Dom (String, Type)], [Dom (String, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n ([Dom (String, Type)]
     -> ([Dom (String, Type)], [Dom (String, Type)]))
    -> [Dom (String, Type)]
    -> ([Dom (String, Type)], [Dom (String, Type)])
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel
                        mut :: [QName]
    mut = [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
    $ RecordData -> Maybe [QName]
    _recMutual RecordData
    rdef
                    -- Check if any recursive symbols appear in the record type.
                    -- Q (2014-07-01): Should we normalize the type?
                    -- A (2017-01-13): Yes, since we also normalize during positivity check?
                    -- See issue #1899.
                    String -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCM Doc -> m ()
    reportSDoc String
    "term.guardedness" Int
    40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc -> TCM Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                      [ TCM Doc
    "looking for recursive occurrences of"
                      , [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((QName -> TCM Doc) -> [QName] -> [TCM Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM [QName]
    mut)
                      , TCM Doc
    "in"
                      , [Dom (String, Type)] -> TCM Doc -> TCM Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    [Dom (String, Type)] -> m a -> m a
    addContext [Dom (String, Type)]
    pars (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM ([Dom (String, Type)] -> Telescope
    telFromList [Dom (String, Type)]
    tel')
                      , TCM Doc
    "and"
                      , Telescope -> TCM Doc -> TCM Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    core
                      ]
                    Bool -> TCMT IO () -> TCMT IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when ([QName] -> Bool
    forall a. Null a => a -> Bool
    null [QName]
    mut) TCMT IO ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    names <- (QName -> Bool) -> ([Type], Type) -> TCM MutualNames
    forall a. GetDefs a => (QName -> Bool) -> a -> TCM MutualNames
    anyDefs ([QName]
    mut [QName] -> QName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    `hasElem`) ((Dom (String, Type) -> Type) -> [Dom (String, Type)] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String, Type) -> Type
    forall a b. (a, b) -> b
    snd ((String, Type) -> Type)
    -> (Dom (String, Type) -> (String, Type))
    -> Dom (String, Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (String, Type) -> (String, Type)
    forall t e. Dom' t e -> e
    unDom) [Dom (String, Type)]
    tel', Type
    core)
                    reportSDoc "term.guardedness" 40 $
                      "found" <+> if null names then "none" else sep (map prettyTCM $ Set.toList names)
                    return $ not $ null names
          Maybe Projection
    _ -> do
            String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.guardedness" Int
    40 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not a proper projection"
            Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      where
      -- Andreas, 2018-02-24, issue #2975, example:
      -- @
      -- record R : Set where
      --   coinductive
      --   field force : R

      --   r : R
      --   force r = r
      -- @
      -- The termination checker expects the positivity checker to have run on the
      -- record declaration R to know whether R is recursive.
      -- However, here, because the awkward processing of record declarations (see #434),
      -- that has not happened.  To avoid crashing (as in Agda 2.5.3),
      -- we rather give the possibly wrong answer here,
      -- restoring the behavior of Agda 2.5.2.  TODO: fix record declaration checking.
      notSafeRecRecursive :: RecordData -> Bool
      notSafeRecRecursive :: RecordData -> Bool
    notSafeRecRecursive = Bool -> ([QName] -> Bool) -> Maybe [QName] -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True [QName] -> Bool
    forall a. Null a => a -> Bool
    null (Maybe [QName] -> Bool)
    -> (RecordData -> Maybe [QName]) -> RecordData -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RecordData -> Maybe [QName]
    _recMutual
        -- @_recMutual@ should be something (@Just (_:_)@) to be safe

    -- * De Bruijn pattern stuff

    -- | How long is the path to the deepest atomic pattern?
    patternDepth :: forall a. Pattern' a -> Int
    patternDepth :: forall a. Pattern' a -> Int
    patternDepth = MaxNat -> Int
    getMaxNat (MaxNat -> Int) -> (Pattern' a -> MaxNat) -> Pattern' a -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern' a -> MaxNat -> MaxNat) -> Pattern' a -> MaxNat
    forall m. Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m
    forall a b m.
    (PatternLike a b, Monoid m) =>
    (Pattern' a -> m -> m) -> b -> m
    foldrPattern Pattern' a -> MaxNat -> MaxNat
    depth where
      depth :: Pattern' a -> MaxNat -> MaxNat
      depth :: Pattern' a -> MaxNat -> MaxNat
    depth ConP{} = MaxNat -> MaxNat
    forall a. Enum a => a -> a
    succ      -- add 1 to the maximum of the depth of the subpatterns
      depth Pattern' a
    _      = MaxNat -> MaxNat
    forall a. a -> a
    id        -- atomic pattern (leaf) has depth 0

    -- | A dummy pattern used to mask a pattern that cannot be used
    --   for structural descent.

    unusedVar :: DeBruijnPattern
    unusedVar :: DeBruijnPattern
    unusedVar = Literal -> DeBruijnPattern
    forall a. Literal -> Pattern' a
    litP (Text -> Literal
    LitString Text
    "term.unused.pat.var")

    -- | Extract variables from 'DeBruijnPattern's that could witness a decrease
    --   via a SIZELT constraint.
    --
    --   These variables must be under an inductive constructor (with no record
    --   constructor in the way), or after a coinductive projection (with no
    --   inductive one in the way).

    class UsableSizeVars a where
      usableSizeVars :: a -> TerM VarSet

    instance UsableSizeVars DeBruijnPattern where
      usableSizeVars :: DeBruijnPattern -> TerM VarSet
    usableSizeVars = (DeBruijnPattern -> TerM VarSet -> TerM VarSet)
    -> DeBruijnPattern -> TerM VarSet
    forall m.
    Monoid m =>
    (DeBruijnPattern -> m -> m) -> DeBruijnPattern -> m
    forall a b m.
    (PatternLike a b, Monoid m) =>
    (Pattern' a -> m -> m) -> b -> m
    foldrPattern ((DeBruijnPattern -> TerM VarSet -> TerM VarSet)
     -> DeBruijnPattern -> TerM VarSet)
    -> (DeBruijnPattern -> TerM VarSet -> TerM VarSet)
    -> DeBruijnPattern
    -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ \case
        VarP PatternInfo
    _ DBPatVar
    x   -> TerM VarSet -> TerM VarSet -> TerM VarSet
    forall a b. a -> b -> a
    const (TerM VarSet -> TerM VarSet -> TerM VarSet)
    -> TerM VarSet -> TerM VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ TerM Bool -> TerM VarSet -> TerM VarSet -> TerM VarSet
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM TerM Bool
    terGetUseSizeLt (VarSet -> TerM VarSet
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (VarSet -> TerM VarSet) -> VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ Int -> VarSet
    VarSet.singleton (Int -> VarSet) -> Int -> VarSet
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x) (TerM VarSet -> TerM VarSet) -> TerM VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $
                       {-else-} VarSet -> TerM VarSet
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return VarSet
    forall a. Monoid a => a
    mempty
        ConP ConHead
    c ConPatternInfo
    _ [NamedArg DeBruijnPattern]
    _ -> QName -> TerM VarSet -> TerM VarSet
    forall a. QName -> TerM a -> TerM a
    conUseSizeLt (QName -> TerM VarSet -> TerM VarSet)
    -> QName -> TerM VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c
        LitP{}     -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        DotP{}     -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        ProjP{}    -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        IApplyP{}  -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        DefP{} -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        where none :: p -> m a
    none p
    _ = a -> m a
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    forall a. Monoid a => a
    mempty

    instance UsableSizeVars [DeBruijnPattern] where
      usableSizeVars :: [DeBruijnPattern] -> TerM VarSet
    usableSizeVars [DeBruijnPattern]
    ps =
        case [DeBruijnPattern]
    ps of
          []               -> VarSet -> TerM VarSet
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return VarSet
    forall a. Monoid a => a
    mempty
          (ProjP ProjOrigin
    _ QName
    q : [DeBruijnPattern]
    ps) -> QName -> TerM VarSet -> TerM VarSet
    forall a. QName -> TerM a -> TerM a
    projUseSizeLt QName
    q (TerM VarSet -> TerM VarSet) -> TerM VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ [DeBruijnPattern] -> TerM VarSet
    forall a. UsableSizeVars a => a -> TerM VarSet
    usableSizeVars [DeBruijnPattern]
    ps
          (DeBruijnPattern
    p         : [DeBruijnPattern]
    ps) -> VarSet -> VarSet -> VarSet
    forall a. Monoid a => a -> a -> a
    mappend (VarSet -> VarSet -> VarSet)
    -> TerM VarSet -> TerM (VarSet -> VarSet)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DeBruijnPattern -> TerM VarSet
    forall a. UsableSizeVars a => a -> TerM VarSet
    usableSizeVars DeBruijnPattern
    p TerM (VarSet -> VarSet) -> TerM VarSet -> TerM VarSet
    forall a b. TerM (a -> b) -> TerM a -> TerM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [DeBruijnPattern] -> TerM VarSet
    forall a. UsableSizeVars a => a -> TerM VarSet
    usableSizeVars [DeBruijnPattern]
    ps

    instance UsableSizeVars (Masked DeBruijnPattern) where
      usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet
    usableSizeVars (Masked Bool
    m DeBruijnPattern
    p) = ((DeBruijnPattern -> TerM VarSet -> TerM VarSet)
    -> DeBruijnPattern -> TerM VarSet
    forall m.
    Monoid m =>
    (DeBruijnPattern -> m -> m) -> DeBruijnPattern -> m
    forall a b m.
    (PatternLike a b, Monoid m) =>
    (Pattern' a -> m -> m) -> b -> m
    `foldrPattern` DeBruijnPattern
    p) ((DeBruijnPattern -> TerM VarSet -> TerM VarSet) -> TerM VarSet)
    -> (DeBruijnPattern -> TerM VarSet -> TerM VarSet) -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ \case
        VarP PatternInfo
    _ DBPatVar
    x   -> TerM VarSet -> TerM VarSet -> TerM VarSet
    forall a b. a -> b -> a
    const (TerM VarSet -> TerM VarSet -> TerM VarSet)
    -> TerM VarSet -> TerM VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ TerM Bool -> TerM VarSet -> TerM VarSet -> TerM VarSet
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM TerM Bool
    terGetUseSizeLt (VarSet -> TerM VarSet
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (VarSet -> TerM VarSet) -> VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ Int -> VarSet
    VarSet.singleton (Int -> VarSet) -> Int -> VarSet
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x) (TerM VarSet -> TerM VarSet) -> TerM VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $
                       {-else-} VarSet -> TerM VarSet
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return VarSet
    forall a. Monoid a => a
    mempty
        ConP ConHead
    c ConPatternInfo
    _ [NamedArg DeBruijnPattern]
    _ -> if Bool
    m then TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none else QName -> TerM VarSet -> TerM VarSet
    forall a. QName -> TerM a -> TerM a
    conUseSizeLt (QName -> TerM VarSet -> TerM VarSet)
    -> QName -> TerM VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c
        LitP{}     -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        DotP{}     -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        ProjP{}    -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        IApplyP{}  -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        DefP{}     -> TerM VarSet -> TerM VarSet
    forall {m :: * -> *} {a} {p}. (Monad m, Monoid a) => p -> m a
    none
        where none :: p -> m a
    none p
    _ = a -> m a
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    forall a. Monoid a => a
    mempty

    instance UsableSizeVars MaskedDeBruijnPatterns where
      usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet
    usableSizeVars MaskedDeBruijnPatterns
    ps =
        case MaskedDeBruijnPatterns
    ps of
          []                          -> VarSet -> TerM VarSet
    forall a. a -> TerM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return VarSet
    forall a. Monoid a => a
    mempty
          (Masked Bool
    _ (ProjP ProjOrigin
    _ QName
    q) : MaskedDeBruijnPatterns
    ps) -> QName -> TerM VarSet -> TerM VarSet
    forall a. QName -> TerM a -> TerM a
    projUseSizeLt QName
    q (TerM VarSet -> TerM VarSet) -> TerM VarSet -> TerM VarSet
    forall a b. (a -> b) -> a -> b
    $ MaskedDeBruijnPatterns -> TerM VarSet
    forall a. UsableSizeVars a => a -> TerM VarSet
    usableSizeVars MaskedDeBruijnPatterns
    ps
          (Masked DeBruijnPattern
    p                    : MaskedDeBruijnPatterns
    ps) -> VarSet -> VarSet -> VarSet
    forall a. Monoid a => a -> a -> a
    mappend (VarSet -> VarSet -> VarSet)
    -> TerM VarSet -> TerM (VarSet -> VarSet)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Masked DeBruijnPattern -> TerM VarSet
    forall a. UsableSizeVars a => a -> TerM VarSet
    usableSizeVars Masked DeBruijnPattern
    p TerM (VarSet -> VarSet) -> TerM VarSet -> TerM VarSet
    forall a b. TerM (a -> b) -> TerM a -> TerM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> MaskedDeBruijnPatterns -> TerM VarSet
    forall a. UsableSizeVars a => a -> TerM VarSet
    usableSizeVars MaskedDeBruijnPatterns
    ps

    -- * Masked patterns (which are not eligible for structural descent, only for size descent)
    --   See issue #1023.

    type MaskedDeBruijnPatterns = [Masked DeBruijnPattern]

    data Masked a = Masked
      { forall a. Masked a -> Bool
    getMask   :: Bool  -- ^ True if thing not eligible for structural descent.
      , forall a. Masked a -> a
    getMasked :: a     -- ^ Thing.
      } deriving (Masked a -> Masked a -> Bool
    (Masked a -> Masked a -> Bool)
    -> (Masked a -> Masked a -> Bool) -> Eq (Masked a)
    forall a. Eq a => Masked a -> Masked a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => Masked a -> Masked a -> Bool
    == :: Masked a -> Masked a -> Bool
    $c/= :: forall a. Eq a => Masked a -> Masked a -> Bool
    /= :: Masked a -> Masked a -> Bool
    Eq, Eq (Masked a)
    Eq (Masked a) =>
    (Masked a -> Masked a -> Ordering)
    -> (Masked a -> Masked a -> Bool)
    -> (Masked a -> Masked a -> Bool)
    -> (Masked a -> Masked a -> Bool)
    -> (Masked a -> Masked a -> Bool)
    -> (Masked a -> Masked a -> Masked a)
    -> (Masked a -> Masked a -> Masked a)
    -> Ord (Masked a)
    Masked a -> Masked a -> Bool
    Masked a -> Masked a -> Ordering
    Masked a -> Masked a -> Masked a
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall a. Ord a => Eq (Masked a)
    forall a. Ord a => Masked a -> Masked a -> Bool
    forall a. Ord a => Masked a -> Masked a -> Ordering
    forall a. Ord a => Masked a -> Masked a -> Masked a
    $ccompare :: forall a. Ord a => Masked a -> Masked a -> Ordering
    compare :: Masked a -> Masked a -> Ordering
    $c< :: forall a. Ord a => Masked a -> Masked a -> Bool
    < :: Masked a -> Masked a -> Bool
    $c<= :: forall a. Ord a => Masked a -> Masked a -> Bool
    <= :: Masked a -> Masked a -> Bool
    $c> :: forall a. Ord a => Masked a -> Masked a -> Bool
    > :: Masked a -> Masked a -> Bool
    $c>= :: forall a. Ord a => Masked a -> Masked a -> Bool
    >= :: Masked a -> Masked a -> Bool
    $cmax :: forall a. Ord a => Masked a -> Masked a -> Masked a
    max :: Masked a -> Masked a -> Masked a
    $cmin :: forall a. Ord a => Masked a -> Masked a -> Masked a
    min :: Masked a -> Masked a -> Masked a
    Ord, Int -> Masked a -> ShowS
    [Masked a] -> ShowS
    Masked a -> String
    (Int -> Masked a -> ShowS)
    -> (Masked a -> String) -> ([Masked a] -> ShowS) -> Show (Masked a)
    forall a. Show a => Int -> Masked a -> ShowS
    forall a. Show a => [Masked a] -> ShowS
    forall a. Show a => Masked a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> Masked a -> ShowS
    showsPrec :: Int -> Masked a -> ShowS
    $cshow :: forall a. Show a => Masked a -> String
    show :: Masked a -> String
    $cshowList :: forall a. Show a => [Masked a] -> ShowS
    showList :: [Masked a] -> ShowS
    Show, (forall a b. (a -> b) -> Masked a -> Masked b)
    -> (forall a b. a -> Masked b -> Masked a) -> Functor Masked
    forall a b. a -> Masked b -> Masked a
    forall a b. (a -> b) -> Masked a -> Masked b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Masked a -> Masked b
    fmap :: forall a b. (a -> b) -> Masked a -> Masked b
    $c<$ :: forall a b. a -> Masked b -> Masked a
    <$ :: forall a b. a -> Masked b -> Masked a
    Functor, (forall m. Monoid m => Masked m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Masked a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Masked a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Masked a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Masked a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Masked a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Masked a -> b)
    -> (forall a. (a -> a -> a) -> Masked a -> a)
    -> (forall a. (a -> a -> a) -> Masked a -> a)
    -> (forall a. Masked a -> [a])
    -> (forall a. Masked a -> Bool)
    -> (forall a. Masked a -> Int)
    -> (forall a. Eq a => a -> Masked a -> Bool)
    -> (forall a. Ord a => Masked a -> a)
    -> (forall a. Ord a => Masked a -> a)
    -> (forall a. Num a => Masked a -> a)
    -> (forall a. Num a => Masked a -> a)
    -> Foldable Masked
    forall a. Eq a => a -> Masked a -> Bool
    forall a. Num a => Masked a -> a
    forall a. Ord a => Masked a -> a
    forall m. Monoid m => Masked m -> m
    forall a. Masked a -> Bool
    forall a. Masked a -> Int
    forall a. Masked a -> [a]
    forall a. (a -> a -> a) -> Masked a -> a
    forall m a. Monoid m => (a -> m) -> Masked a -> m
    forall b a. (b -> a -> b) -> b -> Masked a -> b
    forall a b. (a -> b -> b) -> b -> Masked a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => Masked m -> m
    fold :: forall m. Monoid m => Masked m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Masked a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Masked a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Masked a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Masked a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Masked a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Masked a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Masked a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Masked a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Masked a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Masked a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Masked a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Masked a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Masked a -> a
    foldr1 :: forall a. (a -> a -> a) -> Masked a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Masked a -> a
    foldl1 :: forall a. (a -> a -> a) -> Masked a -> a
    $ctoList :: forall a. Masked a -> [a]
    toList :: forall a. Masked a -> [a]
    $cnull :: forall a. Masked a -> Bool
    null :: forall a. Masked a -> Bool
    $clength :: forall a. Masked a -> Int
    length :: forall a. Masked a -> Int
    $celem :: forall a. Eq a => a -> Masked a -> Bool
    elem :: forall a. Eq a => a -> Masked a -> Bool
    $cmaximum :: forall a. Ord a => Masked a -> a
    maximum :: forall a. Ord a => Masked a -> a
    $cminimum :: forall a. Ord a => Masked a -> a
    minimum :: forall a. Ord a => Masked a -> a
    $csum :: forall a. Num a => Masked a -> a
    sum :: forall a. Num a => Masked a -> a
    $cproduct :: forall a. Num a => Masked a -> a
    product :: forall a. Num a => Masked a -> a
    Foldable, Functor Masked
    Foldable Masked
    (Functor Masked, Foldable Masked) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Masked a -> f (Masked b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Masked (f a) -> f (Masked a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Masked a -> m (Masked b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Masked (m a) -> m (Masked a))
    -> Traversable Masked
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
    forall (f :: * -> *) a.
    Applicative f =>
    Masked (f a) -> f (Masked a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Masked a -> m (Masked b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Masked a -> f (Masked b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Masked a -> f (Masked b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Masked a -> f (Masked b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Masked (f a) -> f (Masked a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Masked (f a) -> f (Masked a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Masked a -> m (Masked b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Masked a -> m (Masked b)
    $csequence :: forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
    sequence :: forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
    Traversable)

    masked :: a -> Masked a
    masked :: forall a. a -> Masked a
    masked = Bool -> a -> Masked a
    forall a. Bool -> a -> Masked a
    Masked Bool
    True

    notMasked :: a -> Masked a
    notMasked :: forall a. a -> Masked a
    notMasked = Bool -> a -> Masked a
    forall a. Bool -> a -> Masked a
    Masked Bool
    False

    instance Decoration Masked where
      traverseF :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> Masked a -> m (Masked b)
    traverseF a -> m b
    f (Masked Bool
    m a
    a) = Bool -> b -> Masked b
    forall a. Bool -> a -> Masked a
    Masked Bool
    m (b -> Masked b) -> m b -> m (Masked b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    f a
    a

    -- | Print masked things in double parentheses.
    instance PrettyTCM a => PrettyTCM (Masked a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Masked a -> m Doc
    prettyTCM (Masked Bool
    m a
    a) = Bool -> (m Doc -> m Doc) -> m Doc -> m Doc
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen Bool
    m (m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> (m Doc -> m Doc) -> m Doc -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens) (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    a

    -- * Call pathes

    -- | Call paths.

    -- An old comment:
    --
    --   The call information is stored as free monoid
    --   over 'CallInfo'.  As long as we never look at it,
    --   only accumulate it, it does not matter whether we use
    --   'Set', (nub) list, or 'Tree'.
    --   Internally, due to lazyness, it is anyway a binary tree of
    --   'mappend' nodes and singleton leafs.
    --   Since we define no order on 'CallInfo' (expensive),
    --   we cannot use a 'Set' or nub list.
    --   Performance-wise, I could not see a difference between Set and list.
    --
    -- If the binary tree is balanced "incorrectly", then forcing it could
    -- be expensive, so a switch was made to difference lists.

    newtype CallPath = CallPath (DList CallInfo)
      deriving (Int -> CallPath -> ShowS
    [CallPath] -> ShowS
    CallPath -> String
    (Int -> CallPath -> ShowS)
    -> (CallPath -> String) -> ([CallPath] -> ShowS) -> Show CallPath
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> CallPath -> ShowS
    showsPrec :: Int -> CallPath -> ShowS
    $cshow :: CallPath -> String
    show :: CallPath -> String
    $cshowList :: [CallPath] -> ShowS
    showList :: [CallPath] -> ShowS
    Show, NonEmpty CallPath -> CallPath
    CallPath -> CallPath -> CallPath
    (CallPath -> CallPath -> CallPath)
    -> (NonEmpty CallPath -> CallPath)
    -> (forall b. Integral b => b -> CallPath -> CallPath)
    -> Semigroup CallPath
    forall b. Integral b => b -> CallPath -> CallPath
    forall a.
    (a -> a -> a)
    -> (NonEmpty a -> a)
    -> (forall b. Integral b => b -> a -> a)
    -> Semigroup a
    $c<> :: CallPath -> CallPath -> CallPath
    <> :: CallPath -> CallPath -> CallPath
    $csconcat :: NonEmpty CallPath -> CallPath
    sconcat :: NonEmpty CallPath -> CallPath
    $cstimes :: forall b. Integral b => b -> CallPath -> CallPath
    stimes :: forall b. Integral b => b -> CallPath -> CallPath
    Semigroup, Semigroup CallPath
    CallPath
    Semigroup CallPath =>
    CallPath
    -> (CallPath -> CallPath -> CallPath)
    -> ([CallPath] -> CallPath)
    -> Monoid CallPath
    [CallPath] -> CallPath
    CallPath -> CallPath -> CallPath
    forall a.
    Semigroup a =>
    a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
    $cmempty :: CallPath
    mempty :: CallPath
    $cmappend :: CallPath -> CallPath -> CallPath
    mappend :: CallPath -> CallPath -> CallPath
    $cmconcat :: [CallPath] -> CallPath
    mconcat :: [CallPath] -> CallPath
    Monoid)

    -- | The calls making up the call path.

    callInfos :: CallPath -> [CallInfo]
    callInfos :: CallPath -> [CallInfo]
    callInfos (CallPath DList CallInfo
    cs) = DList CallInfo -> [CallInfo]
    forall a. DList a -> [a]
    DL.toList DList CallInfo
    cs

    -- | Only show intermediate nodes.  (Drop last 'CallInfo').
    instance Pretty CallPath where
      pretty :: CallPath -> Doc
    pretty CallPath
    cis0 = if [CallInfo] -> Bool
    forall a. Null a => a -> Bool
    null [CallInfo]
    cis then Doc
    forall a. Null a => a
    empty else
        [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.hsep ((CallInfo -> Doc) -> [CallInfo] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ CallInfo
    ci -> Doc
    arrow Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> CallInfo -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty CallInfo
    ci) [CallInfo]
    cis) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> Doc
    arrow
        where
          cis :: [CallInfo]
    cis   = [CallInfo] -> [CallInfo]
    forall a. HasCallStack => [a] -> [a]
    init (CallPath -> [CallInfo]
    callInfos CallPath
    cis0)
          arrow :: Doc
    arrow = Doc
    "-->"

    -- * Size depth estimation

    -- | A very crude way of estimating the @SIZELT@ chains
    --   @i > j > k@ in context.  Returns 3 in this case.
    --   Overapproximates.
    class TerSetSizeDepth b where
      terSetSizeDepth :: b -> TerM a -> TerM a

    instance TerSetSizeDepth Telescope where
      terSetSizeDepth :: forall a. Telescope -> TerM a -> TerM a
    terSetSizeDepth = [Dom (String, Type)] -> TerM a -> TerM a
    forall a. [Dom (String, Type)] -> TerM a -> TerM a
    forall b a. TerSetSizeDepth b => b -> TerM a -> TerM a
    terSetSizeDepth ([Dom (String, Type)] -> TerM a -> TerM a)
    -> (Telescope -> [Dom (String, Type)])
    -> Telescope
    -> TerM a
    -> TerM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList

    -- TODO: more precise analysis, constructing a tree
    -- of relations between size variables.
    instance TerSetSizeDepth ListTel where
      terSetSizeDepth :: forall a. [Dom (String, Type)] -> TerM a -> TerM a
    terSetSizeDepth [Dom (String, Type)]
    doms TerM a
    cont = do
        n <- TCM Int -> TerM Int
    forall a. TCM a -> TerM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Int -> TerM Int) -> TCM Int -> TerM Int
    forall a b. (a -> b) -> a -> b
    $ [Int] -> Int
    forall a. Num a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([Int] -> Int) -> TCMT IO [Int] -> TCM Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          [Dom (String, Type)]
    -> (Dom (String, Type) -> TCM Int) -> TCMT IO [Int]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Dom (String, Type)]
    doms ((Dom (String, Type) -> TCM Int) -> TCMT IO [Int])
    -> (Dom (String, Type) -> TCM Int) -> TCMT IO [Int]
    forall a b. (a -> b) -> a -> b
    $ \ Dom (String, Type)
    dom -> do
            -- Andreas, 2022-03-12, TODO:
            -- use ifBlocked?  Shouldn't blocked types be treated like metas?
            a <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> TCMT IO Type) -> Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ (String, Type) -> Type
    forall a b. (a, b) -> b
    snd ((String, Type) -> Type) -> (String, Type) -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom (String, Type) -> (String, Type)
    forall t e. Dom' t e -> e
    unDom Dom (String, Type)
    dom
            ifM (isJust <$> isSizeType a) (return 1) {- else -} $
              case unEl a of
                MetaV{} -> Int -> TCM Int
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    1
                Term
    _       -> Int -> TCM Int
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    0
        terLocal (set terSizeDepth n) cont