Struct chalk_solve::clauses::builder::ClauseBuilder
source · 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>>,
}
Expand description
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§
source§impl<'me, I: Interner> ClauseBuilder<'me, I>
impl<'me, I: Interner> ClauseBuilder<'me, I>
pub fn new( db: &'me dyn RustIrDatabase<I>, clauses: &'me mut Vec<ProgramClause<I>>, ) -> Self
sourcepub fn push_fact(&mut self, consequence: impl CastTo<DomainGoal<I>>)
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
).
sourcepub fn push_fact_with_priority(
&mut self,
consequence: impl CastTo<DomainGoal<I>>,
constraints: impl IntoIterator<Item = InEnvironment<Constraint<I>>>,
priority: ClausePriority,
)
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
).
sourcepub fn push_clause(
&mut self,
consequence: impl CastTo<DomainGoal<I>>,
conditions: impl IntoIterator<Item = impl CastTo<Goal<I>>>,
)
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>>>, )
sourcepub 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,
)
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
).
sourcepub fn placeholders_in_scope(&self) -> &[GenericArg<I>]
pub fn placeholders_in_scope(&self) -> &[GenericArg<I>]
Accesses the placeholders for the current list of parameters in scope.
sourcepub fn substitution_in_scope(&self) -> Substitution<I>
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
.
sourcepub fn push_binders<R, V>(
&mut self,
binders: Binders<V>,
op: impl FnOnce(&mut Self, V) -> R,
) -> R
pub fn push_binders<R, V>( &mut self, binders: Binders<V>, op: impl FnOnce(&mut Self, V) -> R, ) -> R
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.
sourcepub fn push_bound_ty(&mut self, op: impl FnOnce(&mut Self, Ty<I>))
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.
sourcepub fn push_bound_lifetime(&mut self, op: impl FnOnce(&mut Self, Lifetime<I>))
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
Auto Trait Implementations§
impl<'me, I> Freeze for ClauseBuilder<'me, I>
impl<'me, I> !RefUnwindSafe for ClauseBuilder<'me, I>
impl<'me, I> !Send for ClauseBuilder<'me, I>
impl<'me, I> !Sync for ClauseBuilder<'me, I>
impl<'me, I> Unpin for ClauseBuilder<'me, I>
impl<'me, I> !UnwindSafe for ClauseBuilder<'me, I>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
source§impl<T> Cast for T
impl<T> Cast for T
source§fn cast<U>(self, interner: <U as HasInterner>::Interner) -> Uwhere
Self: CastTo<U>,
U: HasInterner,
fn cast<U>(self, interner: <U as HasInterner>::Interner) -> Uwhere
Self: CastTo<U>,
U: HasInterner,
U
using CastTo
.