Skip to content

Commit 0054e1c

Browse files
matthewjaspermatthewjasper
committed
Add empty and erased regions
1 parent f2e3fd9 commit 0054e1c

File tree

14 files changed

+272
-88
lines changed

14 files changed

+272
-88
lines changed

‎chalk-engine/src/slg/resolvent.rs

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -506,7 +506,9 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
506506
}
507507

508508
(LifetimeData::Static, LifetimeData::Static)
509-
| (LifetimeData::Placeholder(_), LifetimeData::Placeholder(_)) => {
509+
| (LifetimeData::Placeholder(_), LifetimeData::Placeholder(_))
510+
| (LifetimeData::Erased, LifetimeData::Erased)
511+
| (LifetimeData::Empty(_), LifetimeData::Empty(_)) => {
510512
assert_eq!(answer, pending);
511513
Ok(())
512514
}
@@ -518,12 +520,14 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
518520

519521
(LifetimeData::Static, _)
520522
| (LifetimeData::BoundVar(_), _)
521-
| (LifetimeData::Placeholder(_), _) => panic!(
523+
| (LifetimeData::Placeholder(_), _)
524+
| (LifetimeData::Erased, _)
525+
| (LifetimeData::Empty(_), _) => panic!(
522526
"structural mismatch between answer `{:?}` and pending goal `{:?}`",
523527
answer, pending,
524528
),
525529

526-
(LifetimeData::Phantom(..), _) => unreachable!(),
530+
(LifetimeData::Phantom(void, _), _) => match *void {},
527531
}
528532
}
529533

‎chalk-integration/src/lowering.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -866,6 +866,14 @@ impl LowerWithEnv for Lifetime {
866866
interner,
867867
chalk_ir::LifetimeData::Static,
868868
)),
869+
Lifetime::Empty => Ok(chalk_ir::Lifetime::new(
870+
interner,
871+
chalk_ir::LifetimeData::Empty(chalk_ir::UniverseIndex { counter: 0 }),
872+
)),
873+
Lifetime::Erased => Ok(chalk_ir::Lifetime::new(
874+
interner,
875+
chalk_ir::LifetimeData::Erased,
876+
)),
869877
}
870878
}
871879
}

‎chalk-ir/src/debug.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -280,6 +280,9 @@ impl<I: Interner> Debug for LifetimeData<I> {
280280
LifetimeData::InferenceVar(var) => write!(fmt, "'{:?}", var),
281281
LifetimeData::Placeholder(index) => write!(fmt, "'{:?}", index),
282282
LifetimeData::Static => write!(fmt, "'static"),
283+
LifetimeData::Empty(UniverseIndex::ROOT) => write!(fmt, "'<empty>"),
284+
LifetimeData::Empty(universe) => write!(fmt, "'<empty:{:?}>", universe),
285+
LifetimeData::Erased => write!(fmt, "'<erased>"),
283286
LifetimeData::Phantom(..) => unreachable!(),
284287
}
285288
}

‎chalk-ir/src/fold.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -523,7 +523,9 @@ where
523523
folder.fold_free_placeholder_lifetime(*universe, outer_binder)
524524
}
525525
LifetimeData::Static => Ok(LifetimeData::<I>::Static.intern(folder.interner())),
526-
LifetimeData::Phantom(..) => unreachable!(),
526+
LifetimeData::Empty(ui) => Ok(LifetimeData::<I>::Empty(*ui).intern(folder.interner())),
527+
LifetimeData::Erased => Ok(LifetimeData::<I>::Erased.intern(folder.interner())),
528+
LifetimeData::Phantom(void, ..) => match *void {},
527529
}
528530
}
529531
}

‎chalk-ir/src/lib.rs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1055,6 +1055,8 @@ impl<I: Interner> Lifetime<I> {
10551055
LifetimeData::InferenceVar(_) => false,
10561056
LifetimeData::Placeholder(_) => false,
10571057
LifetimeData::Static => false,
1058+
LifetimeData::Empty(_) => false,
1059+
LifetimeData::Erased => false,
10581060
LifetimeData::Phantom(..) => unreachable!(),
10591061
}
10601062
}
@@ -1071,6 +1073,14 @@ pub enum LifetimeData<I: Interner> {
10711073
Placeholder(PlaceholderIndex),
10721074
/// Static lifetime
10731075
Static,
1076+
/// An empty lifetime: a lifetime shorter than any other lifetime in a
1077+
/// universe with a lesser or equal index. The universe only non-zero in
1078+
/// lexical region resolve in rustc, so chalk shouldn't ever see a non-zero
1079+
/// index.
1080+
Empty(UniverseIndex),
1081+
/// An erased lifetime, used by rustc to improve caching when we doesn't
1082+
/// care about lifetimes
1083+
Erased,
10741084
/// Lifetime on phantom data.
10751085
Phantom(Void, PhantomData<I>),
10761086
}

