traits: Implement interning for Goal and Clause

This commit is contained in:
Tatsuyuki Ishi 2018-04-09 16:38:00 +09:00
parent d26f9e42df
commit b15df80345
5 changed files with 154 additions and 62 deletions

View File

@ -23,13 +23,12 @@ use infer::outlives::env::OutlivesEnvironment;
use middle::region;
use middle::const_val::ConstEvalErr;
use ty::subst::Substs;
use ty::{self, AdtKind, Ty, TyCtxt, TypeFoldable, ToPredicate};
use ty::{self, AdtKind, Slice, Ty, TyCtxt, TypeFoldable, ToPredicate};
use ty::error::{ExpectedFound, TypeError};
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};
@ -280,14 +279,28 @@ pub enum QuantifierKind {
Existential,
}
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
#[derive(Copy, 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>>),
Implies(&'tcx Slice<Clause<'tcx>>, &'tcx Goal<'tcx>),
And(&'tcx Goal<'tcx>, &'tcx Goal<'tcx>),
Not(&'tcx Goal<'tcx>),
DomainGoal(DomainGoal<'tcx>),
Quantified(QuantifierKind, Box<ty::Binder<Goal<'tcx>>>)
Quantified(QuantifierKind, ty::Binder<&'tcx Goal<'tcx>>)
}
impl<'tcx> Goal<'tcx> {
pub fn from_poly_domain_goal<'a>(
domain_goal: PolyDomainGoal<'tcx>,
tcx: TyCtxt<'a, 'tcx, 'tcx>,
) -> Goal<'tcx> {
match domain_goal.no_late_bound_regions() {
Some(p) => p.into(),
None => Goal::Quantified(
QuantifierKind::Universal,
domain_goal.map_bound(|p| tcx.mk_goal(Goal::from(p)))
),
}
}
}
impl<'tcx> From<DomainGoal<'tcx>> for Goal<'tcx> {
@ -296,21 +309,9 @@ impl<'tcx> From<DomainGoal<'tcx>> for Goal<'tcx> {
}
}
impl<'tcx> From<PolyDomainGoal<'tcx>> for Goal<'tcx> {
fn from(domain_goal: PolyDomainGoal<'tcx>) -> Self {
match domain_goal.no_late_bound_regions() {
Some(p) => p.into(),
None => Goal::Quantified(
QuantifierKind::Universal,
Box::new(domain_goal.map_bound(|p| p.into()))
),
}
}
}
/// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
/// Harrop Formulas".
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub enum Clause<'tcx> {
Implies(ProgramClause<'tcx>),
ForAll(ty::Binder<ProgramClause<'tcx>>),
@ -322,13 +323,13 @@ pub enum Clause<'tcx> {
/// it with the reverse implication operator `:-` to emphasize the way
/// that programs are actually solved (via backchaining, which starts
/// with the goal to solve and proceeds from there).
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub struct ProgramClause<'tcx> {
/// This goal will be considered true...
pub goal: DomainGoal<'tcx>,
/// ...if we can prove these hypotheses (there may be no hypotheses at all):
pub hypotheses: Vec<Goal<'tcx>>,
pub hypotheses: &'tcx Slice<Goal<'tcx>>,
}
pub type Selection<'tcx> = Vtable<'tcx, PredicateObligation<'tcx>>;

View File

@ -8,6 +8,7 @@
// option. This file may not be copied, modified, or distributed
// except according to those terms.
use rustc_data_structures::accumulate_vec::AccumulateVec;
use traits;
use traits::project::Normalized;
use ty::{self, Lift, TyCtxt};
@ -557,6 +558,28 @@ EnumTypeFoldableImpl! {
}
}
impl<'tcx> TypeFoldable<'tcx> for &'tcx ty::Slice<traits::Goal<'tcx>> {
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
let v = self.iter().map(|t| t.fold_with(folder)).collect::<AccumulateVec<[_; 8]>>();
folder.tcx().intern_goals(&v)
}
fn super_visit_with<V: TypeVisitor<'tcx>>(&self, visitor: &mut V) -> bool {
self.iter().any(|t| t.visit_with(visitor))
}
}
impl<'tcx> TypeFoldable<'tcx> for &'tcx traits::Goal<'tcx> {
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
let v = (**self).fold_with(folder);
folder.tcx().mk_goal(v)
}
fn super_visit_with<V: TypeVisitor<'tcx>>(&self, visitor: &mut V) -> bool {
(**self).visit_with(visitor)
}
}
BraceStructTypeFoldableImpl! {
impl<'tcx> TypeFoldable<'tcx> for traits::ProgramClause<'tcx> {
goal,
@ -570,3 +593,14 @@ EnumTypeFoldableImpl! {
(traits::Clause::ForAll)(clause),
}
}
impl<'tcx> TypeFoldable<'tcx> for &'tcx ty::Slice<traits::Clause<'tcx>> {
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
let v = self.iter().map(|t| t.fold_with(folder)).collect::<AccumulateVec<[_; 8]>>();
folder.tcx().intern_clauses(&v)
}
fn super_visit_with<V: TypeVisitor<'tcx>>(&self, visitor: &mut V) -> bool {
self.iter().any(|t| t.visit_with(visitor))
}
}

