Remove hhgoal

jackh726 · jackh726 · commit ae690eb56f75 · 2020-05-23T18:00:11.000-04:00
diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
@@ -5,7 +5,6 @@
 //! `DomainGoal` type, add arena lifetime parameters, and more. See
 //! [`Context`] trait for a list of types.
 
-use crate::hh::HhGoal;
 use crate::{CompleteAnswer, ExClause};
 use chalk_base::results::{Fallible, Floundered};
 use chalk_ir::interner::Interner;
@@ -40,11 +39,6 @@ pub trait Context<I: Interner>: Clone + Debug {
     /// Represents an inference table.
     type InferenceTable: InferenceTable<I, Self> + Clone;
 
-    /// How to relate two kinds when unifying: for example in rustc, we
-    /// may want to unify parameters either for the sub-typing relation or for
-    /// the equality relation.
-    type Variance;
-
     /// Selects the next appropriate subgoal index for evaluation.
     /// Used by: logic
     fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize;
@@ -141,16 +135,6 @@ pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug + Aggreg
         u_canon: &UCanonical<InEnvironment<Goal<I>>>,
         canonical_subst: &Canonical<AnswerSubst<I>>,
     ) -> bool;
-
-    /// 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, goal: Goal<I>) -> HhGoal<I, C>;
 }
 
 /// Methods for combining solutions to yield an aggregate solution.
@@ -238,7 +222,6 @@ pub trait UnificationOps<I: Interner, C: Context<I>> {
         &mut self,
         interner: &I,
         environment: &Environment<I>,
-        variance: C::Variance,
         a: &GenericArg<I>,
         b: &GenericArg<I>,
         ex_clause: &mut ExClause<I>,
diff --git a/chalk-engine/src/hh.rs b/chalk-engine/src/hh.rs
diff --git a/chalk-engine/src/lib.rs b/chalk-engine/src/lib.rs
@@ -66,7 +66,6 @@ mod boring_impls;
 pub mod context;
 mod derived;
 pub mod forest;
-pub mod hh;
 mod logic;
 mod simplify;
 mod stack;
diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs
@@ -2,7 +2,6 @@ use crate::context::{
     Context, ContextOps, InferenceTable, ResolventOps, TruncateOps, UnificationOps,
 };
 use crate::forest::Forest;
-use crate::hh::HhGoal;
 use crate::stack::{Stack, StackIndex};
 use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand};
 use crate::table::{AnswerIndex, Table};
@@ -12,7 +11,7 @@ use crate::{
 use chalk_base::results::{Floundered, NoSolution};
 
 use chalk_ir::interner::Interner;
-use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, Substitution, UCanonical, UniverseMap};
+use chalk_ir::{Canonical, ConstrainedSubst, Goal, GoalData, InEnvironment, Substitution, UCanonical, UniverseMap};
 
 type RootSearchResult<T> = Result<T, RootSearchFail>;
 
@@ -234,7 +233,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
     /// domain goal, these strands are created from the program
     /// clauses as well as the clauses found in the environment.  If
     /// the table represents a non-domain goal, such as `for<T> G`
-    /// etc, then `simplify_hh_goal` is invoked to create a strand
+    /// etc, then `simplify_goal` is invoked to create a strand
     /// that breaks the goal down.
     ///
     /// In terms of the NFTD paper, this corresponds to the *Program
