[−][src]Struct chalk_solve::clauses::builder::ClauseBuilder
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>
[src]
pub fn new(
db: &'me dyn RustIrDatabase<I>,
clauses: &'me mut Vec<ProgramClause<I>>
) -> Self
[src]
db: &'me dyn RustIrDatabase<I>,
clauses: &'me mut Vec<ProgramClause<I>>
) -> Self
pub fn push_fact(&mut self, consequence: impl CastTo<DomainGoal<I>>)
[src]
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>>,
priority: ClausePriority
)
[src]
&mut self,
consequence: impl CastTo<DomainGoal<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>>>
)
[src]
&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_clause_with_priority(
&mut self,
consequence: impl CastTo<DomainGoal<I>>,
conditions: impl IntoIterator<Item = impl CastTo<Goal<I>>>,
priority: ClausePriority
)
[src]
&mut self,
consequence: impl CastTo<DomainGoal<I>>,
conditions: impl IntoIterator<Item = impl CastTo<Goal<I>>>,
priority: ClausePriority
)
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 placeholders_in_scope(&self) -> &[GenericArg<I>]
[src]
Accesses the placeholders for the current list of parameters in scope.
pub fn substitution_in_scope(&self) -> Substitution<I>
[src]
Accesses the placeholders for the current list of parameters in scope,
in the form of a Substitution
.
pub fn push_binders<V>(
&mut self,
binders: &Binders<V>,
op: impl FnOnce(&mut Self, V::Result)
) where
V: Fold<I> + HasInterner<Interner = I>,
V::Result: Debug,
[src]
&mut self,
binders: &Binders<V>,
op: impl FnOnce(&mut Self, V::Result)
) 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>))
[src]
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 interner(&self) -> &'me I
[src]
Auto Trait Implementations
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> where
<I as Interner>::InternedGenericArg: Unpin,
<I as Interner>::InternedType: Unpin,
<I as Interner>::InternedGenericArg: Unpin,
<I as Interner>::InternedType: Unpin,
impl<'me, I> !UnwindSafe for ClauseBuilder<'me, I>
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Cast for T
[src]
fn cast<U>(self, interner: &<U as HasInterner>::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
[src]
Self: CastTo<U>,
U: HasInterner,
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,