Struct chalk_solve::clauses::builder::ClauseBuilder

pub struct ClauseBuilder<'me, I: Interner> {
    pub db: &'me dyn RustIrDatabase<I>,
    // some fields omitted
}

The "clause builder" is a useful tool for building up sets of program clauses. It takes ownership of the output vector while it lasts, and offers methods like push_clause and so forth to append to it.

Fields

db: &'me dyn RustIrDatabase<I>

Implementations

impl<'me, I: Interner> ClauseBuilder<'me, I>

pub fn new(
    db: &'me dyn RustIrDatabase<I>,
    clauses: &'me mut Vec<ProgramClause<I>>
) -> Self

pub fn push_fact(&mut self, consequence: impl CastTo<DomainGoal<I>>)

Pushes a "fact" forall<..> { consequence } into the set of program clauses, meaning something that we can assume to be true unconditionally. The forall<..> binders will be whichever binders have been pushed (see push_binders).

pub fn push_fact_with_priority(
    &mut self,
    consequence: impl CastTo<DomainGoal<I>>,
    constraints: impl IntoIterator<Item = InEnvironment<Constraint<I>>>,
    priority: ClausePriority
)

Pushes a "fact" forall<..> { consequence } into the set of program clauses, meaning something that we can assume to be true unconditionally. The forall<..> binders will be whichever binders have been pushed (see push_binders).

pub fn push_clause(
    &mut self,
    consequence: impl CastTo<DomainGoal<I>>,
    conditions: impl IntoIterator<Item = impl CastTo<Goal<I>>>
)

Pushes a clause forall<..> { consequence :- conditions } into the set of program clauses, meaning that consequence can be proven if conditions are all true. The forall<..> binders will be whichever binders have been pushed (see push_binders).

pub fn push_fact_with_constraints(
    &mut self,
    consequence: impl CastTo<DomainGoal<I>>,
    constraints: impl IntoIterator<Item = InEnvironment<Constraint<I>>>
)

pub fn push_clause_with_priority(
    &mut self,
    consequence: impl CastTo<DomainGoal<I>>,
    conditions: impl IntoIterator<Item = impl CastTo<Goal<I>>>,
    constraints: impl IntoIterator<Item = InEnvironment<Constraint<I>>>,
    priority: ClausePriority
)

Pushes a clause forall<..> { consequence :- conditions ; constraints } into the set of program clauses, meaning that consequence can be proven if conditions are all true and constraints are proven to hold. The forall<..> binders will be whichever binders have been pushed (see push_binders).

pub fn placeholders_in_scope(&self) -> &[GenericArg<I>]

Accesses the placeholders for the current list of parameters in scope.

pub fn substitution_in_scope(&self) -> Substitution<I>

Accesses the placeholders for the current list of parameters in scope, in the form of a Substitution.

pub fn push_binders<R, V>(
    &mut self,
    binders: &Binders<V>,
    op: impl FnOnce(&mut Self, V::Result) -> R
) -> R where
    V: Fold<I> + HasInterner<Interner = I>,
    V::Result: Debug, 

Executes op with the binders in-scope; op is invoked with the bound value v as a parameter. After op finishes, the binders are popped from scope.

The new binders are always pushed onto the end of the internal list of binders; this means that any extant values where were created referencing the old list of binders are still valid.

pub fn push_bound_ty(&mut self, op: impl FnOnce(&mut Self, Ty<I>))

Push a single binder, for a type, at the end of the binder list. The indices of previously bound variables are unaffected and hence the context remains usable. Invokes op, passing a type representing this new type variable in as an argument.

pub fn push_bound_lifetime(&mut self, op: impl FnOnce(&mut Self, Lifetime<I>))

Push a single binder, for a lifetime, at the end of the binder list. The indices of previously bound variables are unaffected and hence the context remains usable. Invokes op, passing a lifetime representing this new lifetime variable in as an argument.

pub fn interner(&self) -> &'me I