Merge pull request #546 from zaharidichev/zd/separate-rec-solver

Separate recursive solver

Cargo.toml

@@ -25,6 +25,7 @@ chalk-derive = { version = "0.17.0-dev.0", path = "chalk-derive" }
 chalk-engine = { version = "0.17.0-dev.0", path = "chalk-engine" }
 chalk-ir = { version = "0.17.0-dev.0", path = "chalk-ir" }
 chalk-solve = { version = "0.17.0-dev.0", path = "chalk-solve" }
+chalk-recursive = { version = "0.17.0-dev.0", path = "chalk-recursive" }
 chalk-parse = { version = "0.17.0-dev.0", path = "chalk-parse" }
 chalk-integration = { version = "0.17.0-dev.0", path = "chalk-integration" }
 

chalk-engine/Cargo.toml

@@ -18,3 +18,7 @@ tracing = "0.1"
 
 chalk-derive = { version = "0.17.0-dev.0", path = "../chalk-derive" }
 chalk-ir = { version = "0.17.0-dev.0", path = "../chalk-ir" }
+chalk-solve = { version = "0.17.0-dev.0", path = "../chalk-solve" }
+
+[dev-dependencies]
+chalk-integration = { path = "../chalk-integration" }

chalk-engine/src/forest.rs

@@ -8,7 +8,7 @@ use chalk_ir::interner::Interner;
 use chalk_ir::{Goal, InEnvironment, Substitution, UCanonical};
 use tracing::debug;
 
-pub struct Forest<I: Interner, C: Context<I>> {
+pub(crate) struct Forest<I: Interner, C: Context<I>> {
     pub(crate) tables: Tables<I>,
 
     /// This is a clock which always increases. It is

chalk-engine/src/lib.rs

@@ -68,7 +68,10 @@ pub mod context;
 mod derived;
 pub mod forest;
 mod logic;
+mod normalize_deep;
 mod simplify;
+pub mod slg;
+pub mod solve;
 mod stack;
 mod strand;
 mod table;

chalk-solve/src/infer/normalize_deep.rs → chalk-engine/src/normalize_deep.rs

@@ -2,10 +2,14 @@ use chalk_ir::fold::shift::Shift;
 use chalk_ir::fold::{Fold, Folder};
 use chalk_ir::interner::Interner;
 use chalk_ir::*;
+use chalk_solve::infer::InferenceTable;
 
-use super::InferenceTable;
+pub(crate) struct DeepNormalizer<'table, 'i, I: Interner> {
+    table: &'table mut InferenceTable<I>,
+    interner: &'i I,
+}
 
-impl<I: Interner> InferenceTable<I> {
+impl<I: Interner> DeepNormalizer<'_, '_, I> {
     /// Given a value `value` with variables in it, replaces those variables
     /// with their instantiated values (if any). Uninstantiated variables are
     /// left as-is.
@@ -17,24 +21,23 @@ impl<I: Interner> InferenceTable<I> {
     /// See also `InferenceTable::canonicalize`, which -- during real
     /// processing -- is often used to capture the "current state" of
     /// variables.
-    pub(crate) fn normalize_deep<T: Fold<I>>(&mut self, interner: &I, value: &T) -> T::Result {
+    pub fn normalize_deep<T: Fold<I>>(
+        table: &mut InferenceTable<I>,
+        interner: &I,
+        value: &T,
+    ) -> T::Result {
         value
             .fold_with(
                 &mut DeepNormalizer {
                     interner,
-                    table: self,
+                    table: table,
                 },
                 DebruijnIndex::INNERMOST,
             )
             .unwrap()
     }
 }
 
-struct DeepNormalizer<'table, 'i, I: Interner> {
-    table: &'table mut InferenceTable<I>,
-    interner: &'i I,
-}
-
 impl<'i, I: Interner> Folder<'i, I> for DeepNormalizer<'_, 'i, I>
 where
     I: 'i,
@@ -102,3 +105,35 @@ where
         self.interner()
     }
 }
+
+#[cfg(test)]
+mod test {
+    use super::*;
+    use chalk_integration::interner::ChalkIr;
+    use chalk_integration::{arg, ty, ty_name};
+
+    const U0: UniverseIndex = UniverseIndex { counter: 0 };
+
+    #[test]
+    fn infer() {
+        let interner = &ChalkIr;
+        let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
+        let environment0 = Environment::new(interner);
+        let a = table.new_variable(U0).to_ty(interner);
+        let b = table.new_variable(U0).to_ty(interner);
+        table
+            .unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
+            .unwrap();
+        assert_eq!(
+            DeepNormalizer::normalize_deep(&mut table, interner, &a),
+            ty!(apply (item 0) (expr b))
+        );
+        table
+            .unify(interner, &environment0, &b, &ty!(apply (item 1)))
+            .unwrap();
+        assert_eq!(
+            DeepNormalizer::normalize_deep(&mut table, interner, &a),
+            ty!(apply (item 0) (apply (item 1)))
+        );
+    }
+}

chalk-solve/src/solve/slg.rs → chalk-engine/src/slg.rs

@@ -1,58 +1,26 @@
-use crate::clauses::program_clauses_for_goal;
-use crate::coinductive_goal::IsCoinductive;
-use crate::infer::ucanonicalize::UCanonicalized;
-use crate::infer::unify::UnificationResult;
-use crate::infer::InferenceTable;
-use crate::solve::truncate;
-use crate::RustIrDatabase;
+use crate::context;
+use crate::normalize_deep::DeepNormalizer;
+use crate::{ExClause, Literal};
+
 use chalk_derive::HasInterner;
-use chalk_engine::context;
-use chalk_engine::{ExClause, Literal};
 use chalk_ir::cast::Cast;
 use chalk_ir::cast::Caster;
 use chalk_ir::interner::Interner;
 use chalk_ir::*;
-
-use std::fmt::{Debug, Display};
+use chalk_solve::clauses::program_clauses_for_goal;
+use chalk_solve::coinductive_goal::IsCoinductive;
+use chalk_solve::infer::ucanonicalize::UCanonicalized;
+use chalk_solve::infer::unify::UnificationResult;
+use chalk_solve::infer::InferenceTable;
+use chalk_solve::solve::truncate;
+use chalk_solve::RustIrDatabase;
+
+use std::fmt::Debug;
 use std::marker::PhantomData;
 
 pub(crate) mod aggregate;
 mod resolvent;
 
-#[derive(Debug)]
-pub enum SubstitutionResult<S> {
-    Definite(S),
-    Ambiguous(S),
-    Floundered,
-}
-
-impl<S> SubstitutionResult<S> {
-    pub fn as_ref(&self) -> SubstitutionResult<&S> {
-        match self {
-            SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst),
-            SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst),
-            SubstitutionResult::Floundered => SubstitutionResult::Floundered,
-        }
-    }
-    pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> {
-        match self {
-            SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)),
-            SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)),
-            SubstitutionResult::Floundered => SubstitutionResult::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"),
-        }
-    }
-}
-
 #[derive(Clone, Debug, HasInterner)]
 pub(crate) struct SlgContext<I: Interner> {
     phantom: PhantomData<I>,
@@ -111,7 +79,7 @@ impl<'me, I: Interner> context::ContextOps<I, SlgContext<I>> for SlgContextOps<'
         map: &UniverseMap,
         value: &Canonical<InEnvironment<Goal<I>>>,
     ) -> Canonical<InEnvironment<Goal<I>>> {
-        use crate::infer::ucanonicalize::UniverseMapExt;
+        use chalk_solve::infer::ucanonicalize::UniverseMapExt;
         map.map_from_canonical(self.program.interner(), value)
     }
 
