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>

source

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

source

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).

source

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).

source

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).

source

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

source

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).

source

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

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

source

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.

source

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.

source

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.

source

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.

source

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> Any for T
where T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for T
where T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T> Cast for T

source§

fn cast<U>(self, interner: <U as HasInterner>::Interner) -> U
where Self: CastTo<U>, U: HasInterner,

Cast a value to type U using CastTo.
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T> Instrument for T

§

fn instrument(self, span: Span) -> Instrumented<Self>

Instruments this type with the provided [Span], returning an Instrumented wrapper. Read more
§

fn in_current_span(self) -> Instrumented<Self>

Instruments this type with the current Span, returning an Instrumented wrapper. Read more
source§

impl<T, U> Into<U> for T
where U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T> WithSubscriber for T

§

fn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self>
where S: Into<Dispatch>,

Attaches the provided Subscriber to this type, returning a [WithDispatch] wrapper. Read more
§

fn with_current_subscriber(self) -> WithDispatch<Self>

Attaches the current default Subscriber to this type, returning a [WithDispatch] wrapper. Read more