Struct chalk_engine::forest::Forest

source ·
pub(crate) struct Forest<I: Interner> {
    pub(crate) tables: Tables<I>,
    pub(crate) clock: TimeStamp,
}

Fields§

§tables: Tables<I>§clock: TimeStamp

This is a clock which always increases. It is incremented every time a new subgoal is followed. This effectively gives us way to track what depth and loop a table or strand was last followed.

Implementations§

source§

impl<I: Interner> Forest<I>

source

pub fn new() -> Self

source

pub(crate) fn increment_clock(&mut self) -> TimeStamp

source

pub fn iter_answers<'f>( &'f mut self, context: &'f SlgContextOps<'f, I>, goal: &UCanonical<InEnvironment<Goal<I>>>, ) -> impl AnswerStream<I> + 'f

Returns a “solver” for a given goal in the form of an iterator. Each time you invoke next, it will do the work to extract one more answer. These answers are cached in between invocations. Invoking next fewer times is preferable =)

source§

impl<I: Interner> Forest<I>

source

pub(crate) fn root_answer( &mut self, context: &SlgContextOps<'_, I>, table: TableIndex, answer_index: AnswerIndex, ) -> Result<CompleteAnswer<I>, RootSearchFail>

Returns an answer with a given index for the given table. This may require activating a strand and following it. It returns Ok(answer) if they answer is available and otherwise a RootSearchFail result.

source

pub(crate) fn any_future_answer( &self, table: TableIndex, answer_index: AnswerIndex, test: impl FnMut(&Substitution<I>) -> bool, ) -> bool

source

pub(crate) fn answer( &self, table: TableIndex, answer: AnswerIndex, ) -> &Answer<I>

source

fn canonicalize_strand_from( context: &SlgContextOps<'_, I>, infer: &mut InferenceTable<I>, strand: &Strand<I>, ) -> Canonical<Strand<I>>

source

fn get_or_create_table_for_subgoal( &mut self, context: &SlgContextOps<'_, I>, infer: &mut InferenceTable<I>, subgoal: &Literal<I>, ) -> Option<(TableIndex, UniverseMap)>

Given a subgoal, converts the literal into u-canonical form and searches for an existing table. If one is found, it is returned, but otherwise a new table is created (and populated with its initial set of strands).

Returns None if the literal cannot be converted into a table – for example, this can occur when we have selected a negative literal with free existential variables, in which case the execution is said to “flounder”.

In terms of the NFTD paper, creating a new table corresponds to the New Subgoal step as well as the Program Clause Resolution steps.

source

pub(crate) fn get_or_create_table_for_ucanonical_goal( &mut self, context: &SlgContextOps<'_, I>, goal: UCanonical<InEnvironment<Goal<I>>>, ) -> TableIndex

Given a u-canonical goal, searches for an existing table. If one is found, it is returned, but otherwise a new table is created (and populated with its initial set of strands).

In terms of the NFTD paper, creating a new table corresponds to the New Subgoal step as well as the Program Clause Resolution steps.

source

fn build_table( context: &SlgContextOps<'_, I>, table_idx: TableIndex, goal: UCanonical<InEnvironment<Goal<I>>>, ) -> Table<I>

When a table is first created, this function is invoked to create the initial set of strands. If the table represents a domain goal, these strands are created from the program clauses as well as the clauses found in the environment. If the table represents a non-domain goal, such as for<T> G etc, then simplify_goal is invoked to create a strand that breaks the goal down.

In terms of the NFTD paper, this corresponds to the Program Clause Resolution step being applied eagerly, as many times as possible.

source

fn abstract_positive_literal( context: &SlgContextOps<'_, I>, infer: &mut InferenceTable<I>, subgoal: InEnvironment<Goal<I>>, ) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)>

Given a selected positive subgoal, applies the subgoal abstraction function to yield the canonical form that will be used to pick a table. Typically, this abstraction has no effect, and hence we are simply returning the canonical form of subgoal; but if the subgoal is getting too big, we return None, which causes the subgoal to flounder.

source

fn abstract_negative_literal( context: &SlgContextOps<'_, I>, infer: &mut InferenceTable<I>, subgoal: InEnvironment<Goal<I>>, ) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)>

Given a selected negative subgoal, the subgoal is “inverted” (see InferenceTable<I, C>::invert) and then potentially truncated (see abstract_positive_literal). The result subgoal is canonicalized. In some cases, this may return None and hence fail to yield a useful result, for example if free existential variables appear in subgoal (in which case the execution is said to “flounder”).

source§

impl<I: Interner> Forest<I>

source

pub(crate) fn simplify_goal( context: &SlgContextOps<'_, I>, infer: &mut InferenceTable<I>, subst: Substitution<I>, initial_environment: Environment<I>, initial_goal: Goal<I>, ) -> FallibleOrFloundered<ExClause<I>>

Simplifies a goal into a series of positive domain goals and negative goals. This operation may fail if the goal includes unifications that cannot be completed.

Auto Trait Implementations§

§

impl<I> Freeze for Forest<I>

§

impl<I> RefUnwindSafe for Forest<I>
where <I as Interner>::InternedCanonicalVarKinds: RefUnwindSafe, <I as Interner>::InternedGoal: RefUnwindSafe, <I as Interner>::InternedProgramClauses: RefUnwindSafe, <I as Interner>::InternedSubstitution: RefUnwindSafe, <I as Interner>::InternedConstraints: RefUnwindSafe, <I as Interner>::InternedLifetime: RefUnwindSafe, <I as Interner>::InternedType: RefUnwindSafe,

§

impl<I> Send for Forest<I>
where <I as Interner>::InternedCanonicalVarKinds: Send, <I as Interner>::InternedGoal: Send, <I as Interner>::InternedProgramClauses: Send, <I as Interner>::InternedSubstitution: Send, <I as Interner>::InternedConstraints: Send, <I as Interner>::InternedLifetime: Send, <I as Interner>::InternedType: Send,

§

impl<I> Sync for Forest<I>
where <I as Interner>::InternedCanonicalVarKinds: Sync, <I as Interner>::InternedGoal: Sync, <I as Interner>::InternedProgramClauses: Sync, <I as Interner>::InternedSubstitution: Sync, <I as Interner>::InternedConstraints: Sync, <I as Interner>::InternedLifetime: Sync, <I as Interner>::InternedType: Sync,

§

impl<I> Unpin for Forest<I>
where <I as Interner>::InternedCanonicalVarKinds: Unpin, <I as Interner>::InternedGoal: Unpin, <I as Interner>::InternedProgramClauses: Unpin, <I as Interner>::InternedSubstitution: Unpin, <I as Interner>::InternedConstraints: Unpin, <I as Interner>::InternedLifetime: Unpin, <I as Interner>::InternedType: Unpin,

§

impl<I> UnwindSafe for Forest<I>
where <I as Interner>::InternedCanonicalVarKinds: UnwindSafe, <I as Interner>::InternedGoal: UnwindSafe, <I as Interner>::InternedProgramClauses: UnwindSafe, <I as Interner>::InternedSubstitution: UnwindSafe, <I as Interner>::InternedConstraints: UnwindSafe, <I as Interner>::InternedLifetime: UnwindSafe, <I as Interner>::InternedType: UnwindSafe,

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
§

impl<T> Cast for T

§

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