@@ -120,7 +88,7 @@ impl<'me, I: Interner> context::ContextOps<I, SlgContext<I>> for SlgContextOps<'
         map: &UniverseMap,
         value: &Canonical<AnswerSubst<I>>,
     ) -> Canonical<AnswerSubst<I>> {
-        use crate::infer::ucanonicalize::UniverseMapExt;
+        use chalk_solve::infer::ucanonicalize::UniverseMapExt;
         map.map_from_canonical(self.program.interner(), value)
     }
 
@@ -276,7 +244,11 @@ impl<I: Interner> context::UnificationOps<I, SlgContext<I>> for TruncatingInfere
     }
 
     fn debug_ex_clause<'v>(&mut self, interner: &I, value: &'v ExClause<I>) -> Box<dyn Debug + 'v> {
-        Box::new(self.infer.normalize_deep(interner, value))
+        Box::new(DeepNormalizer::normalize_deep(
+            &mut self.infer,
+            interner,
+            value,
+        ))
     }
 
     fn fully_canonicalize_goal(

chalk-solve/src/solve/slg/aggregate.rs → chalk-engine/src/slg/aggregate.rs

@@ -1,14 +1,14 @@
-use crate::ext::*;
-use crate::infer::InferenceTable;
-use crate::solve::slg::SlgContextOps;
-use crate::solve::slg::SubstitutionExt;
-use crate::solve::{Guidance, Solution};
+use crate::context::{self, AnswerResult, ContextOps};
+use crate::slg::SlgContextOps;
+use crate::slg::SubstitutionExt;
+use crate::CompleteAnswer;
 use chalk_ir::cast::Cast;
 use chalk_ir::interner::Interner;
 use chalk_ir::*;
+use chalk_solve::ext::*;
+use chalk_solve::infer::InferenceTable;
+use chalk_solve::solve::{Guidance, Solution};
 
-use chalk_engine::context::{self, AnswerResult, ContextOps};
-use chalk_engine::CompleteAnswer;
 use std::fmt::Debug;
 
 /// Methods for combining solutions to yield an aggregate solution.
@@ -507,63 +507,71 @@ impl<I: Interner> AntiUnifier<'_, '_, I> {
     }
 }
 
