diff options
Diffstat (limited to 'vendor/chalk-engine/src/forest.rs')
-rw-r--r-- | vendor/chalk-engine/src/forest.rs | 116 |
1 files changed, 116 insertions, 0 deletions
diff --git a/vendor/chalk-engine/src/forest.rs b/vendor/chalk-engine/src/forest.rs new file mode 100644 index 000000000..410b9cd0a --- /dev/null +++ b/vendor/chalk-engine/src/forest.rs @@ -0,0 +1,116 @@ +use crate::context::{AnswerResult, AnswerStream}; +use crate::logic::RootSearchFail; +use crate::slg::SlgContextOps; +use crate::table::AnswerIndex; +use crate::tables::Tables; +use crate::{TableIndex, TimeStamp}; + +use chalk_ir::interner::Interner; +use chalk_ir::{Goal, InEnvironment, Substitution, UCanonical}; +use tracing::debug; + +pub(crate) struct Forest<I: Interner> { + pub(crate) tables: Tables<I>, + + /// 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. + pub(crate) clock: TimeStamp, +} + +impl<I: Interner> Forest<I> { + pub fn new() -> Self { + Forest { + tables: Tables::new(), + clock: TimeStamp::default(), + } + } + + // Gets the next clock TimeStamp. This will never decrease. + pub(crate) fn increment_clock(&mut self) -> TimeStamp { + self.clock.increment(); + self.clock + } + + /// 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 iter_answers<'f>( + &'f mut self, + context: &'f SlgContextOps<'f, I>, + goal: &UCanonical<InEnvironment<Goal<I>>>, + ) -> impl AnswerStream<I> + 'f { + let table = self.get_or_create_table_for_ucanonical_goal(context, goal.clone()); + let answer = AnswerIndex::ZERO; + ForestSolver { + forest: self, + context, + table, + answer, + } + } +} + +struct ForestSolver<'me, I: Interner> { + forest: &'me mut Forest<I>, + context: &'me SlgContextOps<'me, I>, + table: TableIndex, + answer: AnswerIndex, +} + +impl<'me, I: Interner> AnswerStream<I> for ForestSolver<'me, I> { + /// # Panics + /// + /// Panics if a negative cycle was detected. + fn peek_answer(&mut self, should_continue: impl Fn() -> bool) -> AnswerResult<I> { + loop { + match self + .forest + .root_answer(self.context, self.table, self.answer) + { + Ok(answer) => { + debug!(answer = ?(&answer)); + return AnswerResult::Answer(answer); + } + + Err(RootSearchFail::InvalidAnswer) => { + self.answer.increment(); + } + Err(RootSearchFail::Floundered) => { + return AnswerResult::Floundered; + } + + Err(RootSearchFail::NoMoreSolutions) => { + return AnswerResult::NoMoreSolutions; + } + + Err(RootSearchFail::QuantumExceeded) => { + if !should_continue() { + return AnswerResult::QuantumExceeded; + } + } + + Err(RootSearchFail::NegativeCycle) => { + // Negative cycles *ought* to be avoided by construction. Hence panic + // if we find one, as that likely indicates a problem in the chalk-solve + // lowering rules. (In principle, we could propagate this error out, + // and let chalk-solve do the asserting, but that seemed like it would + // complicate the function signature more than it's worth.) + panic!("negative cycle was detected"); + } + } + } + } + + fn next_answer(&mut self, should_continue: impl Fn() -> bool) -> AnswerResult<I> { + let answer = self.peek_answer(should_continue); + self.answer.increment(); + answer + } + + fn any_future_answer(&self, test: impl Fn(&Substitution<I>) -> bool) -> bool { + self.forest.any_future_answer(self.table, self.answer, test) + } +} |