Skip to content

Commit

Permalink
Auto merge of #49837 - nikomatsakis:chalkify-engine, r=scalexm
Browse files Browse the repository at this point in the history
work towards chalkify-ing the engine

This work towards creating a "all program clauses needed for this goal" query

r? @scalexm
  • Loading branch information
bors committed Apr 24, 2018
2 parents 52ed3d8 + 2c5fbe2 commit 898c9f7
Show file tree
Hide file tree
Showing 30 changed files with 380 additions and 269 deletions.
1 change: 1 addition & 0 deletions src/librustc/dep_graph/dep_node.rs
Original file line number Diff line number Diff line change
Expand Up @@ -655,6 +655,7 @@ define_dep_nodes!( <'tcx>
[input] Features,

[] ProgramClausesFor(DefId),
[] ProgramClausesForEnv(ParamEnv<'tcx>),
[] WasmImportModuleMap(CrateNum),
[] ForeignModules(CrateNum),

Expand Down
7 changes: 4 additions & 3 deletions src/librustc/hir/map/def_collector.rs
Original file line number Diff line number Diff line change
Expand Up @@ -107,8 +107,9 @@ impl<'a> visit::Visitor<'a> for DefCollector<'a> {
// information we encapsulate into
let def_data = match i.node {
ItemKind::Impl(..) => DefPathData::Impl,
ItemKind::Trait(..) => DefPathData::Trait(i.ident.name.as_str()),
ItemKind::Enum(..) | ItemKind::Struct(..) | ItemKind::Union(..) |
ItemKind::Trait(..) | ItemKind::TraitAlias(..) |
ItemKind::TraitAlias(..) |
ItemKind::ExternCrate(..) | ItemKind::ForeignMod(..) | ItemKind::Ty(..) =>
DefPathData::TypeNs(i.ident.name.as_str()),
ItemKind::Mod(..) if i.ident == keywords::Invalid.ident() => {
Expand Down Expand Up @@ -222,7 +223,7 @@ impl<'a> visit::Visitor<'a> for DefCollector<'a> {
let def_data = match ti.node {
TraitItemKind::Method(..) | TraitItemKind::Const(..) =>
DefPathData::ValueNs(ti.ident.name.as_str()),
TraitItemKind::Type(..) => DefPathData::TypeNs(ti.ident.name.as_str()),
TraitItemKind::Type(..) => DefPathData::AssocTypeInTrait(ti.ident.name.as_str()),
TraitItemKind::Macro(..) => return self.visit_macro_invoc(ti.id, false),
};

Expand All @@ -240,7 +241,7 @@ impl<'a> visit::Visitor<'a> for DefCollector<'a> {
let def_data = match ii.node {
ImplItemKind::Method(..) | ImplItemKind::Const(..) =>
DefPathData::ValueNs(ii.ident.name.as_str()),
ImplItemKind::Type(..) => DefPathData::TypeNs(ii.ident.name.as_str()),
ImplItemKind::Type(..) => DefPathData::AssocTypeInImpl(ii.ident.name.as_str()),
ImplItemKind::Macro(..) => return self.visit_macro_invoc(ii.id, false),
};

Expand Down
15 changes: 15 additions & 0 deletions src/librustc/hir/map/definitions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -212,6 +212,9 @@ impl DefKey {
::std::mem::discriminant(data).hash(&mut hasher);
match *data {
DefPathData::TypeNs(name) |
DefPathData::Trait(name) |
DefPathData::AssocTypeInTrait(name) |
DefPathData::AssocTypeInImpl(name) |
DefPathData::ValueNs(name) |
DefPathData::Module(name) |
DefPathData::MacroDef(name) |
Expand Down Expand Up @@ -358,6 +361,12 @@ pub enum DefPathData {
// Different kinds of items and item-like things:
/// An impl
Impl,
/// A trait
Trait(InternedString),
/// An associated type **declaration** (i.e., in a trait)
AssocTypeInTrait(InternedString),
/// An associated type **value** (i.e., in an impl)
AssocTypeInImpl(InternedString),
/// Something in the type NS
TypeNs(InternedString),
/// Something in the value NS
Expand Down Expand Up @@ -639,6 +648,9 @@ impl DefPathData {
use self::DefPathData::*;
match *self {
TypeNs(name) |
Trait(name) |
AssocTypeInTrait(name) |
AssocTypeInImpl(name) |
ValueNs(name) |
Module(name) |
MacroDef(name) |
Expand All @@ -663,6 +675,9 @@ impl DefPathData {
use self::DefPathData::*;
let s = match *self {
TypeNs(name) |
Trait(name) |
AssocTypeInTrait(name) |
AssocTypeInImpl(name) |
ValueNs(name) |
Module(name) |
MacroDef(name) |
Expand Down
5 changes: 1 addition & 4 deletions src/librustc/ich/impls_ty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1352,10 +1352,6 @@ impl_stable_hash_for!(
}
);

impl_stable_hash_for!(struct infer::canonical::QueryRegionConstraints<'tcx> {
region_outlives, ty_outlives
});

impl_stable_hash_for!(enum infer::canonical::Certainty {
Proven, Ambiguous
});
Expand Down Expand Up @@ -1417,6 +1413,7 @@ impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Goal<'tcx> {
quantifier.hash_stable(hcx, hasher);
goal.hash_stable(hcx, hasher);
},
CannotProve => { },
}
}
}
Expand Down
71 changes: 23 additions & 48 deletions src/librustc/infer/canonical.rs
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@ use traits::{Obligation, ObligationCause, PredicateObligation};
use ty::{self, CanonicalVar, Lift, Region, Slice, Ty, TyCtxt, TypeFlags};
use ty::subst::{Kind, UnpackedKind};
use ty::fold::{TypeFoldable, TypeFolder};
use util::captures::Captures;

use rustc_data_structures::indexed_vec::IndexVec;
use rustc_data_structures::fx::FxHashMap;
Expand Down Expand Up @@ -121,7 +120,7 @@ pub enum CanonicalTyVarKind {
#[derive(Clone, Debug)]
pub struct QueryResult<'tcx, R> {
pub var_values: CanonicalVarValues<'tcx>,
pub region_constraints: QueryRegionConstraints<'tcx>,
pub region_constraints: Vec<QueryRegionConstraint<'tcx>>,
pub certainty: Certainty,
pub value: R,
}
Expand Down Expand Up @@ -181,12 +180,7 @@ impl<'tcx, R> Canonical<'tcx, QueryResult<'tcx, R>> {
}
}

/// Subset of `RegionConstraintData` produced by trait query.
#[derive(Clone, Debug, Default)]
pub struct QueryRegionConstraints<'tcx> {
pub region_outlives: Vec<(Region<'tcx>, Region<'tcx>)>,
pub ty_outlives: Vec<(Ty<'tcx>, Region<'tcx>)>,
}
pub type QueryRegionConstraint<'tcx> = ty::Binder<ty::OutlivesPredicate<Kind<'tcx>, Region<'tcx>>>;

/// Trait implemented by values that can be canonicalized. It mainly
/// serves to identify the interning table we will use.
Expand Down Expand Up @@ -382,35 +376,29 @@ impl<'cx, 'gcx, 'tcx> InferCtxt<'cx, 'gcx, 'tcx> {
&'a self,
cause: &'a ObligationCause<'tcx>,
param_env: ty::ParamEnv<'tcx>,
unsubstituted_region_constraints: &'a QueryRegionConstraints<'tcx>,
unsubstituted_region_constraints: &'a [QueryRegionConstraint<'tcx>],
result_subst: &'a CanonicalVarValues<'tcx>,
) -> impl Iterator<Item = PredicateObligation<'tcx>> + Captures<'gcx> + 'a {
let QueryRegionConstraints {
region_outlives,
ty_outlives,
} = unsubstituted_region_constraints;

let region_obligations = region_outlives.iter().map(move |(r1, r2)| {
let r1 = substitute_value(self.tcx, result_subst, r1);
let r2 = substitute_value(self.tcx, result_subst, r2);
Obligation::new(
cause.clone(),
param_env,
ty::Predicate::RegionOutlives(ty::Binder(ty::OutlivesPredicate(r1, r2))),
)
});

let ty_obligations = ty_outlives.iter().map(move |(t1, r2)| {
let t1 = substitute_value(self.tcx, result_subst, t1);
) -> impl Iterator<Item = PredicateObligation<'tcx>> + 'a {
Box::new(unsubstituted_region_constraints.iter().map(move |constraint| {
let ty::OutlivesPredicate(k1, r2) = constraint.skip_binder(); // restored below
let k1 = substitute_value(self.tcx, result_subst, k1);
let r2 = substitute_value(self.tcx, result_subst, r2);
Obligation::new(
cause.clone(),
param_env,
ty::Predicate::TypeOutlives(ty::Binder(ty::OutlivesPredicate(t1, r2))),
)
});

region_obligations.chain(ty_obligations)
match k1.unpack() {
UnpackedKind::Lifetime(r1) =>
Obligation::new(
cause.clone(),
param_env,
ty::Predicate::RegionOutlives(ty::Binder(ty::OutlivesPredicate(r1, r2))),
),

UnpackedKind::Type(t1) =>
Obligation::new(
cause.clone(),
param_env,
ty::Predicate::TypeOutlives(ty::Binder(ty::OutlivesPredicate(t1, r2))),
),
}
})) as Box<dyn Iterator<Item = _>>
}

