Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Context

Contents

Synopsis

Modifying the context

modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm a #

Modify a Context in a computation.

inTopContext :: MonadTCM tcm => tcm a -> tcm a #

Change to top (=empty) context.

TODO: currently, this makes the ModuleParamDict ill-formed!

escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a #

Delete the last n bindings from the context.

TODO: currently, this makes the ModuleParamDict ill-formed!

Manipulating module parameters --

withModuleParameters :: ModuleParamDict -> TCM a -> TCM a #

Locally set module parameters for a computation.

updateModuleParameters :: MonadTCM tcm => Substitution -> tcm a -> tcm a #

Apply a substitution to all module parameters.

weakenModuleParameters :: MonadTCM tcm => Nat -> tcm a -> tcm a #

Since the ModuleParamDict is relative to the current context, this function should be called everytime the context is extended.

getModuleParameterSub :: MonadTCM tcm => ModuleName -> tcm Substitution #

Get substitution Γ ⊢ ρ : Γm where Γ is the current context and Γm is the module parameter telescope of module m.

In case the current ModuleParamDict does not know m, we return the identity substitution. This is ok for instance if we are outside module m (in which case we have to supply all module parameters to any symbol defined within m we want to refer).

Adding to the context

addCtx :: MonadTCM tcm => Name -> Dom Type -> tcm a -> tcm a #

addCtx x arg cont add a variable to the context.

Chooses an unused Name.

Warning: Does not update module parameter substitution!

unshadowName :: MonadTCM tcm => Name -> tcm Name #

Pick a concrete name that doesn't shadow anything in the context.

class AddContext b where #

Various specializations of addCtx.

Minimal complete definition

addContext, contextSize

Methods

addContext :: MonadTCM tcm => b -> tcm a -> tcm a #

contextSize :: b -> Nat #

Instances

AddContext String # 

Methods

addContext :: MonadTCM tcm => String -> tcm a -> tcm a #

contextSize :: String -> Nat #

AddContext Name # 

Methods

addContext :: MonadTCM tcm => Name -> tcm a -> tcm a #

contextSize :: Name -> Nat #

AddContext Telescope # 

Methods

addContext :: MonadTCM tcm => Telescope -> tcm a -> tcm a #

contextSize :: Telescope -> Nat #

AddContext a => AddContext [a] # 

Methods

addContext :: MonadTCM tcm => [a] -> tcm a -> tcm a #

contextSize :: [a] -> Nat #

AddContext (Dom (String, Type)) # 

Methods

addContext :: MonadTCM tcm => Dom (String, Type) -> tcm a -> tcm a #

contextSize :: Dom (String, Type) -> Nat #

AddContext (Dom (Name, Type)) # 

Methods

addContext :: MonadTCM tcm => Dom (Name, Type) -> tcm a -> tcm a #

contextSize :: Dom (Name, Type) -> Nat #

AddContext (Dom Type) # 

Methods

addContext :: MonadTCM tcm => Dom Type -> tcm a -> tcm a #

contextSize :: Dom Type -> Nat #

AddContext ([WithHiding Name], Dom Type) # 

Methods

addContext :: MonadTCM tcm => ([WithHiding Name], Dom Type) -> tcm a -> tcm a #

contextSize :: ([WithHiding Name], Dom Type) -> Nat #

AddContext ([Name], Dom Type) # 

Methods

addContext :: MonadTCM tcm => ([Name], Dom Type) -> tcm a -> tcm a #

contextSize :: ([Name], Dom Type) -> Nat #

AddContext (String, Dom Type) # 

Methods

addContext :: MonadTCM tcm => (String, Dom Type) -> tcm a -> tcm a #

contextSize :: (String, Dom Type) -> Nat #

AddContext (Name, Dom Type) # 

Methods

addContext :: MonadTCM tcm => (Name, Dom Type) -> tcm a -> tcm a #

contextSize :: (Name, Dom Type) -> Nat #

addContext' :: (MonadTCM tcm, AddContext b) => b -> tcm a -> tcm a #

Since the module parameter substitution is relative to the current context, we need to weaken it when we extend the context. This function takes care of that.

dummyDom :: Dom Type #

Context entries without a type have this dummy type.

underAbstraction :: (Subst t a, MonadTCM tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b #

Go under an abstraction.

underAbstraction_ :: (Subst t a, MonadTCM tcm) => Abs a -> (a -> tcm b) -> tcm b #

Go under an abstract without worrying about the type to add to the context.

addLetBinding :: MonadTCM tcm => ArgInfo -> Name -> Term -> Type -> tcm a -> tcm a #

Add a let bound variable.

Querying the context

getContext :: MonadReader TCEnv m => m [Dom (Name, Type)] #

Get the current context.

getContextSize :: (Applicative m, MonadReader TCEnv m) => m Nat #

Get the size of the current context.

getContextArgs :: (Applicative m, MonadReader TCEnv m) => m Args #

Generate [var (n - 1), ..., var 0] for all declarations in the context.

getContextTerms :: (Applicative m, MonadReader TCEnv m) => m [Term] #

Generate [var (n - 1), ..., var 0] for all declarations in the context.

getContextTelescope :: (Applicative m, MonadReader TCEnv m) => m Telescope #

Get the current context as a Telescope.

getContextId :: MonadReader TCEnv m => m [CtxId] #

Check if we are in a compatible context, i.e. an extension of the given context.

getContextNames :: (Applicative m, MonadReader TCEnv m) => m [Name] #

Get the names of all declarations in the context.

lookupBV :: MonadReader TCEnv m => Nat -> m (Dom (Name, Type)) #

get type of bound variable (i.e. deBruijn index)

getVarInfo :: MonadReader TCEnv m => Name -> m (Term, Dom Type) #

Get the term corresponding to a named variable. If it is a lambda bound variable the deBruijn index is returned and if it is a let bound variable its definition is returned.