Merge pull request #317 from jackh726/tests_refactor

Refactor tests in `slg` into the general test infra

Author: nikomatsakis

Cargo.lock

@@ -13,7 +13,6 @@ edition = "2018"
 bench = []
 
 [dependencies]
-diff = "0.1.11"
 docopt = "1.0.0"
 itertools = "0.8.0"
 lalrpop-intern = "0.15.1"

Cargo.toml

@@ -174,18 +174,17 @@ pub trait Context: Clone + Debug {
     ) -> Self::CanonicalAnswerSubst;
 
     fn goal_from_goal_in_environment(goal: &Self::GoalInEnvironment) -> &Self::Goal;
+
+    /// Returns a identity substitution.
+    fn identity_constrained_subst(
+        goal: &Self::UCanonicalGoalInEnvironment,
+    ) -> Self::CanonicalConstrainedSubst;
 }
 
 pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
     /// True if this is a coinductive goal -- e.g., proving an auto trait.
     fn is_coinductive(&self, goal: &C::UCanonicalGoalInEnvironment) -> bool;
 
-    /// Returns a identity substitution.
-    fn identity_constrained_subst(
-        &self,
-        goal: &C::UCanonicalGoalInEnvironment,
-    ) -> C::CanonicalConstrainedSubst;
-
     /// Returns the set of program clauses that might apply to
     /// `goal`. (This set can be over-approximated, naturally.)
     ///
@@ -246,7 +245,7 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
 pub trait AggregateOps<C: Context> {
     fn make_solution(
         &self,
-        root_goal: &C::CanonicalGoalInEnvironment,
+        root_goal: &C::UCanonicalGoalInEnvironment,
         answers: impl AnswerStream<C>,
     ) -> Option<C::Solution>;
 }
@@ -380,9 +379,58 @@ pub trait ResolventOps<C: Context> {
     ) -> Fallible<()>;
 }
 
