Agda.TypeChecking.Monad.MetaVars
- 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 ()