Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.MetaVars

Contents

- Performing the assignment
- Creating meta variables.
- Orphan instances

Synopsis

- findIdx :: Eq a => [a] -> a -> Maybe Int
- hasTwinMeta :: MetaId -> TCM Bool
- isBlockedTerm :: MetaId -> TCM Bool
- isEtaExpandable :: [MetaClass] -> MetaId -> TCM Bool
- assignTerm :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
- assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
- newSortMetaBelowInf :: TCM Sort
- newSortMeta :: MonadMetaSolver m => m Sort
- newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort
- newTypeMeta' :: Comparison -> Sort -> TCM Type
- newTypeMeta :: Sort -> TCM Type
- newTypeMeta_ :: TCM Type
- newLevelMeta :: MonadMetaSolver m => m Level
- newInstanceMeta :: MonadMetaSolver m => MetaNameSuggestion -> Type -> m (MetaId, Term)
- newInstanceMetaCtx :: MonadMetaSolver m => MetaNameSuggestion -> Type -> Args -> m (MetaId, Term)
- newNamedValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
- newNamedValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
- newValueMetaOfKind :: MonadMetaSolver m => MetaInfo -> RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
- newValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
- newValueMetaCtx :: MonadMetaSolver m => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
- newValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
- newValueMetaCtx' :: MonadMetaSolver m => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
- newTelMeta :: MonadMetaSolver m => Telescope -> m Args
- type Condition = Dom Type -> Abs Type -> Bool
- trueCondition :: Condition
- newArgsMeta :: MonadMetaSolver m => Type -> m Args
- newArgsMeta' :: MonadMetaSolver m => Condition -> Type -> m Args
- newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
- newArgsMetaCtx'' :: MonadMetaSolver m => MetaNameSuggestion -> Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
- newArgsMetaCtx' :: MonadMetaSolver m => Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
- newRecordMeta :: QName -> Args -> TCM Term
- newRecordMetaCtx :: MetaNameSuggestion -> Frozen -> QName -> Args -> Telescope -> Permutation -> Args -> TCM Term
- newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
- newQuestionMark' :: (Comparison -> Type -> TCM (MetaId, Term)) -> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
- blockTerm :: (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m, MonadFresh ProblemId m) => Type -> m Term -> m Term
- blockTermOnProblem :: (MonadMetaSolver m, MonadFresh Nat m) => Type -> Term -> ProblemId -> m Term
- blockTypeOnProblem :: (MonadMetaSolver m, MonadFresh Nat m) => Type -> ProblemId -> m Type
- unblockedTester :: Type -> TCM Blocker
- postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
- postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term
- problemType :: TypeCheckingProblem -> Type
- etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM ()
- etaExpandBlocked :: (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) => Blocked t -> m (Blocked t)
- assignWrapper :: (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m, MonadDebug m, HasOptions m) => CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
- assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
- isInteractionMetaB :: (ReadTCState m, MonadReduce m, MonadPretty m) => MetaId -> Args -> m (Maybe (MetaId, InteractionId, Args))
- assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
- assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
- checkMetaInst :: MetaId -> TCM ()
- checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
- checkSubtypeIsEqual :: Type -> Type -> TCM ()
- subtypingForSizeLt :: CompareDirection -> MetaId -> MetaVariable -> Type -> Args -> Term -> (Term -> TCM ()) -> TCM ()
- expandProjectedVars :: (Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a, PrettyTCM b, TermSubst b) => a -> b -> (a -> b -> TCM c) -> TCM c
- etaExpandProjectedVar :: (PrettyTCM a, TermSubst a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
- class NoProjectedVar a where
  - noProjectedVar :: a -> Either ProjectedVar ()
- class (TermLike a, TermSubst a, Reduce a) => ReduceAndEtaContract a where
  - reduceAndEtaContract :: a -> TCM a
- type FVs = VarSet
- type SubstCand = [(Int, Term)]
- checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
- type Res = [(Arg Nat, Term)]
- data InvertExcept
  - = CantInvert Term
  - | NeutralArg
  - | ProjVar ProjectedVar
- inverseSubst' :: (Term -> Bool) -> Args -> ExceptT InvertExcept TCM SubstCand
- isFaceConstraint :: MetaId -> Args -> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
- tryAddBoundary :: CompareDirection -> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
- openMetasToPostulates :: TCM ()
- dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])

