[][src]Struct chalk_engine::forest::Forest

pub struct Forest<C: Context> {
    context: C,
    pub(crate) tables: Tables<C>,
    pub(crate) stack: Stack,
    dfn: DepthFirstNumber,
}

Fields

context: Ctables: Tables<C>stack: Stackdfn: DepthFirstNumber

Methods

impl<C: Context> Forest<C>[src]

pub fn new(context: C) -> Self[src]

pub fn context(&self) -> &C[src]

Gives access to self.context. In fact, the SLG solver doesn't ever use self.context for anything, and only cares about the associated types and methods defined on it. But the creator of the forest can use the context field to store configuration info (e.g., in chalk, we store the max size of a term in here).

pub(super) fn next_dfn(
    &mut self
) -> DepthFirstNumber
[src]

pub fn force_answers(
    &mut self,
    context: &impl ContextOps<C>,
    goal: C::UCanonicalGoalInEnvironment,
    num_answers: usize
) -> Option<Vec<Answer<C>>>
[src]

Finds the first N answers, looping as much as needed to get them. Returns None if the result flounders.

Thanks to subgoal abstraction and so forth, this should always terminate.

fn iter_answers<'f>(
    &'f mut self,
    context: &'f impl ContextOps<C>,
    goal: &C::UCanonicalGoalInEnvironment
) -> impl AnswerStream<C> + 'f
[src]

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

pub fn solve(
    &mut self,
    context: &impl ContextOps<C>,
    goal: &C::UCanonicalGoalInEnvironment
) -> Option<C::Solution>
[src]

Solves a given goal, producing the solution. This will do only as much work towards goal as it has to (and that works is cached for future attempts).

pub(super) fn top_of_stack_is_coinductive_from(
    &self,
    depth: StackIndex
) -> bool
[src]

True if all the tables on the stack starting from depth and continuing until the top of the stack are coinductive.

Example: Given a program like:

struct Foo { a: Option<Box<Bar>> }
struct Bar { a: Option<Box<Foo>> }
trait XXX { }
impl<T: Send> XXX for T { }

and then a goal of Foo: XXX, we would eventually wind up with a stack like this:

StackIndexTable Goal
0Foo: XXX
1Foo: Send
2Bar: Send

Here, the top of the stack is Bar: Send. And now we are asking top_of_stack_is_coinductive_from(1) -- the answer would be true, since Send is an auto trait, which yields a coinductive goal. But top_of_stack_is_coinductive_from(0) is false, since XXX is not an auto trait.

pub fn num_cached_answers_for_goal(
    &mut self,
    context: &impl ContextOps<C>,
    goal: &C::UCanonicalGoalInEnvironment
) -> usize
[src]

Useful for testing.

impl<C: Context> Forest<C>[src]

pub(super) fn ensure_root_answer(
    &mut self,
    context: &impl ContextOps<C>,
    table: TableIndex,
    answer: AnswerIndex
) -> Result<(), RootSearchFail>
[src]

Ensures that answer with the given index is available from the given table. This may require activating a strand. Returns Ok(()) if the answer is available and otherwise a RootSearchFail result.

pub(super) fn any_future_answer(
    &mut self,
    table: TableIndex,
    answer: AnswerIndex,
    test: impl FnMut(&C::InferenceNormalizedSubst) -> bool
) -> bool
[src]

fn ensure_answer_recursively(
    &mut self,
    context: &impl ContextOps<C>,
    table: TableIndex,
    answer: AnswerIndex
) -> Result<EnsureSuccess, RecursiveSearchFail>
[src]

Ensures that answer with the given index is available from the given table. Returns Ok if there is an answer:

  • EnsureSuccess::AnswerAvailable means that the answer is cached in the table (and can be fetched with e.g. self.answer()).
  • EnsureSuccess::Coinductive means that this was a cyclic request of a coinductive goal and is thus considered true; in this case, the answer is not cached in the table (it is only true in this cyclic context).

This function first attempts to fetch answer that is cached in the table. If none is found, then we will if the table is on the stack; if so, that constitutes a cycle (producing a new result for the table X required producing a new result for the table X), and we return a suitable result. Otherwise, we can push the table onto the stack and select the next available strand -- if none are available, then no more answers are possible.

