Struct chalk_solve::clauses::builder::ClauseBuilder

pub struct ClauseBuilder<'me, I: Interner> {
    pub db: &'me dyn RustIrDatabase<I>,
    clauses: &'me mut Vec<ProgramClause<I>>,
    binders: Vec<VariableKind<I>>,
    parameters: Vec<GenericArg<I>>,
}

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>

clauses: &'me mut Vec<ProgramClause<I>>

binders: Vec<VariableKind<I>>

parameters: Vec<GenericArg<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) -> R ) -> R

where V: TypeFoldable<I> + HasInterner<Interner = I> + 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) -> I