Skip to content

Commit a3f8ea9

Browse files
JulianKnodtJulianKnodt
committed
Add ConstEq to many match cases
Where trivial, add ConstEq, otherwise defer to todos
1 parent 9586104 commit a3f8ea9

14 files changed

+84
-9
lines changed

‎chalk-solve/src/clauses.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -570,6 +570,9 @@ pub fn program_clauses_that_could_match<I: Interner>(
570570
})
571571
});
572572
}
573+
DomainGoal::Holds(WhereClause::ConstEq(const_eq)) => {
574+
todo!()
575+
}
573576
DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
574577
| DomainGoal::LocalImplAllowed(trait_ref) => {
575578
db.trait_datum(trait_ref.trait_id)
@@ -1071,6 +1074,7 @@ fn match_ty<I: Interner>(
10711074
vec![DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()))]
10721075
}
10731076
WhereClause::AliasEq(_)
1077+
| WhereClause::ConstEq(_)
10741078
| WhereClause::LifetimeOutlives(_)
10751079
| WhereClause::TypeOutlives(_) => vec![],
10761080
}

‎chalk-solve/src/clauses/dyn_ty.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ pub(super) fn build_dyn_self_ty_clauses<I: Interner>(
7272
)
7373
}
7474
// 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),
7676
WhereClause::LifetimeOutlives(..) => {}
7777
WhereClause::TypeOutlives(..) => {}
7878
});

‎chalk-solve/src/clauses/program_clauses.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
206206
)
207207
}
208208
// 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),
210210
WhereClause::LifetimeOutlives(..) => {}
211211
WhereClause::TypeOutlives(..) => {}
212212
});

‎chalk-solve/src/clauses/super_traits.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -93,9 +93,10 @@ pub fn super_traits<I: Interner>(
9393
}
9494
Some(tr.clone())
9595
}
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,
99100
})
100101
})
101102
.collect::<Vec<_>>()

‎chalk-solve/src/coinductive_goal.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,10 @@ impl<I: Interner> IsCoinductive<I> for Goal<I> {
2323
db.trait_datum(tr.trait_id).is_auto_trait()
2424
|| db.trait_datum(tr.trait_id).is_coinductive_trait()
2525
}
26-
WhereClause::AliasEq(..) => false,
27-
WhereClause::LifetimeOutlives(..) => false,
28-
WhereClause::TypeOutlives(..) => false,
26+
WhereClause::AliasEq(_)
27+
| WhereClause::LifetimeOutlives(..)
28+
| WhereClause::TypeOutlives(..)
29+
| WhereClause::ConstEq(_) => false,
2930
},
3031
GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
3132
GoalData::Quantified(QuantifierKind::ForAll, goal) => {

‎chalk-solve/src/display.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -165,6 +165,7 @@ fn display_self_where_clauses_as_bounds<'a, I: Interner>(
165165
}
166166
AliasTy::Opaque(opaque) => opaque.display(s).fmt(f),
167167
},
168+
WhereClause::ConstEq(_) => todo!(),
168169
WhereClause::LifetimeOutlives(lifetime) => lifetime.display(s).fmt(f),
169170
WhereClause::TypeOutlives(ty) => ty.display(s).fmt(f),
170171
}

