chalk_engine/
forest.rs

1use crate::context::{AnswerResult, AnswerStream};
2use crate::logic::RootSearchFail;
3use crate::slg::SlgContextOps;
4use crate::table::AnswerIndex;
5use crate::tables::Tables;
6use crate::{TableIndex, TimeStamp};
7
8use chalk_ir::interner::Interner;
9use chalk_ir::{Goal, InEnvironment, Substitution, UCanonical};
10use tracing::debug;
11
12pub(crate) struct Forest<I: Interner> {
13    pub(crate) tables: Tables<I>,
14
15    /// This is a clock which always increases. It is
16    /// incremented every time a new subgoal is followed.
17    /// This effectively gives us way to track what depth
18    /// and loop a table or strand was last followed.
19    pub(crate) clock: TimeStamp,
20}
21
22impl<I: Interner> Forest<I> {
23    pub fn new() -> Self {
24        Forest {
25            tables: Tables::new(),
26            clock: TimeStamp::default(),
27        }
28    }
29
30    // Gets the next clock TimeStamp. This will never decrease.
31    pub(crate) fn increment_clock(&mut self) -> TimeStamp {
32        self.clock.increment();
33        self.clock
34    }
35
36    /// Returns a "solver" for a given goal in the form of an
37    /// iterator. Each time you invoke `next`, it will do the work to
38    /// extract one more answer. These answers are cached in between
39    /// invocations. Invoking `next` fewer times is preferable =)
40    pub fn iter_answers<'f>(
41        &'f mut self,
42        context: &'f SlgContextOps<'f, I>,
43        goal: &UCanonical<InEnvironment<Goal<I>>>,
44    ) -> impl AnswerStream<I> + 'f {
45        let table = self.get_or_create_table_for_ucanonical_goal(context, goal.clone());
46        let answer = AnswerIndex::ZERO;
47        ForestSolver {
48            forest: self,
49            context,
50            table,
51            answer,
52        }
53    }
54}
55
56struct ForestSolver<'me, I: Interner> {
57    forest: &'me mut Forest<I>,
58    context: &'me SlgContextOps<'me, I>,
59    table: TableIndex,
60    answer: AnswerIndex,
61}
62
63impl<'me, I: Interner> AnswerStream<I> for ForestSolver<'me, I> {
64    /// # Panics
65    ///
66    /// Panics if a negative cycle was detected.
67    fn peek_answer(&mut self, should_continue: impl Fn() -> bool) -> AnswerResult<I> {
68        loop {
69            match self
70                .forest
71                .root_answer(self.context, self.table, self.answer)
72            {
73                Ok(answer) => {
74                    debug!(answer = ?(&answer));
75                    return AnswerResult::Answer(answer);
76                }
77
78                Err(RootSearchFail::InvalidAnswer) => {
79                    self.answer.increment();
80                }
81                Err(RootSearchFail::Floundered) => {
82                    return AnswerResult::Floundered;
83                }
84
85                Err(RootSearchFail::NoMoreSolutions) => {
86                    return AnswerResult::NoMoreSolutions;
87                }
88
89                Err(RootSearchFail::QuantumExceeded) => {
90                    if !should_continue() {
91                        return AnswerResult::QuantumExceeded;
92                    }
93                }
94
95                Err(RootSearchFail::NegativeCycle) => {
96                    // Negative cycles *ought* to be avoided by construction. Hence panic
97                    // if we find one, as that likely indicates a problem in the chalk-solve
98                    // lowering rules. (In principle, we could propagate this error out,
99                    // and let chalk-solve do the asserting, but that seemed like it would
100                    // complicate the function signature more than it's worth.)
101                    panic!("negative cycle was detected");
102                }
103            }
104        }
105    }
106
107    fn next_answer(&mut self, should_continue: impl Fn() -> bool) -> AnswerResult<I> {
108        let answer = self.peek_answer(should_continue);
109        self.answer.increment();
110        answer
111    }
112
113    fn any_future_answer(&self, test: impl Fn(&Substitution<I>) -> bool) -> bool {
114        self.forest.any_future_answer(self.table, self.answer, test)
115    }
116}
chalk_engine/forest.rs

chalk_engine/
forest.rs
