Skip to content

Commit 6d8d542

Browse files
committed
refactored binders to have a private value field
1 parent 2c72044 commit 6d8d542

File tree

10 files changed

+94
-66
lines changed

10 files changed

+94
-66
lines changed

chalk-integration/src/lowering.rs

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -169,10 +169,7 @@ impl<'k> Env<'k> {
169169
{
170170
let binders: Vec<_> = binders.into_iter().collect();
171171
let env = self.introduce(binders.iter().cloned())?;
172-
Ok(chalk_ir::Binders {
173-
binders: binders.anonymize(),
174-
value: op(&env)?,
175-
})
172+
Ok(chalk_ir::Binders::new(binders.anonymize(), op(&env)?))
176173
}
177174
}
178175

@@ -528,10 +525,7 @@ impl LowerTypeKind for StructDefn {
528525
Ok(TypeKind {
529526
sort: TypeSort::Struct,
530527
name: self.name.str,
531-
binders: chalk_ir::Binders {
532-
binders: self.all_parameters().anonymize(),
533-
value: (),
534-
},
528+
binders: chalk_ir::Binders::new(self.all_parameters().anonymize(), ()),
535529
})
536530
}
537531
}
@@ -548,11 +542,11 @@ impl LowerTypeKind for TraitDefn {
548542
Ok(TypeKind {
549543
sort: TypeSort::Trait,
550544
name: self.name.str,
551-
binders: chalk_ir::Binders {
545+
binders: chalk_ir::Binders::new(
552546
// for the purposes of the *type*, ignore `Self`:
553-
binders: binders.anonymize(),
554-
value: (),
555-
},
547+
binders.anonymize(),
548+
(),
549+
),
556550
})
557551
}
558552
}

