{-| 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 : Type a} : A -> Type where
    sing : (x : A) -> Sing x

  data Fin : Nat -> Type 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 : Type} (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 Mikan.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 Data.IntSet qualified as IntSet
import Data.Monoid -- for (<>) in GHC 8.0.2

import Mikan.Interaction.Options

import Mikan.Syntax.Common
import Mikan.Syntax.Internal

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

import Mikan.Utils.Boolean (implies)
import Mikan.Utils.List
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Syntax.Common.Pretty (prettyShow)
import Mikan.Utils.Size
import Mikan.Utils.Singleton

import Mikan.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
    let n = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size 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 n == 0 then pure IntSet.empty
      else runReduceM $ execForcedVariableCollection $ forcedVariables vs
    let forcedArgs =
          [ if Int -> IntSet -> Bool
IntSet.member Int
i IntSet
forcedVars then IsForced
Forced else IsForced
NotForced
          | Int
i <- Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n
          ]
    reportS "tc.force" 60
      [ "Forcing analysis for " ++ prettyShow c
      , "  forcedVars  = " ++ show (IntSet.toList forcedVars)
      , "  forcedArgs  = " ++ show forcedArgs
      ]
    return forcedArgs

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

-- | Monad for forced variable analysis.
--
newtype ForcedVariableCollection' a = ForcedVariableCollection
  { forall a. ForcedVariableCollection' a -> StateT IntSet ReduceM a
runForcedVariableCollection :: 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
    , MonadState ForcedVariableState
    -- Needed for HasConstInfo:
    , Monad ForcedVariableCollection'
Functor ForcedVariableCollection'
Applicative ForcedVariableCollection'
ForcedVariableCollection' Bool
ForcedVariableCollection' Verbosity
ForcedVariableCollection' ProfileOptions
(Functor ForcedVariableCollection',
 Applicative ForcedVariableCollection',
 Monad ForcedVariableCollection') =>
([Char] -> Int -> TCM Doc -> ForcedVariableCollection' Doc)
-> (forall a.
    [Char]
    -> Int
    -> Doc
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' a)
-> (forall a.
    [Char]
    -> Int
    -> [Char]
    -> ForcedVariableCollection' a
    -> ForcedVariableCollection' a)
-> ForcedVariableCollection' Verbosity
-> ForcedVariableCollection' ProfileOptions
-> ForcedVariableCollection' Bool
-> (forall a.
    ForcedVariableCollection' a -> ForcedVariableCollection' a)
-> MonadDebug ForcedVariableCollection'
[Char] -> Int -> TCM Doc -> ForcedVariableCollection' Doc
forall a.
[Char]
-> Int
-> [Char]
-> ForcedVariableCollection' a
-> ForcedVariableCollection' a
forall a.
[Char]
-> Int
-> Doc
-> ForcedVariableCollection' a
-> ForcedVariableCollection' a
forall a.
ForcedVariableCollection' a -> ForcedVariableCollection' a
forall (m :: * -> *).
(Functor m, Applicative m, Monad m) =>
([Char] -> Int -> TCM Doc -> m Doc)
-> (forall a. [Char] -> Int -> Doc -> m a -> m a)
-> (forall a. [Char] -> Int -> [Char] -> m a -> m a)
-> m Verbosity
-> m ProfileOptions
-> m Bool
-> (forall a. m a -> m a)
-> MonadDebug m
$cformatDebugMessage :: [Char] -> Int -> TCM Doc -> ForcedVariableCollection' Doc
formatDebugMessage :: [Char] -> Int -> TCM Doc -> ForcedVariableCollection' Doc
$ctraceDebugMessage :: forall a.
[Char]
-> Int
-> Doc
-> ForcedVariableCollection' a
-> ForcedVariableCollection' a
traceDebugMessage :: forall a.
[Char]
-> Int
-> Doc
-> ForcedVariableCollection' a
-> ForcedVariableCollection' a
$cverboseBracket :: forall a.
[Char]
-> Int
-> [Char]
-> ForcedVariableCollection' a
-> ForcedVariableCollection' a
verboseBracket :: forall a.
[Char]
-> Int
-> [Char]
-> 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' CommandLineOptions
ForcedVariableCollection' PragmaOptions
(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'
MonadDebug ForcedVariableCollection'
MonadTCEnv ForcedVariableCollection'
(Functor ForcedVariableCollection',
 Applicative ForcedVariableCollection',
 HasOptions ForcedVariableCollection',
 MonadDebug ForcedVariableCollection',
 MonadTCEnv ForcedVariableCollection') =>
(HasCallStack => QName -> ForcedVariableCollection' Definition)
-> (HasCallStack =>
    QName -> ForcedVariableCollection' (Either SigError Definition))
-> HasConstInfo ForcedVariableCollection'
HasCallStack =>
QName -> ForcedVariableCollection' (Either SigError Definition)
HasCallStack => QName -> ForcedVariableCollection' Definition
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadDebug m,
 MonadTCEnv m) =>
(HasCallStack => QName -> m Definition)
-> (HasCallStack => QName -> m (Either SigError Definition))
-> HasConstInfo m
$cgetConstInfo :: HasCallStack => QName -> ForcedVariableCollection' Definition
getConstInfo :: HasCallStack => QName -> ForcedVariableCollection' Definition
$cgetConstInfo' :: HasCallStack =>
QName -> ForcedVariableCollection' (Either SigError Definition)
getConstInfo' :: HasCallStack =>
QName -> ForcedVariableCollection' (Either SigError Definition)
HasConstInfo
    -- Neded for MonadReduce:
    , Monad ForcedVariableCollection'
ForcedVariableCollection' SessionState
ForcedVariableCollection' TCState
Monad ForcedVariableCollection' =>
ForcedVariableCollection' TCState
-> (forall a b.
    Lens' TCState a
    -> (a -> a)
    -> ForcedVariableCollection' b
    -> ForcedVariableCollection' b)
-> ForcedVariableCollection' SessionState
-> (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)
-> m SessionState
-> (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
$cgetSessionState :: ForcedVariableCollection' SessionState
getSessionState :: ForcedVariableCollection' SessionState
$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 StateT IntSet ReduceM ()
m <> :: ForcedVariableCollection
-> ForcedVariableCollection -> ForcedVariableCollection
<> ForcedVariableCollection StateT IntSet ReduceM ()
m' = StateT IntSet ReduceM () -> ForcedVariableCollection
forall a. StateT IntSet ReduceM a -> ForcedVariableCollection' a
ForcedVariableCollection (StateT IntSet ReduceM ()
m StateT IntSet ReduceM ()
-> StateT IntSet ReduceM () -> StateT IntSet ReduceM ()
forall a b.
StateT IntSet ReduceM a
-> StateT IntSet ReduceM b -> StateT IntSet ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT IntSet ReduceM ()
m')

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

instance Singleton Nat ForcedVariableCollection where
  singleton :: Int -> ForcedVariableCollection
singleton Int
i = StateT IntSet ReduceM () -> ForcedVariableCollection
forall a. StateT IntSet ReduceM a -> ForcedVariableCollection' a
ForcedVariableCollection do
    (IntSet -> IntSet) -> StateT IntSet ReduceM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((IntSet -> IntSet) -> StateT IntSet ReduceM ())
-> (IntSet -> IntSet) -> StateT IntSet ReduceM ()
forall a b. (a -> b) -> a -> b
$ Int -> IntSet -> IntSet
IntSet.insert Int
i

-- | Run the forced variable analysis monad.
execForcedVariableCollection :: ForcedVariableCollection -> ReduceM ForcedVariableState
execForcedVariableCollection :: ForcedVariableCollection -> ReduceM IntSet
execForcedVariableCollection (ForcedVariableCollection StateT IntSet ReduceM ()
m) =
  StateT IntSet ReduceM ()
m 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)

-- | 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 = a -> ForcedVariableCollection
forall a. ForcedVariables a => a -> ForcedVariableCollection
forcedVariables (Arg a -> a
forall e. Arg e -> e
unArg 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 Int
i []   -> Int -> ForcedVariableCollection
forall el coll. Singleton el coll => el -> coll
singleton Int
i
    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 :: * -> *).
(HasCallStack, 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)