Rollup merge of rust-lang#49211 - varkor:chalk-lowering-Implemented-From-Env, r=nikomatsakis

Implement Chalk lowering rule "Implemented-From-Env"

This extends the Chalk lowering pass with the "Implemented-From-Env" rule for generating program clauses from a trait definition as part of rust-lang#49177.

r? @nikomatsakis

Author: kennytm

src/librustc_traits/lowering.rs

@@ -12,6 +12,7 @@ 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::ty::subst::Substs;
 use rustc::traits::{QuantifierKind, Goal, DomainGoal, Clause, WhereClauseAtom};
 use syntax::ast;
 use rustc_data_structures::sync::Lrc;
@@ -104,29 +105,69 @@ crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
     let node_id = tcx.hir.as_local_node_id(def_id).unwrap();
     let item = tcx.hir.expect_item(node_id);
     match item.node {
+        hir::ItemTrait(..) => program_clauses_for_trait(tcx, def_id),
         hir::ItemImpl(..) => program_clauses_for_impl(tcx, def_id),
 
         // FIXME: other constructions e.g. traits, associated types...
         _ => Lrc::new(vec![]),
     }
 }
 
+fn program_clauses_for_trait<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
+    -> Lrc<Vec<Clause<'tcx>>>
+{
+    // Rule Implemented-From-Env (see rustc guide)
+    //
+    // `trait Trait<P1..Pn> where WC { .. } // P0 == Self`
+    //
+    // ```
+    // forall<Self, P1..Pn> {
+    //   Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
+    // }
+    // ```
+
+    // `Self: Trait<P1..Pn>`
+    let trait_pred = ty::TraitPredicate {
+        trait_ref: ty::TraitRef {
+            def_id,
+            substs: Substs::identity_for_item(tcx, def_id)
+        }
+    };
+    // `FromEnv(Self: Trait<P1..Pn>)`
+    let from_env = Goal::DomainGoal(DomainGoal::FromEnv(trait_pred.lower()));
+    // `Implemented(Self: Trait<P1..Pn>)`
+    let impl_trait = DomainGoal::Holds(WhereClauseAtom::Implemented(trait_pred));
+
+    // `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
+    let clause = Clause::Implies(vec![from_env], impl_trait);
+    Lrc::new(vec![clause])
+}
+
 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
+    // Rule Implemented-From-Impl (see rustc guide)
+    //
+    // `impl<P0..Pn> Trait<A1..An> for A0 where WC { .. }`
     //
-    // (see rustc guide)
+    // ```
+    // forall<P0..Pn> {
+    //   Implemented(A0: Trait<A1..An>) :- WC
+    // }
+    // ```
 
     let trait_ref = tcx.impl_trait_ref(def_id).unwrap();
-    let trait_ref = ty::TraitPredicate { trait_ref }.lower();
+    // `Implemented(A0: Trait<A1..An>)`
+    let trait_pred = ty::TraitPredicate { trait_ref }.lower();
+     // `WC`
     let where_clauses = tcx.predicates_of(def_id).predicates.lower();
 
-    let clause = Clause::Implies(where_clauses, trait_ref);
+     // `Implemented(A0: Trait<A1..An>) :- WC`
+    let clause = Clause::Implies(where_clauses, trait_pred);
     Lrc::new(vec![clause])
 }
 

src/test/ui/chalkify/lower_trait.rs

@@ -0,0 +1,22 @@
+// 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)]
+
+#[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<S, T, U>) :-
+trait Foo<S, T, U> {
+    fn s(S) -> S;
+    fn t(T) -> T;
+    fn u(U) -> U;
+}
+
+fn main() {
+    println!("hello");
+}

src/test/ui/chalkify/lower_trait.stderr

@@ -0,0 +1,8 @@
+error: Implemented(Self: Foo<S, T, U>) :- FromEnv(Self: Foo<S, T, U>).
+  --> $DIR/lower_trait.rs:13:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<S, T, U>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to previous error
+