Skip to content

Commit

Permalink
Implement "lifetime juggling" methods from chalk integration trait
Browse files Browse the repository at this point in the history
Fixes #55097.
  • Loading branch information
scalexm committed Dec 27, 2018
1 parent 9b87f59 commit 69007bd
Show file tree
Hide file tree
Showing 3 changed files with 81 additions and 11 deletions.
14 changes: 13 additions & 1 deletion src/librustc/traits/mod.rs
Expand Up @@ -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>;
}
28 changes: 26 additions & 2 deletions src/librustc/traits/structural_impls.rs
Expand Up @@ -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)
}
}

Expand Down
50 changes: 42 additions & 8 deletions src/librustc_traits/chalk_context/mod.rs
Expand Up @@ -21,7 +21,7 @@ use rustc::infer::canonical::{
use rustc::traits::{
DomainGoal,
ExClauseFold,
ExClauseLift,
ChalkContextLift,
Goal,
GoalKind,
Clause,
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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)?),
})
}
}

Expand Down

0 comments on commit 69007bd

Please sign in to comment.