Safe Haskell | None |
---|
Agda.TypeChecking.MetaVars
- 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 ()
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
trueCondition :: t -> t1 -> Bool
newArgsMeta :: Type -> TCM Args
newArgsMeta' :: Condition -> Type -> TCM Args
newRecordMeta :: QName -> Args -> TCM Term
Create a metavariable of record type. This is actually one metavariable for each field.
newQuestionMark :: Type -> 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. |
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.
checkLinearity :: (Nat -> Bool) -> SubstCand -> ErrorT () TCM SubstCand
Turn non-det substitution into proper substitution, if possible.
The substitution can be restricted to elemFVs
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 ()