Skip to content

Commit 0169dc3

Browse files
scalexmscalexm
committed
Implement ResolventOps 
1 parent 3b2cfc5 commit 0169dc3

File tree

4 files changed

+572
-35
lines changed

4 files changed

+572
-35
lines changed

‎src/librustc/ty/fold.rs‎

Lines changed: 38 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -679,24 +679,31 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
679679
// vars. See comment on `shift_vars_through_binders` method in
680680
// `subst.rs` for more details.
681681

682+
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
683+
enum Direction {
684+
In,
685+
Out,
686+
}
687+
682688
struct Shifter<'a, 'gcx: 'a+'tcx, 'tcx: 'a> {
683689
tcx: TyCtxt<'a, 'gcx, 'tcx>,
684-
685690
current_index: ty::DebruijnIndex,
686691
amount: u32,
692+
direction: Direction,
687693
}
688694

689695
impl Shifter<'a, 'gcx, 'tcx> {
690-
pub fn new(tcx: TyCtxt<'a, 'gcx, 'tcx>, amount: u32) -> Self {
696+
pub fn new(tcx: TyCtxt<'a, 'gcx, 'tcx>, amount: u32, direction: Direction) -> Self {
691697
Shifter {
692698
tcx,
693699
current_index: ty::INNERMOST,
694700
amount,
701+
direction,
695702
}
696703
}
697704
}
698705

699-
impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
706+
impl TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
700707
fn tcx<'b>(&'b self) -> TyCtxt<'b, 'gcx, 'tcx> { self.tcx }
701708

702709
fn fold_binder<T: TypeFoldable<'tcx>>(&mut self, t: &ty::Binder<T>) -> ty::Binder<T> {
@@ -712,7 +719,14 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
712719
if self.amount == 0 || debruijn < self.current_index {
713720
r
714721
} else {
715-
let shifted = ty::ReLateBound(debruijn.shifted_in(self.amount), br);
722+
let debruijn = match self.direction {
723+
Direction::In => debruijn.shifted_in(self.amount),
724+
Direction::Out => {
725+
assert!(debruijn.as_u32() >= self.amount);
726+
debruijn.shifted_out(self.amount)
727+
}
728+
};
729+
let shifted = ty::ReLateBound(debruijn, br);
716730
self.tcx.mk_region(shifted)
717731
}
718732
}
@@ -726,8 +740,15 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
726740
if self.amount == 0 || debruijn < self.current_index {
727741
ty
728742
} else {
743+
let debruijn = match self.direction {
744+
Direction::In => debruijn.shifted_in(self.amount),
745+
Direction::Out => {
746+
assert!(debruijn.as_u32() >= self.amount);
747+
debruijn.shifted_out(self.amount)
748+
}
749+
};
729750
self.tcx.mk_ty(
730-
ty::Bound(debruijn.shifted_in(self.amount), bound_ty)
751+
ty::Bound(debruijn, bound_ty)
731752
)
732753
}
733754
}
@@ -760,7 +781,18 @@ pub fn shift_vars<'a, 'gcx, 'tcx, T>(
760781
debug!("shift_vars(value={:?}, amount={})",
761782
value, amount);
762783

763-
value.fold_with(&mut Shifter::new(tcx, amount))
784+
value.fold_with(&mut Shifter::new(tcx, amount, Direction::In))
785+
}
786+
787+
pub fn shift_out_vars<'a, 'gcx, 'tcx, T>(
788+
tcx: TyCtxt<'a, 'gcx, 'tcx>,
789+
value: &T,
790+
amount: u32
791+
) -> T where T: TypeFoldable<'tcx> {
792+
debug!("shift_out_vars(value={:?}, amount={})",
793+
value, amount);
794+
795+
value.fold_with(&mut Shifter::new(tcx, amount, Direction::Out))
764796
}
765797

766798
/// An "escaping var" is a bound var whose binder is not part of `t`. A bound var can be a

‎src/librustc/ty/relate.rs‎

Lines changed: 278 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ use std::rc::Rc;
2525
use std::iter;
2626
use rustc_target::spec::abi;
2727
use hir as ast;
28+
use traits;
2829