# Documentation

findIdx :: Eq a => [a] -> a -> Maybe Int Source #

Find position of a value in a list. Used to change metavar argument indices during assignment.

`reverse` is necessary because we are directly abstracting over the list.

hasTwinMeta :: MetaId -> TCM Bool Source #

Does the given local meta-variable have a twin meta-variable?

isBlockedTerm :: MetaId -> TCM Bool Source #

Check whether a meta variable is a place holder for a blocked term.

isEtaExpandable :: [MetaClass] -> MetaId -> TCM Bool Source #

# Performing the assignment

assignTerm :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m () Source #

Performing the meta variable assignment.

The instantiation should not be an `InstV` and the `MetaId` should point to something `Open` or a `BlockedConst`. Further, the meta variable may not be `Frozen`.

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

Skip frozen check. Used for eta expanding frozen metas.

# Creating meta variables.

newSortMetaBelowInf :: TCM Sort Source #

Create a sort meta that cannot be instantiated with `Inf` (Setω).

newSortMeta :: MonadMetaSolver m => m Sort Source #

Create a sort meta that may be instantiated with `Inf` (Setω).

newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort Source #

Create a sort meta that may be instantiated with `Inf` (Setω).

newTypeMeta' :: Comparison -> Sort -> TCM Type Source #

newTypeMeta :: Sort -> TCM Type Source #

newTypeMeta_ :: TCM Type Source #

newLevelMeta :: MonadMetaSolver m => m Level Source #

newInstanceMeta :: MonadMetaSolver m => MetaNameSuggestion -> Type -> m (MetaId, Term) Source #

`newInstanceMeta s t cands` creates a new instance metavariable of type the output type of `t` with name suggestion `s`.

newInstanceMetaCtx :: MonadMetaSolver m => MetaNameSuggestion -> Type -> Args -> m (MetaId, Term) Source #

newNamedValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term) Source #

Create a new value meta with specific dependencies, possibly η-expanding in the process.

newNamedValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term) Source #

Create a new value meta with specific dependencies without η-expanding.

newValueMetaOfKind Source #

Arguments

:: MonadMetaSolver m |
=> MetaInfo |
-> RunMetaOccursCheck | Ignored for instance metas.
-> Comparison | Ignored for instance metas.
-> Type |
-> m (MetaId, Term) |

newValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term) Source #

Create a new metavariable, possibly η-expanding in the process.

newValueMetaCtx :: MonadMetaSolver m => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term) Source #

newValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term) Source #

Create a new value meta without η-expanding.

newValueMetaCtx' :: MonadMetaSolver m => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term) Source #

newTelMeta :: MonadMetaSolver m => Telescope -> m Args Source #

type Condition = Dom Type -> Abs Type -> Bool Source #

trueCondition :: Condition Source #

newArgsMeta :: MonadMetaSolver m => Type -> m Args Source #

newArgsMeta' :: MonadMetaSolver m => Condition -> Type -> m Args Source #

newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args Source #

newArgsMetaCtx'' :: MonadMetaSolver m => MetaNameSuggestion -> Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args Source #

newArgsMetaCtx' :: MonadMetaSolver m => Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args Source #

newRecordMeta :: QName -> Args -> TCM Term Source #

Create a metavariable of record type. This is actually one metavariable for each field.

newRecordMetaCtx Source #

Arguments

:: MetaNameSuggestion | Name suggestion to be used as a prefix of the name suggestions for the metas that represent each field
-> Frozen | Should the meta be created frozen?
-> QName | Name of record type
-> Args | Parameters of record type.
-> Telescope |
-> Permutation |
-> Args |
-> TCM Term |

newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term) Source #

newQuestionMark' :: (Comparison -> Type -> TCM (MetaId, Term)) -> InteractionId -> Comparison -> Type -> TCM (MetaId, Term) Source #

blockTerm :: (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m, MonadFresh ProblemId m) => Type -> m Term -> m Term Source #

Construct a blocked constant if there are constraints.

blockTermOnProblem :: (MonadMetaSolver m, MonadFresh Nat m) => Type -> Term -> ProblemId -> m Term Source #

blockTypeOnProblem :: (MonadMetaSolver m, MonadFresh Nat m) => Type -> ProblemId -> m Type Source #

unblockedTester :: Type -> TCM Blocker Source #

`unblockedTester t` returns a `Blocker` for `t`.

Auxiliary function used when creating a postponed type checking problem.

postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term Source #

Create a postponed type checking problem `e : t` that waits for type `t` to unblock (become instantiated or its constraints resolved).

postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term Source #

Create a postponed type checking problem `e : t` that waits for conditon `unblock`. A new meta is created in the current context that has as instantiation the postponed type checking problem. An `UnBlock` constraint is added for this meta, which links to this meta.

problemType :: TypeCheckingProblem -> Type Source #

Type of the term that is produced by solving the `TypeCheckingProblem`.

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

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.

etaExpandBlocked :: (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) => Blocked t -> m (Blocked t) Source #

Eta expand blocking metavariables of record type, and reduce the blocked thing.

assignWrapper :: (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m, MonadDebug m, HasOptions m) => CompareDirection -> MetaId -> Elims -> Term -> m () -> m () Source #

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

Miller pattern unification:

`assign dir x vs v a` solves problem `x vs <=(dir) v : a` for meta `x` if `vs` are distinct variables (linearity check) and `v` depends only on these variables and does not contain `x` itself (occurs check).

This is the basic story, but we have added some features:

1. Pruning.
2. Benign cases of non-linearity.
3. `vs` may contain record patterns.

For a reference to some of these extensions, read Andreas Abel and Brigitte Pientka's TLCA 2011 paper.

isInteractionMetaB :: (ReadTCState m, MonadReduce m, MonadPretty m) => MetaId -> Args -> m (Maybe (MetaId, InteractionId, Args)) Source #

Is the given metavariable application secretly an interaction point application? Ugly.

assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM () Source #

`assignMeta m x t ids u` solves `x ids = u` for meta `x` of type `t`, where term `u` lives in a context of length `m`. Precondition: `ids` is linear.

assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM () Source #

`assignMeta' m x t ids u` solves `x = [ids]u` for meta `x` of type `t`, where term `u` lives in a context of length `m`, and `ids` is a partial substitution.

checkMetaInst :: MetaId -> TCM () Source #

Check that the instantiation of the given metavariable fits the type of the metavariable. If the metavariable is not yet instantiated, add a constraint to check the instantiation later.

checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM () Source #

Check that the instantiation of the metavariable with the given term is well-typed.

checkSubtypeIsEqual :: Type -> Type -> TCM () Source #

Given two types `a` and `b` with `a <: b`, check that `a == b`.

subtypingForSizeLt Source #

Arguments

:: CompareDirection

    dir

-> MetaId | The local meta-variable `x`.
-> MetaVariable | Its associated information `mvar <- lookupLocalMeta x`.
-> Type | Its type `t = jMetaType $ mvJudgement mvar`
-> Args | Its arguments.
-> Term | Its to-be-assigned value `v`, such that `x args `dir` v`.
-> (Term -> TCM ()) | Continuation taking its possibly assigned value.
-> TCM () |

Turn the assignment problem `_X args <= SizeLt u` into `_X args = SizeLt (_Y args)` and constraint `_Y args <= u`.

expandProjectedVars Source #

Arguments

:: (Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a, PrettyTCM b, TermSubst b) |
=> a | Meta variable arguments.
-> b | Right hand side.
-> (a -> b -> TCM c) |
-> TCM c |

