chalkify: Implement Rule Implied-Bound-From-Trait

tmandry · tmandry · commit 7ac35eaa12c4 · 2018-04-06T13:05:45.000-05:00
diff --git a/src/librustc_traits/lowering.rs b/src/librustc_traits/lowering.rs
@@ -90,6 +90,28 @@ impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
     }
 }
 
+/// Transforms an existing goal into a FromEnv goal.
+///
+/// Used for lowered where clauses (see rustc guide).
+trait IntoFromEnvGoal {
+    fn into_from_env_goal(self) -> Self;
+}
+
+impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
+    fn into_from_env_goal(self) -> DomainGoal<'tcx> {
+        use self::DomainGoal::*;
+        match self {
+            Holds(wc_atom) => FromEnv(wc_atom),
+            WellFormed(..) |
+            FromEnv(..) |
+            WellFormedTy(..) |
+            FromEnvTy(..) |
+            RegionOutlives(..) |
+            TypeOutlives(..) => self,
+        }
+    }
+}
+
 crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
     -> Lrc<Vec<Clause<'tcx>>>
 {
@@ -107,9 +129,9 @@ crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
 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`
+
+    // Rule Implemented-From-Env (see rustc guide)
     //
     // ```
     // forall<Self, P1..Pn> {
@@ -130,11 +152,50 @@ fn program_clauses_for_trait<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
     let impl_trait = DomainGoal::Holds(WhereClauseAtom::Implemented(trait_pred));
 
     // `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
-    let clause = ProgramClause {
+    let implemented_from_env = ProgramClause {
         goal: impl_trait,
         hypotheses: vec![from_env],
     };
-    Lrc::new(vec![Clause::ForAll(ty::Binder::dummy(clause))])
+    let mut clauses = vec![
+        Clause::ForAll(ty::Binder::dummy(implemented_from_env))
+    ];
+
+    // 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
+    // FIXME: Remove the [1..] slice; this is a hack because the query
+    // predicates_of currently includes the trait itself (`Self: Trait<P1..Pn>`).
+    let where_clauses = &tcx.predicates_of(def_id).predicates;
+    let implied_bound_clauses =
+        where_clauses[1..].into_iter()
+        .map(|wc| implied_bound_from_trait(trait_pred, wc));
+    clauses.extend(implied_bound_clauses);
+
+    Lrc::new(clauses)
+}
+
+/// For a given `where_clause`, returns a clause `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`.
+fn implied_bound_from_trait<'tcx>(
+    trait_pred: ty::TraitPredicate<'tcx>,
+    where_clause: &ty::Predicate<'tcx>,
+) -> Clause<'tcx> {
+    // `FromEnv(Self: Trait<P1..Pn>)`
+    let impl_trait = DomainGoal::FromEnv(WhereClauseAtom::Implemented(trait_pred));
+
+    // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
+    Clause::ForAll(
+        where_clause.lower().map_bound(|goal| ProgramClause {
+            goal: goal.into_from_env_goal(),
+            hypotheses: vec![impl_trait.into()],
+        })
+    )
 }
 
 fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
diff --git a/src/test/ui/chalkify/lower_trait.rs b/src/test/ui/chalkify/lower_trait.rs
@@ -11,6 +11,9 @@
 #![feature(rustc_attrs)]
 
 #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<S, T, U>) :-
+                              //~| ERROR FromEnv
+                              //~| ERROR FromEnv
+                              //~| ERROR FromEnv
 trait Foo<S, T, U> {
     fn s(S) -> S;
     fn t(T) -> T;
diff --git a/src/test/ui/chalkify/lower_trait.stderr b/src/test/ui/chalkify/lower_trait.stderr
@@ -4,5 +4,23 @@ error: Implemented(Self: Foo<S, T, U>) :- FromEnv(Self: Foo<S, T, U>).
 LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<S, T, U>) :-
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-error: aborting due to previous error
+error: FromEnv(S: std::marker::Sized) :- 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: FromEnv(T: std::marker::Sized) :- 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: FromEnv(U: std::marker::Sized) :- 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 4 previous errors
 
