Skip to content

Commit ad91883

Browse files
leoyvensnikomatsakis
leoyvens
authored and
nikomatsakis
committed
add UniversalIndex and use it in Lifetime::ForAll
Compiles and tests but isn't ready for multiple lifetimes yet
1 parent 8b7284b commit ad91883

File tree

11 files changed

+43
-32
lines changed

11 files changed

+43
-32
lines changed

‎chalk-ir/src/debug.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -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: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -349,7 +349,7 @@ pub fn super_fold_lifetime(
349349
} else {
350350
Ok(Lifetime::Var(depth))
351351
},
352-
Lifetime::ForAll(universe) => folder.fold_free_universal_lifetime(universe, binders),
352+
Lifetime::ForAll(universe) => folder.fold_free_universal_lifetime(universe.ui, binders),
353353
}
354354
}
355355

‎chalk-ir/src/lib.rs

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,7 @@ impl UniverseIndex {
135135
}
136136

137137
pub fn to_lifetime(self) -> Lifetime {
138-
Lifetime::ForAll(self)
138+
Lifetime::ForAll(UniversalIndex { ui: self, idx: 0 })
139139
}
140140

141141
pub fn next(self) -> UniverseIndex {
@@ -206,7 +206,18 @@ pub struct QuantifiedTy {
206206
pub enum Lifetime {
207207
/// See Ty::Var(_).
208208
Var(usize),
209-
ForAll(UniverseIndex),
209+
ForAll(UniversalIndex),
210+
}
211+
212+
/// Index of an universally quantified parameter in the environment.
213+
/// Two indexes are required, the one of the universe itself
214+
/// and the relative index inside the universe.
215+
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
216+
pub struct UniversalIndex {
217+
/// Index *of* the universe.
218+
pub ui: UniverseIndex,
219+
/// Index *in* the universe.
220+
pub idx: usize,
210221
}
211222

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

‎chalk-ir/src/macros.rs

Lines changed: 1 addition & 1 deletion
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) => {

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ impl InferenceTable {
106106
let new_universe = self.new_universe();
107107
match *pk {
108108
ParameterKind::Lifetime(()) => {
109-
let lt = Lifetime::ForAll(new_universe);
109+
let lt = Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 });
110110
ParameterKind::Lifetime(lt)
111111
}
112112
ParameterKind::Ty(()) => ParameterKind::Ty(Ty::Apply(ApplicationTy {

‎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/unify.rs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ impl<'t> Unifier<'t> {
178178
let lifetimes1: Vec<_> = (0..ty1.num_binders)
179179
.map(|_| {
180180
let new_universe = self.table.new_universe();
181-
Lifetime::ForAll(new_universe).cast()
181+
Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 }).cast()
182182
})
183183
.collect();
184184

@@ -242,7 +242,7 @@ impl<'t> Unifier<'t> {
242242
let lifetimes1: Vec<_> = (0..ty1.num_binders)
243243
.map(|_| {
244244
let new_universe = self.table.new_universe();
245-
Lifetime::ForAll(new_universe).cast()
245+
Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 }).cast()
246246
})
247247
.collect();
248248

@@ -294,16 +294,16 @@ impl<'t> Unifier<'t> {
294294
Ok(())
295295
}
296296

297-
(&Lifetime::Var(depth), &Lifetime::ForAll(ui))
298-
| (&Lifetime::ForAll(ui), &Lifetime::Var(depth)) => {
297+
(&Lifetime::Var(depth), &Lifetime::ForAll(idx))
298+
| (&Lifetime::ForAll(idx), &Lifetime::Var(depth)) => {
299299
let var = InferenceVariable::from_depth(depth);
300300
let var_ui = self.table.universe_of_unbound_var(var);
301-
if var_ui.can_see(ui) {
301+
if var_ui.can_see(idx.ui) {
302302
debug!(
303303
"unify_lifetime_lifetime: {:?} in {:?} can see {:?}; unifying",
304-
var, var_ui, ui
304+
var, var_ui, idx.ui
305305
);
306-
let v = Lifetime::ForAll(ui);
306+
let v = Lifetime::ForAll(idx);
307307
self.table
308308
.unify
309309
.unify_var_value(var, InferenceValue::from(v))
@@ -312,7 +312,7 @@ impl<'t> Unifier<'t> {
312312
} else {
313313
debug!(
314314
"unify_lifetime_lifetime: {:?} in {:?} cannot see {:?}; pushing constraint",
315-
var, var_ui, ui
315+
var, var_ui, idx.ui
316316
);
317317
Ok(self.push_lifetime_eq_constraint(*a, *b))
318318
}

‎chalk-solve/src/solve/slg/implementation/aggregate.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -320,8 +320,8 @@ impl<'infer> AntiUnifier<'infer> {
320320
match (l1, l2) {
321321
(Lifetime::Var(_), _) | (_, Lifetime::Var(_)) => self.new_lifetime_variable(),
322322

323-
(Lifetime::ForAll(ui1), Lifetime::ForAll(ui2)) => if ui1 == ui2 {
324-
Lifetime::ForAll(*ui1)
323+
(Lifetime::ForAll(_), Lifetime::ForAll(_)) => if l1 == l2 {
324+
*l1
325325
} else {
326326
self.new_lifetime_variable()
327327
},

‎chalk-solve/src/solve/slg/implementation/resolvent.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -388,8 +388,8 @@ impl<'t> Zipper for AnswerSubstitutor<'t> {
388388
self.assert_matching_vars(*answer_depth, *pending_depth)
389389
}
390390

391-
(Lifetime::ForAll(answer_ui), Lifetime::ForAll(pending_ui)) => {
392-
assert_eq!(answer_ui, pending_ui);
391+
(Lifetime::ForAll(_), Lifetime::ForAll(_)) => {
392+
assert_eq!(answer, pending);
393393
Ok(())
394394
}
395395

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -550,7 +550,7 @@ fn basic_region_constraint_from_positive_impl() {
550550
constraints: [
551551
InEnvironment {
552552
environment: Env([]),
553-
goal: '!2 == '!1
553+
goal: '!2'0 == '!1'0
554554
}
555555
]
556556
},

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

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -581,7 +581,7 @@ fn normalize_gat1() {
581581
}
582582
}
583583
} yields {
584-
"Unique; substitution [?0 := Iter<'!2, !1>], lifetime constraints []"
584+
"Unique; substitution [?0 := Iter<'!2'0, !1>], lifetime constraints []"
585585
}
586586
}
587587
}
@@ -606,7 +606,7 @@ fn normalize_gat2() {
606606
}
607607
}
608608
} yields {
609-
"Unique; substitution [?0 := Span<'!1, !2>], lifetime constraints []"
609+
"Unique; substitution [?0 := Span<'!1'0, !2>], lifetime constraints []"
610610
}
611611

612612
goal {
@@ -922,7 +922,7 @@ fn region_equality() {
922922
} yields {
923923
"Unique; substitution [],
924924
lifetime constraints \
925-
[InEnvironment { environment: Env([]), goal: '!2 == '!1 }]
925+
[InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }]
926926
"
927927
}
928928

@@ -933,7 +933,7 @@ fn region_equality() {
933933
}
934934
}
935935
} yields {
936-
"Unique; substitution [?0 := '!1], lifetime constraints []"
936+
"Unique; substitution [?0 := '!1'0], lifetime constraints []"
937937
}
938938
}
939939
}
@@ -971,7 +971,7 @@ fn forall_equality() {
971971
for<'c, 'd> Ref<'c, Ref<'d, Ref<'d, Unit>>>>
972972
} yields {
973973
"Unique; substitution [], lifetime constraints [
974-
InEnvironment { environment: Env([]), goal: '!2 == '!1 }
974+
InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }
975975
]"
976976
}
977977
}
@@ -1185,7 +1185,7 @@ fn normalize_under_binder() {
11851185
}
11861186
}
11871187
} yields {
1188-
"Unique; substitution [?0 := Ref<'!1, I32>], lifetime constraints []"
1188+
"Unique; substitution [?0 := Ref<'!1'0, I32>], lifetime constraints []"
11891189
}
11901190