-/// Test the equivalent of `Vec<i32>` vs `Vec<u32>`
-#[test]
-fn vec_i32_vs_vec_u32() {
-    use chalk_integration::interner::ChalkIr;
-    let mut infer: InferenceTable<ChalkIr> = InferenceTable::new();
-    let mut anti_unifier = AntiUnifier {
-        infer: &mut infer,
-        universe: UniverseIndex::root(),
-        interner: &ChalkIr,
-    };
-
-    let ty = anti_unifier.aggregate_tys(
-        &ty!(apply (item 0) (apply (item 1))),
-        &ty!(apply (item 0) (apply (item 2))),
-    );
-    assert_eq!(ty!(apply (item 0) (infer 0)), ty);
-}
+#[cfg(test)]
+mod test {
+    use crate::slg::aggregate::AntiUnifier;
+    use chalk_integration::{arg, ty, ty_name};
+    use chalk_ir::UniverseIndex;
+    use chalk_solve::infer::InferenceTable;
+
+    /// Test the equivalent of `Vec<i32>` vs `Vec<u32>`
+    #[test]
+    fn vec_i32_vs_vec_u32() {
+        use chalk_integration::interner::ChalkIr;
+        let mut infer: InferenceTable<ChalkIr> = InferenceTable::new();
+        let mut anti_unifier = AntiUnifier {
+            infer: &mut infer,
+            universe: UniverseIndex::root(),
+            interner: &ChalkIr,
+        };
 
-/// Test the equivalent of `Vec<i32>` vs `Vec<i32>`
-#[test]
-fn vec_i32_vs_vec_i32() {
-    use chalk_integration::interner::ChalkIr;
-    let interner = &ChalkIr;
-    let mut infer: InferenceTable<ChalkIr> = InferenceTable::new();
-    let mut anti_unifier = AntiUnifier {
-        interner,
-        infer: &mut infer,
-        universe: UniverseIndex::root(),
-    };
-
-    let ty = anti_unifier.aggregate_tys(
-        &ty!(apply (item 0) (apply (item 1))),
-        &ty!(apply (item 0) (apply (item 1))),
-    );
-    assert_eq!(ty!(apply (item 0) (apply (item 1))), ty);
-}
+        let ty = anti_unifier.aggregate_tys(
+            &ty!(apply (item 0) (apply (item 1))),
+            &ty!(apply (item 0) (apply (item 2))),
+        );
+        assert_eq!(ty!(apply (item 0) (infer 0)), ty);
+    }
 
-/// Test the equivalent of `Vec<X>` vs `Vec<Y>`
-#[test]
-fn vec_x_vs_vec_y() {
-    use chalk_integration::interner::ChalkIr;
-    let interner = &ChalkIr;
-    let mut infer: InferenceTable<ChalkIr> = InferenceTable::new();
-    let mut anti_unifier = AntiUnifier {
-        interner,
-        infer: &mut infer,
-        universe: UniverseIndex::root(),
-    };
-
-    // Note that the `var 0` and `var 1` in these types would be
-    // referring to canonicalized free variables, not variables in
-    // `infer`.
-    let ty = anti_unifier.aggregate_tys(
-        &ty!(apply (item 0) (infer 0)),
-        &ty!(apply (item 0) (infer 1)),
-    );
-
-    // But this `var 0` is from `infer.
-    assert_eq!(ty!(apply (item 0) (infer 0)), ty);
+    /// Test the equivalent of `Vec<i32>` vs `Vec<i32>`
+    #[test]
+    fn vec_i32_vs_vec_i32() {
+        use chalk_integration::interner::ChalkIr;
+        let interner = &ChalkIr;
+        let mut infer: InferenceTable<ChalkIr> = InferenceTable::new();
+        let mut anti_unifier = AntiUnifier {
+            interner,
+            infer: &mut infer,
+            universe: UniverseIndex::root(),
+        };
+
+        let ty = anti_unifier.aggregate_tys(
+            &ty!(apply (item 0) (apply (item 1))),
+            &ty!(apply (item 0) (apply (item 1))),
+        );
+        assert_eq!(ty!(apply (item 0) (apply (item 1))), ty);
+    }
+
+    /// Test the equivalent of `Vec<X>` vs `Vec<Y>`
+    #[test]
+    fn vec_x_vs_vec_y() {
+        use chalk_integration::interner::ChalkIr;
+        let interner = &ChalkIr;
+        let mut infer: InferenceTable<ChalkIr> = InferenceTable::new();
+        let mut anti_unifier = AntiUnifier {
+            interner,
+            infer: &mut infer,
+            universe: UniverseIndex::root(),
+        };
+
+        // Note that the `var 0` and `var 1` in these types would be
+        // referring to canonicalized free variables, not variables in
+        // `infer`.
+        let ty = anti_unifier.aggregate_tys(
+            &ty!(apply (item 0) (infer 0)),
+            &ty!(apply (item 0) (infer 1)),
+        );
+
+        // But this `var 0` is from `infer.
+        assert_eq!(ty!(apply (item 0) (infer 0)), ty);
+    }
 }