Run tests with both solvers by default

Author: flodiebold

chalk-solve/src/solve.rs

@@ -196,14 +196,19 @@ pub enum SolverChoice {
 }
 
 impl SolverChoice {
-    /// Returns the default SLG parameters.
+    /// Returns specific SLG parameters.
     pub fn slg(max_size: usize, expected_answers: Option<usize>) -> Self {
         SolverChoice::SLG {
             max_size,
             expected_answers,
         }
     }
 
+    /// Returns the default SLG parameters.
+    pub fn slg_default() -> Self {
+        SolverChoice::slg(10, None)
+    }
+
     /// Returns the default recursive solver setup.
     pub fn recursive() -> Self {
         SolverChoice::Recursive {
@@ -234,8 +239,8 @@ impl SolverChoice {
 
 impl Default for SolverChoice {
     fn default() -> Self {
-        SolverChoice::recursive()
-        // SolverChoice::slg(10, None)
+        // SolverChoice::recursive()
+        SolverChoice::slg(10, None)
     }
 }
 

tests/test/cycle.rs

@@ -163,9 +163,15 @@ fn overflow() {
         // Will try to prove S<G<Z>>: Q then S<G<G<Z>>>: Q etc ad infinitum
         goal {
             S<Z>: Q
-        } yields {
+        } yields[SolverChoice::slg(10, None)] {
             "Ambiguous; no inference guidance"
         }
+
+        goal {
+            S<Z>: Q
+        } yields[SolverChoice::recursive()] {
+            "No possible solution"
+        }
     }
 }
 

tests/test/mod.rs

@@ -71,26 +71,29 @@ macro_rules! test {
         test!(@program[$program]
               @parsed_goals[
                   $($parsed_goals)*
-                      (stringify!($goal), SolverChoice::default(), TestGoal::Aggregated($expected))
+                      (stringify!($goal), SolverChoice::slg_default(), TestGoal::Aggregated($expected))
+                      (stringify!($goal), SolverChoice::recursive(), TestGoal::Aggregated($expected))
               ]
               @unparsed_goals[$($unparsed_goals)*])
     };
 
-    // goal { G } yields_all { "Y1", "Y2", ... , "YN" } -- test both solvers gets exactly N same answers in
-    // the same order
+    // goal { G } yields_all { "Y1", "Y2", ... , "YN" } -- test that the SLG
+    // solver gets exactly N answers in this order (the recursive solver can't
+    // return multiple answers)
     (@program[$program:tt] @parsed_goals[$($parsed_goals:tt)*] @unparsed_goals[
         goal $goal:tt yields_all { $($expected:expr),* }
         $($unparsed_goals:tt)*
     ]) => {
         test!(@program[$program]
               @parsed_goals[
                   $($parsed_goals)*
-                      (stringify!($goal), SolverChoice::default(), TestGoal::All(vec![$($expected),*]))
+                      (stringify!($goal), SolverChoice::slg_default(), TestGoal::All(vec![$($expected),*]))
               ]
               @unparsed_goals[$($unparsed_goals)*])
     };
 
-    // goal { G } yields_first { "Y1", "Y2", ... , "YN" } -- test both solvers gets at least N same first answers
+    // goal { G } yields_first { "Y1", "Y2", ... , "YN" } -- test that the SLG
+    // solver gets at least N same first answers
     (@program[$program:tt] @parsed_goals[$($parsed_goals:tt)*] @unparsed_goals[
         goal $goal:tt yields_first { $($expected:expr),* }
         $($unparsed_goals:tt)*
@@ -122,6 +125,20 @@ macro_rules! test {
               @unparsed_goals[goal $($unparsed_goals)*])
     };
 
+    // same as above, but there are multiple yields clauses => duplicate the goal
+    (@program[$program:tt] @parsed_goals[$($parsed_goals:tt)*] @unparsed_goals[
+        goal $goal:tt
+            yields[$C:expr] { $expected:expr }
+        yields $($unparsed_tail:tt)*
+    ]) => {
+        test!(@program[$program]
+              @parsed_goals[
+                  $($parsed_goals)*
+                      (stringify!($goal), $C, TestGoal::Aggregated($expected))
+              ]
+              @unparsed_goals[goal $goal yields $($unparsed_tail)*])
+    };
+
     // same as above, but for the final goal in the list.
     (@program[$program:tt] @parsed_goals[$($parsed_goals:tt)*] @unparsed_goals[
         goal $goal:tt yields[$C:expr] { $expected:expr }

tests/test/projection.rs

@@ -142,7 +142,7 @@ fn projection_equality() {
             exists<U> {
                 S: Trait2<U>
             }
-        } yields {
+        } yields[SolverChoice::recursive()] {
             "Unique; substitution [?0 := u32]"
         }
     }

tests/test/unify.rs

@@ -108,11 +108,17 @@ fn unify_quantified_lifetimes() {
                     }
                 }
             }
-        } yields {
+        } yields[SolverChoice::slg(10, None)] {
             "Unique; for<?U0> { \
              substitution [?0 := '^0.0, ?1 := '!1_0], \
              lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \
              }"
+        } yields[SolverChoice::recursive()] {
+            // only difference is in the value of ?1, which is equivalent
+            "Unique; for<?U0> { \
+             substitution [?0 := '^0.0, ?1 := '^0.0], \
+             lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \
+             }"
         }
     }
 }