Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Monad.MetaVars

Synopsis

- getMetaStore :: MonadTCM tcm => tcm MetaStore
- lookupMeta :: MonadTCM tcm => MetaId -> tcm MetaVariable
- updateMetaVar :: MonadTCM tcm => MetaId -> (MetaVariable -> MetaVariable) -> tcm ()
- getMetaPriority :: MonadTCM tcm => MetaId -> tcm MetaPriority
- isSortMeta :: MonadTCM tcm => MetaId -> tcm Bool
- isInstantiatedMeta :: MonadTCM tcm => MetaId -> tcm Bool
- createMetaInfo :: MonadTCM tcm => tcm MetaInfo
- updateMetaVarRange :: MonadTCM tcm => MetaId -> Range -> tcm ()
- addInteractionPoint :: MonadTCM tcm => InteractionId -> MetaId -> tcm ()
- removeInteractionPoint :: MonadTCM tcm => InteractionId -> tcm ()
- getInteractionPoints :: MonadTCM tcm => tcm [InteractionId]
- getInteractionMetas :: MonadTCM tcm => tcm [MetaId]
- isInteractionMeta :: MonadTCM tcm => MetaId -> tcm Bool
- lookupInteractionId :: MonadTCM tcm => InteractionId -> tcm MetaId
- judgementInteractionId :: MonadTCM tcm => InteractionId -> tcm (Judgement Type MetaId)
- newMeta :: MonadTCM tcm => MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> tcm MetaId
- newMeta' :: MonadTCM tcm => MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> tcm MetaId
- getInteractionRange :: MonadTCM tcm => InteractionId -> tcm Range
- getMetaRange :: MonadTCM tcm => MetaId -> tcm Range
- getInteractionScope :: MonadTCM tcm => InteractionId -> tcm ScopeInfo
- withMetaInfo :: MonadTCM tcm => MetaInfo -> tcm a -> tcm a
- getInstantiatedMetas :: MonadTCM tcm => tcm [MetaId]
- getOpenMetas :: MonadTCM tcm => tcm [MetaId]
- listenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm ()
- unlistenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm ()
- getMetaListeners :: MonadTCM tcm => MetaId -> tcm [MetaId]
- clearMetaListeners :: MonadTCM tcm => MetaId -> tcm ()

# Documentation

getMetaStore :: MonadTCM tcm => tcm MetaStore

Get the meta store.

lookupMeta :: MonadTCM tcm => MetaId -> tcm MetaVariable

Lookup a meta variable

updateMetaVar :: MonadTCM tcm => MetaId -> (MetaVariable -> MetaVariable) -> tcm ()

getMetaPriority :: MonadTCM tcm => MetaId -> tcm MetaPriority

isSortMeta :: MonadTCM tcm => MetaId -> tcm Bool

isInstantiatedMeta :: MonadTCM tcm => MetaId -> tcm Bool

createMetaInfo :: MonadTCM tcm => tcm MetaInfo

updateMetaVarRange :: MonadTCM tcm => MetaId -> Range -> tcm ()

addInteractionPoint :: MonadTCM tcm => InteractionId -> MetaId -> tcm ()

removeInteractionPoint :: MonadTCM tcm => InteractionId -> tcm ()

getInteractionPoints :: MonadTCM tcm => tcm [InteractionId]

getInteractionMetas :: MonadTCM tcm => tcm [MetaId]

isInteractionMeta :: MonadTCM tcm => MetaId -> tcm Bool

Does the meta variable correspond to an interaction point?

lookupInteractionId :: MonadTCM tcm => InteractionId -> tcm MetaId

judgementInteractionId :: MonadTCM tcm => InteractionId -> tcm (Judgement Type MetaId)

newMeta :: MonadTCM tcm => MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> tcm MetaId

Generate new meta variable.

newMeta' :: MonadTCM tcm => MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> tcm MetaId

getInteractionRange :: MonadTCM tcm => InteractionId -> tcm Range

getMetaRange :: MonadTCM tcm => MetaId -> tcm Range

getInteractionScope :: MonadTCM tcm => InteractionId -> tcm ScopeInfo

withMetaInfo :: MonadTCM tcm => MetaInfo -> tcm a -> tcm a

getInstantiatedMetas :: MonadTCM tcm => tcm [MetaId]

getOpenMetas :: MonadTCM tcm => tcm [MetaId]

listenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm ()

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

unlistenToMeta :: MonadTCM tcm => MetaId -> MetaId -> tcm ()

Unregister a listener.

getMetaListeners :: MonadTCM tcm => MetaId -> tcm [MetaId]

Get the listeners to a meta.

clearMetaListeners :: MonadTCM tcm => MetaId -> tcm ()