Safe Haskell | None |
---|
- findIdx :: Eq a => [a] -> a -> Maybe Int
- isBlockedTerm :: MetaId -> TCM Bool
- isEtaExpandable :: MetaId -> TCM Bool
- assignTerm :: MetaId -> Term -> TCM ()
- newSortMeta :: TCM Sort
- newSortMetaCtx :: Args -> TCM Sort
- newTypeMeta :: Sort -> TCM Type
- newTypeMeta_ :: TCM Type
- newIFSMeta :: Type -> TCM Term
- newIFSMetaCtx :: Type -> Args -> TCM Term
- newValueMeta :: Type -> TCM Term
- newValueMetaCtx :: Type -> Args -> TCM Term
- newValueMeta' :: Type -> TCM Term
- newValueMetaCtx' :: Type -> Args -> TCM Term
- newTelMeta :: Telescope -> TCM Args
- newArgsMeta :: Type -> TCM Args
- newArgsMetaCtx :: 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
- checkAllVars :: Args -> TCM [Nat]
- allVarOrIrrelevant :: Args -> Maybe [Arg Nat]
- updateMeta :: MetaId -> Term -> TCM ()
Documentation
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.
isEtaExpandable :: MetaId -> TCM BoolSource
Performing the assignment
Creating meta variables.
newSortMetaCtx :: Args -> TCM SortSource
newTypeMeta :: Sort -> TCM TypeSource
newIFSMeta :: Type -> TCM TermSource
Create a new implicit from scope metavariable
newValueMeta :: Type -> TCM TermSource
Create a new metavariable, possibly η-expanding in the process.
newValueMeta' :: Type -> TCM TermSource
Create a new value meta without η-expanding.
newValueMetaCtx' :: Type -> Args -> TCM TermSource
Create a new value meta with specific dependencies.
newTelMeta :: Telescope -> TCM ArgsSource
newArgsMeta :: Type -> TCM ArgsSource
newRecordMeta :: QName -> Args -> TCM TermSource
Create a metavariable of record type. This is actually one metavariable for each field.
newQuestionMark :: Type -> TCM TermSource
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
).
Various kinds of metavariables.
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]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.
checkAllVars :: Args -> TCM [Nat]Source
Check that arguments to a metavar are in pattern fragment.
Assumes all arguments already in whnf.
Parameters are represented as Var
s so checkArgs
really
checks that all args are Var
s 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
.