11911191
goal {
@@ -1197,7 +1197,7 @@ fn normalize_under_binder() {
11971197
} yields {
11981198
"Unique; for<?U0> { \
11991199
substitution [?0 := Ref<'?0, I32>], \
1200-
lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1 }] \
1200+
lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \
12011201
}"
12021202
}
12031203
}
@@ -1221,7 +1221,7 @@ fn unify_quantified_lifetimes() {
12211221
} yields {
12221222
"Unique; for<?U0> { \
12231223
substitution [?0 := '?0], \
1224-
lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1 }] \
1224+
lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \
12251225
}"
12261226
}
12271227

@@ -1237,8 +1237,8 @@ fn unify_quantified_lifetimes() {
12371237
}
12381238
} yields {
12391239
"Unique; for<?U0> { \
1240-
substitution [?0 := '?0, ?1 := '!1], \
1241-
lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1 }] \
1240+
substitution [?0 := '?0, ?1 := '!1'0], \
1241+
lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \
12421242
}"
12431243
}
12441244
}
@@ -1263,7 +1263,7 @@ fn equality_binder() {
12631263
} yields {
12641264
"Unique; for<?U1> { \
12651265
substitution [?0 := '?0], \
1266-
lifetime constraints [InEnvironment { environment: Env([]), goal: '!2 == '?0 }] \
1266+
lifetime constraints [InEnvironment { environment: Env([]), goal: '!2'0 == '?0 }] \
12671267
}"
12681268
}
12691269
}
@@ -2394,7 +2394,7 @@ fn quantified_types() {
23942394
} yields {
23952395
// Lifetime constraints are unsatisfiable
23962396
"Unique; substitution [], \
2397-
lifetime constraints [InEnvironment { environment: Env([]), goal: '!2 == '!1 }]"
2397+
lifetime constraints [InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }]"
23982398
}
23992399
}
24002400
}

0 commit comments

Comments
 (0)