Agda-2.8.0: 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

- unsafeModifyContext :: MonadTCEnv tcm => (Context -> Context) -> tcm a -> tcm a
- modifyContextInfo :: MonadTCEnv tcm => (forall e. Dom e -> Dom e) -> tcm a -> tcm a
- inTopContext :: (MonadTCEnv tcm, ReadTCState tcm) => tcm a -> tcm a
- unsafeInTopContext :: (MonadTCEnv m, ReadTCState m) => m a -> m a
- unsafeEscapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
- escapeContext :: MonadAddContext m => Impossible -> Int -> m a -> m a
- checkpoint :: (MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm, ReadTCState tcm) => Substitution -> tcm a -> tcm a
- checkpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution
- checkpointSubstitution' :: MonadTCEnv tcm => CheckpointId -> tcm (Maybe Substitution)
- getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m (Maybe Substitution)
- class MonadTCEnv m => MonadAddContext (m :: Type -> Type) where
  - addCtx :: Name -> Dom Type -> m a -> m a
  - addLetBinding' :: Origin -> Name -> Term -> Dom Type -> m a -> m a
  - updateContext :: Substitution -> (Context -> Context) -> m a -> m a
  - withFreshName :: Range -> ArgName -> (Name -> m a) -> m a
- defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a
- withFreshName_ :: MonadAddContext m => ArgName -> (Name -> m a) -> m a
- withShadowingNameTCM :: Name -> TCM b -> TCM b
- addRecordNameContext :: (MonadAddContext m, MonadFresh NameId m) => Dom Type -> m b -> m b
- class AddContext b where
  - addContext :: MonadAddContext m => b -> m a -> m a
  - contextSize :: b -> Nat
- newtype KeepNames a = KeepNames a
- underAbstraction :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b
- underAbstraction' :: (Subst a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
- underAbstractionAbs :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b
- underAbstractionAbs' :: (Subst a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
- underAbstraction_ :: (Subst a, MonadAddContext m) => Abs a -> (a -> m b) -> m b
- mapAbstraction :: (Subst a, Subst b, MonadAddContext m) => Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
- mapAbstraction_ :: (Subst a, Subst b, MonadAddContext m) => (a -> m b) -> Abs a -> m (Abs b)
- getLetBindings :: MonadTCEnv tcm => tcm [(Name, LetBinding)]
- defaultAddLetBinding' :: (ReadTCState m, MonadTCEnv m) => Origin -> Name -> Term -> Dom Type -> m a -> m a
- addLetBinding :: MonadAddContext m => ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a
- removeLetBinding :: MonadTCEnv m => Name -> m a -> m a
- removeLetBindingsFrom :: MonadTCEnv m => Name -> m a -> m a
- getContext :: MonadTCEnv m => m Context
- getContextSize :: MonadTCEnv m => m Nat
- getContextVars :: MonadTCEnv m => m [(Int, Dom Name)]
- getContextVars' :: MonadTCEnv m => m [(Int, Dom Name)]
- contextVars :: Context -> [(Int, Dom Name)]
- contextVars' :: Context -> [(Int, Dom Name)]
- getContextArgs :: MonadTCEnv m => m Args
- contextArgs :: Context -> Args
- getContextTerms :: MonadTCEnv m => m [Term]
- contextTerms :: Context -> [Term]
- getContextTelescope :: MonadTCEnv m => m Telescope
- contextToTel :: Context -> Telescope
- getContextNames :: MonadTCEnv m => m [Name]
- getContextNames' :: MonadTCEnv m => m [Name]
- contextNames :: Context -> [Name]
- contextNames' :: Context -> [Name]
- lookupBV_ :: Nat -> Context -> Maybe ContextEntry
- lookupBV' :: MonadTCEnv m => Nat -> m (Maybe ContextEntry)
- lookupBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m ContextEntry
- ctxEntryName :: ContextEntry -> Name
- ctxEntryDom :: ContextEntry -> Dom Type
- ctxEntryType :: ContextEntry -> Type
- domOfBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m (Dom Type)
- typeOfBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m Type
- nameOfBV' :: MonadTCEnv m => Nat -> m (Maybe Name)
- nameOfBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m Name
- getVarInfo :: (MonadDebug m, MonadTCEnv m) => Name -> m (Term, Dom Type)

# Modifying the context

unsafeModifyContext :: MonadTCEnv tcm => (Context -> Context) -> tcm a -> tcm a Source #

Modify a `Context` in a computation. Warning: does not update the checkpoints. Use `updateContext` instead.