/// Given two sets of values for the same set of canonical variables, unify them.
Expand Down Expand Up @@ -913,19 +901,6 @@ BraceStructTypeFoldableImpl! {
}
}

BraceStructTypeFoldableImpl! {
impl<'tcx> TypeFoldable<'tcx> for QueryRegionConstraints<'tcx> {
region_outlives, ty_outlives
}
}

BraceStructLiftImpl! {
impl<'a, 'tcx> Lift<'tcx> for QueryRegionConstraints<'a> {
type Lifted = QueryRegionConstraints<'tcx>;
region_outlives, ty_outlives
}
}

BraceStructTypeFoldableImpl! {
impl<'tcx, R> TypeFoldable<'tcx> for QueryResult<'tcx, R> {
var_values, region_constraints, certainty, value
Expand Down
2 changes: 2 additions & 0 deletions src/librustc/session/config.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1289,6 +1289,8 @@ options! {DebuggingOptions, DebuggingSetter, basic_debugging_options,
"tell the linker to strip debuginfo when building without debuginfo enabled."),
share_generics: Option<bool> = (None, parse_opt_bool, [TRACKED],
"make the current crate share its generic instantiations"),
chalk: bool = (false, parse_bool, [TRACKED],
"enable the experimental Chalk-based trait solving engine"),
}

