Agda.TypeChecking.Monad.MetaVars

Documentation

dontAssignMetas :: TCM a -> TCM a

Switch off assignment of metas.

getMetaStore :: TCM MetaStore

Get the meta store.

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

metasCreatedBy :: TCM a -> TCM (a, IntSet)

Run a computation and record which new metas it created.

lookupMeta' :: MetaId -> TCM (Maybe MetaVariable)

Lookup a meta variable.

lookupMeta :: MetaId -> TCM MetaVariable

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()

Update the information associated with a meta variable.

insertMetaVar :: MetaId -> MetaVariable -> TCM ()

Insert a new meta variable with associated information into the meta store.

getMetaPriority :: MetaId -> TCM MetaPriority

isSortMeta :: MetaId -> TCM Bool

isSortMeta_ :: MetaVariable -> Bool

getMetaType :: MetaId -> TCM Type

getMetaContextArgs :: MetaVariable -> TCM Args

Compute the context variables that a meta should be applied to, accounting for pruning.

getMetaTypeInContext :: MetaId -> TCM Type

Given a meta, return the type applied to the current context.

class IsInstantiatedMeta a where

Check whether all metas are instantiated. Precondition: argument is a meta (in some form) or a list of metas.

Methods

isInstantiatedMeta :: a -> TCM Bool

Instances

IsInstantiatedMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: MetaId -> TCM Bool

IsInstantiatedMeta LevelAtom

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: LevelAtom -> TCM Bool

IsInstantiatedMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: PlusLevel -> TCM Bool

IsInstantiatedMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Level -> TCM Bool

IsInstantiatedMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Term -> TCM Bool

IsInstantiatedMeta a => IsInstantiatedMeta [a]

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: [a] -> TCM Bool

IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Maybe a -> TCM Bool

IsInstantiatedMeta a => IsInstantiatedMeta (Arg a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Arg a -> TCM Bool

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a)

Does not worry about raising.

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Abs a -> TCM Bool

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

allMetas :: TermLike a => a -> [MetaId]

Returns every meta-variable occurrence in the given type, except for those in Terms.

constraintMetas :: Constraint -> TCM (Set MetaId)

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

Create MetaInfo in the current environment.

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

Query and manipulate interaction points.

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()

registerInteractionPoint :: Bool -> Range -> Maybe Nat -> TCM InteractionId

Register an interaction point during scope checking. If there is no interaction id yet, create one.

findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId

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

Hook up meta variable to interaction point.

removeInteractionPoint :: InteractionId -> TCM ()

Mark an interaction point as solved.

getInteractionPoints :: MonadTCM tcm => tcm [InteractionId]

Get a list of interaction ids.

getInteractionMetas :: TCM [MetaId]

Get all metas that correspond to unsolved interaction ids.

getInteractionIdsAndMetas :: TCM [(InteractionId, MetaId)]

Get all metas that correspond to unsolved interaction ids.

isInteractionMeta :: MetaId -> TCM (Maybe InteractionId)

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

Get the information associated to an interaction point.

lookupInteractionId :: InteractionId -> TCM MetaId

Get MetaId for an interaction point. Precondition: interaction point is connected.

lookupInteractionMeta :: InteractionId -> TCM (Maybe MetaId)

Check whether an interaction id is already associated with a meta variable.

lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId

newMeta :: Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId

Generate new meta variable.

newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId

Generate a new meta variable with some instantiation given. For instance, the instantiation could be a PostponedTypeCheckingProblem.

getInteractionRange :: MonadTCM tcm => InteractionId -> tcm Range

Get the Range' for an interaction point.

getMetaRange :: MetaId -> TCM Range

Get the Range' for a meta variable.

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

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

Freezing and unfreezing metas.

withFreezeMetas :: TCM a -> TCM a

Freeze all so far unfrozen metas for the duration of the given computation.

freezeMetas :: TCM [MetaId]

Freeze all meta variables and return the list of metas that got frozen.

freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId]

Freeze some meta variables and return the list of metas that got frozen.

unfreezeMetas :: TCM ()

Thaw all meta variables.

unfreezeMetas' :: (MetaId -> Bool) -> TCM ()

Thaw some metas, as indicated by the passed condition.

isFrozen :: MetaId -> TCM Bool

class UnFreezeMeta a where

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

Methods

unfreezeMeta :: a -> TCM ()

Instances

UnFreezeMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MetaId -> TCM ()

UnFreezeMeta LevelAtom

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: LevelAtom -> TCM ()

UnFreezeMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: PlusLevel -> TCM ()

UnFreezeMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Level -> TCM ()

UnFreezeMeta Sort

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Sort -> TCM ()

UnFreezeMeta Type

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Type -> TCM ()

UnFreezeMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Term -> TCM ()

UnFreezeMeta a => UnFreezeMeta [a]

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: [a] -> TCM ()

UnFreezeMeta a => UnFreezeMeta (Abs a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Abs a -> TCM ()