| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.MetaVars
- dontAssignMetas :: TCM a -> TCM a
- getMetaStore :: TCM MetaStore
- modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
- metasCreatedBy :: TCM a -> TCM (a, Set MetaId)
- lookupMeta :: MetaId -> TCM MetaVariable
- updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
- getMetaPriority :: MetaId -> TCM MetaPriority
- isSortMeta :: MetaId -> TCM Bool
- isSortMeta_ :: MetaVariable -> Bool
- getMetaType :: MetaId -> TCM Type
- getMetaTypeInContext :: MetaId -> TCM Type
- class IsInstantiatedMeta a where
- isInstantiatedMeta' :: MetaId -> TCM (Maybe Term)
- allMetas :: TermLike a => a -> [MetaId]
- createMetaInfo :: TCM MetaInfo
- createMetaInfo' :: RunMetaOccursCheck -> TCM MetaInfo
- setValueMetaName :: Term -> MetaNameSuggestion -> TCM ()
- getMetaNameSuggestion :: MetaId -> TCM MetaNameSuggestion
- setMetaNameSuggestion :: MetaId -> MetaNameSuggestion -> TCM ()
- updateMetaVarRange :: MetaId -> Range -> TCM ()
- setMetaOccursCheck :: MetaId -> RunMetaOccursCheck -> TCM ()
- modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()
- registerInteractionPoint :: Bool -> Range -> Maybe Nat -> TCM InteractionId
- findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
- connectInteractionPoint :: InteractionId -> MetaId -> TCM ()
- removeInteractionPoint :: InteractionId -> TCM ()
- getInteractionPoints :: TCM [InteractionId]
- getInteractionMetas :: TCM [MetaId]
- getInteractionIdsAndMetas :: TCM [(InteractionId, MetaId)]
- isInteractionMeta :: MetaId -> TCM (Maybe InteractionId)
- lookupInteractionPoint :: InteractionId -> TCM InteractionPoint
- lookupInteractionId :: InteractionId -> TCM MetaId
- lookupInteractionMeta :: InteractionId -> TCM (Maybe MetaId)
- lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
- newMeta :: MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId
- newMeta' :: MetaInstantiation -> MetaInfo -> MetaPriority -> Permutation -> Judgement 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]
- isOpenMeta :: MetaInstantiation -> Bool
- listenToMeta :: Listener -> MetaId -> TCM ()
- unlistenToMeta :: Listener -> MetaId -> TCM ()
- getMetaListeners :: MetaId -> TCM [Listener]
- clearMetaListeners :: MetaId -> TCM ()
- withFreezeMetas :: TCM a -> TCM a
- freezeMetas :: TCM [MetaId]
- freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId]
- unfreezeMetas :: TCM ()
- unfreezeMetas' :: (MetaId -> Bool) -> TCM ()
- isFrozen :: MetaId -> TCM Bool
- class UnFreezeMeta a where
Documentation
dontAssignMetas :: TCM a -> TCM a Source #
Switch off assignment of metas.
getMetaStore :: TCM MetaStore Source #
Get the meta store.
metasCreatedBy :: TCM a -> TCM (a, Set MetaId) Source #
Run a computation and record which new metas it created.
lookupMeta :: MetaId -> TCM MetaVariable Source #
Lookup a meta variable
updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM () Source #
getMetaPriority :: MetaId -> TCM MetaPriority Source #
isSortMeta_ :: MetaVariable -> Bool Source #
getMetaTypeInContext :: MetaId -> TCM Type Source #
Given a meta, return the type applied to the current context.
class IsInstantiatedMeta a where Source #
Check whether all metas are instantiated. Precondition: argument is a meta (in some form) or a list of metas.
Minimal complete definition
Methods
isInstantiatedMeta :: a -> TCM Bool Source #
Instances
| IsInstantiatedMeta MetaId Source # | |
| IsInstantiatedMeta LevelAtom Source # | |
| IsInstantiatedMeta PlusLevel Source # | |
| IsInstantiatedMeta Level Source # | |
| IsInstantiatedMeta Term Source # | |
| IsInstantiatedMeta a => IsInstantiatedMeta [a] Source # | |
| IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) Source # | |
| IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # | |
| IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source # | Does not worry about raising. |
allMetas :: TermLike a => a -> [MetaId] Source #
Returns every meta-variable occurrence in the given type, except
for those in Sorts.
setValueMetaName :: Term -> MetaNameSuggestion -> TCM () Source #
setMetaNameSuggestion :: MetaId -> MetaNameSuggestion -> TCM () Source #
setMetaOccursCheck :: MetaId -> RunMetaOccursCheck -> TCM () Source #
Query and manipulate interaction points.
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM () Source #
registerInteractionPoint :: Bool -> Range -> Maybe Nat -> TCM InteractionId Source #
Register an interaction point during scope checking. If there is no interaction id yet, create one.
findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId Source #
Find an interaction point by Range by searching the whole map.
O(n): linear in the number of registered interaction points.
connectInteractionPoint :: InteractionId -> MetaId -> TCM () Source #
Hook up meta variable to interaction point.
removeInteractionPoint :: InteractionId -> TCM () Source #
Mark an interaction point as solved.
getInteractionPoints :: TCM [InteractionId] Source #
Get a list of interaction ids.
getInteractionMetas :: TCM [MetaId] Source #
Get all metas that correspond to unsolved interaction ids.
getInteractionIdsAndMetas :: TCM [(InteractionId, MetaId)] Source #
Get all metas that correspond to unsolved 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.
lookupInteractionMeta :: InteractionId -> TCM (Maybe MetaId) Source #
Check whether an interaction id is already associated with a meta variable.
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.
withMetaInfo' :: MetaVariable -> TCM a -> TCM a Source #
getInstantiatedMetas :: TCM [MetaId] Source #
getOpenMetas :: TCM [MetaId] Source #
isOpenMeta :: MetaInstantiation -> Bool Source #
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.
clearMetaListeners :: MetaId -> TCM () Source #
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.
freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId] Source #
Freeze some 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
Methods
unfreezeMeta :: a -> TCM () Source #
Instances