Goal builder

chalk-ir/src/cast.rs

@@ -80,6 +80,7 @@ reflexive_impl!(for(I: Interner) TraitRef<I>);
 reflexive_impl!(for(I: Interner) DomainGoal<I>);
 reflexive_impl!(for(I: Interner) Goal<I>);
 reflexive_impl!(for(I: Interner) WhereClause<I>);
+reflexive_impl!(for(I: Interner) ProgramClause<I>);
 
 impl<I: Interner> CastTo<WhereClause<I>> for TraitRef<I> {
     fn cast_to(self, _interner: &I) -> WhereClause<I> {

chalk-ir/src/fold/shift.rs

@@ -21,7 +21,7 @@ pub trait Shift<I: Interner>: Fold<I, I> {
     fn shifted_out_to(&self, interner: &I, target_binder: DebruijnIndex) -> Fallible<Self::Result>;
 }
 
-impl<T: Fold<I, I> + Eq, I: Interner> Shift<I> for T {
+impl<T: Fold<I, I>, I: Interner> Shift<I> for T {
     fn shifted_in(&self, interner: &I) -> Self::Result {
         self.shifted_in_from(interner, DebruijnIndex::ONE)
     }

chalk-ir/src/lib.rs

@@ -182,6 +182,11 @@ impl<I: Interner> Ty<I> {
         WellFormed::Ty(self.clone())
     }
 
+    /// Creates a domain goal `FromEnv(T)` where `T` is this type.
+    pub fn into_from_env_goal(self, interner: &I) -> DomainGoal<I> {
+        self.from_env().cast(interner)
+    }
+
     /// If this is a `TyData::BoundVar(d)`, returns `Some(d)` else `None`.
     pub fn bound(&self, interner: &I) -> Option<BoundVar> {
         if let TyData::BoundVar(bv) = self.data(interner) {

chalk-rust-ir/src/lib.rs

@@ -20,6 +20,8 @@ pub enum LangItem {}
 #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct AssociatedTyValueId<I: Interner>(pub I::DefId);
 
+chalk_ir::id_fold!(AssociatedTyValueId);
+
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct ImplDatum<I: Interner> {
     pub polarity: Polarity,
@@ -38,7 +40,7 @@ impl<I: Interner> ImplDatum<I> {
     }
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+#[derive(Clone, Debug, PartialEq, Eq, Hash, HasInterner, Fold)]
 pub struct ImplDatumBound<I: Interner> {
     pub trait_ref: TraitRef<I>,
     pub where_clauses: Vec<QuantifiedWhereClause<I>>,

chalk-solve/src/coherence/solve.rs

@@ -1,6 +1,6 @@
 use crate::coherence::{CoherenceError, CoherenceSolver};
 use crate::ext::*;
-use crate::Solution;
+use crate::{goal_builder::GoalBuilder, Solution};
 use chalk_ir::cast::*;
 use chalk_ir::fold::shift::Shift;
 use chalk_ir::interner::Interner;
@@ -34,7 +34,7 @@ impl<I: Interner> CoherenceSolver<'_, I> {
             // the other. Note that specialization can only run one way - if both
             // specialization checks return *either* true or false, that's an error.
             if !self.disjoint(lhs, rhs) {
-                match (self.specializes(lhs, rhs), self.specializes(rhs, lhs)) {
+                match (self.specializes(l_id, r_id), self.specializes(r_id, l_id)) {
                     (true, false) => record_specialization(l_id, r_id),
                     (false, true) => record_specialization(r_id, l_id),
                     (_, _) => {
@@ -145,23 +145,56 @@ impl<I: Interner> CoherenceSolver<'_, I> {
         result
     }
 
-    // Test for specialization.
+    // Creates a goal which, if provable, means "more special" impl specializes the "less special" one.
     //
-    // If this test succeeds, the second impl specializes the first.
+    // # General rule
     //
-    // Example lowering:
+    // Given the more special impl:
     //
-    // more: impl<T: Clone> Foo for Vec<T>
-    // less: impl<U: Clone> Foo for U
+    // ```ignore
+    // impl<P0..Pn> SomeTrait<T1..Tm> for T0 where WC_more
+    // ```
     //
+    // and less special impl
+    //
+    // ```ignore
+    // impl<Q0..Qo> SomeTrait<U1..Um> for U0 where WC_less
+    // ```
+    //
+    // create the goal:
+    //
+    // ```ignore
+    // forall<P0..Pn> {
+    //   if (WC_more) {}
+    //     exists<Q0..Qo> {
+    //       T0 = U0, ..., Tm = Um,
+    //       WC_less
+    //     }
+    //   }
+    // }
+    // ```
+    //
+    // # Example
+    //
+    // Given:
+    //
+    // * more: `impl<T: Clone> Foo for Vec<T>`
+    // * less: `impl<U: Clone> Foo for U`
+    //
+    // Resulting goal:
+    //
+    // ```ignore
     // forall<T> {
     //  if (T: Clone) {
     //    exists<U> {
     //      Vec<T> = U, U: Clone
     //    }
     //  }
     // }
-    fn specializes(&self, less_special: &ImplDatum<I>, more_special: &ImplDatum<I>) -> bool {
+    // ```
+    fn specializes(&self, less_special_id: ImplId<I>, more_special_id: ImplId<I>) -> bool {
+        let more_special = &self.db.impl_datum(more_special_id);
+        let less_special = &self.db.impl_datum(less_special_id);
         debug_heading!(
             "specializes(less_special={:#?}, more_special={:#?})",
             less_special,
@@ -170,66 +203,54 @@ impl<I: Interner> CoherenceSolver<'_, I> {
 
         let interner = self.db.interner();
 
-        // Negative impls cannot specialize.
-        if !less_special.is_positive() || !more_special.is_positive() {
-            return false;
-        }
+        let gb = &mut GoalBuilder::new(self.db);
 
-        // Create parameter equality goals. Note that parameters from
-        // the "more special" goal have to be "shifted in" across the
-        // binder for the "less special" impl.
-        let more_special_params = params(interner, more_special)
-            .iter()
-            .map(|p| p.shifted_in(interner));
-        let less_special_params = params(interner, less_special).iter().cloned();
-        let params_goals = more_special_params
-            .zip(less_special_params)
-            .map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner));
+        // forall<P0..Pn> { ... }
+        let goal = gb.forall(
+            &more_special.binders,
+            less_special_id,
+            |gb, _, more_special_impl, less_special_id| {
+                // if (WC_more) { ... }
+                gb.implies(more_special_impl.where_clauses.iter().cloned(), |gb| {
+                    let less_special = &gb.db().impl_datum(less_special_id);
 
-        // Create less special where clause goals. These reference the parameters
-        // from the "less special" impl, which are at the same debruijn depth here.
-        let less_special_wc = less_special
-            .binders
-            .value
-            .where_clauses
-            .iter()
-            .cloned()
-            .casted(interner);
+                    // exists<Q0..Qn> { ... }
+                    gb.exists(
+                        &less_special.binders,
+                        &more_special_impl.trait_ref,
+                        |gb, _, less_special_impl, more_special_trait_ref| {
+                            let interner = gb.interner();
 
-        // Create the "more special" where clause goals. These will be
-        // added as an implication without the "less special" goals in
-        // scope, no shift required.
-        let more_special_wc = more_special
-            .binders
-            .value
-            .where_clauses
-            .iter()
-            .cloned()
-            .casted(interner)
-            .collect();
+                            // T0 = U0, ..., Tm = Um
+                            let params_goals = more_special_trait_ref
+                                .substitution
+                                .parameters(interner)
+                                .iter()
+                                .cloned()
+                                .zip(
+                                    less_special_impl
+                                        .trait_ref
+                                        .substitution
+                                        .parameters(interner)
+                                        .iter()
+                                        .cloned(),
+                                )
+                                .map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner));
 
-        // Join all of the goals together:
-        //
-        // forall<..more special..> {
-        //   if (<more special wc>) {
-        //     exists<..less special..> {
-        //       ..less special goals..
-        //       ..equality goals..
-        //     }
-        //   }
-        // }
-        let goal = Box::new(Goal::all(interner, params_goals.chain(less_special_wc)))
-            .quantify(
-                interner,
-                QuantifierKind::Exists,
-                less_special.binders.binders.clone(),
-            )
-            .implied_by(interner, more_special_wc)
-            .quantify(
-                interner,
-                QuantifierKind::ForAll,
-                more_special.binders.binders.clone(),
-            );
+                            // <less_special_wc_goals> = where clauses from the less special impl
+                            let less_special_wc_goals = less_special_impl
+                                .where_clauses
+                                .iter()
+                                .cloned()
+                                .casted(interner);
+
+                            // <equality_goals> && WC_less
+                            gb.all(params_goals.chain(less_special_wc_goals))
+                        },
+                    )
+                })
+            },
+        );
 
         let canonical_goal = &goal.into_closed_goal(interner);
         let result = match self

chalk-solve/src/goal_builder.rs

@@ -0,0 +1,156 @@
+use crate::RustIrDatabase;
+use cast::CastTo;
+use chalk_ir::cast::Cast;
+use chalk_ir::cast::Caster;
+use chalk_ir::*;
+use chalk_rust_ir::ToParameter;
+use fold::shift::Shift;
+use fold::Fold;
+use interner::{HasInterner, Interner};
+
+pub struct GoalBuilder<'i, I: Interner> {
+    db: &'i dyn RustIrDatabase<I>,
+}
+
+impl<'i, I: Interner> GoalBuilder<'i, I> {
+    pub fn new(db: &'i dyn RustIrDatabase<I>) -> Self {
+        GoalBuilder { db }
+    }
+
+    /// Returns the database within the goal builder.
+    pub fn db(&self) -> &'i dyn RustIrDatabase<I> {
+        self.db
+    }
+
+    /// Returns the interner within the goal builder.
+    pub fn interner(&self) -> &'i I {
+        self.db.interner()
+    }
+
+    /// Creates a goal that ensures all of the goals from the `goals`
+    /// iterator are met (e.g., `goals[0] && ... && goals[N]`).
+    pub fn all<GS, G>(&mut self, goals: GS) -> Goal<I>
+    where
+        GS: IntoIterator<Item = G>,
+        G: CastTo<Goal<I>>,
+    {
+        Goal::all(self.interner(), goals.into_iter().casted(self.interner()))
+    }
+
+    /// Creates a goal `clauses => goal`. The clauses are given as an iterator
+    /// and the goal is returned via the contained closure.
+    pub fn implies<CS, C, G>(&mut self, clauses: CS, goal: impl FnOnce(&mut Self) -> G) -> Goal<I>
+    where
+        CS: IntoIterator<Item = C>,
+        C: CastTo<ProgramClause<I>>,
+        G: CastTo<Goal<I>>,
+    {
+        GoalData::Implies(
+            clauses.into_iter().casted(self.interner()).collect(),
+            goal(self).cast(self.interner()),
+        )
+        .intern(self.interner())
+    }
+
+    /// Given a bound value `binders` like `<P0..Pn> V`,
+    /// creates a goal `forall<Q0..Qn> { G }` where
+    /// the goal `G` is created by invoking a helper
+    /// function `body`.
+    ///
+    /// # Parameters to `body`
+    ///
+    /// `body` will be invoked with:
+    ///
+    /// * the goal builder `self`
+    /// * the substitution `Q0..Qn`
+    /// * the bound value `[P0..Pn => Q0..Qn] V` instantiated
+    ///   with the substitution
+    /// * the value `passthru`, appropriately shifted so that
+    ///   any debruijn indices within account for the new binder
+    ///
+    /// # Why is `body` a function and not a closure?
+    ///
+    /// This is to ensure that `body` doesn't accidentally reference
+    /// values from the environment whose debruijn indices do not
+    /// account for the new binder being created.
+    pub fn forall<G, B, P>(
+        &mut self,
+        binders: &Binders<B>,
+        passthru: P,
+        body: fn(&mut Self, Substitution<I>, &B, P::Result) -> G,
+    ) -> Goal<I>
+    where
+        B: Fold<I> + HasInterner<Interner = I>,
+        P: Fold<I>,
+        B::Result: std::fmt::Debug,
+        G: CastTo<Goal<I>>,
+    {
+        self.quantified(QuantifierKind::ForAll, binders, passthru, body)
+    }
+
+    /// Like [`GoalBuilder::forall`], but for a `exists<Q0..Qn> { G }` goal.
+    pub fn exists<G, B, P>(
+        &mut self,
+        binders: &Binders<B>,
+        passthru: P,
+        body: fn(&mut Self, Substitution<I>, &B, P::Result) -> G,
+    ) -> Goal<I>
+    where
+        B: Fold<I> + HasInterner<Interner = I>,
+        P: Fold<I>,
+        B::Result: std::fmt::Debug,
+        G: CastTo<Goal<I>>,
+    {
+        self.quantified(QuantifierKind::Exists, binders, passthru, body)
+    }
+
+    /// A combined helper functon for the various methods
+    /// to create `forall` and `exists` goals. See:
+    ///
+    /// * [`GoalBuilder::forall`]
+    /// * [`GoalBuilder::exists`]
+    ///
+    /// for details.
+    fn quantified<G, B, P>(
+        &mut self,
+        quantifier_kind: QuantifierKind,
+        binders: &Binders<B>,
+        passthru: P,
+        body: fn(&mut Self, Substitution<I>, &B, P::Result) -> G,
+    ) -> Goal<I>
+    where
+        B: Fold<I> + HasInterner<Interner = I>,
+        P: Fold<I>,
+        B::Result: std::fmt::Debug,
+        G: CastTo<Goal<I>>,
+    {
+        let interner = self.interner();
+
+        // Make an identity mapping `[0 => ^0.0, 1 => ^0.1, ..]`
+        // and so forth. This substitution is mapping from the `<P0..Pn>` variables
+        // in `binders` to the corresponding `P0..Pn` variables we're about to
+        // introduce in the form of a `forall<P0..Pn>` goal. Of course, it's
+        // actually an identity mapping, since this `forall` will be the innermost
+        // debruijn binder and so forth, so there's no actual reason to
+        // *do* the substitution, since it would effectively just be a clone.
+        let substitution: Substitution<I> = Substitution::from(
+            interner,
+            binders
+                .binders
+                .iter()
+                .zip(0..)
+                .map(|p| p.to_parameter(interner)),
+        );
+
+        // Shift passthru into one level of binder, to account for the `forall<P0..Pn>`
+        // we are about to introduce.
+        let passthru_shifted = passthru.shifted_in(self.interner());
+
+        // Invoke `body` function, which returns a goal, and wrap that goal in the binders
+        // from `binders`, and finally a `forall` or `exists` goal.
+        let bound_goal = binders.map_ref(|bound_value| {
+            body(self, substitution, bound_value, passthru_shifted).cast(interner)
+        });
+        GoalData::Quantified(quantifier_kind, bound_goal).intern(interner)
+    }
+}