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

pub trait Context: Sized + Clone + Debug + ContextOps<Self> + Aggregate<Self> {
    type Environment: Environment<Self>;
    type Goal: Goal<Self>;
    type DomainGoal: DomainGoal<Self>;
    type UniverseMap: UniverseMap<Self>;
    type GoalInEnvironment: GoalInEnvironment<Self>;
    type CanonicalExClause: Debug + Clone;
    type CanonicalGoalInEnvironment: Debug + Clone;
    type UCanonicalGoalInEnvironment: UCanonicalGoalInEnvironment<Self>;
    type RegionConstraint: ConstraintInEnvironment<Self>;
    type Substitution: Substitution<Self>;
    type CanonicalConstrainedSubst: CanonicalConstrainedSubst<Self>;
    type BindersGoal: BindersGoal<Self>;
    type Parameter: Parameter<Self>;
    type ProgramClause: ProgramClause<Self>;
    type UnificationResult: UnificationResult<Self>;
    type Solution;
}

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.

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

Represents a goal along with an environment.

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

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.

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

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.

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

Implementors