‎chalk-ir/src/visit.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -380,8 +380,10 @@ impl<I: Interner> SuperVisit<I> for Lifetime<I> {
380380
LifetimeData::Placeholder(universe) => {
381381
visitor.visit_free_placeholder(*universe, outer_binder)
382382
}
383-
LifetimeData::Static => ControlFlow::CONTINUE,
384-
LifetimeData::Phantom(..) => unreachable!(),
383+
LifetimeData::Static | LifetimeData::Empty(_) | LifetimeData::Erased => {
384+
ControlFlow::CONTINUE
385+
}
386+
LifetimeData::Phantom(void, ..) => match *void {},
385387
}
386388
}
387389
}

‎chalk-parse/src/ast.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -370,6 +370,8 @@ impl Default for Safety {
370370
pub enum Lifetime {
371371
Id { name: Identifier },
372372
Static,
373+
Erased,
374+
Empty,
373375
}
374376

375377
#[derive(Clone, PartialEq, Eq, Debug)]

‎chalk-parse/src/parser.lalrpop

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ WellKnownTrait: WellKnownTrait = {
6363
"#" "[" "lang" "(" "fn_mut" ")" "]" => WellKnownTrait::FnMut,
6464
"#" "[" "lang" "(" "fn" ")" "]" => WellKnownTrait::Fn,
6565
"#" "[" "lang" "(" "unsize" ")" "]" => WellKnownTrait::Unsize,
66-
"#" "[" "lang" "(" "unpin" ")" "]" => WellKnownTrait::Unpin,
66+
"#" "[" "lang" "(" "unpin" ")" "]" => WellKnownTrait::Unpin,
6767
"#" "[" "lang" "(" "coerce_unsized" ")" "]" => WellKnownTrait::CoerceUnsized,
6868
};
6969

@@ -432,6 +432,8 @@ RawMutability: Mutability = {
432432
Lifetime: Lifetime = {
433433
<n:LifetimeId> => Lifetime::Id { name: n },
434434
"'static" => Lifetime::Static,
435+
"'erased" => Lifetime::Erased,
436+
"'empty" => Lifetime::Empty,
435437
};
436438

437439
ConstWithoutId: Const = {

‎chalk-solve/src/display/ty.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -240,6 +240,8 @@ impl<I: Interner> RenderAsRust<I> for LifetimeData<I> {
240240
write!(f, "'_placeholder_{}_{}", ix.ui.counter, ix.idx)
241241
}
242242
LifetimeData::Static => write!(f, "'static"),
243+
LifetimeData::Empty(_) => write!(f, "'<empty>"),
244+
LifetimeData::Erased => write!(f, "'_"),
243245
// Matching the void ensures at compile time that this code is
244246
// unreachable
245247
LifetimeData::Phantom(void, _) => match *void {},

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

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
use crate::debug_span;
22
use chalk_ir::fold::shift::Shift;
3-
use chalk_ir::fold::{Fold, Folder};
3+
use chalk_ir::fold::{Fold, Folder, SuperFold};
44
use chalk_ir::interner::{HasInterner, Interner};
55
use chalk_ir::*;
66
use std::cmp::max;
@@ -237,6 +237,21 @@ where
237237
}
238238
}
239239

240+
fn fold_lifetime(
241+
&mut self,
242+
lifetime: &Lifetime<I>,
243+
outer_binder: DebruijnIndex,
244+
) -> Fallible<Lifetime<I>> {
245+
match *lifetime.data(self.interner) {
246+
LifetimeData::Empty(ui) if ui.counter != 0 => {
247+
// ReEmpty in non-root universes is only used by lexical region
248+
// inference. We shouldn't see it in canonicalization.
249+
panic!("Cannot canonicalize ReEmpty in non-root universe")
250+
}
251+
_ => lifetime.super_fold_with(self, outer_binder),
252+
}
253+
}
254+
240255
fn interner(&self) -> &'i I {
241256
self.interner
242257
}

0 commit comments

Comments
 (0)