Safe Haskell | None |
---|---|
Language | Haskell98 |
- findIdx :: Eq a => [a] -> a -> Maybe Int
- isBlockedTerm :: MetaId -> TCM Bool
- isEtaExpandable :: [MetaKind] -> MetaId -> TCM Bool
- assignTerm :: MetaId -> [Arg ArgName] -> Term -> TCM ()
- assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
- newSortMeta :: TCM Sort
- newSortMetaCtx :: Args -> TCM Sort
- newTypeMeta :: Sort -> TCM Type
- newTypeMeta_ :: TCM Type
- newIFSMeta :: MetaNameSuggestion -> Type -> Maybe [Candidate] -> TCM Term
- newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> Maybe [Candidate] -> TCM Term
- newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM Term
- newValueMeta :: RunMetaOccursCheck -> Type -> TCM Term
- newValueMetaCtx :: RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM Term
- newValueMeta' :: RunMetaOccursCheck -> Type -> TCM Term
- newValueMetaCtx' :: RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM Term
- newTelMeta :: Telescope -> TCM Args
- type Condition = Dom Type -> Abs Type -> Bool
- trueCondition :: Condition
- newArgsMeta :: Type -> TCM Args
- newArgsMeta' :: Condition -> Type -> TCM Args
- newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
- newArgsMetaCtx' :: Condition -> Type -> Telescope -> Permutation -> Args -> TCM Args
- newRecordMeta :: QName -> Args -> TCM Term
- newRecordMetaCtx :: QName -> Args -> Telescope -> Permutation -> Args -> TCM Term
- newQuestionMark :: InteractionId -> Type -> TCM Term
- blockTerm :: Type -> TCM Term -> TCM Term
- blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term
- blockTypeOnProblem :: Type -> ProblemId -> TCM Type
- unblockedTester :: Type -> TCM Bool
- postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
- postponeTypeCheckingProblem :: TypeCheckingProblem -> TCM Bool -> TCM Term
- problemType :: TypeCheckingProblem -> TCM Type
- etaExpandListeners :: MetaId -> TCM ()
- wakeupListener :: Listener -> TCM ()
- etaExpandMetaSafe :: MetaId -> TCM ()
- data MetaKind
- allMetaKinds :: [MetaKind]
- etaExpandMeta :: [MetaKind] -> MetaId -> TCM ()
- etaExpandBlocked :: Reduce t => Blocked t -> TCM (Blocked t)
- assignV :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
- assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM ()
- assign :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
- assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
- assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
- subtypingForSizeLt :: CompareDirection -> MetaId -> MetaVariable -> Type -> Args -> Term -> (Term -> TCM ()) -> TCM ()
- expandProjectedVars :: (Normalise a, TermLike a, Show a, PrettyTCM a, NoProjectedVar a, Subst Term a, PrettyTCM b, Subst Term b) => a -> b -> (a -> b -> TCM c) -> TCM c
- etaExpandProjectedVar :: (PrettyTCM a, Subst Term a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
- class NoProjectedVar a where
- noProjectedVar :: a -> Either ProjVarExc ()
- data ProjVarExc = ProjVarExc Int [QName]
- type FVs = VarSet
- type SubstCand = [(Nat, Term)]
- checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
- type Res = [(Arg Nat, Term)]
- data InvertExcept
- = CantInvert
- | NeutralArg
- | ProjectedVar Int [QName]
- inverseSubst :: Args -> ExceptT InvertExcept TCM SubstCand
- updateMeta :: MetaId -> Term -> TCM ()
- allMetas :: TermLike a => a -> [MetaId]
Documentation
findIdx :: Eq a => [a] -> a -> Maybe Int Source
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 Source
Check whether a meta variable is a place holder for a blocked term.
Performing the assignment
assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM () Source
Skip frozen check. Used for eta expanding frozen metas.
Creating meta variables.
newSortMeta :: TCM Sort Source
newSortMetaCtx :: Args -> TCM Sort Source
newTypeMeta :: Sort -> TCM Type Source
newIFSMeta :: MetaNameSuggestion -> Type -> Maybe [Candidate] -> TCM Term Source
newIFSMeta s t cands
creates a new "implicit from scope" metavariable
of type the output type of t
with name suggestion s
and initial
solution candidates cands
. If t
is a function type, then insert enough
lambdas in front of it.
newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> Maybe [Candidate] -> TCM Term Source
Create a new value meta with specific dependencies.
newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM Term Source
newValueMeta :: RunMetaOccursCheck -> Type -> TCM Term Source
Create a new metavariable, possibly η-expanding in the process.
newValueMetaCtx :: RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM Term Source
newValueMeta' :: RunMetaOccursCheck -> Type -> TCM Term Source
Create a new value meta without η-expanding.
newValueMetaCtx' :: RunMetaOccursCheck -> Type -> Telescope -> Permutation -> Args -> TCM Term Source
Create a new value meta with specific dependencies.
newTelMeta :: Telescope -> TCM Args Source
newArgsMeta :: Type -> TCM Args Source
newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args Source
newArgsMetaCtx' :: Condition -> Type -> Telescope -> Permutation -> Args -> TCM Args Source
newRecordMeta :: QName -> Args -> TCM Term Source
Create a metavariable of record type. This is actually one metavariable for each field.
newRecordMetaCtx :: QName -> Args -> Telescope -> Permutation -> Args -> TCM Term Source
newQuestionMark :: InteractionId -> Type -> TCM Term Source
blockTerm :: Type -> TCM Term -> TCM Term Source
Construct a blocked constant if there are constraints.
unblockedTester :: Type -> TCM Bool Source
unblockedTester t
returns False
if t
is a meta or a blocked term.
Auxiliary function to create a postponed type checking problem.
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term Source
Create a postponed type checking problem e : t
that waits for type t
to unblock (become instantiated or its constraints resolved).
postponeTypeCheckingProblem :: TypeCheckingProblem -> TCM Bool -> TCM Term Source
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.
problemType :: TypeCheckingProblem -> TCM Type Source
Type of the term that is produced by solving the TypeCheckingProblem
.
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 :: CompareDirection -> 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.
assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM () Source
assign :: CompareDirection -> MetaId -> Args -> Term -> TCM () Source
Miller pattern unification:
assign x vs v
solves problem x vs = v
for meta x
if vs
are distinct variables (linearity check)
and v
depends only on these variables
and does not contain x
itself (occurs check).
This is the basic story, but we have added some features:
- Pruning.
- Benign cases of non-linearity.
vs
may contain record patterns.
For a reference to some of these extensions, read Andreas Abel and Brigitte Pientka's TLCA 2011 paper.
assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM () Source
assignMeta m x t ids u
solves x ids = u
for meta x
of type t
,
where term u
lives in a context of length m
.
Precondition: ids
is linear.
assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM () Source
assignMeta' m x t ids u
solves x = [ids]u
for meta x
of type t
,
where term u
lives in a context of length m
,
and ids
is a partial substitution.
:: CompareDirection | dir |
-> MetaId | The meta variable |
-> MetaVariable | Its associated information |
-> Type | Its type |
-> Args | Its arguments. |
-> Term | Its to-be-assigned value |
-> (Term -> TCM ()) | Continuation taking its possibly assigned value. |
-> TCM () |
Turn the assignment problem _X args <= SizeLt u
into
_X args = SizeLt (_Y args)
and constraint
_Y args <= u
.
expandProjectedVars :: (Normalise a, TermLike a, Show a, PrettyTCM a, NoProjectedVar a, Subst Term a, PrettyTCM b, Subst Term b) => a -> b -> (a -> b -> TCM c) -> TCM c Source
Eta-expand bound variables like z
in X (fst z)
.
etaExpandProjectedVar :: (PrettyTCM a, Subst Term a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c Source
Eta-expand a de Bruijn index of record type in context and passed term(s).
class NoProjectedVar a where Source
Check whether one of the meta args is a projected var.
noProjectedVar :: a -> Either ProjVarExc () Source
NoProjectedVar Term Source | |
NoProjectedVar a => NoProjectedVar [a] Source | |
NoProjectedVar a => NoProjectedVar (Arg a) Source |
data ProjVarExc Source
checkLinearity :: SubstCand -> ExceptT () TCM SubstCand Source
Turn non-det substitution into proper substitution, if possible. Otherwise, raise the error.
data InvertExcept Source
Exceptions raised when substitution cannot be inverted.
CantInvert | Cannot recover. |
NeutralArg | A potentially neutral arg: can't invert, but can try pruning. |
ProjectedVar Int [QName] | Try to eta-expand var to remove projs. |
inverseSubst :: Args -> ExceptT InvertExcept TCM 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 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.