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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Context

Contents

- Modifying the context
- Manipulating checkpoints --
- Adding to the context
- Querying the context

Synopsis

- modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm a
- safeInTopContext :: MonadTCM tcm => tcm a -> tcm a
- inTopContext :: MonadTCM tcm => tcm a -> tcm a
- escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
- checkpoint :: (MonadDebug tcm, MonadTCM tcm) => Substitution -> tcm a -> tcm a
- updateContext :: (MonadDebug tcm, MonadTCM tcm) => Substitution -> (Context -> Context) -> tcm a -> tcm a
- checkpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution
- checkpointSubstitution' :: MonadTCEnv tcm => CheckpointId -> tcm (Maybe Substitution)
- getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m Substitution
- addCtx :: (MonadDebug tcm, MonadTCM tcm) => Name -> Dom Type -> tcm a -> tcm a
- addRecordNameContext :: (MonadDebug m, MonadTCM m) => Dom Type -> m b -> m b
- class AddContext b where
  - addContext :: (MonadTCM tcm, MonadDebug tcm) => b -> tcm a -> tcm a
  - contextSize :: b -> Nat
- newtype KeepNames a = KeepNames a
- underAbstraction :: (Subst t a, MonadTCM tcm, MonadDebug tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b
- underAbstraction' :: (Subst t a, MonadTCM tcm, MonadDebug tcm, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> tcm b) -> tcm b
- underAbstractionAbs :: (Subst t a, MonadTCM tcm, MonadDebug tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b
- underAbstractionAbs' :: (Subst t a, MonadTCM tcm, MonadDebug tcm, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> tcm b) -> tcm b
- underAbstraction_ :: (Subst t a, MonadTCM tcm, MonadDebug tcm) => Abs a -> (a -> tcm b) -> tcm b
- getLetBindings :: MonadTCM tcm => tcm [(Name, (Term, Dom Type))]
- addLetBinding' :: MonadTCM tcm => Name -> Term -> Dom Type -> tcm a -> tcm a
- addLetBinding :: MonadTCM tcm => ArgInfo -> Name -> Term -> Type -> tcm a -> tcm a
- getContext :: MonadTCEnv m => m [Dom (Name, Type)]
- getContextSize :: (Applicative m, MonadTCEnv m) => m Nat
- getContextArgs :: (Applicative m, MonadTCEnv m) => m Args
- getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term]
- getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope
- getContextNames :: (Applicative m, MonadTCEnv m) => m [Name]
- lookupBV :: MonadTCEnv m => Nat -> m (Dom (Name, Type))
- typeOfBV' :: (Applicative m, MonadTCEnv m) => Nat -> m (Dom Type)
- typeOfBV :: (Applicative m, MonadTCEnv m) => Nat -> m Type
- nameOfBV :: (Applicative m, MonadTCEnv m) => Nat -> m Name
- getVarInfo :: MonadTCEnv m => Name -> m (Term, Dom Type)

# Modifying the context

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

Modify a `Context` in a computation.

safeInTopContext :: MonadTCM tcm => tcm a -> tcm a Source #

Change to top (=empty) context. Resets the checkpoints.

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

Change to top (=empty) context, but don't update the checkpoints. Totally not safe!

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

Delete the last `n` bindings from the context.

Doesn't update checkpoints! Use `updateContext rho (drop n)` instead, for an appropriate substitution `rho`.

# Manipulating checkpoints --

checkpoint :: (MonadDebug tcm, MonadTCM tcm) => Substitution -> tcm a -> tcm a Source #

Add a new checkpoint. Do not use directly!

updateContext :: (MonadDebug tcm, MonadTCM tcm) => Substitution -> (Context -> Context) -> tcm a -> tcm a Source #

Update the context. Requires a substitution from the old context to the new.

checkpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution Source #

Get the substitution from the context at a given checkpoint to the current context.

checkpointSubstitution' :: MonadTCEnv tcm => CheckpointId -> tcm (Maybe Substitution) Source #

Get the substitution from the context at a given checkpoint to the current context.

getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m Substitution Source #

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

In case the we don't have a checkpoint for `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 :: (MonadDebug tcm, MonadTCM tcm) => Name -> Dom Type -> tcm a -> tcm a Source #

`addCtx x arg cont` add a variable to the context.

Chooses an unused `Name`.

Warning: Does not update module parameter substitution!

addRecordNameContext :: (MonadDebug m, MonadTCM m) => Dom Type -> m b -> m b Source #

class AddContext b where Source #

Various specializations of `addCtx`.

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => b -> tcm a -> tcm a Source #

contextSize :: b -> Nat Source #

Instances

AddContext String Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => String -> tcm a -> tcm a Source # contextSize :: String -> Nat Source #
AddContext Name Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Name -> tcm a -> tcm a Source # contextSize :: Name -> Nat Source #
AddContext Telescope Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a Source # contextSize :: Telescope -> Nat Source #
AddContext a => AddContext [a] Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => [a] -> tcm a0 -> tcm a0 Source # contextSize :: [a] -> Nat Source #
AddContext (Dom (String, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a Source # contextSize :: Dom (String, Type) -> Nat Source #
AddContext (Dom (Name, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a Source # contextSize :: Dom (Name, Type) -> Nat Source #
AddContext (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom Type -> tcm a -> tcm a Source # contextSize :: Dom Type -> Nat Source #
AddContext (KeepNames Telescope) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a Source # contextSize :: KeepNames Telescope -> Nat Source #
AddContext ([NamedArg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([Arg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Arg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([Arg Name], Type) -> Nat Source #
AddContext ([WithHiding Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (String, Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a Source # contextSize :: (Name, Dom Type) -> Nat Source #
AddContext (KeepNames String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (KeepNames String, Dom Type) -> Nat Source #

newtype KeepNames a Source #

Wrapper to tell `addContext` not to mark names as `NotInScope`. Used when adding a user-provided, but already type checked, telescope to the context.

Constructors

KeepNames a |

Instances

AddContext (KeepNames Telescope) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a Source # contextSize :: KeepNames Telescope -> Nat Source #
AddContext (KeepNames String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (KeepNames String, Dom Type) -> Nat Source #

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

Go under an abstraction. Do not extend context in case of `NoAbs`.

underAbstraction' :: (Subst t a, MonadTCM tcm, MonadDebug tcm, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> tcm b) -> tcm b Source #

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

Go under an abstraction, treating `NoAbs` as `Abs`.

underAbstractionAbs' :: (Subst t a, MonadTCM tcm, MonadDebug tcm, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> tcm b) -> tcm b Source #

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

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

getLetBindings :: MonadTCM tcm => tcm [(Name, (Term, Dom Type))] Source #

addLetBinding' :: MonadTCM tcm => Name -> Term -> Dom Type -> tcm a -> tcm a Source #

Add a let bound variable

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

Add a let bound variable

# Querying the context

getContext :: MonadTCEnv m => m [Dom (Name, Type)] Source #

Get the current context.

getContextSize :: (Applicative m, MonadTCEnv m) => m Nat Source #

Get the size of the current context.

getContextArgs :: (Applicative m, MonadTCEnv m) => m Args Source #

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

getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term] Source #

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

getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope Source #

Get the current context as a `Telescope`.

getContextNames :: (Applicative m, MonadTCEnv m) => m [Name] Source #

Get the names of all declarations in the context.

lookupBV :: MonadTCEnv m => Nat -> m (Dom (Name, Type)) Source #

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

typeOfBV' :: (Applicative m, MonadTCEnv m) => Nat -> m (Dom Type) Source #

typeOfBV :: (Applicative m, MonadTCEnv m) => Nat -> m Type Source #

nameOfBV :: (Applicative m, MonadTCEnv m) => Nat -> m Name Source #

getVarInfo :: MonadTCEnv m => Name -> m (Term, Dom Type) Source #

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.