Merge pull request #120 from nikomatsakis/fewer-engine-traits

Fewer engine traits

Author: nikomatsakis

chalk-engine/src/context/mod.rs

@@ -8,7 +8,7 @@ crate mod prelude;
 
 /// The "context" in which the SLG solver operates.
 pub trait Context: Sized + Clone + Debug + ContextOps<Self> + AggregateOps<Self> {
-    type CanonicalExClause: CanonicalExClause<Self>;
+    type CanonicalExClause: Debug;
 
     /// A map between universes. These are produced when
     /// u-canonicalizing something; they map canonical results back to
@@ -41,33 +41,39 @@ pub trait Context: Sized + Clone + Debug + ContextOps<Self> + AggregateOps<Self>
     /// completely opaque to the SLG solver; it is produced by
     /// `make_solution`.
     type Solution;
+
+    /// Extracts the inner normalized substitution.
+    fn inference_normalized_subst(canon_ex_clause: &Self::CanonicalExClause)
+                                  -> &Self::InferenceNormalizedSubst;
+}
+
+pub trait ExClauseContext<C: Context>: Sized + Debug {
+    /// Represents a substitution from the "canonical variables" found
+    /// in a canonical goal to specific values.
+    type Substitution: Debug;
+
+    /// Represents a region constraint that will be propagated back
+    /// (but not verified).
+    type RegionConstraint: Debug;
+
+    /// Represents a goal along with an environment.
+    type GoalInEnvironment: Debug + Clone + Eq + Hash;
 }
 
 /// The set of types belonging to an "inference context"; in rustc,
 /// these types are tied to the lifetime of the arena within which an
 /// inference context operates.