pub fn default_lib_output() -> CrateType {
Expand Down
12 changes: 9 additions & 3 deletions src/librustc/traits/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -282,13 +282,16 @@ pub enum QuantifierKind {

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub enum Goal<'tcx> {
Implies(&'tcx Slice<Clause<'tcx>>, &'tcx Goal<'tcx>),
Implies(Clauses<'tcx>, &'tcx Goal<'tcx>),
And(&'tcx Goal<'tcx>, &'tcx Goal<'tcx>),
Not(&'tcx Goal<'tcx>),
DomainGoal(DomainGoal<'tcx>),
Quantified(QuantifierKind, ty::Binder<&'tcx Goal<'tcx>>)
Quantified(QuantifierKind, ty::Binder<&'tcx Goal<'tcx>>),
CannotProve,
}

pub type Goals<'tcx> = &'tcx Slice<Goal<'tcx>>;

impl<'tcx> Goal<'tcx> {
pub fn from_poly_domain_goal<'a>(
domain_goal: PolyDomainGoal<'tcx>,
Expand Down Expand Up @@ -318,6 +321,9 @@ pub enum Clause<'tcx> {
ForAll(ty::Binder<ProgramClause<'tcx>>),
}

/// Multiple clauses.
pub type Clauses<'tcx> = &'tcx Slice<Clause<'tcx>>;

/// A "program clause" has the form `D :- G1, ..., Gn`. It is saying
/// that the domain goal `D` is true if `G1...Gn` are provable. This
/// is equivalent to the implication `G1..Gn => D`; we usually write
Expand All @@ -330,7 +336,7 @@ pub struct ProgramClause<'tcx> {
pub goal: DomainGoal<'tcx>,

/// ...if we can prove these hypotheses (there may be no hypotheses at all):
pub hypotheses: &'tcx Slice<Goal<'tcx>>,
pub hypotheses: Goals<'tcx>,
}

pub type Selection<'tcx> = Vtable<'tcx, PredicateObligation<'tcx>>;
Expand Down
2 changes: 2 additions & 0 deletions src/librustc/traits/structural_impls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -491,6 +491,7 @@ impl<'tcx> fmt::Display for traits::Goal<'tcx> {
// FIXME: appropriate binder names
write!(fmt, "{}<> {{ {} }}", qkind, goal.skip_binder())
}
CannotProve => write!(fmt, "CannotProve"),
}
}
}
Expand Down Expand Up @@ -557,6 +558,7 @@ EnumTypeFoldableImpl! {
(traits::Goal::Not)(goal),
(traits::Goal::DomainGoal)(domain_goal),
(traits::Goal::Quantified)(qkind, goal),
(traits::Goal::CannotProve),
}
}

