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

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

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.

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.

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.

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.

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.

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

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

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Cast a value to type U using CastTo.

Returns the argument unchanged.

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

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

Calls U::from(self).

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

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.

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

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