Merge pull request #193 from KiChjang/smarter-goal-selection

Implement goal prioritization in logic

Author: nikomatsakis

chalk-engine/src/context.rs

@@ -262,6 +262,10 @@ pub trait InferenceTable<C: Context, I: Context>:
 
     /// Create a "cannot prove" goal (see `HhGoal::CannotProve`).
     fn cannot_prove(&self) -> I::Goal;
+
+    /// Selects the next appropriate subgoal index for evaluation.
+    /// Used by: logic
+    fn next_subgoal_index(&mut self, ex_clause: &ExClause<I>) -> usize;
 }
 
 /// Methods for unifying and manipulating terms and binders.

chalk-engine/src/logic.rs

@@ -497,14 +497,7 @@ impl<C: Context> Forest<C> {
                 return self.pursue_answer(depth, strand);
             }
 
-            // For now, we always pick the last subgoal in the
-            // list.
-            //
-            // FIXME(rust-lang/chalk#80) -- we should be more
-            // selective. For example, we don't want to pick a
-            // negative literal that will flounder, and we don't want
-            // to pick things like `?T: Sized` if we can help it.
-            let subgoal_index = strand.ex_clause.subgoals.len() - 1;
+            let subgoal_index = strand.infer.next_subgoal_index(&strand.ex_clause);
 
             // Get or create table for this subgoal.
             match self.get_or_create_table_for_subgoal(

chalk-solve/src/solve/slg.rs

@@ -210,6 +210,18 @@ impl<'me> context::InferenceTable<SlgContext, SlgContext> for TruncatingInferenc
     fn cannot_prove(&self) -> Goal {
         Goal::CannotProve(())
     }
+
+    // Used by: logic
+    fn next_subgoal_index(&mut self, ex_clause: &ExClause<SlgContext>) -> usize {
+        // For now, we always pick the last subgoal in the
+        // list.
+        //
+        // FIXME(rust-lang-nursery/chalk#80) -- we should be more
+        // selective. For example, we don't want to pick a
+        // negative literal that will flounder, and we don't want
+        // to pick things like `?T: Sized` if we can help it.
+        ex_clause.subgoals.len() - 1
+    }
 }
 
 impl<'me> context::UnificationOps<SlgContext, SlgContext> for TruncatingInferenceTable<'me> {