Skip to content

Commit 8157eee

Browse files
leoyvensnikomatsakis
leoyvens
authored and
nikomatsakis
committed
One universe many types
1 parent ea09744 commit 8157eee

File tree

11 files changed

+50
-53
lines changed

11 files changed

+50
-53
lines changed

‎chalk-ir/src/debug.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ impl Debug for TypeName {
3030
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
3131
match self {
3232
TypeName::ItemId(id) => write!(fmt, "{:?}", id),
33-
TypeName::ForAll(universe) => write!(fmt, "!{}", universe.counter),
33+
TypeName::ForAll(universe) => write!(fmt, "!{}_{}", universe.ui.counter, universe.idx),
3434
TypeName::AssociatedType(assoc_ty) => write!(fmt, "{:?}", assoc_ty),
3535
}
3636
}

‎chalk-ir/src/fold.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,7 @@ pub trait UniversalFolder {
135135
///
136136
/// - `universe` is the universe of the `TypeName::ForAll` that was found
137137
/// - `binders` is the number of binders in scope
138-
fn fold_free_universal_ty(&mut self, universe: UniverseIndex, binders: usize) -> Fallible<Ty>;
138+
fn fold_free_universal_ty(&mut self, universe: UniversalIndex, binders: usize) -> Fallible<Ty>;
139139

140140
/// As with `fold_free_universal_ty`, but for lifetimes.
141141
fn fold_free_universal_lifetime(
@@ -151,8 +151,8 @@ pub trait UniversalFolder {
151151
pub trait IdentityUniversalFolder {}
152152

153153
impl<T: IdentityUniversalFolder> UniversalFolder for T {
154-
fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible<Ty> {
155-
Ok(TypeName::ForAll(universe).to_ty())
154+
fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible<Ty> {
155+
Ok(universe.to_ty())
156156
}
157157

158158
fn fold_free_universal_lifetime(

‎chalk-ir/src/lib.rs

+8-10
Original file line numberDiff line numberDiff line change
@@ -96,21 +96,12 @@ pub enum TypeName {
9696
ItemId(ItemId),
9797

9898
/// skolemized form of a type parameter like `T`
99-
ForAll(UniverseIndex),
99+
ForAll(UniversalIndex),
100100

101101
/// an associated type like `Iterator::Item`; see `AssociatedType` for details
102102
AssociatedType(ItemId),
103103
}
104104

105-
impl TypeName {
106-
pub fn to_ty(self) -> Ty {
107-
Ty::Apply(ApplicationTy {
108-
name: self,
109-
parameters: vec![],
110-
})
111-
}
112-
}
113-
114105
/// An universe index is how a universally quantified parameter is
115106
/// represented when it's binder is moved into the environment.
116107
/// An example chain of transformations would be:
@@ -220,6 +211,13 @@ impl UniversalIndex {
220211
pub fn to_lifetime(self) -> Lifetime {
221212
Lifetime::ForAll(self)
222213
}
214+
215+
pub fn to_ty(self) -> Ty {
216+
Ty::Apply(ApplicationTy {
217+
name: TypeName::ForAll(self),
218+
parameters: vec![],
219+
})
220+
}
223221
}
224222

225223
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]

‎chalk-ir/src/macros.rs

+6-1
Original file line numberDiff line numberDiff line change
@@ -69,5 +69,10 @@ macro_rules! lifetime {
6969
#[macro_export]
7070
macro_rules! ty_name {
7171
((item $n:expr)) => { $crate::TypeName::ItemId(ItemId { index: $n }) };
72-
((skol $n:expr)) => { $crate::TypeName::ForAll(UniverseIndex { counter: $n }) }
72+
((skol $n:expr)) => { $crate::TypeName::ForAll(
73+
UniversalIndex {
74+
ui: UniverseIndex { counter: $n },
75+
idx: 0,
76+
})
77+
}
7378
}

‎chalk-solve/src/infer/canonicalize.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -94,9 +94,9 @@ impl<'q> Canonicalizer<'q> {
9494
impl<'q> DefaultTypeFolder for Canonicalizer<'q> {}
9595

9696
impl<'q> UniversalFolder for Canonicalizer<'q> {
97-
fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible<Ty> {
98-
self.max_universe = max(self.max_universe, universe);
99-
Ok(TypeName::ForAll(universe).to_ty())
97+
fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible<Ty> {
98+
self.max_universe = max(self.max_universe, universe.ui);
99+
Ok(universe.to_ty())
100100
}
101101

102102
fn fold_free_universal_lifetime(

‎chalk-solve/src/infer/instantiate.rs

+6-12
Original file line numberDiff line numberDiff line change
@@ -100,24 +100,18 @@ impl InferenceTable {
100100
T: Fold,
101101
{
102102
let (binders, value) = arg.split();
103-
let lifetime_ui = self.new_universe();
104-
let mut idx = 0;
103+
let ui = self.new_universe();
105104
let parameters: Vec<_> = binders
106105
.iter()
107-
.map(|pk| {
106+
.enumerate()
107+
.map(|(idx, pk)| {
108+
let universal_idx = UniversalIndex { ui, idx };
108109
match *pk {
109110
ParameterKind::Lifetime(()) => {
110-
let lt = Lifetime::ForAll(UniversalIndex { ui: lifetime_ui, idx });
111-
idx += 1;
111+
let lt = universal_idx.to_lifetime();
112112
ParameterKind::Lifetime(lt)
113113
}
114-
ParameterKind::Ty(()) => {
115-
let new_universe = self.new_universe();
116-
ParameterKind::Ty(Ty::Apply(ApplicationTy {
117-
name: TypeName::ForAll(new_universe),
118-
parameters: vec![],
119-
}))
120-
}
114+
ParameterKind::Ty(()) => ParameterKind::Ty(universal_idx.to_ty()),
121115
}
122116
})
123117
.collect();

‎chalk-solve/src/infer/invert.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ impl InferenceTable {
9797

9898
struct Inverter<'q> {
9999
table: &'q mut InferenceTable,
100-
inverted_ty: HashMap<UniverseIndex, InferenceVariable>,
100+
inverted_ty: HashMap<UniversalIndex, InferenceVariable>,
101101
inverted_lifetime: HashMap<UniversalIndex, InferenceVariable>,
102102
}
103103

@@ -114,12 +114,12 @@ impl<'q> Inverter<'q> {
114114
impl<'q> DefaultTypeFolder for Inverter<'q> {}
115115

116116
impl<'q> UniversalFolder for Inverter<'q> {
117-
fn fold_free_universal_ty(&mut self, universe: UniverseIndex, binders: usize) -> Fallible<Ty> {
117+
fn fold_free_universal_ty(&mut self, universe: UniversalIndex, binders: usize) -> Fallible<Ty> {
118118
let table = &mut self.table;
119119
Ok(
120120
self.inverted_ty
121121
.entry(universe)
122-
.or_insert_with(|| table.new_variable(universe))
122+
.or_insert_with(|| table.new_variable(universe.ui))
123123
.to_ty()
124124
.shifted_in(binders),
125125
)

‎chalk-solve/src/infer/ucanonicalize.rs

+9-9
Original file line numberDiff line numberDiff line change
@@ -220,9 +220,9 @@ struct UCollector<'q> {
220220
impl<'q> DefaultTypeFolder for UCollector<'q> {}
221221

222222
impl<'q> UniversalFolder for UCollector<'q> {
223-
fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible<Ty> {
224-
self.universes.add(universe);
225-
Ok(TypeName::ForAll(universe).to_ty())
223+
fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible<Ty> {
224+
self.universes.add(universe.ui);
225+
Ok(universe.to_ty())
226226
}
227227

228228
fn fold_free_universal_lifetime(
@@ -246,11 +246,11 @@ impl<'q> DefaultTypeFolder for UMapToCanonical<'q> {}
246246
impl<'q> UniversalFolder for UMapToCanonical<'q> {
247247
fn fold_free_universal_ty(
248248
&mut self,
249-
universe0: UniverseIndex,
249+
universe0: UniversalIndex,
250250
_binders: usize,
251251
) -> Fallible<Ty> {
252-
let universe = self.universes.map_universe_to_canonical(universe0);
253-
Ok(TypeName::ForAll(universe).to_ty())
252+
let ui = self.universes.map_universe_to_canonical(universe0.ui);
253+
Ok(UniversalIndex { ui, idx: universe0.idx }.to_ty())
254254
}
255255

256256
fn fold_free_universal_lifetime(
@@ -274,11 +274,11 @@ impl<'q> DefaultTypeFolder for UMapFromCanonical<'q> {}
274274
impl<'q> UniversalFolder for UMapFromCanonical<'q> {
275275
fn fold_free_universal_ty(
276276
&mut self,
277-
universe0: UniverseIndex,
277+
universe0: UniversalIndex,
278278
_binders: usize,
279279
) -> Fallible<Ty> {
280-
let universe = self.universes.map_universe_from_canonical(universe0);
281-
Ok(TypeName::ForAll(universe).to_ty())
280+
let ui = self.universes.map_universe_from_canonical(universe0.ui);
281+
Ok(UniversalIndex { ui, idx: universe0.idx }.to_ty())
282282
}
283283

284284
fn fold_free_universal_lifetime(

‎chalk-solve/src/infer/unify.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -377,11 +377,11 @@ impl<'u, 't> OccursCheck<'u, 't> {
377377
impl<'u, 't> DefaultTypeFolder for OccursCheck<'u, 't> {}
378378

379379
impl<'u, 't> UniversalFolder for OccursCheck<'u, 't> {
380-
fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible<Ty> {
381-
if self.universe_index < universe {
380+
fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible<Ty> {
381+
if self.universe_index < universe.ui {
382382
Err(NoSolution)
383383
} else {
384-
Ok(TypeName::ForAll(universe).to_ty()) // no need to shift, not relative to depth
384+
Ok(universe.to_ty()) // no need to shift, not relative to depth
385385
}
386386
}
387387

‎chalk-solve/src/solve/slg/test.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -482,7 +482,7 @@ fn subgoal_cycle_uninhabited() {
482482
Answer {
483483
subst: Canonical {
484484
value: ConstrainedSubst {
485-
subst: [?0 := !1],
485+
subst: [?0 := !1_0],
486486
constraints: []
487487
},
488488
binders: []

‎chalk-solve/src/solve/test.rs

+7-7
Original file line numberDiff line numberDiff line change
@@ -476,7 +476,7 @@ fn normalize_basic() {
476476
}
477477
}
478478
} yields {
479-
"Unique; substitution [?0 := !1], lifetime constraints []"
479+
"Unique; substitution [?0 := !1_0], lifetime constraints []"
480480
}
481481

482482
goal {
@@ -506,7 +506,7 @@ fn normalize_basic() {
506506
}
507507
}
508508
} yields {
509-
"Unique; substitution [?0 := (Iterator::Item)<!1>]"
509+
"Unique; substitution [?0 := (Iterator::Item)<!1_0>]"
510510
}
511511

512512
goal {
@@ -518,7 +518,7 @@ fn normalize_basic() {
518518
}
519519
}
520520
} yields {
521-
"Unique; substitution [?0 := (Iterator::Item)<!1>]"
521+
"Unique; substitution [?0 := (Iterator::Item)<!1_0>]"
522522
}
523523

524524
goal {
@@ -581,7 +581,7 @@ fn normalize_gat1() {
581581
}
582582
}
583583
} yields {
584-
"Unique; substitution [?0 := Iter<'!2_0, !1>], lifetime constraints []"
584+
"Unique; substitution [?0 := Iter<'!2_0, !1_0>], lifetime constraints []"
585585
}
586586
}
587587
}
@@ -606,7 +606,7 @@ fn normalize_gat2() {
606606
}
607607
}
608608
} yields {
609-
"Unique; substitution [?0 := Span<'!1_0, !2>], lifetime constraints []"
609+
"Unique; substitution [?0 := Span<'!1_0, !1_1>], lifetime constraints []"
610610
}
611611

612612
goal {
@@ -664,7 +664,7 @@ fn normalize_gat_with_where_clause() {
664664
}
665665
}
666666
} yields {
667-
"Unique; substitution [?0 := Value<!1>]"
667+
"Unique; substitution [?0 := Value<!1_0>]"
668668
}
669669
}
670670
}
@@ -703,7 +703,7 @@ fn normalize_gat_with_where_clause2() {
703703
}
704704
}
705705
} yields {
706-
"Unique; substitution [?0 := !2]"
706+
"Unique; substitution [?0 := !1_1]"
707707
}
708708
}
709709
}

0 commit comments

Comments
 (0)