Merge pull request #514 from declanvk/issue-511

Refactor ProgramClauseData to remove Implies variant

Author: jackh726

chalk-integration/src/lowering.rs

@@ -1671,7 +1671,7 @@ impl LowerClause for Clause {
             .into_iter()
             .map(
                 |implication: chalk_ir::Binders<chalk_ir::ProgramClauseImplication<ChalkIr>>| {
-                    chalk_ir::ProgramClauseData::ForAll(implication).intern(interner)
+                    chalk_ir::ProgramClauseData(implication).intern(interner)
                 },
             )
             .collect();

chalk-ir/src/cast.rs

@@ -199,12 +199,14 @@ where
     I: Interner,
 {
     fn cast_to(self, interner: &I) -> ProgramClause<I> {
-        ProgramClauseData::Implies(ProgramClauseImplication {
+        let implication = ProgramClauseImplication {
             consequence: self.cast(interner),
             conditions: Goals::new(interner),
             priority: ClausePriority::High,
-        })
-        .intern(interner)
+        };
+
+        ProgramClauseData(Binders::empty(interner, implication.shifted_in(interner)))
+            .intern(interner)
     }
 }
 
@@ -214,7 +216,7 @@ where
     T: HasInterner<Interner = I> + CastTo<DomainGoal<I>>,
 {
     fn cast_to(self, interner: &I) -> ProgramClause<I> {
-        ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication {
+        ProgramClauseData(self.map(|bound| ProgramClauseImplication {
             consequence: bound.cast(interner),
             conditions: Goals::new(interner),
             priority: ClausePriority::High,
@@ -223,18 +225,6 @@ where
     }
 }
 
-impl<I: Interner> CastTo<ProgramClause<I>> for ProgramClauseImplication<I> {
-    fn cast_to(self, interner: &I) -> ProgramClause<I> {
-        ProgramClauseData::Implies(self).intern(interner)
-    }
-}
-
-impl<I: Interner> CastTo<ProgramClause<I>> for Binders<ProgramClauseImplication<I>> {
-    fn cast_to(self, interner: &I) -> ProgramClause<I> {
-        ProgramClauseData::ForAll(self).intern(interner)
-    }
-}
-
 impl<T, U> CastTo<Option<U>> for Option<T>
 where
     T: CastTo<U>,

chalk-ir/src/could_match.rs

@@ -68,15 +68,7 @@ where
 
 impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClauseData<I> {
     fn could_match(&self, interner: &I, other: &DomainGoal<I>) -> bool {
-        match self {
-            ProgramClauseData::Implies(implication) => {
-                implication.consequence.could_match(interner, other)
-            }
-
-            ProgramClauseData::ForAll(clause) => {
-                clause.value.consequence.could_match(interner, other)
-            }
-        }
+        self.0.value.consequence.could_match(interner, other)
     }
 }
 

chalk-ir/src/debug.rs

@@ -699,10 +699,7 @@ impl<T: HasInterner + Debug> Debug for Binders<T> {
 
 impl<I: Interner> Debug for ProgramClauseData<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
-        match self {
-            ProgramClauseData::Implies(pc) => write!(fmt, "{:?}", pc),
-            ProgramClauseData::ForAll(pc) => write!(fmt, "{:?}", pc),
-        }
+        write!(fmt, "{:?}", self.0)
     }
 }
 

chalk-ir/src/fold.rs

@@ -9,6 +9,7 @@ mod boring_impls;
 pub mod shift;
 mod subst;
 
+pub use self::shift::Shift;
 pub use self::subst::Subst;
 
 /// A "folder" is a transformer that can be used to make a copy of

chalk-ir/src/fold/boring_impls.rs

@@ -290,14 +290,7 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClauseData<
         I: 'i,
         TI: 'i,
     {
-        match self {
-            ProgramClauseData::Implies(pci) => Ok(ProgramClauseData::Implies(
-                pci.fold_with(folder, outer_binder)?,
-            )),
-            ProgramClauseData::ForAll(pci) => Ok(ProgramClauseData::ForAll(
-                pci.fold_with(folder, outer_binder)?,
-            )),
-        }
+        Ok(ProgramClauseData(self.0.fold_with(folder, outer_binder)?))
     }
 }
 

chalk-ir/src/lib.rs

@@ -1732,10 +1732,7 @@ impl std::ops::BitAnd for ClausePriority {
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, Fold, HasInterner, Zip)]
-pub enum ProgramClauseData<I: Interner> {
-    Implies(ProgramClauseImplication<I>),
-    ForAll(Binders<ProgramClauseImplication<I>>),
-}
+pub struct ProgramClauseData<I: Interner>(pub Binders<ProgramClauseImplication<I>>);
 
 impl<I: Interner> ProgramClauseImplication<I> {
     pub fn into_from_env_clause(self, interner: &I) -> ProgramClauseImplication<I> {
@@ -1753,14 +1750,7 @@ impl<I: Interner> ProgramClauseImplication<I> {
 
 impl<I: Interner> ProgramClauseData<I> {
     pub fn into_from_env_clause(self, interner: &I) -> ProgramClauseData<I> {
-        match self {
-            ProgramClauseData::Implies(implication) => {
-                ProgramClauseData::Implies(implication.into_from_env_clause(interner))
-            }
-            ProgramClauseData::ForAll(binders_implication) => ProgramClauseData::ForAll(
-                binders_implication.map(|i| i.into_from_env_clause(interner)),
-            ),
-        }
+        ProgramClauseData(self.0.map(|i| i.into_from_env_clause(interner)))
     }
 
     pub fn intern(self, interner: &I) -> ProgramClause<I> {

chalk-ir/src/visit/boring_impls.rs

@@ -6,9 +6,9 @@
 
 use crate::{
     AdtId, AssocTypeId, ClausePriority, DebruijnIndex, FloatTy, FnDefId, GenericArg, Goals, ImplId,
-    IntTy, Interner, Mutability, OpaqueTyId, PlaceholderIndex, ProgramClause, ProgramClauseData,
-    ProgramClauses, QuantifiedWhereClauses, QuantifierKind, Scalar, Substitution, SuperVisit,
-    TraitId, UintTy, UniverseIndex, Visit, VisitResult, Visitor,
+    IntTy, Interner, Mutability, OpaqueTyId, PlaceholderIndex, ProgramClause, ProgramClauses,
+    QuantifiedWhereClauses, QuantifierKind, Scalar, Substitution, SuperVisit, TraitId, UintTy,
+    UniverseIndex, Visit, VisitResult, Visitor,
 };
 use std::{marker::PhantomData, sync::Arc};
 
@@ -247,10 +247,7 @@ impl<I: Interner> SuperVisit<I> for ProgramClause<I> {
     {
         let interner = visitor.interner();
 
-        match self.data(interner) {
-            ProgramClauseData::Implies(pci) => pci.visit_with(visitor, outer_binder),
-            ProgramClauseData::ForAll(pci) => pci.visit_with(visitor, outer_binder),
-        }
+        self.data(interner).0.visit_with(visitor, outer_binder)
     }
 }
 

chalk-solve/src/clauses/builder.rs

@@ -3,7 +3,7 @@ use std::marker::PhantomData;
 
 use crate::cast::{Cast, CastTo};
 use crate::RustIrDatabase;
-use chalk_ir::fold::Fold;
+use chalk_ir::fold::{Fold, Shift};
 use chalk_ir::interner::{HasInterner, Interner};
 use chalk_ir::*;
 
@@ -77,18 +77,20 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
             priority,
         };
 
-        if self.binders.len() == 0 {
-            self.clauses
-                .push(ProgramClauseData::Implies(clause).intern(interner));
+        let clause = if self.binders.is_empty() {
+            // Compensate for the added empty binder
+            clause.shifted_in(interner)
         } else {
-            self.clauses.push(
-                ProgramClauseData::ForAll(Binders::new(
-                    VariableKinds::from(interner, self.binders.clone()),
-                    clause,
-                ))
-                .intern(interner),
-            );
-        }
+            clause
+        };
+
+        self.clauses.push(
+            ProgramClauseData(Binders::new(
+                VariableKinds::from(interner, self.binders.clone()),
+                clause,
+            ))
+            .intern(interner),
+        );
 
         debug!("pushed clause {:?}", self.clauses.last());
     }

chalk-solve/src/recursive/solve.rs

@@ -1,7 +1,6 @@
 use super::combine;
 use super::fulfill::{Fulfill, RecursiveInferenceTable};
 use super::lib::{Guidance, Minimums, Solution, UCanonicalGoal};
-use super::Solver;
 use crate::clauses::program_clauses_for_goal;
 use crate::infer::{InferenceTable, ParameterEnaVariableExt};
 use crate::{solve::truncate, RustIrDatabase};
@@ -13,7 +12,7 @@ use chalk_ir::{debug, debug_heading, info_heading};
 use chalk_ir::{
     Binders, Canonical, ClausePriority, Constraint, DomainGoal, Environment, Fallible, Floundered,
     GenericArg, Goal, GoalData, InEnvironment, NoSolution, ProgramClause, ProgramClauseData,
-    ProgramClauseImplication, Substitution, UCanonical, UniverseMap, VariableKinds,
+    ProgramClauseImplication, Substitution, UCanonical, UniverseMap,
 };
 use std::fmt::Debug;
 
@@ -144,19 +143,9 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
                 return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High);
             }
 
-            let res = match program_clause.data(self.interner()) {
-                ProgramClauseData::Implies(implication) => self.solve_via_implication(
-                    canonical_goal,
-                    &Binders::new(
-                        VariableKinds::from(self.interner(), vec![]),
-                        implication.clone(),
-                    ),
-                    minimums,
-                ),
-                ProgramClauseData::ForAll(implication) => {
-                    self.solve_via_implication(canonical_goal, implication, minimums)
-                }
-            };
+            let ProgramClauseData(implication) = program_clause.data(self.interner());
+            let res = self.solve_via_implication(canonical_goal, implication, minimums);
+
             if let (Ok(solution), priority) = res {
                 debug!("ok: solution={:?} prio={:?}", solution, priority);
                 cur_solution = Some(match cur_solution {