2930
pub type RelateResult<'tcx, T> = Result<T, TypeError<'tcx>>;
3031

@@ -723,6 +724,283 @@ impl<'tcx> Relate<'tcx> for Kind<'tcx> {
723724
}
724725
}
725726

727+
impl<'tcx> Relate<'tcx> for ty::TraitPredicate<'tcx> {
728+
fn relate<'a, 'gcx, R>(
729+
relation: &mut R,
730+
a: &ty::TraitPredicate<'tcx>,
731+
b: &ty::TraitPredicate<'tcx>
732+
) -> RelateResult<'tcx, ty::TraitPredicate<'tcx>>
733+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
734+
{
735+
Ok(ty::TraitPredicate {
736+
trait_ref: relation.relate(&a.trait_ref, &b.trait_ref)?,
737+
})
738+
}
739+
}
740+
741+
impl<'tcx> Relate<'tcx> for ty::ProjectionPredicate<'tcx> {
742+
fn relate<'a, 'gcx, R>(
743+
relation: &mut R,
744+
a: &ty::ProjectionPredicate<'tcx>,
745+
b: &ty::ProjectionPredicate<'tcx>,
746+
) -> RelateResult<'tcx, ty::ProjectionPredicate<'tcx>>
747+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
748+
{
749+
Ok(ty::ProjectionPredicate {
750+
projection_ty: relation.relate(&a.projection_ty, &b.projection_ty)?,
751+
ty: relation.relate(&a.ty, &b.ty)?,
752+
})
753+
}
754+
}
755+
756+
impl<'tcx> Relate<'tcx> for traits::WhereClause<'tcx> {
757+
fn relate<'a, 'gcx, R>(
758+
relation: &mut R,
759+
a: &traits::WhereClause<'tcx>,
760+
b: &traits::WhereClause<'tcx>
761+
) -> RelateResult<'tcx, traits::WhereClause<'tcx>>
762+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
763+
{
764+
use traits::WhereClause::*;
765+
match (a, b) {
766+
(Implemented(a_pred), Implemented(b_pred)) => {
767+
Ok(Implemented(relation.relate(a_pred, b_pred)?))
768+
}
769+
770+
(ProjectionEq(a_pred), ProjectionEq(b_pred)) => {
771+
Ok(ProjectionEq(relation.relate(a_pred, b_pred)?))
772+
}
773+
774+
(RegionOutlives(a_pred), RegionOutlives(b_pred)) => {
775+
Ok(RegionOutlives(ty::OutlivesPredicate(
776+
relation.relate(&a_pred.0, &b_pred.0)?,
777+
relation.relate(&a_pred.1, &b_pred.1)?,
778+
)))
779+
}
780+
781+
(TypeOutlives(a_pred), TypeOutlives(b_pred)) => {
782+
Ok(TypeOutlives(ty::OutlivesPredicate(
783+
relation.relate(&a_pred.0, &b_pred.0)?,
784+
relation.relate(&a_pred.1, &b_pred.1)?,
785+
)))
786+
}
787+
788+
_ => Err(TypeError::Mismatch),
789+
}
790+
}
791+
}
792+
793+
impl<'tcx> Relate<'tcx> for traits::WellFormed<'tcx> {
794+
fn relate<'a, 'gcx, R>(
795+
relation: &mut R,
796+
a: &traits::WellFormed<'tcx>,
797+
b: &traits::WellFormed<'tcx>
798+
) -> RelateResult<'tcx, traits::WellFormed<'tcx>>
799+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
800+
{
801+
use traits::WellFormed::*;
802+
match (a, b) {
803+
(Trait(a_pred), Trait(b_pred)) => Ok(Trait(relation.relate(a_pred, b_pred)?)),
804+
(Ty(a_ty), Ty(b_ty)) => Ok(Ty(relation.relate(a_ty, b_ty)?)),
805+
_ => Err(TypeError::Mismatch),
806+
}
807+
}
808+
}
809+
810+
impl<'tcx> Relate<'tcx> for traits::FromEnv<'tcx> {
811+
fn relate<'a, 'gcx, R>(
812+
relation: &mut R,
813+
a: &traits::FromEnv<'tcx>,
814+
b: &traits::FromEnv<'tcx>
815+
) -> RelateResult<'tcx, traits::FromEnv<'tcx>>
816+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
817+
{
818+
use traits::FromEnv::*;
819+
match (a, b) {
820+
(Trait(a_pred), Trait(b_pred)) => Ok(Trait(relation.relate(a_pred, b_pred)?)),
821+
(Ty(a_ty), Ty(b_ty)) => Ok(Ty(relation.relate(a_ty, b_ty)?)),
822+
_ => Err(TypeError::Mismatch),
823+
}
824+
}
825+
}
826+
827+
impl<'tcx> Relate<'tcx> for traits::DomainGoal<'tcx> {
828+
fn relate<'a, 'gcx, R>(
829+
relation: &mut R,
830+
a: &traits::DomainGoal<'tcx>,
831+
b: &traits::DomainGoal<'tcx>
832+
) -> RelateResult<'tcx, traits::DomainGoal<'tcx>>
833+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
834+
{
835+
use traits::DomainGoal::*;
836+
match (a, b) {
837+
(Holds(a_wc), Holds(b_wc)) => Ok(Holds(relation.relate(a_wc, b_wc)?)),
838+
(WellFormed(a_wf), WellFormed(b_wf)) => Ok(WellFormed(relation.relate(a_wf, b_wf)?)),
839+
(FromEnv(a_fe), FromEnv(b_fe)) => Ok(FromEnv(relation.relate(a_fe, b_fe)?)),
840+
841+
(Normalize(a_pred), Normalize(b_pred)) => {
842+
Ok(Normalize(relation.relate(a_pred, b_pred)?))
843+
}
844+
845+
_ => Err(TypeError::Mismatch),
846+
}
847+
}
848+
}
849+
850+
impl<'tcx> Relate<'tcx> for traits::Goal<'tcx> {
851+
fn relate<'a, 'gcx, R>(
852+
relation: &mut R,
853+
a: &traits::Goal<'tcx>,
854+
b: &traits::Goal<'tcx>
855+
) -> RelateResult<'tcx, traits::Goal<'tcx>>
856+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
857+
{
858+
use traits::GoalKind::*;
859+
match (a, b) {
860+
(Implies(a_clauses, a_goal), Implies(b_clauses, b_goal)) => {
861+
let clauses = relation.relate(a_clauses, b_clauses)?;
862+
let goal = relation.relate(a_goal, b_goal)?;
863+
Ok(relation.tcx().mk_goal(Implies(clauses, goal)))
864+
}
865+
866+
(And(a_left, a_right), And(b_left, b_right)) => {
867+
let left = relation.relate(a_left, b_left)?;
868+
let right = relation.relate(a_right, b_right)?;
869+
Ok(relation.tcx().mk_goal(And(left, right)))
870+
}
871+
872+
(Not(a_goal), Not(b_goal)) => {
873+
let goal = relation.relate(a_goal, b_goal)?;
874+
Ok(relation.tcx().mk_goal(Not(goal)))
875+
}
876+
877+
(DomainGoal(a_goal), DomainGoal(b_goal)) => {
878+
let goal = relation.relate(a_goal, b_goal)?;
879+
Ok(relation.tcx().mk_goal(DomainGoal(goal)))
880+
}
881+
882+
(Quantified(a_qkind, a_goal), Quantified(b_qkind, b_goal))
883+
if a_qkind == b_qkind =>
884+
{
885+
let goal = relation.relate(a_goal, b_goal)?;
886+
Ok(relation.tcx().mk_goal(Quantified(*a_qkind, goal)))
887+
}
888+
889+
(CannotProve, CannotProve) => Ok(*a),
890+
891+
_ => Err(TypeError::Mismatch),
892+
}
893+
}
894+
}
895+
896+
impl<'tcx> Relate<'tcx> for traits::Goals<'tcx> {
897+
fn relate<'a, 'gcx, R>(
898+
relation: &mut R,
899+
a: &traits::Goals<'tcx>,
900+
b: &traits::Goals<'tcx>
901+
) -> RelateResult<'tcx, traits::Goals<'tcx>>
902+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
903+
{
904+
if a.len() != b.len() {
905+
return Err(TypeError::Mismatch);
906+
}
907+
908+
let tcx = relation.tcx();
909+
let goals = a.iter().zip(b.iter()).map(|(a, b)| relation.relate(a, b));
910+
Ok(tcx.mk_goals(goals)?)
911+
}
912+
}
913+
914+
impl<'tcx> Relate<'tcx> for traits::Clause<'tcx> {
915+
fn relate<'a, 'gcx, R>(
916+
relation: &mut R,
917+
a: &traits::Clause<'tcx>,
918+
b: &traits::Clause<'tcx>
919+
) -> RelateResult<'tcx, traits::Clause<'tcx>>
920+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
921+
{
922+
use traits::Clause::*;
923+
match (a, b) {
924+
(Implies(a_clause), Implies(b_clause)) => {
925+
let clause = relation.relate(a_clause, b_clause)?;
926+
Ok(Implies(clause))
927+
}
928+
929+
(ForAll(a_clause), ForAll(b_clause)) => {
930+
let clause = relation.relate(a_clause, b_clause)?;
931+
Ok(ForAll(clause))
932+
}
933+
934+
_ => Err(TypeError::Mismatch),
935+
}
936+
}
937+
}
938+
939+
impl<'tcx> Relate<'tcx> for traits::Clauses<'tcx> {
940+
fn relate<'a, 'gcx, R>(
941+
relation: &mut R,
942+
a: &traits::Clauses<'tcx>,
943+
b: &traits::Clauses<'tcx>
944+
) -> RelateResult<'tcx, traits::Clauses<'tcx>>
945+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
946+
{
947+
if a.len() != b.len() {
948+
return Err(TypeError::Mismatch);
949+
}
950+
951+
let tcx = relation.tcx();
952+
let clauses = a.iter().zip(b.iter()).map(|(a, b)| relation.relate(a, b));
953+
Ok(tcx.mk_clauses(clauses)?)
954+
}
955+
}
956+
957+
impl<'tcx> Relate<'tcx> for traits::ProgramClause<'tcx> {
958+
fn relate<'a, 'gcx, R>(
959+
relation: &mut R,
960+
a: &traits::ProgramClause<'tcx>,
961+
b: &traits::ProgramClause<'tcx>
962+
) -> RelateResult<'tcx, traits::ProgramClause<'tcx>>
963+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
964+
{
965+
Ok(traits::ProgramClause {
966+
goal: relation.relate(&a.goal, &b.goal)?,
967+
hypotheses: relation.relate(&a.hypotheses, &b.hypotheses)?,
968+
category: traits::ProgramClauseCategory::Other,
969+
})
970+
}
971+
}
972+
973+
impl<'tcx> Relate<'tcx> for traits::Environment<'tcx> {
974+
fn relate<'a, 'gcx, R>(
975+
relation: &mut R,
976+
a: &traits::Environment<'tcx>,
977+
b: &traits::Environment<'tcx>
978+
) -> RelateResult<'tcx, traits::Environment<'tcx>>
979+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
980+
{
981+
Ok(traits::Environment {
982+
clauses: relation.relate(&a.clauses, &b.clauses)?,
983+
})
984+
}
985+
}
986+
987+
impl<'tcx, G> Relate<'tcx> for traits::InEnvironment<'tcx, G>
988+
where G: Relate<'tcx>
989+
{
990+
fn relate<'a, 'gcx, R>(
991+
relation: &mut R,
992+
a: &traits::InEnvironment<'tcx, G>,
993+
b: &traits::InEnvironment<'tcx, G>
994+
) -> RelateResult<'tcx, traits::InEnvironment<'tcx, G>>
995+
where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
996+
{
997+
Ok(traits::InEnvironment {
998+
environment: relation.relate(&a.environment, &b.environment)?,
999+
goal: relation.relate(&a.goal, &b.goal)?,
1000+
})
1001+
}
1002+
}
1003+
7261004
///////////////////////////////////////////////////////////////////////////
7271005
// Error handling
7281006

0 commit comments

Comments
 (0)