Struct chalk_engine::forest::Forest

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

impl<I: Interner> Forest<I>

pub fn new() -> Self

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

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

impl<I: Interner> Forest<I>

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.

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

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

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

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.

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.

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.

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.

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

impl<I: Interner> Forest<I>

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.