‎chalk-solve/src/display/bounds.rs

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,7 @@ impl<I: Interner> RenderAsRust<I> for WhereClause<I> {
9191
match self {
9292
WhereClause::Implemented(trait_ref) => trait_ref.fmt(s, f),
9393
WhereClause::AliasEq(alias_eq) => alias_eq.fmt(s, f),
94+
WhereClause::ConstEq(const_eq) => const_eq.fmt(s, f),
9495
WhereClause::LifetimeOutlives(lifetime) => lifetime.display(s).fmt(f),
9596
WhereClause::TypeOutlives(ty) => ty.display(s).fmt(f),
9697
}
@@ -153,6 +154,12 @@ impl<I: Interner> RenderAsRust<I> for AliasEq<I> {
153154
}
154155
}
155156

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+
156163
impl<I: Interner> RenderAsRust<I> for LifetimeOutlives<I> {
157164
fn fmt(&self, s: &InternalWriterState<'_, I>, f: &mut Formatter<'_>) -> Result {
158165
// a': 'b

‎chalk-solve/src/display/stub.rs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ impl<I: Interner, DB: RustIrDatabase<I>> RustIrDatabase<I> for StubWrapper<'_, D
4444
fn associated_ty_data(
4545
&self,
4646
ty: chalk_ir::AssocItemId<I>,
47-
) -> std::sync::Arc<crate::rust_ir::AssociatedTyDatum<I>> {
47+
) -> Arc<crate::rust_ir::AssociatedTyDatum<I>> {
4848
let mut v = (*self.db.associated_ty_data(ty)).clone();
4949
v.binders = Binders::new(
5050
v.binders.binders.clone(),
@@ -56,6 +56,13 @@ impl<I: Interner, DB: RustIrDatabase<I>> RustIrDatabase<I> for StubWrapper<'_, D
5656
Arc::new(v)
5757
}
5858

59+
fn associated_const_data(
60+
&self,
61+
ct: chalk_ir::AssocItemId<I>,
62+
) -> Arc<crate::rust_ir::AssociatedConstDatum<I>> {
63+
Arc::new((*self.db.associated_const_data(ct)).clone())
64+
}
65+
5966
fn trait_datum(
6067
&self,
6168
trait_id: chalk_ir::TraitId<I>,

‎chalk-solve/src/infer/unify.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -672,6 +672,9 @@ impl<'t, I: Interner> Unifier<'t, I> {
672672
self.table.new_variable(universe_index).to_ty(interner);
673673
WhereClause::AliasEq(AliasEq { alias, ty })
674674
}
675+
WhereClause::ConstEq(ConstEq { term, ct }) => {
676+
todo!();
677+
}
675678
WhereClause::TypeOutlives(_) => {
676679
let lifetime_var = self.table.new_variable(universe_index);
677680
let lifetime = lifetime_var.to_lifetime(interner);

‎chalk-solve/src/lib.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,9 @@ pub trait RustIrDatabase<I: Interner>: Debug {
4949
/// Returns the datum for the associated type with the given id.
5050
fn associated_ty_data(&self, ty: AssocItemId<I>) -> Arc<AssociatedTyDatum<I>>;
5151

52+
/// Returns the datum for the associated type with the given id.
53+
fn associated_const_data(&self, ty: AssocItemId<I>) -> Arc<AssociatedConstDatum<I>>;
54+
5255
/// Returns the datum for the definition with the given id.
5356
fn trait_datum(&self, trait_id: TraitId<I>) -> Arc<TraitDatum<I>>;
5457

‎chalk-solve/src/logging_db.rs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,15 @@ where
128128
ty_datum
129129
}
130130

131+
fn associated_const_data(
132+
&self,
133+
ct: chalk_ir::AssocItemId<I>,
134+
) -> Arc<crate::rust_ir::AssociatedConstDatum<I>> {
135+
let ct_datum = self.ws.db().associated_const_data(ct);
136+
self.record(ct_datum.trait_id);
137+
ct_datum
138+
}
139+
131140
fn trait_datum(&self, trait_id: TraitId<I>) -> Arc<TraitDatum<I>> {
132141
self.record(trait_id);
133142
self.ws.db().trait_datum(trait_id)
@@ -402,6 +411,13 @@ where
402411
self.db.associated_ty_data(ty)
403412
}
404413

414+
fn associated_const_data(
415+
&self,
416+
ct: chalk_ir::AssocItemId<I>,
417+
) -> Arc<crate::rust_ir::AssociatedConstDatum<I>> {
418+
self.db.associated_const_data(ct)
419+
}
420+
405421
fn trait_datum(&self, trait_id: TraitId<I>) -> Arc<TraitDatum<I>> {
406422
self.db.trait_datum(trait_id)
407423
}

‎chalk-solve/src/logging_db/id_collector.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -154,6 +154,10 @@ impl<'i, I: Interner, DB: RustIrDatabase<I>> Visitor<I> for IdCollector<'i, I, D
154154
match where_clause {
155155
WhereClause::Implemented(trait_ref) => self.record(trait_ref.trait_id),
156156
WhereClause::AliasEq(alias_eq) => self.visit_alias(&alias_eq.alias),
157+
WhereClause::ConstEq(const_eq) => {
158+
self.db.associated_const_data(const_eq.term);
159+
self.visit_const(&const_eq.ct, outer_binder)?;
160+
}
157161
WhereClause::LifetimeOutlives(_lifetime_outlives) => (),
158162
WhereClause::TypeOutlives(_type_outlives) => (),
159163
}

‎chalk-solve/src/rust_ir.rs

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -524,6 +524,30 @@ impl<I: Interner> Visit<I> for AssociatedTyDatum<I> {
524524
}
525525
}
526526

527+
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
528+
pub struct AssociatedConstDatum<I: Interner> {
529+
/// The trait this associated type is defined in.
530+
pub trait_id: TraitId<I>,
531+
532+
/// The ID of this associated type
533+
pub id: AssocItemId<I>,
534+
535+
/// Name of this associated type.
536+
pub name: I::Identifier,
537+
}
538+
539+
// Manual implementation to avoid I::Identifier type.
540+
impl<I: Interner> Visit<I> for AssociatedConstDatum<I> {
541+
fn visit_with<B>(
542+
&self,
543+
visitor: &mut dyn chalk_ir::visit::Visitor<I, BreakTy = B>,
544+
outer_binder: DebruijnIndex,
545+
) -> ControlFlow<B> {
546+
try_break!(self.trait_id.visit_with(visitor, outer_binder));
547+
self.id.visit_with(visitor, outer_binder)
548+
}
549+
}
550+
527551
/// Encodes the parts of `AssociatedTyDatum` where the parameters
528552
/// `P0..Pm` are in scope (`bounds` and `where_clauses`).
529553
#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit, HasInterner)]

‎chalk-solve/src/wf.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,10 @@ impl<I: Interner> Visitor<I> for InputTypeCollector<I> {
9090
.clone()
9191
.intern(self.interner)
9292
.visit_with(self, outer_binder),
93+
WhereClause::ConstEq(const_eq) => {
94+
const_eq.term.visit_with(self, outer_binder)?;
95+
const_eq.ct.visit_with(self, outer_binder)
96+
}
9397
WhereClause::Implemented(trait_ref) => trait_ref.visit_with(self, outer_binder),
9498
WhereClause::TypeOutlives(TypeOutlives { ty, .. }) => ty.visit_with(self, outer_binder),
9599
WhereClause::LifetimeOutlives(..) => ControlFlow::Continue(()),

0 commit comments

Comments
 (0)