Struct chalk_recursive::fulfill::Fulfill
source · 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,
}
Expand description
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§
source§impl<'s, I: Interner, Solver: SolveDatabase<I>> Fulfill<'s, I, Solver>
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>)
sourcepub(crate) fn unify<T>(
&mut self,
environment: &Environment<I>,
variance: Variance,
a: &T,
b: &T,
) -> Fallible<()>
pub(crate) fn unify<T>( &mut self, environment: &Environment<I>, variance: Variance, a: &T, b: &T, ) -> Fallible<()>
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.
sourcepub(crate) fn push_goal(
&mut self,
environment: &Environment<I>,
goal: Goal<I>,
) -> Fallible<()>
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>
sourcefn apply_solution(
&mut self,
free_vars: Vec<GenericArg<I>>,
universes: UniverseMap,
subst: Canonical<ConstrainedSubst<I>>,
)
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>
sourcepub(crate) fn solve(
self,
minimums: &mut Minimums,
should_continue: impl Fn() -> bool + Clone,
) -> Fallible<Solution<I>>
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.