+pub enum AnswerResult<C: Context> {
+    /// The next available answer.
+    Answer(CompleteAnswer<C>),
+
+    /// No answer could be returned because there are no more solutions.
+    NoMoreSolutions,
+
+    /// No answer could be returned because the goal has floundered.
+    Floundered,
+}
+
+impl<C: Context> AnswerResult<C> {
+    pub fn is_answer(&self) -> bool {
+        match self {
+            Self::Answer(_) => true,
+            _ => false,
+        }
+    }
+
+    pub fn answer(self) -> CompleteAnswer<C> {
+        match self {
+            Self::Answer(answer) => answer,
+            _ => panic!("Not an answer."),
+        }
+    }
+
+    pub fn is_no_more_solutions(&self) -> bool {
+        match self {
+            Self::NoMoreSolutions => true,
+            _ => false,
+        }
+    }
+}
+
+impl<C: Context> Debug for AnswerResult<C> {
+    fn fmt(&self, fmt: &mut std::fmt::Formatter) -> std::fmt::Result {
+        match self {
+            AnswerResult::Answer(answer) => write!(fmt, "{:?}", answer),
+            AnswerResult::Floundered => write!(fmt, "Floundered"),
+            AnswerResult::NoMoreSolutions => write!(fmt, "None"),
+        }
+    }
+}
+
 pub trait AnswerStream<C: Context> {
-    fn peek_answer(&mut self) -> Option<CompleteAnswer<C>>;
-    fn next_answer(&mut self) -> Option<CompleteAnswer<C>>;
+    /// Gets the next answer for a given goal, but doesn't increment the answer index.
+    /// Calling this or `next_answer` again will give the same answer.
+    fn peek_answer(&mut self) -> AnswerResult<C>;
+
+    /// Gets the next answer for a given goal, incrementing the answer index.
+    /// Calling this or `peek_answer` again will give the next answer.
+    fn next_answer(&mut self) -> AnswerResult<C>;
 
     /// Invokes `test` with each possible future answer, returning true immediately
     /// if we find any answer for which `test` returns true.

chalk-engine/src/context.rs

@@ -1,10 +1,12 @@
 use crate::context::prelude::*;
+use crate::context::AnswerResult;
 use crate::context::AnswerStream;
 use crate::logic::RootSearchFail;
 use crate::stack::{Stack, StackIndex};
 use crate::table::AnswerIndex;
 use crate::tables::Tables;
-use crate::{CompleteAnswer, TableIndex};
+use crate::TableIndex;
+use std::fmt::Display;
 
 pub struct Forest<C: Context> {
     context: C,
@@ -31,53 +33,6 @@ impl<C: Context> Forest<C> {
         &self.context
     }
 
-    /// 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.
-    ///
-    /// # Panics
-    ///
-    /// Panics if a negative cycle was detected.
-    pub fn force_answers(
-        &mut self,
-        context: &impl ContextOps<C>,
-        goal: C::UCanonicalGoalInEnvironment,
-        num_answers: usize,
-    ) -> Option<Vec<CompleteAnswer<C>>> {
-        let table = self.get_or_create_table_for_ucanonical_goal(context, goal);
-        let mut answers = Vec::with_capacity(num_answers);
-        let mut count = 0;
-        for _ in 0..num_answers {
-            loop {
-                match self.root_answer(context, table, AnswerIndex::from(count)) {
-                    Ok(answer) => {
-                        answers.push(answer.clone());
-                        break;
-                    }
-                    Err(RootSearchFail::InvalidAnswer) => {
-                        count += 1;
-                    }
-                    Err(RootSearchFail::Floundered) => return None,
-                    Err(RootSearchFail::QuantumExceeded) => continue,
-                    Err(RootSearchFail::NoMoreSolutions) => return Some(answers),
-                    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");
-                    }
-                }
-            }
-            count += 1;
-        }
-
-        Some(answers)
-    }
-
     /// 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
@@ -105,7 +60,7 @@ impl<C: Context> Forest<C> {
         context: &impl ContextOps<C>,
         goal: &C::UCanonicalGoalInEnvironment,
     ) -> Option<C::Solution> {
-        context.make_solution(C::canonical(&goal), self.iter_answers(context, goal))
+        context.make_solution(&goal, self.iter_answers(context, goal))
     }
 
     /// Solves a given goal, producing the solution. This will do only
@@ -116,18 +71,28 @@ impl<C: Context> Forest<C> {
         &mut self,
         context: &impl ContextOps<C>,
         goal: &C::UCanonicalGoalInEnvironment,
-        mut f: impl FnMut(C::CanonicalConstrainedSubst, bool) -> bool,
+        mut f: impl FnMut(SubstitutionResult<C::CanonicalConstrainedSubst>, bool) -> bool,
     ) -> bool {
         let mut answers = self.iter_answers(context, goal);
-        while let Some(answer) = answers.next_answer() {
-            if !f(
-                context.constrained_subst_from_answer(answer),
-                answers.peek_answer().is_some(),
-            ) {
+        loop {
+            let subst = match answers.next_answer() {
+                AnswerResult::Answer(answer) => {
+                    if !answer.ambiguous {
+                        SubstitutionResult::Definite(context.constrained_subst_from_answer(answer))
+                    } else {
+                        SubstitutionResult::Ambiguous(context.constrained_subst_from_answer(answer))
+                    }
+                }
+                AnswerResult::Floundered => SubstitutionResult::Floundered,
+                AnswerResult::NoMoreSolutions => {
+                    return true;
+                }
+            };
+
+            if !f(subst, !answers.peek_answer().is_no_more_solutions()) {
                 return false;
             }
         }
-        return true;
     }
 
     /// True if all the tables on the stack starting from `depth` and
@@ -162,15 +127,22 @@ impl<C: Context> Forest<C> {
             self.tables[table].coinductive_goal
         })
     }
+}
 
