Skip to content

Commit 0435fc2

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #149 from leodasvacas/many-lifetimes-one-universe
Many lifetimes one universe
2 parents 8b7284b + 8440ed8 commit 0435fc2

File tree

16 files changed

+147
-129
lines changed

16 files changed

+147
-129
lines changed

‎chalk-ir/src/debug.rs

Lines changed: 2 additions & 2 deletions
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
}
@@ -60,7 +60,7 @@ impl Debug for Lifetime {
6060
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
6161
match self {
6262
Lifetime::Var(depth) => write!(fmt, "'?{}", depth),
63-
Lifetime::ForAll(universe) => write!(fmt, "'!{}", universe.counter),
63+
Lifetime::ForAll(UniversalIndex { ui, idx }) => write!(fmt, "'!{}_{}", ui.counter, idx),
6464
}
6565
}
6666
}

‎chalk-ir/src/fold.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -135,12 +135,12 @@ 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(
142142
&mut self,
143-
universe: UniverseIndex,
143+
universe: UniversalIndex,
144144
binders: usize,
145145
) -> Fallible<Lifetime>;
146146
}
@@ -151,13 +151,13 @@ 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(
159159
&mut self,
160-
universe: UniverseIndex,
160+
universe: UniversalIndex,
161161
_binders: usize,
162162
) -> Fallible<Lifetime> {
163163
Ok(universe.to_lifetime())

‎chalk-ir/src/lib.rs

Lines changed: 26 additions & 15 deletions
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:
@@ -134,10 +125,6 @@ impl UniverseIndex {
134125
self.counter >= ui.counter
135126
}
136127

137-
pub fn to_lifetime(self) -> Lifetime {
138-
Lifetime::ForAll(self)
139-
}
140-
141128
pub fn next(self) -> UniverseIndex {
142129
UniverseIndex {
143130
counter: self.counter + 1,
@@ -206,7 +193,31 @@ pub struct QuantifiedTy {
206193
pub enum Lifetime {
207194
/// See Ty::Var(_).
208195
Var(usize),
209-
ForAll(UniverseIndex),
196+
ForAll(UniversalIndex),
197+
}
198+
199+
/// Index of an universally quantified parameter in the environment.
200+
/// Two indexes are required, the one of the universe itself
201+
/// and the relative index inside the universe.
202+
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
203+
pub struct UniversalIndex {
204+
/// Index *of* the universe.
205+
pub ui: UniverseIndex,
206+
/// Index *in* the universe.
207+
pub idx: usize,
208+
}
209+
210+
impl UniversalIndex {
211+
pub fn to_lifetime(self) -> Lifetime {
212+
Lifetime::ForAll(self)
213+
}
214+
215+
pub fn to_ty(self) -> Ty {
216+
Ty::Apply(ApplicationTy {
217+
name: TypeName::ForAll(self),
218+
parameters: vec![],
219+
})
220+
}
210221
}
211222

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

‎chalk-ir/src/macros.rs

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ macro_rules! lifetime {
5454
};
5555

5656
(skol $b:expr) => {
57-
$crate::Lifetime::ForAll(UniverseIndex { counter: $b })
57+
$crate::Lifetime::ForAll(UniversalIndex { ui: UniverseIndex { counter: $b }, idx: 0})
5858
};
5959

6060
(expr $b:expr) => {
@@ -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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -94,17 +94,17 @@ 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(
103103
&mut self,
104-
universe: UniverseIndex,
104+
universe: UniversalIndex,
105105
_binders: usize,
106106
) -> Fallible<Lifetime> {
107-
self.max_universe = max(self.max_universe, universe);
107+
self.max_universe = max(self.max_universe, universe.ui);
108108
Ok(universe.to_lifetime())
109109
}
110110
}

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

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -100,19 +100,18 @@ impl InferenceTable {
100100
T: Fold,
101101
{
102102
let (binders, value) = arg.split();
103+
let ui = self.new_universe();
103104
let parameters: Vec<_> = binders
104105
.iter()
105-
.map(|pk| {
106-
let new_universe = self.new_universe();
106+
.enumerate()
107+
.map(|(idx, pk)| {
108+
let universal_idx = UniversalIndex { ui, idx };
107109
match *pk {
108110
ParameterKind::Lifetime(()) => {
109-
let lt = Lifetime::ForAll(new_universe);
111+
let lt = universal_idx.to_lifetime();
110112
ParameterKind::Lifetime(lt)
111113
}
112-
ParameterKind::Ty(()) => ParameterKind::Ty(Ty::Apply(ApplicationTy {
113-
name: TypeName::ForAll(new_universe),
114-
parameters: vec![],
115-
})),
114+
ParameterKind::Ty(()) => ParameterKind::Ty(universal_idx.to_ty()),
116115
}
117116
})
118117
.collect();

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -97,8 +97,8 @@ impl InferenceTable {
9797

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

104104
impl<'q> Inverter<'q> {
@@ -114,27 +114,27 @@ 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
)
126126
}
127127

128128
fn fold_free_universal_lifetime(
129129
&mut self,
130-
universe: UniverseIndex,
130+
universe: UniversalIndex,
131131
binders: usize,
132132
) -> Fallible<Lifetime> {
133133
let table = &mut self.table;
134134
Ok(
135135
self.inverted_lifetime
136136
.entry(universe)
137-
.or_insert_with(|| table.new_variable(universe))
137+
.or_insert_with(|| table.new_variable(universe.ui))
138138
.to_lifetime()
139139
.shifted_in(binders),
140140
)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -294,6 +294,6 @@ fn lifetime_constraint_indirect() {
294294
assert_eq!(constraints.len(), 1);
295295
assert_eq!(
296296
format!("{:?}", constraints[0]),
297-
"InEnvironment { environment: Env([]), goal: \'?2 == \'!1 }",
297+
"InEnvironment { environment: Env([]), goal: \'?2 == \'!1_0 }",
298298
);
299299
}

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

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -220,17 +220,17 @@ 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(
229229
&mut self,
230-
universe: UniverseIndex,
230+
universe: UniversalIndex,
231231
_binders: usize,
232232
) -> Fallible<Lifetime> {
233-
self.universes.add(universe);
233+
self.universes.add(universe.ui);
234234
Ok(universe.to_lifetime())
235235
}
236236
}
@@ -246,20 +246,20 @@ 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(
257257
&mut self,
258-
universe0: UniverseIndex,
258+
universe0: UniversalIndex,
259259
_binders: usize,
260260
) -> Fallible<Lifetime> {
261-
let universe = self.universes.map_universe_to_canonical(universe0);
262-
Ok(universe.to_lifetime())
261+
let universe = self.universes.map_universe_to_canonical(universe0.ui);
262+
Ok(UniversalIndex { ui: universe, idx: universe0.idx }.to_lifetime())
263263
}
264264
}
265265

@@ -274,20 +274,20 @@ 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(
285285
&mut self,
286-
universe0: UniverseIndex,
286+
universe0: UniversalIndex,
287287
_binders: usize,
288288
) -> Fallible<Lifetime> {
289-
let universe = self.universes.map_universe_from_canonical(universe0);
290-
Ok(universe.to_lifetime())
289+
let universe = self.universes.map_universe_from_canonical(universe0.ui);
290+
Ok(UniversalIndex { ui: universe, idx: universe0.idx }.to_lifetime())
291291
}
292292
}
293293

0 commit comments

Comments
 (0)