ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Monad.MetaVars

3 types
4 classes
72 values

PackageAgda-2.7.0.1
Exports79
LanguageHaskell2010
LicenceMIT
SourceMetaVars.hs

datadata MetaClass

Various classes 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.

Instances4Bounded, Enum, Eq, Show

Bounded MetaClassDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
Enum MetaClassDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
Eq MetaClassDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
Show MetaClassDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars

valueallMetaClasses :: [MetaClass]

All possible metavariable classes.

datadata KeepMetas

KeepMetas RollBackMetas

class

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' :: 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 :: [MetaClass] -> MetaId -> m ()
Eta-expand a local meta-variable, if it is of the specified class. 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.

Instances3MonadMetaSolver

MonadMetaSolver TCMDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars · orphan
(PureTCM m, MonadBlock m) => MonadMetaSolver (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure
MonadMetaSolver m => MonadMetaSolver (ReaderT r m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars

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

Switch off assignment of metas.

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

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

valuenextLocalMeta :: 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).

datadata LocalMetaStores

Pairs of local meta-stores.

Constructors

LocalMetaStores
- openMetas :: LocalMetaStore
  A MetaStore containing open meta-variables.
- solvedMetas :: LocalMetaStore
  A MetaStore containing instantiated meta-variables.

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

Run a computation and record which new metas it created.

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

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

valuelookupLocalMeta

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

Find information about the given local meta-variable.

valuelookupMeta

:: 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.

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

Find the meta-variable's instantiation.

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

Find the meta-variable's judgement.

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

Find the meta-variable's modality.

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

The type of a term or sort meta-variable.

valueupdateMetaVarTCM

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

Update the information associated with a local meta-variable.

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

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

valuegetMetaPriority

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

Returns the MetaPriority of the given local meta-variable.

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

valueisSortMeta_ :: MetaVariable -> Bool

valueisSortJudgement :: Judgement a -> Bool

valuemetaInstantiationToMetaKind :: MetaInstantiation -> MetaKind

If a meta variable is still open, what is its kind?

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

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

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

valuegetMetaTypeInContext

:: (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.

valueisGeneralizableMeta

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

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

classclass 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

Instances8IsInstantiatedMeta, …

IsInstantiatedMeta MetaIdDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
IsInstantiatedMeta LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
IsInstantiatedMeta PlusLevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
IsInstantiatedMeta TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
IsInstantiatedMeta a => IsInstantiatedMeta (Arg a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
Does not worry about raising.
IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
IsInstantiatedMeta a => IsInstantiatedMeta [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars

valueisInstantiatedMeta'

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

valueconstraintMetas :: 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).

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

Create MetaInfo in the current environment.

valuecreateMetaInfo'

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

valuegetMetaNameSuggestion

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

valuesetMetaNameSuggestion

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

valuesetMetaGeneralizableArgInfo

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

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

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

valuesetMetaOccursCheck

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

Query and manipulate interaction points.

36 declarations

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

Methods

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

Instances6MonadInteractionPoints

MonadInteractionPoints AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadInteractionPoints TCMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
(PureTCM m, MonadBlock m) => MonadInteractionPoints (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure
MonadInteractionPoints m => MonadInteractionPoints (IdentityT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
MonadInteractionPoints m => MonadInteractionPoints (StateT s m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars

valueregisterInteractionPoint

valuefindInteractionPoint_ :: 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.

valueconnectInteractionPoint

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

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

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

Mark an interaction point as solved.

valuegetInteractionPoints :: ReadTCState m => m [InteractionId]

Get a list of interaction ids.

valuegetInteractionMetas :: ReadTCState m => m [MetaId]

Get all metas that correspond to unsolved interaction ids.

valuegetUniqueMetasRanges

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

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

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

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

Get all metas that correspond to unsolved interaction ids.

valueisInteractionMeta :: 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.

valuelookupInteractionPoint

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

Get the information associated to an interaction point.

valuelookupInteractionId

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

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

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

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

valuelookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId

valuenewMeta

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

Generate new meta variable.

valuenewMetaTCM'

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

valuegetInteractionRange

:: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m)
=> InteractionId
-> m Range

Get the Range for an interaction point.

valuegetMetaRange

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

Get the Range for a local meta-variable.

valuegetInteractionScope

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

valuewithMetaInfo'

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

valuewithMetaInfo

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

valuewithInteractionId

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

valuewithMetaId

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

valuegetOpenMetas :: ReadTCState m => m [MetaId]

valueisOpenMeta :: MetaInstantiation -> Bool

valuelistenToMeta :: 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.

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

Unregister a listener.

valuegetMetaListeners

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

Get the listeners for a local meta-variable.

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

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

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

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

Eta expand metavariables listening on the current meta.

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

Wake up a meta listener and let it do its thing

valuesolveAwakeConstraints :: MonadConstraint m => m ()

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

Freezing and unfreezing metas.

5 declarations

valuefreezeMetas :: 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.

valueunfreezeMetas :: TCM ()

Thaw all open meta variables.

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

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

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

Instances8UnFreezeMeta, …

UnFreezeMeta MetaIdDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
UnFreezeMeta LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
UnFreezeMeta PlusLevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
UnFreezeMeta SortDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
UnFreezeMeta TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
UnFreezeMeta TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
UnFreezeMeta a => UnFreezeMeta (Abs a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars
UnFreezeMeta a => UnFreezeMeta [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.MetaVars