Skip to content

Commit 761d360

Browse files
crlf0710crlf0710
committed
Switch Vec<ParameterKind<()>> to ParameterKinds<I>.
1 parent 02d1033 commit 761d360

File tree

27 files changed

+296
-161
lines changed

27 files changed

+296
-161
lines changed

‎chalk-engine/src/lib.rs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -278,5 +278,3 @@ impl Minimums {
278278
min(self.positive, self.negative)
279279
}
280280
}
281-
282-

‎chalk-integration/src/lib.rs

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ pub mod program;
1111
pub mod program_environment;
1212
pub mod query;
1313

14+
use chalk_ir::interner::{ChalkIr, HasInterner};
1415
pub use chalk_ir::interner::{Identifier, RawId};
1516
use chalk_ir::Binders;
1617

@@ -21,9 +22,16 @@ pub enum TypeSort {
2122
Opaque,
2223
}
2324

25+
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
26+
pub struct Unit;
27+
28+
impl HasInterner for Unit {
29+
type Interner = ChalkIr;
30+
}
31+
2432
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
2533
pub struct TypeKind {
2634
pub sort: TypeSort,
2735
pub name: Identifier,
28-
pub binders: Binders<()>,
36+
pub binders: Binders<Unit>,
2937
}

‎chalk-integration/src/lowering.rs

Lines changed: 31 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
use chalk_ir::cast::{Cast, Caster};
2-
use chalk_ir::interner::ChalkIr;
2+
use chalk_ir::interner::{ChalkIr, HasInterner};
33
use chalk_ir::{
4-
self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId,
5-
QuantifiedWhereClauses, StructId, Substitution, TraitId,
4+
self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, ParameterKinds, QuantifiedWhereClauses,
5+
StructId, Substitution, TraitId,
66
};
77
use chalk_parse::ast::*;
88
use chalk_rust_ir as rust_ir;
@@ -174,11 +174,16 @@ impl<'k> Env<'k> {
174174
where
175175
I: IntoIterator<Item = chalk_ir::ParameterKind<Ident>>,
176176
I::IntoIter: ExactSizeIterator,
177+
T: HasInterner<Interner = ChalkIr>,
177178
OP: FnOnce(&Self) -> LowerResult<T>,
178179
{
180+
let interner = &ChalkIr;
179181
let binders: Vec<_> = binders.into_iter().collect();
180182
let env = self.introduce(binders.iter().cloned())?;
181-
Ok(chalk_ir::Binders::new(binders.anonymize(), op(&env)?))
183+
Ok(chalk_ir::Binders::new(
184+
ParameterKinds::from(interner, binders.anonymize()),
185+
op(&env)?,
186+
))
182187
}
183188
}
184189

