Agda.TypeChecking.Monad.MetaVars

Documentation

data MetaKind

Various kinds of metavariables.

Constructors

Records

Meta variables of record type.

SingletonRecords

Meta variables of "hereditarily singleton" record type.

Levels

Meta variables of level type, if type-in-type is activated.

Instances

Bounded MetaKind

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

minBound :: MetaKind

maxBound :: MetaKind

Enum MetaKind

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

succ :: MetaKind -> MetaKind

pred :: MetaKind -> MetaKind

toEnum :: Int -> MetaKind

fromEnum :: MetaKind -> Int

enumFrom :: MetaKind -> [MetaKind]

enumFromThen :: MetaKind -> MetaKind -> [MetaKind]

enumFromTo :: MetaKind -> MetaKind -> [MetaKind]

enumFromThenTo :: MetaKind -> MetaKind -> MetaKind -> [MetaKind]

Show MetaKind

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

showsPrec :: Int -> MetaKind -> ShowS

show :: MetaKind -> String

showList :: [MetaKind] -> ShowS

Eq MetaKind

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

(==) :: MetaKind -> MetaKind -> Bool

(/=) :: MetaKind -> MetaKind -> Bool

allMetaKinds :: [MetaKind]

All possible metavariable kinds.

data KeepMetas

Constructors

KeepMetas

RollBackMetas

class (MonadConstraint m, MonadReduce m, MonadAddContext m, MonadTCEnv m, ReadTCState m, HasBuiltins m, HasConstInfo m, MonadDebug m) => MonadMetaSolver (m :: Type -> Type) where

Monad service class for creating, solving and eta-expanding of metavariables.

Methods

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

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

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()

Assign to an open metavar which may not be frozen. First check that metavar args are in pattern fragment. Then do extended occurs check on given thing.

Assignment is aborted by throwing a PatternErr via a call to patternViolation. This error is caught by catchConstraint during equality checking (compareAtom) and leads to restoration of the original constraints.

assignTerm' :: MetaId -> [Arg ArgName] -> Term -> m ()

Directly instantiate the metavariable. Skip pattern check, occurs check and frozen check. Used for eta expanding frozen metas.

etaExpandMeta :: [MetaKind] -> MetaId -> m ()

Eta-expand a local meta-variable, if it is of the specified kind. Don't do anything if the meta-variable is a blocked term.

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

Update the status of the metavariable

speculateMetas :: m () -> m KeepMetas -> m ()

'speculateMetas fallback m' speculatively runs m, but if the result is RollBackMetas any changes to metavariables are rolled back and fallback is run instead.

Instances

MonadMetaSolver TCM

Defined in Agda.TypeChecking.MetaVars

Methods

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

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()

assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM ()

etaExpandMeta :: [MetaKind] -> MetaId -> TCM ()

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

speculateMetas :: TCM () -> TCM KeepMetas -> TCM ()

(PureTCM m, MonadBlock m) => MonadMetaSolver (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> PureConversionT m ()

assignTerm' :: MetaId -> [Arg ArgName] -> Term -> PureConversionT m ()

etaExpandMeta :: [MetaKind] -> MetaId -> PureConversionT m ()

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m ()

speculateMetas :: PureConversionT m () -> PureConversionT m KeepMetas -> PureConversionT m ()

MonadMetaSolver m => MonadMetaSolver (ReaderT r m)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> ReaderT r m MetaId

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> ReaderT r m ()

assignTerm' :: MetaId -> [Arg ArgName] -> Term -> ReaderT r m ()

etaExpandMeta :: [MetaKind] -> MetaId -> ReaderT r m ()

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> ReaderT r m ()

speculateMetas :: ReaderT r m () -> ReaderT r m KeepMetas -> ReaderT r m ()

dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a

Switch off assignment of metas.

isRemoteMeta :: ReadTCState m => m (MetaId -> Bool)

Is the meta-variable from another top-level module?

nextLocalMeta :: ReadTCState m => m MetaId

If another meta-variable is created, then it will get this MetaId (unless the state is changed too much, for instance by setTopLevelModule).

data LocalMetaStores

Pairs of local meta-stores.

Constructors

LocalMetaStores

Fields

• openMetas :: LocalMetaStore

  A MetaStore containing open meta-variables.

• solvedMetas :: LocalMetaStore

  A MetaStore containing instantiated meta-variables.

metasCreatedBy :: ReadTCState m => m a -> m (a, LocalMetaStores)

Run a computation and record which new metas it created.

lookupLocalMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)

