Auto merge of #48985 - scalexm:lowering, r=nikomatsakis

MVP for chalkification

r? @nikomatsakis

14 files changed, 526 insertions, 3 deletions

diff --git a/src/librustc/dep_graph/dep_node.rs b/src/librustc/dep_graph/dep_node.rs
index 8d7fef90b75..744e3a5eaab 100644
--- a/src/librustc/dep_graph/dep_node.rs
+++ b/src/librustc/dep_graph/dep_node.rs
@@ -648,6 +648,8 @@ define_dep_nodes!( <'tcx>
     [] GetSymbolExportLevel(DefId),
 
     [input] Features,
+
+    [] ProgramClausesFor(DefId),
 );
 
 trait DepNodeParams<'a, 'gcx: 'tcx + 'a, 'tcx: 'a> : fmt::Debug {
diff --git a/src/librustc/ich/impls_ty.rs b/src/librustc/ich/impls_ty.rs
index bb3051b546e..7f91bbd6ea2 100644
--- a/src/librustc/ich/impls_ty.rs
+++ b/src/librustc/ich/impls_ty.rs
@@ -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
+});
diff --git a/src/librustc/traits/mod.rs b/src/librustc/traits/mod.rs
index bd8f99780f9..a0ba88f7d55 100644
--- a/src/librustc/traits/mod.rs
+++ b/src/librustc/traits/mod.rs
@@ -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)]
diff --git a/src/librustc/traits/structural_impls.rs b/src/librustc/traits/structural_impls.rs
index a2d98a456f4..d6e6f0e98ad 100644
--- a/src/librustc/traits/structural_impls.rs
+++ b/src/librustc/traits/structural_impls.rs
@@ -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),
+    }
+}
diff --git a/src/librustc/ty/maps/config.rs b/src/librustc/ty/maps/config.rs
index 11675f54287..a3a0e26a843 100644
--- a/src/librustc/ty/maps/config.rs
+++ b/src/librustc/ty/maps/config.rs
@@ -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> {
diff --git a/src/librustc/ty/maps/mod.rs b/src/librustc/ty/maps/mod.rs
index c1783654eff..b6b7361bb2f 100644
--- a/src/librustc/ty/maps/mod.rs
+++ b/src/librustc/ty/maps/mod.rs
@@ -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>>>,
 }
 
 //////////////////////////////////////////////////////////////////////
diff --git a/src/librustc/ty/maps/plumbing.rs b/src/librustc/ty/maps/plumbing.rs
index bc7186f781a..dd65d4b4190 100644
--- a/src/librustc/ty/maps/plumbing.rs
+++ b/src/librustc/ty/maps/plumbing.rs
@@ -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
diff --git a/src/librustc/ty/mod.rs b/src/librustc/ty/mod.rs
index 09b11a36352..c9150223519 100644
--- a/src/librustc/ty/mod.rs
+++ b/src/librustc/ty/mod.rs
@@ -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> {
diff --git a/src/librustc_driver/driver.rs b/src/librustc_driver/driver.rs
index 710fef8db40..f2fe6542db1 100644
--- a/src/librustc_driver/driver.rs
+++ b/src/librustc_driver/driver.rs
@@ -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()));
     })
 }
diff --git a/src/librustc_traits/lib.rs b/src/librustc_traits/lib.rs
index 45d23a2733a..2a0f076cefd 100644
--- a/src/librustc_traits/lib.rs
+++ b/src/librustc_traits/lib.rs
@@ -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
     };
 }
diff --git a/src/librustc_traits/lowering.rs b/src/librustc_traits/lowering.rs
new file mode 100644
index 00000000000..c9666f55d44
--- /dev/null
+++ b/src/librustc_traits/lowering.rs
@@ -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);
+    }
+}
diff --git a/src/libsyntax/feature_gate.rs b/src/libsyntax/feature_gate.rs
index a5af8564057..fa600cd6860 100644
--- a/src/libsyntax/feature_gate.rs
+++ b/src/libsyntax/feature_gate.rs
@@ -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",
diff --git a/src/test/ui/chalkify/lower_impl.rs b/src/test/ui/chalkify/lower_impl.rs
new file mode 100644
index 00000000000..2083ada6d2d
--- /dev/null
+++ b/src/test/ui/chalkify/lower_impl.rs
@@ -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");
+}
diff --git a/src/test/ui/chalkify/lower_impl.stderr b/src/test/ui/chalkify/lower_impl.stderr
new file mode 100644
index 00000000000..b5d791d640a
--- /dev/null
+++ b/src/test/ui/chalkify/lower_impl.stderr
@@ -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
+