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

Safe Haskell | None

Agda.TypeChecking.Monad.MetaVars

Synopsis

- 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.

getMetaStore :: TCM MetaStore

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.

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

Does the meta variable correspond to an interaction point?

lookupInteractionId :: InteractionId -> TCM MetaId

judgementInteractionId :: InteractionId -> TCM (Judgement Type MetaId)

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`.

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 ()

`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 ()

isFrozen :: MetaId -> TCM Bool