Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone





dontAssignMetas :: TCM a -> TCM a Source

Switch off assignment of metas.

getMetaStore :: TCM MetaStore Source

Get the meta store.

lookupMeta :: MetaId -> TCM MetaVariable Source

Lookup a meta variable

getMetaTypeInContext :: MetaId -> TCM Type Source

Given a meta, return the type applied to the current context.

createMetaInfo :: TCM MetaInfo Source

Create MetaInfo in the current environment.

Query and manipulate interaction points.

registerInteractionPoint :: Range -> Maybe Nat -> TCM InteractionId Source

Register an interaction point during scope checking. If there is no interaction id yet, create one.

connectInteractionPoint :: InteractionId -> MetaId -> TCM () Source

Hook up meta variable to interaction point.

removeInteractionPoint :: InteractionId -> TCM () Source

Move an interaction point from the current ones to the old ones.

getInteractionPoints :: TCM [InteractionId] Source

Get a list of interaction ids.

getInteractionMetas :: TCM [MetaId] Source

Get all metas that correspond to interaction ids.

getInteractionIdsAndMetas :: TCM [(InteractionId, MetaId)] Source

Get all metas that correspond to interaction ids.

isInteractionMeta :: MetaId -> TCM (Maybe InteractionId) Source

Does the meta variable correspond to an interaction point?

Time: O(n) where n is the number of interaction metas.

lookupInteractionPoint :: InteractionId -> TCM InteractionPoint Source

Get the information associated to an interaction point.

lookupInteractionId :: InteractionId -> TCM MetaId Source

Get MetaId for an interaction point. Precondition: interaction point is connected.

newMeta :: MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId Source

Generate new meta variable.

newMeta' :: MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId Source

Generate a new meta variable with some instantiation given. For instance, the instantiation could be a PostponedTypeCheckingProblem.

getInteractionRange :: InteractionId -> TCM Range Source

Get the Range for an interaction point.

getMetaRange :: MetaId -> TCM Range Source

Get the Range for a meta variable.

listenToMeta :: Listener -> MetaId -> TCM () Source

listenToMeta l m: register l as a listener to m. This is done when the type of l is blocked by m.

unlistenToMeta :: Listener -> MetaId -> TCM () Source

Unregister a listener.

getMetaListeners :: MetaId -> TCM [Listener] Source

Get the listeners to a meta.

Freezing and unfreezing metas.

withFreezeMetas :: TCM a -> TCM a Source

Freeze all so far unfrozen metas for the duration of the given computation.

freezeMetas :: TCM [MetaId] Source

Freeze all meta variables and return the list of metas that got frozen.

unfreezeMetas :: TCM () Source

Thaw all meta variables.

unfreezeMetas' :: (MetaId -> Bool) -> TCM () Source

Thaw some metas, as indicated by the passed condition.

class UnFreezeMeta a where Source

Unfreeze meta and its type if this is a meta again. Does not unfreeze deep occurrences of metas.


unfreezeMeta :: a -> TCM () Source