Skip to content

Commit 912074c

Browse files
committed
track outermost binder instead of number of binders
This is more strongly typed. In the process, rename `shifted_in_by/shifted_out_by` to * `shifted_in_from(D)` -- i.e., we are shifting a value from the binder D into this one * `shifted_out_to(D)` -- i.e., we are shifting a value from this binder into the binder D I at least find those names give me a better intuition for what's going on in most cases. i.e., we are taking a term that was valid from some outer binder D and shifting it *in* to the inner binder.
1 parent 37219f7 commit 912074c

File tree

19 files changed

+361
-299
lines changed

19 files changed

+361
-299
lines changed

chalk-derive/src/lib.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
3333
fn fold_with<'i>(
3434
&self,
3535
folder: &mut dyn Folder < 'i, #arg, #arg >,
36-
binders: usize,
36+
outer_binder: DebruijnIndex,
3737
) -> ::chalk_engine::fallible::Fallible<Self::Result> {
3838
#body
3939
}
@@ -97,7 +97,7 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
9797
fn fold_with<'i>(
9898
&self,
9999
folder: &mut dyn Folder < 'i, _I, _TI >,
100-
binders: usize,
100+
outer_binder: DebruijnIndex,
101101
) -> ::chalk_engine::fallible::Fallible<Self::Result>
102102
where
103103
_I: 'i,
@@ -136,7 +136,7 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
136136
fn fold_with<'i>(
137137
&self,
138138
folder: &mut dyn Folder < 'i, #i, _TI >,
139-
binders: usize,
139+
outer_binder: DebruijnIndex,
140140
) -> ::chalk_engine::fallible::Fallible<Self::Result>
141141
where
142142
#i: 'i,
@@ -157,7 +157,7 @@ fn derive_fold_body(type_name: &Ident, data: Data) -> proc_macro2::TokenStream {
157157
Data::Struct(s) => {
158158
let fields = s.fields.into_iter().map(|f| {
159159
let name = f.ident.as_ref().expect("Unnamed field in Foldable struct");
160-
quote! { #name: self.#name.fold_with(folder, binders)? }
160+
quote! { #name: self.#name.fold_with(folder, outer_binder)? }
161161
});
162162
quote! {
163163
Ok(#type_name {
@@ -187,7 +187,7 @@ fn derive_fold_body(type_name: &Ident, data: Data) -> proc_macro2::TokenStream {
187187
.collect();
188188
quote! {
189189
#type_name::#variant( #(ref #names),* ) => {
190-
Ok(#type_name::#variant( #(#names.fold_with(folder, binders)?),* ))
190+
Ok(#type_name::#variant( #(#names.fold_with(folder, outer_binder)?),* ))
191191
}
192192
}
193193
}

chalk-ir/src/debug.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,7 @@ impl<I: Interner> Debug for TyData<I> {
135135
}
136136

137137
impl Debug for BoundVar {
138-
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
138+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
139139
let BoundVar { debruijn, index } = self;
140140
write!(fmt, "{:?}.{:?}", debruijn, index)
141141
}

chalk-ir/src/fold.rs

Lines changed: 66 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -80,30 +80,34 @@ where
8080
/// encountered when folding. By default, invokes
8181
/// `super_fold_with`, which will in turn invoke the more
8282
/// specialized folding methods below, like `fold_free_var_ty`.
83-
fn fold_ty(&mut self, ty: &Ty<I>, binders: usize) -> Fallible<Ty<TI>> {
84-
ty.super_fold_with(self.as_dyn(), binders)
83+
fn fold_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> Fallible<Ty<TI>> {
84+
ty.super_fold_with(self.as_dyn(), outer_binder)
8585
}
8686

8787
/// Top-level callback: invoked for each `Lifetime<I>` that is
8888
/// encountered when folding. By default, invokes
8989
/// `super_fold_with`, which will in turn invoke the more
9090
/// specialized folding methods below, like `fold_free_lifetime_ty`.
91-
fn fold_lifetime(&mut self, lifetime: &Lifetime<I>, binders: usize) -> Fallible<Lifetime<TI>> {
92-
lifetime.super_fold_with(self.as_dyn(), binders)
91+
fn fold_lifetime(
92+
&mut self,
93+
lifetime: &Lifetime<I>,
94+
outer_binder: DebruijnIndex,
95+
) -> Fallible<Lifetime<TI>> {
96+
lifetime.super_fold_with(self.as_dyn(), outer_binder)
9397
}
9498

9599
/// Invoked for every program clause. By default, recursively folds the goals contents.
96100
fn fold_program_clause(
97101
&mut self,
98102
clause: &ProgramClause<I>,
99-
binders: usize,
103+
outer_binder: DebruijnIndex,
100104
) -> Fallible<ProgramClause<TI>> {
101-
clause.super_fold_with(self.as_dyn(), binders)
105+
clause.super_fold_with(self.as_dyn(), outer_binder)
102106
}
103107

104108
/// Invoked for every goal. By default, recursively folds the goals contents.
105-
fn fold_goal(&mut self, goal: &Goal<I>, binders: usize) -> Fallible<Goal<TI>> {
106-
goal.super_fold_with(self.as_dyn(), binders)
109+
fn fold_goal(&mut self, goal: &Goal<I>, outer_binder: DebruijnIndex) -> Fallible<Goal<TI>> {
110+
goal.super_fold_with(self.as_dyn(), outer_binder)
107111
}
108112

109113
/// If overridden to return true, then folding will panic if a
@@ -122,14 +126,18 @@ where
122126
///
123127
/// This should return a type suitable for a context with
124128
/// `binders` in scope.
125-
fn fold_free_var_ty(&mut self, bound_var: BoundVar, binders: usize) -> Fallible<Ty<TI>> {
129+
fn fold_free_var_ty(
130+
&mut self,
131+
bound_var: BoundVar,
132+
outer_binder: DebruijnIndex,
133+
) -> Fallible<Ty<TI>> {
126134
if self.forbid_free_vars() {
127135
panic!(
128-
"unexpected free variable with depth `{:?}` in {} binders",
129-
bound_var, binders
136+
"unexpected free variable with depth `{:?}` with outer binder {:?}",
137+
bound_var, outer_binder
130138
)
131139
} else {
132-
let bound_var = bound_var.shifted_in_by(binders);
140+
let bound_var = bound_var.shifted_in_from(outer_binder);
133141
Ok(TyData::<TI>::BoundVar(bound_var).intern(self.target_interner()))
134142
}
135143
}
@@ -138,15 +146,15 @@ where
138146
fn fold_free_var_lifetime(
139147
&mut self,
140148
bound_var: BoundVar,
141-
binders: usize,
149+
outer_binder: DebruijnIndex,
142150
) -> Fallible<Lifetime<TI>> {
143151
if self.forbid_free_vars() {
144152
panic!(
145-
"unexpected free variable with depth `{:?}` in {} binders",
146-
bound_var, binders
153+
"unexpected free variable with depth `{:?}` with outer binder {:?}",
154+
bound_var, outer_binder
147155
)
148156
} else {
149-
let bound_var = bound_var.shifted_in_by(binders);
157+
let bound_var = bound_var.shifted_in_from(outer_binder);
150158
Ok(LifetimeData::<TI>::BoundVar(bound_var).intern(self.target_interner()))
151159
}
152160
}
@@ -164,10 +172,11 @@ where
164172
///
165173
/// - `universe` is the universe of the `TypeName::ForAll` that was found
166174
/// - `binders` is the number of binders in scope
175+
#[allow(unused_variables)]
167176
fn fold_free_placeholder_ty(
168177
&mut self,
169178
universe: PlaceholderIndex,
170-
_binders: usize,
179+
outer_binder: DebruijnIndex,
171180
) -> Fallible<Ty<TI>> {
172181
if self.forbid_free_placeholders() {
173182
panic!("unexpected placeholder type `{:?}`", universe)
@@ -177,10 +186,11 @@ where
177186
}
178187

179188
/// As with `fold_free_placeholder_ty`, but for lifetimes.
189+
#[allow(unused_variables)]
180190
fn fold_free_placeholder_lifetime(
181191
&mut self,
182192
universe: PlaceholderIndex,
183-
_binders: usize,
193+
outer_binder: DebruijnIndex,
184194
) -> Fallible<Lifetime<TI>> {
185195
if self.forbid_free_placeholders() {
186196
panic!("unexpected placeholder lifetime `{:?}`", universe)
@@ -203,7 +213,12 @@ where
203213
///
204214
/// - `universe` is the universe of the `TypeName::ForAll` that was found
205215
/// - `binders` is the number of binders in scope
206-
fn fold_inference_ty(&mut self, var: InferenceVar, _binders: usize) -> Fallible<Ty<TI>> {
216+
#[allow(unused_variables)]
217+
fn fold_inference_ty(
218+
&mut self,
219+
var: InferenceVar,
220+
outer_binder: DebruijnIndex,
221+
) -> Fallible<Ty<TI>> {
207222
if self.forbid_inference_vars() {
208223
panic!("unexpected inference type `{:?}`", var)
209224
} else {
@@ -212,10 +227,11 @@ where
212227
}
213228

214229
/// As with `fold_free_inference_ty`, but for lifetimes.
230+
#[allow(unused_variables)]
215231
fn fold_inference_lifetime(
216232
&mut self,
217233
var: InferenceVar,
218-
_binders: usize,
234+
outer_binder: DebruijnIndex,
219235
) -> Fallible<Lifetime<TI>> {
220236
if self.forbid_inference_vars() {
221237
panic!("unexpected inference lifetime `'{:?}`", var)
@@ -260,7 +276,7 @@ pub trait Fold<I: Interner, TI: TargetInterner<I> = I>: Debug {
260276
fn fold_with<'i>(
261277
&self,
262278
folder: &mut dyn Folder<'i, I, TI>,
263-
binders: usize,
279+
outer_binder: DebruijnIndex,
264280
) -> Fallible<Self::Result>
265281
where
266282
I: 'i,
@@ -274,7 +290,7 @@ pub trait SuperFold<I: Interner, TI: TargetInterner<I> = I>: Fold<I, TI> {
274290
fn super_fold_with<'i>(
275291
&self,
276292
folder: &mut dyn Folder<'i, I, TI>,
277-
binders: usize,
293+
outer_binder: DebruijnIndex,
278294
) -> Fallible<Self::Result>
279295
where
280296
I: 'i,
@@ -290,13 +306,13 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Ty<I> {
290306
fn fold_with<'i>(
291307
&self,
292308
folder: &mut dyn Folder<'i, I, TI>,
293-
binders: usize,
309+
outer_binder: DebruijnIndex,
294310
) -> Fallible<Self::Result>
295311
where
296312
I: 'i,
297313
TI: 'i,
298314
{
299-
folder.fold_ty(self, binders)
315+
folder.fold_ty(self, outer_binder)
300316
}
301317
}
302318

@@ -309,7 +325,7 @@ where
309325
fn super_fold_with<'i>(
310326
&self,
311327
folder: &mut dyn Folder<'i, I, TI>,
312-
binders: usize,
328+
outer_binder: DebruijnIndex,
313329
) -> Fallible<Ty<TI>>
314330
where
315331
I: 'i,
@@ -318,36 +334,29 @@ where
318334
let interner = folder.interner();
319335
match self.data(interner) {
320336
TyData::BoundVar(bound_var) => {
321-
if let Some(bound_var1) = bound_var.shifted_out_by(binders) {
337+
if let Some(bound_var1) = bound_var.shifted_out_to(outer_binder) {
322338
// This variable was bound outside of the binders
323339
// that we have traversed during folding;
324340
// therefore, it is free. Let the folder have a
325341
// crack at it.
326-
folder.fold_free_var_ty(bound_var1, binders)
342+
folder.fold_free_var_ty(bound_var1, outer_binder)
327343
} else {
328344
// This variable was bound within the binders that
329345
// we folded over, so just return a bound
330346
// variable.
331347
Ok(TyData::<TI>::BoundVar(*bound_var).intern(folder.target_interner()))
332348
}
333349
}
334-
TyData::Dyn(clauses) => {
335-
Ok(TyData::Dyn(clauses.fold_with(folder, binders)?)
336-
.intern(folder.target_interner()))
337-
}
338-
TyData::InferenceVar(var) => folder.fold_inference_ty(*var, binders),
339-
TyData::Apply(apply) => {
340-
Ok(TyData::Apply(apply.fold_with(folder, binders)?)
341-
.intern(folder.target_interner()))
342-
}
343-
TyData::Placeholder(ui) => Ok(folder.fold_free_placeholder_ty(*ui, binders)?),
344-
TyData::Alias(proj) => Ok(
345-
TyData::Alias(proj.fold_with(folder, binders)?).intern(folder.target_interner())
346-
),
347-
TyData::Function(fun) => {
348-
Ok(TyData::Function(fun.fold_with(folder, binders)?)
349-
.intern(folder.target_interner()))
350-
}
350+
TyData::Dyn(clauses) => Ok(TyData::Dyn(clauses.fold_with(folder, outer_binder)?)
351+
.intern(folder.target_interner())),
352+
TyData::InferenceVar(var) => folder.fold_inference_ty(*var, outer_binder),
353+
TyData::Apply(apply) => Ok(TyData::Apply(apply.fold_with(folder, outer_binder)?)
354+
.intern(folder.target_interner())),
355+
TyData::Placeholder(ui) => Ok(folder.fold_free_placeholder_ty(*ui, outer_binder)?),
356+
TyData::Alias(proj) => Ok(TyData::Alias(proj.fold_with(folder, outer_binder)?)
357+
.intern(folder.target_interner())),
358+
TyData::Function(fun) => Ok(TyData::Function(fun.fold_with(folder, outer_binder)?)
359+
.intern(folder.target_interner())),
351360
}
352361
}
353362
}
@@ -361,13 +370,13 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Lifetime<I> {
361370
fn fold_with<'i>(
362371
&self,
363372
folder: &mut dyn Folder<'i, I, TI>,
364-
binders: usize,
373+
outer_binder: DebruijnIndex,
365374
) -> Fallible<Self::Result>
366375
where
367376
I: 'i,
368377
TI: 'i,
369378
{
370-
folder.fold_lifetime(self, binders)
379+
folder.fold_lifetime(self, outer_binder)
371380
}
372381
}
373382

@@ -379,7 +388,7 @@ where
379388
fn super_fold_with<'i>(
380389
&self,
381390
folder: &mut dyn Folder<'i, I, TI>,
382-
binders: usize,
391+
outer_binder: DebruijnIndex,
383392
) -> Fallible<Lifetime<TI>>
384393
where
385394
I: 'i,
@@ -388,22 +397,22 @@ where
388397
let interner = folder.interner();
389398
match self.data(interner) {
390399
LifetimeData::BoundVar(bound_var) => {
391-
if let Some(bound_var1) = bound_var.shifted_out_by(binders) {
400+
if let Some(bound_var1) = bound_var.shifted_out_to(outer_binder) {
392401
// This variable was bound outside of the binders
393402
// that we have traversed during folding;
394403
// therefore, it is free. Let the folder have a
395404
// crack at it.
396-
folder.fold_free_var_lifetime(bound_var1, binders)
405+
folder.fold_free_var_lifetime(bound_var1, outer_binder)
397406
} else {
398407
// This variable was bound within the binders that
399408
// we folded over, so just return a bound
400409
// variable.
401410
Ok(LifetimeData::<TI>::BoundVar(*bound_var).intern(folder.target_interner()))
402411
}
403412
}
404-
LifetimeData::InferenceVar(var) => folder.fold_inference_lifetime(*var, binders),
413+
LifetimeData::InferenceVar(var) => folder.fold_inference_lifetime(*var, outer_binder),
405414
LifetimeData::Placeholder(universe) => {
406-
folder.fold_free_placeholder_lifetime(*universe, binders)
415+
folder.fold_free_placeholder_lifetime(*universe, outer_binder)
407416
}
408417
LifetimeData::Phantom(..) => unreachable!(),
409418
}
@@ -418,13 +427,13 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goal<I> {
418427
fn fold_with<'i>(
419428
&self,
420429
folder: &mut dyn Folder<'i, I, TI>,
421-
binders: usize,
430+
outer_binder: DebruijnIndex,
422431
) -> Fallible<Self::Result>
423432
where
424433
I: 'i,
425434
TI: 'i,
426435
{
427-
folder.fold_goal(self, binders)
436+
folder.fold_goal(self, outer_binder)
428437
}
429438
}
430439

@@ -433,7 +442,7 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for Goal<I> {
433442
fn super_fold_with<'i>(
434443
&self,
435444
folder: &mut dyn Folder<'i, I, TI>,
436-
binders: usize,
445+
outer_binder: DebruijnIndex,
437446
) -> Fallible<Self::Result>
438447
where
439448
I: 'i,
@@ -443,7 +452,7 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for Goal<I> {
443452
let target_interner = folder.target_interner();
444453
Ok(Goal::new(
445454
target_interner,
446-
self.data(interner).fold_with(folder, binders)?,
455+
self.data(interner).fold_with(folder, outer_binder)?,
447456
))
448457
}
449458
}
@@ -457,12 +466,12 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for ProgramClause<I> {
457466
fn fold_with<'i>(
458467
&self,
459468
folder: &mut dyn Folder<'i, I, TI>,
460-
binders: usize,
469+
outer_binder: DebruijnIndex,
461470
) -> Fallible<Self::Result>
462471
where
463472
I: 'i,
464473
TI: 'i,
465474
{
466-
folder.fold_program_clause(self, binders)
475+
folder.fold_program_clause(self, outer_binder)
467476
}
468477
}

0 commit comments

Comments
 (0)