2018-03-10 05:44:33 -06:00
|
|
|
// Copyright 2018 The Rust Project Developers. See the COPYRIGHT
|
|
|
|
// file at the top-level directory of this distribution and at
|
|
|
|
// http://rust-lang.org/COPYRIGHT.
|
|
|
|
//
|
|
|
|
// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
|
|
|
|
// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
|
|
|
|
// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
|
|
|
|
// option. This file may not be copied, modified, or distributed
|
|
|
|
// except according to those terms.
|
|
|
|
|
2018-03-14 08:45:30 -05:00
|
|
|
use rustc::hir::def_id::DefId;
|
|
|
|
use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
|
2018-04-10 04:55:18 -05:00
|
|
|
use rustc::hir::map::definitions::DefPathData;
|
|
|
|
use rustc::hir::{self, ImplPolarity};
|
2018-05-01 19:02:47 -05:00
|
|
|
use rustc::traits::{
|
|
|
|
Clause, Clauses, DomainGoal, FromEnv, Goal, PolyDomainGoal, ProgramClause, WellFormed,
|
|
|
|
WhereClause,
|
|
|
|
};
|
2018-06-27 08:42:00 -05:00
|
|
|
use rustc::ty::query::Providers;
|
2018-04-10 04:56:35 -05:00
|
|
|
use rustc::ty::{self, Slice, TyCtxt};
|
2018-04-10 04:55:18 -05:00
|
|
|
use rustc_data_structures::fx::FxHashSet;
|
|
|
|
use std::mem;
|
2018-04-10 04:56:35 -05:00
|
|
|
use syntax::ast;
|
2018-03-10 05:44:33 -06:00
|
|
|
|
2018-04-09 02:38:00 -05:00
|
|
|
use std::iter;
|
|
|
|
|
2018-06-27 08:42:00 -05:00
|
|
|
crate fn provide(p: &mut Providers) {
|
|
|
|
*p = Providers {
|
|
|
|
program_clauses_for,
|
|
|
|
program_clauses_for_env,
|
|
|
|
..*p
|
|
|
|
};
|
|
|
|
}
|
|
|
|
|
2018-05-08 16:15:48 -05:00
|
|
|
crate trait Lower<T> {
|
2018-06-04 06:57:56 -05:00
|
|
|
/// Lower a rustc construct (e.g. `ty::TraitPredicate`) to a chalk-like type.
|
2018-03-10 05:44:33 -06:00
|
|
|
fn lower(&self) -> T;
|
|
|
|
}
|
|
|
|
|
2018-04-10 04:56:35 -05:00
|
|
|
impl<T, U> Lower<Vec<U>> for Vec<T>
|
|
|
|
where
|
|
|
|
T: Lower<U>,
|
|
|
|
{
|
2018-03-10 05:44:33 -06:00
|
|
|
fn lower(&self) -> Vec<U> {
|
|
|
|
self.iter().map(|item| item.lower()).collect()
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-06-04 06:57:56 -05:00
|
|
|
impl<'tcx> Lower<WhereClause<'tcx>> for ty::TraitPredicate<'tcx> {
|
|
|
|
fn lower(&self) -> WhereClause<'tcx> {
|
|
|
|
WhereClause::Implemented(*self)
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-06-04 06:57:56 -05:00
|
|
|
impl<'tcx> Lower<WhereClause<'tcx>> for ty::ProjectionPredicate<'tcx> {
|
|
|
|
fn lower(&self) -> WhereClause<'tcx> {
|
|
|
|
WhereClause::ProjectionEq(*self)
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-06-04 06:57:56 -05:00
|
|
|
impl<'tcx> Lower<WhereClause<'tcx>> for ty::RegionOutlivesPredicate<'tcx> {
|
|
|
|
fn lower(&self) -> WhereClause<'tcx> {
|
|
|
|
WhereClause::RegionOutlives(*self)
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-06-04 06:57:56 -05:00
|
|
|
impl<'tcx> Lower<WhereClause<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
|
|
|
|
fn lower(&self) -> WhereClause<'tcx> {
|
|
|
|
WhereClause::TypeOutlives(*self)
|
2018-03-14 07:38:03 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-06-04 06:57:56 -05:00
|
|
|
impl<'tcx, T> Lower<DomainGoal<'tcx>> for T
|
|
|
|
where
|
|
|
|
T: Lower<WhereClause<'tcx>>,
|
|
|
|
{
|
2018-03-14 07:38:03 -05:00
|
|
|
fn lower(&self) -> DomainGoal<'tcx> {
|
2018-06-04 06:57:56 -05:00
|
|
|
DomainGoal::Holds(self.lower())
|
2018-03-14 07:38:03 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-03-14 09:19:17 -05:00
|
|
|
/// `ty::Binder` is used for wrapping a rustc construction possibly containing generic
|
|
|
|
/// lifetimes, e.g. `for<'a> T: Fn(&'a i32)`. Instead of representing higher-ranked things
|
|
|
|
/// in that leaf-form (i.e. `Holds(Implemented(Binder<TraitPredicate>))` in the previous
|
2018-03-28 07:13:08 -05:00
|
|
|
/// example), we model them with quantified domain goals, e.g. as for the previous example:
|
2018-03-14 09:19:17 -05:00
|
|
|
/// `forall<'a> { T: Fn(&'a i32) }` which corresponds to something like
|
|
|
|
/// `Binder<Holds(Implemented(TraitPredicate))>`.
|
2018-03-28 07:13:08 -05:00
|
|
|
impl<'tcx, T> Lower<PolyDomainGoal<'tcx>> for ty::Binder<T>
|
2018-04-10 04:56:35 -05:00
|
|
|
where
|
|
|
|
T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx>,
|
2018-03-14 07:38:03 -05:00
|
|
|
{
|
2018-03-28 07:13:08 -05:00
|
|
|
fn lower(&self) -> PolyDomainGoal<'tcx> {
|
|
|
|
self.map_bound_ref(|p| p.lower())
|
2018-03-14 07:38:03 -05:00
|
|
|
}
|
|
|
|
}
|
2018-03-10 05:44:33 -06:00
|
|
|
|
2018-03-28 07:13:08 -05:00
|
|
|
impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
|
|
|
|
fn lower(&self) -> PolyDomainGoal<'tcx> {
|
2018-06-04 06:57:56 -05:00
|
|
|
use rustc::ty::Predicate;
|
2018-03-14 07:38:03 -05:00
|
|
|
|
|
|
|
match self {
|
2018-06-04 06:57:56 -05:00
|
|
|
Predicate::Trait(predicate) => predicate.lower(),
|
|
|
|
Predicate::RegionOutlives(predicate) => predicate.lower(),
|
|
|
|
Predicate::TypeOutlives(predicate) => predicate.lower(),
|
|
|
|
Predicate::Projection(predicate) => predicate.lower(),
|
2018-05-01 19:02:47 -05:00
|
|
|
Predicate::WellFormed(ty) => {
|
|
|
|
ty::Binder::dummy(DomainGoal::WellFormed(WellFormed::Ty(*ty)))
|
2018-04-10 04:56:35 -05:00
|
|
|
}
|
2018-05-01 19:02:47 -05:00
|
|
|
Predicate::ObjectSafe(..)
|
|
|
|
| Predicate::ClosureKind(..)
|
|
|
|
| Predicate::Subtype(..)
|
|
|
|
| Predicate::ConstEvaluatable(..) => unimplemented!(),
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-03-26 23:03:50 -05:00
|
|
|
/// Used for lowered where clauses (see rustc guide).
|
|
|
|
trait IntoFromEnvGoal {
|
2018-05-01 19:02:47 -05:00
|
|
|
// Transforms an existing goal into a FromEnv goal.
|
2018-03-26 23:03:50 -05:00
|
|
|
fn into_from_env_goal(self) -> Self;
|
|
|
|
}
|
|
|
|
|
2018-05-01 19:02:47 -05:00
|
|
|
trait IntoWellFormedGoal {
|
|
|
|
fn into_wellformed_goal(self) -> Self;
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<'tcx> IntoGoal for DomainGoal<'tcx> {
|
|
|
|
// Transforms an existing goal into a WellFormed goal.
|
2018-03-26 23:03:50 -05:00
|
|
|
fn into_from_env_goal(self) -> DomainGoal<'tcx> {
|
2018-06-04 06:57:56 -05:00
|
|
|
use self::WhereClause::*;
|
|
|
|
|
2018-03-26 23:03:50 -05:00
|
|
|
match self {
|
2018-05-01 19:02:47 -05:00
|
|
|
DomainGoal::Holds(Implemented(trait_ref)) => {
|
|
|
|
DomainGoal::FromEnv(FromEnv::Trait(trait_ref))
|
|
|
|
}
|
2018-06-04 06:57:56 -05:00
|
|
|
other => other,
|
2018-03-26 23:03:50 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-05-01 19:02:47 -05:00
|
|
|
impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
|
|
|
|
fn into_wellformed_goal(self) -> DomainGoal<'tcx> {
|
|
|
|
use self::DomainGoal::*;
|
|
|
|
match self {
|
|
|
|
Holds(wc_atom) => WellFormed(wc_atom),
|
|
|
|
WellFormed(..) | FromEnv(..) | WellFormedTy(..) | FromEnvTy(..) | Normalize(..)
|
|
|
|
| RegionOutlives(..) | TypeOutlives(..) => self,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-04-10 04:56:35 -05:00
|
|
|
crate fn program_clauses_for<'a, 'tcx>(
|
|
|
|
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
|
|
|
def_id: DefId,
|
2018-04-23 12:12:00 -05:00
|
|
|
) -> Clauses<'tcx> {
|
2018-04-10 04:55:18 -05:00
|
|
|
match tcx.def_key(def_id).disambiguated_data.data {
|
|
|
|
DefPathData::Trait(_) => program_clauses_for_trait(tcx, def_id),
|
|
|
|
DefPathData::Impl => program_clauses_for_impl(tcx, def_id),
|
|
|
|
DefPathData::AssocTypeInImpl(..) => program_clauses_for_associated_type_value(tcx, def_id),
|
2018-06-06 12:03:56 -05:00
|
|
|
DefPathData::AssocTypeInTrait(..) => program_clauses_for_associated_type_def(tcx, def_id),
|
|
|
|
DefPathData::TypeNs(..) => program_clauses_for_type_def(tcx, def_id),
|
2018-04-23 12:12:00 -05:00
|
|
|
_ => Slice::empty(),
|
2018-04-10 04:55:18 -05:00
|
|
|
}
|
|
|
|
}
|
2018-03-14 09:19:17 -05:00
|
|
|
|
2018-04-10 04:55:18 -05:00
|
|
|
crate fn program_clauses_for_env<'a, 'tcx>(
|
|
|
|
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
|
|
|
param_env: ty::ParamEnv<'tcx>,
|
2018-04-23 12:12:00 -05:00
|
|
|
) -> Clauses<'tcx> {
|
2018-04-10 04:55:18 -05:00
|
|
|
debug!("program_clauses_for_env(param_env={:?})", param_env);
|
|
|
|
|
|
|
|
let mut last_round = FxHashSet();
|
|
|
|
last_round.extend(
|
|
|
|
param_env
|
|
|
|
.caller_bounds
|
|
|
|
.iter()
|
|
|
|
.flat_map(|&p| predicate_def_id(p)),
|
|
|
|
);
|
|
|
|
|
|
|
|
let mut closure = last_round.clone();
|
|
|
|
let mut next_round = FxHashSet();
|
|
|
|
while !last_round.is_empty() {
|
|
|
|
next_round.extend(
|
|
|
|
last_round
|
|
|
|
.drain()
|
|
|
|
.flat_map(|def_id| {
|
|
|
|
tcx.predicates_of(def_id)
|
|
|
|
.instantiate_identity(tcx)
|
|
|
|
.predicates
|
|
|
|
})
|
|
|
|
.flat_map(|p| predicate_def_id(p))
|
|
|
|
.filter(|&def_id| closure.insert(def_id)),
|
|
|
|
);
|
|
|
|
mem::swap(&mut next_round, &mut last_round);
|
|
|
|
}
|
|
|
|
|
|
|
|
debug!("program_clauses_for_env: closure = {:#?}", closure);
|
|
|
|
|
2018-04-23 12:12:00 -05:00
|
|
|
return tcx.mk_clauses(
|
|
|
|
closure
|
|
|
|
.into_iter()
|
|
|
|
.flat_map(|def_id| tcx.program_clauses_for(def_id).iter().cloned()),
|
2018-04-10 04:55:18 -05:00
|
|
|
);
|
|
|
|
|
|
|
|
/// Given that `predicate` is in the environment, returns the
|
|
|
|
/// def-id of something (e.g., a trait, associated item, etc)
|
|
|
|
/// whose predicates can also be assumed to be true. We will
|
|
|
|
/// compute the transitive closure of such things.
|
|
|
|
fn predicate_def_id<'tcx>(predicate: ty::Predicate<'tcx>) -> Option<DefId> {
|
|
|
|
match predicate {
|
|
|
|
ty::Predicate::Trait(predicate) => Some(predicate.def_id()),
|
|
|
|
|
|
|
|
ty::Predicate::Projection(projection) => Some(projection.item_def_id()),
|
|
|
|
|
|
|
|
ty::Predicate::WellFormed(..)
|
|
|
|
| ty::Predicate::RegionOutlives(..)
|
|
|
|
| ty::Predicate::TypeOutlives(..)
|
|
|
|
| ty::Predicate::ObjectSafe(..)
|
|
|
|
| ty::Predicate::ClosureKind(..)
|
|
|
|
| ty::Predicate::Subtype(..)
|
|
|
|
| ty::Predicate::ConstEvaluatable(..) => None,
|
|
|
|
}
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2018-04-10 04:56:35 -05:00
|
|
|
fn program_clauses_for_trait<'a, 'tcx>(
|
|
|
|
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
|
|
|
def_id: DefId,
|
2018-04-23 12:12:00 -05:00
|
|
|
) -> Clauses<'tcx> {
|
2018-03-20 10:13:44 -05:00
|
|
|
// `trait Trait<P1..Pn> where WC { .. } // P0 == Self`
|
2018-03-26 23:03:50 -05:00
|
|
|
|
|
|
|
// Rule Implemented-From-Env (see rustc guide)
|
2018-03-20 10:13:44 -05:00
|
|
|
//
|
|
|
|
// ```
|
|
|
|
// forall<Self, P1..Pn> {
|
|
|
|
// Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
|
|
|
|
// }
|
|
|
|
// ```
|
|
|
|
|
|
|
|
// `Self: Trait<P1..Pn>`
|
|
|
|
let trait_pred = ty::TraitPredicate {
|
2018-06-29 05:59:00 -05:00
|
|
|
trait_ref: ty::TraitRef::identity(tcx, def_id),
|
2018-03-20 10:13:44 -05:00
|
|
|
};
|
2018-06-04 06:57:56 -05:00
|
|
|
|
2018-03-20 10:13:44 -05:00
|
|
|
// `Implemented(Self: Trait<P1..Pn>)`
|
2018-06-04 06:57:56 -05:00
|
|
|
let impl_trait: DomainGoal = trait_pred.lower();
|
|
|
|
|
2018-05-01 19:02:47 -05:00
|
|
|
// `FromEnv(Self: Trait<P1..Pn>)`
|
2018-06-06 12:03:56 -05:00
|
|
|
let from_env_goal = impl_trait.into_from_env_goal().into_goal();
|
|
|
|
let hypotheses = tcx.intern_goals(&[from_env_goal]);
|
2018-03-20 10:13:44 -05:00
|
|
|
|
|
|
|
// `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
|
2018-03-26 23:03:50 -05:00
|
|
|
let implemented_from_env = ProgramClause {
|
2018-03-28 07:13:08 -05:00
|
|
|
goal: impl_trait,
|
2018-06-04 06:57:56 -05:00
|
|
|
hypotheses,
|
2018-03-28 07:13:08 -05:00
|
|
|
};
|
2018-06-04 06:57:56 -05:00
|
|
|
|
2018-04-10 04:56:35 -05:00
|
|
|
let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env)));
|
2018-03-26 23:03:50 -05:00
|
|
|
|
|
|
|
// Rule Implied-Bound-From-Trait
|
|
|
|
//
|
|
|
|
// For each where clause WC:
|
|
|
|
// ```
|
|
|
|
// forall<Self, P1..Pn> {
|
|
|
|
// FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn)
|
|
|
|
// }
|
|
|
|
// ```
|
|
|
|
|
|
|
|
// `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`, for each where clause WC
|
2018-07-02 09:35:30 -05:00
|
|
|
let where_clauses = &tcx.predicates_defined_on(def_id).predicates;
|
|
|
|
let implied_bound_clauses = where_clauses
|
2018-04-10 04:56:35 -05:00
|
|
|
.into_iter()
|
2018-06-04 06:57:56 -05:00
|
|
|
.map(|wc| wc.lower())
|
2018-03-26 23:03:50 -05:00
|
|
|
|
2018-06-04 06:57:56 -05:00
|
|
|
// `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
|
|
|
|
.map(|wc| wc.map_bound(|goal| ProgramClause {
|
|
|
|
goal: goal.into_from_env_goal(),
|
|
|
|
hypotheses,
|
|
|
|
}))
|
2018-05-01 19:02:47 -05:00
|
|
|
.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),
|
|
|
|
)
|
|
|
|
}
|
2018-03-26 23:03:50 -05:00
|
|
|
|
2018-05-01 19:02:47 -05:00
|
|
|
fn wellformed_from_bound<'a, 'tcx>(
|
|
|
|
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
|
|
|
trait_pred: ty::TraitPredicate<'tcx>,
|
|
|
|
where_clause: &ty::Predicate<'tcx>,
|
|
|
|
) -> Clause<'tcx> {
|
|
|
|
// Rule WellFormed-TraitRef
|
|
|
|
//
|
|
|
|
// For each where clause WC:
|
|
|
|
// forall<Self, P1..Pn> {
|
|
|
|
// WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
|
|
|
|
// }
|
2018-06-04 06:57:56 -05:00
|
|
|
|
2018-05-01 19:02:47 -05:00
|
|
|
// WellFormed(Self: Trait<P1..Pn>)
|
|
|
|
let wellformed_trait = DomainGoal::WellFormed(WhereClauseAtom::Implemented(trait_pred));
|
|
|
|
// Impemented(Self: Trait<P1..Pn>)
|
|
|
|
let impl_trait = ty::Binder::dummy(DomainGoal::Holds(WhereClauseAtom::Implemented(trait_pred)));
|
|
|
|
// WellFormed(WC)
|
|
|
|
let wellformed_wc = where_clause
|
|
|
|
.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)),
|
|
|
|
),
|
|
|
|
}
|
|
|
|
}))
|
2018-03-20 10:13:44 -05:00
|
|
|
}
|
|
|
|
|
2018-04-23 12:12:00 -05:00
|
|
|
fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Clauses<'tcx> {
|
2018-03-10 05:44:33 -06:00
|
|
|
if let ImplPolarity::Negative = tcx.impl_polarity(def_id) {
|
2018-04-23 12:12:00 -05:00
|
|
|
return Slice::empty();
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
2018-03-15 17:20:06 -05:00
|
|
|
|
2018-03-20 10:11:26 -05:00
|
|
|
// Rule Implemented-From-Impl (see rustc guide)
|
2018-03-15 13:27:00 -05:00
|
|
|
//
|
2018-03-20 10:11:26 -05:00
|
|
|
// `impl<P0..Pn> Trait<A1..An> for A0 where WC { .. }`
|
|
|
|
//
|
|
|
|
// ```
|
|
|
|
// forall<P0..Pn> {
|
|
|
|
// Implemented(A0: Trait<A1..An>) :- WC
|
|
|
|
// }
|
|
|
|
// ```
|
2018-03-10 05:44:33 -06:00
|
|
|
|
2018-06-04 06:57:56 -05:00
|
|
|
let trait_ref = tcx.impl_trait_ref(def_id).expect("not an impl");
|
|
|
|
|
2018-03-20 10:11:26 -05:00
|
|
|
// `Implemented(A0: Trait<A1..An>)`
|
|
|
|
let trait_pred = ty::TraitPredicate { trait_ref }.lower();
|
2018-06-04 06:57:56 -05:00
|
|
|
|
2018-04-10 04:56:35 -05:00
|
|
|
// `WC`
|
2018-03-10 05:44:33 -06:00
|
|
|
let where_clauses = tcx.predicates_of(def_id).predicates.lower();
|
|
|
|
|
2018-04-10 04:56:35 -05:00
|
|
|
// `Implemented(A0: Trait<A1..An>) :- WC`
|
2018-03-28 07:13:08 -05:00
|
|
|
let clause = ProgramClause {
|
|
|
|
goal: trait_pred,
|
2018-04-09 02:38:00 -05:00
|
|
|
hypotheses: tcx.mk_goals(
|
2018-04-10 04:56:35 -05:00
|
|
|
where_clauses
|
|
|
|
.into_iter()
|
|
|
|
.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
|
|
|
|
),
|
2018-03-28 07:13:08 -05:00
|
|
|
};
|
2018-05-16 02:43:24 -05:00
|
|
|
tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))])
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
|
|
|
|
2018-06-06 12:03:56 -05:00
|
|
|
pub fn program_clauses_for_type_def<'a, 'tcx>(
|
|
|
|
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
|
|
|
def_id: DefId,
|
|
|
|
) -> Clauses<'tcx> {
|
|
|
|
// Rule WellFormed-Type
|
|
|
|
//
|
|
|
|
// `struct Ty<P1..Pn> where WC1, ..., WCm`
|
|
|
|
//
|
|
|
|
// ```
|
|
|
|
// forall<P1..Pn> {
|
|
|
|
// WellFormed(Ty<...>) :- WC1, ..., WCm`
|
|
|
|
// }
|
|
|
|
// ```
|
|
|
|
|
|
|
|
// `Ty<...>`
|
|
|
|
let ty = tcx.type_of(def_id);
|
|
|
|
|
|
|
|
// `WC`
|
|
|
|
let where_clauses = tcx.predicates_of(def_id).predicates.lower();
|
|
|
|
|
|
|
|
// `WellFormed(Ty<...>) :- WC1, ..., WCm`
|
|
|
|
let well_formed = ProgramClause {
|
|
|
|
goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
|
|
|
|
hypotheses: tcx.mk_goals(
|
2018-05-01 19:02:47 -05:00
|
|
|
where_clauses
|
|
|
|
.iter()
|
|
|
|
.cloned()
|
|
|
|
.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
|
2018-06-06 12:03:56 -05:00
|
|
|
),
|
|
|
|
};
|
|
|
|
|
|
|
|
let well_formed_clause = iter::once(Clause::ForAll(ty::Binder::dummy(well_formed)));
|
|
|
|
|
|
|
|
// Rule FromEnv-Type
|
|
|
|
//
|
|
|
|
// For each where clause `WC`:
|
|
|
|
// ```
|
|
|
|
// forall<P1..Pn> {
|
|
|
|
// FromEnv(WC) :- FromEnv(Ty<...>)
|
|
|
|
// }
|
|
|
|
// ```
|
|
|
|
|
|
|
|
// `FromEnv(Ty<...>)`
|
|
|
|
let from_env_goal = DomainGoal::FromEnv(FromEnv::Ty(ty)).into_goal();
|
|
|
|
let hypotheses = tcx.intern_goals(&[from_env_goal]);
|
|
|
|
|
|
|
|
// For each where clause `WC`:
|
|
|
|
let from_env_clauses = where_clauses
|
|
|
|
.into_iter()
|
|
|
|
|
|
|
|
// `FromEnv(WC) :- FromEnv(Ty<...>)`
|
|
|
|
.map(|wc| wc.map_bound(|goal| ProgramClause {
|
|
|
|
goal: goal.into_from_env_goal(),
|
|
|
|
hypotheses,
|
|
|
|
}))
|
|
|
|
|
|
|
|
.map(Clause::ForAll);
|
|
|
|
|
|
|
|
tcx.mk_clauses(well_formed_clause.chain(from_env_clauses))
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
|
|
|
|
_tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
|
|
|
_item_id: DefId,
|
|
|
|
) -> Clauses<'tcx> {
|
|
|
|
unimplemented!()
|
|
|
|
}
|
|
|
|
|
2018-04-06 19:04:28 -05:00
|
|
|
pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
|
|
|
|
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
|
|
|
item_id: DefId,
|
2018-04-23 12:12:00 -05:00
|
|
|
) -> Clauses<'tcx> {
|
2018-04-03 10:53:13 -05:00
|
|
|
// Rule Normalize-From-Impl (see rustc guide)
|
|
|
|
//
|
|
|
|
// ```impl<P0..Pn> Trait<A1..An> for A0
|
|
|
|
// {
|
2018-06-04 06:57:56 -05:00
|
|
|
// type AssocType<Pn+1..Pm> = T;
|
2018-04-03 10:53:13 -05:00
|
|
|
// }```
|
|
|
|
//
|
2018-06-06 12:03:56 -05:00
|
|
|
// FIXME: For the moment, we don't account for where clauses written on the associated
|
|
|
|
// ty definition (i.e. in the trait def, as in `type AssocType<T> where T: Sized`).
|
2018-04-03 10:53:13 -05:00
|
|
|
// ```
|
|
|
|
// forall<P0..Pm> {
|
|
|
|
// forall<Pn+1..Pm> {
|
|
|
|
// Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
|
2018-06-04 06:57:56 -05:00
|
|
|
// Implemented(A0: Trait<A1..An>)
|
2018-04-03 10:53:13 -05:00
|
|
|
// }
|
|
|
|
// }
|
|
|
|
// ```
|
|
|
|
|
|
|
|
let item = tcx.associated_item(item_id);
|
|
|
|
debug_assert_eq!(item.kind, ty::AssociatedKind::Type);
|
2018-06-04 06:57:56 -05:00
|
|
|
let impl_id = match item.container {
|
|
|
|
ty::AssociatedItemContainer::ImplContainer(impl_id) => impl_id,
|
|
|
|
_ => bug!("not an impl container"),
|
2018-04-03 10:53:13 -05:00
|
|
|
};
|
2018-06-06 12:03:56 -05:00
|
|
|
|
2018-04-03 10:53:13 -05:00
|
|
|
// `A0 as Trait<A1..An>`
|
|
|
|
let trait_ref = tcx.impl_trait_ref(impl_id).unwrap();
|
2018-06-04 06:57:56 -05:00
|
|
|
|
2018-04-03 10:53:13 -05:00
|
|
|
// `T`
|
|
|
|
let ty = tcx.type_of(item_id);
|
2018-06-04 06:57:56 -05:00
|
|
|
|
2018-04-11 14:20:25 -05:00
|
|
|
// `Implemented(A0: Trait<A1..An>)`
|
|
|
|
let trait_implemented = ty::Binder::dummy(ty::TraitPredicate { trait_ref }.lower());
|
2018-06-04 06:57:56 -05:00
|
|
|
|
|
|
|
// `Implemented(A0: Trait<A1..An>)`
|
|
|
|
let hypotheses = vec![trait_implemented];
|
|
|
|
|
2018-04-03 10:53:13 -05:00
|
|
|
// `<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm>`
|
2018-06-10 14:24:24 -05:00
|
|
|
let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident);
|
2018-06-04 06:57:56 -05:00
|
|
|
|
2018-04-03 10:53:13 -05:00
|
|
|
// `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T)`
|
|
|
|
let normalize_goal = DomainGoal::Normalize(ty::ProjectionPredicate { projection_ty, ty });
|
2018-06-04 06:57:56 -05:00
|
|
|
|
2018-04-11 14:20:25 -05:00
|
|
|
// `Normalize(... -> T) :- ...`
|
2018-04-11 07:27:00 -05:00
|
|
|
let clause = ProgramClause {
|
|
|
|
goal: normalize_goal,
|
2018-04-15 16:49:41 -05:00
|
|
|
hypotheses: tcx.mk_goals(
|
2018-06-04 06:57:56 -05:00
|
|
|
hypotheses
|
2018-04-10 04:56:35 -05:00
|
|
|
.into_iter()
|
|
|
|
.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
|
2018-04-15 16:49:41 -05:00
|
|
|
),
|
2018-04-11 07:27:00 -05:00
|
|
|
};
|
2018-05-16 02:43:24 -05:00
|
|
|
tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))])
|
2018-04-03 10:53:13 -05:00
|
|
|
}
|
|
|
|
|
2018-03-10 05:44:33 -06:00
|
|
|
pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
|
|
|
|
if !tcx.features().rustc_attrs {
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
|
|
|
let mut visitor = ClauseDumper { tcx };
|
2018-04-10 04:56:35 -05:00
|
|
|
tcx.hir
|
|
|
|
.krate()
|
|
|
|
.visit_all_item_likes(&mut visitor.as_deep_visitor());
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
|
|
|
|
|
|
|
struct ClauseDumper<'a, 'tcx: 'a> {
|
|
|
|
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
|
|
|
}
|
|
|
|
|
2018-04-10 04:56:35 -05:00
|
|
|
impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
|
2018-03-10 05:44:33 -06:00
|
|
|
fn process_attrs(&mut self, node_id: ast::NodeId, attrs: &[ast::Attribute]) {
|
|
|
|
let def_id = self.tcx.hir.local_def_id(node_id);
|
|
|
|
for attr in attrs {
|
2018-04-18 18:58:22 -05:00
|
|
|
let mut clauses = None;
|
|
|
|
|
2018-03-10 05:44:33 -06:00
|
|
|
if attr.check_name("rustc_dump_program_clauses") {
|
2018-04-18 18:58:22 -05:00
|
|
|
clauses = Some(self.tcx.program_clauses_for(def_id));
|
|
|
|
}
|
|
|
|
|
|
|
|
if attr.check_name("rustc_dump_env_program_clauses") {
|
|
|
|
let param_env = self.tcx.param_env(def_id);
|
|
|
|
clauses = Some(self.tcx.program_clauses_for_env(param_env));
|
|
|
|
}
|
|
|
|
|
|
|
|
if let Some(clauses) = clauses {
|
2018-05-01 19:02:47 -05:00
|
|
|
let mut err = self
|
|
|
|
.tcx
|
2018-04-18 18:58:22 -05:00
|
|
|
.sess
|
|
|
|
.struct_span_err(attr.span, "program clause dump");
|
|
|
|
|
2018-04-17 05:06:33 -05:00
|
|
|
let mut strings: Vec<_> = clauses
|
|
|
|
.iter()
|
|
|
|
.map(|clause| {
|
|
|
|
// Skip the top-level binder for a less verbose output
|
|
|
|
let program_clause = match clause {
|
|
|
|
Clause::Implies(program_clause) => program_clause,
|
|
|
|
Clause::ForAll(program_clause) => program_clause.skip_binder(),
|
|
|
|
};
|
|
|
|
format!("{}", program_clause)
|
|
|
|
})
|
|
|
|
.collect();
|
|
|
|
|
|
|
|
strings.sort();
|
|
|
|
|
|
|
|
for string in strings {
|
|
|
|
err.note(&string);
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
2018-04-18 18:58:22 -05:00
|
|
|
|
|
|
|
err.emit();
|
2018-03-10 05:44:33 -06:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<'a, 'tcx> Visitor<'tcx> for ClauseDumper<'a, 'tcx> {
|
|
|
|
fn nested_visit_map<'this>(&'this mut self) -> NestedVisitorMap<'this, 'tcx> {
|
|
|
|
NestedVisitorMap::OnlyBodies(&self.tcx.hir)
|
|
|
|
}
|
|
|
|
|
|
|
|
fn visit_item(&mut self, item: &'tcx hir::Item) {
|
|
|
|
self.process_attrs(item.id, &item.attrs);
|
|
|
|
intravisit::walk_item(self, item);
|
|
|
|
}
|
|
|
|
|
|
|
|
fn visit_trait_item(&mut self, trait_item: &'tcx hir::TraitItem) {
|
|
|
|
self.process_attrs(trait_item.id, &trait_item.attrs);
|
|
|
|
intravisit::walk_trait_item(self, trait_item);
|
|
|
|
}
|
|
|
|
|
|
|
|
fn visit_impl_item(&mut self, impl_item: &'tcx hir::ImplItem) {
|
|
|
|
self.process_attrs(impl_item.id, &impl_item.attrs);
|
|
|
|
intravisit::walk_impl_item(self, impl_item);
|
|
|
|
}
|
|
|
|
|
|
|
|
fn visit_struct_field(&mut self, s: &'tcx hir::StructField) {
|
|
|
|
self.process_attrs(s.id, &s.attrs);
|
|
|
|
intravisit::walk_struct_field(self, s);
|
|
|
|
}
|
|
|
|
}
|