Skip to content

Commit 21437de

Browse files
nikomatsakisnikomatsakis
committed
introduce DebruijnIndex new type
1 parent c7bd2bf commit 21437de

File tree

12 files changed

+229
-76
lines changed

12 files changed

+229
-76
lines changed

‎chalk-integration/src/lowering.rs

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
use chalk_ir::cast::{Cast, Caster};
22
use chalk_ir::interner::ChalkIr;
3-
use chalk_ir::{self, AssocTypeId, ImplId, StructId, TraitId};
3+
use chalk_ir::{self, AssocTypeId, DebruijnIndex, ImplId, StructId, TraitId};
44
use chalk_parse::ast::*;
55
use chalk_rust_ir as rust_ir;
66
use chalk_rust_ir::{Anonymize, AssociatedTyValueId, IntoWhereClauses, ToParameter};
@@ -19,7 +19,7 @@ type TraitKinds = BTreeMap<chalk_ir::TraitId<ChalkIr>, TypeKind>;
1919
type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedTyLookup>;
2020
type AssociatedTyValueIds =
2121
BTreeMap<(chalk_ir::ImplId<ChalkIr>, Ident), AssociatedTyValueId<ChalkIr>>;
22-
type ParameterMap = BTreeMap<chalk_ir::ParameterKind<Ident>, usize>;
22+
type ParameterMap = BTreeMap<chalk_ir::ParameterKind<Ident>, DebruijnIndex>;
2323

2424
pub type LowerResult<T> = Result<T, RustIrError>;
2525

