move Priority out from search graph and into the "value"

nikomatsakis · nikomatsakis · commit d05412f56b2d · 2021-05-18T05:27:38.000-04:00
diff --git a/chalk-recursive/src/lib.rs b/chalk-recursive/src/lib.rs
@@ -1,5 +1,7 @@
 use crate::search_graph::DepthFirstNumber;
-use chalk_ir::{Goal, InEnvironment, UCanonical};
+use chalk_ir::{
+    interner::Interner, ClausePriority, Fallible, Goal, InEnvironment, NoSolution, UCanonical,
+};
 
 pub type UCanonicalGoal<I> = UCanonical<InEnvironment<Goal<I>>>;
 
@@ -12,8 +14,35 @@ pub mod solve;
 mod stack;
 
 pub use cache::Cache;
+use chalk_solve::{Guidance, Solution};
 pub use recursive::RecursiveSolver;
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub struct PrioritizedSolution<I: Interner> {
+    priority: ClausePriority,
+    solution: Fallible<Solution<I>>,
+}
+
+impl<I: Interner> PrioritizedSolution<I> {
+    /// Create a new prioritized solution.
+    pub(crate) fn new(solution: Fallible<Solution<I>>, priority: ClausePriority) -> Self {
+        Self { priority, solution }
+    }
+
+    /// Create a high priority solution.
+    pub(crate) fn high(solution: Fallible<Solution<I>>) -> Self {
+        Self::new(solution, ClausePriority::High)
+    }
 
+    /// Returns a high-priority solution that represents an error (no solution)
+    pub(crate) fn error() -> Self {
+        Self::high(Err(NoSolution))
+    }
+
+    /// Returns a high-priority solution that represents ambiguity with no guidance.
+    pub(crate) fn ambiguity() -> Self {
+        Self::high(Ok(Solution::Ambig(Guidance::Unknown)))
+    }
+}
 /// The `minimums` struct is used while solving to track whether we encountered
 /// any cycles in the process.
 #[derive(Copy, Clone, Debug)]
diff --git a/chalk-recursive/src/recursive.rs b/chalk-recursive/src/recursive.rs
@@ -1,8 +1,8 @@
-use crate::cache::Cache;
 use crate::search_graph::DepthFirstNumber;
 use crate::search_graph::SearchGraph;
 use crate::solve::{SolveDatabase, SolveIteration};
 use crate::stack::{Stack, StackDepth};
+use crate::{cache::Cache, PrioritizedSolution};
 use crate::{Minimums, UCanonicalGoal};
 use chalk_ir::{interner::Interner, NoSolution};
 use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical};
