Skip to content

Commit 69007bd

Browse files
committed
Implement "lifetime juggling" methods from chalk integration trait
Fixes #55097.
1 parent 9b87f59 commit 69007bd

File tree

3 files changed

+81
-11
lines changed

3 files changed

+81
-11
lines changed

src/librustc/traits/mod.rs

+13-1
Original file line numberDiff line numberDiff line change
@@ -1164,14 +1164,26 @@ where
11641164
) -> bool;
11651165
}
11661166

1167-
pub trait ExClauseLift<'tcx>
1167+
pub trait ChalkContextLift<'tcx>
11681168
where
11691169
Self: chalk_engine::context::Context + Clone,
11701170
{
11711171
type LiftedExClause: Debug + 'tcx;
1172+
type LiftedDelayedLiteral: Debug + 'tcx;
1173+
type LiftedLiteral: Debug + 'tcx;
11721174

11731175
fn lift_ex_clause_to_tcx<'a, 'gcx>(
11741176
ex_clause: &chalk_engine::ExClause<Self>,
11751177
tcx: TyCtxt<'a, 'gcx, 'tcx>,
11761178
) -> Option<Self::LiftedExClause>;
1179+
1180+
fn lift_delayed_literal_to_tcx<'a, 'gcx>(
1181+
ex_clause: &chalk_engine::DelayedLiteral<Self>,
1182+
tcx: TyCtxt<'a, 'gcx, 'tcx>,
1183+
) -> Option<Self::LiftedDelayedLiteral>;
1184+
1185+
fn lift_literal_to_tcx<'a, 'gcx>(
1186+
ex_clause: &chalk_engine::Literal<Self>,
1187+
tcx: TyCtxt<'a, 'gcx, 'tcx>,
1188+
) -> Option<Self::LiftedLiteral>;
11771189
}

src/librustc/traits/structural_impls.rs

+26-2
Original file line numberDiff line numberDiff line change
@@ -700,12 +700,36 @@ impl<'a, 'tcx, G: Lift<'tcx>> Lift<'tcx> for traits::InEnvironment<'a, G> {
700700
impl<'tcx, C> Lift<'tcx> for chalk_engine::ExClause<C>
701701
where
702702
C: chalk_engine::context::Context + Clone,
703-
C: traits::ExClauseLift<'tcx>,
703+
C: traits::ChalkContextLift<'tcx>,
704704
{
705705
type Lifted = C::LiftedExClause;
706706

707707
fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
708-
<C as traits::ExClauseLift>::lift_ex_clause_to_tcx(self, tcx)
708+
<C as traits::ChalkContextLift>::lift_ex_clause_to_tcx(self, tcx)
709+
}
710+
}
711+
712+
impl<'tcx, C> Lift<'tcx> for chalk_engine::DelayedLiteral<C>
713+
where
714+
C: chalk_engine::context::Context + Clone,
715+
C: traits::ChalkContextLift<'tcx>,
716+
{
717+
type Lifted = C::LiftedDelayedLiteral;
718+
719+
fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
720+
<C as traits::ChalkContextLift>::lift_delayed_literal_to_tcx(self, tcx)
721+
}
722+
}
723+
724+
impl<'tcx, C> Lift<'tcx> for chalk_engine::Literal<C>
725+
where
726+
C: chalk_engine::context::Context + Clone,
727+
C: traits::ChalkContextLift<'tcx>,
728+
{
729+
type Lifted = C::LiftedLiteral;
730+
731+
fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
732+
<C as traits::ChalkContextLift>::lift_literal_to_tcx(self, tcx)
709733
}
710734
}
711735

src/librustc_traits/chalk_context/mod.rs

+42-8
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ use rustc::infer::canonical::{
2121
use rustc::traits::{
2222
DomainGoal,
2323
ExClauseFold,
24-
ExClauseLift,
24+
ChalkContextLift,
2525
Goal,
2626
GoalKind,
2727
Clause,
@@ -441,9 +441,12 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
441441

442442
fn lift_delayed_literal(
443443
&self,
444-
_value: DelayedLiteral<ChalkArenas<'tcx>>,
444+
value: DelayedLiteral<ChalkArenas<'tcx>>,
445445
) -> DelayedLiteral<ChalkArenas<'gcx>> {
446-
panic!("lift")
446+
match self.infcx.tcx.lift_to_global(&value) {
447+
Some(literal) => literal,
448+
None => bug!("cannot lift {:?}", value),
449+
}
447450
}
448451

449452
fn into_ex_clause(
@@ -478,14 +481,45 @@ impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
478481
}
479482
}
480483

481-
impl ExClauseLift<'gcx> for ChalkArenas<'a> {
482-
type LiftedExClause = ChalkExClause<'gcx>;
484+
impl ChalkContextLift<'tcx> for ChalkArenas<'a> {
485+
type LiftedExClause = ChalkExClause<'tcx>;
486+
type LiftedDelayedLiteral = DelayedLiteral<ChalkArenas<'tcx>>;
487+
type LiftedLiteral = Literal<ChalkArenas<'tcx>>;
483488

484489
fn lift_ex_clause_to_tcx(
485-
_ex_clause: &ChalkExClause<'a>,
486-
_tcx: TyCtxt<'_, '_, 'tcx>,
490+
ex_clause: &ChalkExClause<'a>,
491+
tcx: TyCtxt<'_, 'gcx, 'tcx>
487492
) -> Option<Self::LiftedExClause> {
488-
panic!()
493+
Some(ChalkExClause {
494+
subst: tcx.lift(&ex_clause.subst)?,
495+
delayed_literals: tcx.lift(&ex_clause.delayed_literals)?,
496+
constraints: tcx.lift(&ex_clause.constraints)?,
497+
subgoals: tcx.lift(&ex_clause.subgoals)?,
498+
})
499+
}
500+
501+
fn lift_delayed_literal_to_tcx(
502+
literal: &DelayedLiteral<ChalkArenas<'a>>,
503+
tcx: TyCtxt<'_, 'gcx, 'tcx>
504+
) -> Option<Self::LiftedDelayedLiteral> {
505+
Some(match literal {
506+
DelayedLiteral::CannotProve(()) => DelayedLiteral::CannotProve(()),
507+
DelayedLiteral::Negative(index) => DelayedLiteral::Negative(*index),
508+
DelayedLiteral::Positive(index, subst) => DelayedLiteral::Positive(
509+
*index,
510+
tcx.lift(subst)?
511+
)
512+
})
513+
}
514+
515+
fn lift_literal_to_tcx(
516+
literal: &Literal<ChalkArenas<'a>>,
517+
tcx: TyCtxt<'_, 'gcx, 'tcx>,
518+
) -> Option<Self::LiftedLiteral> {
519+
Some(match literal {
520+
Literal::Negative(goal) => Literal::Negative(tcx.lift(goal)?),
521+
Literal::Positive(goal) => Literal::Positive(tcx.lift(goal)?),
522+
})
489523
}
490524
}
491525

0 commit comments

Comments
 (0)