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 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' :: MonadMetaSolver m => 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 metavariable, if it is of the specified kind. Don't do anything if the metavariable 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 ()

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

Switch off assignment of metas.

getMetaStore :: ReadTCState m => m MetaStore

Get the meta store.

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

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

Run a computation and record which new metas it created.

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

Lookup a meta variable.

lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable

metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type

Type of a term or sort meta.

updateMetaVarTCM :: 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 :: (MonadFail m, ReadTCState m) => MetaId -> m MetaPriority

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

isSortMeta_ :: MetaVariable -> Bool

getMetaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type

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

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

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

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

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

Is it a meta 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 :: (MonadFail 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 meta.

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

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

Query and manipulate interaction points.

class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints m where

Minimal complete definition

Nothing

Methods

freshInteractionId :: m InteractionId

default freshInteractionId :: (MonadTrans t, MonadInteractionPoints n, t n ~ m) => m InteractionId

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

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

Instances

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 :: forall m. 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 meta variable to 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 :: (MonadFail m, ReadTCState m) => [MetaId] -> m [Range]

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

getUnsolvedInteractionMetas :: (MonadFail 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 :: (MonadFail m, ReadTCState m) => MetaId -> m Range

Get the Range' for a meta variable.

getInteractionScope :: (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 :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m, MonadTrace m) => InteractionId -> m a -> m a

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

getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId]

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 :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener]

Get the listeners to a meta.

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

Freezing and unfreezing metas.

freezeMetas :: MetaStore -> TCM IntSet

Freeze the given meta-variables and return those that were not already frozen.

unfreezeMetas :: TCM ()

Thaw all meta variables.

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