Add ConstEq to many match cases

Where trivial, add ConstEq, otherwise defer to todos

Author: JulianKnodt

chalk-integration/src/db.rs

@@ -14,6 +14,7 @@ use chalk_ir::{
 };
 use chalk_solve::rust_ir::{
     AdtDatum, AdtRepr, AdtSizeAlign, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId,
+    AssociatedConstDatum,
     ClosureKind, FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum,
     ImplDatum, OpaqueTyDatum, TraitDatum, WellKnownTrait,
 };
@@ -91,6 +92,13 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
         self.program_ir().unwrap().associated_ty_data(ty)
     }
 
+    fn associated_const_data(
+        &self,
+        ct: AssocItemId<ChalkIr>,
+    ) -> Arc<AssociatedConstDatum<ChalkIr>> {
+        self.program_ir().unwrap().associated_const_data(ct)
+    }
+
     fn trait_datum(&self, id: TraitId<ChalkIr>) -> Arc<TraitDatum<ChalkIr>> {
         self.program_ir().unwrap().trait_datum(id)
     }

chalk-integration/src/lowering.rs

@@ -173,7 +173,8 @@ impl LowerWithEnv for WhereClause {
             ],
             WhereClause::ConstProjectionEq { projection, val } => {
                 vec![chalk_ir::WhereClause::ConstEq(chalk_ir::ConstEq {
-                    term: chalk_ir::AliasTy::Projection(projection.lower(env)?),
+                    // TODO maybe this should just be a projection term instead
+                    term: projection.lower(env)?.associated_term_id,
                     ct: val.lower(env)?,
                 })]
             }

chalk-integration/src/lowering/program_lowerer.rs

@@ -158,6 +158,7 @@ impl ProgramLowerer {
         let mut well_known_traits = BTreeMap::new();
         let mut impl_data = BTreeMap::new();
         let mut associated_const_values = BTreeMap::new();
+        let mut associated_const_data = BTreeMap::new();
         let mut associated_ty_data = BTreeMap::new();
         let mut associated_ty_values = BTreeMap::new();
         let mut opaque_ty_data = BTreeMap::new();
@@ -317,6 +318,9 @@ impl ProgramLowerer {
                             }),
                         );
                     }
+                    for assoc_ct_defn in &trait_defn.assoc_const_defns {
+                        todo!();
+                    }
                 }
                 Item::Impl(ref impl_defn) => {
                     let impl_id = ImplId(raw_id);
@@ -522,6 +526,7 @@ impl ProgramLowerer {
             well_known_traits,
             impl_data,
             associated_const_values,
+            associated_const_data,
             associated_ty_values,
             associated_ty_data,
             opaque_ty_ids: self.opaque_ty_ids,

chalk-integration/src/program.rs

@@ -10,6 +10,7 @@ use chalk_ir::{
 };
 use chalk_solve::rust_ir::{
     AdtDatum, AdtRepr, AdtSizeAlign, AssociatedConstValue, AssociatedConstValueId,
+    AssociatedConstDatum,
     AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ClosureKind, FnDefDatum,
     FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum, ImplDatum, ImplType,
     OpaqueTyDatum, TraitDatum, WellKnownTrait,
@@ -104,6 +105,9 @@ pub struct Program {
     /// For each associated ty declaration `type Foo` found in a trait:
     pub associated_ty_data: BTreeMap<AssocItemId<ChalkIr>, Arc<AssociatedTyDatum<ChalkIr>>>,
 
+    /// For each associated const declaration `const Foo` found in a trait:
+    pub associated_const_data: BTreeMap<AssocItemId<ChalkIr>, Arc<AssociatedConstDatum<ChalkIr>>>,
+
     /// For each user-specified clause
     pub custom_clauses: Vec<ProgramClause<ChalkIr>>,
 
@@ -395,6 +399,10 @@ impl RustIrDatabase<ChalkIr> for Program {
         self.associated_ty_data[&ty].clone()
     }
 
+    fn associated_const_data(&self, ct: AssocItemId<ChalkIr>) -> Arc<AssociatedConstDatum<ChalkIr>> {
+        self.associated_const_data[&ct].clone()
+    }
+
     fn trait_datum(&self, id: TraitId<ChalkIr>) -> Arc<TraitDatum<ChalkIr>> {
         self.trait_data[&id].clone()
     }

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![],
                         }

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(..) => {}
             });

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(..) => {}
                 });

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<_>>()

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) => {

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),
                         }