chalk-integration/src/program.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -275,7 +275,7 @@ impl RustIrDatabase<ChalkIr> for Program {
275275
self.impl_data
276276
.iter()
277277
.filter(|(_, impl_datum)| {
278-
let trait_ref = &impl_datum.binders.value.trait_ref;
278+
let trait_ref = &impl_datum.binders.skip_binders().trait_ref;
279279
trait_id == trait_ref.trait_id && {
280280
assert_eq!(trait_ref.substitution.len(interner), parameters.len());
281281
<[_] as CouldMatch<[_]>>::could_match(
@@ -308,7 +308,7 @@ impl RustIrDatabase<ChalkIr> for Program {
308308
// Look for an impl like `impl Send for Foo` where `Foo` is
309309
// the struct. See `push_auto_trait_impls` for more.
310310
self.impl_data.values().any(|impl_datum| {
311-
let impl_trait_ref = &impl_datum.binders.value.trait_ref;
311+
let impl_trait_ref = &impl_datum.binders.skip_binders().trait_ref;
312312
impl_trait_ref.trait_id == auto_trait_id
313313
&& match impl_trait_ref.self_type_parameter(interner).data(interner) {
314314
TyData::Apply(apply) => match apply.name {

chalk-ir/src/lib.rs

Lines changed: 58 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1144,14 +1144,43 @@ impl<I: Interner> HasInterner for AliasEq<I> {
11441144
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
11451145
pub struct Binders<T> {
11461146
pub binders: Vec<ParameterKind<()>>,
1147-
pub value: T,
1147+
value: T,
11481148
}
11491149

11501150
impl<T: HasInterner> HasInterner for Binders<T> {
11511151
type Interner = T::Interner;
11521152
}
11531153

11541154
impl<T> Binders<T> {
1155+
pub fn new(binders: Vec<ParameterKind<()>>, value: T) -> Self {
1156+
Self { binders, value }
1157+
}
1158+
1159+
/// Skips the binder and returns the "bound" value. This is a
1160+
/// risky thing to do because it's easy to get confused about
1161+
/// De Bruijn indices and the like. It is usually better to
1162+
/// discharge the binder using `no_bound_vars` or something
1163+
/// like that. `skip_binder` is only valid when you are either
1164+
/// extracting data that has nothing to do with bound vars, you
1165+
/// are doing some sort of test that does not involve bound
1166+
/// regions, or you are being very careful about your depth
1167+
/// accounting.
1168+
///
1169+
/// Some examples where `skip_binder` is reasonable:
1170+
///
1171+
/// - extracting the `TraitId` from a TraitRef;
1172+
/// - checking if there are any fields in a StructDatum
1173+
pub fn skip_binders(&self) -> &T {
1174+
&self.value
1175+
}
1176+
1177+
pub fn as_ref(&self) -> Binders<&T> {
1178+
Binders {
1179+
binders: self.binders.clone(),
1180+
value: &self.value,
1181+
}
1182+
}
1183+
11551184
pub fn map<U, OP>(self, op: OP) -> Binders<U>
11561185
where
11571186
OP: FnOnce(T) -> U,
@@ -1167,11 +1196,7 @@ impl<T> Binders<T> {
11671196
where
11681197
OP: FnOnce(&'a T) -> U,
11691198
{
1170-
let value = op(&self.value);
1171-
Binders {
1172-
binders: self.binders.clone(),
1173-
value,
1174-
}
1199+
self.as_ref().map(op)
11751200
}
11761201

11771202
/// Creates a fresh binders that contains a single type
@@ -1194,11 +1219,38 @@ impl<T> Binders<T> {
11941219
}
11951220
}
11961221

1222+
/// Unwraps and returns the value within, but only if it contains
1223+
/// no vars bound by this binder. (In other words, if this binder --
1224+
/// and indeed any enclosing binder -- doesn't bind anything at
1225+
/// all.) Otherwise, returns `None`.
1226+
///
1227+
/// (One could imagine having a method that just unwraps a single
1228+
/// binder, but permits late-bound vars bound by enclosing
1229+
/// binders, but that would require adjusting the debruijn
1230+
/// indices, and given the shallow binding structure we often use,
1231+
/// would not be that useful.)
1232+
pub fn no_bound_vars<I: Interner>(&self, interner: &I) -> Option<&T>
1233+
where
1234+
T: Visit<I>,
1235+
{
1236+
if self.skip_binders().has_free_vars(interner) {
1237+
None
1238+
} else {
1239+
Some(self.skip_binders())
1240+
}
1241+
}
1242+
11971243
pub fn len(&self) -> usize {
11981244
self.binders.len()
11991245
}
12001246
}
12011247

1248+
impl<T> From<Binders<T>> for (Vec<ParameterKind<()>>, T) {
1249+
fn from(binders: Binders<T>) -> Self {
1250+
(binders.binders, binders.value)
1251+
}
1252+
}
1253+
12021254
impl<T, I> Binders<T>
12031255
where
12041256
T: Fold<I, I> + HasInterner<Interner = I>,

chalk-rust-ir/src/lib.rs

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ impl<I: Interner> ImplDatum<I> {
3636
}
3737

3838
pub fn trait_id(&self) -> TraitId<I> {
39-
self.binders.value.trait_ref.trait_id
39+
self.binders.skip_binders().trait_ref.trait_id
4040
}
4141
}
4242

@@ -234,13 +234,8 @@ impl<I: Interner> IntoWhereClauses<I> for QuantifiedInlineBound<I> {
234234

235235
fn into_where_clauses(&self, interner: &I, self_ty: Ty<I>) -> Vec<QuantifiedWhereClause<I>> {
236236
let self_ty = self_ty.shifted_in(interner);
237-
self.value
238-
.into_where_clauses(interner, self_ty)
237+
self.map_ref(|b| b.into_where_clauses(interner, self_ty))
239238
.into_iter()
240-
.map(|wc| Binders {
241-
binders: self.binders.clone(),
242-
value: wc,
243-
})
244239
.collect()
245240
}
246241
}
@@ -413,8 +408,7 @@ impl<I: Interner> AssociatedTyDatum<I> {
413408
/// these quantified where clauses are in the scope of the
414409
/// `binders` field.
415410
pub fn bounds_on_self(&self, interner: &I) -> Vec<QuantifiedWhereClause<I>> {
416-
let Binders { binders, value } = &self.binders;
417-
411+
let (binders, assoc_ty_datum) = self.binders.as_ref().into();
418412
// Create a list `P0...Pn` of references to the binders in
419413
// scope for this associated type:
420414
let substitution = Substitution::from(
@@ -435,7 +429,7 @@ impl<I: Interner> AssociatedTyDatum<I> {
435429
// ```
436430
// <P0 as Foo<P1..Pn>>::Item<Pn..Pm>: Debug
437431
// ```
438-
value
432+
assoc_ty_datum
439433
.bounds
440434
.iter()
441435
.flat_map(|b| b.into_where_clauses(interner, self_ty.clone()))

chalk-solve/src/clauses/builder.rs

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -55,11 +55,8 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
5555
.push(ProgramClauseData::Implies(clause).intern(interner));
5656
} else {
5757
self.clauses.push(
58-
ProgramClauseData::ForAll(Binders {
59-
binders: self.binders.clone(),
60-
value: clause,
61-
})
62-
.intern(interner),
58+
ProgramClauseData::ForAll(Binders::new(self.binders.clone(), clause))
59+
.intern(interner),
6360
);
6461
}
6562

@@ -121,10 +118,7 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
121118
#[allow(dead_code)]
122119
pub fn push_bound_ty(&mut self, op: impl FnOnce(&mut Self, Ty<I>)) {
123120
let interner = self.interner();
124-
let binders = Binders {
125-
binders: vec![ParameterKind::Ty(())],
126-
value: PhantomData::<I>,
127-
};
121+
let binders = Binders::new(vec![ParameterKind::Ty(())], PhantomData::<I>);
128122
self.push_binders(&binders, |this, PhantomData| {
129123
let ty = this
130124
.placeholders_in_scope()

chalk-solve/src/clauses/builtin_traits/sized.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ pub fn add_sized_program_clauses<I: Interner>(
2525
let struct_datum = db.struct_datum(struct_id);
2626

2727
// Structs with no fields are always Sized
28-
if struct_datum.binders.map_ref(|b| b.fields.is_empty()).value {
28+
if struct_datum.binders.skip_binders().fields.is_empty() {
2929
builder.push_fact(trait_ref.clone());
3030
return;
3131
}

chalk-solve/src/coherence/solve.rs

Lines changed: 15 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -85,9 +85,12 @@ impl<I: Interner> CoherenceSolver<'_, I> {
8585

8686
let interner = self.db.interner();
8787

88+
let (lhs_binders, lhs_bound) = lhs.binders.as_ref().into();
89+
let (rhs_binders, rhs_bound) = rhs.binders.as_ref().into();
90+
8891
// Upshift the rhs variables in params to account for the joined binders
89-
let lhs_params = params(interner, lhs).iter().cloned();
90-
let rhs_params = params(interner, rhs)
92+
let lhs_params = params(interner, lhs_bound).iter().cloned();
93+
let rhs_params = params(interner, rhs_bound)
9194
.iter()
9295
.map(|param| param.shifted_in(interner));
9396

@@ -98,10 +101,8 @@ impl<I: Interner> CoherenceSolver<'_, I> {
98101
.map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner));
99102

100103
// Upshift the rhs variables in where clauses
101-
let lhs_where_clauses = lhs.binders.value.where_clauses.iter().cloned();
102-
let rhs_where_clauses = rhs
103-
.binders
104-
.value
104+
let lhs_where_clauses = lhs_bound.where_clauses.iter().cloned();
105+
let rhs_where_clauses = rhs_bound
105106
.where_clauses
106107
.iter()
107108
.map(|wc| wc.shifted_in(interner));
@@ -114,16 +115,8 @@ impl<I: Interner> CoherenceSolver<'_, I> {
114115
// Join all the goals we've created together with And, then quantify them
115116
// over the joined binders. This is our query.
116117
let goal = Box::new(Goal::all(interner, params_goals.chain(wc_goals)))
117-
.quantify(
118-
interner,
119-
QuantifierKind::Exists,
120-
lhs.binders.binders.clone(),
121-
)
122-
.quantify(
123-
interner,
124-
QuantifierKind::Exists,
125-
rhs.binders.binders.clone(),
126-
)
118+
.quantify(interner, QuantifierKind::Exists, lhs_binders)
119+
.quantify(interner, QuantifierKind::Exists, rhs_binders)
127120
.compatible(interner)
128121
.negate(interner);
129122

@@ -268,11 +261,10 @@ impl<I: Interner> CoherenceSolver<'_, I> {
268261
}
269262
}
270263

271-
fn params<'a, I: Interner>(interner: &I, impl_datum: &'a ImplDatum<I>) -> &'a [Parameter<I>] {
272-
impl_datum
273-
.binders
274-
.value
275-
.trait_ref
276-
.substitution
277-
.parameters(interner)
264+
fn params<'a, I: Interner>(
265+
interner: &I,
266+
impl_datum_bound: &'a ImplDatumBound<I>,
267+
) -> &'a [Parameter<I>] {
268+
// We can skip binders here because the caller is handling correct binders handling
269+
impl_datum_bound.trait_ref.substitution.parameters(interner)
278270
}

chalk-solve/src/coinductive_goal.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,9 @@ impl<I: Interner> IsCoinductive<I> for Goal<I> {
2626
WhereClause::AliasEq(..) => false,
2727
},
2828
GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
29-
GoalData::Quantified(QuantifierKind::ForAll, goal) => goal.value.is_coinductive(db),
29+
GoalData::Quantified(QuantifierKind::ForAll, goal) => {
30+
goal.skip_binders().is_coinductive(db)
31+
}
3032
_ => false,
3133
}
3234
}

chalk-solve/src/infer/instantiate.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ impl<'a, T> IntoBindersAndValue for &'a Binders<T> {
114114
type Value = &'a T;
115115

116116
fn into_binders_and_value(self) -> (Self::Binders, Self::Value) {
117-
(self.binders.iter().cloned(), &self.value)
117+
(self.binders.iter().cloned(), self.skip_binders())
118118
}
119119
}
120120

chalk-solve/src/solve/slg/resolvent.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -485,7 +485,7 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
485485
T: Zip<I> + Fold<I, Result = T>,
486486
{
487487
self.outer_binder.shift_in();
488-
Zip::zip_with(self, &answer.value, &pending.value)?;
488+
Zip::zip_with(self, &answer.skip_binders(), &pending.skip_binders())?;
489489
self.outer_binder.shift_out();
490490
Ok(())
491491
}

0 commit comments

Comments
 (0)