Move inference table creation to Solver and store free vars as GenericArgs

Author: jackh726

chalk-solve/src/recursive.rs

@@ -6,7 +6,7 @@ use self::fulfill::{Fulfill, RecursiveInferenceTable};
 use self::search_graph::{DepthFirstNumber, SearchGraph};
 use self::stack::{Stack, StackDepth};
 use crate::clauses::program_clauses_for_goal;
-use crate::infer::{InferenceTable, ParameterEnaVariable};
+use crate::infer::{InferenceTable, ParameterEnaVariableExt};
 use crate::solve::truncate;
 use crate::{Guidance, RustIrDatabase, Solution};
 use chalk_ir::fold::Fold;
@@ -17,7 +17,8 @@ use chalk_ir::{debug, debug_heading, info, info_heading};
 use chalk_ir::{
     Binders, Canonical, ClausePriority, ConstrainedSubst, Constraint, DomainGoal, Environment,
     Fallible, Floundered, GenericArg, Goal, GoalData, InEnvironment, NoSolution, ProgramClause,
-    ProgramClauseData, ProgramClauseImplication, UCanonical, UniverseMap, VariableKinds,
+    ProgramClauseData, ProgramClauseImplication, Substitution, UCanonical, UniverseMap,
+    VariableKinds,
 };
 use rustc_hash::FxHashMap;
 use std::fmt::Debug;
@@ -63,13 +64,18 @@ impl<I: Interner> RecursiveInferenceTable<I> for RecursiveInferenceTableImpl<I>
         &mut self,
         interner: &I,
         value: &T,