-pub trait InferenceContext<C: Context>: Sized + Debug {
+pub trait InferenceContext<C: Context>: ExClauseContext<C> {
     /// Represents a set of hypotheses that are assumed to be true.
-    type Environment: Environment<C, Self>;
+    type Environment: Debug + Clone;
 
     /// Goals correspond to things we can prove.
-    type Goal: Goal<C, Self>;
+    type Goal: Clone + Debug + Eq;
 
     /// A goal that can be targeted by a program clause. The SLG
     /// solver treats these opaquely; in contrast, it understands
     /// "meta" goals like `G1 && G2` and so forth natively.
-    type DomainGoal: DomainGoal<C, Self>;
-
-    /// Represents a goal along with an environment.
-    type GoalInEnvironment: GoalInEnvironment<C, Self>;
-
-    /// Represents a region constraint that will be propagated back
-    /// (but not verified).
-    type RegionConstraint: Debug;
-
-    /// Represents a substitution from the "canonical variables" found
-    /// in a canonical goal to specific values.
-    type Substitution: Debug;
+    type DomainGoal: Debug;
 
     /// A "higher-order" goal, quantified over some types and/or
     /// lifetimes. When you have a quantification, like `forall<T> { G
@@ -89,7 +95,34 @@ pub trait InferenceContext<C: Context>: Sized + Debug {
 
     /// The successful result from unification: contains new subgoals
     /// and things that can be attached to an ex-clause.
-    type UnificationResult: UnificationResult<C, Self>;
+    type UnificationResult;
+
+    fn goal_in_environment(environment: &Self::Environment, goal: Self::Goal) -> Self::GoalInEnvironment;
+    
+    /// Upcast this domain goal into a more general goal.
+    fn into_goal(domain_goal: Self::DomainGoal) -> Self::Goal;
+
+    /// Create a "cannot prove" goal (see `HhGoal::CannotProve`).
+    fn cannot_prove() -> Self::Goal;
+
+    /// Convert the context's goal type into the `HhGoal` type that
+    /// the SLG solver understands. The expectation is that the
+    /// context's goal type has the same set of variants, but with
+    /// different names and a different setup. If you inspect
+    /// `HhGoal`, you will see that this is a "shallow" or "lazy"
+    /// conversion -- that is, we convert the outermost goal into an
+    /// `HhGoal`, but the goals contained within are left as context
+    /// goals.
+    fn into_hh_goal(goal: Self::Goal) -> HhGoal<C, Self>;
+
+    /// Add the residual subgoals as new subgoals of the ex-clause.
+    /// Also add region constraints.
+    fn into_ex_clause(result: Self::UnificationResult, ex_clause: &mut ExClause<C, Self>);
+
+    // Used by: simplify
+    fn add_clauses(env: &Self::Environment,
+                  clauses: impl IntoIterator<Item = Self::ProgramClause>)
+                  -> Self::Environment;
 }
 
 pub trait ContextOps<C: Context> {
@@ -273,27 +306,6 @@ pub trait ResolventOps<C: Context, I: InferenceContext<C>> {
     ) -> Fallible<ExClause<C, I>>;
 }
 
-pub trait GoalInEnvironment<C: Context, I: InferenceContext<C>>:
-    Debug + Clone + Eq + Ord + Hash
-{
-    fn new(
-        environment: &I::Environment,
-        goal: I::Goal,
-    ) -> Self;
-
-    fn environment(&self) -> &I::Environment;
-}
-
-pub trait Environment<C: Context, I: InferenceContext<C>>: Debug + Clone {
-    // Used by: simplify
-    fn add_clauses(&self, clauses: impl IntoIterator<Item = I::ProgramClause>) -> Self;
-}
-
-pub trait CanonicalExClause<C: Context>: Debug {
-    /// Extracts the inner normalized substitution.
-    fn inference_normalized_subst(&self) -> &C::InferenceNormalizedSubst;
-}
-
 pub trait CanonicalConstrainedSubst<C: Context>: Clone + Debug + Eq + Hash + Ord {
     /// True if this solution has no region constraints.
     fn empty_constraints(&self) -> bool;
@@ -302,26 +314,6 @@ pub trait CanonicalConstrainedSubst<C: Context>: Clone + Debug + Eq + Hash + Ord
     fn inference_normalized_subst(&self) -> &C::InferenceNormalizedSubst;
 }
 
-pub trait DomainGoal<C: Context, I: InferenceContext<C>>: Debug {
-    /// Upcast this domain goal into a more general goal.
-    fn into_goal(self) -> I::Goal;
-}
-
-pub trait Goal<C: Context, I: InferenceContext<C>>: Clone + Debug + Eq {
-    /// Create a "cannot prove" goal (see `HhGoal::CannotProve`).
-    fn cannot_prove() -> Self;
-
-    /// Convert the context's goal type into the `HhGoal` type that
-    /// the SLG solver understands. The expectation is that the
-    /// context's goal type has the same set of variants, but with
-    /// different names and a different setup. If you inspect
-    /// `HhGoal`, you will see that this is a "shallow" or "lazy"
-    /// conversion -- that is, we convert the outermost goal into an
-    /// `HhGoal`, but the goals contained within are left as context
-    /// goals.
-    fn into_hh_goal(self) -> HhGoal<C, I>;
-}
-
 pub trait UniverseMap<C: Context>: Clone + Debug {
     /// Convert a goal G *from* the canonical universes *into* our
     /// local universes. This will yield a goal G' that is the same
@@ -341,23 +333,12 @@ pub trait UniverseMap<C: Context>: Clone + Debug {
     ) -> C::CanonicalConstrainedSubst;
 }
 
-/// Embodies the result of a unification operation: we presume that
-/// unification may produce new residual subgoals, which must be
-/// further proven, as well as region constraints.
-pub trait UnificationResult<C: Context, I: InferenceContext<C>> {
-    /// Add the residual subgoals as new subgoals of the ex-clause.
-    /// Also add region constraints.
-    fn into_ex_clause(self, ex_clause: &mut ExClause<C, I>);
-}
-
 pub trait AnswerStream<C: Context> {
     fn peek_answer(&mut self) -> Option<SimplifiedAnswer<C>>;
     fn next_answer(&mut self) -> Option<SimplifiedAnswer<C>>;
 
     /// Invokes `test` with each possible future answer, returning true immediately
     /// if we find any answer for which `test` returns true.
-    fn any_future_answer(
-        &mut self,
-        test: impl FnMut(&C::InferenceNormalizedSubst) -> bool,
-    ) -> bool;
+    fn any_future_answer(&mut self, test: impl FnMut(&C::InferenceNormalizedSubst) -> bool)
+        -> bool;
 }

chalk-engine/src/context/prelude.rs

@@ -4,15 +4,8 @@ crate use super::Context;
 crate use super::ContextOps;
 crate use super::ResolventOps;
 crate use super::TruncateOps;
-crate use super::Environment;
 crate use super::InferenceTable;
 crate use super::InferenceContext;
-crate use super::UnificationResult;
-crate use super::GoalInEnvironment;
 crate use super::UCanonicalGoalInEnvironment;
 crate use super::UniverseMap;
-crate use super::CanonicalExClause;
 crate use super::CanonicalConstrainedSubst;
-crate use super::Goal;
-crate use super::DomainGoal;
-

chalk-engine/src/derived.rs

@@ -119,7 +119,7 @@ impl<C: Context> Hash for DelayedLiteral<C> {
 
 ///////////////////////////////////////////////////////////////////////////
 
-impl<C: Context, I: InferenceContext<C>> PartialEq for Literal<C, I> {
+impl<C: Context, I: ExClauseContext<C>> PartialEq for Literal<C, I> {
     fn eq(&self, other: &Literal<C, I>) -> bool {
         match (self, other) {
             (Literal::Positive(goal1), Literal::Positive(goal2))
@@ -130,10 +130,10 @@ impl<C: Context, I: InferenceContext<C>> PartialEq for Literal<C, I> {
     }
 }
 
-impl<C: Context, I: InferenceContext<C>> Eq for Literal<C, I> {
+impl<C: Context, I: ExClauseContext<C>> Eq for Literal<C, I> {
 }
 
-impl<C: Context, I: InferenceContext<C>> Hash for Literal<C, I> {
+impl<C: Context, I: ExClauseContext<C>> Hash for Literal<C, I> {
     fn hash<H: Hasher>(&self, state: &mut H) {
         mem::discriminant(self).hash(state);
         match self {

chalk-engine/src/lib.rs

@@ -55,12 +55,11 @@
 #![feature(in_band_lifetimes)]
 #![feature(macro_vis_matcher)]
 #![feature(step_trait)]
-#![feature(underscore_lifetimes)]
 
 #[macro_use] extern crate chalk_macros;
 extern crate stacker;
 
-use crate::context::{Context, InferenceContext};
+use crate::context::{Context, ExClauseContext};
 use std::collections::HashSet;
 use std::cmp::min;
 use std::usize;
@@ -105,20 +104,20 @@ struct DepthFirstNumber {
 
 /// The paper describes these as `A :- D | G`.
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
-pub struct ExClause<C: Context, I: InferenceContext<C>> {
+pub struct ExClause<C: Context, E: ExClauseContext<C>> {
     /// The substitution which, applied to the goal of our table,
     /// would yield A.
-    pub subst: I::Substitution,
+    pub subst: E::Substitution,
 
     /// Delayed literals: things that we depend on negatively,
     /// but which have not yet been fully evaluated.
     pub delayed_literals: Vec<DelayedLiteral<C>>,
 
     /// Region constraints we have accumulated.
-    pub constraints: Vec<I::RegionConstraint>,
+    pub constraints: Vec<E::RegionConstraint>,
 
     /// Subgoals: literals that must be proven
-    pub subgoals: Vec<Literal<C, I>>,
+    pub subgoals: Vec<Literal<C, E>>,
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -185,9 +184,9 @@ pub enum DelayedLiteral<C: Context> {
 
 /// Either `A` or `~A`, where `A` is a `Env |- Goal`.
 #[derive(Clone, Debug)]
-pub enum Literal<C: Context, I: InferenceContext<C>> { // FIXME: pub b/c fold
-    Positive(I::GoalInEnvironment),
-    Negative(I::GoalInEnvironment),
+pub enum Literal<C: Context, E: ExClauseContext<C>> { // FIXME: pub b/c fold
+    Positive(E::GoalInEnvironment),
+    Negative(E::GoalInEnvironment),
 }
 
 /// The `Minimums` structure is used to track the dependencies between

chalk-engine/src/logic.rs

@@ -115,7 +115,7 @@ impl<C: Context> Forest<C> {
         }
 
         self.tables[table].strands_mut().any(|strand| {
-            test(strand.canonical_ex_clause.inference_normalized_subst())
+            test(C::inference_normalized_subst(&strand.canonical_ex_clause))
         })
     }
 
@@ -760,7 +760,7 @@ impl<C: Context> Forest<C> {
         goal: I::Goal,
     ) {
         let table_ref = &mut self.tables[table];
-        match goal.into_hh_goal() {
+        match I::into_hh_goal(goal) {
             HhGoal::DomainGoal(domain_goal) => {
                 let clauses = infer.program_clauses(&environment, &domain_goal);
                 for clause in clauses {

chalk-engine/src/simplify.rs

@@ -28,35 +28,35 @@ impl<C: Context> Forest<C> {
             match hh_goal {
                 HhGoal::ForAll(subgoal) => {
                     let subgoal = infer.instantiate_binders_universally(&subgoal);
-                    pending_goals.push((environment, subgoal.into_hh_goal()));
+                    pending_goals.push((environment, I::into_hh_goal(subgoal)));
                 }
                 HhGoal::Exists(subgoal) => {
                     let subgoal = infer.instantiate_binders_existentially(&subgoal);
-                    pending_goals.push((environment, subgoal.into_hh_goal()))
+                    pending_goals.push((environment, I::into_hh_goal(subgoal)))
                 }
                 HhGoal::Implies(wc, subgoal) => {
-                    let new_environment = environment.add_clauses(wc);
-                    pending_goals.push((new_environment, subgoal.into_hh_goal()));
+                    let new_environment = I::add_clauses(&environment, wc);
+                    pending_goals.push((new_environment, I::into_hh_goal(subgoal)));
                 }
                 HhGoal::And(subgoal1, subgoal2) => {
-                    pending_goals.push((environment.clone(), subgoal1.into_hh_goal()));
-                    pending_goals.push((environment, subgoal2.into_hh_goal()));
+                    pending_goals.push((environment.clone(), I::into_hh_goal(subgoal1)));
+                    pending_goals.push((environment, I::into_hh_goal(subgoal2)));
                 }
                 HhGoal::Not(subgoal) => {
                     ex_clause
                         .subgoals
-                        .push(Literal::Negative(I::GoalInEnvironment::new(&environment, subgoal)));
+                        .push(Literal::Negative(I::goal_in_environment(&environment, subgoal)));
                 }
                 HhGoal::Unify(a, b) => {
-                    infer.unify_parameters(&environment, &a, &b)?
-                        .into_ex_clause(&mut ex_clause)
+                    I::into_ex_clause(infer.unify_parameters(&environment, &a, &b)?,
+                                      &mut ex_clause)
                 }
                 HhGoal::DomainGoal(domain_goal) => {
                     ex_clause
                         .subgoals
-                        .push(Literal::Positive(I::GoalInEnvironment::new(
+                        .push(Literal::Positive(I::goal_in_environment(
                             &environment,
-                            domain_goal.into_goal(),
+                            I::into_goal(domain_goal),
                         )));
                 }
                 HhGoal::CannotProve => {
@@ -66,10 +66,10 @@ impl<C: Context> Forest<C> {
                     // course, will always create a negative cycle and
                     // hence a delayed literal that cannot be
                     // resolved.
-                    let goal = I::Goal::cannot_prove();
+                    let goal = I::cannot_prove();
                     ex_clause
                         .subgoals
-                        .push(Literal::Negative(I::GoalInEnvironment::new(&environment, goal)));
+                        .push(Literal::Negative(I::goal_in_environment(&environment, goal)));
                 }
             }
         }

src/lib.rs

@@ -9,7 +9,6 @@
 #![feature(macro_vis_matcher)]
 #![feature(specialization)]
 #![feature(step_trait)]
-#![feature(underscore_lifetimes)]
 
 extern crate chalk_parse;
 #[macro_use]