Struct chalk_solve::goal_builder::GoalBuilder

pub struct GoalBuilder<'i, I: Interner> {
    db: &'i dyn RustIrDatabase<I>,
}

Fields

db: &'i dyn RustIrDatabase<I>

Implementations

impl<'i, I: Interner> GoalBuilder<'i, I>

pub fn new(db: &'i dyn RustIrDatabase<I>) -> Self

pub fn db(&self) -> &'i dyn RustIrDatabase<I>

Returns the database within the goal builder.

pub fn interner(&self) -> I

Returns the interner within the goal builder.

pub fn all<GS, G>(&mut self, goals: GS) -> Goal<I>

where GS: IntoIterator<Item = G>, G: CastTo<Goal<I>>,

Creates a goal that ensures all of the goals from the goals iterator are met (e.g., goals[0] && ... && goals[N]).

pub fn implies<CS, C, G>( &mut self, clauses: CS, goal: impl FnOnce(&mut Self) -> G, ) -> Goal<I>

where CS: IntoIterator<Item = C>, C: CastTo<ProgramClause<I>>, G: CastTo<Goal<I>>,

Creates a goal clauses => goal. The clauses are given as an iterator and the goal is returned via the contained closure.

pub fn forall<G, B, P>( &mut self, binders: &Binders<B>, passthru: P, body: fn(_: &mut Self, _: Substitution<I>, _: &B, _: P) -> G, ) -> Goal<I>

where B: HasInterner<Interner = I>, P: TypeFoldable<I>, G: CastTo<Goal<I>>,

Given a bound value binders like <P0..Pn> V, creates a goal forall<Q0..Qn> { G } where the goal G is created by invoking a helper function body.

Parameters to body

body will be invoked with:

• the goal builder self
• the substitution Q0..Qn
• the bound value [P0..Pn => Q0..Qn] V instantiated with the substitution
• the value passthru, appropriately shifted so that any debruijn indices within account for the new binder

Why is body a function and not a closure?

This is to ensure that body doesn’t accidentally reference values from the environment whose debruijn indices do not account for the new binder being created.

pub fn exists<G, B, P>( &mut self, binders: &Binders<B>, passthru: P, body: fn(_: &mut Self, _: Substitution<I>, _: &B, _: P) -> G, ) -> Goal<I>

where B: HasInterner<Interner = I>, P: TypeFoldable<I>, G: CastTo<Goal<I>>,

Like GoalBuilder::forall, but for a exists<Q0..Qn> { G } goal.

fn quantified<G, B, P>( &mut self, quantifier_kind: QuantifierKind, binders: &Binders<B>, passthru: P, body: fn(_: &mut Self, _: Substitution<I>, _: &B, _: P) -> G, ) -> Goal<I>

where B: HasInterner<Interner = I>, P: TypeFoldable<I>, G: CastTo<Goal<I>>,

A combined helper functon for the various methods to create forall and exists goals. See:

• GoalBuilder::forall
• GoalBuilder::exists

for details.