@@ -17,12 +17,12 @@ struct RecursiveContext<I: Interner> {
 
     /// The "search graph" stores "in-progress results" that are still being
     /// solved.
-    search_graph: SearchGraph<UCanonicalGoal<I>, Fallible<Solution<I>>>,
+    search_graph: SearchGraph<UCanonicalGoal<I>, PrioritizedSolution<I>>,
 
     /// The "cache" stores results for goals that we have completely solved.
     /// Things are added to the cache when we have completely processed their
     /// result.
-    cache: Option<Cache<UCanonicalGoal<I>, Fallible<Solution<I>>>>,
+    cache: Option<Cache<UCanonicalGoal<I>, PrioritizedSolution<I>>>,
 
     /// The maximum size for goals.
     max_size: usize,
@@ -46,7 +46,7 @@ impl<I: Interner> RecursiveSolver<I> {
     pub fn new(
         overflow_depth: usize,
         max_size: usize,
-        cache: Option<Cache<UCanonicalGoal<I>, Fallible<Solution<I>>>>,
+        cache: Option<Cache<UCanonicalGoal<I>, PrioritizedSolution<I>>>,
     ) -> Self {
         Self {
             ctx: Box::new(RecursiveContext::new(overflow_depth, max_size, cache)),
@@ -84,7 +84,7 @@ impl<I: Interner> RecursiveContext<I> {
     pub fn new(
         overflow_depth: usize,
         max_size: usize,
-        cache: Option<Cache<UCanonicalGoal<I>, Fallible<Solution<I>>>>,
+        cache: Option<Cache<UCanonicalGoal<I>, PrioritizedSolution<I>>>,
     ) -> Self {
         RecursiveContext {
             stack: Stack::new(overflow_depth),
@@ -149,7 +149,7 @@ impl<'me, I: Interner> Solver<'me, I> {
         // so this function will eventually be constant and the loop terminates.
         loop {
             let minimums = &mut Minimums::new();
-            let (current_answer, current_prio) = self.solve_iteration(&canonical_goal, minimums);
+            let current_answer = self.solve_iteration(&canonical_goal, minimums);
 
             debug!(
                 "solve_new_subgoal: loop iteration result = {:?} with minimums {:?}",
@@ -160,24 +160,22 @@ impl<'me, I: Interner> Solver<'me, I> {
                 // None of our subgoals depended on us directly.
                 // We can return.
                 self.context.search_graph[dfn].solution = current_answer;
-                self.context.search_graph[dfn].solution_priority = current_prio;
                 return *minimums;
             }
 
             // Some of our subgoals depended on us. We need to re-run
             // with the current answer.
-            if self.context.search_graph[dfn].solution == current_answer {
+            if self.context.search_graph[dfn].solution.solution == current_answer.solution {
                 // Reached a fixed point.
                 return *minimums;
             }
 
-            let current_answer_is_ambig = match &current_answer {
+            let current_answer_is_ambig = match &current_answer.solution {
                 Ok(s) => s.is_ambig(),
                 Err(_) => false,
             };
 
             self.context.search_graph[dfn].solution = current_answer;
-            self.context.search_graph[dfn].solution_priority = current_prio;
 
             // Subtle: if our current answer is ambiguous, we can just stop, and
             // in fact we *must* -- otherwise, we sometimes fail to reach a
@@ -206,7 +204,7 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
         if let Some(cache) = &self.context.cache {
             if let Some(value) = cache.get(&goal) {
                 debug!("solve_reduced_goal: cache hit, value={:?}", value);
-                return value.clone();
+                return value.solution.clone();
             }
         }
 
@@ -231,12 +229,11 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
 
             // Return the solution from the table.
             let previous_solution = self.context.search_graph[dfn].solution.clone();
-            let previous_solution_priority = self.context.search_graph[dfn].solution_priority;
             info!(
-                "solve_goal: cycle detected, previous solution {:?} with prio {:?}",
-                previous_solution, previous_solution_priority
+                "solve_goal: cycle detected, previous solution {:?}",
+                previous_solution,
             );
-            previous_solution
+            previous_solution.solution
         } else {
             // Otherwise, push the goal onto the stack and create a table.
             // The initial result for this table depends on whether the goal is coinductive.
@@ -253,10 +250,11 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
             } else {
                 Err(NoSolution)
             };
-            let dfn = self
-                .context
-                .search_graph
-                .insert(&goal, depth, initial_solution);
+            let dfn = self.context.search_graph.insert(
+                &goal,
+                depth,
+                PrioritizedSolution::high(initial_solution),
+            );
             let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn);
             self.context.search_graph[dfn].links = subgoal_minimums;
             self.context.search_graph[dfn].stack_depth = None;
@@ -265,7 +263,6 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
 
             // Read final result from table.
             let result = self.context.search_graph[dfn].solution.clone();
-            let priority = self.context.search_graph[dfn].solution_priority;
 
             // If processing this subgoal did not involve anything
             // outside of its subtree, then we can promote it to the
@@ -283,8 +280,8 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
                 }
             }
 
-            info!("solve_goal: solution = {:?} prio {:?}", result, priority);
-            result
+            info!("solve_goal: solution = {:#?}", result);
+            result.solution
         }
     }
 
diff --git a/chalk-recursive/src/search_graph.rs b/chalk-recursive/src/search_graph.rs
@@ -1,6 +1,5 @@
 use super::stack::StackDepth;
 use crate::{Cache, Minimums};
-use chalk_ir::ClausePriority;
 use rustc_hash::FxHashMap;
 use std::fmt::Debug;
 use std::hash::Hash;
@@ -30,7 +29,6 @@ pub(super) struct Node<K, V> {
     pub(crate) goal: K,
 
     pub(crate) solution: V,
-    pub(crate) solution_priority: ClausePriority,
 
     /// This is `Some(X)` if we are actively exploring this node, or
     /// `None` otherwise.
@@ -78,7 +76,6 @@ where
         let node = Node {
             goal: goal.clone(),
             solution,
-            solution_priority: ClausePriority::High,
             stack_depth: Some(stack_depth),
             links: Minimums { positive: dfn },
         };
diff --git a/chalk-recursive/src/solve.rs b/chalk-recursive/src/solve.rs
@@ -1,6 +1,6 @@
 use super::combine;
 use super::fulfill::Fulfill;
-use crate::{Minimums, UCanonicalGoal};
+use crate::{Minimums, PrioritizedSolution, UCanonicalGoal};
 use chalk_ir::could_match::CouldMatch;
 use chalk_ir::fold::Fold;
 use chalk_ir::interner::{HasInterner, Interner};
@@ -39,7 +39,7 @@ pub(super) trait SolveIteration<I: Interner>: SolveDatabase<I> {
         &mut self,
         canonical_goal: &UCanonicalGoal<I>,
         minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
+    ) -> PrioritizedSolution<I> {
         let UCanonical {
             universes,
             canonical:
@@ -68,14 +68,14 @@ pub(super) trait SolveIteration<I: Interner>: SolveDatabase<I> {
                 // or from the lowered program, which includes fallback
                 // clauses. We try each approach in turn:
 
-                let (prog_solution, prog_prio) = {
+                let solution = {
                     debug_span!("prog_clauses");
 
                     self.solve_from_clauses(&canonical_goal, minimums)
                 };
-                debug!(?prog_solution);
+                debug!(?solution);
 
-                (prog_solution, prog_prio)
+                solution
             }
 
             _ => {
@@ -107,11 +107,11 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
         &mut self,
         canonical_goal: &UCanonicalGoal<I>,
         minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
+    ) -> PrioritizedSolution<I> {
         let (infer, subst, goal) = self.new_inference_table(canonical_goal);
         match Fulfill::new_with_simplification(self, infer, subst, goal) {
-            Ok(fulfill) => (fulfill.solve(minimums), ClausePriority::High),
-            Err(e) => (Err(e), ClausePriority::High),
+            Ok(fulfill) => PrioritizedSolution::high(fulfill.solve(minimums)),
+            Err(NoSolution) => PrioritizedSolution::error(),
         }
     }
 
@@ -122,7 +122,7 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
         &mut self,
         canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
         minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
+    ) -> PrioritizedSolution<I> {
         let mut clauses = vec![];
 
         let db = self.db();
@@ -137,7 +137,7 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
         match program_clauses_that_could_match(db, canonical_goal) {
             Ok(goal_clauses) => clauses.extend(goal_clauses.into_iter().filter(could_match)),
             Err(Floundered) => {
-                return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High);
+                return PrioritizedSolution::ambiguity();
             }
         }
 
@@ -155,7 +155,7 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
 
             // If we have a completely ambiguous answer, it's not going to get better, so stop
             if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) {
-                return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High);
+                return PrioritizedSolution::ambiguity();
             }
 
             let ProgramClauseData(implication) = program_clause.data(self.interner());
@@ -184,7 +184,12 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
                 debug!("Error");
             }
         }
-        cur_solution.map_or((Err(NoSolution), ClausePriority::High), |(s, p)| (Ok(s), p))
+
+        if let Some((s, p)) = cur_solution {
+            PrioritizedSolution::new(Ok(s), p)
+        } else {
+            PrioritizedSolution::error()
+        }
     }
 
     fn new_inference_table<T: Fold<I, Result = T> + HasInterner<Interner = I> + Clone>(
