ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Monad.Context

1 type
2 classes
40 values

PackageAgda-2.7.0.1
Exports43
LanguageHaskell2010
LicenceMIT
SourceContext.hs

Modifying the context

6 declarations

valueunsafeModifyContext

:: MonadTCEnv tcm
=> Context -> Context
-> tcm a
-> tcm a

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

valuemodifyContextInfo

:: MonadTCEnv tcm
=> forall e. Dom e -> Dom e
-> tcm a
-> tcm a

Modify the Dom part of context entries.

valueinTopContext :: (MonadTCEnv tcm, ReadTCState tcm) => tcm a -> tcm a

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

valueunsafeInTopContext :: (MonadTCEnv m, ReadTCState m) => m a -> m a

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

valueunsafeEscapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a

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.

valueescapeContext :: MonadAddContext m => Impossible -> Int -> m a -> m a

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

Manipulating checkpoints --

4 declarations

valuecheckpoint

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

Add a new checkpoint. Do not use directly!

valuecheckpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution

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

valuecheckpointSubstitution'

:: MonadTCEnv tcm
=> CheckpointId
-> tcm (Maybe Substitution)

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

valuegetModuleParameterSub

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

19 declarations

classclass MonadTCEnv m => MonadAddContext (m :: Type -> Type) where

Methods

addCtx :: Name -> Dom Type -> m a -> m a
addCtx x arg cont add a variable to the context.
Chooses an unused Name.
Warning: Does not update module parameter substitution!
addLetBinding' :: Origin -> Name -> Term -> Dom Type -> m a -> m a
Add a let bound variable to the context
updateContext :: Substitution -> (Context -> Context) -> m a -> m a
Update the context. Requires a substitution that transports things living in the old context to the new.
withFreshName :: Range -> ArgName -> (Name -> m a) -> m a

Instances16MonadAddContext, …

MonadAddContext AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadAddContext TerMDefined in Agda-2.7.0.1 · Agda.Termination.Monad
MonadAddContext ReduceMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce.Monad · orphan
MonadAddContext TCMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
MonadAddContext NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadAddContext m => MonadAddContext (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure
MonadAddContext m => MonadAddContext (BlockT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
MonadAddContext m => MonadAddContext (NamesT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Names
MonadAddContext m => MonadAddContext (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
MonadAddContext m => MonadAddContext (ChangeT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
MonadAddContext m => MonadAddContext (MaybeT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
MonadAddContext m => MonadAddContext (ExceptT e m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
MonadAddContext m => MonadAddContext (IdentityT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
MonadAddContext m => MonadAddContext (ReaderT r m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
MonadAddContext m => MonadAddContext (StateT r m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
(Monoid w, MonadAddContext m) => MonadAddContext (WriterT w m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context

valuedefaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a

Default implementation of addCtx in terms of updateContext

valuewithFreshName_ :: MonadAddContext m => ArgName -> (Name -> m a) -> m a

valuewithShadowingNameTCM :: Name -> TCM b -> TCM b

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.

valueaddRecordNameContext

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

classclass AddContext b where

Various specializations of addCtx.

Methods

addContext :: MonadAddContext m => b -> m a -> m a
contextSize :: b -> Nat

Instances20AddContext, …

AddContext NameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext TelescopeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext StringDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (Dom (Name, Type))Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (Dom (String, Type))Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (KeepNames Telescope)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext a => AddContext [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (Name, Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (KeepNames String, Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (List1 Name, Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (List1 (Arg Name), Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (List1 (NamedArg Name), Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (List1 (WithHiding Name), Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (String, Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (Text, Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext ([Name], Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext ([Arg Name], Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext ([NamedArg Name], Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext ([WithHiding Name], Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context

newtypenewtype KeepNames a

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

Instances2AddContext

AddContext (KeepNames Telescope)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
AddContext (KeepNames String, Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context

valueunderAbstraction

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

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

valueunderAbstraction'

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

valueunderAbstractionAbs

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

Go under an abstraction, treating NoAbs as Abs.

valueunderAbstractionAbs'

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

valueunderAbstraction_

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

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

valuemapAbstraction

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

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

valuemapAbstraction_

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

valuegetLetBindings :: MonadTCEnv tcm => tcm [(Name, LetBinding)]

valuedefaultAddLetBinding'

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

Add a let bound variable

valueaddLetBinding

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

Add a let bound variable

valueremoveLetBinding :: MonadTCEnv m => Name -> m a -> m a

Remove a let bound variable.

valueremoveLetBindingsFrom :: MonadTCEnv m => Name -> m a -> m a

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

14 declarations

valuegetContext :: MonadTCEnv m => m Context

Get the current context.

valuegetContextSize :: (Applicative m, MonadTCEnv m) => m Nat

Get the size of the current context.

valuegetContextArgs :: (Applicative m, MonadTCEnv m) => m Args

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

valuegetContextTerms :: (Applicative m, MonadTCEnv m) => m [Term]

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

valuegetContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope

Get the current context as a Telescope.

valuegetContextNames :: (Applicative m, MonadTCEnv m) => m [Name]

Get the names of all declarations in the context.

valuelookupBV_ :: Nat -> Context -> Maybe ContextEntry

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

valuelookupBV' :: MonadTCEnv m => Nat -> m (Maybe ContextEntry)

valuelookupBV :: (MonadFail m, MonadTCEnv m) => Nat -> m (Dom (Name, Type))

valuedomOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Dom Type)

valuetypeOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Type

valuenameOfBV'

:: (Applicative m, MonadFail m, MonadTCEnv m)
=> Nat
-> m (Maybe Name)

valuenameOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Name

valuegetVarInfo :: (MonadFail m, MonadTCEnv 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.