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.

isBlockedTerm :: MetaId -> TCM Bool

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

isEtaExpandable :: MetaId -> TCM Bool

Performing the assignment

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

Performing the meta variable assignment.

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

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

Skip frozen check. Used for eta expanding frozen metas.

Creating meta variables.

newSortMeta :: TCM Sort

newSortMetaCtx :: Args -> TCM Sort

newTypeMeta :: Sort -> TCM Type

newTypeMeta_ :: TCM Type

newIFSMeta :: MetaNameSuggestion -> Type -> Maybe [(Term, Type)] -> TCM Term

newIFSMeta s t cands creates a new "implicit from scope" metavariable of type the output type of t with name suggestion s and initial solution candidates cands. If t is a function type, then insert enough lambdas in front of it.

newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> Maybe [(Term, Type)] -> TCM Term

Create a new value meta with specific dependencies.

newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM Term

newValueMeta :: RunMetaOccursCheck -> Type -> TCM Term

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

newValueMetaCtx :: RunMetaOccursCheck -> Type -> Args -> TCM Term

newValueMeta' :: RunMetaOccursCheck -> Type -> TCM Term

Create a new value meta without η-expanding.

newValueMetaCtx' :: RunMetaOccursCheck -> Type -> Args -> TCM Term

Create a new value meta with specific dependencies.

newTelMeta :: Telescope -> TCM Args

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

trueCondition :: Condition

newArgsMeta :: Type -> TCM Args

newArgsMeta' :: Condition -> Type -> TCM Args

newArgsMetaCtx :: Type -> Telescope -> Args -> TCM Args

newArgsMetaCtx' :: Condition -> Type -> Telescope -> Args -> TCM Args

newRecordMeta :: QName -> Args -> TCM Term

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

newRecordMetaCtx :: QName -> Args -> Telescope -> Args -> TCM Term

newQuestionMark :: InteractionId -> Type -> TCM Term

blockTerm :: Type -> TCM Term -> TCM Term

Construct a blocked constant if there are constraints.

blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term

blockTypeOnProblem :: Type -> ProblemId -> TCM Type

unblockedTester :: Type -> TCM Bool

unblockedTester t returns False if t is a meta or a blocked term.

Auxiliary function to create 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 -> TCM Bool -> 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.

etaExpandListeners :: MetaId -> TCM ()

Eta expand metavariables listening on the current meta.

wakeupListener :: Listener -> TCM ()

Wake up a meta listener and let it do its thing

etaExpandMetaSafe :: MetaId -> TCM ()

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

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

Enum MetaKind

Eq MetaKind

Show MetaKind

allMetaKinds :: [MetaKind]

All possible metavariable kinds.

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

Eta expand a metavariable, if it is of the specified kind. Don't do anything if the metavariable is a blocked term.

etaExpandBlocked :: Reduce t => Blocked t -> TCM (Blocked t)

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

Solve constraint x vs = v.

assignV :: CompareDirection -> MetaId -> Args -> Term -> TCM ()

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.

assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM ()

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

Miller pattern unification:

assign x vs v solves problem x vs = v 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.

subtypingForSizeLt :: CompareDirection -> MetaId -> MetaVariable -> Type -> Args -> Term -> (Term -> TCM ()) -> TCM ()

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

expandProjectedVars :: (Normalise a, TermLike a, PrettyTCM a, NoProjectedVar a, Subst a, PrettyTCM b, Subst b) => a -> b -> (a -> b -> TCM c) -> TCM c

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

etaExpandProjectedVar :: (PrettyTCM a, Subst 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.

Methods

noProjectedVar :: a -> Either ProjVarExc ()

Instances

NoProjectedVar Term

NoProjectedVar a => NoProjectedVar [a]

NoProjectedVar a => NoProjectedVar (Arg a)

data ProjVarExc

Constructors

ProjVarExc Int [QName]

Instances

Error ProjVarExc

type FVs = VarSet

type SubstCand

Arguments

 = [(Nat, 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.

ProjectedVar Int [QName]

Try to eta-expand var to remove projs.

Instances

Error InvertExcept

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.

updateMeta :: MetaId -> Term -> TCM ()

Used in giveExpr.

allMetas :: TermLike a => a -> [MetaId]

Returns every meta-variable occurrence in the given type, except for those in Sorts.