Merge pull request #215 from detrumi/simplify-crate-structure

Simplify crate structure

Author: nikomatsakis

Cargo.lock

@@ -49,8 +49,4 @@ path = "chalk-engine"
 version = "0.1.0"
 path = "chalk-rust-ir"
 
-[dependencies.chalk-rules]
-version = "0.1.0"
-path = "chalk-rules"
-
 [workspace]

Cargo.toml

@@ -10,7 +10,11 @@ keywords = ["compiler", "traits", "prolog"]
 edition = "2018"
 
 [dependencies]
+derive-new = "0.5.6"
 ena = "0.10.1"
+failure = "0.1"
+itertools = "0.7.8"
+petgraph = "0.4.13"
 
 [dependencies.chalk-macros]
 version = "0.1.0"
@@ -23,3 +27,7 @@ path = "../chalk-engine"
 [dependencies.chalk-ir]
 version = "0.1.0"
 path = "../chalk-ir"
+
+[dependencies.chalk-rust-ir]
+version = "0.1.0"
+path = "../chalk-rust-ir"

chalk-rules/Cargo.toml

@@ -1,4 +1,4 @@
-use crate::RustIrSource;
+use crate::RustIrDatabase;
 use chalk_ir::cast::{Cast, Caster};
 use chalk_ir::fold::shift::Shift;
 use chalk_ir::fold::Subst;