@@ -247,8 +246,8 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
     ) -> Table<I> {
         let mut table = Table::new(goal.clone(), context.is_coinductive(&goal));
         let (mut infer, subst, environment, goal) = context.instantiate_ucanonical_goal(&goal);
-        match context.into_hh_goal(goal) {
-            HhGoal::DomainGoal(domain_goal) => {
+        match goal.data(context.interner()) {
+            GoalData::DomainGoal(domain_goal) => {
                 match context.program_clauses(&environment, &domain_goal, &mut infer) {
                     Ok(clauses) => {
                         for clause in clauses {
@@ -280,7 +279,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
                 }
             }
 
-            hh_goal => {
+            _ => {
                 // `canonical_goal` is an HH goal. We can simplify it
                 // into a series of *literals*, all of which must be
                 // true. Thus, in EWFS terms, we are effectively
@@ -290,7 +289,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
                 // applying built-in "meta program clauses" that
                 // reduce HH goals into Domain goals.
                 if let Ok(ex_clause) =
-                    Self::simplify_hh_goal(context, &mut infer, subst, environment, hh_goal)
+                    Self::simplify_goal(context, &mut infer, subst, environment, goal)
                 {
                     info!(
                         "pushing initial strand with ex-clause: {:#?}",
diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs
@@ -1,22 +1,21 @@
 use crate::context::{Context, ContextOps, InferenceTable};
 use crate::forest::Forest;
-use crate::hh::HhGoal;
 use crate::{ExClause, Literal, TimeStamp};
 use chalk_base::results::Fallible;
 
 use chalk_ir::interner::Interner;
-use chalk_ir::{Environment, InEnvironment, Substitution};
+use chalk_ir::{Environment, InEnvironment, Goal, GoalData, Substitution, QuantifierKind};
 
 impl<I: Interner, C: Context<I>> Forest<I, C> {
     /// Simplifies an HH goal into a series of positive domain goals
     /// and negative HH goals. This operation may fail if the HH goal
     /// includes unifications that cannot be completed.
-    pub(super) fn simplify_hh_goal(
+    pub(super) fn simplify_goal(
         context: &impl ContextOps<I, C>,
         infer: &mut dyn InferenceTable<I, C>,
         subst: Substitution<I>,
         initial_environment: Environment<I>,
-        initial_hh_goal: HhGoal<I, C>,
+        initial_hh_goal: Goal<I>,
     ) -> Fallible<ExClause<I>> {
         let mut ex_clause = ExClause {
             subst,
@@ -32,45 +31,46 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
         let mut pending_goals = vec![(initial_environment, initial_hh_goal)];
 
         while let Some((environment, hh_goal)) = pending_goals.pop() {
-            match hh_goal {
-                HhGoal::ForAll(subgoal) => {
+            match hh_goal.data(context.interner()) {
+                GoalData::Quantified(QuantifierKind::ForAll, subgoal) => {
                     let subgoal =
                         infer.instantiate_binders_universally(context.interner(), &subgoal);
-                    pending_goals.push((environment, context.into_hh_goal(subgoal)));
+                    pending_goals.push((environment, subgoal.clone()));
                 }
-                HhGoal::Exists(subgoal) => {
+                GoalData::Quantified(QuantifierKind::Exists, subgoal) => {
                     let subgoal =
                         infer.instantiate_binders_existentially(context.interner(), &subgoal);
-                    pending_goals.push((environment, context.into_hh_goal(subgoal)))
+                    pending_goals.push((environment, subgoal.clone()));
                 }
-                HhGoal::Implies(wc, subgoal) => {
-                    let new_environment = context.add_clauses(&environment, wc);
-                    pending_goals.push((new_environment, context.into_hh_goal(subgoal)));
+                GoalData::Implies(wc, subgoal) => {
+                    let new_environment = context.add_clauses(&environment, wc.clone());
+                    pending_goals.push((new_environment, subgoal.clone()));
                 }
-                HhGoal::All(subgoals) => {
-                    for subgoal in subgoals {
-                        pending_goals.push((environment.clone(), context.into_hh_goal(subgoal)));
+                GoalData::All(subgoals) => {
+                    for subgoal in subgoals.iter(context.interner()) {
+                        pending_goals.push((environment.clone(), subgoal.clone()));
                     }
                 }
-                HhGoal::Not(subgoal) => {
+                GoalData::Not(subgoal) => {
                     ex_clause
                         .subgoals
-                        .push(Literal::Negative(InEnvironment::new(&environment, subgoal)));
+                        .push(Literal::Negative(InEnvironment::new(&environment, subgoal.clone())));
                 }
-                HhGoal::Unify(variance, a, b) => infer.unify_generic_args_into_ex_clause(
-                    context.interner(),
-                    &environment,
-                    variance,
-                    &a,
-                    &b,
-                    &mut ex_clause,
-                )?,
-                HhGoal::DomainGoal(domain_goal) => {
+                GoalData::EqGoal(goal) => {
+                    infer.unify_generic_args_into_ex_clause(
+                        context.interner(),
+                        &environment,
+                        &goal.a,
+                        &goal.b,
+                        &mut ex_clause,
+                    )?
+                },
+                GoalData::DomainGoal(domain_goal) => {
                     ex_clause
                         .subgoals
-                        .push(Literal::Positive(InEnvironment::new(&environment, context.into_goal(domain_goal))));
+                        .push(Literal::Positive(InEnvironment::new(&environment, context.into_goal(domain_goal.clone()))));
                 }
-                HhGoal::CannotProve => {
+                GoalData::CannotProve(()) => {
                     ex_clause.ambiguous = true;
                 }
             }
diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs
@@ -9,8 +9,7 @@ use crate::RustIrDatabase;
 use chalk_base::results::{Fallible, Floundered};
 use chalk_derive::HasInterner;
 use chalk_engine::context;
-use chalk_engine::hh::HhGoal;
-use chalk_engine::{CompleteAnswer, ExClause, Literal};
+use chalk_engine::{ExClause, Literal};
 use chalk_ir::cast::Cast;
 use chalk_ir::cast::Caster;
 use chalk_ir::interner::Interner;
@@ -67,7 +66,6 @@ pub struct TruncatingInferenceTable<I: Interner> {
 impl<I: Interner> context::Context<I> for SlgContext<I> {
     type Solution = Solution<I>;
     type InferenceTable = TruncatingInferenceTable<I>;
-    type Variance = ();
 
     // Used by: logic
     fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize {
@@ -210,24 +208,6 @@ impl<'me, I: Interner> context::ContextOps<I, SlgContext<I>> for SlgContextOps<'
         let interner = self.interner();
         u_canon.is_trivial_substitution(interner, canonical_subst)
     }
-
-    fn into_hh_goal(&self, goal: Goal<I>) -> HhGoal<I, SlgContext<I>> {
-        let interner = self.interner();
-        match goal.data(interner).clone() {
-            GoalData::Quantified(QuantifierKind::ForAll, binders_goal) => {
-                HhGoal::ForAll(binders_goal)
-            }
-            GoalData::Quantified(QuantifierKind::Exists, binders_goal) => {
-                HhGoal::Exists(binders_goal)
-            }
-            GoalData::Implies(dg, subgoal) => HhGoal::Implies(dg, subgoal),
-            GoalData::All(goals) => HhGoal::All(goals.iter(interner).cloned().collect()),
-            GoalData::Not(g1) => HhGoal::Not(g1),
-            GoalData::EqGoal(EqGoal { a, b }) => HhGoal::Unify((), a, b),
-            GoalData::DomainGoal(domain_goal) => HhGoal::DomainGoal(domain_goal),
-            GoalData::CannotProve(()) => HhGoal::CannotProve,
-        }
-    }
 }
 
 impl<I: Interner> TruncatingInferenceTable<I> {
@@ -332,7 +312,6 @@ impl<I: Interner> context::UnificationOps<I, SlgContext<I>> for TruncatingInfere
         &mut self,
         interner: &I,
         environment: &Environment<I>,
-        _: (),
         a: &GenericArg<I>,
         b: &GenericArg<I>,
         ex_clause: &mut ExClause<I>,
