{-# 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 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 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 => 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
  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 }