Find information about the given local meta-variable, if any.

lookupLocalMeta :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m MetaVariable

Find information about the given local meta-variable.

lookupMeta :: ReadTCState m => MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))

Find information about the (local or remote) meta-variable, if any.

If no meta-variable is found, then the reason could be that the dead-code elimination (eliminateDeadCode) failed to find the meta-variable, perhaps because some NamesIn instance is incorrectly defined.

lookupMetaInstantiation :: ReadTCState m => MetaId -> m MetaInstantiation

Find the meta-variable's instantiation.

lookupMetaJudgement :: ReadTCState m => MetaId -> m (Judgement MetaId)

Find the meta-variable's judgement.

lookupMetaModality :: ReadTCState m => MetaId -> m Modality

Find the meta-variable's modality.

metaType :: ReadTCState m => MetaId -> m Type

The type of a term or sort meta-variable.

updateMetaVarTCM :: HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()

Update the information associated with a local meta-variable.

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

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

getMetaPriority :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m MetaPriority

Returns the MetaPriority of the given local meta-variable.

isSortMeta :: ReadTCState m => MetaId -> m Bool

isSortMeta_ :: MetaVariable -> Bool

isSortJudgement :: Judgement a -> Bool

getMetaType :: ReadTCState m => MetaId -> m Type

getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args

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

getMetaTypeInContext :: (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m, MonadTCEnv m, ReadTCState m) => MetaId -> m Type

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

isGeneralizableMeta :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m DoGeneralize

Is it a local meta-variable that might be generalized?

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 :: (MonadFail m, ReadTCState m) => a -> m Bool

Instances

IsInstantiatedMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool

IsInstantiatedMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Level -> m Bool

IsInstantiatedMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool

IsInstantiatedMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Term -> m Bool

IsInstantiatedMeta a => IsInstantiatedMeta (Arg a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Arg a -> m Bool

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a)

Does not worry about raising.

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Abs a -> m Bool

IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Maybe a -> m Bool

IsInstantiatedMeta a => IsInstantiatedMeta [a]

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => [a] -> m Bool

isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term)

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. This is used for the purpose of deciding if a metavariable is constrained or if it can be generalized over (see Agda.TypeChecking.Generalize).

createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo

Create MetaInfo in the current environment.

createMetaInfo' :: (MonadTCEnv m, ReadTCState m) => RunMetaOccursCheck -> m MetaInfo

setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m ()

getMetaNameSuggestion :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m MetaNameSuggestion

setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()

setMetaGeneralizableArgInfo :: MonadMetaSolver m => MetaId -> ArgInfo -> m ()

Change the ArgInfo that will be used when generalizing over this local meta-variable.

updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()

setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m ()

Query and manipulate interaction points.

class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints (m :: Type -> Type) where

Minimal complete definition

Nothing

Methods

freshInteractionId :: m InteractionId

default freshInteractionId :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadInteractionPoints n, t n ~ m) => m InteractionId

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()

default modifyInteractionPoints :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadInteractionPoints n, t n ~ m) => (InteractionPoints -> InteractionPoints) -> m ()

Instances

MonadInteractionPoints AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

freshInteractionId :: AbsToCon InteractionId

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> AbsToCon ()

MonadInteractionPoints TCM

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

freshInteractionId :: TCM InteractionId

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

