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.Syntax.TopLevelModuleName

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 :: 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 a. a -> m a
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 a. Num a => [a] -> a
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 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 :: [(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 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 :: 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 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 :: 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 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 :: 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 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 :: 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 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 :: 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 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 :: 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 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 :: 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 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 -> 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 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 :: 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 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 :: Bool
envCallByNeed = Bool
False }