merge wellformed(wc)s

This commit is contained in:
csmoe 2018-05-11 18:32:51 +08:00
parent dabd3f6935
commit ff83ef0c24
5 changed files with 24 additions and 38 deletions

View file

@ -13,10 +13,9 @@ use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
use rustc::hir::map::definitions::DefPathData;
use rustc::hir::{self, ImplPolarity};
use rustc::traits::{
Clause, Clauses, DomainGoal, FromEnv, Goal, PolyDomainGoal, ProgramClause, WellFormed,
WhereClause,
Clause, Clauses, DomainGoal, Goal, PolyDomainGoal, ProgramClause, WhereClauseAtom,
};
use rustc::ty::query::Providers;
use rustc::ty::subst::Substs;
use rustc::ty::{self, Slice, TyCtxt};
use rustc_data_structures::fx::FxHashSet;
use std::mem;
@ -278,21 +277,15 @@ fn program_clauses_for_trait<'a, 'tcx>(
hypotheses,
}))
.map(|wc| implied_bound_from_trait(tcx, trait_pred, wc));
let wellformed_clauses = where_clauses[1..]
.into_iter()
.map(|wc| wellformed_from_bound(tcx, trait_pred, wc));
tcx.mk_clauses(
clauses
.chain(implied_bound_clauses)
.chain(wellformed_clauses),
)
let wellformed_clauses = wellformed_from_bound(tcx, trait_pred, &where_clauses[1..]);
tcx.mk_clauses(clauses.chain(implied_bound_clauses).chain(wellformed_clauses))
}
fn wellformed_from_bound<'a, 'tcx>(
tcx: TyCtxt<'a, 'tcx, 'tcx>,
trait_pred: ty::TraitPredicate<'tcx>,
where_clause: &ty::Predicate<'tcx>,
) -> Clause<'tcx> {
where_clauses: &[ty::Predicate<'tcx>],
) -> iter::Once<Clause<'tcx>> {
// Rule WellFormed-TraitRef
//
// For each where clause WC:
@ -309,18 +302,17 @@ fn wellformed_from_bound<'a, 'tcx>(
.lower()
.map_bound(|wc| wc.into_wellformed_goal());
// Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
let mut where_clauses = vec![impl_trait];
where_clauses.push(wellformed_wc);
Clause::ForAll(where_clause.lower().map_bound(|_| {
ProgramClause {
goal: wellformed_trait,
hypotheses: tcx.mk_goals(
where_clauses
.into_iter()
.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
),
}
}))
let mut wcs = vec![impl_trait];
wcs.extend(wellformed_wcs);
let clause = ProgramClause {
goal: wellformed_trait,
hypotheses: tcx.mk_goals(
wcs.into_iter()
.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
),
};
iter::once(Clause::ForAll(ty::Binder::dummy(clause)))
}
fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Clauses<'tcx> {

View file

@ -7,8 +7,7 @@ LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
= note: FromEnv(Self: Foo) :- FromEnv(Self: Bar).
= note: FromEnv(Self: Foo) :- FromEnv(Self: Bar).
= note: Implemented(Self: Bar) :- FromEnv(Self: Bar).
= note: WellFormed(Self: Bar) :- Implemented(Self: Bar), WellFormed(Self: Bar).
= note: WellFormed(Self: Bar) :- Implemented(Self: Bar), WellFormed(Self: Foo).
= note: WellFormed(Self: Bar) :- Implemented(Self: Bar), WellFormed(Self: Bar), WellFormed(Self: Foo).
error: program clause dump
--> $DIR/lower_env1.rs:19:1
@ -21,8 +20,9 @@ LL | #[rustc_dump_env_program_clauses] //~ ERROR program clause dump
= note: Implemented(Self: Bar) :- FromEnv(Self: Bar).
= note: Implemented(Self: Foo) :- FromEnv(Self: Foo).
= note: Implemented(Self: std::marker::Sized) :- FromEnv(Self: std::marker::Sized).
= note: WellFormed(Self: Bar) :- Implemented(Self: Bar), WellFormed(Self: Bar).
= note: WellFormed(Self: Bar) :- Implemented(Self: Bar), WellFormed(Self: Foo).
= note: WellFormed(Self: Bar) :- Implemented(Self: Bar), WellFormed(Self: Bar), WellFormed(Self: Foo).
= note: WellFormed(Self: Foo) :- Implemented(Self: Foo).
= note: WellFormed(Self: std::marker::Sized) :- Implemented(Self: std::marker::Sized).
error: aborting due to 2 previous errors