Eta-expand bound variables like `z` in `X (fst z)`.

etaExpandProjectedVar :: (PrettyTCM a, TermSubst a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c Source #

Eta-expand a de Bruijn index of record type in context and passed term(s).

class NoProjectedVar a where Source #

Check whether one of the meta args is a projected var.

Minimal complete definition

Nothing

Methods

noProjectedVar :: a -> Either ProjectedVar () Source #

default noProjectedVar :: forall b (t :: Type -> Type). (NoProjectedVar b, Foldable t, t b ~ a) => a -> Either ProjectedVar () Source #

#### Instances

Instances details

NoProjectedVar Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Term -> Either ProjectedVar () Source #
NoProjectedVar a => NoProjectedVar (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Arg a -> Either ProjectedVar () Source #
NoProjectedVar a => NoProjectedVar [a] Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: [a] -> Either ProjectedVar () Source #

class (TermLike a, TermSubst a, Reduce a) => ReduceAndEtaContract a where Source #

Normalize just far enough to be able to eta-contract maximally.

Minimal complete definition

Nothing

Methods

reduceAndEtaContract :: a -> TCM a Source #

default reduceAndEtaContract :: forall (f :: Type -> Type) b. (Traversable f, TermLike b, Subst b, Reduce b, ReduceAndEtaContract b, f b ~ a) => a -> TCM a Source #

#### Instances

Instances details

ReduceAndEtaContract Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: Term -> TCM Term Source #
ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: Arg a -> TCM (Arg a) Source #
ReduceAndEtaContract a => ReduceAndEtaContract [a] Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: [a] -> TCM [a] Source #

type FVs = VarSet Source #

type SubstCand Source #

Arguments

= [(Int, Term)] | a possibly non-deterministic substitution

checkLinearity :: SubstCand -> ExceptT () TCM SubstCand Source #

Turn non-det substitution into proper substitution, if possible. Otherwise, raise the error.

type Res = [(Arg Nat, Term)] Source #

data InvertExcept Source #

Exceptions raised when substitution cannot be inverted.

Constructors

CantInvert Term | Cannot recover.
NeutralArg | A potentially neutral arg: can't invert, but can try pruning.
ProjVar ProjectedVar | Try to eta-expand var to remove projs.

inverseSubst' :: (Term -> Bool) -> Args -> ExceptT InvertExcept TCM SubstCand Source #

Check that arguments `args` to a metavar are in pattern fragment. Assumes all arguments already in whnf and eta-reduced. Parameters are represented as `Var`s so `checkArgs` really checks that all args are `Var`s and returns the "substitution" to be applied to the rhs of the equation to solve. (If `args` is considered a substitution, its inverse is returned.)

The returned list might not be ordered. Linearity, i.e., whether the substitution is deterministic, has to be checked separately.

isFaceConstraint :: MetaId -> Args -> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)) Source #

If the given metavariable application represents a face, return:

- The metavariable information;
- The actual face, as an assignment of booleans to variables;
- The substitution candidate resulting from `inverseSubst'`. This is guaranteed to be linear and deterministic.
- The actual substitution, mapping from the constraint context to the metavariable's context.

Put concisely, a face constraint is an equation in the pattern fragment modulo the presence of endpoints (`i0` and `i1`) in the telescope. In more detail, a face constraint has the form

    ?0 Δ (i = i0) (j = i0) Γ (k = i1) Θ (l = i0) = t

where all the greek letters consist entirely of distinct bound variables (and, of course, arbitrarily many endpoints are allowed between each substitution fragment).

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

Record a "face" equation onto an interaction point into the actual interaction point boundary. Takes all the same arguments as `assignMeta'`.

openMetasToPostulates :: TCM () Source #

Turn open metas into postulates.

Preconditions:

1. We are `inTopContext`.
2. `envCurrentModule` is set to the top-level module.

dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId]) Source #

Sort metas in dependency order.

# Orphan instances

MonadMetaSolver TCM Source # |

Instance details

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 #