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.

Minimal complete definition



unfreezeMeta :: a -> TCM () Source #