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

Safe HaskellNone

Agda.TypeChecking.MetaVars

Contents

Synopsis

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.

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.

Creating meta variables.

newIFSMeta :: Type -> TCM Term

Create a new implicit from scope metavariable

newIFSMetaCtx :: Type -> Args -> TCM Term

Create a new value meta with specific dependencies.

newValueMeta :: Type -> TCM Term

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

newValueMeta' :: Type -> TCM Term

Create a new value meta without η-expanding.

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

Create a new value meta with specific dependencies.

newRecordMeta :: QName -> Args -> TCM Term

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

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

Construct a blocked constant if there are constraints.

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.

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

checkAllVars :: Args -> TCM [Nat]

Check that arguments to a metavar are in pattern fragment. Assumes all arguments already in whnf. Parameters are represented as Vars so checkArgs really checks that all args are Vars and returns the list of corresponding indices for each arg. Linearity has to be checked separately.

reverse is necessary because we are directly abstracting over this list ids.

allVarOrIrrelevant :: Args -> Maybe [Arg Nat]

filter out irrelevant args and check that all others are variables. Return the reversed list of variables.