Implement "lifetime juggling" methods from chalk integration trait
Fixes #55097.
This commit is contained in:
parent
9b87f590dc
commit
69007bd660
@ -1164,14 +1164,26 @@ where
|
||||
) -> bool;
|
||||
}
|
||||
|
||||
pub trait ExClauseLift<'tcx>
|
||||
pub trait ChalkContextLift<'tcx>
|
||||
where
|
||||
Self: chalk_engine::context::Context + Clone,
|
||||
{
|
||||
type LiftedExClause: Debug + 'tcx;
|
||||
type LiftedDelayedLiteral: Debug + 'tcx;
|
||||
type LiftedLiteral: Debug + 'tcx;
|
||||
|
||||
fn lift_ex_clause_to_tcx<'a, 'gcx>(
|
||||
ex_clause: &chalk_engine::ExClause<Self>,
|
||||
tcx: TyCtxt<'a, 'gcx, 'tcx>,
|
||||
) -> Option<Self::LiftedExClause>;
|
||||
|
||||
fn lift_delayed_literal_to_tcx<'a, 'gcx>(
|
||||
ex_clause: &chalk_engine::DelayedLiteral<Self>,
|
||||
tcx: TyCtxt<'a, 'gcx, 'tcx>,
|
||||
) -> Option<Self::LiftedDelayedLiteral>;
|
||||
|
||||
fn lift_literal_to_tcx<'a, 'gcx>(
|
||||
ex_clause: &chalk_engine::Literal<Self>,
|
||||
tcx: TyCtxt<'a, 'gcx, 'tcx>,
|
||||
) -> Option<Self::LiftedLiteral>;
|
||||
}
|
||||
|
@ -700,12 +700,36 @@ impl<'a, 'tcx, G: Lift<'tcx>> Lift<'tcx> for traits::InEnvironment<'a, G> {
|
||||
impl<'tcx, C> Lift<'tcx> for chalk_engine::ExClause<C>
|
||||
where
|
||||
C: chalk_engine::context::Context + Clone,
|
||||
C: traits::ExClauseLift<'tcx>,
|
||||
C: traits::ChalkContextLift<'tcx>,
|
||||
{
|
||||
type Lifted = C::LiftedExClause;
|
||||
|
||||
fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
|
||||
<C as traits::ExClauseLift>::lift_ex_clause_to_tcx(self, tcx)
|
||||
<C as traits::ChalkContextLift>::lift_ex_clause_to_tcx(self, tcx)
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx, C> Lift<'tcx> for chalk_engine::DelayedLiteral<C>
|
||||
where
|
||||
C: chalk_engine::context::Context + Clone,
|
||||
C: traits::ChalkContextLift<'tcx>,
|
||||
{
|
||||
type Lifted = C::LiftedDelayedLiteral;
|
||||
|
||||
fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
|
||||
<C as traits::ChalkContextLift>::lift_delayed_literal_to_tcx(self, tcx)
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx, C> Lift<'tcx> for chalk_engine::Literal<C>
|
||||
where
|
||||
C: chalk_engine::context::Context + Clone,
|
||||
C: traits::ChalkContextLift<'tcx>,
|
||||
{
|
||||
type Lifted = C::LiftedLiteral;
|
||||
|
||||
fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
|
||||
<C as traits::ChalkContextLift>::lift_literal_to_tcx(self, tcx)
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -21,7 +21,7 @@ use rustc::infer::canonical::{
|
||||
use rustc::traits::{
|
||||
DomainGoal,
|
||||
ExClauseFold,
|
||||
ExClauseLift,
|
||||
ChalkContextLift,
|
||||
Goal,
|
||||
GoalKind,
|
||||
Clause,
|
||||
@ -441,9 +441,12 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
|
||||
fn lift_delayed_literal(
|
||||
&self,
|
||||
_value: DelayedLiteral<ChalkArenas<'tcx>>,
|
||||
value: DelayedLiteral<ChalkArenas<'tcx>>,
|
||||
) -> DelayedLiteral<ChalkArenas<'gcx>> {
|
||||
panic!("lift")
|
||||
match self.infcx.tcx.lift_to_global(&value) {
|
||||
Some(literal) => literal,
|
||||
None => bug!("cannot lift {:?}", value),
|
||||
}
|
||||
}
|
||||
|
||||
fn into_ex_clause(
|
||||
@ -478,14 +481,45 @@ impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
|
||||
}
|
||||
}
|
||||
|
||||
impl ExClauseLift<'gcx> for ChalkArenas<'a> {
|
||||
type LiftedExClause = ChalkExClause<'gcx>;
|
||||
impl ChalkContextLift<'tcx> for ChalkArenas<'a> {
|
||||
type LiftedExClause = ChalkExClause<'tcx>;
|
||||
type LiftedDelayedLiteral = DelayedLiteral<ChalkArenas<'tcx>>;
|
||||
type LiftedLiteral = Literal<ChalkArenas<'tcx>>;
|
||||
|
||||
fn lift_ex_clause_to_tcx(
|
||||
_ex_clause: &ChalkExClause<'a>,
|
||||
_tcx: TyCtxt<'_, '_, 'tcx>,
|
||||
ex_clause: &ChalkExClause<'a>,
|
||||
tcx: TyCtxt<'_, 'gcx, 'tcx>
|
||||
) -> Option<Self::LiftedExClause> {
|
||||
panic!()
|
||||
Some(ChalkExClause {
|
||||
subst: tcx.lift(&ex_clause.subst)?,
|
||||
delayed_literals: tcx.lift(&ex_clause.delayed_literals)?,
|
||||
constraints: tcx.lift(&ex_clause.constraints)?,
|
||||
subgoals: tcx.lift(&ex_clause.subgoals)?,
|
||||
})
|
||||
}
|
||||
|
||||
fn lift_delayed_literal_to_tcx(
|
||||
literal: &DelayedLiteral<ChalkArenas<'a>>,
|
||||
tcx: TyCtxt<'_, 'gcx, 'tcx>
|
||||
) -> Option<Self::LiftedDelayedLiteral> {
|
||||
Some(match literal {
|
||||
DelayedLiteral::CannotProve(()) => DelayedLiteral::CannotProve(()),
|
||||
DelayedLiteral::Negative(index) => DelayedLiteral::Negative(*index),
|
||||
DelayedLiteral::Positive(index, subst) => DelayedLiteral::Positive(
|
||||
*index,
|
||||
tcx.lift(subst)?
|
||||
)
|
||||
})
|
||||
}
|
||||
|
||||
fn lift_literal_to_tcx(
|
||||
literal: &Literal<ChalkArenas<'a>>,
|
||||
tcx: TyCtxt<'_, 'gcx, 'tcx>,
|
||||
) -> Option<Self::LiftedLiteral> {
|
||||
Some(match literal {
|
||||
Literal::Negative(goal) => Literal::Negative(tcx.lift(goal)?),
|
||||
Literal::Positive(goal) => Literal::Positive(tcx.lift(goal)?),
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user