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
sourceimpl<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 =)
sourceimpl<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”).
sourceimpl<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.
Auto Trait Implementations
impl<I> RefUnwindSafe for Forest<I> where
<I as Interner>::InternedCanonicalVarKinds: RefUnwindSafe,
<I as Interner>::InternedConstraints: RefUnwindSafe,
<I as Interner>::InternedGoal: RefUnwindSafe,
<I as Interner>::InternedLifetime: RefUnwindSafe,
<I as Interner>::InternedProgramClauses: RefUnwindSafe,
<I as Interner>::InternedSubstitution: RefUnwindSafe,
<I as Interner>::InternedType: RefUnwindSafe,
impl<I> Send for Forest<I> where
<I as Interner>::InternedCanonicalVarKinds: Send,
<I as Interner>::InternedConstraints: Send,
<I as Interner>::InternedGoal: Send,
<I as Interner>::InternedLifetime: Send,
<I as Interner>::InternedProgramClauses: Send,
<I as Interner>::InternedSubstitution: Send,
<I as Interner>::InternedType: Send,
impl<I> Sync for Forest<I> where
<I as Interner>::InternedCanonicalVarKinds: Sync,
<I as Interner>::InternedConstraints: Sync,
<I as Interner>::InternedGoal: Sync,
<I as Interner>::InternedLifetime: Sync,
<I as Interner>::InternedProgramClauses: Sync,
<I as Interner>::InternedSubstitution: Sync,
<I as Interner>::InternedType: Sync,
impl<I> Unpin for Forest<I> where
<I as Interner>::InternedCanonicalVarKinds: Unpin,
<I as Interner>::InternedConstraints: Unpin,
<I as Interner>::InternedGoal: Unpin,
<I as Interner>::InternedLifetime: Unpin,
<I as Interner>::InternedProgramClauses: Unpin,
<I as Interner>::InternedSubstitution: Unpin,
<I as Interner>::InternedType: Unpin,
impl<I> UnwindSafe for Forest<I> where
<I as Interner>::InternedCanonicalVarKinds: UnwindSafe,
<I as Interner>::InternedConstraints: UnwindSafe,
<I as Interner>::InternedGoal: UnwindSafe,
<I as Interner>::InternedLifetime: UnwindSafe,
<I as Interner>::InternedProgramClauses: UnwindSafe,
<I as Interner>::InternedSubstitution: UnwindSafe,
<I as Interner>::InternedType: UnwindSafe,
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
sourceimpl<T> Cast for T
impl<T> Cast for T
sourcefn cast<U>(self, interner: <U as HasInterner>::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
fn cast<U>(self, interner: <U as HasInterner>::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
Cast a value to type U
using CastTo
.
sourceimpl<T> Instrument for T
impl<T> Instrument for T
sourcefn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
sourcefn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
sourceimpl<T> WithSubscriber for T
impl<T> WithSubscriber for T
sourcefn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self> where
S: Into<Dispatch>,
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
sourcefn with_current_subscriber(self) -> WithDispatch<Self>
fn with_current_subscriber(self) -> WithDispatch<Self>
Attaches the current default Subscriber
to this type, returning a
WithDispatch
wrapper. Read more