(PureTCM m, MonadBlock m) => MonadInteractionPoints (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

freshInteractionId :: PureConversionT m InteractionId

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> PureConversionT m ()

MonadInteractionPoints m => MonadInteractionPoints (IdentityT m)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

freshInteractionId :: IdentityT m InteractionId

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> IdentityT m ()

MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

freshInteractionId :: ReaderT r m InteractionId

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> ReaderT r m ()

MonadInteractionPoints m => MonadInteractionPoints (StateT s m)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

freshInteractionId :: StateT s m InteractionId

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> StateT s m ()

registerInteractionPoint :: MonadInteractionPoints m => Bool -> Range -> Maybe Nat -> m 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. Issue 3000: Don't consider solved interaction points.

O(n): linear in the number of registered interaction points.

connectInteractionPoint :: MonadInteractionPoints m => InteractionId -> MetaId -> m ()

Hook up a local meta-variable to an interaction point.

removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m ()

Mark an interaction point as solved.

getInteractionPoints :: ReadTCState m => m [InteractionId]

Get a list of interaction ids.

getInteractionMetas :: ReadTCState m => m [MetaId]

Get all metas that correspond to unsolved interaction ids.

getUniqueMetasRanges :: (HasCallStack, MonadDebug m, ReadTCState m) => [MetaId] -> m [Range]

getUnsolvedMetas :: (HasCallStack, MonadDebug m, ReadTCState m) => m [Range]

getUnsolvedInteractionMetas :: (HasCallStack, MonadDebug m, ReadTCState m) => m [Range]

getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId, MetaId)]

Get all metas that correspond to unsolved interaction ids.

isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId)

Does the meta variable correspond to an interaction point?

Time: O(log n) where n is the number of interaction metas.

lookupInteractionPoint :: (MonadFail m, ReadTCState m, MonadError TCErr m) => InteractionId -> m InteractionPoint

Get the information associated to an interaction point.

lookupInteractionId :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m MetaId

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

lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId)

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

lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId

newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId

Generate new meta variable.

newMetaTCM' :: 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 :: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) => InteractionId -> m Range

Get the Range for an interaction point.

getMetaRange :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Range

Get the Range for a local meta-variable.

getInteractionScope :: (MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m ScopeInfo

withMetaInfo' :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => MetaVariable -> m a -> m a

withMetaInfo :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => Closure Range -> m a -> m a

withInteractionId :: (MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m, MonadTrace m) => InteractionId -> m a -> m a

withMetaId :: (HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m, ReadTCState m) => MetaId -> m a -> m a

getOpenMetas :: ReadTCState m => m [MetaId]

isOpenMeta :: MetaInstantiation -> Bool

listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()

listenToMeta l m: register l as a listener to m. This is done when the type of l is blocked by m.

unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()

Unregister a listener.

getMetaListeners :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m [Listener]

Get the listeners for a local meta-variable.

clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()

etaExpandMetaSafe :: MonadMetaSolver m => MetaId -> m ()

Do safe eta-expansions for meta (SingletonRecords,Levels).

etaExpandListeners :: MonadMetaSolver m => MetaId -> m ()

Eta expand metavariables listening on the current meta.

wakeupListener :: MonadMetaSolver m => Listener -> m ()

Wake up a meta listener and let it do its thing

solveAwakeConstraints :: MonadConstraint m => m ()

solveAwakeConstraints' :: MonadConstraint m => Bool -> m ()

Freezing and unfreezing metas.

freezeMetas :: MonadTCState m => LocalMetaStore -> m (Set MetaId)

Freeze the given meta-variables (but only if they are open) and return those that were not already frozen.

unfreezeMetas :: TCM ()

Thaw all open meta variables.

isFrozen :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Bool

withFrozenMetas :: (MonadMetaSolver m, MonadTCState m) => m a -> m a

class UnFreezeMeta a where

Unfreeze a meta and its type if this is a meta again. Does not unfreeze deep occurrences of meta-variables or remote meta-variables.

Methods

unfreezeMeta :: MonadMetaSolver m => a -> m ()

Instances

UnFreezeMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => MetaId -> m ()

UnFreezeMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Level -> m ()

UnFreezeMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m ()

UnFreezeMeta Sort

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Sort -> m ()

UnFreezeMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Term -> m ()

UnFreezeMeta Type

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Type -> m ()

UnFreezeMeta a => UnFreezeMeta (Abs a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Abs a -> m ()

UnFreezeMeta a => UnFreezeMeta [a]

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => [a] -> m ()