    module Agda.TypeChecking.Monad.Env where

    import qualified Data.List as List

    import Data.Maybe (fromMaybe)

    import Agda.Syntax.Common
    import Agda.Syntax.Abstract.Name

    import Agda.TypeChecking.Monad.Base

    import Agda.Utils.FileName
    import qualified Agda.Utils.SmallSet as SmallSet

    import Agda.Utils.Impossible

    -- | Get the name of the current module, if any.
    {-# SPECIALIZE currentModule :: TCM ModuleName #-}
    {-# SPECIALIZE currentModule :: ReduceM ModuleName #-}
    currentModule :: MonadTCEnv m => m ModuleName
    currentModule :: forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule = (TCEnv -> ModuleName) -> m ModuleName
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> ModuleName
    envCurrentModule

    -- | Set the name of the current module.
    withCurrentModule :: (MonadTCEnv m) => ModuleName -> m a -> m a
    withCurrentModule :: forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
    withCurrentModule ModuleName
    m =
        (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envCurrentModule :: ModuleName
    envCurrentModule = ModuleName
    m }

    -- | Get the path of the currently checked file
    getCurrentPath :: MonadTCEnv m => m AbsolutePath
    getCurrentPath :: forall (m :: * -> *). MonadTCEnv m => m AbsolutePath
    getCurrentPath = AbsolutePath -> Maybe AbsolutePath -> AbsolutePath
    forall a. a -> Maybe a -> a
    fromMaybe AbsolutePath
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe AbsolutePath -> AbsolutePath)
    -> m (Maybe AbsolutePath) -> m AbsolutePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Maybe AbsolutePath) -> m (Maybe AbsolutePath)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe AbsolutePath
    envCurrentPath

    -- | Get the number of variables bound by anonymous modules.
    {-# SPECIALIZE getAnonymousVariables :: ModuleName -> TCM Nat #-}
    {-# SPECIALIZE getAnonymousVariables :: ModuleName -> ReduceM Nat #-}
    getAnonymousVariables :: MonadTCEnv m => ModuleName -> m Nat
    getAnonymousVariables :: forall (m :: * -> *). MonadTCEnv m => ModuleName -> m Nat
    getAnonymousVariables ModuleName
    m = do
      [(ModuleName, Nat)]
    ms <- (TCEnv -> [(ModuleName, Nat)]) -> m [(ModuleName, Nat)]
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> [(ModuleName, Nat)]
    envAnonymousModules
      Nat -> m Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Nat -> m Nat) -> Nat -> m Nat
    forall a b. (a -> b) -> a -> b
    $ [Nat] -> Nat
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum [ Nat
    n | (ModuleName
    m', Nat
    n) <- [(ModuleName, Nat)]
    ms, ModuleName -> [Name]
    mnameToList ModuleName
    m' [Name] -> [Name] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isPrefixOf` ModuleName -> [Name]
    mnameToList ModuleName
    m ]

    -- | Add variables bound by an anonymous module.
    withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a
    withAnonymousModule :: forall a. ModuleName -> Nat -> TCM a -> TCM a
    withAnonymousModule ModuleName
    m Nat
    n =
      (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envAnonymousModules :: [(ModuleName, Nat)]
    envAnonymousModules = (ModuleName
    m, Nat
    n) (ModuleName, Nat) -> [(ModuleName, Nat)] -> [(ModuleName, Nat)]
    forall a. a -> [a] -> [a]
    : TCEnv -> [(ModuleName, Nat)]
    envAnonymousModules TCEnv
    e }

    -- | Set the current environment to the given
    withEnv :: MonadTCEnv m => TCEnv -> m a -> m a
    withEnv :: forall (m :: * -> *) a. MonadTCEnv m => TCEnv -> m a -> m a
    withEnv TCEnv
    env = (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    env0 -> TCEnv
    env
      -- Keep persistent settings
      { envPrintMetasBare :: Bool
    envPrintMetasBare         = TCEnv -> Bool
    envPrintMetasBare TCEnv
    env0
      }

    -- | Get the current environment
    getEnv :: TCM TCEnv
    getEnv :: TCM TCEnv
    getEnv = TCM TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC

    -- | Set highlighting level
    withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a
    withHighlightingLevel :: forall a. HighlightingLevel -> TCM a -> TCM a
    withHighlightingLevel HighlightingLevel
    h = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envHighlightingLevel :: HighlightingLevel
    envHighlightingLevel = HighlightingLevel
    h }

    -- | Restore setting for 'ExpandLast' to default.
    doExpandLast :: TCM a -> TCM a
    doExpandLast :: forall a. TCM a -> TCM a
    doExpandLast = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envExpandLast :: ExpandHidden
    envExpandLast = ExpandHidden -> ExpandHidden
    setExpand (TCEnv -> ExpandHidden
    envExpandLast TCEnv
    e) }
      where
        setExpand :: ExpandHidden -> ExpandHidden
    setExpand ExpandHidden
    ReallyDontExpandLast = ExpandHidden
    ReallyDontExpandLast
        setExpand ExpandHidden
    _                    = ExpandHidden
    ExpandLast

    dontExpandLast :: TCM a -> TCM a
    dontExpandLast :: forall a. TCM a -> TCM a
    dontExpandLast = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envExpandLast :: ExpandHidden
    envExpandLast = ExpandHidden
    DontExpandLast }

    reallyDontExpandLast :: TCM a -> TCM a
    reallyDontExpandLast :: forall a. TCM a -> TCM a
    reallyDontExpandLast = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envExpandLast :: ExpandHidden
    envExpandLast = ExpandHidden
    ReallyDontExpandLast }

    -- | If the reduced did a proper match (constructor or literal pattern),
    --   then record this as simplification step.
    {-# SPECIALIZE performedSimplification :: TCM a -> TCM a #-}
    performedSimplification :: MonadTCEnv m => m a -> m a
    performedSimplification :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    performedSimplification = (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envSimplification :: Simplification
    envSimplification = Simplification
    YesSimplification }

    {-# SPECIALIZE performedSimplification' :: Simplification -> TCM a -> TCM a #-}
    performedSimplification' :: MonadTCEnv m => Simplification -> m a -> m a
    performedSimplification' :: forall (m :: * -> *) a.
    MonadTCEnv m =>
    Simplification -> m a -> m a
    performedSimplification' Simplification
    simpl = (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envSimplification :: Simplification
    envSimplification = Simplification
    simpl Simplification -> Simplification -> Simplification
    forall a. Monoid a => a -> a -> a
    `mappend` TCEnv -> Simplification
    envSimplification TCEnv
    e }

    getSimplification :: MonadTCEnv m => m Simplification
    getSimplification :: forall (m :: * -> *). MonadTCEnv m => m Simplification
    getSimplification = (TCEnv -> Simplification) -> m Simplification
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Simplification
    envSimplification

    -- * Controlling reduction.

    -- | Lens for 'AllowedReductions'.
    updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
    updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
    updateAllowedReductions AllowedReductions -> AllowedReductions
    f TCEnv
    e = TCEnv
    e { envAllowedReductions :: AllowedReductions
    envAllowedReductions = AllowedReductions -> AllowedReductions
    f (TCEnv -> AllowedReductions
    envAllowedReductions TCEnv
    e) }

    modifyAllowedReductions :: MonadTCEnv m => (AllowedReductions -> AllowedReductions) -> m a -> m a
    modifyAllowedReductions :: forall (m :: * -> *) a.
    MonadTCEnv m =>
    (AllowedReductions -> AllowedReductions) -> m a -> m a
    modifyAllowedReductions = (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a)
    -> ((AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv)
    -> (AllowedReductions -> AllowedReductions)
    -> m a
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
    updateAllowedReductions

    putAllowedReductions :: MonadTCEnv m => AllowedReductions -> m a -> m a
    putAllowedReductions :: forall (m :: * -> *) a.
    MonadTCEnv m =>
    AllowedReductions -> m a -> m a
    putAllowedReductions = (AllowedReductions -> AllowedReductions) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (AllowedReductions -> AllowedReductions) -> m a -> m a
    modifyAllowedReductions ((AllowedReductions -> AllowedReductions) -> m a -> m a)
    -> (AllowedReductions -> AllowedReductions -> AllowedReductions)
    -> AllowedReductions
    -> m a
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AllowedReductions -> AllowedReductions -> AllowedReductions
    forall a b. a -> b -> a
    const

    -- | Reduce @Def f vs@ only if @f@ is a projection.
    onlyReduceProjections :: MonadTCEnv m => m a -> m a
    onlyReduceProjections :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceProjections = AllowedReductions -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    AllowedReductions -> m a -> m a
    putAllowedReductions (AllowedReductions -> m a -> m a)
    -> AllowedReductions -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ AllowedReduction -> AllowedReductions
    forall a. SmallSetElement a => a -> SmallSet a
    SmallSet.singleton AllowedReduction
    ProjectionReductions

    -- | Allow all reductions except for non-terminating functions (default).
    allowAllReductions :: MonadTCEnv m => m a -> m a
    allowAllReductions :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    allowAllReductions = AllowedReductions -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    AllowedReductions -> m a -> m a
    putAllowedReductions AllowedReductions
    allReductions

    -- | Allow all reductions including non-terminating functions.
    allowNonTerminatingReductions :: MonadTCEnv m => m a -> m a
    allowNonTerminatingReductions :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    allowNonTerminatingReductions = AllowedReductions -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    AllowedReductions -> m a -> m a
    putAllowedReductions AllowedReductions
    reallyAllReductions

    -- | Allow all reductions when reducing types. Otherwise only allow
    --   inlined functions to be unfolded.
    onlyReduceTypes :: MonadTCEnv m => m a -> m a
    onlyReduceTypes :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes = AllowedReductions -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    AllowedReductions -> m a -> m a
    putAllowedReductions (AllowedReductions -> m a -> m a)
    -> AllowedReductions -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ [AllowedReduction] -> AllowedReductions
    forall a. SmallSetElement a => [a] -> SmallSet a
    SmallSet.fromList [AllowedReduction
    TypeLevelReductions, AllowedReduction
    InlineReductions]

    -- | Update allowed reductions when working on types
    typeLevelReductions :: MonadTCEnv m => m a -> m a
    typeLevelReductions :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    typeLevelReductions = (AllowedReductions -> AllowedReductions) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (AllowedReductions -> AllowedReductions) -> m a -> m a
    modifyAllowedReductions ((AllowedReductions -> AllowedReductions) -> m a -> m a)
    -> (AllowedReductions -> AllowedReductions) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \AllowedReductions
    reds -> if
      | AllowedReduction
    TypeLevelReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    reds ->
          if AllowedReduction
    NonTerminatingReductions AllowedReduction -> AllowedReductions -> Bool
    forall a. SmallSetElement a => a -> SmallSet a -> Bool
    `SmallSet.member` AllowedReductions
    reds
           then AllowedReductions
    reallyAllReductions
           else AllowedReductions
    allReductions
      | Bool
    otherwise -> AllowedReductions
    reds

    -- * Concerning 'envInsideDotPattern'

    insideDotPattern :: TCM a -> TCM a
    insideDotPattern :: forall a. TCM a -> TCM a
    insideDotPattern = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envInsideDotPattern :: Bool
    envInsideDotPattern = Bool
    True }

    isInsideDotPattern :: TCM Bool
    isInsideDotPattern :: TCM Bool
    isInsideDotPattern = (TCEnv -> Bool) -> TCM Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envInsideDotPattern

    -- | Don't use call-by-need evaluation for the given computation.
    callByName :: TCM a -> TCM a
    callByName :: forall a. TCM a -> TCM a
    callByName = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ TCEnv
    e -> TCEnv
    e { envCallByNeed :: Bool
    envCallByNeed = Bool
    False }