module Agda.TypeChecking.Monad.Env where
import Control.Monad.Reader
import Data.List
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 (const env) m
getEnv :: TCM TCEnv
getEnv = ask
leaveTopLevel :: TCM a -> TCM a
leaveTopLevel = local $ \ env -> env { envTopLevel = False }
onTopLevel :: TCM Bool
onTopLevel = asks envTopLevel