Skip to content

Commit

Permalink
traits: Implement interning for Goal and Clause
Browse files Browse the repository at this point in the history
  • Loading branch information
ishitatsuyuki committed Apr 12, 2018
1 parent d26f9e4 commit b15df80
Show file tree
Hide file tree
Showing 5 changed files with 151 additions and 59 deletions.
41 changes: 21 additions & 20 deletions src/librustc/traits/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};

Expand Down Expand Up @@ -280,37 +279,39 @@ 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>>>)
}

impl<'tcx> From<DomainGoal<'tcx>> for Goal<'tcx> {
fn from(domain_goal: DomainGoal<'tcx>) -> Self {
Goal::DomainGoal(domain_goal)
}
Quantified(QuantifierKind, ty::Binder<&'tcx Goal<'tcx>>)
}

impl<'tcx> From<PolyDomainGoal<'tcx>> for Goal<'tcx> {
fn from(domain_goal: PolyDomainGoal<'tcx>) -> Self {
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,
Box::new(domain_goal.map_bound(|p| p.into()))
domain_goal.map_bound(|p| tcx.mk_goal(Goal::from(p)))
),
}
}
}

impl<'tcx> From<DomainGoal<'tcx>> for Goal<'tcx> {
fn from(domain_goal: DomainGoal<'tcx>) -> Self {
Goal::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)]
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub enum Clause<'tcx> {
Implies(ProgramClause<'tcx>),
ForAll(ty::Binder<ProgramClause<'tcx>>),
Expand All @@ -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>>;
Expand Down
34 changes: 34 additions & 0 deletions src/librustc/traits/structural_impls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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,
Expand All @@ -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))
}
}
89 changes: 71 additions & 18 deletions src/librustc/ty/context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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(),
}
}

Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down
4 changes: 2 additions & 2 deletions src/librustc/ty/maps/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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)
Expand Down
Loading

0 comments on commit b15df80

Please sign in to comment.