diff --git a/src/test/ui/chalkify/lower_trait_higher_rank.rs b/src/test/ui/chalkify/lower_trait_higher_rank.rs
@@ -0,0 +1,24 @@
+// 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<F>) :-
+                              //~| ERROR FromEnv
+                              //~| ERROR FromEnv
+                              //~| ERROR FromEnv
+trait Foo<F> where for<'a> F: Fn(&'a (u8, u16)) -> &'a u8
+{
+    fn s(F) -> F;
+}
+
+fn main() {
+    println!("hello");
+}
diff --git a/src/test/ui/chalkify/lower_trait_higher_rank.stderr b/src/test/ui/chalkify/lower_trait_higher_rank.stderr
@@ -0,0 +1,26 @@
+error: Implemented(Self: Foo<F>) :- FromEnv(Self: Foo<F>).
+  --> $DIR/lower_trait_higher_rank.rs:13:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<F>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: FromEnv(F: std::marker::Sized) :- FromEnv(Self: Foo<F>).
+  --> $DIR/lower_trait_higher_rank.rs:13:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<F>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: FromEnv(F: std::ops::Fn<(&'a (u8, u16),)>) :- FromEnv(Self: Foo<F>).
+  --> $DIR/lower_trait_higher_rank.rs:13:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<F>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: FromEnv(<F as std::ops::FnOnce<(&'a (u8, u16),)>>::Output == &'a u8) :- FromEnv(Self: Foo<F>).
+  --> $DIR/lower_trait_higher_rank.rs:13:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<F>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to 4 previous errors
+
diff --git a/src/test/ui/chalkify/lower_trait_where_clause.rs b/src/test/ui/chalkify/lower_trait_where_clause.rs
@@ -0,0 +1,31 @@
+// 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)]
+
+use std::fmt::{Debug, Display};
+use std::borrow::Borrow;
+
+#[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<'a, 'b, S, T, U>) :-
+                              //~| ERROR FromEnv
+                              //~| ERROR FromEnv
+                              //~| ERROR FromEnv
+                              //~| ERROR FromEnv
+                              //~| ERROR RegionOutlives
+                              //~| ERROR TypeOutlives
+trait Foo<'a, 'b, S, T, U> where S: Debug, T: Borrow<U>, U: ?Sized, 'a: 'b, U: 'b {
+    fn s(S) -> S;
+    fn t(T) -> T;
+    fn u(U) -> U;
+}
+
+fn main() {
+    println!("hello");
+}
diff --git a/src/test/ui/chalkify/lower_trait_where_clause.stderr b/src/test/ui/chalkify/lower_trait_where_clause.stderr
@@ -0,0 +1,44 @@
+error: Implemented(Self: Foo<'a, 'b, S, T, U>) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
+  --> $DIR/lower_trait_where_clause.rs:16:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<'a, 'b, S, T, U>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: FromEnv(S: std::marker::Sized) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
+  --> $DIR/lower_trait_where_clause.rs:16:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<'a, 'b, S, T, U>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: FromEnv(T: std::marker::Sized) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
+  --> $DIR/lower_trait_where_clause.rs:16:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<'a, 'b, S, T, U>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: FromEnv(S: std::fmt::Debug) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
+  --> $DIR/lower_trait_where_clause.rs:16:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<'a, 'b, S, T, U>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: FromEnv(T: std::borrow::Borrow<U>) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
+  --> $DIR/lower_trait_where_clause.rs:16:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<'a, 'b, S, T, U>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: RegionOutlives('a : 'b) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
+  --> $DIR/lower_trait_where_clause.rs:16:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<'a, 'b, S, T, U>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: TypeOutlives(U : 'b) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
+  --> $DIR/lower_trait_where_clause.rs:16:1
+   |
+LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(Self: Foo<'a, 'b, S, T, U>) :-
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to 7 previous errors
+
