Auto merge of #48985 - scalexm:lowering, r=nikomatsakis
MVP for chalkification r? @nikomatsakis
This commit is contained in:
bors
commit
7c396ebd0b
14 changed files with 526 additions and 3 deletions
|
|
@ -648,6 +648,8 @@ define_dep_nodes!( <'tcx>
|
|||
[] GetSymbolExportLevel(DefId),
|
||||
|
||||
[input] Features,
|
||||
|
||||
[] ProgramClausesFor(DefId),
|
||||
);
|
||||
|
||||
trait DepNodeParams<'a, 'gcx: 'tcx + 'a, 'tcx: 'a> : fmt::Debug {
|
||||
|
|
|
|||
|
|
@ -1285,3 +1285,86 @@ impl_stable_hash_for!(struct infer::canonical::QueryRegionConstraints<'tcx> {
|
|||
impl_stable_hash_for!(enum infer::canonical::Certainty {
|
||||
Proven, Ambiguous
|
||||
});
|
||||
|
||||
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::WhereClauseAtom<'tcx> {
|
||||
fn hash_stable<W: StableHasherResult>(&self,
|
||||
hcx: &mut StableHashingContext<'a>,
|
||||
hasher: &mut StableHasher<W>) {
|
||||
use traits::WhereClauseAtom::*;
|
||||
|
||||
mem::discriminant(self).hash_stable(hcx, hasher);
|
||||
match self {
|
||||
Implemented(trait_ref) => trait_ref.hash_stable(hcx, hasher),
|
||||
ProjectionEq(projection) => projection.hash_stable(hcx, hasher),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::DomainGoal<'tcx> {
|
||||
fn hash_stable<W: StableHasherResult>(&self,
|
||||
hcx: &mut StableHashingContext<'a>,
|
||||
hasher: &mut StableHasher<W>) {
|
||||
use traits::DomainGoal::*;
|
||||
|
||||
mem::discriminant(self).hash_stable(hcx, hasher);
|
||||
match self {
|
||||
Holds(where_clause) |
|
||||
WellFormed(where_clause) |
|
||||
FromEnv(where_clause) => where_clause.hash_stable(hcx, hasher),
|
||||
|
||||
WellFormedTy(ty) => ty.hash_stable(hcx, hasher),
|
||||
FromEnvTy(ty) => ty.hash_stable(hcx, hasher),
|
||||
RegionOutlives(predicate) => predicate.hash_stable(hcx, hasher),
|
||||
TypeOutlives(predicate) => predicate.hash_stable(hcx, hasher),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Goal<'tcx> {
|
||||
fn hash_stable<W: StableHasherResult>(&self,
|
||||
hcx: &mut StableHashingContext<'a>,
|
||||
hasher: &mut StableHasher<W>) {
|
||||
use traits::Goal::*;
|
||||
|
||||
mem::discriminant(self).hash_stable(hcx, hasher);
|
||||
match self {
|
||||
Implies(hypotheses, goal) => {
|
||||
hypotheses.hash_stable(hcx, hasher);
|
||||
goal.hash_stable(hcx, hasher);
|
||||
},
|
||||
And(goal1, goal2) => {
|
||||
goal1.hash_stable(hcx, hasher);
|
||||
goal2.hash_stable(hcx, hasher);
|
||||
}
|
||||
Not(goal) => goal.hash_stable(hcx, hasher),
|
||||
DomainGoal(domain_goal) => domain_goal.hash_stable(hcx, hasher),
|
||||
Quantified(quantifier, goal) => {
|
||||
quantifier.hash_stable(hcx, hasher);
|
||||
goal.hash_stable(hcx, hasher);
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Clause<'tcx> {
|
||||
fn hash_stable<W: StableHasherResult>(&self,
|
||||
hcx: &mut StableHashingContext<'a>,
|
||||
hasher: &mut StableHasher<W>) {
|
||||
use traits::Clause::*;
|
||||
|
||||
mem::discriminant(self).hash_stable(hcx, hasher);
|
||||
match self {
|
||||
Implies(hypotheses, goal) => {
|
||||
hypotheses.hash_stable(hcx, hasher);
|
||||
goal.hash_stable(hcx, hasher);
|
||||
}
|
||||
DomainGoal(domain_goal) => domain_goal.hash_stable(hcx, hasher),
|
||||
ForAll(clause) => clause.hash_stable(hcx, hasher),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl_stable_hash_for!(enum traits::QuantifierKind {
|
||||
Universal,
|
||||
Existential
|
||||
});
|
||||
|
|
|
|||
|
|
@ -29,6 +29,7 @@ use infer::{InferCtxt};
|
|||
|
||||
use rustc_data_structures::sync::Lrc;
|
||||
use std::rc::Rc;
|
||||
use std::convert::From;
|
||||
use syntax::ast;
|
||||
use syntax_pos::{Span, DUMMY_SP};
|
||||
|
||||
|
|
@ -244,6 +245,69 @@ pub type Obligations<'tcx, O> = Vec<Obligation<'tcx, O>>;
|
|||
pub type PredicateObligations<'tcx> = Vec<PredicateObligation<'tcx>>;
|
||||
pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
|
||||
|
||||
/// The following types:
|
||||
/// * `WhereClauseAtom`
|
||||
/// * `DomainGoal`
|
||||
/// * `Goal`
|
||||
/// * `Clause`
|
||||
/// are used for representing the trait system in the form of
|
||||
/// logic programming clauses. They are part of the interface
|
||||
/// for the chalk SLG solver.
|
||||
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
|
||||
pub enum WhereClauseAtom<'tcx> {
|
||||
Implemented(ty::TraitPredicate<'tcx>),
|
||||
ProjectionEq(ty::ProjectionPredicate<'tcx>),
|
||||
}
|
||||
|
||||
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
|
||||
pub enum DomainGoal<'tcx> {
|
||||
Holds(WhereClauseAtom<'tcx>),
|
||||
WellFormed(WhereClauseAtom<'tcx>),
|
||||
FromEnv(WhereClauseAtom<'tcx>),
|
||||
WellFormedTy(Ty<'tcx>),
|
||||
FromEnvTy(Ty<'tcx>),
|
||||
RegionOutlives(ty::RegionOutlivesPredicate<'tcx>),
|
||||
TypeOutlives(ty::TypeOutlivesPredicate<'tcx>),
|
||||
}
|
||||
|
||||
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub enum QuantifierKind {
|
||||
Universal,
|
||||
Existential,
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub enum Goal<'tcx> {
|
||||
// FIXME: use interned refs instead of `Box`
|
||||
Implies(Vec<Clause<'tcx>>, Box<Goal<'tcx>>),
|
||||
And(Box<Goal<'tcx>>, Box<Goal<'tcx>>),
|
||||
Not(Box<Goal<'tcx>>),
|
||||
DomainGoal(DomainGoal<'tcx>),
|
||||
Quantified(QuantifierKind, Box<ty::Binder<Goal<'tcx>>>)
|
||||
}
|
||||
|
||||
impl<'tcx> From<DomainGoal<'tcx>> for Goal<'tcx> {
|
||||
fn from(domain_goal: DomainGoal<'tcx>) -> Self {
|
||||
Goal::DomainGoal(domain_goal)
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> From<DomainGoal<'tcx>> for Clause<'tcx> {
|
||||
fn from(domain_goal: DomainGoal<'tcx>) -> Self {
|
||||
Clause::DomainGoal(domain_goal)
|
||||
}
|
||||
}
|
||||
|
||||
/// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
|
||||
/// Harrop Formulas".
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub enum Clause<'tcx> {
|
||||
// FIXME: again, use interned refs instead of `Box`
|
||||
Implies(Vec<Goal<'tcx>>, DomainGoal<'tcx>),
|
||||
DomainGoal(DomainGoal<'tcx>),
|
||||
ForAll(Box<ty::Binder<Clause<'tcx>>>),
|
||||
}
|
||||
|
||||
pub type Selection<'tcx> = Vtable<'tcx, PredicateObligation<'tcx>>;
|
||||
|
||||
#[derive(Clone,Debug)]
|
||||
|
|
|
|||
|
|
@ -425,3 +425,138 @@ BraceStructTypeFoldableImpl! {
|
|||
obligations
|
||||
} where T: TypeFoldable<'tcx>
|
||||
}
|
||||
|
||||
impl<'tcx> fmt::Display for traits::WhereClauseAtom<'tcx> {
|
||||
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
|
||||
use traits::WhereClauseAtom::*;
|
||||
|
||||
match self {
|
||||
Implemented(trait_ref) => write!(fmt, "Implemented({})", trait_ref),
|
||||
ProjectionEq(projection) => write!(fmt, "ProjectionEq({})", projection),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> fmt::Display for traits::DomainGoal<'tcx> {
|
||||
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
|
||||
use traits::DomainGoal::*;
|
||||
use traits::WhereClauseAtom::*;
|
||||
|
||||
match self {
|
||||
Holds(wc) => write!(fmt, "{}", wc),
|
||||
WellFormed(Implemented(trait_ref)) => write!(fmt, "WellFormed({})", trait_ref),
|
||||
WellFormed(ProjectionEq(projection)) => write!(fmt, "WellFormed({})", projection),
|
||||
FromEnv(Implemented(trait_ref)) => write!(fmt, "FromEnv({})", trait_ref),
|
||||
FromEnv(ProjectionEq(projection)) => write!(fmt, "FromEnv({})", projection),
|
||||
WellFormedTy(ty) => write!(fmt, "WellFormed({})", ty),
|
||||
FromEnvTy(ty) => write!(fmt, "FromEnv({})", ty),
|
||||
RegionOutlives(predicate) => write!(fmt, "RegionOutlives({})", predicate),
|
||||
TypeOutlives(predicate) => write!(fmt, "TypeOutlives({})", predicate),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl fmt::Display for traits::QuantifierKind {
|
||||
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
|
||||
use traits::QuantifierKind::*;
|
||||
|
||||
match self {
|
||||
Universal => write!(fmt, "forall"),
|
||||
Existential => write!(fmt, "exists"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> fmt::Display for traits::Goal<'tcx> {
|
||||
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
|
||||
use traits::Goal::*;
|
||||
|
||||
match self {
|
||||
Implies(hypotheses, goal) => {
|
||||
write!(fmt, "if (")?;
|
||||
for (index, hyp) in hypotheses.iter().enumerate() {
|
||||
if index > 0 {
|
||||
write!(fmt, ", ")?;
|
||||
}
|
||||
write!(fmt, "{}", hyp)?;
|
||||
}
|
||||
write!(fmt, ") {{ {} }}", goal)
|
||||
}
|
||||
And(goal1, goal2) => write!(fmt, "({} && {})", goal1, goal2),
|
||||
Not(goal) => write!(fmt, "not {{ {} }}", goal),
|
||||
DomainGoal(goal) => write!(fmt, "{}", goal),
|
||||
Quantified(qkind, goal) => {
|
||||
// FIXME: appropriate binder names
|
||||
write!(fmt, "{}<> {{ {} }}", qkind, goal.skip_binder())
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> fmt::Display for traits::Clause<'tcx> {
|
||||
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
|
||||
use traits::Clause::*;
|
||||
|
||||
match self {
|
||||
Implies(hypotheses, goal) => {
|
||||
write!(fmt, "{}", goal)?;
|
||||
if !hypotheses.is_empty() {
|
||||
write!(fmt, " :- ")?;
|
||||
for (index, condition) in hypotheses.iter().enumerate() {
|
||||
if index > 0 {
|
||||
write!(fmt, ", ")?;
|
||||
}
|
||||
write!(fmt, "{}", condition)?;
|
||||
}
|
||||
}
|
||||
write!(fmt, ".")
|
||||
}
|
||||
DomainGoal(domain_goal) => write!(fmt, "{}.", domain_goal),
|
||||
ForAll(clause) => {
|
||||
// FIXME: appropriate binder names
|
||||
write!(fmt, "forall<> {{ {} }}", clause.skip_binder())
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
EnumTypeFoldableImpl! {
|
||||
impl<'tcx> TypeFoldable<'tcx> for traits::WhereClauseAtom<'tcx> {
|
||||
(traits::WhereClauseAtom::Implemented)(trait_ref),
|
||||
(traits::WhereClauseAtom::ProjectionEq)(projection),
|
||||
}
|
||||
}
|
||||
|
||||
EnumTypeFoldableImpl! {
|
||||
impl<'tcx> TypeFoldable<'tcx> for traits::DomainGoal<'tcx> {
|
||||
(traits::DomainGoal::Holds)(wc),
|
||||
(traits::DomainGoal::WellFormed)(wc),
|
||||
(traits::DomainGoal::FromEnv)(wc),
|
||||
(traits::DomainGoal::WellFormedTy)(ty),
|
||||
(traits::DomainGoal::FromEnvTy)(ty),
|
||||
(traits::DomainGoal::RegionOutlives)(predicate),
|
||||
(traits::DomainGoal::TypeOutlives)(predicate),
|
||||
}
|
||||
}
|
||||
|
||||
CloneTypeFoldableImpls! {
|
||||
traits::QuantifierKind,
|
||||
}
|
||||
|
||||
EnumTypeFoldableImpl! {
|
||||
impl<'tcx> TypeFoldable<'tcx> for traits::Goal<'tcx> {
|
||||
(traits::Goal::Implies)(hypotheses, goal),
|
||||
(traits::Goal::And)(goal1, goal2),
|
||||
(traits::Goal::Not)(goal),
|
||||
(traits::Goal::DomainGoal)(domain_goal),
|
||||
(traits::Goal::Quantified)(qkind, goal),
|
||||
}
|
||||
}
|
||||
|
||||
EnumTypeFoldableImpl! {
|
||||
impl<'tcx> TypeFoldable<'tcx> for traits::Clause<'tcx> {
|
||||
(traits::Clause::Implies)(hypotheses, goal),
|
||||
(traits::Clause::DomainGoal)(domain_goal),
|
||||
(traits::Clause::ForAll)(clause),
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -693,6 +693,12 @@ impl<'tcx> QueryDescription<'tcx> for queries::generics_of<'tcx> {
|
|||
}
|
||||
}
|
||||
|
||||
impl<'tcx> QueryDescription<'tcx> for queries::program_clauses_for<'tcx> {
|
||||
fn describe(_tcx: TyCtxt, _: DefId) -> String {
|
||||
format!("generating chalk-style clauses")
|
||||
}
|
||||
}
|
||||
|
||||
macro_rules! impl_disk_cacheable_query(
|
||||
($query_name:ident, |$key:tt| $cond:expr) => {
|
||||
impl<'tcx> QueryDescription<'tcx> for queries::$query_name<'tcx> {
|
||||
|
|
|
|||
|
|
@ -38,6 +38,7 @@ use traits::query::{CanonicalProjectionGoal, CanonicalTyGoal, NoSolution};
|
|||
use traits::query::dropck_outlives::{DtorckConstraint, DropckOutlivesResult};
|
||||
use traits::query::normalize::NormalizationResult;
|
||||
use traits::specialization_graph;
|
||||
use traits::Clause;
|
||||
use ty::{self, CrateInherentImpls, ParamEnvAnd, Ty, TyCtxt};
|
||||
use ty::steal::Steal;
|
||||
use ty::subst::Substs;
|
||||
|
|
@ -417,6 +418,8 @@ define_maps! { <'tcx>
|
|||
-> usize,
|
||||
|
||||
[] fn features_query: features_node(CrateNum) -> Lrc<feature_gate::Features>,
|
||||
|
||||
[] fn program_clauses_for: ProgramClausesFor(DefId) -> Lrc<Vec<Clause<'tcx>>>,
|
||||
}
|
||||
|
||||
//////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -935,6 +935,8 @@ pub fn force_from_dep_node<'a, 'gcx, 'lcx>(tcx: TyCtxt<'a, 'gcx, 'lcx>,
|
|||
|
||||
DepKind::GetSymbolExportLevel => { force!(symbol_export_level, def_id!()); }
|
||||
DepKind::Features => { force!(features_query, LOCAL_CRATE); }
|
||||
|
||||
DepKind::ProgramClausesFor => { force!(program_clauses_for, def_id!()); }
|
||||
}
|
||||
|
||||
true
|
||||
|
|
|
|||
|
|
@ -1073,9 +1073,12 @@ impl<'tcx> PolyTraitPredicate<'tcx> {
|
|||
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, RustcEncodable, RustcDecodable)]
|
||||
pub struct OutlivesPredicate<A,B>(pub A, pub B); // `A : B`
|
||||
pub type PolyOutlivesPredicate<A,B> = ty::Binder<OutlivesPredicate<A,B>>;
|
||||
pub type PolyRegionOutlivesPredicate<'tcx> = PolyOutlivesPredicate<ty::Region<'tcx>,
|
||||
ty::Region<'tcx>>;
|
||||
pub type PolyTypeOutlivesPredicate<'tcx> = PolyOutlivesPredicate<Ty<'tcx>, ty::Region<'tcx>>;
|
||||
pub type RegionOutlivesPredicate<'tcx> = OutlivesPredicate<ty::Region<'tcx>,
|
||||
ty::Region<'tcx>>;
|
||||
pub type TypeOutlivesPredicate<'tcx> = OutlivesPredicate<Ty<'tcx>,
|
||||
ty::Region<'tcx>>;
|
||||
pub type PolyRegionOutlivesPredicate<'tcx> = ty::Binder<RegionOutlivesPredicate<'tcx>>;
|
||||
pub type PolyTypeOutlivesPredicate<'tcx> = ty::Binder<TypeOutlivesPredicate<'tcx>>;
|
||||
|
||||
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, RustcEncodable, RustcDecodable)]
|
||||
pub struct SubtypePredicate<'tcx> {
|
||||
|
|
|
|||
|
|
@ -1091,6 +1091,10 @@ pub fn phase_3_run_analysis_passes<'tcx, F, R>(trans: &TransCrate,
|
|||
|
||||
time(sess, "lint checking", || lint::check_crate(tcx));
|
||||
|
||||
time(sess,
|
||||
"dumping chalk-like clauses",
|
||||
|| rustc_traits::lowering::dump_program_clauses(tcx));
|
||||
|
||||
return Ok(f(tcx, analysis, rx, tcx.sess.compile_status()));
|
||||
})
|
||||
}
|
||||
|
|
|
|||
|
|
@ -29,6 +29,7 @@ mod dropck_outlives;
|
|||
mod normalize_projection_ty;
|
||||
mod normalize_erasing_regions;
|
||||
mod util;
|
||||
pub mod lowering;
|
||||
|
||||
use rustc::ty::maps::Providers;
|
||||
|
||||
|
|
@ -39,6 +40,7 @@ pub fn provide(p: &mut Providers) {
|
|||
normalize_projection_ty: normalize_projection_ty::normalize_projection_ty,
|
||||
normalize_ty_after_erasing_regions:
|
||||
normalize_erasing_regions::normalize_ty_after_erasing_regions,
|
||||
program_clauses_for: lowering::program_clauses_for,
|
||||
..*p
|
||||
};
|
||||
}
|
||||
|
|
|
|||
184
src/librustc_traits/lowering.rs
Normal file
184
src/librustc_traits/lowering.rs
Normal file
|
|
@ -0,0 +1,184 @@
|
|||
// 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.
|
||||
|
||||
use rustc::hir::{self, ImplPolarity};
|
||||
use rustc::hir::def_id::DefId;
|
||||
use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
|
||||
use rustc::ty::{self, TyCtxt};
|
||||
use rustc::traits::{QuantifierKind, Goal, DomainGoal, Clause, WhereClauseAtom};
|
||||
use syntax::ast;
|
||||
use rustc_data_structures::sync::Lrc;
|
||||
|
||||
trait Lower<T> {
|
||||
/// Lower a rustc construction (e.g. `ty::TraitPredicate`) to a chalk-like type.
|
||||
fn lower(&self) -> T;
|
||||
}
|
||||
|
||||
impl<T, U> Lower<Vec<U>> for Vec<T> where T: Lower<U> {
|
||||
fn lower(&self) -> Vec<U> {
|
||||
self.iter().map(|item| item.lower()).collect()
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Lower<WhereClauseAtom<'tcx>> for ty::TraitPredicate<'tcx> {
|
||||
fn lower(&self) -> WhereClauseAtom<'tcx> {
|
||||
WhereClauseAtom::Implemented(*self)
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Lower<WhereClauseAtom<'tcx>> for ty::ProjectionPredicate<'tcx> {
|
||||
fn lower(&self) -> WhereClauseAtom<'tcx> {
|
||||
WhereClauseAtom::ProjectionEq(*self)
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx, T> Lower<DomainGoal<'tcx>> for T where T: Lower<WhereClauseAtom<'tcx>> {
|
||||
fn lower(&self) -> DomainGoal<'tcx> {
|
||||
DomainGoal::Holds(self.lower())
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Lower<DomainGoal<'tcx>> for ty::RegionOutlivesPredicate<'tcx> {
|
||||
fn lower(&self) -> DomainGoal<'tcx> {
|
||||
DomainGoal::RegionOutlives(*self)
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Lower<DomainGoal<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
|
||||
fn lower(&self) -> DomainGoal<'tcx> {
|
||||
DomainGoal::TypeOutlives(*self)
|
||||
}
|
||||
}
|
||||
|
||||
/// `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
|
||||
/// example), we model them with quantified goals, e.g. as for the previous example:
|
||||
/// `forall<'a> { T: Fn(&'a i32) }` which corresponds to something like
|
||||
/// `Binder<Holds(Implemented(TraitPredicate))>`.
|
||||
///
|
||||
/// Also, if `self` does not contain generic lifetimes, we can safely drop the binder and we
|
||||
/// can directly lower to a leaf goal instead of a quantified goal.
|
||||
impl<'tcx, T> Lower<Goal<'tcx>> for ty::Binder<T>
|
||||
where T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx> + Copy
|
||||
{
|
||||
fn lower(&self) -> Goal<'tcx> {
|
||||
match self.no_late_bound_regions() {
|
||||
Some(p) => p.lower().into(),
|
||||
None => Goal::Quantified(
|
||||
QuantifierKind::Universal,
|
||||
Box::new(self.map_bound(|p| p.lower().into()))
|
||||
),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Lower<Goal<'tcx>> for ty::Predicate<'tcx> {
|
||||
fn lower(&self) -> Goal<'tcx> {
|
||||
use rustc::ty::Predicate::*;
|
||||
|
||||
match self {
|
||||
Trait(predicate) => predicate.lower(),
|
||||
RegionOutlives(predicate) => predicate.lower(),
|
||||
TypeOutlives(predicate) => predicate.lower(),
|
||||
Projection(predicate) => predicate.lower(),
|
||||
WellFormed(ty) => DomainGoal::WellFormedTy(*ty).into(),
|
||||
ObjectSafe(..) |
|
||||
ClosureKind(..) |
|
||||
Subtype(..) |
|
||||
ConstEvaluatable(..) => unimplemented!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
|
||||
-> Lrc<Vec<Clause<'tcx>>>
|
||||
{
|
||||
let node_id = tcx.hir.as_local_node_id(def_id).unwrap();
|
||||
let item = tcx.hir.expect_item(node_id);
|
||||
match item.node {
|
||||
hir::ItemImpl(..) => program_clauses_for_impl(tcx, def_id),
|
||||
|
||||
// FIXME: other constructions e.g. traits, associated types...
|
||||
_ => Lrc::new(vec![]),
|
||||
}
|
||||
}
|
||||
|
||||
fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
|
||||
-> Lrc<Vec<Clause<'tcx>>>
|
||||
{
|
||||
if let ImplPolarity::Negative = tcx.impl_polarity(def_id) {
|
||||
return Lrc::new(vec![]);
|
||||
}
|
||||
|
||||
// Rule Implemented-From-Impl
|
||||
//
|
||||
// (see rustc guide)
|
||||
|
||||
let trait_ref = tcx.impl_trait_ref(def_id).unwrap();
|
||||
let trait_ref = ty::TraitPredicate { trait_ref }.lower();
|
||||
let where_clauses = tcx.predicates_of(def_id).predicates.lower();
|
||||
|
||||
let clause = Clause::Implies(where_clauses, trait_ref);
|
||||
Lrc::new(vec![clause])
|
||||
}
|
||||
|
||||
pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
|
||||
if !tcx.features().rustc_attrs {
|
||||
return;
|
||||
}
|
||||
|
||||
let mut visitor = ClauseDumper { tcx };
|
||||
tcx.hir.krate().visit_all_item_likes(&mut visitor.as_deep_visitor());
|
||||
}
|
||||
|
||||
struct ClauseDumper<'a, 'tcx: 'a> {
|
||||
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
||||
}
|
||||
|
||||
impl <'a, 'tcx> ClauseDumper<'a, 'tcx > {
|
||||
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 {
|
||||
if attr.check_name("rustc_dump_program_clauses") {
|
||||
let clauses = self.tcx.program_clauses_for(def_id);
|
||||
for clause in &*clauses {
|
||||
self.tcx.sess.struct_span_err(attr.span, &format!("{}", clause)).emit();
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
|
@ -832,6 +832,13 @@ pub const BUILTIN_ATTRIBUTES: &'static [(&'static str, AttributeType, AttributeG
|
|||
across crates and will never be stable",
|
||||
cfg_fn!(rustc_attrs))),
|
||||
|
||||
("rustc_dump_program_clauses", Whitelisted, Gated(Stability::Unstable,
|
||||
"rustc_attrs",
|
||||
"the `#[rustc_dump_program_clauses]` \
|
||||
attribute is just used for rustc unit \
|
||||
tests and will never be stable",
|
||||
cfg_fn!(rustc_attrs))),
|
||||
|
||||
// RFC #2094
|
||||
("nll", Whitelisted, Gated(Stability::Unstable,
|
||||
"nll",
|
||||
|
|
|
|||
20
src/test/ui/chalkify/lower_impl.rs
Normal file
20
src/test/ui/chalkify/lower_impl.rs
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
// 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.
|
||||
|
||||
#![feature(rustc_attrs)]
|
||||
|
||||
trait Foo { }
|
||||
|
||||
#[rustc_dump_program_clauses] //~ ERROR Implemented(T: Foo) :-
|
||||
impl<T: 'static> Foo for T where T: Iterator<Item = i32> { }
|
||||
|
||||
fn main() {
|
||||
println!("hello");
|
||||
}
|
||||
8
src/test/ui/chalkify/lower_impl.stderr
Normal file
8
src/test/ui/chalkify/lower_impl.stderr
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
error: Implemented(T: Foo) :- ProjectionEq(<T as std::iter::Iterator>::Item == i32), TypeOutlives(T : 'static), Implemented(T: std::iter::Iterator), Implemented(T: std::marker::Sized).
|
||||
--> $DIR/lower_impl.rs:15:1
|
||||
|
|
||||
LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(T: Foo) :-
|
||||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
error: aborting due to previous error
|
||||
|
||||
Loading…
Add table
Reference in a new issue