-
Notifications
You must be signed in to change notification settings - Fork 13.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
traits: Implement interning for Goal and Clause #49800
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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,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>>), | ||
|
@@ -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>>, | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Maybe worth a type alias? |
||
} | ||
|
||
pub type Selection<'tcx> = Vtable<'tcx, PredicateObligation<'tcx>>; | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. At some point we should think about making a macro for these "intern-wrapping impls"... but not, I suppose, in this PR. |
||
} | ||
|
||
fn super_visit_with<V: TypeVisitor<'tcx>>(&self, visitor: &mut V) -> bool { | ||
self.iter().any(|t| t.visit_with(visitor)) | ||
} | ||
} | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Do we want an impl for |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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] | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this is clever... |
||
} | ||
|
||
pub fn lint_node<S: Into<MultiSpan>>(self, | ||
lint: &'static Lint, | ||
id: NodeId, | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Woohoo, copy types FTW 🐻