Add ConstEq to many match cases

JulianKnodt · JulianKnodt · commit a3f8ea960d2f · 2022-05-05T04:07:30.000Z
Where trivial, add ConstEq, otherwise defer to todos
diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs
@@ -570,6 +570,9 @@ pub fn program_clauses_that_could_match<I: Interner>(
                 })
             });
         }
+        DomainGoal::Holds(WhereClause::ConstEq(const_eq)) => {
+            todo!()
+        }
         DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
         | DomainGoal::LocalImplAllowed(trait_ref) => {
             db.trait_datum(trait_ref.trait_id)
@@ -1071,6 +1074,7 @@ fn match_ty<I: Interner>(
                                 vec![DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()))]
                             }
                             WhereClause::AliasEq(_)
+                            | WhereClause::ConstEq(_)
                             | WhereClause::LifetimeOutlives(_)
                             | WhereClause::TypeOutlives(_) => vec![],
                         }
diff --git a/chalk-solve/src/clauses/dyn_ty.rs b/chalk-solve/src/clauses/dyn_ty.rs
@@ -72,7 +72,7 @@ pub(super) fn build_dyn_self_ty_clauses<I: Interner>(
                     )
                 }
                 // FIXME: Associated item bindings are just taken as facts (?)
-                WhereClause::AliasEq(_) => builder.push_fact(bound),
+                WhereClause::AliasEq(_) | WhereClause::ConstEq(_) => builder.push_fact(bound),
                 WhereClause::LifetimeOutlives(..) => {}
                 WhereClause::TypeOutlives(..) => {}
             });
diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs
@@ -206,7 +206,7 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
                         )
                     }
                     // FIXME: Associated item bindings are just taken as facts (?)
-                    WhereClause::AliasEq(_) => builder.push_fact(bound),
+                    WhereClause::AliasEq(_) | WhereClause::ConstEq(_) => builder.push_fact(bound),
                     WhereClause::LifetimeOutlives(..) => {}
                     WhereClause::TypeOutlives(..) => {}
                 });
diff --git a/chalk-solve/src/clauses/super_traits.rs b/chalk-solve/src/clauses/super_traits.rs
@@ -93,9 +93,10 @@ pub fn super_traits<I: Interner>(
                                 }
                                 Some(tr.clone())
                             }
-                            WhereClause::AliasEq(_) => None,
-                            WhereClause::LifetimeOutlives(..) => None,
-                            WhereClause::TypeOutlives(..) => None,
+                            WhereClause::AliasEq(_)
+                            | WhereClause::LifetimeOutlives(..)
+                            | WhereClause::ConstEq(_)
+                            | WhereClause::TypeOutlives(..) => None,
                         })
                     })
                     .collect::<Vec<_>>()
diff --git a/chalk-solve/src/coinductive_goal.rs b/chalk-solve/src/coinductive_goal.rs
@@ -23,9 +23,10 @@ impl<I: Interner> IsCoinductive<I> for Goal<I> {
                     db.trait_datum(tr.trait_id).is_auto_trait()
                         || db.trait_datum(tr.trait_id).is_coinductive_trait()
                 }
-                WhereClause::AliasEq(..) => false,
-                WhereClause::LifetimeOutlives(..) => false,
-                WhereClause::TypeOutlives(..) => false,
+                WhereClause::AliasEq(_)
+                | WhereClause::LifetimeOutlives(..)
+                | WhereClause::TypeOutlives(..)
+                | WhereClause::ConstEq(_) => false,
             },
             GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
             GoalData::Quantified(QuantifierKind::ForAll, goal) => {
diff --git a/chalk-solve/src/display.rs b/chalk-solve/src/display.rs
@@ -165,6 +165,7 @@ fn display_self_where_clauses_as_bounds<'a, I: Interner>(
                                 }
                                 AliasTy::Opaque(opaque) => opaque.display(s).fmt(f),
                             },
+                            WhereClause::ConstEq(_) => todo!(),
                             WhereClause::LifetimeOutlives(lifetime) => lifetime.display(s).fmt(f),
                             WhereClause::TypeOutlives(ty) => ty.display(s).fmt(f),
                         }
