Skip to content

Commit 557170e

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #386 from crlf0710/master
Migrate `Vec<ParameterKinds<()>>` and `Vec<ParameterKinds<UniverseIndex>>` to interned
2 parents f438d7e + 5f76ce4 commit 557170e

File tree

33 files changed

+719
-225
lines changed

33 files changed

+719
-225
lines changed

‎chalk-engine/src/forest.rs

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,23 @@ pub enum SubstitutionResult<S> {
113113
Floundered,
114114
}
115115

116+
impl<S> SubstitutionResult<S> {
117+
pub fn as_ref(&self) -> SubstitutionResult<&S> {
118+
match self {
119+
SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst),
120+
SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst),
121+
SubstitutionResult::Floundered => SubstitutionResult::Floundered,
122+
}
123+
}
124+
pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> {
125+
match self {
126+
SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)),
127+
SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)),
128+
SubstitutionResult::Floundered => SubstitutionResult::Floundered,
129+
}
130+
}
131+
}
132+
116133
impl<S: Display> Display for SubstitutionResult<S> {
117134
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
118135
match self {

‎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: 35 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
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,
4+
self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, ParameterKinds,
55
QuantifiedWhereClauses, StructId, Substitution, TraitId,
66
};
77
use chalk_parse::ast::*;
@@ -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,26 +619,31 @@ 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
}
624634
}
625635