-    /// Useful for testing.
-    pub fn num_cached_answers_for_goal(
-        &mut self,
-        context: &impl ContextOps<C>,
-        goal: &C::UCanonicalGoalInEnvironment,
-    ) -> usize {
-        let table = self.get_or_create_table_for_ucanonical_goal(context, goal.clone());
-        self.tables[table].num_cached_answers()
+#[derive(Debug)]
+pub enum SubstitutionResult<S> {
+    Definite(S),
+    Ambiguous(S),
+    Floundered,
+}
+
+impl<S: Display> Display for SubstitutionResult<S> {
+    fn fmt(&self, fmt: &mut std::fmt::Formatter) -> std::fmt::Result {
+        match self {
+            SubstitutionResult::Definite(subst) => write!(fmt, "{}", subst),
+            SubstitutionResult::Ambiguous(subst) => write!(fmt, "Ambiguous({})", subst),
+            SubstitutionResult::Floundered => write!(fmt, "Floundered"),
+        }
     }
 }
 
@@ -185,29 +157,25 @@ impl<'me, C: Context, CO: ContextOps<C>> AnswerStream<C> for ForestSolver<'me, C
     /// # Panics
     ///
     /// Panics if a negative cycle was detected.
-    fn peek_answer(&mut self) -> Option<CompleteAnswer<C>> {
+    fn peek_answer(&mut self) -> AnswerResult<C> {
         loop {
             match self
                 .forest
                 .root_answer(self.context, self.table, self.answer)
             {
                 Ok(answer) => {
-                    return Some(answer.clone());
+                    return AnswerResult::Answer(answer.clone());
                 }
 
                 Err(RootSearchFail::InvalidAnswer) => {
                     self.answer.increment();
                 }
                 Err(RootSearchFail::Floundered) => {
-                    let table_goal = &self.forest.tables[self.table].table_goal;
-                    return Some(CompleteAnswer {
-                        subst: self.context.identity_constrained_subst(table_goal),
-                        ambiguous: true,
-                    });
+                    return AnswerResult::Floundered;
                 }
 
                 Err(RootSearchFail::NoMoreSolutions) => {
-                    return None;
+                    return AnswerResult::NoMoreSolutions;
                 }
 
                 Err(RootSearchFail::QuantumExceeded) => {}
@@ -224,11 +192,10 @@ impl<'me, C: Context, CO: ContextOps<C>> AnswerStream<C> for ForestSolver<'me, C
         }
     }
 
-    fn next_answer(&mut self) -> Option<CompleteAnswer<C>> {
-        self.peek_answer().map(|answer| {
-            self.answer.increment();
-            answer
-        })
+    fn next_answer(&mut self) -> AnswerResult<C> {
+        let answer = self.peek_answer();
+        self.answer.increment();
+        answer
     }
 
     fn any_future_answer(

chalk-engine/src/forest.rs

@@ -154,11 +154,6 @@ impl<C: Context> Table<C> {
         self.answers.get(index.value)
     }
 
-    /// Useful for testing.
-    pub fn num_cached_answers(&self) -> usize {
-        self.answers.len()
-    }
-
     pub(super) fn next_answer_index(&self) -> AnswerIndex {
         AnswerIndex::from(self.answers.len())
     }

chalk-engine/src/table.rs

@@ -12,6 +12,10 @@ edition = "2018"
 lalrpop-intern = "0.15.1"
 salsa = "0.10.0"
 
+[dependencies.chalk-engine]
+version = "0.9.0"
+path = "../chalk-engine"
+
 [dependencies.chalk-solve]
 version = "0.1.0"
 path = "../chalk-solve"

chalk-integration/Cargo.toml

@@ -2,6 +2,7 @@ use crate::error::ChalkError;
 use crate::lowering::LowerGoal;
 use crate::program::Program;
 use crate::query::{Lowering, LoweringDatabase};
+use chalk_engine::forest::SubstitutionResult;
 use chalk_ir::family::ChalkIr;
 use chalk_ir::tls;
 use chalk_ir::AssocTypeId;
@@ -70,7 +71,7 @@ impl ChalkDatabase {
     pub fn solve_multiple(
         &self,
         goal: &UCanonical<InEnvironment<Goal<ChalkIr>>>,
-        f: impl FnMut(Canonical<ConstrainedSubst<ChalkIr>>, bool) -> bool,
+        f: impl FnMut(SubstitutionResult<Canonical<ConstrainedSubst<ChalkIr>>>, bool) -> bool,
     ) -> bool {
         let solver = self.solver();
         let solution = solver.lock().unwrap().solve_multiple(self, goal, f);

chalk-integration/src/db.rs

@@ -76,7 +76,7 @@ fn coherence(
 ) -> Result<BTreeMap<TraitId<ChalkIr>, Arc<SpecializationPriorities<ChalkIr>>>, ChalkError> {
     let program = db.program_ir()?;
 
-    tls::set_current_program(&program, || -> Result<_, ChalkError> {
+    let priorities_map = tls::set_current_program(&program, || -> Result<_, ChalkError> {
         let priorities_map: Result<BTreeMap<_, _>, ChalkError> = program
             .trait_data
             .keys()
@@ -87,11 +87,10 @@ fn coherence(
             })
             .collect();
         let priorities_map = priorities_map?;
-
-        let () = db.orphan_check()?;
-
         Ok(priorities_map)
-    })
+    });
+    let () = db.orphan_check()?;
+    priorities_map
 }
 
 fn checked_program(db: &impl LoweringDatabase) -> Result<Arc<Program>, ChalkError> {

chalk-integration/src/query.rs

@@ -75,4 +75,3 @@ pub use solve::Guidance;
 pub use solve::Solution;
 pub use solve::Solver;
 pub use solve::SolverChoice;
-pub use solve::TestSolver;