@@ -62,11 +62,11 @@ struct AssociatedTyLookup {
6262

6363
enum TypeLookup {
6464
Struct(chalk_ir::StructId<ChalkIr>),
65-
Parameter(usize),
65+
Parameter(DebruijnIndex),
6666
}
6767

6868
enum LifetimeLookup {
69-
Parameter(usize),
69+
Parameter(DebruijnIndex),
7070
}
7171

7272
const SELF: &str = "Self";
@@ -138,12 +138,15 @@ impl<'k> Env<'k> {
138138
I: IntoIterator<Item = chalk_ir::ParameterKind<Ident>>,
139139
I::IntoIter: ExactSizeIterator,
140140
{
141-
let binders = binders.into_iter().enumerate().map(|(i, k)| (k, i));
141+
let binders = binders
142+
.into_iter()
143+
.enumerate()
144+
.map(|(i, k)| (k, DebruijnIndex::from(i)));
142145
let len = binders.len();
143146
let parameter_map: ParameterMap = self
144147
.parameter_map
145148
.iter()
146-
.map(|(&k, &v)| (k, v + len))
149+
.map(|(&k, &v)| (k, v.shifted_in(len)))
147150
.chain(binders)
148151
.collect();
149152
if parameter_map.len() != self.parameter_map.len() + len {
@@ -416,7 +419,10 @@ trait LowerParameterMap {
416419
// trait is not object-safe, and hence not supposed to be used
417420
// as an object. Actually the handling of object types is
418421
// probably just kind of messed up right now. That's ok.
419-
self.all_parameters().into_iter().zip(0..).collect()
422+
self.all_parameters()
423+
.into_iter()
424+
.zip((0..).map(DebruijnIndex::from_u32))
425+
.collect()
420426
}
421427

422428
fn interner(&self) -> &ChalkIr {
@@ -997,7 +1003,8 @@ impl LowerTy for Ty {
9971003
.flat_map(|qil| {
9981004
qil.into_where_clauses(
9991005
interner,
1000-
chalk_ir::TyData::BoundVar(0).intern(interner),
1006+
chalk_ir::TyData::BoundVar(DebruijnIndex::INNERMOST)
1007+
.intern(interner),
10011008
)
10021009
})
10031010
.collect())

‎chalk-ir/src/debug.rs

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -123,7 +123,7 @@ impl<I: Interner> Debug for TypeName<I> {
123123
impl<I: Interner> Debug for TyData<I> {
124124
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
125125
match self {
126-
TyData::BoundVar(depth) => write!(fmt, "^{}", depth),
126+
TyData::BoundVar(db) => write!(fmt, "{:?}", db),
127127
TyData::Dyn(clauses) => write!(fmt, "{:?}", clauses),
128128
TyData::InferenceVar(var) => write!(fmt, "{:?}", var),
129129
TyData::Apply(apply) => write!(fmt, "{:?}", apply),
@@ -134,6 +134,13 @@ impl<I: Interner> Debug for TyData<I> {
134134
}
135135
}
136136

137+
impl Debug for DebruijnIndex {
138+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
139+
let DebruijnIndex { depth } = self;
140+
write!(fmt, "^{}", depth)
141+
}
142+
}
143+
137144
impl<I: Interner> Debug for DynTy<I> {
138145
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
139146
let DynTy { bounds } = self;
@@ -161,7 +168,7 @@ impl<I: Interner> Debug for Fn<I> {
161168
impl<I: Interner> Debug for LifetimeData<I> {
162169
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
163170
match self {
164-
LifetimeData::BoundVar(depth) => write!(fmt, "'^{}", depth),
171+
LifetimeData::BoundVar(db) => write!(fmt, "'{:?}", db),
165172
LifetimeData::InferenceVar(var) => write!(fmt, "'{:?}", var),
166173
LifetimeData::Placeholder(index) => write!(fmt, "'{:?}", index),
167174
LifetimeData::Phantom(..) => unreachable!(),

‎chalk-ir/src/fold.rs

Lines changed: 26 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,8 @@ where
126126
if self.forbid_free_vars() {
127127
panic!("unexpected free variable with depth `{:?}`", depth)
128128
} else {
129-
Ok(TyData::<TI>::BoundVar(depth + binders).intern(self.target_interner()))
129+
let debruijn = DebruijnIndex::from(depth).shifted_in(binders);
130+
Ok(TyData::<TI>::BoundVar(debruijn).intern(self.target_interner()))
130131
}
131132
}
132133

@@ -135,7 +136,8 @@ where
135136
if self.forbid_free_vars() {
136137
panic!("unexpected free variable with depth `{:?}`", depth)
137138
} else {
138-
Ok(LifetimeData::<TI>::BoundVar(depth + binders).intern(self.target_interner()))
139+
let debruijn = DebruijnIndex::from(depth).shifted_in(binders);
140+
Ok(LifetimeData::<TI>::BoundVar(debruijn).intern(self.target_interner()))
139141
}
140142
}
141143

@@ -304,11 +306,18 @@ where
304306
TI: 'i,
305307
{
306308
match self.data(folder.interner()) {
307-
TyData::BoundVar(depth) => {
308-
if *depth >= binders {
309-
folder.fold_free_var_ty(*depth - binders, binders)
309+
TyData::BoundVar(debruijn) => {
310+
let debruijn = *debruijn;
311+
if debruijn.within(binders) {
312+
// If `debruijn` refers to one of the binders that
313+
// we folded over, then just return a bound
314+
// variable.
315+
Ok(TyData::<TI>::BoundVar(debruijn).intern(folder.target_interner()))
310316
} else {
311-
Ok(TyData::<TI>::BoundVar(*depth).intern(folder.target_interner()))
317+
// Otherwise, this variable was bound outside the
318+
// folded term, so invoke `fold_free_var_ty`.
319+
let index = debruijn.shifted_out(binders).as_usize();
320+
folder.fold_free_var_ty(index, binders)
312321
}
313322
}
314323
TyData::Dyn(clauses) => {
@@ -368,11 +377,18 @@ where
368377
let interner = folder.interner();
369378
let target_interner = folder.target_interner();
370379
match self.data(interner) {
371-
LifetimeData::BoundVar(depth) => {
372-
if *depth >= binders {
373-
folder.fold_free_var_lifetime(depth - binders, binders)
380+
LifetimeData::BoundVar(debruijn) => {
381+
let debruijn = *debruijn;
382+
if debruijn.within(binders) {
383+
// If `debruijn` refers to one of the binders that
384+
// we folded over, then just return a bound
385+
// variable.
386+
Ok(LifetimeData::<TI>::BoundVar(debruijn).intern(target_interner))
374387
} else {
375-
Ok(LifetimeData::<TI>::BoundVar(*depth).intern(target_interner))
388+
// Otherwise, this variable was bound outside the
389+
// folded term, so invoke `fold_free_var_lifetime`.
390+
let index = debruijn.shifted_out(binders).as_usize();
391+
folder.fold_free_var_lifetime(index, binders)
376392
}
377393
}
378394
LifetimeData::InferenceVar(var) => folder.fold_inference_lifetime(*var, binders),

‎chalk-ir/src/fold/boring_impls.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,7 @@ copy_fold!(UniverseIndex);
190190
copy_fold!(usize);
191191
copy_fold!(PlaceholderIndex);
192192
copy_fold!(QuantifierKind);
193+
copy_fold!(DebruijnIndex);
193194
copy_fold!(chalk_engine::TableIndex);
194195
copy_fold!(chalk_engine::TimeStamp);
195196
copy_fold!(());

‎chalk-ir/src/fold/shift.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -93,8 +93,8 @@ impl<I> Shifter<'_, I> {
9393
/// Given a free variable at `depth`, shifts that depth to `depth
9494
/// + self.adjustment`, and then wraps *that* within the internal
9595
/// set `binders`.
96-
fn adjust(&self, depth: usize, binders: usize) -> usize {
97-
depth + self.adjustment + binders
96+
fn adjust(&self, depth: usize, binders: usize) -> DebruijnIndex {
97+
DebruijnIndex::from(depth + self.adjustment + binders)
9898
}
9999
}
100100

@@ -139,9 +139,9 @@ impl<I> DownShifter<'_, I> {
139139
/// those internal binders (i.e., `depth < self.adjustment`) the
140140
/// this will fail with `Err`. Otherwise, returns the variable at
141141
/// this new depth (but adjusted to appear within `binders`).
142-
fn adjust(&self, depth: usize, binders: usize) -> Fallible<usize> {
142+
fn adjust(&self, depth: usize, binders: usize) -> Fallible<DebruijnIndex> {
143143
match depth.checked_sub(self.adjustment) {
144-
Some(new_depth) => Ok(new_depth + binders),
144+
Some(new_depth) => Ok(DebruijnIndex::from(new_depth + binders)),
145145
None => Err(NoSolution),
146146
}
147147
}

‎chalk-ir/src/fold/subst.rs

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,8 @@ impl<'i, I: Interner> Folder<'i, I> for Subst<'_, 'i, I> {
3131
fn fold_free_var_ty(&mut self, depth: usize, binders: usize) -> Fallible<Ty<I>> {
3232
let interner = self.interner();
3333
if depth >= self.parameters.len() {
34-
Ok(TyData::<I>::BoundVar(depth - self.parameters.len() + binders).intern(interner))
34+
let debruijn = DebruijnIndex::from(depth - self.parameters.len() + binders);
35+
Ok(TyData::<I>::BoundVar(debruijn).intern(interner))
3536
} else {
3637
match self.parameters[depth].data(interner) {
3738
ParameterKind::Ty(t) => Ok(t.shifted_in(interner, binders)),
@@ -43,10 +44,8 @@ impl<'i, I: Interner> Folder<'i, I> for Subst<'_, 'i, I> {
4344
fn fold_free_var_lifetime(&mut self, depth: usize, binders: usize) -> Fallible<Lifetime<I>> {
4445
let interner = self.interner();
4546
if depth >= self.parameters.len() {
46-
Ok(
47-
LifetimeData::<I>::BoundVar(depth - self.parameters.len() + binders)
48-
.intern(interner),
49-
)
47+
let debruijn = DebruijnIndex::from(depth - self.parameters.len() + binders);
48+
Ok(LifetimeData::<I>::BoundVar(debruijn).intern(interner))
5049
} else {
5150
match self.parameters[depth].data(interner) {
5251
ParameterKind::Lifetime(l) => Ok(l.shifted_in(interner, binders)),

0 commit comments

Comments
 (0)