Skip to content

Commit

Permalink
Implement Rule Implemented-From-Env
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
varkor committed Mar 20, 2018
1 parent de9e665 commit b8c75d9
Showing 1 changed file with 32 additions and 0 deletions.
32 changes: 32 additions & 0 deletions src/librustc_traits/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -104,13 +105,44 @@ 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>>>
{
Expand Down

0 comments on commit b8c75d9

Please sign in to comment.