View file

@ -8,9 +8,7 @@ LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
= note: FromEnv(T: std::marker::Sized) :- FromEnv(Self: Foo<S, T, U>).
= note: FromEnv(U: std::marker::Sized) :- FromEnv(Self: Foo<S, T, U>).
= note: Implemented(Self: Foo<S, T, U>) :- FromEnv(Self: Foo<S, T, U>).
= note: WellFormed(Self: Foo<S, T, U>) :- Implemented(Self: Foo<S, T, U>), WellFormed(S: std::marker::Sized).
= note: WellFormed(Self: Foo<S, T, U>) :- Implemented(Self: Foo<S, T, U>), WellFormed(T: std::marker::Sized).
= note: WellFormed(Self: Foo<S, T, U>) :- Implemented(Self: Foo<S, T, U>), WellFormed(U: std::marker::Sized).
= note: WellFormed(Self: Foo<S, T, U>) :- Implemented(Self: Foo<S, T, U>), WellFormed(S: std::marker::Sized), WellFormed(T: std::marker::Sized), WellFormed(U: std::marker::Sized).
error: aborting due to previous error

View file

@ -11,6 +11,7 @@ LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
= note: WellFormed(Self: Foo<F>) :- Implemented(Self: Foo<F>), WellFormed(F: std::marker::Sized).
= note: WellFormed(Self: Foo<F>) :- Implemented(Self: Foo<F>), forall<> { WellFormed(<F as std::ops::FnOnce<(&'a (u8, u16),)>>::Output == &'a u8) }.
= note: WellFormed(Self: Foo<F>) :- Implemented(Self: Foo<F>), forall<> { WellFormed(F: std::ops::Fn<(&'a (u8, u16),)>) }.
= note: WellFormed(Self: Foo<F>) :- Implemented(Self: Foo<F>), WellFormed(F: std::marker::Sized), forall<> { WellFormed(F: std::ops::Fn<(&'a (u8, u16),)>) }, forall<> { WellFormed(<F as std::ops::FnOnce<(&'a (u8, u16),)>>::Output == &'a u8) }.
error: aborting due to previous error

View file

@ -11,12 +11,7 @@ LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
= note: Implemented(Self: Foo<'a, 'b, S, T, U>) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
= note: RegionOutlives('a : 'b) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
= note: TypeOutlives(U : 'b) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
= note: WellFormed(Self: Foo<'a, 'b, S, T, U>) :- Implemented(Self: Foo<'a, 'b, S, T, U>), RegionOutlives('a : 'b).
= note: WellFormed(Self: Foo<'a, 'b, S, T, U>) :- Implemented(Self: Foo<'a, 'b, S, T, U>), TypeOutlives(U : 'b).
= note: WellFormed(Self: Foo<'a, 'b, S, T, U>) :- Implemented(Self: Foo<'a, 'b, S, T, U>), WellFormed(S: std::fmt::Debug).
= note: WellFormed(Self: Foo<'a, 'b, S, T, U>) :- Implemented(Self: Foo<'a, 'b, S, T, U>), WellFormed(S: std::marker::Sized).
= note: WellFormed(Self: Foo<'a, 'b, S, T, U>) :- Implemented(Self: Foo<'a, 'b, S, T, U>), WellFormed(T: std::borrow::Borrow<U>).
= note: WellFormed(Self: Foo<'a, 'b, S, T, U>) :- Implemented(Self: Foo<'a, 'b, S, T, U>), WellFormed(T: std::marker::Sized).
= note: WellFormed(Self: Foo<'a, 'b, S, T, U>) :- Implemented(Self: Foo<'a, 'b, S, T, U>), WellFormed(S: std::marker::Sized), WellFormed(T: std::marker::Sized), WellFormed(S: std::fmt::Debug), WellFormed(T: std::borrow::Borrow<U>), RegionOutlives('a : 'b), TypeOutlives(U : 'b).
error: aborting due to previous error