pub(crate) fn answer(
    &self,
    table: TableIndex,
    answer: AnswerIndex
) -> &Answer<C>
[src]

fn pursue_next_strand(
    &mut self,
    context: &impl ContextOps<C>,
    depth: StackIndex
) -> Result<(), RecursiveSearchFail>
[src]

Selects the next eligible strand from the table at depth depth and pursues it. If that strand encounters a cycle, then this function will loop and keep trying strands until it reaches one that did not encounter a cycle; that result is propagated. If all strands return a cycle, then the entire subtree is "completed" by invoking cycle.

fn with_instantiated_strand<R>(
    context: &impl ContextOps<C>,
    num_universes: usize,
    canonical_strand: &CanonicalStrand<C>,
    op: impl WithInstantiatedStrand<C, Output = R>
) -> R
[src]

fn canonicalize_strand(strand: Strand<C, impl Context>) -> CanonicalStrand<C>[src]

fn canonicalize_strand_from<I: Context>(
    infer: &mut dyn InferenceTable<C, I>,
    ex_clause: &ExClause<I>,
    selected_subgoal: Option<SelectedSubgoal<C>>
) -> CanonicalStrand<C>
[src]

fn cycle(
    &mut self,
    context: &impl ContextOps<C>,
    depth: StackIndex,
    strands: Vec<CanonicalStrand<C>>,
    minimums: Minimums
) -> Option<RecursiveSearchFail>
[src]

Invoked when all available strands for a table have encountered a cycle. In this case, the vector strands are the set of strands that encountered cycles, and minimums is the minimum stack depths that they were dependent on.

Returns None if we have resolved the cycle and should try to pick a strand again. Returns Some(_) if the cycle indicates an error that we can propagate higher up.

fn clear_strands_after_cycle(
    &mut self,
    table: TableIndex,
    strands: impl IntoIterator<Item = CanonicalStrand<C>>
)
[src]

Invoked after we have determined that every strand in table encounters a cycle; strands is the set of strands (which have been moved out of the table). This method then recursively clears the active strands from the tables referenced in strands, since all of them must encounter cycles too.

fn delay_strands_after_cycle(
    &mut self,
    context: &impl ContextOps<C>,
    table: TableIndex,
    visited: &mut FxHashSet<TableIndex>
)
[src]

Invoked after we have determined that every strand in table encounters a cycle, and that some of those cycles involve negative edges. In that case, walks all negative edges and converts them to delayed literals.

fn delay_strand_after_cycle(
    table: TableIndex,
    strand: Strand<C, impl Context>
) -> (CanonicalStrand<C>, TableIndex)
[src]

fn pursue_strand(
    &mut self,
    context: &impl ContextOps<C>,
    depth: StackIndex,
    strand: Strand<C, impl Context>
) -> Result<(), StrandFail<C>>
[src]

Pursues strand to see if it leads us to a new answer, either by selecting a new subgoal or by checking to see if the selected subgoal has an answer. strand is associated with the table on the stack at the given depth.

fn pursue_answer(
    &mut self,
    depth: StackIndex,
    strand: Strand<C, impl Context>
) -> Result<(), StrandFail<C>>
[src]

Invoked when a strand represents an answer. This means that the strand has no subgoals left. There are two possibilities:

  • the strand may represent an answer we have already found; in that case, we can return StrandFail::NoSolution, as this strand led nowhere of interest.
  • the strand may represent a new answer, in which case it is added to the table and Ok is returned.

fn reconsider_floundered_subgoals(
    &mut self,
    ex_clause: &mut ExClause<impl Context>
)
[src]

fn get_or_create_table_for_subgoal<I: Context>(
    &mut self,
    context: &impl ContextOps<C>,
    infer: &mut dyn InferenceTable<C, I>,
    subgoal: &Literal<I>
) -> Option<(TableIndex, C::UniverseMap)>
[src]

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: &impl ContextOps<C>,
    goal: C::UCanonicalGoalInEnvironment
) -> TableIndex
[src]

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 push_initial_strands(
    &mut self,
    context: &impl ContextOps<C>,
    table: TableIndex
)
[src]

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_hh_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 push_initial_strands_instantiated<I: Context>(
    &mut self,
    table: TableIndex,
    infer: &mut dyn InferenceTable<C, I>,
    subst: I::Substitution,
    environment: I::Environment,
    goal: I::Goal
)
[src]

