Struct chalk_solve::goal_builder::GoalBuilder

pub struct GoalBuilder<'i, I: Interner> { /* fields omitted */ }

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 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::Result) -> G
) -> Goal<I> where
    B: HasInterner<Interner = I>,
    P: Fold<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::Result) -> G
) -> Goal<I> where
    B: HasInterner<Interner = I>,
    P: Fold<I>,
    G: CastTo<Goal<I>>, 

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