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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.MetaVars

Contents

- Query and manipulate interaction points.
- Freezing and unfreezing metas.

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, Monoid m) => (MetaId -> m) -> a -> m
- allMetasList :: TermLike a => a -> [MetaId]
- noMetas :: TermLike a => a -> Bool
- firstMeta :: TermLike a => a -> Maybe 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.

modifyMetaStore :: (MetaStore -> MetaStore) -> TCM () Source #

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 :: MetaId -> TCM Bool Source #

isSortMeta_ :: MetaVariable -> Bool Source #

getMetaType :: MetaId -> TCM Type 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.

Methods

isInstantiatedMeta :: a -> TCM Bool Source #

Instances

IsInstantiatedMeta MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: MetaId -> TCM Bool Source #
IsInstantiatedMeta LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: LevelAtom -> TCM Bool Source #
IsInstantiatedMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: PlusLevel -> TCM Bool Source #
IsInstantiatedMeta Level Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Level -> TCM Bool Source #
IsInstantiatedMeta Term Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Term -> TCM Bool Source #
IsInstantiatedMeta a => IsInstantiatedMeta [a] Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: [a] -> TCM Bool Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Maybe a -> TCM Bool Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Arg a -> TCM Bool Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source # | Does not worry about raising.
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Abs a -> TCM Bool Source #

isInstantiatedMeta' :: MetaId -> TCM (Maybe Term) Source #

allMetas :: (TermLike a, Monoid m) => (MetaId -> m) -> a -> m Source #

Returns every meta-variable occurrence in the given type, except for those in `Term`s.

allMetasList :: TermLike a => a -> [MetaId] Source #

Returns `allMetas` in a list. `allMetasList = allMetas (:[])`.

Note: this resulting list is computed via difference lists. Thus, use this function if you actually need the whole list of metas. Otherwise, use `allMetas` with a suitable monoid.

noMetas :: TermLike a => a -> Bool Source #

`True` if thing contains no metas. `noMetas = null . allMetasList`.

firstMeta :: TermLike a => a -> Maybe MetaId Source #

Returns the first meta it find in the thing, if any. `firstMeta == headMaybe . allMetasList`.

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.

createMetaInfo :: TCM MetaInfo Source #

Create `MetaInfo` in the current environment.

createMetaInfo' :: RunMetaOccursCheck -> TCM MetaInfo Source #

setValueMetaName :: Term -> MetaNameSuggestion -> TCM () Source #

getMetaNameSuggestion :: MetaId -> TCM MetaNameSuggestion Source #

setMetaNameSuggestion :: MetaId -> MetaNameSuggestion -> TCM () Source #

setMetaArgInfo :: MetaId -> ArgInfo -> TCM () Source #

updateMetaVarRange :: MetaId -> Range -> 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.

lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId Source #

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.

getMetaRange :: MetaId -> TCM Range Source #

Get the `Range'` for a meta variable.

getInteractionScope :: InteractionId -> TCM ScopeInfo Source #

withMetaInfo' :: MetaVariable -> TCM a -> TCM a Source #

withMetaInfo :: Closure Range -> TCM a -> TCM a Source #

getMetaVariableSet :: TCM IntSet 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`.

unlistenToMeta :: Listener -> MetaId -> TCM () Source #

Unregister a listener.

getMetaListeners :: MetaId -> TCM [Listener] Source #

Get the listeners to a meta.

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.

isFrozen :: MetaId -> TCM Bool Source #

class UnFreezeMeta a where Source #

Unfreeze meta and its type if this is a meta again. Does not unfreeze deep occurrences of metas.

Methods

unfreezeMeta :: a -> TCM () Source #

Instances

UnFreezeMeta MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MetaId -> TCM () Source #
UnFreezeMeta LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: LevelAtom -> TCM () Source #
UnFreezeMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: PlusLevel -> TCM () Source #
UnFreezeMeta Level Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Level -> TCM () Source #
UnFreezeMeta Sort Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Sort -> TCM () Source #
UnFreezeMeta Type Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Type -> TCM () Source #
UnFreezeMeta Term Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Term -> TCM () Source #
UnFreezeMeta a => UnFreezeMeta [a] Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: [a] -> TCM () Source #
UnFreezeMeta a => UnFreezeMeta (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Abs a -> TCM () Source #