Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- findIdx :: Eq a => [a] -> a -> Maybe Int
- hasTwinMeta :: MetaId -> TCM Bool
- isBlockedTerm :: MetaId -> TCM Bool
- isEtaExpandable :: [MetaClass] -> MetaId -> TCM Bool
- assignTerm :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
- assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
- newSortMetaBelowInf :: TCM Sort
- newSortMeta :: MonadMetaSolver m => m Sort
- newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort
- newTypeMeta' :: Comparison -> Sort -> TCM Type
- newTypeMeta :: Sort -> TCM Type
- newTypeMeta_ :: TCM Type
- newLevelMeta :: MonadMetaSolver m => m Level
- newInstanceMeta :: MonadMetaSolver m => MetaNameSuggestion -> Type -> m (MetaId, Term)
- newInstanceMetaCtx :: MonadMetaSolver m => MetaNameSuggestion -> Type -> Args -> m (MetaId, Term)
- newNamedValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
- newNamedValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
- newValueMetaOfKind :: MonadMetaSolver m => MetaInfo -> RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
- newValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
- newValueMetaCtx :: MonadMetaSolver m => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
- newValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
- newValueMetaCtx' :: MonadMetaSolver m => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
- newTelMeta :: MonadMetaSolver m => Telescope -> m Args
- type Condition = Dom Type -> Abs Type -> Bool
- trueCondition :: Condition
- newArgsMeta :: MonadMetaSolver m => Type -> m Args
- newArgsMeta' :: MonadMetaSolver m => Condition -> Type -> m Args
- newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
- newArgsMetaCtx'' :: MonadMetaSolver m => MetaNameSuggestion -> Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
- newArgsMetaCtx' :: MonadMetaSolver m => Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
- newRecordMeta :: QName -> Args -> TCM Term
- newRecordMetaCtx :: MetaNameSuggestion -> Frozen -> QName -> Args -> Telescope -> Permutation -> Args -> TCM Term
- newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
- newQuestionMark' :: (Comparison -> Type -> TCM (MetaId, Term)) -> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
- blockTerm :: (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m, MonadFresh ProblemId m) => Type -> m Term -> m Term
- blockTermOnProblem :: (MonadMetaSolver m, MonadFresh Nat m) => Type -> Term -> ProblemId -> m Term
- blockTypeOnProblem :: (MonadMetaSolver m, MonadFresh Nat m) => Type -> ProblemId -> m Type
- unblockedTester :: Type -> TCM Blocker
- postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
- postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term
- problemType :: TypeCheckingProblem -> Type
- etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM ()
- etaExpandBlocked :: (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) => Blocked t -> m (Blocked t)
- assignWrapper :: (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m, MonadDebug m, HasOptions m) => CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
- assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
- isInteractionMetaB :: (ReadTCState m, MonadReduce m, MonadPretty m) => MetaId -> Args -> m (Maybe (MetaId, InteractionId, Args))
- assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
- assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
- checkMetaInst :: MetaId -> TCM ()
- checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
- checkSubtypeIsEqual :: Type -> Type -> TCM ()
- subtypingForSizeLt :: CompareDirection -> MetaId -> MetaVariable -> Type -> Args -> Term -> (Term -> TCM ()) -> TCM ()
- expandProjectedVars :: (Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a, PrettyTCM b, TermSubst b) => a -> b -> (a -> b -> TCM c) -> TCM c
- etaExpandProjectedVar :: (PrettyTCM a, TermSubst a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
- class NoProjectedVar a where
- noProjectedVar :: a -> Either ProjectedVar ()
- class (TermLike a, TermSubst a, Reduce a) => ReduceAndEtaContract a where
- reduceAndEtaContract :: a -> TCM a
- type FVs = VarSet
- type SubstCand = [(Int, Term)]
- checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
- type Res = [(Arg Nat, Term)]
- data InvertExcept
- inverseSubst' :: (Term -> Bool) -> Args -> ExceptT InvertExcept TCM SubstCand
- isFaceConstraint :: MetaId -> Args -> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
- tryAddBoundary :: CompareDirection -> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
- openMetasToPostulates :: TCM ()
- dependencySortMetas :: [MetaId] -> TCM (Maybe [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.
hasTwinMeta :: MetaId -> TCM Bool Source #
Does the given local meta-variable have a twin meta-variable?
isBlockedTerm :: MetaId -> TCM Bool Source #
Check whether a meta variable is a place holder for a blocked term.
Performing the assignment
assignTerm :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m () Source #
Performing the meta variable assignment.
The instantiation should not be an InstV
and the MetaId
should point to something Open
or a BlockedConst
.
Further, the meta variable may not be Frozen
.
assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM () Source #
Skip frozen check. Used for eta expanding frozen metas.
Creating meta variables.
newSortMetaBelowInf :: TCM Sort Source #
Create a sort meta that cannot be instantiated with Inf
(Setω).
newSortMeta :: MonadMetaSolver m => m Sort Source #
Create a sort meta that may be instantiated with Inf
(Setω).
newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort Source #
Create a sort meta that may be instantiated with Inf
(Setω).
newTypeMeta' :: Comparison -> Sort -> TCM Type Source #
newTypeMeta_ :: TCM Type Source #
newLevelMeta :: MonadMetaSolver m => m Level Source #
newInstanceMeta :: MonadMetaSolver m => MetaNameSuggestion -> Type -> m (MetaId, Term) Source #
newInstanceMeta s t cands
creates a new instance metavariable
of type the output type of t
with name suggestion s
.
newInstanceMetaCtx :: MonadMetaSolver m => MetaNameSuggestion -> Type -> Args -> m (MetaId, Term) Source #
newNamedValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term) Source #
Create a new value meta with specific dependencies, possibly η-expanding in the process.
newNamedValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term) Source #
Create a new value meta with specific dependencies without η-expanding.
:: MonadMetaSolver m | |
=> MetaInfo | |
-> RunMetaOccursCheck | Ignored for instance metas. |
-> Comparison | Ignored for instance metas. |
-> Type | |
-> m (MetaId, Term) |
newValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term) Source #
Create a new metavariable, possibly η-expanding in the process.
newValueMetaCtx :: MonadMetaSolver m => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term) Source #
newValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term) Source #
Create a new value meta without η-expanding.
newValueMetaCtx' :: MonadMetaSolver m => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term) Source #
newTelMeta :: MonadMetaSolver m => Telescope -> m Args Source #
newArgsMeta :: MonadMetaSolver m => Type -> m Args Source #
newArgsMeta' :: MonadMetaSolver m => Condition -> Type -> m Args Source #
newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args Source #
newArgsMetaCtx'' :: MonadMetaSolver m => MetaNameSuggestion -> Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args Source #
newArgsMetaCtx' :: MonadMetaSolver m => Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args Source #
newRecordMeta :: QName -> Args -> TCM Term Source #
Create a metavariable of record type. This is actually one metavariable for each field.
:: MetaNameSuggestion | Name suggestion to be used as a prefix of the name suggestions for the metas that represent each field |
-> Frozen | Should the meta be created frozen? |
-> QName | Name of record type |
-> Args | Parameters of record type. |
-> Telescope | |
-> Permutation | |
-> Args | |
-> TCM Term |
newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term) Source #
newQuestionMark' :: (Comparison -> Type -> TCM (MetaId, Term)) -> InteractionId -> Comparison -> Type -> TCM (MetaId, Term) Source #
blockTerm :: (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m, MonadFresh ProblemId m) => Type -> m Term -> m Term Source #
Construct a blocked constant if there are constraints.
blockTermOnProblem :: (MonadMetaSolver m, MonadFresh Nat m) => Type -> Term -> ProblemId -> m Term Source #
blockTypeOnProblem :: (MonadMetaSolver m, MonadFresh Nat m) => Type -> ProblemId -> m Type Source #
unblockedTester :: Type -> TCM Blocker Source #
unblockedTester t
returns a Blocker
for t
.
Auxiliary function used when creating 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 -> Blocker -> 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 -> Type Source #
Type of the term that is produced by solving the TypeCheckingProblem
.
etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM () Source #
Eta-expand a local meta-variable, if it is of the specified kind. Don't do anything if the meta-variable is a blocked term.
etaExpandBlocked :: (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) => Blocked t -> m (Blocked t) Source #
Eta expand blocking metavariables of record type, and reduce the blocked thing.
assignWrapper :: (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m, MonadDebug m, HasOptions m) => CompareDirection -> MetaId -> Elims -> Term -> m () -> m () Source #
assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM () Source #
Miller pattern unification:
assign dir x vs v a
solves problem x vs <=(dir) v : a
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.
isInteractionMetaB :: (ReadTCState m, MonadReduce m, MonadPretty m) => MetaId -> Args -> m (Maybe (MetaId, InteractionId, Args)) Source #
Is the given metavariable application secretly an interaction point application? Ugly.
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.
checkMetaInst :: MetaId -> TCM () Source #
Check that the instantiation of the given metavariable fits the type of the metavariable. If the metavariable is not yet instantiated, add a constraint to check the instantiation later.
checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM () Source #
Check that the instantiation of the metavariable with the given term is well-typed.
checkSubtypeIsEqual :: Type -> Type -> TCM () Source #
Given two types a
and b
with a <: b
, check that a == b
.
:: CompareDirection | dir |
-> MetaId | The local 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
.
:: (Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a, PrettyTCM b, TermSubst b) | |
=> a | Meta variable arguments. |
-> b | Right hand side. |
-> (a -> b -> TCM c) | |
-> TCM c |
Eta-expand bound variables like z
in X (fst z)
.
etaExpandProjectedVar :: (PrettyTCM a, TermSubst 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.
Nothing
noProjectedVar :: a -> Either ProjectedVar () Source #
default noProjectedVar :: forall b (t :: Type -> Type). (NoProjectedVar b, Foldable t, t b ~ a) => a -> Either ProjectedVar () Source #
Instances
NoProjectedVar Term Source # | |
Defined in Agda.TypeChecking.MetaVars noProjectedVar :: Term -> Either ProjectedVar () Source # | |
NoProjectedVar a => NoProjectedVar (Arg a) Source # | |
Defined in Agda.TypeChecking.MetaVars noProjectedVar :: Arg a -> Either ProjectedVar () Source # | |
NoProjectedVar a => NoProjectedVar [a] Source # | |
Defined in Agda.TypeChecking.MetaVars noProjectedVar :: [a] -> Either ProjectedVar () Source # |
class (TermLike a, TermSubst a, Reduce a) => ReduceAndEtaContract a where Source #
Normalize just far enough to be able to eta-contract maximally.
Nothing
reduceAndEtaContract :: a -> TCM a Source #
default reduceAndEtaContract :: forall (f :: Type -> Type) b. (Traversable f, TermLike b, Subst b, Reduce b, ReduceAndEtaContract b, f b ~ a) => a -> TCM a Source #
Instances
ReduceAndEtaContract Term Source # | |
Defined in Agda.TypeChecking.MetaVars | |
ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) Source # | |
Defined in Agda.TypeChecking.MetaVars | |
ReduceAndEtaContract a => ReduceAndEtaContract [a] Source # | |
Defined in Agda.TypeChecking.MetaVars reduceAndEtaContract :: [a] -> TCM [a] 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 Term | Cannot recover. |
NeutralArg | A potentially neutral arg: can't invert, but can try pruning. |
ProjVar ProjectedVar | Try to eta-expand var to remove projs. |
inverseSubst' :: (Term -> Bool) -> 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.
isFaceConstraint :: MetaId -> Args -> TCM (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution)) Source #
If the given metavariable application represents a face, return:
- The metavariable information;
- The actual face, as an assignment of booleans to variables;
- The substitution candidate resulting from
inverseSubst'
. This is guaranteed to be linear and deterministic. - The actual substitution, mapping from the constraint context to the metavariable's context.
Put concisely, a face constraint is an equation in the pattern
fragment modulo the presence of endpoints (i0
and i1
) in the
telescope. In more detail, a face constraint has the form
?0 Δ (i = i0) (j = i0) Γ (k = i1) Θ (l = i0) = t
where all the greek letters consist entirely of distinct bound variables (and, of course, arbitrarily many endpoints are allowed between each substitution fragment).
tryAddBoundary :: CompareDirection -> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM () Source #
Record a "face" equation onto an interaction point into the actual
interaction point boundary. Takes all the same arguments as
assignMeta'
.
openMetasToPostulates :: TCM () Source #
Turn open metas into postulates.
Preconditions:
- We are
inTopContext
. envCurrentModule
is set to the top-level module.
Orphan instances
MonadMetaSolver TCM Source # | |
newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId Source # assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM () Source # assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM () Source # etaExpandMeta :: [MetaClass] -> MetaId -> TCM () Source # updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM () Source # speculateMetas :: TCM () -> TCM KeepMetas -> TCM () Source # |