module Agda.TypeChecking.Monad.Env where
import Control.Monad.Reader
import Data.List
import Data.Monoid
import Agda.Syntax.Common
import Agda.Syntax.Abstract.Name
import Agda.TypeChecking.Monad.Base
currentModule :: TCM ModuleName
currentModule = asks envCurrentModule
withCurrentModule :: ModuleName -> TCM a -> TCM a
withCurrentModule m =
local $ \e -> e { envCurrentModule = m }
getAnonymousVariables :: ModuleName -> TCM Nat
getAnonymousVariables m = do
ms <- asks envAnonymousModules
return $ sum [ n | (m', n) <- ms, mnameToList m' `isPrefixOf` mnameToList m ]
withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a
withAnonymousModule m n =
local $ \e -> e { envAnonymousModules = (m, n) : envAnonymousModules e
}
withEnv :: TCEnv -> TCM a -> TCM a
withEnv env m = local (\env0 -> env { envAllowDestructiveUpdate = envAllowDestructiveUpdate env0 }) m
getEnv :: TCM TCEnv
getEnv = ask
withIncreasedModuleNestingLevel :: TCM a -> TCM a
withIncreasedModuleNestingLevel =
local (\e -> e { envModuleNestingLevel =
envModuleNestingLevel e + 1 })
withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a
withHighlightingLevel h = local $ \e -> e { envHighlightingLevel = h }
doExpandLast :: TCM a -> TCM a
doExpandLast = local $ \ e -> e { envExpandLast = ExpandLast }
dontExpandLast :: TCM a -> TCM a
dontExpandLast = local $ \ e -> e { envExpandLast = DontExpandLast }
performedSimplification :: MonadReader TCEnv m => m a -> m a
performedSimplification = local $ \ e -> e { envSimplification = YesSimplification }
performedSimplification' :: MonadReader TCEnv m => Simplification -> m a -> m a
performedSimplification' simpl = local $ \ e -> e { envSimplification = simpl `mappend` envSimplification e }
getSimplification :: MonadReader TCEnv m => m Simplification
getSimplification = asks envSimplification
onlyReduceProjections :: TCM a -> TCM a
onlyReduceProjections = local $ \ e -> e { envAllowedReductions = [ProjectionReductions] }
dontReduceProjections :: TCM a -> TCM a
dontReduceProjections = local $ \ e -> e { envAllowedReductions = allReductions \\ [ProjectionReductions] }
dontReduceLevels :: TCM a -> TCM a
dontReduceLevels = local $ \ e -> e { envAllowedReductions = allReductions \\ [LevelReductions] }
allowAllReductions :: TCM a -> TCM a
allowAllReductions = local $ \ e -> e { envAllowedReductions = allReductions }
allowNonTerminatingReductions :: TCM a -> TCM a
allowNonTerminatingReductions = local $ \ e -> e { envAllowedReductions = allReductions ++ [NonTerminatingReductions] }
insideDotPattern :: TCM a -> TCM a
insideDotPattern = local $ \e -> e { envInsideDotPattern = True }
isInsideDotPattern :: TCM Bool
isInsideDotPattern = asks envInsideDotPattern
isReifyingUnquoted :: TCM Bool
isReifyingUnquoted = asks envReifyUnquoted
nowReifyingUnquoted :: TCM a -> TCM a
nowReifyingUnquoted = local $ \e -> e { envReifyUnquoted = True }