Agda.TypeChecking.MetaVars

Documentation

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

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

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

isBlockedTerm :: MetaId -> TCM Bool

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

isEtaExpandable :: [MetaKind] -> MetaId -> TCM Bool

Performing the assignment

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

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

Skip frozen check. Used for eta expanding frozen metas.

Creating meta variables.

newSortMetaBelowInf :: TCM Sort

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

newSortMeta :: MonadMetaSolver m => m Sort

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

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

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

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)

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)

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

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

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

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

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

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

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

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

Create a new value meta without η-expanding.

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 => Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args

newRecordMeta :: QName -> Args -> TCM Term

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

newRecordMetaCtx

Arguments

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

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

Construct a blocked constant if there are constraints.

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

unblockedTester t returns a Blocker for t.

Auxiliary function used when creating a postponed type checking problem.

postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term

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

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

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

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

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)

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

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

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.

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

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

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

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

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

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

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

subtypingForSizeLt

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

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

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

class NoProjectedVar a where

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

Minimal complete definition

Nothing

Methods

noProjectedVar :: a -> Either ProjectedVar ()

default noProjectedVar :: (NoProjectedVar b, Foldable t, t b ~ a) => a -> Either ProjectedVar ()

Instances

NoProjectedVar Term

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: Term -> Either ProjectedVar ()

NoProjectedVar a => NoProjectedVar (Arg a)

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: Arg a -> Either ProjectedVar ()

NoProjectedVar a => NoProjectedVar [a]

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: [a] -> Either ProjectedVar ()

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

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

Minimal complete definition

Nothing

Methods

reduceAndEtaContract :: a -> TCM a

default reduceAndEtaContract :: (Traversable f, TermLike b, Subst b, Reduce b, ReduceAndEtaContract b, f b ~ a) => a -> TCM a

Instances

ReduceAndEtaContract Term

Defined in Agda.TypeChecking.MetaVars

Methods

reduceAndEtaContract :: Term -> TCM Term

ReduceAndEtaContract a => ReduceAndEtaContract (Arg a)

Defined in Agda.TypeChecking.MetaVars

Methods

reduceAndEtaContract :: Arg a -> TCM (Arg a)

ReduceAndEtaContract a => ReduceAndEtaContract [a]

Defined in Agda.TypeChecking.MetaVars

Methods

reduceAndEtaContract :: [a] -> TCM [a]

type FVs = VarSet

type SubstCand

Arguments

 = [(Int, Term)]

a possibly non-deterministic substitution

checkLinearity :: SubstCand -> ExceptT () TCM SubstCand

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

type Res = [(Arg Nat, Term)]

data InvertExcept

Exceptions raised when substitution cannot be inverted.

Constructors

CantInvert

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 :: Args -> ExceptT InvertExcept TCM SubstCand

Check that arguments args to a metavar are in pattern fragment. Assumes all arguments already in whnf and eta-reduced. Parameters are represented as Vars so checkArgs really checks that all args are Vars 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.

openMetasToPostulates :: TCM ()

Turn open metas into postulates.

Preconditions:

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

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

Sort metas in dependency order.

Orphan instances

MonadMetaSolver TCM

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