Agda-2.8.0: 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

- data MetaClass
  - = Records
  - | SingletonRecords
  - | Levels
- allMetaClasses :: [MetaClass]
- data KeepMetas
  - = KeepMetas
  - | RollBackMetas
- class (MonadConstraint m, MonadReduce m, MonadAddContext m, MonadTCEnv m, ReadTCState m, HasBuiltins m, HasConstInfo m, MonadDebug m) => MonadMetaSolver (m :: Type -> Type) where
  - newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
  - assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
  - assignTerm' :: MetaId -> [Arg ArgName] -> Term -> m ()
  - etaExpandMeta :: [MetaClass] -> MetaId -> m ()
  - updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m ()
  - speculateMetas :: m () -> m KeepMetas -> m ()
- dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a
- isRemoteMeta :: ReadTCState m => m (MetaId -> Bool)
- nextLocalMeta :: ReadTCState m => m MetaId
- data LocalMetaStores = LocalMetaStores {
  - openMetas :: LocalMetaStore
  - solvedMetas :: LocalMetaStore
  }
- metasCreatedBy :: ReadTCState m => m a -> m (a, LocalMetaStores)
- lookupLocalMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
- lookupLocalMeta :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m MetaVariable
- lookupMeta :: ReadTCState m => MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
- lookupMetaInstantiation :: ReadTCState m => MetaId -> m MetaInstantiation
- lookupMetaJudgement :: ReadTCState m => MetaId -> m (Judgement MetaId)
- lookupMetaModality :: ReadTCState m => MetaId -> m Modality
- metaType :: ReadTCState m => MetaId -> m Type
- updateMetaVarTCM :: HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
- insertMetaVar :: MetaId -> MetaVariable -> TCM ()
- getMetaPriority :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m MetaPriority
- isSortMeta :: ReadTCState m => MetaId -> m Bool
- isSortMeta_ :: MetaVariable -> Bool
- isSortJudgement :: Judgement a -> Bool
- metaInstantiationToMetaKind :: MetaInstantiation -> MetaKind
- getMetaType :: ReadTCState m => MetaId -> m Type
- getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args
- getMetaTypeInContext :: (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m, MonadTCEnv m, ReadTCState m) => MetaId -> m Type
- isGeneralizableMeta :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m DoGeneralize
- class IsInstantiatedMeta a where
  - isInstantiatedMeta :: ReadTCState m => a -> m Bool
- isInstantiatedMeta' :: ReadTCState m => MetaId -> m (Maybe Term)
- constraintMetas :: Constraint -> TCM (Set MetaId)
- createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo
- 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 ()
- updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()
- setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m ()
- class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints (m :: Type -> Type) where
  - freshInteractionId :: m InteractionId
  - modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()