Expand Down
12 changes: 5 additions & 7 deletions src/librustc/ty/context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ use ty::subst::{Kind, Substs};
use ty::ReprOptions;
use ty::Instance;
use traits;
use traits::{Clause, Goal};
use traits::{Clause, Clauses, Goal, Goals};
use ty::{self, Ty, TypeAndMut};
use ty::{TyS, TypeVariants, Slice};
use ty::{AdtKind, AdtDef, ClosureSubsts, GeneratorInterior, Region, Const};
Expand Down Expand Up @@ -2517,15 +2517,15 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
}
}

pub fn intern_clauses(self, ts: &[Clause<'tcx>]) -> &'tcx Slice<Clause<'tcx>> {
pub fn intern_clauses(self, ts: &[Clause<'tcx>]) -> Clauses<'tcx> {
if ts.len() == 0 {
Slice::empty()
} else {
self._intern_clauses(ts)
}
}

pub fn intern_goals(self, ts: &[Goal<'tcx>]) -> &'tcx Slice<Goal<'tcx>> {
pub fn intern_goals(self, ts: &[Goal<'tcx>]) -> Goals<'tcx> {
if ts.len() == 0 {
Slice::empty()
} else {
Expand Down Expand Up @@ -2579,13 +2579,11 @@ 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 {
pub fn mk_clauses<I: InternAs<[Clause<'tcx>], Clauses<'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 {
pub fn mk_goals<I: InternAs<[Goal<'tcx>], Goals<'tcx>>>(self, iter: I) -> I::Output {
iter.intern_with(|xs| self.intern_goals(xs))
}

Expand Down
3 changes: 3 additions & 0 deletions src/librustc/ty/item_path.rs
Original file line number Diff line number Diff line change
Expand Up @@ -204,6 +204,9 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
// finer-grained distinctions, e.g. between enum/struct).
data @ DefPathData::Misc |
data @ DefPathData::TypeNs(..) |
data @ DefPathData::Trait(..) |
data @ DefPathData::AssocTypeInTrait(..) |
data @ DefPathData::AssocTypeInImpl(..) |
data @ DefPathData::ValueNs(..) |
data @ DefPathData::Module(..) |
data @ DefPathData::TypeParam(..) |
Expand Down
6 changes: 6 additions & 0 deletions src/librustc/ty/maps/config.rs
Original file line number Diff line number Diff line change
Expand Up @@ -717,6 +717,12 @@ impl<'tcx> QueryDescription<'tcx> for queries::program_clauses_for<'tcx> {
}
}

impl<'tcx> QueryDescription<'tcx> for queries::program_clauses_for_env<'tcx> {
fn describe(_tcx: TyCtxt, _: ty::ParamEnv<'tcx>) -> String {
format!("generating chalk-style clauses for param env")
}
}

impl<'tcx> QueryDescription<'tcx> for queries::wasm_import_module_map<'tcx> {
fn describe(_tcx: TyCtxt, _: CrateNum) -> String {
format!("wasm import module map")
Expand Down
9 changes: 9 additions & 0 deletions src/librustc/ty/maps/keys.rs
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,15 @@ impl<'tcx> Key for Ty<'tcx> {
}
}

impl<'tcx> Key for ty::ParamEnv<'tcx> {
fn map_crate(&self) -> CrateNum {
LOCAL_CRATE
}
fn default_span(&self, _: TyCtxt) -> Span {
DUMMY_SP
}
}

impl<'tcx, T: Key> Key for ty::ParamEnvAnd<'tcx, T> {
fn map_crate(&self) -> CrateNum {
self.value.map_crate()
Expand Down
10 changes: 7 additions & 3 deletions src/librustc/ty/maps/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,8 @@ use traits::query::{CanonicalProjectionGoal, CanonicalTyGoal, NoSolution};
use traits::query::dropck_outlives::{DtorckConstraint, DropckOutlivesResult};
use traits::query::normalize::NormalizationResult;
use traits::specialization_graph;
use traits::Clause;
use ty::{self, CrateInherentImpls, ParamEnvAnd, Slice, Ty, TyCtxt};
use traits::Clauses;
use ty::{self, CrateInherentImpls, ParamEnvAnd, Ty, TyCtxt};
use ty::steal::Steal;
use ty::subst::Substs;
use util::nodemap::{DefIdSet, DefIdMap, ItemLocalSet};
Expand Down Expand Up @@ -445,7 +445,11 @@ define_maps! { <'tcx>

[] fn features_query: features_node(CrateNum) -> Lrc<feature_gate::Features>,

[] fn program_clauses_for: ProgramClausesFor(DefId) -> Lrc<&'tcx Slice<Clause<'tcx>>>,
[] fn program_clauses_for: ProgramClausesFor(DefId) -> Clauses<'tcx>,

[] fn program_clauses_for_env: ProgramClausesForEnv(
ty::ParamEnv<'tcx>
) -> Clauses<'tcx>,

[] fn wasm_custom_sections: WasmCustomSections(CrateNum) -> Lrc<Vec<DefId>>,
[] fn wasm_import_module_map: WasmImportModuleMap(CrateNum)
Expand Down
1 change: 1 addition & 0 deletions src/librustc/ty/maps/plumbing.rs
Original file line number Diff line number Diff line change
Expand Up @@ -978,6 +978,7 @@ pub fn force_from_dep_node<'a, 'gcx, 'lcx>(tcx: TyCtxt<'a, 'gcx, 'lcx>,
DepKind::DropckOutlives |
DepKind::SubstituteNormalizeAndTestPredicates |
DepKind::InstanceDefSizeEstimate |
DepKind::ProgramClausesForEnv |

// This one should never occur in this context
DepKind::Null => {
Expand Down
5 changes: 5 additions & 0 deletions src/librustc/ty/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1138,6 +1138,11 @@ pub struct ProjectionPredicate<'tcx> {
pub type PolyProjectionPredicate<'tcx> = Binder<ProjectionPredicate<'tcx>>;

impl<'tcx> PolyProjectionPredicate<'tcx> {
/// Returns the def-id of the associated item being projected.
pub fn item_def_id(&self) -> DefId {
self.skip_binder().projection_ty.item_def_id
}

pub fn to_poly_trait_ref(&self, tcx: TyCtxt) -> PolyTraitRef<'tcx> {
// Note: unlike with TraitRef::to_poly_trait_ref(),
// self.0.trait_ref is permitted to have escaping regions.
Expand Down
Loading

0 comments on commit 898c9f7

Please sign in to comment.