|
1 |
| -use crate::{DelayedLiteral, DelayedLiteralSet, DepthFirstNumber, ExClause, Literal, Minimums, |
| 1 | +use {DelayedLiteral, DelayedLiteralSet, DepthFirstNumber, ExClause, Literal, Minimums, |
2 | 2 | TableIndex};
|
3 |
| -use crate::fallible::NoSolution; |
4 |
| -use crate::context::{WithInstantiatedExClause, WithInstantiatedUCanonicalGoal, prelude::*}; |
5 |
| -use crate::forest::Forest; |
6 |
| -use crate::hh::HhGoal; |
7 |
| -use crate::stack::StackIndex; |
8 |
| -use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand}; |
9 |
| -use crate::table::{Answer, AnswerIndex}; |
| 3 | +use fallible::NoSolution; |
| 4 | +use context::{WithInstantiatedExClause, WithInstantiatedUCanonicalGoal, prelude::*}; |
| 5 | +use forest::Forest; |
| 6 | +use hh::HhGoal; |
| 7 | +use stack::StackIndex; |
| 8 | +use strand::{CanonicalStrand, SelectedSubgoal, Strand}; |
| 9 | +use table::{Answer, AnswerIndex}; |
10 | 10 | use rustc_hash::FxHashSet;
|
11 | 11 | use std::marker::PhantomData;
|
12 | 12 | use std::mem;
|
@@ -56,7 +56,8 @@ enum RecursiveSearchFail {
|
56 | 56 | QuantumExceeded,
|
57 | 57 | }
|
58 | 58 |
|
59 |
| -type StrandResult<C, T> = Result<T, StrandFail<C>>; |
| 59 | +#[allow(type_alias_bounds)] |
| 60 | +type StrandResult<C: Context, T> = Result<T, StrandFail<C>>; |
60 | 61 |
|
61 | 62 | /// Possible failures from pursuing a particular strand.
|
62 | 63 | #[derive(Debug)]
|
@@ -183,7 +184,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
|
183 | 184 | result.map(|()| EnsureSuccess::AnswerAvailable)
|
184 | 185 | }
|
185 | 186 |
|
186 |
| - crate fn answer(&self, table: TableIndex, answer: AnswerIndex) -> &Answer<C> { |
| 187 | + pub(crate) fn answer(&self, table: TableIndex, answer: AnswerIndex) -> &Answer<C> { |
187 | 188 | self.tables[table].answer(answer).unwrap()
|
188 | 189 | }
|
189 | 190 |
|
@@ -691,7 +692,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
|
691 | 692 | /// In terms of the NFTD paper, creating a new table corresponds
|
692 | 693 | /// to the *New Subgoal* step as well as the *Program Clause
|
693 | 694 | /// Resolution* steps.
|
694 |
| - crate fn get_or_create_table_for_ucanonical_goal( |
| 695 | + pub(crate) fn get_or_create_table_for_ucanonical_goal( |
695 | 696 | &mut self,
|
696 | 697 | goal: C::UCanonicalGoalInEnvironment,
|
697 | 698 | ) -> TableIndex {
|
@@ -1166,7 +1167,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
|
1166 | 1167 | depth: StackIndex,
|
1167 | 1168 | strand: Strand<'_, C, impl Context>,
|
1168 | 1169 | ) -> StrandResult<C, ()> {
|
1169 |
| - crate::maybe_grow_stack(|| self.pursue_strand(depth, strand)) |
| 1170 | + ::maybe_grow_stack(|| self.pursue_strand(depth, strand)) |
1170 | 1171 | }
|
1171 | 1172 |
|
1172 | 1173 | /// Invoked when we have found a successful answer to the given
|
|
0 commit comments