[−][src]Trait chalk_engine::context::Context
The "context" in which the SLG solver operates. It defines all the types that the SLG solver may need to refer to, as well as a few very simple interconversion methods.
At any given time, the SLG solver may have more than one context
active. First, there is always the global context, but when we
are in the midst of pursuing some particular strand, we will
instantiate a second context just for that work, via the
instantiate_ucanonical_goal and instantiate_ex_clause methods.
In the chalk implementation, these two contexts are mapped to the same type. But in the rustc implementation, this second context corresponds to a fresh arena, and data allocated in that second context will be freed once the work is done. (The "canonicalizing" steps offer a way to convert data from the inference context back into the global context.)
FIXME: Clone and Debug bounds are just for easy derive, they are not actually necessary. But dang are they convenient.
Associated Types
type CanonicalExClause: Debug
type UniverseMap: Clone + Debug
A map between universes. These are produced when u-canonicalizing something; they map canonical results back to the universes from the original.
type InferenceNormalizedSubst: Debug
Extracted from a canonicalized substitution or canonicalized ex clause, this is the type of substitution that is fully normalized with respect to inference variables.
type CanonicalGoalInEnvironment: Debug
A canonicalized GoalInEnvironment -- that is, one where all
free inference variables have been bound into the canonical
binder. See the rustc-dev-guide for more information.
type UCanonicalGoalInEnvironment: Debug + Clone + Eq + Hash
A u-canonicalized GoalInEnvironment -- this is one where the
free universes are renumbered to consecutive integers starting
from U1 (but preserving their relative order).
type Solution
A final solution that is passed back to the user. This is
completely opaque to the SLG solver; it is produced by
make_solution.
type CanonicalConstrainedSubst: Clone + Debug + Eq + Hash
Part of a complete answer: the canonical version of a substitution and region constraints but without any delayed literals.
type CanonicalAnswerSubst: Clone + Debug + Eq + Hash
Part of an answer: the canonical version of a substitution, region constraints, and delayed literals.
type Substitution: Clone + Debug
Represents a substitution from the "canonical variables" found in a canonical goal to specific values.
type RegionConstraint: Clone + Debug
Represents a region constraint that will be propagated back (but not verified).
type GoalInEnvironment: Debug + Clone + Eq + Hash
Represents a goal along with an environment.
type InferenceTable: InferenceTable<Self> + Clone
Represents an inference table.
type Environment: Debug + Clone
Represents a set of hypotheses that are assumed to be true.
type Goal: Clone + Debug + Eq
Goals correspond to things we can prove.
type DomainGoal: Debug
A goal that can be targeted by a program clause. The SLG
solver treats these opaquely; in contrast, it understands
"meta" goals like G1 && G2 and so forth natively.
type BindersGoal: Debug
A "higher-order" goal, quantified over some types and/or
lifetimes. When you have a quantification, like forall<T> { G } or exists<T> { G }, this represents the <T> { G } part.
(In Lambda Prolog, this would be a "lambda predicate", like T \ Goal).
type Parameter: Debug
A term that can be quantified over and unified -- in current Chalk, either a type or lifetime.
type ProgramClause: Debug
A rule like DomainGoal :- Goal.
resolvent_clause combines a program-clause and a concrete
goal we are trying to solve to produce an ex-clause.
type ProgramClauses: Debug
A vector of program clauses.
type Variance
How to relate two kinds when unifying: for example in rustc, we may want to unify parameters either for the sub-typing relation or for the equality relation.
type Interner
The type used to store concrete representations of "core types" from chalk-ir.
Required methods
fn goal_in_environment(
environment: &Self::Environment,
goal: Self::Goal
) -> Self::GoalInEnvironment
environment: &Self::Environment,
goal: Self::Goal
) -> Self::GoalInEnvironment
Given an environment and a goal, glue them together to create
a GoalInEnvironment.
fn inference_normalized_subst_from_ex_clause(
canon_ex_clause: &Self::CanonicalExClause
) -> &Self::InferenceNormalizedSubst
canon_ex_clause: &Self::CanonicalExClause
) -> &Self::InferenceNormalizedSubst
Extracts the inner normalized substitution from a canonical ex-clause.
fn inference_normalized_subst_from_subst(
canon_ex_clause: &Self::CanonicalAnswerSubst
) -> &Self::InferenceNormalizedSubst
canon_ex_clause: &Self::CanonicalAnswerSubst
) -> &Self::InferenceNormalizedSubst
Extracts the inner normalized substitution from a canonical constraint subst.
fn empty_constraints(ccs: &Self::CanonicalAnswerSubst) -> bool
True if this solution has no region constraints.
fn canonical(
u_canon: &Self::UCanonicalGoalInEnvironment
) -> &Self::CanonicalGoalInEnvironment
u_canon: &Self::UCanonicalGoalInEnvironment
) -> &Self::CanonicalGoalInEnvironment
fn has_delayed_subgoals(canonical_subst: &Self::CanonicalAnswerSubst) -> bool
fn num_universes(_: &Self::UCanonicalGoalInEnvironment) -> usize
fn canonical_constrained_subst_from_canonical_constrained_answer(
canonical_subst: &Self::CanonicalAnswerSubst
) -> Self::CanonicalConstrainedSubst
canonical_subst: &Self::CanonicalAnswerSubst
) -> Self::CanonicalConstrainedSubst
fn goal_from_goal_in_environment(goal: &Self::GoalInEnvironment) -> &Self::Goal
fn next_subgoal_index(ex_clause: &ExClause<Self>) -> usize
Selects the next appropriate subgoal index for evaluation. Used by: logic