modifyContextInfo :: MonadTCEnv tcm => (forall e. Dom e -> Dom e) -> tcm a -> tcm a Source #

Modify the `Dom` part of context entries.

inTopContext :: (MonadTCEnv tcm, ReadTCState tcm) => tcm a -> tcm a Source #

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

unsafeInTopContext :: (MonadTCEnv m, ReadTCState m) => m a -> m a Source #

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

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

Delete the last `n` bindings from the context.

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

escapeContext :: MonadAddContext m => Impossible -> Int -> m a -> m a Source #

Delete the last `n` bindings from the context. Any occurrences of these variables are replaced with the given `err`.

# Manipulating checkpoints --

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

Add a new checkpoint. Do not use directly!

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 (Maybe Substitution) Source #

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

Returns `Nothing` in case the we don't have a checkpoint for `m`.

# Adding to the context

class MonadTCEnv m => MonadAddContext (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

addCtx :: Name -> Dom Type -> m a -> m a Source #

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

Chooses an unused `Name`.

Warning: Does not update module parameter substitution!

default addCtx :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type) a. (MonadAddContext n, MonadTransControl t, t n ~ m) => Name -> Dom Type -> m a -> m a Source #

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> m a -> m a Source #

Add a let bound variable to the context

default addLetBinding' :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type) a. (MonadAddContext n, MonadTransControl t, t n ~ m) => Origin -> Name -> Term -> Dom Type -> m a -> m a Source #

updateContext :: Substitution -> (Context -> Context) -> m a -> m a Source #

Update the context. Requires a substitution that transports things living in the old context to the new.

default updateContext :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type) a. (MonadAddContext n, MonadTransControl t, t n ~ m) => Substitution -> (Context -> Context) -> m a -> m a Source #

withFreshName :: Range -> ArgName -> (Name -> m a) -> m a Source #

default withFreshName :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type) a. (MonadAddContext n, MonadTransControl t, t n ~ m) => Range -> ArgName -> (Name -> m a) -> m a Source #

#### Instances

Instances details

MonadAddContext TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods addCtx :: Name -> Dom Type -> TerM a -> TerM a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> TerM a -> TerM a Source # updateContext :: Substitution -> (Context -> Context) -> TerM a -> TerM a Source # withFreshName :: Range -> ArgName -> (Name -> TerM a) -> TerM a Source #
MonadAddContext ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods addCtx :: Name -> Dom Type -> ReduceM a -> ReduceM a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> ReduceM a -> ReduceM a Source # updateContext :: Substitution -> (Context -> Context) -> ReduceM a -> ReduceM a Source # withFreshName :: Range -> ArgName -> (Name -> ReduceM a) -> ReduceM a Source #
MonadAddContext TCM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addCtx :: Name -> Dom Type -> TCM a -> TCM a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> TCM a -> TCM a Source # updateContext :: Substitution -> (Context -> Context) -> TCM a -> TCM a Source # withFreshName :: Range -> ArgName -> (Name -> TCM a) -> TCM a Source #
MonadAddContext NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods addCtx :: Name -> Dom Type -> NLM a -> NLM a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a Source # updateContext :: Substitution -> (Context -> Context) -> NLM a -> NLM a Source # withFreshName :: Range -> ArgName -> (Name -> NLM a) -> NLM a Source #
MonadAddContext m => MonadAddContext (PureConversionT m) Source # |

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addCtx :: Name -> Dom Type -> PureConversionT m a -> PureConversionT m a Source #

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> PureConversionT m a -> PureConversionT m a Source #

updateContext :: Substitution -> (Context -> Context) -> PureConversionT m a -> PureConversionT m a Source #

withFreshName :: Range -> ArgName -> (Name -> PureConversionT m a) -> PureConversionT m a Source #