-    ) -> (Canonical<T::Result>, Vec<ParameterEnaVariable<I>>)
+    ) -> (Canonical<T::Result>, Vec<GenericArg<I>>)
     where
         T: Fold<I>,
         T::Result: HasInterner<Interner = I>,
     {
         let res = self.infer.canonicalize(interner, value);
-        (res.quantified, res.free_vars)
+        let free_vars = res
+            .free_vars
+            .into_iter()
+            .map(|free_var| free_var.to_generic_arg(interner))
+            .collect();
+        (res.quantified, free_vars)
     }
 
     fn u_canonicalize<T>(
@@ -184,6 +190,25 @@ impl<I: Interner> RecursiveContext<I> {
 }
 
 impl<'me, I: Interner> Solver<'me, I> {
+    pub(crate) fn new_inference_table<
+        T: Fold<I, I, Result = T> + HasInterner<Interner = I> + Clone,
+    >(
+        &self,
+        ucanonical_goal: &UCanonical<InEnvironment<T>>,
+    ) -> (
+        RecursiveInferenceTableImpl<I>,
+        Substitution<I>,
+        InEnvironment<T::Result>,
+    ) {
+        let (infer, subst, canonical_goal) = InferenceTable::from_canonical(
+            self.program.interner(),
+            ucanonical_goal.universes,
+            &ucanonical_goal.canonical,
+        );
+        let infer = crate::recursive::RecursiveInferenceTableImpl { infer };
+        (infer, subst, canonical_goal)
+    }
+
     /// Solves a canonical goal. The substitution returned in the
     /// solution will be for the fully decomposed goal. For example, given the
     /// program
@@ -440,7 +465,8 @@ impl<'me, I: Interner> Solver<'me, I> {
         minimums: &mut Minimums,
     ) -> (Fallible<Solution<I>>, ClausePriority) {
         debug_heading!("solve_via_simplification({:?})", canonical_goal);
-        match Fulfill::new_with_simplification(self, canonical_goal) {
+        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),
         }
@@ -515,7 +541,8 @@ impl<'me, I: Interner> Solver<'me, I> {
             clause
         );
 
-        match Fulfill::new_with_clause(self, canonical_goal, clause) {
+        let (infer, subst, goal) = self.new_inference_table(canonical_goal);
+        match Fulfill::new_with_clause(self, infer, subst, goal, clause) {
             Ok(fulfill) => (fulfill.solve(minimums), clause.skip_binders().priority),
             Err(e) => (Err(e), ClausePriority::High),
         }

chalk-solve/src/recursive/fulfill.rs

@@ -1,5 +1,4 @@
-use crate::infer::{InferenceTable, ParameterEnaVariable, ParameterEnaVariableExt};
-use crate::recursive::{Minimums, RecursiveInferenceTableImpl, Solver};
+use crate::recursive::{Minimums, Solver};
 use crate::solve::{Guidance, Solution};
 use chalk_ir::cast::Cast;
 use chalk_ir::fold::Fold;
@@ -9,8 +8,8 @@ use chalk_ir::zip::Zip;
 use chalk_ir::{debug, debug_heading};
 use chalk_ir::{
     Binders, Canonical, ConstrainedSubst, Constraint, DomainGoal, Environment, EqGoal, Fallible,
-    Goal, GoalData, InEnvironment, LifetimeOutlives, NoSolution, ProgramClauseImplication,
-    QuantifierKind, Substitution, UCanonical, UniverseMap, WhereClause,
+    GenericArg, Goal, GoalData, InEnvironment, LifetimeOutlives, NoSolution,
+    ProgramClauseImplication, QuantifierKind, Substitution, UCanonical, UniverseMap, WhereClause,
 };
 use rustc_hash::FxHashSet;
 use std::fmt::Debug;
@@ -46,7 +45,7 @@ enum Obligation<I: Interner> {
 /// so that we can update inference state accordingly.
 #[derive(Clone, Debug)]
 struct PositiveSolution<I: Interner> {
-    free_vars: Vec<ParameterEnaVariable<I>>,
+    free_vars: Vec<GenericArg<I>>,
     universes: UniverseMap,
     solution: Solution<I>,
 }
@@ -79,7 +78,7 @@ pub(crate) trait RecursiveInferenceTable<I: Interner> {
         &mut self,
         interner: &I,
         value: &T,
-    ) -> (Canonical<T::Result>, Vec<ParameterEnaVariable<I>>)
+    ) -> (Canonical<T::Result>, Vec<GenericArg<I>>)
     where
         T: Fold<I>,
         T::Result: HasInterner<Interner = I>;
@@ -149,18 +148,15 @@ pub(crate) struct Fulfill<'s, 'db, I: Interner, Infer: RecursiveInferenceTable<I
     cannot_prove: bool,
 }
 
-impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I, RecursiveInferenceTableImpl<I>> {
-    fn new<T: Fold<I, I, Result = T> + HasInterner<Interner = I> + Clone>(
+impl<'s, 'db, I: Interner, Infer: RecursiveInferenceTable<I>> Fulfill<'s, 'db, I, Infer> {
+    pub(crate) fn new_with_clause(
         solver: &'s mut Solver<'db, I>,
-        ucanonical_goal: &UCanonical<InEnvironment<T>>,
-    ) -> (Self, InEnvironment<T::Result>) {
-        let (infer, subst, canonical_goal) = InferenceTable::from_canonical(
-            solver.program.interner(),
-            ucanonical_goal.universes,
-            &ucanonical_goal.canonical,
-        );
-        let infer = crate::recursive::RecursiveInferenceTableImpl { infer };
-        let fulfill = Fulfill {
+        infer: Infer,
+        subst: Substitution<I>,
+        canonical_goal: InEnvironment<DomainGoal<I>>,
+        clause: &Binders<ProgramClauseImplication<I>>,
+    ) -> Fallible<Self> {
+        let mut fulfill = Fulfill {
             solver,
             infer,
             subst,
@@ -169,16 +165,6 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I, RecursiveInferenceTableImpl<I>> {
             cannot_prove: false,
         };
 
-        (fulfill, canonical_goal)
-    }
-
-    pub(crate) fn new_with_clause(
-        solver: &'s mut Solver<'db, I>,
-        ucanonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
-        clause: &Binders<ProgramClauseImplication<I>>,
-    ) -> Fallible<Self> {
-        let (mut fulfill, canonical_goal) = Fulfill::new(solver, ucanonical_goal);
-
         let ProgramClauseImplication {
             consequence,
             conditions,
@@ -209,9 +195,18 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I, RecursiveInferenceTableImpl<I>> {
 
     pub(crate) fn new_with_simplification(
         solver: &'s mut Solver<'db, I>,
-        ucanonical_goal: &UCanonical<InEnvironment<Goal<I>>>,
+        infer: Infer,
+        subst: Substitution<I>,
+        canonical_goal: InEnvironment<Goal<I>>,
     ) -> Fallible<Self> {
-        let (mut fulfill, canonical_goal) = Fulfill::new(solver, ucanonical_goal);
+        let mut fulfill = Fulfill {
+            solver,
+            infer,
+            subst,
+            obligations: vec![],
+            constraints: FxHashSet::default(),
+            cannot_prove: false,
+        };
 
         if let Err(e) = fulfill.push_goal(&canonical_goal.environment, canonical_goal.goal.clone())
         {
@@ -383,7 +378,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I, RecursiveInferenceTableImpl<I>> {
     /// be mapped into our variables with `free_vars`.
     fn apply_solution(
         &mut self,
-        free_vars: Vec<ParameterEnaVariable<I>>,
+        free_vars: Vec<GenericArg<I>>,
         universes: UniverseMap,
         subst: Canonical<ConstrainedSubst<I>>,
     ) {
@@ -406,8 +401,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I, RecursiveInferenceTableImpl<I>> {
 
         for (i, free_var) in free_vars.into_iter().enumerate() {
             let subst_value = subst.at(self.interner(), i);
-            let free_value = free_var.to_generic_arg(self.interner());
-            self.unify(empty_env, &free_value, subst_value)
+            self.unify(empty_env, &free_var, subst_value)
                 .unwrap_or_else(|err| {
                     panic!(
                         "apply_solution failed with free_var={:?}, subst_value={:?}: {:?}",