Simplify crate structure

Cargo.toml

@@ -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]

chalk-solve/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/src/clauses.rs → chalk-solve/src/clauses.rs

@@ -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/coherence.rs → chalk-solve/src/coherence.rs

@@ -1,6 +1,6 @@
 use petgraph::prelude::*;
 
-use crate::ChalkRulesDatabase;
+use crate::ChalkSolveDatabase;
 use chalk_ir::{self, Identifier, ImplId, TraitId};
 use derive_new::new;
 use failure::Fallible;
@@ -13,7 +13,7 @@ mod solve;
 #[derive(new)]
 pub struct CoherenceSolver<'db, DB>
 where
-    DB: ChalkRulesDatabase,
+    DB: ChalkSolveDatabase,
 {
     db: &'db DB,
     trait_id: TraitId,
@@ -56,7 +56,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-rules/src/coherence/orphan.rs → chalk-solve/src/coherence/orphan.rs

@@ -1,8 +1,8 @@
 use crate::coherence::CoherenceError;
-use crate::ChalkRulesDatabase;
+use crate::ext::GoalExt;
+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.
@@ -14,7 +14,7 @@ use failure::Fallible;
 // 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,
+    DB: ChalkSolveDatabase,
 {
     debug_heading!("orphan_check(impl={:#?})", impl_id);
 

chalk-rules/src/coherence/solve.rs → chalk-solve/src/coherence/solve.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,

chalk-solve/src/coinductive_goal.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,

chalk-solve/src/lib.rs

@@ -1,24 +1,78 @@
-use chalk_ir::{DomainGoal, ProgramClause, TraitId};
+use chalk_ir::*;
+use chalk_rust_ir::*;
 use std::fmt::Debug;
+use std::sync::Arc;
 
 #[macro_use]
 extern crate chalk_macros;
+#[macro_use]
+extern crate failure;
 
+pub mod clauses;
+pub mod coherence;
 mod coinductive_goal;
 pub mod ext;
 mod infer;
 mod solve;
+pub mod wf;
+
+pub trait GoalSolver {
+    fn solve(&self, goal: &UCanonical<InEnvironment<Goal>>) -> Option<Solution>;
+}
+
+pub trait RustIrDatabase {
+    /// Returns the datum for the associated type with the given id.
+    fn associated_ty_data(&self, ty: TypeId) -> Arc<AssociatedTyDatum>;
+
+    /// Returns the datum for the impl with the given id.
+    fn trait_datum(&self, trait_id: TraitId) -> Arc<TraitDatum>;
+
+    /// Returns the datum for the impl with the given id.
+    fn struct_datum(&self, struct_id: StructId) -> Arc<StructDatum>;
+
+    /// Returns the datum for the impl with the given id.
+    fn impl_datum(&self, impl_id: ImplId) -> Arc<ImplDatum>;
+
+    /// Returns all the impls for a given trait.
+    fn impls_for_trait(&self, trait_id: TraitId) -> Vec<ImplId>;
+
+    /// Returns true if there is an explicit impl of the auto trait
+    /// `auto_trait_id` for the struct `struct_id`. This is part of
+    /// the auto trait handling -- if there is no explicit impl given
+    /// by the user for the struct, then we provide default impls
+    /// based on the field types (otherwise, we rely on the impls the
+    /// user gave).
+    fn impl_provided_for(&self, auto_trait_id: TraitId, struct_id: StructId) -> bool;
+
+    /// Returns the name for the type with the given id.
+    fn type_name(&self, id: TypeKindId) -> Identifier;
+
+    /// Given a projection of an associated type, splits the type
+    /// parameters into two parts: those that come from the trait, and
+    /// those that come from the associated type itself.
+    ///
+    /// e.g. given a projection `<Foo as Iterable>::Item<'x>`, where `Iterable` is defined like so:
+    ///
+    /// ```ignore
+    /// trait Iterable { type Item<'a>; }
+    /// ```
+    ///
+    /// we would split into the type parameter lists `[Foo]` (from the
+    /// trait) and `['x]` (from the type).
+    fn split_projection<'p>(
+        &self,
+        projection: &'p ProjectionTy,
+    ) -> (Arc<AssociatedTyDatum>, &'p [Parameter], &'p [Parameter]);
+}
 
 /// The trait for defining the program clauses that are in scope when
 /// solving a goal.
-pub trait ChalkSolveDatabase: Debug {
+pub trait ChalkSolveDatabase: GoalSolver + RustIrDatabase + Debug {
     /// Returns a set of program clauses that could possibly match
     /// `goal`. This can be any superset of the correct set, but the
     /// more precise you can make it, the more efficient solving will
     /// be.
     fn program_clauses_that_could_match(&self, goal: &DomainGoal, vec: &mut Vec<ProgramClause>);
-
-    fn is_coinductive_trait(&self, trait_id: TraitId) -> bool;
 }
 
 pub use solve::Solution;