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

pub trait InferenceContext<C: Context>: Sized + Debug {
    type Environment: Environment<C, Self>;
    type Goal: Goal<C, Self>;
    type DomainGoal: DomainGoal<C, Self>;
    type GoalInEnvironment: GoalInEnvironment<C, Self>;
    type RegionConstraint: Debug;
    type Substitution: Debug;
    type BindersGoal: Debug;
    type Parameter: Debug;
    type ProgramClause: Debug;
    type UnificationResult: UnificationResult<C, Self>;
}

The set of types belonging to an "inference context"; in rustc, these types are tied to the lifetime of the arena within which an inference context operates.

Associated Types

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.

Represents a goal along with an environment.

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

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

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.

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

Implementors