MonadAddContext m => MonadAddContext (BlockT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addCtx :: Name -> Dom Type -> BlockT m a -> BlockT m a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> BlockT m a -> BlockT m a Source # updateContext :: Substitution -> (Context -> Context) -> BlockT m a -> BlockT m a Source # withFreshName :: Range -> ArgName -> (Name -> BlockT m a) -> BlockT m a Source #
MonadAddContext m => MonadAddContext (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods addCtx :: Name -> Dom Type -> NamesT m a -> NamesT m a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> NamesT m a -> NamesT m a Source # updateContext :: Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a Source # withFreshName :: Range -> ArgName -> (Name -> NamesT m a) -> NamesT m a Source #
MonadAddContext m => MonadAddContext (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addCtx :: Name -> Dom Type -> ListT m a -> ListT m a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> ListT m a -> ListT m a Source # updateContext :: Substitution -> (Context -> Context) -> ListT m a -> ListT m a Source # withFreshName :: Range -> ArgName -> (Name -> ListT m a) -> ListT m a Source #
MonadAddContext m => MonadAddContext (ChangeT m) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ChangeT m a -> ChangeT m a Source #

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> ChangeT m a -> ChangeT m a Source #

updateContext :: Substitution -> (Context -> Context) -> ChangeT m a -> ChangeT m a Source #

withFreshName :: Range -> ArgName -> (Name -> ChangeT m a) -> ChangeT m a Source #

MonadAddContext m => MonadAddContext (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addCtx :: Name -> Dom Type -> MaybeT m a -> MaybeT m a Source # addLetBinding' :: Origin -> Name -> Term -> Dom Type -> MaybeT m a -> MaybeT m a Source # updateContext :: Substitution -> (Context -> Context) -> MaybeT m a -> MaybeT m a Source # withFreshName :: Range -> ArgName -> (Name -> MaybeT m a) -> MaybeT m a Source #
MonadAddContext m => MonadAddContext (ExceptT e m) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ExceptT e m a -> ExceptT e m a Source #

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> ExceptT e m a -> ExceptT e m a Source #

updateContext :: Substitution -> (Context -> Context) -> ExceptT e m a -> ExceptT e m a Source #

withFreshName :: Range -> ArgName -> (Name -> ExceptT e m a) -> ExceptT e m a Source #

MonadAddContext m => MonadAddContext (IdentityT m) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> IdentityT m a -> IdentityT m a Source #

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> IdentityT m a -> IdentityT m a Source #

updateContext :: Substitution -> (Context -> Context) -> IdentityT m a -> IdentityT m a Source #

withFreshName :: Range -> ArgName -> (Name -> IdentityT m a) -> IdentityT m a Source #

MonadAddContext m => MonadAddContext (ReaderT r m) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ReaderT r m a -> ReaderT r m a Source #

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> ReaderT r m a -> ReaderT r m a Source #

updateContext :: Substitution -> (Context -> Context) -> ReaderT r m a -> ReaderT r m a Source #

withFreshName :: Range -> ArgName -> (Name -> ReaderT r m a) -> ReaderT r m a Source #

MonadAddContext m => MonadAddContext (StateT r m) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> StateT r m a -> StateT r m a Source #

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> StateT r m a -> StateT r m a Source #

updateContext :: Substitution -> (Context -> Context) -> StateT r m a -> StateT r m a Source #

withFreshName :: Range -> ArgName -> (Name -> StateT r m a) -> StateT r m a Source #

(Monoid w, MonadAddContext m) => MonadAddContext (WriterT w m) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> WriterT w m a -> WriterT w m a Source #

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> WriterT w m a -> WriterT w m a Source #

updateContext :: Substitution -> (Context -> Context) -> WriterT w m a -> WriterT w m a Source #

withFreshName :: Range -> ArgName -> (Name -> WriterT w m a) -> WriterT w m a Source #

defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a Source #

Default implementation of addCtx in terms of updateContext

withFreshName_ :: MonadAddContext m => ArgName -> (Name -> m a) -> m a Source #

withShadowingNameTCM :: Name -> TCM b -> TCM b Source #

Run the given TCM action, and register the given variable as being shadowed by all the names with the same root that are added to the context during this TCM action.

addRecordNameContext :: (MonadAddContext m, MonadFresh NameId m) => Dom Type -> m b -> m b Source #

class AddContext b where Source #

Various specializations of `addCtx`.

Methods

addContext :: MonadAddContext m => b -> m a -> m a Source #

contextSize :: b -> Nat Source #

#### Instances

Instances details

AddContext Name Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Name -> m a -> m a Source # contextSize :: Name -> Nat Source #
AddContext Telescope Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source #
AddContext ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ContextEntry -> m a -> m a Source # contextSize :: ContextEntry -> Nat Source #
AddContext String Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => String -> m a -> m a Source # contextSize :: String -> Nat Source #
AddContext (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom Type -> m a -> m a Source # contextSize :: Dom Type -> Nat Source #
AddContext (Dom (Name, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # contextSize :: Dom (Name, Type) -> Nat Source #
AddContext (Dom (String, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source # contextSize :: Dom (String, Type) -> Nat Source #
AddContext (KeepNames Telescope) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # contextSize :: KeepNames Telescope -> Nat Source #
AddContext a => AddContext [a] Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => [a] -> m a0 -> m a0 Source # contextSize :: [a] -> Nat Source #
AddContext (Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # contextSize :: (Name, Dom Type) -> Nat Source #
AddContext (KeepNames String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source # contextSize :: (KeepNames String, Dom Type) -> Nat Source #
AddContext (List1 Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 Name, Dom Type) -> m a -> m a Source # contextSize :: (List1 Name, Dom Type) -> Nat Source #
AddContext (List1 (Arg Name), Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (Arg Name), Type) -> m a -> m a Source # contextSize :: (List1 (Arg Name), Type) -> Nat Source #
AddContext (List1 (NamedArg Name), Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # contextSize :: (List1 (NamedArg Name), Type) -> Nat Source #
AddContext (List1 (WithHiding Name), Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source #
AddContext (Text, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source # contextSize :: (Text, Dom Type) -> Nat Source #
AddContext (String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source # contextSize :: (String, Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext ([Arg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # contextSize :: ([Arg Name], Type) -> Nat Source #
AddContext ([NamedArg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([WithHiding Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], 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

Instances details

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

underAbstraction :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b Source #

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

underAbstraction' :: (Subst a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b Source #

underAbstractionAbs :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b Source #

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

underAbstractionAbs' :: (Subst a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b Source #

underAbstraction_ :: (Subst a, MonadAddContext m) => Abs a -> (a -> m b) -> m b Source #

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

mapAbstraction :: (Subst a, Subst b, MonadAddContext m) => Dom Type -> (a -> m b) -> Abs a -> m (Abs b) Source #

Map a monadic function on the thing under the abstraction, adding the abstracted variable to the context.

mapAbstraction_ :: (Subst a, Subst b, MonadAddContext m) => (a -> m b) -> Abs a -> m (Abs b) Source #

getLetBindings :: MonadTCEnv tcm => tcm [(Name, LetBinding)] Source #

defaultAddLetBinding' :: (ReadTCState m, MonadTCEnv m) => Origin -> Name -> Term -> Dom Type -> m a -> m a Source #

Add a let bound variable

addLetBinding :: MonadAddContext m => ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a Source #

Add a let bound variable

removeLetBinding :: MonadTCEnv m => Name -> m a -> m a Source #

Remove a let bound variable.

removeLetBindingsFrom :: MonadTCEnv m => Name -> m a -> m a Source #

Remove a let bound variable and all let bindings introduced after it. For instance before printing its body to avoid folding the binding itself, or using bindings defined later. Relies on the invariant that names introduced later are sorted after earlier names.

# Querying the context

getContext :: MonadTCEnv m => m Context Source #

Get the current context.

getContextSize :: MonadTCEnv m => m Nat Source #

Get the size of the current context.

getContextVars :: MonadTCEnv m => m [(Int, Dom Name)] Source #

getContextVars' :: MonadTCEnv m => m [(Int, Dom Name)] Source #

contextVars :: Context -> [(Int, Dom Name)] Source #

contextVars' :: Context -> [(Int, Dom Name)] Source #

getContextArgs :: MonadTCEnv m => m Args Source #

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

contextArgs :: Context -> Args Source #

getContextTerms :: MonadTCEnv m => m [Term] Source #

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

contextTerms :: Context -> [Term] Source #

getContextTelescope :: MonadTCEnv m => m Telescope Source #

Get the current context as a `Telescope`.

contextToTel :: Context -> Telescope Source #

getContextNames :: MonadTCEnv m => m [Name] Source #

Get the names of all declarations in the context.

getContextNames' :: MonadTCEnv m => m [Name] Source #

contextNames :: Context -> [Name] Source #

contextNames' :: Context -> [Name] Source #

lookupBV_ :: Nat -> Context -> Maybe ContextEntry Source #

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

lookupBV' :: MonadTCEnv m => Nat -> m (Maybe ContextEntry) Source #

lookupBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m ContextEntry Source #

ctxEntryName :: ContextEntry -> Name Source #

ctxEntryDom :: ContextEntry -> Dom Type Source #

ctxEntryType :: ContextEntry -> Type Source #

domOfBV :: (MonadDebug m, MonadTCEnv m) => Nat -> m (Dom Type) Source #

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

nameOfBV' :: MonadTCEnv m => Nat -> m (Maybe Name) Source #

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

getVarInfo :: (MonadDebug m, 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.