Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone





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

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 BoolSource

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

Performing the assignment

assignTerm :: MetaId -> Term -> TCM ()Source

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

Skip frozen check. Used for eta expanding frozen metas.

Creating meta variables.

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

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 TermSource

Create a new value meta with specific dependencies.

newValueMeta :: RunMetaOccursCheck -> Type -> TCM TermSource

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

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

Create a new value meta without η-expanding.

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

Create a new value meta with specific dependencies.

newRecordMeta :: QName -> Args -> TCM TermSource

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

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

Construct a blocked constant if there are constraints.

unblockedTester :: Type -> TCM BoolSource

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 TermSource

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 TermSource

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

Eta expand metavariables listening on the current meta.

wakeupListener :: Listener -> TCM ()Source

Wake up a meta listener and let it do its thing

etaExpandMetaSafe :: MetaId -> TCM ()Source

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

data MetaKind Source

Various kinds of metavariables.



Meta variables of record type.


Meta variables of "hereditarily singleton" record type.


Meta variables of level type, if type-in-type is activated.

allMetaKinds :: [MetaKind]Source

All possible metavariable kinds.

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

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

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

Solve constraint x vs = v.

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

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

assign sort? x vs v

type SubstCandSource


 = [(Nat, Term)]

a possibly non-deterministic substitution

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

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

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

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

allMetas :: Type -> [MetaId]Source

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