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

Safe Haskell | None

Agda.TypeChecking.MetaVars

Contents

- Performing the assignment
- Creating meta variables.
- Solve constraint `x vs = v`.

Synopsis

- findIdx :: Eq a => [a] -> a -> Maybe Int
- isBlockedTerm :: MetaId -> TCM Bool
- isEtaExpandable :: MetaId -> TCM Bool
- assignTerm :: MetaId -> Term -> TCM ()
- assignTerm' :: MetaId -> Term -> TCM ()
- newSortMeta :: TCM Sort
- newSortMetaCtx :: Args -> TCM Sort
- newTypeMeta :: Sort -> TCM Type
- newTypeMeta_ :: TCM Type
- newIFSMeta :: MetaNameSuggestion -> Type -> [(Term, Type)] -> TCM Term
- newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> [(Term, Type)] -> TCM Term
- newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM Term
- newValueMeta :: RunMetaOccursCheck -> Type -> TCM Term
- newValueMetaCtx :: RunMetaOccursCheck -> Type -> Args -> TCM Term
- newValueMeta' :: RunMetaOccursCheck -> Type -> TCM Term
- newValueMetaCtx' :: RunMetaOccursCheck -> Type -> Args -> TCM Term
- newTelMeta :: Telescope -> TCM Args
- type Condition = Dom Type -> Abs Type -> Bool
- trueCondition :: t -> t1 -> Bool
- 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
- newRecordMetaCtx :: QName -> Args -> Telescope -> Args -> TCM Term
- newQuestionMark :: Type -> TCM Term
- blockTerm :: Type -> TCM Term -> TCM Term
- blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term
- unblockedTester :: Type -> TCM Bool
- postponeTypeCheckingProblem_ :: Expr -> Type -> TCM Term
- postponeTypeCheckingProblem :: Expr -> Type -> TCM Bool -> TCM Term
- etaExpandListeners :: MetaId -> TCM ()
- wakeupListener :: Listener -> TCM ()
- etaExpandMetaSafe :: MetaId -> TCM ()
- data MetaKind
  - = Records
  - | SingletonRecords
  - | Levels
- allMetaKinds :: [MetaKind]
- etaExpandMeta :: [MetaKind] -> MetaId -> TCM ()
- etaExpandBlocked :: Reduce t => Blocked t -> TCM (Blocked t)
- assignV :: MetaId -> Args -> Term -> TCM ()
- assign :: MetaId -> Args -> Term -> TCM ()
- type FVs = VarSet
- type SubstCand = [(Nat, Term)]
- checkLinearity :: (Nat -> Bool) -> SubstCand -> ErrorT () TCM SubstCand
- type Res = Maybe [(Arg Nat, Term)]
- inverseSubst :: Args -> ErrorT () TCM (Maybe SubstCand)
- updateMeta :: MetaId -> Term -> TCM ()
- allMetas :: Type -> [MetaId]

# 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 -> 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 -> 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 -> [(Term, Type)] -> TCM Term

`newIFSMeta s t cands` creates a new implicit from scope metavariable of type `t` with name suggestion `s` and initial solution candidates `cands`.

newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> [(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 :: t -> t1 -> Bool

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 :: Type -> TCM Term

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

Construct a blocked constant if there are constraints.

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

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_ :: Expr -> Type -> TCM Term

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

postponeTypeCheckingProblem :: Expr -> Type -> 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.

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

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

    assign sort? x vs v

type FVs = VarSet

type SubstCand

Arguments

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

checkLinearity :: (Nat -> Bool) -> SubstCand -> ErrorT () TCM SubstCand

Turn non-det substitution into proper substitution, if possible. The substitution can be restricted to `elemFVs`

type Res = Maybe [(Arg Nat, Term)]

inverseSubst :: Args -> ErrorT () TCM (Maybe 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 `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.

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

allMetas :: Type -> [MetaId]

Returns every meta-variable occurrence in the given type, except for those in `Sort`s.