Trait chalk_engine::context::Context[−][src]

pub trait Context: Clone + Debug {
    type CanonicalExClause: Debug;
    type UniverseMap: Clone + Debug;
    type InferenceNormalizedSubst: Debug;
    type CanonicalGoalInEnvironment: Debug;
    type UCanonicalGoalInEnvironment: Debug + Clone + Eq + Hash;
    type Solution;
    type CanonicalConstrainedSubst: Clone + Debug + Eq + Hash;
    type Substitution: Debug;
    type RegionConstraint: Debug;
    type GoalInEnvironment: Debug + Clone + Eq + Hash;
    type Environment: Debug + Clone;
    type Goal: Clone + Debug + Eq;
    type DomainGoal: Debug;
    type BindersGoal: Debug;
    type Parameter: Debug;
    type ProgramClause: Debug;
    type ProgramClauses: Debug;
    type UnificationResult;
    fn goal_in_environment(
        environment: &Self::Environment, 
        goal: Self::Goal
    ) -> Self::GoalInEnvironment;

    fn into_goal(domain_goal: Self::DomainGoal) -> Self::Goal;

    fn cannot_prove() -> Self::Goal;
}

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

A map between universes. These are produced when u-canonicalizing something; they map canonical results back to the universes from the original.

Extracted from a canonicalized substitution or canonicalized ex clause, this is the type of substitution that is fully normalized with respect to inference variables.

A canonicalized GoalInEnvironment -- that is, one where all free inference variables have been bound into the canonical binder. See the rustc-guide for more information.

A u-canonicalized GoalInEnvironment -- this is one where the free universes are renumbered to consecutive integers starting from U1 (but preserving their relative order).

A final solution that is passed back to the user. This is completely opaque to the SLG solver; it is produced by make_solution.

Part of an answer: represents a canonicalized substitution, combined with region constraints. See the rustc-guide for more information.

Represents a substitution from the "canonical variables" found in a canonical goal to specific values.

Represents a region constraint that will be propagated back (but not verified).

Represents a goal along with an environment.

Represents a set of hypotheses that are assumed to be true.

Goals correspond to things we can prove.

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.

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).

A term that can be quantified over and unified -- in current Chalk, either a type or lifetime.

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.

A vector of program clauses.

The successful result from unification: contains new subgoals and things that can be attached to an ex-clause.

Required Methods

Given an environment and a goal, glue them together to create a GoalInEnvironment.

Upcast this domain goal into a more general goal.

Create a "cannot prove" goal (see HhGoal::CannotProve).

Implementors