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>
impl<I: Interner> Forest<I>
pub fn new() -> Self
pub(crate) fn increment_clock(&mut self) -> TimeStamp
sourcepub fn iter_answers<'f>(
&'f mut self,
context: &'f SlgContextOps<'f, I>,
goal: &UCanonical<InEnvironment<Goal<I>>>,
) -> impl AnswerStream<I> + 'f
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>
impl<I: Interner> Forest<I>
sourcepub(crate) fn root_answer(
&mut self,
context: &SlgContextOps<'_, I>,
table: TableIndex,
answer_index: AnswerIndex,
) -> Result<CompleteAnswer<I>, RootSearchFail>
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>>
sourcefn get_or_create_table_for_subgoal(
&mut self,
context: &SlgContextOps<'_, I>,
infer: &mut InferenceTable<I>,
subgoal: &Literal<I>,
) -> Option<(TableIndex, UniverseMap)>
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.
sourcepub(crate) fn get_or_create_table_for_ucanonical_goal(
&mut self,
context: &SlgContextOps<'_, I>,
goal: UCanonical<InEnvironment<Goal<I>>>,
) -> TableIndex
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.
sourcefn build_table(
context: &SlgContextOps<'_, I>,
table_idx: TableIndex,
goal: UCanonical<InEnvironment<Goal<I>>>,
) -> Table<I>
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.
sourcefn abstract_positive_literal(
context: &SlgContextOps<'_, I>,
infer: &mut InferenceTable<I>,
subgoal: InEnvironment<Goal<I>>,
) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)>
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.
sourcefn abstract_negative_literal(
context: &SlgContextOps<'_, I>,
infer: &mut InferenceTable<I>,
subgoal: InEnvironment<Goal<I>>,
) -> Option<(UCanonical<InEnvironment<Goal<I>>>, UniverseMap)>
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>
impl<I: Interner> Forest<I>
sourcepub(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>>
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.