View File

@ -38,6 +38,7 @@ use ty::subst::{Kind, Substs};
use ty::ReprOptions;
use ty::Instance;
use traits;
use traits::{Clause, Goal};
use ty::{self, Ty, TypeAndMut};
use ty::{TyS, TypeVariants, Slice};
use ty::{AdtKind, AdtDef, ClosureSubsts, GeneratorInterior, Region, Const};
@ -125,34 +126,40 @@ impl<'tcx> GlobalArenas<'tcx> {
}
}
type InternedSet<'tcx, T> = Lock<FxHashSet<Interned<'tcx, T>>>;
pub struct CtxtInterners<'tcx> {
/// The arena that types, regions, etc are allocated from
arena: &'tcx DroplessArena,
/// Specifically use a speedy hash algorithm for these hash sets,
/// they're accessed quite often.
type_: Lock<FxHashSet<Interned<'tcx, TyS<'tcx>>>>,
type_list: Lock<FxHashSet<Interned<'tcx, Slice<Ty<'tcx>>>>>,
substs: Lock<FxHashSet<Interned<'tcx, Substs<'tcx>>>>,
canonical_var_infos: Lock<FxHashSet<Interned<'tcx, Slice<CanonicalVarInfo>>>>,
region: Lock<FxHashSet<Interned<'tcx, RegionKind>>>,
existential_predicates: Lock<FxHashSet<Interned<'tcx, Slice<ExistentialPredicate<'tcx>>>>>,
predicates: Lock<FxHashSet<Interned<'tcx, Slice<Predicate<'tcx>>>>>,
const_: Lock<FxHashSet<Interned<'tcx, Const<'tcx>>>>,
type_: InternedSet<'tcx, TyS<'tcx>>,
type_list: InternedSet<'tcx, Slice<Ty<'tcx>>>,
substs: InternedSet<'tcx, Substs<'tcx>>,
canonical_var_infos: InternedSet<'tcx, Slice<CanonicalVarInfo>>,
region: InternedSet<'tcx, RegionKind>,
existential_predicates: InternedSet<'tcx, Slice<ExistentialPredicate<'tcx>>>,
predicates: InternedSet<'tcx, Slice<Predicate<'tcx>>>,
const_: InternedSet<'tcx, Const<'tcx>>,
clauses: InternedSet<'tcx, Slice<Clause<'tcx>>>,
goals: InternedSet<'tcx, Slice<Goal<'tcx>>>,
}
impl<'gcx: 'tcx, 'tcx> CtxtInterners<'tcx> {
fn new(arena: &'tcx DroplessArena) -> CtxtInterners<'tcx> {
CtxtInterners {
arena: arena,
type_: Lock::new(FxHashSet()),
type_list: Lock::new(FxHashSet()),
substs: Lock::new(FxHashSet()),
canonical_var_infos: Lock::new(FxHashSet()),
region: Lock::new(FxHashSet()),
existential_predicates: Lock::new(FxHashSet()),
predicates: Lock::new(FxHashSet()),
const_: Lock::new(FxHashSet()),
arena,
type_: Default::default(),
type_list: Default::default(),
substs: Default::default(),
region: Default::default(),
existential_predicates: Default::default(),
canonical_var_infos: Default::default(),
predicates: Default::default(),
const_: Default::default(),
clauses: Default::default(),
goals: Default::default(),
}
}
@ -2088,6 +2095,20 @@ impl<'tcx: 'lcx, 'lcx> Borrow<Const<'lcx>> for Interned<'tcx, Const<'tcx>> {
}
}
impl<'tcx: 'lcx, 'lcx> Borrow<[Clause<'lcx>]>
for Interned<'tcx, Slice<Clause<'tcx>>> {
fn borrow<'a>(&'a self) -> &'a [Clause<'lcx>] {
&self.0[..]
}
}
impl<'tcx: 'lcx, 'lcx> Borrow<[Goal<'lcx>]>
for Interned<'tcx, Slice<Goal<'tcx>>> {
fn borrow<'a>(&'a self) -> &'a [Goal<'lcx>] {
&self.0[..]
}
}
macro_rules! intern_method {
($lt_tcx:tt, $name:ident: $method:ident($alloc:ty,
$alloc_method:ident,
@ -2185,7 +2206,9 @@ slice_interners!(
existential_predicates: _intern_existential_predicates(ExistentialPredicate),
predicates: _intern_predicates(Predicate),
type_list: _intern_type_list(Ty),
substs: _intern_substs(Kind)
substs: _intern_substs(Kind),
clauses: _intern_clauses(Clause),
goals: _intern_goals(Goal)
);
// This isn't a perfect fit: CanonicalVarInfo slices are always
@ -2490,6 +2513,22 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
}
}
pub fn intern_clauses(self, ts: &[Clause<'tcx>]) -> &'tcx Slice<Clause<'tcx>> {
if ts.len() == 0 {
Slice::empty()
} else {
self._intern_clauses(ts)
}
}
pub fn intern_goals(self, ts: &[Goal<'tcx>]) -> &'tcx Slice<Goal<'tcx>> {
if ts.len() == 0 {
Slice::empty()
} else {
self._intern_goals(ts)
}
}
pub fn mk_fn_sig<I>(self,
inputs: I,
output: I::Item,
@ -2536,6 +2575,20 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
self.mk_substs(iter::once(s).chain(t.into_iter().cloned()).map(Kind::from))
}
pub fn mk_clauses<I: InternAs<[Clause<'tcx>],
&'tcx Slice<Clause<'tcx>>>>(self, iter: I) -> I::Output {
iter.intern_with(|xs| self.intern_clauses(xs))
}
pub fn mk_goals<I: InternAs<[Goal<'tcx>],
&'tcx Slice<Goal<'tcx>>>>(self, iter: I) -> I::Output {
iter.intern_with(|xs| self.intern_goals(xs))
}
pub fn mk_goal(self, goal: Goal<'tcx>) -> &'tcx Goal {
&self.mk_goals(iter::once(goal))[0]
}
pub fn lint_node<S: Into<MultiSpan>>(self,
lint: &'static Lint,
id: NodeId,

View File

@ -39,7 +39,7 @@ 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::{self, CrateInherentImpls, ParamEnvAnd, Slice, Ty, TyCtxt};
use ty::steal::Steal;
use ty::subst::Substs;
use util::nodemap::{DefIdSet, DefIdMap, ItemLocalSet};
@ -435,7 +435,7 @@ define_maps! { <'tcx>
[] fn features_query: features_node(CrateNum) -> Lrc<feature_gate::Features>,
[] fn program_clauses_for: ProgramClausesFor(DefId) -> Lrc<Vec<Clause<'tcx>>>,
[] fn program_clauses_for: ProgramClausesFor(DefId) -> Lrc<&'tcx Slice<Clause<'tcx>>>,
[] fn wasm_custom_sections: WasmCustomSections(CrateNum) -> Lrc<Vec<DefId>>,
[] fn wasm_import_module_map: WasmImportModuleMap(CrateNum)

View File

@ -11,12 +11,14 @@
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::{self, Slice, TyCtxt};
use rustc::ty::subst::Substs;
use rustc::traits::{WhereClauseAtom, PolyDomainGoal, DomainGoal, ProgramClause, Clause};
use rustc::traits::{WhereClauseAtom, PolyDomainGoal, DomainGoal, ProgramClause, Clause, Goal};
use syntax::ast;
use rustc_data_structures::sync::Lrc;
use std::iter;
trait Lower<T> {
/// Lower a rustc construction (e.g. `ty::TraitPredicate`) to a chalk-like type.
fn lower(&self) -> T;
@ -113,7 +115,7 @@ impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
}
crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
-> Lrc<Vec<Clause<'tcx>>>
-> Lrc<&'tcx Slice<Clause<'tcx>>>
{
let node_id = tcx.hir.as_local_node_id(def_id).unwrap();
let item = tcx.hir.expect_item(node_id);
@ -122,12 +124,12 @@ crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
hir::ItemImpl(..) => program_clauses_for_impl(tcx, def_id),
// FIXME: other constructions e.g. traits, associated types...
_ => Lrc::new(vec![]),
_ => Lrc::new(tcx.mk_clauses(iter::empty::<Clause>())),
}
}
fn program_clauses_for_trait<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
-> Lrc<Vec<Clause<'tcx>>>
-> Lrc<&'tcx Slice<Clause<'tcx>>>
{
// `trait Trait<P1..Pn> where WC { .. } // P0 == Self`
@ -147,18 +149,18 @@ fn program_clauses_for_trait<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
}
};
// `FromEnv(Self: Trait<P1..Pn>)`
let from_env = DomainGoal::FromEnv(trait_pred.lower()).into();
let from_env = Goal::from(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 implemented_from_env = ProgramClause {
goal: impl_trait,
hypotheses: vec![from_env],
hypotheses: tcx.mk_goals(iter::once(from_env)),
};
let mut clauses = vec![
let clauses = iter::once(
Clause::ForAll(ty::Binder::dummy(implemented_from_env))
];
);
// Rule Implied-Bound-From-Trait
//
@ -175,14 +177,14 @@ fn program_clauses_for_trait<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
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);
.map(|wc| implied_bound_from_trait(tcx, trait_pred, wc));
Lrc::new(clauses)
Lrc::new(tcx.mk_clauses(clauses.chain(implied_bound_clauses)))
}
/// For a given `where_clause`, returns a clause `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`.
fn implied_bound_from_trait<'tcx>(
fn implied_bound_from_trait<'a, 'tcx>(
tcx: TyCtxt<'a, 'tcx, 'tcx>,
trait_pred: ty::TraitPredicate<'tcx>,
where_clause: &ty::Predicate<'tcx>,
) -> Clause<'tcx> {
@ -193,16 +195,16 @@ fn implied_bound_from_trait<'tcx>(
Clause::ForAll(
where_clause.lower().map_bound(|goal| ProgramClause {
goal: goal.into_from_env_goal(),
hypotheses: vec![impl_trait.into()],
hypotheses: tcx.mk_goals(iter::once(Goal::from(impl_trait))),
})
)
}
fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
-> Lrc<Vec<Clause<'tcx>>>
-> Lrc<&'tcx Slice<Clause<'tcx>>>
{
if let ImplPolarity::Negative = tcx.impl_polarity(def_id) {
return Lrc::new(vec![]);
return Lrc::new(tcx.mk_clauses(iter::empty::<Clause>()));
}
// Rule Implemented-From-Impl (see rustc guide)
@ -224,9 +226,11 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
// `Implemented(A0: Trait<A1..An>) :- WC`
let clause = ProgramClause {
goal: trait_pred,
hypotheses: where_clauses.into_iter().map(|wc| wc.into()).collect()
hypotheses: tcx.mk_goals(
where_clauses.into_iter().map(|wc| Goal::from_poly_domain_goal(wc, tcx))
)
};
Lrc::new(vec![Clause::ForAll(ty::Binder::dummy(clause))])
Lrc::new(tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause)))))
}
pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
@ -248,7 +252,7 @@ impl<'a, 'tcx> ClauseDumper<'a, 'tcx > {
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 {
for clause in *clauses {
// Skip the top-level binder for a less verbose output
let program_clause = match clause {
Clause::Implies(program_clause) => program_clause,