Skip to content

Commit 61e5a0b

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #360 from nikomatsakis/debruijn
Count binders, not variables
2 parents d383af7 + 042c296 commit 61e5a0b

31 files changed

+965
-499
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-integration/src/lowering.rs

Lines changed: 35 additions & 24 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, BoundVar, 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>, BoundVar>;
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(BoundVar),
6666
}
6767

6868
enum LifetimeLookup {
69-
Parameter(usize),
69+
Parameter(BoundVar),
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, BoundVar::new(DebruijnIndex::INNERMOST, 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()))
147150
.chain(binders)
148151
.collect();
149152
if parameter_map.len() != self.parameter_map.len() + len {
@@ -395,6 +398,16 @@ trait LowerParameterMap {
395398
.chain(self.synthetic_parameters()) // (*) see below
396399
.collect()
397400
*/
401+
402+
// (*) It is important that the declared parameters come
403+
// before the synthetic parameters in the ordering. This is
404+
// because of traits, when used as types, only have the first
405+
// N parameters in their kind (that is, they do not have Self).
406+
//
407+
// Note that if `Self` appears in the where-clauses etc, the
408+
// trait is not object-safe, and hence not supposed to be used
409+
// as an object. Actually the handling of object types is
410+
// probably just kind of messed up right now. That's ok.
398411
}
399412

400413
fn parameter_refs(&self) -> Vec<chalk_ir::Parameter<ChalkIr>> {
@@ -407,16 +420,10 @@ trait LowerParameterMap {
407420
}
408421

409422
fn parameter_map(&self) -> ParameterMap {
410-
// (*) It is important that the declared parameters come
411-
// before the subtle parameters in the ordering. This is
412-
// because of traits, when used as types, only have the first
413-
// N parameters in their kind (that is, they do not have Self).
414-
//
415-
// Note that if `Self` appears in the where-clauses etc, the
416-
// trait is not object-safe, and hence not supposed to be used
417-
// as an object. Actually the handling of object types is
418-
// probably just kind of messed up right now. That's ok.
419-
self.all_parameters().into_iter().zip(0..).collect()
423+
self.all_parameters()
424+
.into_iter()
425+
.zip((0..).map(|i| BoundVar::new(DebruijnIndex::INNERMOST, i)))
426+
.collect()
420427
}
421428

422429
fn interner(&self) -> &ChalkIr {
@@ -997,7 +1004,11 @@ impl LowerTy for Ty {
9971004
.flat_map(|qil| {
9981005
qil.into_where_clauses(
9991006
interner,
1000-
chalk_ir::TyData::BoundVar(0).intern(interner),
1007+
chalk_ir::TyData::BoundVar(BoundVar::new(
1008+
DebruijnIndex::INNERMOST,
1009+
0,
1010+
))
1011+
.intern(interner),
10011012
)
10021013
})
10031014
.collect())
@@ -1187,11 +1198,7 @@ impl LowerClause for Clause {
11871198
.into_iter()
11881199
.map(
11891200
|implication: chalk_ir::Binders<chalk_ir::ProgramClauseImplication<ChalkIr>>| {
1190-
if implication.binders.is_empty() {
1191-
chalk_ir::ProgramClause::Implies(implication.value)
1192-
} else {
1193-
chalk_ir::ProgramClause::ForAll(implication)
1194-
}
1201+
chalk_ir::ProgramClause::ForAll(implication)
11951202
},
11961203
)
11971204
.collect();
@@ -1236,12 +1243,16 @@ impl LowerTrait for TraitDefn {
12361243
.map(|defn| env.associated_ty_lookups[&(trait_id, defn.name.str)].id)
12371244
.collect();
12381245

1239-
Ok(rust_ir::TraitDatum {
1246+
let trait_datum = rust_ir::TraitDatum {
12401247
id: trait_id,
12411248
binders: binders,
12421249
flags: self.flags.lower(),
12431250
associated_ty_ids,
1244-
})
1251+
};
1252+
1253+
debug!("trait_datum={:?}", trait_datum);
1254+
1255+
Ok(trait_datum)
12451256
}
12461257
}
12471258

‎chalk-ir/src/cast.rs

Lines changed: 9 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -138,15 +138,11 @@ impl<I: Interner> CastTo<Goal<I>> for EqGoal<I> {
138138

139139
impl<T: CastTo<Goal<I>>, I: Interner> CastTo<Goal<I>> for Binders<T> {
140140
fn cast_to(self, interner: &I) -> Goal<I> {
141-
if self.binders.is_empty() {
142-
self.value.cast(interner)
143-
} else {
144-
GoalData::Quantified(
145-
QuantifierKind::ForAll,
146-
self.map(|bound| bound.cast(interner)),
147-
)
148-
.intern(interner)
149-
}
141+
GoalData::Quantified(
142+
QuantifierKind::ForAll,
143+
self.map(|bound| bound.cast(interner)),
144+
)
145+
.intern(interner)
150146
}
151147
}
152148

@@ -199,14 +195,10 @@ where
199195
I: Interner,
200196
{
201197
fn cast_to(self, interner: &I) -> ProgramClause<I> {
202-
if self.binders.is_empty() {
203-
self.value.cast::<ProgramClause<I>>(interner)
204-
} else {
205-
ProgramClause::ForAll(self.map(|bound| ProgramClauseImplication {
206-
consequence: bound.cast(interner),
207-
conditions: Goals::new(interner),
208-
}))
209-
}
198+
ProgramClause::ForAll(self.map(|bound| ProgramClauseImplication {
199+
consequence: bound.cast(interner),
200+
conditions: Goals::new(interner),
201+
}))
210202
}
211203
}
212204

‎chalk-ir/src/debug.rs

Lines changed: 38 additions & 13 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,20 @@ impl<I: Interner> Debug for TyData<I> {
134134
}
135135
}
136136

137+
impl Debug for BoundVar {
138+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
139+
let BoundVar { debruijn, index } = self;
140+
write!(fmt, "{:?}.{:?}", debruijn, index)
141+
}
142+
}
143+
144+
impl Debug for DebruijnIndex {
145+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
146+
let DebruijnIndex { depth } = self;
147+
write!(fmt, "^{}", depth)
148+
}
149+
}
150+
137151
impl<I: Interner> Debug for DynTy<I> {
138152
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
139153
let DynTy { bounds } = self;
@@ -161,7 +175,7 @@ impl<I: Interner> Debug for Fn<I> {
161175
impl<I: Interner> Debug for LifetimeData<I> {
162176
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
163177
match self {
164-
LifetimeData::BoundVar(depth) => write!(fmt, "'^{}", depth),
178+
LifetimeData::BoundVar(db) => write!(fmt, "'{:?}", db),
165179
LifetimeData::InferenceVar(var) => write!(fmt, "'{:?}", var),
166180
LifetimeData::Placeholder(index) => write!(fmt, "'{:?}", index),
167181
LifetimeData::Phantom(..) => unreachable!(),
@@ -499,19 +513,24 @@ impl<T: Debug> Debug for Binders<T> {
499513
ref binders,
500514
ref value,
501515
} = *self;
502-
if !binders.is_empty() {
503-
write!(fmt, "for<")?;
504-
for (index, binder) in binders.iter().enumerate() {
505-
if index > 0 {
506-
write!(fmt, ", ")?;
507-
}
508-
match *binder {
509-
ParameterKind::Ty(()) => write!(fmt, "type")?,
510-
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
511-
}
516+
517+
// NB: We always print the `for<>`, even if it is empty,
518+
// because it may affect the debruijn indices of things
519+
// contained within. For example, `for<> { ^1.0 }` is very
520+
// different from `^1.0` in terms of what variable is being
521+
// referenced.
522+
523+
write!(fmt, "for<")?;
524+
for (index, binder) in binders.iter().enumerate() {
525+
if index > 0 {
526+
write!(fmt, ", ")?;
527+
}
528+
match *binder {
529+
ParameterKind::Ty(()) => write!(fmt, "type")?,
530+
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
512531
}
513-
write!(fmt, "> ")?;
514532
}
533+
write!(fmt, "> ")?;
515534
Debug::fmt(value, fmt)
516535
}
517536
}
@@ -536,6 +555,12 @@ impl<T: Display> Display for Canonical<T> {
536555
let Canonical { binders, value } = self;
537556

538557
if binders.is_empty() {
558+
// Ordinarily, we try to print all binder levels, if they
559+
// are empty, but we can skip in this *particular* case
560+
// because we know that `Canonical` terms are never
561+
// supposed to contain free variables. In other words,
562+
// all "bound variables" that appear inside the canonical
563+
// value must reference values that appear in `binders`.
539564
write!(f, "{}", value)?;
540565
} else {
541566
write!(f, "for<")?;

0 commit comments

Comments
 (0)