    {-| A constructor argument is forced if it appears as pattern variable
    in an index of the target.

    For instance @x@ is forced in @sing@ and @n@ is forced in @zero@ and @suc@:

    @
      data Sing {a}{A : Set a} : A -> Set where
        sing : (x : A) -> Sing x

      data Fin : Nat -> Set where
        zero : (n : Nat) -> Fin (suc n)
        suc  : (n : Nat) (i : Fin n) -> Fin (suc n)
    @

    At runtime, forced constructor arguments may be erased as they can be
    recovered from dot patterns.  For instance,
    @
      unsing : {A : Set} (x : A) -> Sing x -> A
      unsing .x (sing x) = x
    @
    can become
    @
      unsing x sing = x
    @
    and
    @
      proj : (n : Nat) (i : Fin n) -> Nat
      proj .(suc n) (zero n) = n
      proj .(suc n) (suc n i) = n
    @
    becomes
    @
      proj (suc n) zero    = n
      proj (suc n) (suc i) = n
    @

    This module implements the analysis of which constructor arguments are forced. The process of moving
    the binding site of forced arguments is implemented in the unifier (see the Solution step of
    Agda.TypeChecking.Rules.LHS.Unify.unifyStep).

    Forcing is a concept from pattern matching and thus builds on the
    concept of equality (I) used there (closed terms, extensional) which is
    different from the equality (II) used in conversion checking and the
    constraint solver (open terms, intensional).

    Up to issue 1441 (Feb 2015), the forcing analysis here relied on the
    wrong equality (II), considering type constructors as injective.  This is
    unsound for program extraction, but ok if forcing is only used to decide which
    arguments to skip during conversion checking.

    From now on, forcing uses equality (I) and does not search for forced
    variables under type constructors.  This may lose some savings during
    conversion checking.  If this turns out to be a problem, the old
    forcing could be brought back, using a new modality @Skip@ to indicate
    that this is a relevant argument but still can be skipped during
    conversion checking as it is forced by equality (II).

    -}

    module Agda.TypeChecking.Forcing
      ( computeForcingAnnotations,
        isForced,
        nextIsForced ) where

    import Control.Monad.Reader ( MonadReader, ask, local, ReaderT, runReaderT )
    import Control.Monad.State  ( MonadState, modify, StateT, execStateT )

    import Data.Bifunctor
    import Data.Function ((&))
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import Data.Monoid -- for (<>) in GHC 8.0.2

    import Agda.Interaction.Options

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Datatypes (consOfHIT)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope

    import Agda.Utils.Boolean (implies)
    import Agda.Utils.IArray (Array, listArray)
    import qualified Agda.Utils.IArray as Array
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Utils.Size
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    -- | Given the type of a constructor (excluding the parameters),
    --   decide which arguments are forced.
    computeForcingAnnotations :: QName -> Type -> TCM [IsForced]
    computeForcingAnnotations :: QName -> Type -> TCM [IsForced]
    computeForcingAnnotations QName
    c Type
    t =
      TCMT IO Bool -> TCM [IsForced] -> TCM [IsForced] -> TCM [IsForced]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (PragmaOptions -> Bool
    optForcing (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions {-then-}) ([IsForced] -> TCM [IsForced]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []) (TCM [IsForced] -> TCM [IsForced])
    -> TCM [IsForced] -> TCM [IsForced]
    forall a b. (a -> b) -> a -> b
    $ {-else-} do
        -- Andreas, 2015-03-10  Normalization prevents Issue 1454.
        -- t <- normalise t
        -- Andreas, 2015-03-28  Issue 1469: Normalization too costly.
        -- Instantiation also fixes Issue 1454.
        -- Note that normalization of s0 below does not help.
        -- t <- instantiateFull t
        -- Ulf, 2018-01-28 (#2919): We do need to reduce the target type enough to
        -- get to the actual data type.
        -- Also #2947: The type might reduce to a pi type.
        -- Andreas, 2024-07-07, issue #6744, iteratively reduce.
        TelV tel (El _ a) <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
        erasureOn <- optErasure <$> pragmaOptions
        -- Modalities of constructor arguments:
        let n = Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel
            -- Candidates for forced arguments, indexed by their de Bruijn index.
            -- 'Nothing' means cannot possibly be forced.
            forcedArgCands :: ForcedVariableCandidates
            forcedArgCands = (Nat, Nat) -> [Maybe Modality] -> ForcedVariableCandidates
    forall (a :: * -> * -> *) e i.
    (IArray a e, Ix i) =>
    (i, i) -> [e] -> a i e
    listArray (Nat
    0,Nat
    nNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1)
              [ -- Jesper, 2023-09-20 (#6867): With --erasure, only arguments with @0 can be forced.
                if (Bool
    erasureOn Bool -> Bool -> Bool
    forall a. Boolean a => a -> a -> a
    `implies` Modality -> Bool
    forall a. LensQuantity a => a -> Bool
    hasQuantity0 Modality
    m)
                -- Also the argument shouldn't be irrelevant, since in that
                -- case it isn't really forced.
                Bool -> Bool -> Bool
    && (Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Modality -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Modality
    m)
                then Modality -> Maybe Modality
    forall a. a -> Maybe a
    Just Modality
    m else Maybe Modality
    forall a. Maybe a
    Nothing
              | Modality
    m <- (Dom (ArgName, Type) -> Modality)
    -> [Dom (ArgName, Type)] -> [Modality]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom (ArgName, Type) -> Modality
    forall a. LensModality a => a -> Modality
    getModality ([Dom (ArgName, Type)] -> [Modality])
    -> [Dom (ArgName, Type)] -> [Modality]
    forall a b. (a -> b) -> a -> b
    $ [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a. [a] -> [a]
    reverse ([Dom (ArgName, Type)] -> [Dom (ArgName, Type)])
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel
              ]
        -- Computation of forced arguments:
        let vs = case Term
    a of
              Def QName
    _ Elims
    us -> Elims
    us
              Term
    _        -> Elims
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        forcedVars <-
              -- No candidates, no winners!
          if all isNothing forcedArgCands then pure IntSet.empty
          else runReduceM $ execForcedVariableCollection forcedArgCands $ forcedVariables vs
        let forcedArgs =
              [ if Nat -> IntSet -> Bool
    IntSet.member Nat
    i IntSet
    forcedVars then IsForced
    Forced else IsForced
    NotForced
              | Nat
    i <- Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom Nat
    n
              ]
        reportS "tc.force" 60
          [ "Forcing analysis for " ++ prettyShow c
          , "  forcedVars  = " ++ show (IntSet.toList forcedVars)
          , "  forcedArgs  = " ++ show forcedArgs
          ]
        return forcedArgs

    -- | Candidates for forced constructor arguments (@Just m@) with their modality (@m@)
    --   in the constructor telescope.
    --
    type ForcedVariableCandidates = Array Nat (Maybe Modality)

    -- | Environment for forced variable collection.
    --
    data ForcedVariableContext = ForcedVariableContext
      { ForcedVariableContext -> Modality
    fvcModality   :: Modality
          -- ^ Modality of current position.  (Accumulated from traversed 'Arg's.)
      , ForcedVariableContext -> ForcedVariableCandidates
    fvcCandidates :: ForcedVariableCandidates
          -- ^ Candidates for forced variables.  (Immutable.)
      }

    -- | Which candidates are actually forced?
    --
    type ForcedVariableState = IntSet

    -- | Monad for forced variable analysis.
    --
    newtype ForcedVariableCollection' a = ForcedVariableCollection
      { forall a.
    ForcedVariableCollection' a
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) a
    runForcedVariableCollection :: ReaderT ForcedVariableContext (StateT ForcedVariableState ReduceM) a }
      deriving
        ( (forall a b.
     (a -> b)
     -> ForcedVariableCollection' a -> ForcedVariableCollection' b)
    -> (forall a b.
        a -> ForcedVariableCollection' b -> ForcedVariableCollection' a)
    -> Functor ForcedVariableCollection'
    forall a b.
    a -> ForcedVariableCollection' b -> ForcedVariableCollection' a
    forall a b.
    (a -> b)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' 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)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' b
    fmap :: forall a b.
    (a -> b)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' b
    $c<$ :: forall a b.
    a -> ForcedVariableCollection' b -> ForcedVariableCollection' a
    <$ :: forall a b.
    a -> ForcedVariableCollection' b -> ForcedVariableCollection' a
    Functor, Functor ForcedVariableCollection'
    Functor ForcedVariableCollection' =>
    (forall a. a -> ForcedVariableCollection' a)
    -> (forall a b.
        ForcedVariableCollection' (a -> b)
        -> ForcedVariableCollection' a -> ForcedVariableCollection' b)
    -> (forall a b c.
        (a -> b -> c)
        -> ForcedVariableCollection' a
        -> ForcedVariableCollection' b
        -> ForcedVariableCollection' c)
    -> (forall a b.
        ForcedVariableCollection' a
        -> ForcedVariableCollection' b -> ForcedVariableCollection' b)
    -> (forall a b.
        ForcedVariableCollection' a
        -> ForcedVariableCollection' b -> ForcedVariableCollection' a)
    -> Applicative ForcedVariableCollection'
    forall a. a -> ForcedVariableCollection' a
    forall a b.
    ForcedVariableCollection' a
    -> ForcedVariableCollection' b -> ForcedVariableCollection' a
    forall a b.
    ForcedVariableCollection' a
    -> ForcedVariableCollection' b -> ForcedVariableCollection' b
    forall a b.
    ForcedVariableCollection' (a -> b)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' b
    forall a b c.
    (a -> b -> c)
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' b
    -> ForcedVariableCollection' 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 -> ForcedVariableCollection' a
    pure :: forall a. a -> ForcedVariableCollection' a
    $c<*> :: forall a b.
    ForcedVariableCollection' (a -> b)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' b
    <*> :: forall a b.
    ForcedVariableCollection' (a -> b)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' b
    $cliftA2 :: forall a b c.
    (a -> b -> c)
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' b
    -> ForcedVariableCollection' c
    liftA2 :: forall a b c.
    (a -> b -> c)
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' b
    -> ForcedVariableCollection' c
    $c*> :: forall a b.
    ForcedVariableCollection' a
    -> ForcedVariableCollection' b -> ForcedVariableCollection' b
    *> :: forall a b.
    ForcedVariableCollection' a
    -> ForcedVariableCollection' b -> ForcedVariableCollection' b
    $c<* :: forall a b.
    ForcedVariableCollection' a
    -> ForcedVariableCollection' b -> ForcedVariableCollection' a
    <* :: forall a b.
    ForcedVariableCollection' a
    -> ForcedVariableCollection' b -> ForcedVariableCollection' a
    Applicative, Applicative ForcedVariableCollection'
    Applicative ForcedVariableCollection' =>
    (forall a b.
     ForcedVariableCollection' a
     -> (a -> ForcedVariableCollection' b)
     -> ForcedVariableCollection' b)
    -> (forall a b.
        ForcedVariableCollection' a
        -> ForcedVariableCollection' b -> ForcedVariableCollection' b)
    -> (forall a. a -> ForcedVariableCollection' a)
    -> Monad ForcedVariableCollection'
    forall a. a -> ForcedVariableCollection' a
    forall a b.
    ForcedVariableCollection' a
    -> ForcedVariableCollection' b -> ForcedVariableCollection' b
    forall a b.
    ForcedVariableCollection' a
    -> (a -> ForcedVariableCollection' b)
    -> ForcedVariableCollection' 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.
    ForcedVariableCollection' a
    -> (a -> ForcedVariableCollection' b)
    -> ForcedVariableCollection' b
    >>= :: forall a b.
    ForcedVariableCollection' a
    -> (a -> ForcedVariableCollection' b)
    -> ForcedVariableCollection' b
    $c>> :: forall a b.
    ForcedVariableCollection' a
    -> ForcedVariableCollection' b -> ForcedVariableCollection' b
    >> :: forall a b.
    ForcedVariableCollection' a
    -> ForcedVariableCollection' b -> ForcedVariableCollection' b
    $creturn :: forall a. a -> ForcedVariableCollection' a
    return :: forall a. a -> ForcedVariableCollection' a
    Monad
        , MonadReader ForcedVariableContext, MonadState ForcedVariableState
        -- Needed for HasConstInfo:
        , Monad ForcedVariableCollection'
    Functor ForcedVariableCollection'
    Applicative ForcedVariableCollection'
    ForcedVariableCollection' Bool
    ForcedVariableCollection' Verbosity
    ForcedVariableCollection' ProfileOptions
    (Functor ForcedVariableCollection',
     Applicative ForcedVariableCollection',
     Monad ForcedVariableCollection') =>
    (ArgName -> Nat -> TCM Doc -> ForcedVariableCollection' ArgName)
    -> (forall a.
        ArgName
        -> Nat
        -> ArgName
        -> ForcedVariableCollection' a
        -> ForcedVariableCollection' a)
    -> (forall a.
        ArgName
        -> Nat
        -> ArgName
        -> ForcedVariableCollection' a
        -> ForcedVariableCollection' a)
    -> ForcedVariableCollection' Verbosity
    -> ForcedVariableCollection' ProfileOptions
    -> ForcedVariableCollection' Bool
    -> (forall a.
        ForcedVariableCollection' a -> ForcedVariableCollection' a)
    -> MonadDebug ForcedVariableCollection'
    ArgName -> Nat -> TCM Doc -> ForcedVariableCollection' ArgName
    forall a.
    ArgName
    -> Nat
    -> ArgName
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' a
    forall a.
    ForcedVariableCollection' a -> ForcedVariableCollection' a
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    (ArgName -> Nat -> TCM Doc -> m ArgName)
    -> (forall a. ArgName -> Nat -> ArgName -> m a -> m a)
    -> (forall a. ArgName -> Nat -> ArgName -> m a -> m a)
    -> m Verbosity
    -> m ProfileOptions
    -> m Bool
    -> (forall a. m a -> m a)
    -> MonadDebug m
    $cformatDebugMessage :: ArgName -> Nat -> TCM Doc -> ForcedVariableCollection' ArgName
    formatDebugMessage :: ArgName -> Nat -> TCM Doc -> ForcedVariableCollection' ArgName
    $ctraceDebugMessage :: forall a.
    ArgName
    -> Nat
    -> ArgName
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' a
    traceDebugMessage :: forall a.
    ArgName
    -> Nat
    -> ArgName
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' a
    $cverboseBracket :: forall a.
    ArgName
    -> Nat
    -> ArgName
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' a
    verboseBracket :: forall a.
    ArgName
    -> Nat
    -> ArgName
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' a
    $cgetVerbosity :: ForcedVariableCollection' Verbosity
    getVerbosity :: ForcedVariableCollection' Verbosity
    $cgetProfileOptions :: ForcedVariableCollection' ProfileOptions
    getProfileOptions :: ForcedVariableCollection' ProfileOptions
    $cisDebugPrinting :: ForcedVariableCollection' Bool
    isDebugPrinting :: ForcedVariableCollection' Bool
    $cnowDebugPrinting :: forall a.
    ForcedVariableCollection' a -> ForcedVariableCollection' a
    nowDebugPrinting :: forall a.
    ForcedVariableCollection' a -> ForcedVariableCollection' a
    MonadDebug, Monad ForcedVariableCollection'
    ForcedVariableCollection' TCEnv
    Monad ForcedVariableCollection' =>
    ForcedVariableCollection' TCEnv
    -> (forall a.
        (TCEnv -> TCEnv)
        -> ForcedVariableCollection' a -> ForcedVariableCollection' a)
    -> MonadTCEnv ForcedVariableCollection'
    forall a.
    (TCEnv -> TCEnv)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' a
    forall (m :: * -> *).
    Monad m =>
    m TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
    $caskTC :: ForcedVariableCollection' TCEnv
    askTC :: ForcedVariableCollection' TCEnv
    $clocalTC :: forall a.
    (TCEnv -> TCEnv)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' a
    localTC :: forall a.
    (TCEnv -> TCEnv)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' a
    MonadTCEnv, Monad ForcedVariableCollection'
    Functor ForcedVariableCollection'
    Applicative ForcedVariableCollection'
    ForcedVariableCollection' PragmaOptions
    ForcedVariableCollection' CommandLineOptions
    (Functor ForcedVariableCollection',
     Applicative ForcedVariableCollection',
     Monad ForcedVariableCollection') =>
    ForcedVariableCollection' PragmaOptions
    -> ForcedVariableCollection' CommandLineOptions
    -> HasOptions ForcedVariableCollection'
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    m PragmaOptions -> m CommandLineOptions -> HasOptions m
    $cpragmaOptions :: ForcedVariableCollection' PragmaOptions
    pragmaOptions :: ForcedVariableCollection' PragmaOptions
    $ccommandLineOptions :: ForcedVariableCollection' CommandLineOptions
    commandLineOptions :: ForcedVariableCollection' CommandLineOptions
    HasOptions
        , Functor ForcedVariableCollection'
    Applicative ForcedVariableCollection'
    HasOptions ForcedVariableCollection'
    MonadTCEnv ForcedVariableCollection'
    MonadDebug ForcedVariableCollection'
    (Functor ForcedVariableCollection',
     Applicative ForcedVariableCollection',
     HasOptions ForcedVariableCollection',
     MonadDebug ForcedVariableCollection',
     MonadTCEnv ForcedVariableCollection') =>
    (QName -> ForcedVariableCollection' Definition)
    -> (QName
        -> ForcedVariableCollection' (Either SigError Definition))
    -> (QName -> ForcedVariableCollection' RewriteRules)
    -> HasConstInfo ForcedVariableCollection'
    QName -> ForcedVariableCollection' RewriteRules
    QName -> ForcedVariableCollection' (Either SigError Definition)
    QName -> ForcedVariableCollection' 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 -> ForcedVariableCollection' Definition
    getConstInfo :: QName -> ForcedVariableCollection' Definition
    $cgetConstInfo' :: QName -> ForcedVariableCollection' (Either SigError Definition)
    getConstInfo' :: QName -> ForcedVariableCollection' (Either SigError Definition)
    $cgetRewriteRulesFor :: QName -> ForcedVariableCollection' RewriteRules
    getRewriteRulesFor :: QName -> ForcedVariableCollection' RewriteRules
    HasConstInfo
        -- Neded for MonadReduce:
        , Monad ForcedVariableCollection'
    ForcedVariableCollection' TCState
    Monad ForcedVariableCollection' =>
    ForcedVariableCollection' TCState
    -> (forall a b.
        Lens' TCState a
        -> (a -> a)
        -> ForcedVariableCollection' b
        -> ForcedVariableCollection' b)
    -> (forall a.
        (TCState -> TCState)
        -> ForcedVariableCollection' a -> ForcedVariableCollection' a)
    -> ReadTCState ForcedVariableCollection'
    forall a.
    (TCState -> TCState)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' a
    forall a b.
    Lens' TCState a
    -> (a -> a)
    -> ForcedVariableCollection' b
    -> ForcedVariableCollection' 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 :: ForcedVariableCollection' TCState
    getTCState :: ForcedVariableCollection' TCState
    $clocallyTCState :: forall a b.
    Lens' TCState a
    -> (a -> a)
    -> ForcedVariableCollection' b
    -> ForcedVariableCollection' b
    locallyTCState :: forall a b.
    Lens' TCState a
    -> (a -> a)
    -> ForcedVariableCollection' b
    -> ForcedVariableCollection' b
    $cwithTCState :: forall a.
    (TCState -> TCState)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' a
    withTCState :: forall a.
    (TCState -> TCState)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' a
    ReadTCState
        , Applicative ForcedVariableCollection'
    HasOptions ForcedVariableCollection'
    MonadTCEnv ForcedVariableCollection'
    ReadTCState ForcedVariableCollection'
    (Applicative ForcedVariableCollection',
     MonadTCEnv ForcedVariableCollection',
     ReadTCState ForcedVariableCollection',
     HasOptions ForcedVariableCollection') =>
    (forall a. ReduceM a -> ForcedVariableCollection' a)
    -> MonadReduce ForcedVariableCollection'
    forall a. ReduceM a -> ForcedVariableCollection' a
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) =>
    (forall a. ReduceM a -> m a) -> MonadReduce m
    $cliftReduce :: forall a. ReduceM a -> ForcedVariableCollection' a
    liftReduce :: forall a. ReduceM a -> ForcedVariableCollection' a
    MonadReduce
        )

    type ForcedVariableCollection = ForcedVariableCollection' ()

    instance Semigroup ForcedVariableCollection where
      ForcedVariableCollection ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    m <> :: ForcedVariableCollection
    -> ForcedVariableCollection -> ForcedVariableCollection
    <> ForcedVariableCollection ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    m' = ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    -> ForcedVariableCollection
    forall a.
    ReaderT ForcedVariableContext (StateT IntSet ReduceM) a
    -> ForcedVariableCollection' a
    ForcedVariableCollection (ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    m ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    forall a b.
    ReaderT ForcedVariableContext (StateT IntSet ReduceM) a
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) b
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    m')

    instance Monoid ForcedVariableCollection where
      mempty :: ForcedVariableCollection
    mempty = ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    -> ForcedVariableCollection
    forall a.
    ReaderT ForcedVariableContext (StateT IntSet ReduceM) a
    -> ForcedVariableCollection' a
    ForcedVariableCollection (ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
     -> ForcedVariableCollection)
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    -> ForcedVariableCollection
    forall a b. (a -> b) -> a -> b
    $ () -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    forall a.
    a -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

    instance Singleton (Nat, Modality) ForcedVariableCollection where
      singleton :: (Nat, Modality) -> ForcedVariableCollection
    singleton (Nat
    i, Modality
    m) = ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    -> ForcedVariableCollection
    forall a.
    ReaderT ForcedVariableContext (StateT IntSet ReduceM) a
    -> ForcedVariableCollection' a
    ForcedVariableCollection do
        ForcedVariableContext mc cands <- ReaderT
      ForcedVariableContext (StateT IntSet ReduceM) ForcedVariableContext
    forall r (m :: * -> *). MonadReader r m => m r
    ask
        whenJust (join $ cands Array.!? i) \ Modality
    m0 -> do
          -- #2819: We can only mark an argument as forced if it appears in the
          -- type with a relevance below (i.e. more relevant) than the one of the
          -- constructor argument. Otherwise we can't actually get the value from
          -- the type.
          Bool
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (Modality -> Modality -> Modality
    composeModality Modality
    mc Modality
    m Modality -> Modality -> Bool
    `moreUsableModality` Modality
    m0) do
            (IntSet -> IntSet)
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((IntSet -> IntSet)
     -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ())
    -> (IntSet -> IntSet)
    -> ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    forall a b. (a -> b) -> a -> b
    $ Nat -> IntSet -> IntSet
    IntSet.insert Nat
    i

    -- | Step into an argument labelled with the given modality.
    --
    underModality :: Modality -> ForcedVariableCollection -> ForcedVariableCollection
    underModality :: Modality -> ForcedVariableCollection -> ForcedVariableCollection
    underModality Modality
    m = (ForcedVariableContext -> ForcedVariableContext)
    -> ForcedVariableCollection -> ForcedVariableCollection
    forall a.
    (ForcedVariableContext -> ForcedVariableContext)
    -> ForcedVariableCollection' a -> ForcedVariableCollection' a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local \ (ForcedVariableContext Modality
    mc ForcedVariableCandidates
    cands) -> Modality -> ForcedVariableCandidates -> ForcedVariableContext
    ForcedVariableContext (Modality -> Modality -> Modality
    composeModality Modality
    mc Modality
    m) ForcedVariableCandidates
    cands

    -- | Run the forced variable analysis monad.
    execForcedVariableCollection :: ForcedVariableCandidates -> ForcedVariableCollection -> ReduceM ForcedVariableState
    execForcedVariableCollection :: ForcedVariableCandidates
    -> ForcedVariableCollection -> ReduceM IntSet
    execForcedVariableCollection ForcedVariableCandidates
    cands (ForcedVariableCollection ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    m) =
      ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    m ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    -> (ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
        -> StateT IntSet ReduceM ())
    -> StateT IntSet ReduceM ()
    forall a b. a -> (a -> b) -> b
    & (ReaderT ForcedVariableContext (StateT IntSet ReduceM) ()
    -> ForcedVariableContext -> StateT IntSet ReduceM ()
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` ForcedVariableContext
    cxt)
        StateT IntSet ReduceM ()
    -> (StateT IntSet ReduceM () -> ReduceM IntSet) -> ReduceM IntSet
    forall a b. a -> (a -> b) -> b
    & (StateT IntSet ReduceM () -> IntSet -> ReduceM IntSet
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
    `execStateT` IntSet
    IntSet.empty)
      where cxt :: ForcedVariableContext
    cxt = Modality -> ForcedVariableCandidates -> ForcedVariableContext
    ForcedVariableContext Modality
    unitModality ForcedVariableCandidates
    cands

    -- | Compute the pattern variables of a term or term-like thing.
    class ForcedVariables a where
      forcedVariables :: a -> ForcedVariableCollection

      default forcedVariables ::
        (ForcedVariables b, Foldable t, a ~ t b) =>
        a -> ForcedVariableCollection
      forcedVariables = (b -> ForcedVariableCollection) -> t b -> ForcedVariableCollection
    forall m a. Monoid m => (a -> m) -> t a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap b -> ForcedVariableCollection
    forall a. ForcedVariables a => a -> ForcedVariableCollection
    forcedVariables

    instance ForcedVariables a => ForcedVariables [a] where

    -- Note that the 'a' does not include the 'Arg' in 'Apply'.
    instance ForcedVariables a => ForcedVariables (Elim' a) where
      forcedVariables :: Elim' a -> ForcedVariableCollection
    forcedVariables (Apply Arg a
    x) = Arg a -> ForcedVariableCollection
    forall a. ForcedVariables a => a -> ForcedVariableCollection
    forcedVariables Arg a
    x
      forcedVariables IApply{}  = ForcedVariableCollection
    forall a. Monoid a => a
    mempty  -- No forced variables in path applications
      forcedVariables Proj{}    = ForcedVariableCollection
    forall a. Monoid a => a
    mempty

    instance ForcedVariables a => ForcedVariables (Arg a) where
      forcedVariables :: Arg a -> ForcedVariableCollection
    forcedVariables Arg a
    x =
        Modality -> ForcedVariableCollection -> ForcedVariableCollection
    underModality Modality
    m (ForcedVariableCollection -> ForcedVariableCollection)
    -> ForcedVariableCollection -> ForcedVariableCollection
    forall a b. (a -> b) -> a -> b
    $ a -> ForcedVariableCollection
    forall a. ForcedVariables a => a -> ForcedVariableCollection
    forcedVariables (a -> ForcedVariableCollection) -> a -> ForcedVariableCollection
    forall a b. (a -> b) -> a -> b
    $ Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    x
        where m :: Modality
    m = Arg a -> Modality
    forall a. LensModality a => a -> Modality
    getModality Arg a
    x

    -- | Assumes that the term is in normal form.
    instance ForcedVariables Term where
      -- Andreas, 2024-07-07, issue #6744, add reduction.
      forcedVariables :: Term -> ForcedVariableCollection
    forcedVariables Term
    v = Term -> ForcedVariableCollection' Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v ForcedVariableCollection' Term
    -> (Term -> ForcedVariableCollection) -> ForcedVariableCollection
    forall a b.
    ForcedVariableCollection' a
    -> (a -> ForcedVariableCollection' b)
    -> ForcedVariableCollection' b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Var Nat
    i []   -> (Nat, Modality) -> ForcedVariableCollection
    forall el coll. Singleton el coll => el -> coll
    singleton (Nat
    i, Modality
    unitModality)
        Con ConHead
    c ConInfo
    _ Elims
    vs -> ForcedVariableCollection' Bool
    -> ForcedVariableCollection
    -> ForcedVariableCollection
    -> ForcedVariableCollection
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> ForcedVariableCollection' Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    consOfHIT (QName -> ForcedVariableCollection' Bool)
    -> QName -> ForcedVariableCollection' Bool
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c) ForcedVariableCollection
    forall a. Monoid a => a
    mempty (ForcedVariableCollection -> ForcedVariableCollection)
    -> ForcedVariableCollection -> ForcedVariableCollection
    forall a b. (a -> b) -> a -> b
    $ {-else-} Elims -> ForcedVariableCollection
    forall a. ForcedVariables a => a -> ForcedVariableCollection
    forcedVariables Elims
    vs
        Term
    _          -> ForcedVariableCollection
    forall a. Monoid a => a
    mempty

    isForced :: IsForced -> Bool
    isForced :: IsForced -> Bool
    isForced IsForced
    Forced    = Bool
    True
    isForced IsForced
    NotForced = Bool
    False

    nextIsForced :: [IsForced] -> (IsForced, [IsForced])
    nextIsForced :: [IsForced] -> (IsForced, [IsForced])
    nextIsForced []     = (IsForced
    NotForced, [])
    nextIsForced (IsForced
    f:[IsForced]
    fs) = (IsForced
    f, [IsForced]
    fs)