626636
impl LowerTypeKind for OpaqueTyDefn {
627637
fn lower_type_kind(&self) -> LowerResult<TypeKind> {
638+
let interner = &ChalkIr;
628639
let binders: Vec<_> = self.parameter_kinds.iter().map(|p| p.lower()).collect();
629640
Ok(TypeKind {
630641
sort: TypeSort::Opaque,
631642
name: self.identifier.str,
632-
binders: chalk_ir::Binders::new(binders.anonymize(), ()),
643+
binders: chalk_ir::Binders::new(
644+
ParameterKinds::from(interner, binders.anonymize()),
645+
crate::Unit,
646+
),
633647
})
634648
}
635649
}
@@ -835,6 +849,7 @@ trait LowerTraitBound {
835849

836850
impl LowerTraitBound for TraitBound {
837851
fn lower(&self, env: &Env) -> LowerResult<rust_ir::TraitBound<ChalkIr>> {
852+
let interner = &ChalkIr;
838853
let trait_id = env.lookup_trait(self.trait_name)?;
839854

840855
let k = env.trait_kind(trait_id);
@@ -848,15 +863,15 @@ impl LowerTraitBound for TraitBound {
848863
.map(|a| Ok(a.lower(env)?))
849864
.collect::<LowerResult<Vec<_>>>()?;
850865

851-
if parameters.len() != k.binders.len() {
866+
if parameters.len() != k.binders.len(interner) {
852867
Err(RustIrError::IncorrectNumberOfTypeParameters {
853868
identifier: self.trait_name,
854-
expected: k.binders.len(),
869+
expected: k.binders.len(interner),
855870
actual: parameters.len(),
856871
})?;
857872
}
858873

859-
for (binder, param) in k.binders.binders.iter().zip(parameters.iter()) {
874+
for (binder, param) in k.binders.binders.iter(interner).zip(parameters.iter()) {
860875
if binder.kind() != param.kind() {
861876
Err(RustIrError::IncorrectTraitParameterKind {
862877
identifier: self.trait_name,
@@ -1062,10 +1077,10 @@ impl LowerTy for Ty {
10621077
Ty::Id { name } => match env.lookup_type(name)? {
10631078
TypeLookup::Struct(id) => {
10641079
let k = env.struct_kind(id);
1065-
if k.binders.len() > 0 {
1080+
if k.binders.len(interner) > 0 {
10661081
Err(RustIrError::IncorrectNumberOfTypeParameters {
10671082
identifier: name,
1068-
expected: k.binders.len(),
1083+
expected: k.binders.len(interner),
10691084
actual: 0,
10701085
})
10711086
} else {
@@ -1118,10 +1133,10 @@ impl LowerTy for Ty {
11181133
};
11191134

11201135
let k = env.struct_kind(id);
1121-
if k.binders.len() != args.len() {
1136+
if k.binders.len(interner) != args.len() {
11221137
Err(RustIrError::IncorrectNumberOfTypeParameters {
11231138
identifier: name,
1124-
expected: k.binders.len(),
1139+
expected: k.binders.len(interner),
11251140
actual: args.len(),
11261141
})?;
11271142
}
@@ -1131,7 +1146,7 @@ impl LowerTy for Ty {
11311146
args.iter().map(|t| Ok(t.lower(env)?)),
11321147
)?;
11331148

1134-
for (param, arg) in k.binders.binders.iter().zip(args.iter()) {
1149+
for (param, arg) in k.binders.binders.iter(interner).zip(args.iter()) {
11351150
if param.kind() != arg.kind() {
11361151
Err(RustIrError::IncorrectParameterKind {
11371152
identifier: name,
@@ -1362,14 +1377,16 @@ pub trait LowerGoal<A> {
13621377

13631378
impl LowerGoal<LoweredProgram> for Goal {
13641379
fn lower(&self, program: &LoweredProgram) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
1380+
let interner = &ChalkIr;
13651381
let associated_ty_lookups: BTreeMap<_, _> = program
13661382
.associated_ty_data
13671383
.iter()
13681384
.map(|(&associated_ty_id, datum)| {
13691385
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();
1386+
let num_trait_params = trait_datum.binders.len(interner);
1387+
let num_addl_params = datum.binders.len(interner) - num_trait_params;
1388+
let addl_parameter_kinds =
1389+
datum.binders.binders.as_slice(interner)[..num_addl_params].to_owned();
13731390
let lookup = AssociatedTyLookup {
13741391
id: associated_ty_id,
13751392
addl_parameter_kinds,

‎chalk-integration/src/program.rs

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -188,6 +188,33 @@ impl tls::DebugContext for Program {
188188
write!(fmt, "{:?}", parameter.data(interner).inner_debug())
189189
}
190190

191+
fn debug_parameter_kinds(
192+
&self,
193+
parameter_kinds: &chalk_ir::ParameterKinds<ChalkIr>,
194+
fmt: &mut fmt::Formatter<'_>,
195+
) -> Result<(), fmt::Error> {
196+
let interner = self.interner();
197+
write!(fmt, "{:?}", parameter_kinds.as_slice(interner))
198+
}
199+
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+
209+
fn debug_canonical_var_kinds(
210+
&self,
211+
parameter_kinds: &chalk_ir::CanonicalVarKinds<ChalkIr>,
212+
fmt: &mut fmt::Formatter<'_>,
213+
) -> Result<(), fmt::Error> {
214+
let interner = self.interner();
215+
write!(fmt, "{:?}", parameter_kinds.as_slice(interner))
216+
}
217+
191218
fn debug_goal(
192219
&self,
193220
goal: &Goal<ChalkIr>,

‎chalk-ir/src/cast.rs

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,8 @@ reflexive_impl!(for(I: Interner) Goal<I>);
8282
reflexive_impl!(for(I: Interner) WhereClause<I>);
8383
reflexive_impl!(for(I: Interner) ProgramClause<I>);
8484
reflexive_impl!(for(I: Interner) QuantifiedWhereClause<I>);
85+
reflexive_impl!(for(I: Interner) ParameterKinds<I>);
86+
reflexive_impl!(for(I: Interner) CanonicalVarKinds<I>);
8587

8688
impl<I: Interner> CastTo<WhereClause<I>> for TraitRef<I> {
8789
fn cast_to(self, _interner: &I) -> WhereClause<I> {
@@ -138,7 +140,7 @@ impl<I: Interner> CastTo<Goal<I>> for EqGoal<I> {
138140
}
139141
}
140142

141-
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> {
142144
fn cast_to(self, interner: &I) -> Goal<I> {
143145
GoalData::Quantified(
144146
QuantifierKind::ForAll,
@@ -193,10 +195,10 @@ where
193195
}
194196
}
195197

196-
impl<T, I> CastTo<ProgramClause<I>> for Binders<T>
198+
impl<I, T> CastTo<ProgramClause<I>> for Binders<T>
197199
where
198-
T: CastTo<DomainGoal<I>>,
199200
I: Interner,
201+
T: HasInterner<Interner = I> + CastTo<DomainGoal<I>>,
200202
{
201203
fn cast_to(self, interner: &I) -> ProgramClause<I> {
202204
ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication {
@@ -268,16 +270,16 @@ where
268270
impl<T, U> CastTo<Canonical<U>> for Canonical<T>
269271
where
270272
T: CastTo<U> + HasInterner,
271-
U: HasInterner,
273+
U: HasInterner<Interner = T::Interner>,
272274
{
273-
fn cast_to(self, interner: &U::Interner) -> Canonical<U> {
275+
fn cast_to(self, interner: &T::Interner) -> Canonical<U> {
274276
// Subtle point: It should be ok to re-use the binders here,
275277
// because `cast()` never introduces new inference variables,
276278
// nor changes the "substance" of the type we are working
277279
// with. It just introduces new wrapper types.
278280
Canonical {
279281
value: self.value.cast(interner),
280-
binders: self.binders,
282+
binders: self.binders.cast(interner),
281283
}
282284
}
283285
}

‎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
}

0 commit comments

Comments
 (0)