    -- | 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 qualified Control.Monad.Fail as Fail

    import Control.Monad          ( forM )
    import Control.Monad.IO.Class ( MonadIO(..) )
    import Control.Monad.Except
    import Control.Monad.Reader

    import Data.Semigroup ( Semigroup(..) )
    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.Syntax.Position (noRange)

    import Agda.Termination.CutOff
    import Agda.Termination.Order (Order,le,unknown)
    import Agda.Termination.RecCheck (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.Utils.Pretty (Pretty, prettyShow)
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.VarSet (VarSet)
    import qualified Agda.Utils.VarSet as VarSet

    import Agda.Utils.Impossible

    -- | The mutual block we are checking.
    --
    --   The functions are numbered according to their order of appearance
    --   in this list.

    type MutualNames = [QName]

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

    type Target = QName

    -- | 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 :: [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 -> Maybe QName
    terTarget  :: Maybe Target
        -- ^ Target type of the function we are currently termination checking.
        --   Only the constructors of 'Target' are considered guarding.
      , TerEnv -> Delayed
    terDelayed :: Delayed
        -- ^ Are we checking a delayed definition?
      , 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 :: Bool
    -> Maybe QName
    -> Maybe QName
    -> CutOff
    -> QName
    -> MutualNames
    -> MutualNames
    -> Bool
    -> Maybe QName
    -> Delayed
    -> [Bool]
    -> Bool
    -> Int
    -> MaskedDeBruijnPatterns
    -> Int
    -> Guarded
    -> Bool
    -> VarSet
    -> TerEnv
    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 :: Maybe QName
    terTarget                   = Maybe QName
    forall a. Maybe a
    Nothing
      , terDelayed :: Delayed
    terDelayed                  = Delayed
    NotDelayed
      , 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
    <$ :: forall a b. a -> TerM b -> TerM a
    $c<$ :: forall a b. a -> TerM b -> TerM a
    fmap :: forall a b. (a -> b) -> TerM a -> TerM b
    $cfmap :: forall a b. (a -> b) -> TerM a -> TerM b
    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
    <* :: forall a b. TerM a -> TerM b -> TerM a
    $c<* :: forall a b. TerM a -> TerM b -> TerM a
    *> :: forall a b. TerM a -> TerM b -> TerM b
    $c*> :: forall a b. TerM a -> TerM b -> TerM b
    liftA2 :: forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
    $cliftA2 :: forall a b c. (a -> b -> c) -> TerM a -> TerM b -> TerM c
    <*> :: forall a b. TerM (a -> b) -> TerM a -> TerM b
    $c<*> :: forall a b. TerM (a -> b) -> TerM a -> TerM b
    pure :: forall a. a -> TerM a
    $cpure :: forall a. a -> 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
    return :: forall a. a -> TerM a
    $creturn :: forall a. a -> TerM a
    >> :: forall a b. TerM a -> TerM b -> TerM b
    $c>> :: forall a b. TerM a -> TerM b -> TerM b
    >>= :: forall a b. TerM a -> (a -> TerM b) -> TerM b
    $c>>= :: forall a b. TerM a -> (a -> TerM b) -> TerM b
    Monad
               , Monad TerM
    Monad TerM -> (forall a. String -> TerM a) -> MonadFail TerM
    forall a. String -> TerM a
    forall (m :: * -> *).
    Monad m -> (forall a. String -> m a) -> MonadFail m
    fail :: forall a. String -> TerM a
    $cfail :: forall a. String -> TerM a
    Fail.MonadFail
               , 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
    modifyCounter :: String -> (Integer -> Integer) -> TerM ()
    $cmodifyCounter :: 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
    commandLineOptions :: TerM CommandLineOptions
    $ccommandLineOptions :: TerM CommandLineOptions
    pragmaOptions :: TerM PragmaOptions
    $cpragmaOptions :: TerM PragmaOptions
    HasOptions
               , Functor TerM
    MonadFail TerM
    Applicative TerM
    Functor TerM
    -> Applicative TerM
    -> MonadFail TerM
    -> (String -> TerM (Maybe (Builtin PrimFun)))
    -> HasBuiltins TerM
    String -> TerM (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    Functor m
    -> Applicative m
    -> MonadFail m
    -> (String -> m (Maybe (Builtin PrimFun)))
    -> HasBuiltins m
    getBuiltinThing :: String -> TerM (Maybe (Builtin PrimFun))
    $cgetBuiltinThing :: String -> TerM (Maybe (Builtin PrimFun))
    HasBuiltins
               , Monad TerM
    Functor TerM
    Applicative TerM
    TerM Bool
    TerM Verbosity
    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 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 Bool
    -> (forall a. m a -> m a)
    -> MonadDebug m
    nowDebugPrinting :: forall a. TerM a -> TerM a
    $cnowDebugPrinting :: forall a. TerM a -> TerM a
    isDebugPrinting :: TerM Bool
    $cisDebugPrinting :: TerM Bool
    getVerbosity :: TerM Verbosity
    $cgetVerbosity :: TerM Verbosity
    verboseBracket :: forall a. String -> Int -> String -> TerM a -> TerM a
    $cverboseBracket :: forall a. String -> Int -> String -> TerM a -> TerM a
    traceDebugMessage :: forall a. String -> Int -> String -> TerM a -> TerM a
    $ctraceDebugMessage :: forall a. String -> Int -> String -> TerM a -> TerM a
    formatDebugMessage :: String -> Int -> TCM Doc -> TerM String
    $cformatDebugMessage :: String -> Int -> TCM Doc -> TerM String
    MonadDebug
               , Functor TerM
    MonadFail TerM
    Applicative TerM
    MonadDebug TerM
    HasOptions TerM
    MonadTCEnv TerM
    Functor TerM
    -> Applicative TerM
    -> MonadFail 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
    -> MonadFail m
    -> HasOptions m
    -> MonadDebug m
    -> MonadTCEnv m
    -> (QName -> m Definition)
    -> (QName -> m (Either SigError Definition))
    -> (QName -> m RewriteRules)
    -> HasConstInfo m
    getRewriteRulesFor :: QName -> TerM RewriteRules
    $cgetRewriteRulesFor :: QName -> TerM RewriteRules
    getConstInfo' :: QName -> TerM (Either SigError Definition)
    $cgetConstInfo' :: QName -> TerM (Either SigError Definition)
    getConstInfo :: QName -> TerM Definition
    $cgetConstInfo :: QName -> TerM Definition
    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
    liftIO :: forall a. IO a -> TerM a
    $cliftIO :: 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
    localTC :: forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
    $clocalTC :: forall a. (TCEnv -> TCEnv) -> TerM a -> TerM a
    askTC :: TerM TCEnv
    $caskTC :: TerM TCEnv
    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
    modifyTC :: (TCState -> TCState) -> TerM ()
    $cmodifyTC :: (TCState -> TCState) -> TerM ()
    putTC :: TCState -> TerM ()
    $cputTC :: TCState -> TerM ()
    getTC :: TerM TCState
    $cgetTC :: TerM TCState
    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
    liftTCM :: forall a. TCM a -> TerM a
    $cliftTCM :: forall a. TCM a -> TerM a
    MonadTCM
               , Monad TerM
    TerM TCState
    Monad TerM
    -> TerM TCState
    -> (forall a b. Lens' a TCState -> (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' a TCState -> (a -> a) -> TerM b -> TerM b
    forall (m :: * -> *).
    Monad m
    -> m TCState
    -> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
    -> (forall a. (TCState -> TCState) -> m a -> m a)
    -> ReadTCState m
    withTCState :: forall a. (TCState -> TCState) -> TerM a -> TerM a
    $cwithTCState :: forall a. (TCState -> TCState) -> TerM a -> TerM a
    locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> TerM b -> TerM b
    $clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> TerM b -> TerM b
    getTCState :: TerM TCState
    $cgetTCState :: TerM TCState
    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
    liftReduce :: forall a. ReduceM a -> TerM a
    $cliftReduce :: forall a. ReduceM a -> TerM a
    MonadReduce
               , MonadTCEnv TerM
    MonadTCEnv TerM
    -> (forall a. Name -> Dom Type -> TerM a -> TerM a)
    -> (forall a. 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. 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. 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
    withFreshName :: forall a. Range -> String -> (Name -> TerM a) -> TerM a
    $cwithFreshName :: forall a. Range -> String -> (Name -> TerM a) -> TerM a
    updateContext :: forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
    $cupdateContext :: forall a. Substitution -> (Context -> Context) -> TerM a -> TerM a
    addLetBinding' :: forall a. Name -> Term -> Dom Type -> TerM a -> TerM a
    $caddLetBinding' :: forall a. Name -> Term -> Dom Type -> TerM a -> TerM a
    addCtx :: forall a. Name -> Dom Type -> TerM a -> TerM a
    $caddCtx :: forall a. Name -> Dom Type -> TerM a -> TerM a
    MonadAddContext
               , MonadDebug TerM
    MonadTCEnv TerM
    MonadReduce TerM
    ReadTCState TerM
    MonadAddContext TerM
    HasBuiltins 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 Phase) -> TerM (Benchmark Phase)
    forall a. ReaderT TerEnv TCM a -> TerM a
    TerM (ReaderT TerEnv TCM (Benchmark Phase) -> TerM (Benchmark Phase))
    -> ReaderT TerEnv TCM (Benchmark Phase) -> TerM (Benchmark Phase)
    forall a b. (a -> b) -> a -> b
    $ ReaderT TerEnv TCM (Benchmark Phase)
    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 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 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 (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 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 -> TCM 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
    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)
      Maybe QName
    suc <- TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, HasOptions m) =>
    m (Maybe QName)
    sizeSucName

      -- The name of sharp (if available).
      Maybe QName
    sharp <- (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CoinductionKit -> QName
    nameOfSharp (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

      let tenv :: TerEnv
    tenv = TerEnv
    defaultTerEnv
            { terSizeSuc :: Maybe QName
    terSizeSuc                  = Maybe QName
    suc
            , terSharp :: Maybe QName
    terSharp                    = Maybe QName
    sharp
            , terCutOff :: CutOff
    terCutOff                   = CutOff
    cutoff
            }

      TerEnv -> TerM a -> TCM a
    forall a. TerEnv -> TerM a -> TCM a
    runTer TerEnv
    tenv TerM a
    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 (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 (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)
    sequence

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

    terGetUseDotPatterns :: TerM Bool
    terGetUseDotPatterns :: TerM Bool
    terGetUseDotPatterns = (TerEnv -> Bool) -> TerM Bool
    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 (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 :: Bool
    terUseDotPatterns = Bool
    b }

    terGetSizeSuc :: TerM (Maybe QName)
    terGetSizeSuc :: TerM (Maybe QName)
    terGetSizeSuc = (TerEnv -> Maybe QName) -> TerM (Maybe QName)
    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 (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 (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 :: QName
    terCurrent = QName
    q }

    terGetSharp :: TerM (Maybe QName)
    terGetSharp :: TerM (Maybe QName)
    terGetSharp = (TerEnv -> Maybe QName) -> TerM (Maybe QName)
    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 (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> CutOff
    terCutOff

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

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

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

    terSetTarget :: Maybe Target -> TerM a -> TerM a
    terSetTarget :: forall a. Maybe QName -> TerM a -> TerM a
    terSetTarget Maybe QName
    t = (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 :: Maybe QName
    terTarget = Maybe QName
    t }

    terGetHaveInlinedWith :: TerM Bool
    terGetHaveInlinedWith :: TerM Bool
    terGetHaveInlinedWith = (TerEnv -> Bool) -> TerM Bool
    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 (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 :: Bool
    terHaveInlinedWith = Bool
    True }

    terGetDelayed :: TerM Delayed
    terGetDelayed :: TerM Delayed
    terGetDelayed = (TerEnv -> Delayed) -> TerM Delayed
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Delayed
    terDelayed

    terSetDelayed :: Delayed -> TerM a -> TerM a
    terSetDelayed :: forall a. Delayed -> TerM a -> TerM a
    terSetDelayed Delayed
    b = (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 { terDelayed :: Delayed
    terDelayed = Delayed
    b }

    terGetMaskArgs :: TerM [Bool]
    terGetMaskArgs :: TerM [Bool]
    terGetMaskArgs = (TerEnv -> [Bool]) -> TerM [Bool]
    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 (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 :: [Bool]
    terMaskArgs = [Bool]
    b }

    terGetMaskResult :: TerM Bool
    terGetMaskResult :: TerM Bool
    terGetMaskResult = (TerEnv -> Bool) -> TerM Bool
    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 (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 :: Bool
    terMaskResult = Bool
    b }

    terGetPatterns :: TerM (MaskedDeBruijnPatterns)
    terGetPatterns :: TerM MaskedDeBruijnPatterns
    terGetPatterns = do
      Int
    n   <- (TerEnv -> Int) -> TerM Int
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> Int
    terPatternsRaise
      MaskedDeBruijnPatterns
    mps <- (TerEnv -> MaskedDeBruijnPatterns) -> TerM MaskedDeBruijnPatterns
    forall (m :: * -> *) a. MonadTer m => (TerEnv -> a) -> m a
    terAsks TerEnv -> MaskedDeBruijnPatterns
    terPatterns
      MaskedDeBruijnPatterns -> TerM MaskedDeBruijnPatterns
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MaskedDeBruijnPatterns -> TerM MaskedDeBruijnPatterns)
    -> MaskedDeBruijnPatterns -> TerM MaskedDeBruijnPatterns
    forall a b. (a -> b) -> a -> b
    $ if Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then MaskedDeBruijnPatterns
    mps else (Masked DeBruijnPattern -> Masked DeBruijnPattern)
    -> MaskedDeBruijnPatterns -> MaskedDeBruijnPatterns
    forall a b. (a -> b) -> [a] -> [b]
    map ((DeBruijnPattern -> DeBruijnPattern)
    -> Masked DeBruijnPattern -> Masked DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Int -> DeBruijnPattern -> DeBruijnPattern
    forall a. Subst a => Int -> a -> a
    raise Int
    n)) MaskedDeBruijnPatterns
    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 (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 :: MaskedDeBruijnPatterns
    terPatterns = MaskedDeBruijnPatterns
    ps }

    terRaise :: TerM a -> TerM a
    terRaise :: forall a. TerM a -> TerM a
    terRaise = (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 :: Int
    terPatternsRaise = TerEnv -> Int
    terPatternsRaise TerEnv
    e Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 }

    terGetGuarded :: TerM Guarded
    terGetGuarded :: TerM Guarded
    terGetGuarded = (TerEnv -> Guarded) -> TerM Guarded
    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 (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 :: Guarded
    terGuarded = Guarded -> Guarded
    f (Guarded -> Guarded) -> Guarded -> Guarded
    forall a b. (a -> b) -> a -> b
    $ TerEnv -> Guarded
    terGuarded TerEnv
    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' Int TerEnv
    terSizeDepth :: Lens' Int TerEnv
    terSizeDepth Int -> f Int
    f TerEnv
    e = Int -> f Int
    f (TerEnv -> Int
    _terSizeDepth TerEnv
    e) f Int -> (Int -> TerEnv) -> f TerEnv
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Int
    i -> TerEnv
    e { _terSizeDepth :: Int
    _terSizeDepth = Int
    i }

    -- | Lens for 'terUsableVars'.

    terGetUsableVars :: TerM VarSet
    terGetUsableVars :: TerM VarSet
    terGetUsableVars = (TerEnv -> VarSet) -> TerM VarSet
    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 (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 :: VarSet
    terUsableVars = VarSet -> VarSet
    f (VarSet -> VarSet) -> VarSet -> VarSet
    forall a b. (a -> b) -> a -> b
    $ TerEnv -> VarSet
    terUsableVars TerEnv
    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 (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 (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 :: Bool
    terUseSizeLt = Bool -> Bool
    f (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ TerEnv -> Bool
    terUseSizeLt TerEnv
    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
      VarSet
    vars <- a -> TerM VarSet
    forall a. UsableSizeVars a => a -> TerM VarSet
    usableSizeVars a
    pats
      String -> Int -> String -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.size" Int
    70 (String -> TerM ()) -> String -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ String
    "usableSizeVars = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ VarSet -> String
    forall a. Show a => a -> String
    show VarSet
    vars
      String -> Int -> TCM Doc -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCM Doc -> m ()
    reportSDoc String
    "term.size" Int
    20 (TCM Doc -> TerM ()) -> TCM Doc -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ if VarSet -> Bool
    forall a. Null a => a -> Bool
    null VarSet
    vars then TCM Doc
    "no usuable size vars" else
        TCM Doc
    "the size variables amoung these variables are usable: " TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
          [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((Int -> TCM Doc) -> [Int] -> [TCM Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Term -> TCM Doc) -> (Int -> Term) -> Int -> TCM Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    var) ([Int] -> [TCM Doc]) -> [Int] -> [TCM Doc]
    forall a b. (a -> b) -> a -> b
    $ VarSet -> [Int]
    VarSet.toList VarSet
    vars)
      VarSet -> TerM b -> TerM b
    forall a. VarSet -> TerM a -> TerM a
    terSetUsableVars VarSet
    vars (TerM b -> TerM b) -> TerM b -> TerM b
    forall a b. (a -> b) -> a -> b
    $ TerM b
    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 (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
      Bool
    co <- Bool -> QName -> TerM Bool
    forall (tcm :: * -> *). MonadTCM tcm => Bool -> QName -> tcm Bool
    isCoinductiveProjection Bool
    False QName
    q
      String -> Int -> String -> TerM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "term.size" Int
    20 (String -> TerM ()) -> String -> TerM ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> (String -> String) -> String -> String
    forall a. Bool -> (a -> a) -> a -> a
    applyUnless Bool
    co (String
    "not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $
        String
    "using SIZELT vars after projection " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q
      Bool -> TerM a -> TerM a
    forall a. Bool -> TerM a -> TerM a
    terSetUseSizeLt Bool
    co TerM a
    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 (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
      Bool
    b <- QName -> TCM Bool
    isProjectionButNotCoinductive' QName
    qn
      String -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCM Doc -> m ()
    reportSDoc String
    "term.proj" Int
    60 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
        TCM Doc
    "identifier" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    qn TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do
          String -> TCM Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCM Doc) -> String -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $
            if Bool
    b then String
    "is an inductive projection"
              else String
    "is either not a projection or coinductive"
      Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    b
      where
        isProjectionButNotCoinductive' :: QName -> TCM Bool
    isProjectionButNotCoinductive' QName
    qn = do
          Maybe QName
    flat <- (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
    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 QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    qn Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    flat
            then Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
            else do
              Maybe Projection
    mp <- QName -> TCMT IO (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isProjection QName
    qn
              case Maybe Projection
    mp of
                Just Projection{ projProper :: Projection -> Maybe QName
    projProper = Just{}, projFromType :: Projection -> Arg QName
    projFromType = Arg QName
    t }
                  -> QName -> TCM Bool
    isInductiveRecord (Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    t)
                Maybe Projection
    _ -> Bool -> TCM Bool
    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 (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 -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q
      Maybe QName
    flat <- (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
    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 QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    flat then Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True else do
        Definition
    pdef <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
        case Defn -> Maybe Projection
    isProjection_ (Definition -> Defn
    theDef Definition
    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 Defn) -> TCM Bool -> (Defn -> 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 Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r) TCM Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((Defn -> TCM Bool) -> TCM Bool) -> (Defn -> TCM Bool) -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ \ Defn
    rdef -> do
              -- no for inductive or non-recursive record
              if Defn -> Maybe Induction
    recInduction Defn
    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 (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 -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is coinductive; record type is " String -> String -> String
    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 (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 -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " must be recursive"
                  if Bool -> Bool
    not (Defn -> Bool
    safeRecRecursive Defn
    rdef) then Bool -> TCM Bool
    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 -> String -> String
    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 :: MutualNames
    mut = MutualNames -> Maybe MutualNames -> MutualNames
    forall a. a -> Maybe a -> a
    fromMaybe MutualNames
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe MutualNames -> MutualNames)
    -> Maybe MutualNames -> MutualNames
    forall a b. (a -> b) -> a -> b
    $ Defn -> Maybe MutualNames
    recMutual Defn
    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) -> MutualNames -> [TCM Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MutualNames
    mut)
                      , TCM Doc
    "in"
                      , [Dom (String, Type)] -> TCM Doc -> TCM Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> 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
    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
    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
    prettyTCM Type
    core
                      ]
                    Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (MutualNames -> Bool
    forall a. Null a => a -> Bool
    null MutualNames
    mut) TCMT IO ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    Set QName
    names <- (QName -> Bool) -> ([Type], Type) -> TCM (Set QName)
    forall a. GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)
    anyDefs (MutualNames
    mut MutualNames -> 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)
                    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
    "found" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> if Set QName -> Bool
    forall a. Null a => a -> Bool
    null Set QName
    names then TCM Doc
    "none" else [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((QName -> TCM Doc) -> MutualNames -> [TCM Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (MutualNames -> [TCM Doc]) -> MutualNames -> [TCM Doc]
    forall a b. (a -> b) -> a -> b
    $ Set QName -> MutualNames
    forall a. Set a -> [a]
    Set.toList Set QName
    names)
                    Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> TCM Bool) -> Bool -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Set QName -> Bool
    forall a. Null a => a -> Bool
    null Set QName
    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 -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not a proper projection"
            Bool -> TCM Bool
    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.
      safeRecRecursive :: Defn -> Bool
      safeRecRecursive :: Defn -> Bool
    safeRecRecursive (Record { recMutual :: Defn -> Maybe MutualNames
    recMutual = Just MutualNames
    qs }) = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ MutualNames -> Bool
    forall a. Null a => a -> Bool
    null MutualNames
    qs
      safeRecRecursive Defn
    _ = Bool
    False

    -- * 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 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 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 (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 (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 (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 (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 (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 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 (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 (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 (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 (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 (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
    /= :: Masked a -> Masked a -> Bool
    $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
    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
    min :: Masked a -> Masked a -> Masked a
    $cmin :: forall a. Ord a => Masked a -> Masked a -> Masked a
    max :: Masked a -> Masked a -> Masked a
    $cmax :: forall a. Ord a => Masked a -> Masked a -> Masked a
    >= :: 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
    $c< :: forall a. Ord a => Masked a -> Masked a -> Bool
    compare :: Masked a -> Masked a -> Ordering
    $ccompare :: forall a. Ord a => Masked a -> Masked a -> Ordering
    Ord, Int -> Masked a -> String -> String
    [Masked a] -> String -> String
    Masked a -> String
    (Int -> Masked a -> String -> String)
    -> (Masked a -> String)
    -> ([Masked a] -> String -> String)
    -> Show (Masked a)
    forall a. Show a => Int -> Masked a -> String -> String
    forall a. Show a => [Masked a] -> String -> String
    forall a. Show a => Masked a -> String
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    showList :: [Masked a] -> String -> String
    $cshowList :: forall a. Show a => [Masked a] -> String -> String
    show :: Masked a -> String
    $cshow :: forall a. Show a => Masked a -> String
    showsPrec :: Int -> Masked a -> String -> String
    $cshowsPrec :: forall a. Show a => Int -> Masked a -> String -> String
    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
    <$ :: forall a b. a -> Masked b -> Masked a
    $c<$ :: forall a b. a -> Masked b -> Masked a
    fmap :: forall a b. (a -> b) -> Masked a -> Masked b
    $cfmap :: forall a b. (a -> b) -> Masked a -> Masked b
    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
    product :: forall a. Num a => Masked a -> a
    $cproduct :: forall a. Num a => Masked a -> a
    sum :: forall a. Num a => Masked a -> a
    $csum :: forall a. Num a => Masked a -> a
    minimum :: forall a. Ord a => Masked a -> a
    $cminimum :: forall a. Ord a => Masked a -> a
    maximum :: forall a. Ord a => Masked a -> a
    $cmaximum :: forall a. Ord a => Masked a -> a
    elem :: forall a. Eq a => a -> Masked a -> Bool
    $celem :: forall a. Eq a => a -> Masked a -> Bool
    length :: forall a. Masked a -> Int
    $clength :: forall a. Masked a -> Int
    null :: forall a. Masked a -> Bool
    $cnull :: forall a. Masked a -> Bool
    toList :: forall a. Masked a -> [a]
    $ctoList :: forall a. Masked a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> Masked a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Masked a -> a
    foldr1 :: forall a. (a -> a -> a) -> Masked a -> a
    $cfoldr1 :: forall a. (a -> a -> a) -> Masked a -> a
    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
    $cfoldl :: forall b a. (b -> a -> 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
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Masked a -> b
    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
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Masked a -> m
    fold :: forall m. Monoid m => Masked m -> m
    $cfold :: forall m. Monoid m => Masked m -> m
    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)
    sequence :: forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
    $csequence :: forall (m :: * -> *) a. Monad m => Masked (m a) -> m (Masked a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Masked a -> m (Masked b)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Masked a -> m (Masked b)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Masked (f a) -> f (Masked a)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Masked (f a) -> f (Masked a)
    traverse :: 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)
    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 a. Bool -> (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
    prettyTCM a
    a

    -- * Call pathes

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

    newtype CallPath = CallPath { CallPath -> [CallInfo]
    callInfos :: [CallInfo] }
      deriving (Int -> CallPath -> String -> String
    [CallPath] -> String -> String
    CallPath -> String
    (Int -> CallPath -> String -> String)
    -> (CallPath -> String)
    -> ([CallPath] -> String -> String)
    -> Show CallPath
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    showList :: [CallPath] -> String -> String
    $cshowList :: [CallPath] -> String -> String
    show :: CallPath -> String
    $cshow :: CallPath -> String
    showsPrec :: Int -> CallPath -> String -> String
    $cshowsPrec :: Int -> CallPath -> String -> String
    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
    stimes :: forall b. Integral b => b -> CallPath -> CallPath
    $cstimes :: forall b. Integral b => b -> CallPath -> CallPath
    sconcat :: NonEmpty CallPath -> CallPath
    $csconcat :: NonEmpty CallPath -> CallPath
    <> :: CallPath -> CallPath -> CallPath
    $c<> :: CallPath -> 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
    mconcat :: [CallPath] -> CallPath
    $cmconcat :: [CallPath] -> CallPath
    mappend :: CallPath -> CallPath -> CallPath
    $cmappend :: CallPath -> CallPath -> CallPath
    mempty :: CallPath
    $cmempty :: CallPath
    Monoid)

    -- | Only show intermediate nodes.  (Drop last 'CallInfo').
    instance Pretty CallPath where
      pretty :: CallPath -> Doc
    pretty (CallPath [CallInfo]
    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
    P.<+> CallInfo -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty CallInfo
    ci) [CallInfo]
    cis) Doc -> Doc -> Doc
    P.<+> Doc
    arrow
        where
          cis :: [CallInfo]
    cis   = [CallInfo] -> [CallInfo]
    forall a. [a] -> [a]
    init [CallInfo]
    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.

    -- TODO: more precise analysis, constructing a tree
    -- of relations between size variables.
    terSetSizeDepth :: Telescope -> TerM a -> TerM a
    terSetSizeDepth :: forall a. Telescope -> TerM a -> TerM a
    terSetSizeDepth Telescope
    tel TerM a
    cont = do
      Int
    n <- TCM Int -> TerM Int
    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 (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 (Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel) ((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
          Type
    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
          TCM Bool -> TCM Int -> TCM Int -> TCM Int
    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) -> TCM 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
    a) (Int -> TCM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    1) {- else -} (TCM Int -> TCM Int) -> TCM Int -> TCM Int
    forall a b. (a -> b) -> a -> b
    $
            case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a of
              MetaV{} -> Int -> TCM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    1
              Term
    _       -> Int -> TCM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    0
      (TerEnv -> TerEnv) -> TerM a -> TerM a
    forall (m :: * -> *) a.
    MonadTer m =>
    (TerEnv -> TerEnv) -> m a -> m a
    terLocal (Lens' Int TerEnv -> LensSet Int TerEnv
    forall i o. Lens' i o -> LensSet i o
    set Lens' Int TerEnv
    terSizeDepth Int
    n) TerM a
    cont