diff --git a/chalk-solve/src/display/bounds.rs b/chalk-solve/src/display/bounds.rs
@@ -91,6 +91,7 @@ impl<I: Interner> RenderAsRust<I> for WhereClause<I> {
         match self {
             WhereClause::Implemented(trait_ref) => trait_ref.fmt(s, f),
             WhereClause::AliasEq(alias_eq) => alias_eq.fmt(s, f),
+            WhereClause::ConstEq(const_eq) => const_eq.fmt(s, f),
             WhereClause::LifetimeOutlives(lifetime) => lifetime.display(s).fmt(f),
             WhereClause::TypeOutlives(ty) => ty.display(s).fmt(f),
         }
@@ -153,6 +154,12 @@ impl<I: Interner> RenderAsRust<I> for AliasEq<I> {
     }
 }
 
+impl<I: Interner> RenderAsRust<I> for ConstEq<I> {
+    fn fmt(&self, s: &InternalWriterState<'_, I>, f: &'_ mut Formatter<'_>) -> Result {
+        todo!()
+    }
+}
+
 impl<I: Interner> RenderAsRust<I> for LifetimeOutlives<I> {
     fn fmt(&self, s: &InternalWriterState<'_, I>, f: &mut Formatter<'_>) -> Result {
         // a': 'b
diff --git a/chalk-solve/src/display/stub.rs b/chalk-solve/src/display/stub.rs
@@ -44,7 +44,7 @@ impl<I: Interner, DB: RustIrDatabase<I>> RustIrDatabase<I> for StubWrapper<'_, D
     fn associated_ty_data(
         &self,
         ty: chalk_ir::AssocItemId<I>,
-    ) -> std::sync::Arc<crate::rust_ir::AssociatedTyDatum<I>> {
+    ) -> Arc<crate::rust_ir::AssociatedTyDatum<I>> {
         let mut v = (*self.db.associated_ty_data(ty)).clone();
         v.binders = Binders::new(
             v.binders.binders.clone(),
@@ -56,6 +56,13 @@ impl<I: Interner, DB: RustIrDatabase<I>> RustIrDatabase<I> for StubWrapper<'_, D
         Arc::new(v)
     }
 
+    fn associated_const_data(
+        &self,
+        ct: chalk_ir::AssocItemId<I>,
+    ) -> Arc<crate::rust_ir::AssociatedConstDatum<I>> {
+        Arc::new((*self.db.associated_const_data(ct)).clone())
+    }
+
     fn trait_datum(
         &self,
         trait_id: chalk_ir::TraitId<I>,
diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs
@@ -672,6 +672,9 @@ impl<'t, I: Interner> Unifier<'t, I> {
                                         self.table.new_variable(universe_index).to_ty(interner);
                                     WhereClause::AliasEq(AliasEq { alias, ty })
                                 }
+                                WhereClause::ConstEq(ConstEq { term, ct }) => {
+                                    todo!();
+                                }
                                 WhereClause::TypeOutlives(_) => {
                                     let lifetime_var = self.table.new_variable(universe_index);
                                     let lifetime = lifetime_var.to_lifetime(interner);
diff --git a/chalk-solve/src/lib.rs b/chalk-solve/src/lib.rs
@@ -49,6 +49,9 @@ pub trait RustIrDatabase<I: Interner>: Debug {
     /// Returns the datum for the associated type with the given id.
     fn associated_ty_data(&self, ty: AssocItemId<I>) -> Arc<AssociatedTyDatum<I>>;
 
+    /// Returns the datum for the associated type with the given id.
+    fn associated_const_data(&self, ty: AssocItemId<I>) -> Arc<AssociatedConstDatum<I>>;
+
     /// Returns the datum for the definition with the given id.
     fn trait_datum(&self, trait_id: TraitId<I>) -> Arc<TraitDatum<I>>;
 
diff --git a/chalk-solve/src/logging_db.rs b/chalk-solve/src/logging_db.rs
@@ -128,6 +128,15 @@ where
         ty_datum
     }
 
+    fn associated_const_data(
+        &self,
+        ct: chalk_ir::AssocItemId<I>,
+    ) -> Arc<crate::rust_ir::AssociatedConstDatum<I>> {
+        let ct_datum = self.ws.db().associated_const_data(ct);
+        self.record(ct_datum.trait_id);
+        ct_datum
+    }
+
     fn trait_datum(&self, trait_id: TraitId<I>) -> Arc<TraitDatum<I>> {
         self.record(trait_id);
         self.ws.db().trait_datum(trait_id)
@@ -402,6 +411,13 @@ where
         self.db.associated_ty_data(ty)
     }
 
+    fn associated_const_data(
+        &self,
+        ct: chalk_ir::AssocItemId<I>,
+    ) -> Arc<crate::rust_ir::AssociatedConstDatum<I>> {
+        self.db.associated_const_data(ct)
+    }
+
     fn trait_datum(&self, trait_id: TraitId<I>) -> Arc<TraitDatum<I>> {
         self.db.trait_datum(trait_id)
     }
diff --git a/chalk-solve/src/logging_db/id_collector.rs b/chalk-solve/src/logging_db/id_collector.rs
@@ -154,6 +154,10 @@ impl<'i, I: Interner, DB: RustIrDatabase<I>> Visitor<I> for IdCollector<'i, I, D
         match where_clause {
             WhereClause::Implemented(trait_ref) => self.record(trait_ref.trait_id),
             WhereClause::AliasEq(alias_eq) => self.visit_alias(&alias_eq.alias),
+            WhereClause::ConstEq(const_eq) => {
+                self.db.associated_const_data(const_eq.term);
+                self.visit_const(&const_eq.ct, outer_binder)?;
+            }
             WhereClause::LifetimeOutlives(_lifetime_outlives) => (),
             WhereClause::TypeOutlives(_type_outlives) => (),
         }
diff --git a/chalk-solve/src/rust_ir.rs b/chalk-solve/src/rust_ir.rs
@@ -524,6 +524,30 @@ impl<I: Interner> Visit<I> for AssociatedTyDatum<I> {
     }
 }
 
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct AssociatedConstDatum<I: Interner> {
+    /// The trait this associated type is defined in.
+    pub trait_id: TraitId<I>,
+
+    /// The ID of this associated type
+    pub id: AssocItemId<I>,
+
+    /// Name of this associated type.
+    pub name: I::Identifier,
+}
+
+// Manual implementation to avoid I::Identifier type.
+impl<I: Interner> Visit<I> for AssociatedConstDatum<I> {
+    fn visit_with<B>(
+        &self,
+        visitor: &mut dyn chalk_ir::visit::Visitor<I, BreakTy = B>,
+        outer_binder: DebruijnIndex,
+    ) -> ControlFlow<B> {
+        try_break!(self.trait_id.visit_with(visitor, outer_binder));
+        self.id.visit_with(visitor, outer_binder)
+    }
+}
+
 /// Encodes the parts of `AssociatedTyDatum` where the parameters
 /// `P0..Pm` are in scope (`bounds` and `where_clauses`).
 #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit, HasInterner)]
diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs
@@ -90,6 +90,10 @@ impl<I: Interner> Visitor<I> for InputTypeCollector<I> {
                 .clone()
                 .intern(self.interner)
                 .visit_with(self, outer_binder),
+            WhereClause::ConstEq(const_eq) => {
+                const_eq.term.visit_with(self, outer_binder)?;
+                const_eq.ct.visit_with(self, outer_binder)
+            }
             WhereClause::Implemented(trait_ref) => trait_ref.visit_with(self, outer_binder),
             WhereClause::TypeOutlives(TypeOutlives { ty, .. }) => ty.visit_with(self, outer_binder),
             WhereClause::LifetimeOutlives(..) => ControlFlow::Continue(()),

Original file line number	Diff line number	Diff line change
`@@ -570,6 +570,9 @@ pub fn program_clauses_that_could_match<I: Interner>(`
`570`	`570`	`})`
`571`	`571`	`});`
`572`	`572`	`}`
	`573`	`+ DomainGoal::Holds(WhereClause::ConstEq(const_eq)) => {`
	`574`	`+ todo!()`
	`575`	`+ }`
`573`	`576`	`DomainGoal::WellFormed(WellFormed::Trait(trait_ref))`
`574`	`577`	`\| DomainGoal::LocalImplAllowed(trait_ref) => {`
`575`	`578`	`db.trait_datum(trait_ref.trait_id)`
`@@ -1071,6 +1074,7 @@ fn match_ty<I: Interner>(`
`1071`	`1074`	`vec![DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()))]`
`1072`	`1075`	`}`
`1073`	`1076`	`WhereClause::AliasEq(_)`
	`1077`	`+ \| WhereClause::ConstEq(_)`
`1074`	`1078`	`\| WhereClause::LifetimeOutlives(_)`
`1075`	`1079`	`\| WhereClause::TypeOutlives(_) => vec![],`
`1076`	`1080`	`}`
Original file line number	Diff line number	Diff line change
`@@ -72,7 +72,7 @@ pub(super) fn build_dyn_self_ty_clauses<I: Interner>(`
`72`	`72`	`)`
`73`	`73`	`}`
`74`	`74`	`// FIXME: Associated item bindings are just taken as facts (?)`
`75`		`- WhereClause::AliasEq(_) => builder.push_fact(bound),`
	`75`	`+ WhereClause::AliasEq(_) \| WhereClause::ConstEq(_) => builder.push_fact(bound),`
`76`	`76`	`WhereClause::LifetimeOutlives(..) => {}`
`77`	`77`	`WhereClause::TypeOutlives(..) => {}`
`78`	`78`	`});`
Original file line number	Diff line number	Diff line change
`@@ -206,7 +206,7 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {`
`206`	`206`	`)`
`207`	`207`	`}`
`208`	`208`	`// FIXME: Associated item bindings are just taken as facts (?)`
`209`		`- WhereClause::AliasEq(_) => builder.push_fact(bound),`
	`209`	`+ WhereClause::AliasEq(_) \| WhereClause::ConstEq(_) => builder.push_fact(bound),`
`210`	`210`	`WhereClause::LifetimeOutlives(..) => {}`
`211`	`211`	`WhereClause::TypeOutlives(..) => {}`
`212`	`212`	`});`
Original file line number	Diff line number	Diff line change
`@@ -93,9 +93,10 @@ pub fn super_traits<I: Interner>(`
`93`	`93`	`}`
`94`	`94`	`Some(tr.clone())`
`95`	`95`	`}`
`96`		`- WhereClause::AliasEq(_) => None,`
`97`		`- WhereClause::LifetimeOutlives(..) => None,`
`98`		`- WhereClause::TypeOutlives(..) => None,`
	`96`	`+ WhereClause::AliasEq(_)`
	`97`	`+ \| WhereClause::LifetimeOutlives(..)`
	`98`	`+ \| WhereClause::ConstEq(_)`
	`99`	`+ \| WhereClause::TypeOutlives(..) => None,`
`99`	`100`	`})`
`100`	`101`	`})`
`101`	`102`	`.collect::<Vec<_>>()`
Original file line number	Diff line number	Diff line change
`@@ -165,6 +165,7 @@ fn display_self_where_clauses_as_bounds<'a, I: Interner>(`
`165`	`165`	`}`
`166`	`166`	`AliasTy::Opaque(opaque) => opaque.display(s).fmt(f),`
`167`	`167`	`},`
	`168`	`+ WhereClause::ConstEq(_) => todo!(),`
`168`	`169`	`WhereClause::LifetimeOutlives(lifetime) => lifetime.display(s).fmt(f),`
`169`	`170`	`WhereClause::TypeOutlives(ty) => ty.display(s).fmt(f),`
`170`	`171`	`}`
Original file line number	Diff line number	Diff line change
`@@ -91,6 +91,7 @@ impl<I: Interner> RenderAsRust<I> for WhereClause<I> {`
`91`	`91`	`match self {`
`92`	`92`	`WhereClause::Implemented(trait_ref) => trait_ref.fmt(s, f),`
`93`	`93`	`WhereClause::AliasEq(alias_eq) => alias_eq.fmt(s, f),`
	`94`	`+ WhereClause::ConstEq(const_eq) => const_eq.fmt(s, f),`
`94`	`95`	`WhereClause::LifetimeOutlives(lifetime) => lifetime.display(s).fmt(f),`
`95`	`96`	`WhereClause::TypeOutlives(ty) => ty.display(s).fmt(f),`
`96`	`97`	`}`
`@@ -153,6 +154,12 @@ impl<I: Interner> RenderAsRust<I> for AliasEq<I> {`
`153`	`154`	`}`
`154`	`155`	`}`
`155`	`156`
	`157`	`+impl<I: Interner> RenderAsRust<I> for ConstEq<I> {`
	`158`	`+ fn fmt(&self, s: &InternalWriterState<'_, I>, f: &'_ mut Formatter<'_>) -> Result {`
	`159`	`+ todo!()`
	`160`	`+ }`
	`161`	`+}`
	`162`	`+`
`156`	`163`	`impl<I: Interner> RenderAsRust<I> for LifetimeOutlives<I> {`
`157`	`164`	`fn fmt(&self, s: &InternalWriterState<'_, I>, f: &mut Formatter<'_>) -> Result {`
`158`	`165`	`// a': 'b`