Skip to content

Commit 36fe821

Browse files
yaahcyaahc
committed
Merge branch 'master' of https://github.com/rust-lang/chalk into builtin
2 parents 312dded + 61e5a0b commit 36fe821

32 files changed

+1182
-583
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,13 +1243,17 @@ 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,
12441251
well_known: self.well_known.map(|t| t.lower()),
1245-
})
1252+
};
1253+
1254+
debug!("trait_datum={:?}", trait_datum);
1255+
1256+
Ok(trait_datum)
12461257
}
12471258
}
12481259

‎chalk-integration/src/program.rs

Lines changed: 11 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ use chalk_ir::debug::Angle;
44
use chalk_ir::interner::ChalkIr;
55
use chalk_ir::tls;
66
use chalk_ir::{
7-
debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, GoalData, Goals, ImplId,
8-
Lifetime, Parameter, ParameterKind, ProgramClause, ProgramClauseImplication, StructId,
9-
Substitution, TraitId, Ty, TyData, TypeName,
7+
debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, Lifetime,
8+
Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
9+
TyData, TypeName,
1010
};
1111
use chalk_rust_ir::{
1212
AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
@@ -143,10 +143,7 @@ impl tls::DebugContext for Program {
143143
fmt: &mut fmt::Formatter<'_>,
144144
) -> Result<(), fmt::Error> {
145145
let interner = self.interner();
146-
match parameter.data(interner) {
147-
ParameterKind::Ty(n) => write!(fmt, "{:?}", n),
148-
ParameterKind::Lifetime(n) => write!(fmt, "{:?}", n),
149-
}
146+
write!(fmt, "{:?}", parameter.data(interner).inner_debug())
150147
}
151148

152149
fn debug_goal(
@@ -155,27 +152,7 @@ impl tls::DebugContext for Program {
155152
fmt: &mut fmt::Formatter<'_>,
156153
) -> Result<(), fmt::Error> {
157154
let interner = self.interner();
158-
match goal.data(interner) {
159-
GoalData::Quantified(qkind, ref subgoal) => {
160-
write!(fmt, "{:?}<", qkind)?;
161-
for (index, binder) in subgoal.binders.iter().enumerate() {
162-
if index > 0 {
163-
write!(fmt, ", ")?;
164-
}
165-
match *binder {
166-
ParameterKind::Ty(()) => write!(fmt, "type")?,
167-
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
168-
}
169-
}
170-
write!(fmt, "> {{ {:?} }}", subgoal.value)
171-
}
172-
GoalData::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
173-
GoalData::All(ref goals) => write!(fmt, "all{:?}", goals),
174-
GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
175-
GoalData::EqGoal(ref wc) => write!(fmt, "{:?}", wc),
176-
GoalData::DomainGoal(ref wc) => write!(fmt, "{:?}", wc),
177-
GoalData::CannotProve(()) => write!(fmt, r"¯\_(ツ)_/¯"),
178-
}
155+
write!(fmt, "{:?}", goal.data(interner))
179156
}
180157

181158
fn debug_goals(
@@ -184,15 +161,7 @@ impl tls::DebugContext for Program {
184161
fmt: &mut fmt::Formatter<'_>,
185162
) -> Result<(), fmt::Error> {
186163
let interner = self.interner();
187-
write!(fmt, "(")?;
188-
for (goal, index) in goals.iter(interner).zip(0..) {
189-
if index > 0 {
190-
write!(fmt, ", ")?;
191-
}
192-
write!(fmt, "{:?}", goal)?;
193-
}
194-
write!(fmt, ")")?;
195-
Ok(())
164+
write!(fmt, "{:?}", goals.debug(interner))
196165
}
197166

198167
fn debug_program_clause_implication(
@@ -201,20 +170,7 @@ impl tls::DebugContext for Program {
201170
fmt: &mut fmt::Formatter<'_>,
202171
) -> Result<(), fmt::Error> {
203172
let interner = self.interner();
204-
write!(fmt, "{:?}", pci.consequence)?;
205-
206-
let conditions = pci.conditions.as_slice(interner);
207-
208-
let conds = conditions.len();
209-
if conds == 0 {
210-
return Ok(());
211-
}
212-
213-
write!(fmt, " :- ")?;
214-
for cond in &conditions[..conds - 1] {
215-
write!(fmt, "{:?}, ", cond)?;
216-
}
217-
write!(fmt, "{:?}", conditions[conds - 1])
173+
write!(fmt, "{:?}", pci.debug(interner))
218174
}
219175

220176
fn debug_application_ty(
@@ -223,8 +179,7 @@ impl tls::DebugContext for Program {
223179
fmt: &mut fmt::Formatter<'_>,
224180
) -> Result<(), fmt::Error> {
225181
let interner = self.interner();
226-
let ApplicationTy { name, substitution } = application_ty;
227-
write!(fmt, "{:?}{:?}", name, substitution.with_angle(interner))
182+
write!(fmt, "{:?}", application_ty.debug(interner))
228183
}
229184

230185
fn debug_substitution(
@@ -233,43 +188,16 @@ impl tls::DebugContext for Program {
233188
fmt: &mut fmt::Formatter<'_>,
234189
) -> Result<(), fmt::Error> {
235190
let interner = self.interner();
236-
let mut first = true;
237-
238-
write!(fmt, "[")?;
239-
240-
for (index, value) in substitution.iter(interner).enumerate() {
241-
if first {
242-
first = false;
243-
} else {
244-
write!(fmt, ", ")?;
245-
}
246-
247-
write!(fmt, "?{} := {:?}", index, value)?;
248-
}
249-
250-
write!(fmt, "]")?;
251-
252-
Ok(())
191+
write!(fmt, "{:?}", substitution.debug(interner))
253192
}
254193

255194
fn debug_separator_trait_ref(
256195
&self,
257-
separator_trait_ref: &SeparatorTraitRef<ChalkIr>,
196+
separator_trait_ref: &SeparatorTraitRef<'_, ChalkIr>,
258197
fmt: &mut fmt::Formatter<'_>,
259198
) -> Result<(), fmt::Error> {
260199
let interner = self.interner();
261-
let parameters = separator_trait_ref
262-
.trait_ref
263-
.substitution
264-
.parameters(interner);
265-
write!(
266-
fmt,
267-
"{:?}{}{:?}{:?}",
268-
parameters[0],
269-
separator_trait_ref.separator,
270-
separator_trait_ref.trait_ref.trait_id,
271-
Angle(&parameters[1..])
272-
)
200+
write!(fmt, "{:?}", separator_trait_ref.debug(interner))
273201
}
274202
}
275203

‎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

0 commit comments

Comments
 (0)