Skip to content

Commit ad5573b

Browse files
authored
Merge pull request #384 from Areredify/binders_refactor
refactored binders to have a private value field
2 parents 0a43a81 + dfe713a commit ad5573b

File tree

10 files changed

+75
-68
lines changed

10 files changed

+75
-68
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: 37 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. `skip_binder` is only valid
1162+
/// when you are either extracting data that has nothing to
1163+
/// do with bound vars, or you are being very careful about
1164+
/// your depth accounting.
1165+
///
1166+
/// Some examples where `skip_binder` is reasonable:
1167+
///
1168+
/// - extracting the `TraitId` from a TraitRef;
1169+
/// - checking if there are any fields in a StructDatum
1170+
pub fn skip_binders(&self) -> &T {
1171+
&self.value
1172+
}
1173+
1174+
/// Converts `&Binders<T>` to `Binders<&T>`. Produces new `Binders`
1175+
/// with cloned quantifiers containing a reference to the original
1176+
/// value, leaving the original in place.
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
@@ -1199,6 +1224,12 @@ impl<T> Binders<T> {
11991224
}
12001225
}
12011226

1227+
impl<T> From<Binders<T>> for (Vec<ParameterKind<()>>, T) {
1228+
fn from(binders: Binders<T>) -> Self {
1229+
(binders.binders, binders.value)
1230+
}
1231+
}
1232+
12021233
impl<T, I> Binders<T>
12031234
where
12041235
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: 17 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -85,9 +85,20 @@ 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 = lhs_bound
93+
.trait_ref
94+
.substitution
95+
.parameters(interner)
96+
.iter()
97+
.cloned();
98+
let rhs_params = rhs_bound
99+
.trait_ref
100+
.substitution
101+
.parameters(interner)
91102
.iter()
92103
.map(|param| param.shifted_in(interner));
93104

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

100111
// 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
112+
let lhs_where_clauses = lhs_bound.where_clauses.iter().cloned();
113+
let rhs_where_clauses = rhs_bound
105114
.where_clauses
106115
.iter()
107116
.map(|wc| wc.shifted_in(interner));
@@ -114,16 +123,8 @@ impl<I: Interner> CoherenceSolver<'_, I> {
114123
// Join all the goals we've created together with And, then quantify them
115124
// over the joined binders. This is our query.
116125
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-
)
126+
.quantify(interner, QuantifierKind::Exists, lhs_binders)
127+
.quantify(interner, QuantifierKind::Exists, rhs_binders)
127128
.compatible(interner)
128129
.negate(interner);
129130

@@ -267,12 +268,3 @@ impl<I: Interner> CoherenceSolver<'_, I> {
267268
result
268269
}
269270
}
270-
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)
278-
}

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)