    {-# OPTIONS_GHC -Wunused-imports #-}

    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 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 a. (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 = m }

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

    -- | 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
      ms <- (TCEnv -> [(ModuleName, Nat)]) -> m [(ModuleName, Nat)]
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> [(ModuleName, Nat)]
    envAnonymousModules
      return $ sum [ n | (m', n) <- ms, mnameToList m' `List.isPrefixOf` mnameToList 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 a. (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 = (m, n) : envAnonymousModules 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 a. (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         = envPrintMetasBare 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 a. (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 = 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 a. (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 = setExpand (envExpandLast 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 a. (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 = DontExpandLast }

    reallyDontExpandLast :: TCM a -> TCM a
    reallyDontExpandLast :: forall a. TCM a -> TCM a
    reallyDontExpandLast = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a. (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 = 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 a. (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 = 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 a. (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 = simpl `mappend` envSimplification 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 = f (envAllowedReductions 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 a. (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 -> 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 -> AllowedReductions -> AllowedReductions
    forall a.
    SmallSetElement a =>
    SmallSet a -> SmallSet a -> SmallSet a
    SmallSet.intersection (AllowedReductions -> AllowedReductions -> AllowedReductions)
    -> AllowedReductions -> AllowedReductions -> AllowedReductions
    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 -> 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 -> AllowedReductions -> AllowedReductions
    forall a.
    SmallSetElement a =>
    SmallSet a -> SmallSet a -> SmallSet a
    SmallSet.intersection (AllowedReductions -> AllowedReductions -> AllowedReductions)
    -> AllowedReductions -> AllowedReductions -> AllowedReductions
    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 a. (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 = 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 a. (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 = False }

    -- | Don't fold let bindings when printing. This is a bit crude since it disables any folding of let
    --   bindings at all. In many cases it's better to use `removeLetBinding` before printing to drop
    --   the let bindings that should not be folded.
    dontFoldLetBindings :: MonadTCEnv m => m a -> m a
    dontFoldLetBindings :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    dontFoldLetBindings = (TCEnv -> TCEnv) -> m a -> m a
    forall a. (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 { envFoldLetBindings = False }