Safe Haskell | None |
---|
Agda.TypeChecking.Monad.MetaVars
- dontAssignMetas :: TCM a -> TCM a
- getMetaStore :: TCM MetaStore
- modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
- lookupMeta :: MetaId -> TCM MetaVariable
- updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
- getMetaPriority :: MetaId -> TCM MetaPriority
- isSortMeta :: MetaId -> TCM Bool
- getMetaType :: MetaId -> TCM Type
- isInstantiatedMeta :: MetaId -> TCM Bool
- createMetaInfo :: TCM MetaInfo
- createMetaInfo' :: RunMetaOccursCheck -> TCM MetaInfo
- setValueMetaName :: Term -> MetaNameSuggestion -> TCM ()
- getMetaNameSuggestion :: MetaId -> TCM MetaNameSuggestion
- setMetaNameSuggestion :: MetaId -> MetaNameSuggestion -> TCM ()
- updateMetaVarRange :: MetaId -> Range -> TCM ()
- addInteractionPoint :: InteractionId -> MetaId -> TCM ()
- removeInteractionPoint :: InteractionId -> TCM ()
- getInteractionPoints :: TCM [InteractionId]
- getInteractionMetas :: TCM [MetaId]
- isInteractionMeta :: MetaId -> TCM Bool
- lookupInteractionId :: InteractionId -> TCM MetaId
- judgementInteractionId :: InteractionId -> TCM (Judgement Type MetaId)
- newMeta :: MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> TCM MetaId
- newMeta' :: MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> TCM MetaId
- getInteractionRange :: InteractionId -> TCM Range
- getMetaRange :: MetaId -> TCM Range
- getInteractionScope :: InteractionId -> TCM ScopeInfo
- withMetaInfo' :: MetaVariable -> TCM a -> TCM a
- withMetaInfo :: Closure Range -> TCM a -> TCM a
- getInstantiatedMetas :: TCM [MetaId]
- getOpenMetas :: TCM [MetaId]
- listenToMeta :: Listener -> MetaId -> TCM ()
- unlistenToMeta :: Listener -> MetaId -> TCM ()
- getMetaListeners :: MetaId -> TCM [Listener]
- clearMetaListeners :: MetaId -> TCM ()
- freezeMetas :: TCM ()
- unfreezeMetas :: TCM ()
- isFrozen :: MetaId -> TCM Bool
Documentation
dontAssignMetas :: TCM a -> TCM a
Switch off assignment of metas.
Get the meta store.
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
lookupMeta :: MetaId -> TCM MetaVariable
Lookup a meta variable
updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
getMetaPriority :: MetaId -> TCM MetaPriority
isSortMeta :: MetaId -> TCM Bool
getMetaType :: MetaId -> TCM Type
isInstantiatedMeta :: MetaId -> TCM Bool
createMetaInfo :: TCM MetaInfo
Create MetaInfo
in the current environment.
setValueMetaName :: Term -> MetaNameSuggestion -> TCM ()
setMetaNameSuggestion :: MetaId -> MetaNameSuggestion -> TCM ()
updateMetaVarRange :: MetaId -> Range -> TCM ()
addInteractionPoint :: InteractionId -> MetaId -> TCM ()
getInteractionMetas :: TCM [MetaId]
isInteractionMeta :: MetaId -> TCM Bool
Does the meta variable correspond to an interaction point?
newMeta :: MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> TCM MetaId
Generate new meta variable.
newMeta' :: MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation -> Judgement Type a -> TCM MetaId
Generate a new meta variable with some instantiation given.
For instance, the instantiation could be a PostponedTypeCheckingProblem
.
getMetaRange :: MetaId -> TCM Range
withMetaInfo' :: MetaVariable -> TCM a -> TCM a
withMetaInfo :: Closure Range -> TCM a -> TCM a
getOpenMetas :: TCM [MetaId]
listenToMeta :: Listener -> 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 :: Listener -> MetaId -> TCM ()
Unregister a listener.
getMetaListeners :: MetaId -> TCM [Listener]
Get the listeners to a meta.
clearMetaListeners :: MetaId -> TCM ()
freezeMetas :: TCM ()
Freeze all meta variables.
unfreezeMetas :: TCM ()