- registerInteractionPoint :: MonadInteractionPoints m => Bool -> Range -> Maybe Nat -> m InteractionId
- findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
- connectInteractionPoint :: MonadInteractionPoints m => InteractionId -> MetaId -> m ()
- removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m ()
- getInteractionPoints :: ReadTCState m => m [InteractionId]
- getInteractionMetas :: ReadTCState m => m [MetaId]
- 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)]
- isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId)
- lookupInteractionPoint :: (ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m InteractionPoint
- lookupInteractionId :: (ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m MetaId
- lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId)
- lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
- newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
- newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId
- getInteractionRange :: (MonadInteractionPoints m, MonadDebug m, MonadError TCErr m) => InteractionId -> m Range
- getMetaRange :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Range
- getInteractionScope :: (MonadDebug 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, 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 ()
- unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
- getMetaListeners :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m [Listener]
- clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
- etaExpandMetaSafe :: MonadMetaSolver m => MetaId -> m ()
- etaExpandListeners :: MonadMetaSolver m => MetaId -> m ()
- wakeupListener :: MonadMetaSolver m => Listener -> m ()
- solveAwakeConstraints :: MonadConstraint m => m ()
- solveAwakeConstraints' :: MonadConstraint m => Bool -> m ()
- freezeMetas :: (MonadTCState m, ReadTCState m) => LocalMetaStore -> m (Set MetaId)
- unfreezeMetas :: TCM ()
- isFrozen :: (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Bool
- withFrozenMetas :: (MonadMetaSolver m, MonadTCState m) => m a -> m a
- class UnFreezeMeta a where
  - unfreezeMeta :: MonadMetaSolver m => a -> m ()

# Documentation

data MetaClass Source #

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.

#### Instances

Instances details

Bounded MetaClass Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods minBound :: MetaClass Source # maxBound :: MetaClass Source #
Enum MetaClass Source # |

Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

succ :: MetaClass -> MetaClass Source #

pred :: MetaClass -> MetaClass Source #

toEnum :: Int -> MetaClass Source #

fromEnum :: MetaClass -> Int Source #

enumFrom :: MetaClass -> [MetaClass] Source #

enumFromThen :: MetaClass -> MetaClass -> [MetaClass] Source #

enumFromTo :: MetaClass -> MetaClass -> [MetaClass] Source #

enumFromThenTo :: MetaClass -> MetaClass -> MetaClass -> [MetaClass] Source #

Show MetaClass Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods showsPrec :: Int -> MetaClass -> ShowS Source # show :: MetaClass -> String Source # showList :: [MetaClass] -> ShowS Source #
Eq MetaClass Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods (==) :: MetaClass -> MetaClass -> Bool Source # (/=) :: MetaClass -> MetaClass -> Bool Source #

allMetaClasses :: [MetaClass] Source #

All possible metavariable classes.

data KeepMetas Source #

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 Source #

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

Methods

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

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

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

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

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

etaExpandMeta :: [MetaClass] -> MetaId -> m () Source #

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

Update the status of the metavariable

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

'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

Instances details

MonadMetaSolver TCM Source # |

Instance details

Defined in Agda.TypeChecking.MetaVars

Methods

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

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

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

etaExpandMeta :: [MetaClass] -> MetaId -> TCM () Source #

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

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

PureTCM m => MonadMetaSolver (PureConversionT m) Source # |

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

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

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

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

etaExpandMeta :: [MetaClass] -> MetaId -> PureConversionT m () Source #

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

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

MonadMetaSolver m => MonadMetaSolver (ReaderT r m) Source # |

Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

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

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

etaExpandMeta :: [MetaClass] -> MetaId -> ReaderT r m () Source #

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

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

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

Switch off assignment of metas.

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

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

nextLocalMeta :: ReadTCState m => m MetaId Source #

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 Source #

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) Source #

Run a computation and record which new metas it created.

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

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

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

Find information about the given local meta-variable.

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

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 Source #

Find the meta-variable's instantiation.

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

Find the meta-variable's judgement.

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

Find the meta-variable's modality.

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

The type of a term or sort meta-variable.

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

Update the information associated with a local meta-variable.

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

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

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

Returns the `MetaPriority` of the given local meta-variable.

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

isSortMeta_ :: MetaVariable -> Bool Source #

isSortJudgement :: Judgement a -> Bool Source #

metaInstantiationToMetaKind :: MetaInstantiation -> MetaKind Source #

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

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

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

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 Source #

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

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

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

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 :: ReadTCState m => a -> m Bool Source #

#### Instances

Instances details

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

isInstantiatedMeta' :: ReadTCState m => MetaId -> m (Maybe Term) Source #

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. 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 Source #

Create `MetaInfo` in the current environment.

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

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

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

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

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

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

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

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

# Query and manipulate interaction points.

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

Minimal complete definition

Nothing

Methods

freshInteractionId :: m InteractionId Source #

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

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

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

#### Instances

Instances details

MonadInteractionPoints TCM Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: TCM InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM () Source #
PureTCM m => MonadInteractionPoints (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods freshInteractionId :: PureConversionT m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> PureConversionT m () Source #
MonadInteractionPoints m => MonadInteractionPoints (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: MaybeT m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> MaybeT m () Source #
MonadInteractionPoints m => MonadInteractionPoints (ExceptT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: ExceptT e m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> ExceptT e m () Source #
MonadInteractionPoints m => MonadInteractionPoints (IdentityT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: IdentityT m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> IdentityT m () Source #
MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: ReaderT r m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> ReaderT r m () Source #
MonadInteractionPoints m => MonadInteractionPoints (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: StateT s m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> StateT s m () Source #
(MonadInteractionPoints m, Monoid w) => MonadInteractionPoints (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods freshInteractionId :: WriterT w m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> WriterT w m () Source #

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

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

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

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

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

Mark an interaction point as solved.

getInteractionPoints :: ReadTCState m => m [InteractionId] Source #

Get a list of interaction ids.

getInteractionMetas :: ReadTCState m => m [MetaId] Source #

Get all metas that correspond to unsolved interaction ids.

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

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

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

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

Get all metas that correspond to unsolved interaction ids.

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

Does the meta variable correspond to an interaction point?

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

lookupInteractionPoint :: (ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m InteractionPoint Source #

Get the information associated to an interaction point.

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

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

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

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

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

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

Generate new meta variable.

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

Get the `Range` for an interaction point.

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

Get the `Range` for a local meta-variable.

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

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

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

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

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

getOpenMetas :: ReadTCState m => m [MetaId] Source #

isOpenMeta :: MetaInstantiation -> Bool Source #

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

`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 () Source #

Unregister a listener.

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

Get the listeners for a local meta-variable.

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

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

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

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

Eta expand metavariables listening on the current meta.

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

Wake up a meta listener and let it do its thing

solveAwakeConstraints :: MonadConstraint m => m () Source #

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

# Freezing and unfreezing metas.

freezeMetas :: (MonadTCState m, ReadTCState m) => LocalMetaStore -> m (Set MetaId) Source #

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

unfreezeMetas :: TCM () Source #

Thaw all open meta variables.

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

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

class UnFreezeMeta a where Source #

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

#### Instances

Instances details

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