@@ -594,10 +599,14 @@ trait LowerWhereClauses {
594599

595600
impl LowerTypeKind for StructDefn {
596601
fn lower_type_kind(&self) -> LowerResult<TypeKind> {
602+
let interner = &ChalkIr;
597603
Ok(TypeKind {
598604
sort: TypeSort::Struct,
599605
name: self.name.str,
600-
binders: chalk_ir::Binders::new(self.all_parameters().anonymize(), ()),
606+
binders: chalk_ir::Binders::new(
607+
ParameterKinds::from(interner, self.all_parameters().anonymize()),
608+
crate::Unit,
609+
),
601610
})
602611
}
603612
}
@@ -610,14 +619,15 @@ impl LowerWhereClauses for StructDefn {
610619

611620
impl LowerTypeKind for TraitDefn {
612621
fn lower_type_kind(&self) -> LowerResult<TypeKind> {
622+
let interner = &ChalkIr;
613623
let binders: Vec<_> = self.parameter_kinds.iter().map(|p| p.lower()).collect();
614624
Ok(TypeKind {
615625
sort: TypeSort::Trait,
616626
name: self.name.str,
617627
binders: chalk_ir::Binders::new(
618628
// for the purposes of the *type*, ignore `Self`:
619-
binders.anonymize(),
620-
(),
629+
ParameterKinds::from(interner, binders.anonymize()),
630+
crate::Unit,
621631
),
622632
})
623633
}
@@ -835,6 +845,7 @@ trait LowerTraitBound {
835845

836846
impl LowerTraitBound for TraitBound {
837847
fn lower(&self, env: &Env) -> LowerResult<rust_ir::TraitBound<ChalkIr>> {
848+
let interner = &ChalkIr;
838849
let trait_id = env.lookup_trait(self.trait_name)?;
839850

840851
let k = env.trait_kind(trait_id);
@@ -848,15 +859,15 @@ impl LowerTraitBound for TraitBound {
848859
.map(|a| Ok(a.lower(env)?))
849860
.collect::<LowerResult<Vec<_>>>()?;
850861

851-
if parameters.len() != k.binders.len() {
862+
if parameters.len() != k.binders.len(interner) {
852863
Err(RustIrError::IncorrectNumberOfTypeParameters {
853864
identifier: self.trait_name,
854-
expected: k.binders.len(),
865+
expected: k.binders.len(interner),
855866
actual: parameters.len(),
856867
})?;
857868
}
858869

859-
for (binder, param) in k.binders.binders.iter().zip(parameters.iter()) {
870+
for (binder, param) in k.binders.binders.iter(interner).zip(parameters.iter()) {
860871
if binder.kind() != param.kind() {
861872
Err(RustIrError::IncorrectTraitParameterKind {
862873
identifier: self.trait_name,
@@ -1062,10 +1073,10 @@ impl LowerTy for Ty {
10621073
Ty::Id { name } => match env.lookup_type(name)? {
10631074
TypeLookup::Struct(id) => {
10641075
let k = env.struct_kind(id);
1065-
if k.binders.len() > 0 {
1076+
if k.binders.len(interner) > 0 {
10661077
Err(RustIrError::IncorrectNumberOfTypeParameters {
10671078
identifier: name,
1068-
expected: k.binders.len(),
1079+
expected: k.binders.len(interner),
10691080
actual: 0,
10701081
})
10711082
} else {
@@ -1118,10 +1129,10 @@ impl LowerTy for Ty {
11181129
};
11191130

11201131
let k = env.struct_kind(id);
1121-
if k.binders.len() != args.len() {
1132+
if k.binders.len(interner) != args.len() {
11221133
Err(RustIrError::IncorrectNumberOfTypeParameters {
11231134
identifier: name,
1124-
expected: k.binders.len(),
1135+
expected: k.binders.len(interner),
11251136
actual: args.len(),
11261137
})?;
11271138
}
@@ -1131,7 +1142,7 @@ impl LowerTy for Ty {
11311142
args.iter().map(|t| Ok(t.lower(env)?)),
11321143
)?;
11331144

1134-
for (param, arg) in k.binders.binders.iter().zip(args.iter()) {
1145+
for (param, arg) in k.binders.binders.iter(interner).zip(args.iter()) {
11351146
if param.kind() != arg.kind() {
11361147
Err(RustIrError::IncorrectParameterKind {
11371148
identifier: name,
@@ -1362,14 +1373,16 @@ pub trait LowerGoal<A> {
13621373

13631374
impl LowerGoal<LoweredProgram> for Goal {
13641375
fn lower(&self, program: &LoweredProgram) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
1376+
let interner = &ChalkIr;
13651377
let associated_ty_lookups: BTreeMap<_, _> = program
13661378
.associated_ty_data
13671379
.iter()
13681380
.map(|(&associated_ty_id, datum)| {
13691381
let trait_datum = &program.trait_data[&datum.trait_id];
1370-
let num_trait_params = trait_datum.binders.len();
1371-
let num_addl_params = datum.binders.len() - num_trait_params;
1372-
let addl_parameter_kinds = datum.binders.binders[..num_addl_params].to_owned();
1382+
let num_trait_params = trait_datum.binders.len(interner);
1383+
let num_addl_params = datum.binders.len(interner) - num_trait_params;
1384+
let addl_parameter_kinds =
1385+
datum.binders.binders.as_slice(interner)[..num_addl_params].to_owned();
13731386
let lookup = AssociatedTyLookup {
13741387
id: associated_ty_id,
13751388
addl_parameter_kinds,

‎chalk-integration/src/program.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -197,6 +197,15 @@ impl tls::DebugContext for Program {
197197
write!(fmt, "{:?}", parameter_kinds.as_slice(interner))
198198
}
199199

200+
fn debug_parameter_kinds_with_angles(
201+
&self,
202+
parameter_kinds: &chalk_ir::ParameterKinds<ChalkIr>,
203+
fmt: &mut fmt::Formatter<'_>,
204+
) -> Result<(), fmt::Error> {
205+
let interner = self.interner();
206+
write!(fmt, "{:?}", parameter_kinds.inner_debug(interner))
207+
}
208+
200209
fn debug_parameter_kinds_with_universe_index(
201210
&self,
202211
parameter_kinds: &chalk_ir::ParameterKindsWithUniverseIndex<ChalkIr>,

‎chalk-ir/src/cast.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,7 @@ impl<I: Interner> CastTo<Goal<I>> for EqGoal<I> {
140140
}
141141
}
142142

143-
impl<T: CastTo<Goal<I>>, I: Interner> CastTo<Goal<I>> for Binders<T> {
143+
impl<I: Interner, T: HasInterner<Interner = I> + CastTo<Goal<I>>> CastTo<Goal<I>> for Binders<T> {
144144
fn cast_to(self, interner: &I) -> Goal<I> {
145145
GoalData::Quantified(
146146
QuantifierKind::ForAll,
@@ -195,10 +195,10 @@ where
195195
}
196196
}
197197

198-
impl<T, I> CastTo<ProgramClause<I>> for Binders<T>
198+
impl<I, T> CastTo<ProgramClause<I>> for Binders<T>
199199
where
200-
T: CastTo<DomainGoal<I>>,
201200
I: Interner,
201+
T: HasInterner<Interner = I> + CastTo<DomainGoal<I>>,
202202
{
203203
fn cast_to(self, interner: &I) -> ProgramClause<I> {
204204
ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication {

‎chalk-ir/src/could_match.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ where
5050

5151
fn zip_binders<T>(&mut self, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
5252
where
53-
T: Zip<I>,
53+
T: HasInterner + Zip<I>,
5454
{
5555
Zip::zip_with(self, &a.value, &b.value)
5656
}

‎chalk-ir/src/debug.rs

Lines changed: 57 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -210,22 +210,64 @@ impl<I: Interner> Debug for LifetimeData<I> {
210210
}
211211
}
212212

213+
impl<I: Interner> ParameterKinds<I> {
214+
fn debug(&self) -> ParameterKindsDebug<'_, I> {
215+
ParameterKindsDebug(self)
216+
}
217+
218+
pub fn inner_debug<'a>(&'a self, interner: &'a I) -> ParameterKindsInnerDebug<'a, I> {
219+
ParameterKindsInnerDebug {
220+
parameter_kinds: self,
221+
interner,
222+
}
223+
}
224+
}
225+
226+
struct ParameterKindsDebug<'a, I: Interner>(&'a ParameterKinds<I>);
227+
228+
impl<'a, I: Interner> Debug for ParameterKindsDebug<'a, I> {
229+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
230+
I::debug_parameter_kinds_with_angles(self.0, fmt)
231+
.unwrap_or_else(|| write!(fmt, "{:?}", self.0.interned))
232+
}
233+
}
234+
235+
pub struct ParameterKindsInnerDebug<'a, I: Interner> {
236+
parameter_kinds: &'a ParameterKinds<I>,
237+
interner: &'a I,
238+
}
239+
240+
impl<'a, I: Interner> Debug for ParameterKindsInnerDebug<'a, I> {
241+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
242+
// NB: We always print the `for<>`, even if it is empty,
243+
// because it may affect the debruijn indices of things
244+
// contained within. For example, `for<> { ^1.0 }` is very
245+
// different from `^1.0` in terms of what variable is being
246+
// referenced.
247+
write!(fmt, "<")?;
248+
for (index, binder) in self.parameter_kinds.iter(self.interner).enumerate() {
249+
if index > 0 {
250+
write!(fmt, ", ")?;
251+
}
252+
match *binder {
253+
ParameterKind::Ty(()) => write!(fmt, "type")?,
254+
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
255+
}
256+
}
257+
write!(fmt, ">")
258+
}
259+
}
260+
213261
impl<I: Interner> Debug for GoalData<I> {
214262
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
215263
match self {
216-
GoalData::Quantified(qkind, ref subgoal) => {
217-
write!(fmt, "{:?}<", qkind)?;
218-
for (index, binder) in subgoal.binders.iter().enumerate() {
219-
if index > 0 {
220-
write!(fmt, ", ")?;
221-
}
222-
match *binder {
223-
ParameterKind::Ty(()) => write!(fmt, "type")?,
224-
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
225-
}
226-
}
227-
write!(fmt, "> {{ {:?} }}", subgoal.value)
228-
}
264+
GoalData::Quantified(qkind, ref subgoal) => write!(
265+
fmt,
266+
"{:?}{:?} {{ {:?} }}",
267+
qkind,
268+
subgoal.binders.debug(),
269+
subgoal.value
270+
),
229271
GoalData::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
230272
GoalData::All(ref goals) => write!(fmt, "all{:?}", goals),
231273
GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
@@ -593,30 +635,13 @@ impl<I: Interner> Debug for EqGoal<I> {
593635
}
594636
}
595637

596-
impl<T: Debug> Debug for Binders<T> {
638+
impl<T: HasInterner + Debug> Debug for Binders<T> {
597639
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
598640
let Binders {
599641
ref binders,
600642
ref value,
601643
} = *self;
602-
603-
// NB: We always print the `for<>`, even if it is empty,
604-
// because it may affect the debruijn indices of things
605-
// contained within. For example, `for<> { ^1.0 }` is very
606-
// different from `^1.0` in terms of what variable is being
607-
// referenced.
608-
609-
write!(fmt, "for<")?;
610-
for (index, binder) in binders.iter().enumerate() {
611-
if index > 0 {
612-
write!(fmt, ", ")?;
613-
}
614-
match *binder {
615-
ParameterKind::Ty(()) => write!(fmt, "type")?,
616-
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
617-
}
618-
}
619-
write!(fmt, "> ")?;
644+
write!(fmt, "for{:?} ", binders.debug())?;
620645
Debug::fmt(value, fmt)
621646
}
622647
}
@@ -687,17 +712,6 @@ impl<'a, T: HasInterner + Display> Display for CanonicalDisplay<'a, T> {
687712
}
688713
}
689714

690-
pub struct CanonicalDisplay<'a, I: Interner, T> {
691-
canonical: &'a Canonical<I, T>,
692-
interner: &'a I,
693-
}
694-
695-
impl<'a, I: Interner, T: Display> Display for CanonicalDisplay<'a, I, T> {
696-
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
697-
DisplayWithInterner::fmt_with_interner(self.canonical, self.interner, f)
698-
}
699-
}
700-
701715
impl<T: Debug, L: Debug> Debug for ParameterKind<T, L> {
702716
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
703717
match *self {

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

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,8 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Fn<I> {
3030

3131
impl<T, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Binders<T>
3232
where
33-
T: Fold<I, TI>,
33+
T: HasInterner<Interner = I> + Fold<I, TI>,
34+
<T as Fold<I, TI>>::Result: HasInterner<Interner = TI>,
3435
I: Interner,
3536
{
3637
type Result = Binders<T::Result>;
@@ -48,10 +49,10 @@ where
4849
value: self_value,
4950
} = self;
5051
let value = self_value.fold_with(folder, outer_binder.shifted_in())?;
51-
Ok(Binders {
52-
binders: self_binders.clone(),
53-
value: value,
54-
})
52+
let binders = ParameterKinds {
53+
interned: TI::transfer_parameter_kinds(self_binders.interned().clone()),
54+
};
55+
Ok(Binders::new(binders, value))
5556
}
5657
}
5758

0 commit comments

Comments
 (0)