| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.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 where
- addCtx :: Name -> Dom Type -> m a -> m a
- addLetBinding' :: 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)
- getLetBindings :: MonadTCM tcm => tcm [(Name, (Term, Dom Type))]
- defaultAddLetBinding' :: (ReadTCState m, MonadTCEnv m) => Name -> Term -> Dom Type -> m a -> m a
- addLetBinding :: MonadAddContext m => ArgInfo -> Name -> Term -> Type -> m a -> m 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 (Maybe (Dom (Name, Type)))
- lookupBV :: (MonadFail m, MonadTCEnv m) => Nat -> m (Dom (Name, Type))
- domOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Dom Type)
- typeOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Type
- nameOfBV' :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Maybe Name)
- nameOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Name
- getVarInfo :: (MonadFail 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 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 :: (MonadAddContext n, MonadTransControl t, t n ~ m) => Name -> Dom Type -> m a -> m a Source #
addLetBinding' :: Name -> Term -> Dom Type -> m a -> m a Source #
Add a let bound variable to the context
default addLetBinding' :: (MonadAddContext n, MonadTransControl t, t n ~ m) => 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 :: (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 :: (MonadAddContext n, MonadTransControl t, t n ~ m) => Range -> ArgName -> (Name -> m a) -> m a Source #
Instances
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.
Instances
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 # | |
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |
| AddContext (KeepNames String, Dom Type) Source # | |
Defined in Agda.TypeChecking.Monad.Context | |
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 #
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.
defaultAddLetBinding' :: (ReadTCState m, MonadTCEnv m) => Name -> Term -> Dom Type -> m a -> m a Source #
Add a let bound variable
addLetBinding :: MonadAddContext m => ArgInfo -> Name -> Term -> Type -> m a -> m 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 (Maybe (Dom (Name, Type))) Source #
get type of bound variable (i.e. deBruijn index)
domOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Dom Type) Source #
typeOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Type Source #
nameOfBV' :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Maybe Name) Source #
nameOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Name Source #
getVarInfo :: (MonadFail 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.