Struct chalk_recursive::fulfill::Fulfill

pub(crate) struct Fulfill<'s, I: Interner, Solver: SolveDatabase<I>> {
    solver: &'s mut Solver,
    subst: Substitution<I>,
    infer: InferenceTable<I>,
    obligations: Vec<Obligation<I>>,
    constraints: FxHashSet<InEnvironment<Constraint<I>>>,
    cannot_prove: bool,
}

A Fulfill is where we actually break down complex goals, instantiate variables, and perform inference. It’s highly stateful. It’s generally used in Chalk to try to solve a goal, and then package up what was learned in a stateless, canonical way.

In rustc, you can think of there being an outermost Fulfill that’s used when type checking each function body, etc. There, the state reflects the state of type inference in general. But when solving trait constraints, fresh Fulfill instances will be created to solve canonicalized, free-standing goals, and transport what was learned back to the outer context.

Fields

solver: &'s mut Solver

subst: Substitution<I>

infer: InferenceTable<I>

obligations: Vec<Obligation<I>>

The remaining goals to prove or refute

constraints: FxHashSet<InEnvironment<Constraint<I>>>

Lifetime constraints that must be fulfilled for a solution to be fully validated.

cannot_prove: bool

Record that a goal has been processed that can neither be proved nor refuted. In such a case the solution will be either CannotProve, or Err in the case where some other goal leads to an error.

Implementations

impl<'s, I: Interner, Solver: SolveDatabase<I>> Fulfill<'s, I, Solver>

pub(crate) fn new_with_clause( solver: &'s mut Solver, infer: InferenceTable<I>, subst: Substitution<I>, canonical_goal: InEnvironment<DomainGoal<I>>, clause: &Binders<ProgramClauseImplication<I>> ) -> Fallible<Self>

pub(crate) fn new_with_simplification( solver: &'s mut Solver, infer: InferenceTable<I>, subst: Substitution<I>, canonical_goal: InEnvironment<Goal<I>> ) -> Fallible<Self>

fn push_obligation(&mut self, obligation: Obligation<I>)

pub(crate) fn unify<T>( &mut self, environment: &Environment<I>, variance: Variance, a: &T, b: &T ) -> Fallible<()>

where T: ?Sized + Zip<I> + Debug,

Unifies a and b in the given environment.

Wraps InferenceTable::unify; any resulting normalizations are added into our list of pending obligations with the given environment.

pub(crate) fn push_goal( &mut self, environment: &Environment<I>, goal: Goal<I> ) -> Fallible<()>

Create obligations for the given goal in the given environment. This may ultimately create any number of obligations.

fn prove( &mut self, wc: InEnvironment<Goal<I>>, minimums: &mut Minimums, should_continue: impl Fn() -> bool + Clone ) -> Fallible<PositiveSolution<I>>

fn refute( &mut self, goal: InEnvironment<Goal<I>>, should_continue: impl Fn() -> bool + Clone ) -> Fallible<NegativeSolution>

fn apply_solution( &mut self, free_vars: Vec<GenericArg<I>>, universes: UniverseMap, subst: Canonical<ConstrainedSubst<I>> )

Trying to prove some goal led to a the substitution subst; we wish to apply that substitution to our own inference variables (and incorporate any region constraints). This substitution requires some mapping to get it into our namespace – first, the universes it refers to have been canonicalized, and universes stores the mapping back into our universes. Second, the free variables that appear within can be mapped into our variables with free_vars.

fn fulfill( &mut self, minimums: &mut Minimums, should_continue: impl Fn() -> bool + Clone ) -> Fallible<Outcome>

pub(crate) fn solve( self, minimums: &mut Minimums, should_continue: impl Fn() -> bool + Clone ) -> Fallible<Solution<I>>

Try to fulfill all pending obligations and build the resulting solution. The returned solution will transform subst substitution with the outcome of type inference by updating the replacements it provides.

fn interner(&self) -> I