fn abstract_positive_literal<I: Context>(
    &mut self,
    infer: &mut dyn InferenceTable<C, I>,
    subgoal: &I::GoalInEnvironment
) -> C::CanonicalGoalInEnvironment
[src]

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 may truncate the goal to ensure termination.

This technique is described in the SA paper.

fn abstract_negative_literal<I: Context>(
    &mut self,
    infer: &mut dyn InferenceTable<C, I>,
    subgoal: &I::GoalInEnvironment
) -> Option<C::CanonicalGoalInEnvironment>
[src]

Given a selected negative subgoal, the subgoal is "inverted" (see InferenceTable<C, I>::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").

fn pursue_positive_subgoal(
    &mut self,
    context: &impl ContextOps<C>,
    depth: StackIndex,
    strand: Strand<C, impl Context>,
    selected_subgoal: &SelectedSubgoal<C>
) -> Result<(), StrandFail<C>>
[src]

Invoked when we have selected a positive literal, created its table, and selected a particular answer index N we are looking for. Searches for that answer. If we find one, we can do two things:

  • create a new strand with the same selected subgoal, but searching for the answer with index N+1
  • use the answer to resolve our selected literal and select the next subgoal in this strand to pursue

When an answer is found, that corresponds to Positive Return from the NFTD paper.

fn flounder_subgoal(
    &self,
    ex_clause: &mut ExClause<impl Context>,
    subgoal_index: usize
)
[src]

Removes the subgoal at subgoal_index from the strand's subgoal list and adds it to the strand's floundered subgoal list.

fn truncate_returned<I: Context>(
    &self,
    ex_clause: ExClause<I>,
    infer: &mut dyn InferenceTable<C, I>
) -> ExClause<I>
[src]

Used whenever we process an answer (whether new or cached) on a positive edge (the SLG POSITIVE RETURN operation). Truncates the resolvent (or factor) if it has grown too large.

fn pursue_strand_recursively(
    &mut self,
    context: &impl ContextOps<C>,
    depth: StackIndex,
    strand: Strand<C, impl Context>
) -> Result<(), StrandFail<C>>
[src]

fn push_strand_pursuing_next_answer(
    &mut self,
    depth: StackIndex,
    strand: &mut Strand<C, impl Context>,
    selected_subgoal: &SelectedSubgoal<C>
)
[src]

Invoked when we have found a successful answer to the given table. Queues up a strand to look for the next answer from that table.

fn pursue_negative_subgoal(
    &mut self,
    context: &impl ContextOps<C>,
    depth: StackIndex,
    strand: Strand<C, impl Context>,
    selected_subgoal: &SelectedSubgoal<C>
) -> Result<(), StrandFail<C>>
[src]

impl<C: Context> Forest<C>[src]

pub(super) fn simplify_hh_goal<I: Context>(
    infer: &mut dyn InferenceTable<C, I>,
    subst: I::Substitution,
    initial_environment: &I::Environment,
    initial_hh_goal: HhGoal<I>
) -> Fallible<ExClause<I>>
[src]

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

Auto Trait Implementations

impl<C> Send for Forest<C> where
    C: Send,
    <C as Context>::CanonicalConstrainedSubst: Send,
    <C as Context>::CanonicalExClause: Send,
    <C as Context>::UCanonicalGoalInEnvironment: Send,
    <C as Context>::UniverseMap: Send

impl<C> Sync for Forest<C> where
    C: Sync,
    <C as Context>::CanonicalConstrainedSubst: Sync,
    <C as Context>::CanonicalExClause: Sync,
    <C as Context>::UCanonicalGoalInEnvironment: Sync,
    <C as Context>::UniverseMap: Sync

Blanket Implementations

impl<T> From<T> for T[src]

impl<T, U> Into<U> for T where
    U: From<T>, 
[src]

impl<T, U> TryFrom<U> for T where
    U: Into<T>, 
[src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, 
[src]

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

impl<T> BorrowMut<T> for T where
    T: ?Sized
[src]

impl<T> Borrow<T> for T where
    T: ?Sized
[src]

impl<T> Any for T where
    T: 'static + ?Sized
[src]