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>

source

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>

source

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

source

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

source

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.

source

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.

source

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

source

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

source

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.

source

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

source

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.

source

fn interner(&self) -> I

Auto Trait Implementations§

§

impl<'s, I, Solver> Freeze for Fulfill<'s, I, Solver>
where <I as Interner>::InternedSubstitution: Freeze,

§

impl<'s, I, Solver> RefUnwindSafe for Fulfill<'s, I, Solver>
where Solver: RefUnwindSafe, <I as Interner>::InternedSubstitution: RefUnwindSafe, I: RefUnwindSafe, <I as Interner>::InternedGoal: RefUnwindSafe, <I as Interner>::InternedProgramClauses: RefUnwindSafe, <I as Interner>::InternedLifetime: RefUnwindSafe, <I as Interner>::InternedType: RefUnwindSafe, <I as Interner>::InternedGenericArg: RefUnwindSafe,

§

impl<'s, I, Solver> Send for Fulfill<'s, I, Solver>
where Solver: Send, <I as Interner>::InternedSubstitution: Send, I: Send, <I as Interner>::InternedGoal: Send, <I as Interner>::InternedProgramClauses: Send, <I as Interner>::InternedLifetime: Send, <I as Interner>::InternedType: Send, <I as Interner>::InternedGenericArg: Send,

§

impl<'s, I, Solver> Sync for Fulfill<'s, I, Solver>
where Solver: Sync, <I as Interner>::InternedSubstitution: Sync, I: Sync, <I as Interner>::InternedGoal: Sync, <I as Interner>::InternedProgramClauses: Sync, <I as Interner>::InternedLifetime: Sync, <I as Interner>::InternedType: Sync, <I as Interner>::InternedGenericArg: Sync,

§

impl<'s, I, Solver> Unpin for Fulfill<'s, I, Solver>
where <I as Interner>::InternedSubstitution: Unpin, I: Unpin, <I as Interner>::InternedGoal: Unpin, <I as Interner>::InternedProgramClauses: Unpin, <I as Interner>::InternedLifetime: Unpin, <I as Interner>::InternedType: Unpin, <I as Interner>::InternedGenericArg: Unpin,

§

impl<'s, I, Solver> !UnwindSafe for Fulfill<'s, I, Solver>

Blanket Implementations§

source§

impl<T> Any for T
where T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for T
where T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
§

impl<T> Cast for T

§

fn cast<U>(self, interner: <U as HasInterner>::Interner) -> U
where Self: CastTo<U>, U: HasInterner,

Cast a value to type U using CastTo.
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T> Instrument for T

§

fn instrument(self, span: Span) -> Instrumented<Self>

Instruments this type with the provided [Span], returning an Instrumented wrapper. Read more
§

fn in_current_span(self) -> Instrumented<Self>

Instruments this type with the current Span, returning an Instrumented wrapper. Read more
source§

impl<T, U> Into<U> for T
where U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T> WithSubscriber for T

§

fn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self>
where S: Into<Dispatch>,

Attaches the provided Subscriber to this type, returning a [WithDispatch] wrapper. Read more
§

fn with_current_subscriber(self) -> WithDispatch<Self>

Attaches the current default Subscriber to this type, returning a [WithDispatch] wrapper. Read more