@@ -10,7 +10,7 @@ use std::iter;
 /// or struct definition) into its associated "program clauses" --
 /// that is, into the lowered, logical rules that it defines.
 pub trait ToProgramClauses {
-    fn to_program_clauses(&self, program: &dyn RustIrSource, clauses: &mut Vec<ProgramClause>);
+    fn to_program_clauses(&self, program: &dyn RustIrDatabase, clauses: &mut Vec<ProgramClause>);
 }
 
 impl ToProgramClauses for ImplDatum {
@@ -22,7 +22,7 @@ impl ToProgramClauses for ImplDatum {
     ///     Implemented(Vec<T>: Clone) :- Implemented(T: Clone).
     /// }
     /// ```
-    fn to_program_clauses(&self, _program: &dyn RustIrSource, clauses: &mut Vec<ProgramClause>) {
+    fn to_program_clauses(&self, _program: &dyn RustIrDatabase, clauses: &mut Vec<ProgramClause>) {
         clauses.push(
             self.binders
                 .map_ref(|bound| ProgramClauseImplication {
@@ -69,7 +69,7 @@ pub fn push_auto_trait_impls(
     auto_trait: &TraitDatum,
     struct_id: StructId,
     struct_datum: &StructDatum,
-    program: &dyn RustIrSource,
+    program: &dyn RustIrDatabase,
     vec: &mut Vec<ProgramClause>,
 ) {
     // Must be an auto trait.
@@ -153,7 +153,7 @@ impl ToProgramClauses for AssociatedTyValue {
     ///         Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>).
     /// }
     /// ```
-    fn to_program_clauses(&self, program: &dyn RustIrSource, clauses: &mut Vec<ProgramClause>) {
+    fn to_program_clauses(&self, program: &dyn RustIrDatabase, clauses: &mut Vec<ProgramClause>) {
         let impl_datum = program.impl_datum(self.impl_id);
         let associated_ty = program.associated_ty_data(self.associated_ty_id);
 
@@ -309,7 +309,7 @@ impl ToProgramClauses for StructDatum {
     /// forall<T> { DownstreamType(Box<T>) :- DownstreamType(T). }
     /// ```
     ///
-    fn to_program_clauses(&self, _program: &dyn RustIrSource, clauses: &mut Vec<ProgramClause>) {
+    fn to_program_clauses(&self, _program: &dyn RustIrDatabase, clauses: &mut Vec<ProgramClause>) {
         let wf = self
             .binders
             .map_ref(|bound_datum| ProgramClauseImplication {
@@ -552,7 +552,7 @@ impl ToProgramClauses for TraitDatum {
     /// To implement fundamental traits, we simply just do not add the rule above that allows
     /// upstream types to implement upstream traits. Fundamental traits are not allowed to
     /// compatibly do that.
-    fn to_program_clauses(&self, _program: &dyn RustIrSource, clauses: &mut Vec<ProgramClause>) {
+    fn to_program_clauses(&self, _program: &dyn RustIrDatabase, clauses: &mut Vec<ProgramClause>) {
         let trait_ref = self.binders.value.trait_ref.clone();
 
         let trait_ref_impl = WhereClause::Implemented(self.binders.value.trait_ref.clone());
@@ -777,7 +777,7 @@ impl ToProgramClauses for AssociatedTyDatum {
     ///     FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self, 'a,T>).
     /// }
     /// ```
-    fn to_program_clauses(&self, program: &dyn RustIrSource, clauses: &mut Vec<ProgramClause>) {
+    fn to_program_clauses(&self, program: &dyn RustIrDatabase, clauses: &mut Vec<ProgramClause>) {
         let binders: Vec<_> = self
             .parameter_kinds
             .iter()

chalk-rules/src/lib.rs

@@ -1,6 +1,7 @@
 use petgraph::prelude::*;
 
-use crate::ChalkRulesDatabase;
+use crate::solve::SolverChoice;
+use crate::ChalkSolveDatabase;
 use chalk_ir::{self, Identifier, ImplId, TraitId};
 use derive_new::new;
 use failure::Fallible;
@@ -13,9 +14,10 @@ mod solve;
 #[derive(new)]
 pub struct CoherenceSolver<'db, DB>
 where
-    DB: ChalkRulesDatabase,
+    DB: ChalkSolveDatabase,
 {
     db: &'db DB,
+    solver_choice: SolverChoice,
     trait_id: TraitId,
 }
 
@@ -56,7 +58,7 @@ pub struct SpecializationPriority(usize);
 
 impl<'db, DB> CoherenceSolver<'db, DB>
 where
-    DB: ChalkRulesDatabase,
+    DB: ChalkSolveDatabase,
 {
     pub fn specialization_priorities(&self) -> Fallible<Arc<SpecializationPriorities>> {
         let mut result = SpecializationPriorities::default();

chalk-solve/Cargo.toml

@@ -1,8 +1,9 @@
 use crate::coherence::CoherenceError;
-use crate::ChalkRulesDatabase;
+use crate::ext::GoalExt;
+use crate::solve::SolverChoice;
+use crate::ChalkSolveDatabase;
 use chalk_ir::cast::*;
 use chalk_ir::*;
-use chalk_solve::ext::*;
 use failure::Fallible;
 
 // Test if a local impl violates the orphan rules.
@@ -12,10 +13,11 @@ use failure::Fallible;
 //     forall<T> { LocalImplAllowed(MyType<T>: Trait) }
 //
 // This must be provable in order to pass the orphan check.
-pub fn perform_orphan_check<DB>(db: &DB, impl_id: ImplId) -> Fallible<()>
-where
-    DB: ChalkRulesDatabase,
-{
+pub fn perform_orphan_check(
+    db: &dyn ChalkSolveDatabase,
+    solver_choice: SolverChoice,
+    impl_id: ImplId,
+) -> Fallible<()> {
     debug_heading!("orphan_check(impl={:#?})", impl_id);
 
     let impl_datum = db.impl_datum(impl_id);
@@ -30,7 +32,10 @@ where
         .cast();
 
     let canonical_goal = &impl_allowed.into_closed_goal();
-    let is_allowed = db.solve(canonical_goal).is_some();
+    let is_allowed = solver_choice
+        .into_solver()
+        .solve(db, canonical_goal)
+        .is_some();
     debug!("overlaps = {:?}", is_allowed);
 
     if !is_allowed {

chalk-rules/src/clauses.rs renamed to chalk-solve/src/clauses.rs

@@ -1,17 +1,17 @@
 use crate::coherence::{CoherenceError, CoherenceSolver};
-use crate::ChalkRulesDatabase;
+use crate::ext::*;
+use crate::ChalkSolveDatabase;
+use crate::Solution;
 use chalk_ir::cast::*;
 use chalk_ir::fold::shift::Shift;
 use chalk_ir::*;
 use chalk_rust_ir::*;
-use chalk_solve::ext::*;
-use chalk_solve::Solution;
 use failure::Fallible;
 use itertools::Itertools;
 
 impl<'db, DB> CoherenceSolver<'db, DB>
 where
-    DB: ChalkRulesDatabase,
+    DB: ChalkSolveDatabase,
 {
     pub(super) fn visit_specializations_of_trait(
         &self,
@@ -135,7 +135,10 @@ where
             .negate();
 
         let canonical_goal = &goal.into_closed_goal();
-        let solution = self.db.solve(canonical_goal);
+        let solution = self
+            .solver_choice
+            .into_solver()
+            .solve(self.db, canonical_goal);
         let result = match solution {
             // Goal was proven with a unique solution, so no impl was found that causes these two
             // to overlap
@@ -214,7 +217,11 @@ where
             .quantify(QuantifierKind::ForAll, more_special.binders.binders.clone());
 
         let canonical_goal = &goal.into_closed_goal();
-        let result = match self.db.solve(canonical_goal) {
+        let result = match self
+            .solver_choice
+            .into_solver()
+            .solve(self.db, canonical_goal)
+        {
             Some(sol) => sol.is_unique(),
             None => false,
         };

chalk-rules/src/coherence.rs renamed to chalk-solve/src/coherence.rs

@@ -17,7 +17,9 @@ impl IsCoinductive for Goal {
     fn is_coinductive(&self, db: &dyn ChalkSolveDatabase) -> bool {
         match self {
             Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Holds(wca))) => match wca {
-                WhereClause::Implemented(tr) => db.is_coinductive_trait(tr.trait_id),
+                WhereClause::Implemented(tr) => {
+                    db.trait_datum(tr.trait_id).binders.value.flags.auto
+                }
                 WhereClause::ProjectionEq(..) => false,
             },
             Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..)))) => true,