Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- dontAssignMetas :: TCM a -> TCM a
- getMetaStore :: TCM MetaStore
- modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
- metasCreatedBy :: TCM a -> TCM (a, IntSet)
- lookupMeta' :: MetaId -> TCM (Maybe MetaVariable)
- lookupMeta :: MetaId -> TCM MetaVariable
- updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
- insertMetaVar :: MetaId -> MetaVariable -> TCM ()
- getMetaPriority :: MetaId -> TCM MetaPriority
- isSortMeta :: MetaId -> TCM Bool
- isSortMeta_ :: MetaVariable -> Bool
- getMetaType :: MetaId -> TCM Type
- getMetaContextArgs :: MetaVariable -> TCM Args
- getMetaTypeInContext :: MetaId -> TCM Type
- class IsInstantiatedMeta a where
- isInstantiatedMeta :: a -> TCM Bool
- isInstantiatedMeta' :: MetaId -> TCM (Maybe Term)
- allMetas :: TermLike a => a -> [MetaId]
- constraintMetas :: Constraint -> TCM (Set MetaId)
- createMetaInfo :: TCM MetaInfo
- createMetaInfo' :: RunMetaOccursCheck -> TCM MetaInfo
- setValueMetaName :: Term -> MetaNameSuggestion -> TCM ()
- getMetaNameSuggestion :: MetaId -> TCM MetaNameSuggestion
- setMetaNameSuggestion :: MetaId -> MetaNameSuggestion -> TCM ()
- setMetaArgInfo :: MetaId -> ArgInfo -> 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 :: MonadTCM tcm => tcm [InteractionId]
- getInteractionMetas :: TCM [MetaId]
- getInteractionIdsAndMetas :: TCM [(InteractionId, MetaId)]
- isInteractionMeta :: MetaId -> TCM (Maybe InteractionId)
- lookupInteractionPoint :: MonadTCM tcm => InteractionId -> tcm InteractionPoint
- lookupInteractionId :: InteractionId -> TCM MetaId
- lookupInteractionMeta :: InteractionId -> TCM (Maybe MetaId)
- lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
- newMeta :: Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId
- newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId
- getInteractionRange :: MonadTCM tcm => InteractionId -> tcm Range
- getMetaRange :: MetaId -> TCM Range
- getInteractionScope :: InteractionId -> TCM ScopeInfo
- withMetaInfo' :: MetaVariable -> TCM a -> TCM a
- withMetaInfo :: Closure Range -> TCM a -> TCM a
- getMetaVariableSet :: TCM IntSet
- getMetaVariables :: (MetaVariable -> Bool) -> TCM [MetaId]
- 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
- unfreezeMeta :: a -> TCM ()
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, IntSet) Source #
Run a computation and record which new metas it created.
lookupMeta' :: MetaId -> TCM (Maybe MetaVariable) Source #
Lookup a meta variable.
lookupMeta :: MetaId -> TCM MetaVariable Source #
updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM () Source #
Update the information associated with a meta variable.
insertMetaVar :: MetaId -> MetaVariable -> TCM () Source #
Insert a new meta variable with associated information into the meta store.
getMetaPriority :: MetaId -> TCM MetaPriority Source #
isSortMeta_ :: MetaVariable -> Bool Source #
getMetaContextArgs :: MetaVariable -> TCM Args Source #
Compute the context variables that a meta should be applied to, accounting for pruning.
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.
isInstantiatedMeta :: a -> TCM Bool Source #
Instances
IsInstantiatedMeta MetaId Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars | |
IsInstantiatedMeta LevelAtom Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars | |
IsInstantiatedMeta PlusLevel Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars | |
IsInstantiatedMeta Level Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars | |
IsInstantiatedMeta Term Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars | |
IsInstantiatedMeta a => IsInstantiatedMeta [a] Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: [a] -> TCM Bool Source # | |
IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars | |
IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars | |
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source # | Does not worry about raising. |
Defined in Agda.TypeChecking.Monad.MetaVars |
allMetas :: TermLike a => a -> [MetaId] Source #
Returns every meta-variable occurrence in the given type, except
for those in Term
s.
constraintMetas :: Constraint -> TCM (Set MetaId) Source #
Returns all metavariables in a constraint. Slightly complicated by the fact that blocked terms are represented by two meta variables. To find the second one we need to look up the meta listeners for the one in the UnBlock constraint.
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 :: MonadTCM tcm => 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 :: MonadTCM tcm => 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 :: Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId Source #
Generate new meta variable.
newMeta' :: MetaInstantiation -> Frozen -> 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 :: MonadTCM tcm => InteractionId -> tcm Range Source #
Get the Range'
for an interaction point.
withMetaInfo' :: MetaVariable -> TCM a -> TCM a Source #
getMetaVariables :: (MetaVariable -> Bool) -> TCM [MetaId] 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.
unfreezeMeta :: a -> TCM () Source #