Skip to content

Commit 7c396eb

Browse files
borsbors
committed
Auto merge of #48985 - scalexm:lowering, r=nikomatsakis
MVP for chalkification r? @nikomatsakis
2 parents 5e3ecdc + ef3b4e1 commit 7c396eb

File tree

14 files changed

+526
-3
lines changed

14 files changed

+526
-3
lines changed

Diff for: ‎src/librustc/dep_graph/dep_node.rs

+2
Original file line numberDiff line numberDiff line change
@@ -648,6 +648,8 @@ define_dep_nodes!( <'tcx>
648648
[] GetSymbolExportLevel(DefId),
649649

650650
[input] Features,
651+
652+
[] ProgramClausesFor(DefId),
651653
);
652654

653655
trait DepNodeParams<'a, 'gcx: 'tcx + 'a, 'tcx: 'a> : fmt::Debug {

Diff for: ‎src/librustc/ich/impls_ty.rs

+83
Original file line numberDiff line numberDiff line change
@@ -1285,3 +1285,86 @@ impl_stable_hash_for!(struct infer::canonical::QueryRegionConstraints<'tcx> {
12851285
impl_stable_hash_for!(enum infer::canonical::Certainty {
12861286
Proven, Ambiguous
12871287
});
1288+
1289+
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::WhereClauseAtom<'tcx> {
1290+
fn hash_stable<W: StableHasherResult>(&self,
1291+
hcx: &mut StableHashingContext<'a>,
1292+
hasher: &mut StableHasher<W>) {
1293+
use traits::WhereClauseAtom::*;
1294+
1295+
mem::discriminant(self).hash_stable(hcx, hasher);
1296+
match self {
1297+
Implemented(trait_ref) => trait_ref.hash_stable(hcx, hasher),
1298+
ProjectionEq(projection) => projection.hash_stable(hcx, hasher),
1299+
}
1300+
}
1301+
}
1302+
1303+
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::DomainGoal<'tcx> {
1304+
fn hash_stable<W: StableHasherResult>(&self,
1305+
hcx: &mut StableHashingContext<'a>,
1306+
hasher: &mut StableHasher<W>) {
1307+
use traits::DomainGoal::*;
1308+
1309+
mem::discriminant(self).hash_stable(hcx, hasher);
1310+
match self {
1311+
Holds(where_clause) |
1312+
WellFormed(where_clause) |
1313+
FromEnv(where_clause) => where_clause.hash_stable(hcx, hasher),
1314+
1315+
WellFormedTy(ty) => ty.hash_stable(hcx, hasher),
1316+
FromEnvTy(ty) => ty.hash_stable(hcx, hasher),
1317+
RegionOutlives(predicate) => predicate.hash_stable(hcx, hasher),
1318+
TypeOutlives(predicate) => predicate.hash_stable(hcx, hasher),
1319+
}
1320+
}
1321+
}
1322+
1323+
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Goal<'tcx> {
1324+
fn hash_stable<W: StableHasherResult>(&self,
1325+
hcx: &mut StableHashingContext<'a>,
1326+
hasher: &mut StableHasher<W>) {
1327+
use traits::Goal::*;
1328+
1329+
mem::discriminant(self).hash_stable(hcx, hasher);
1330+
match self {
1331+
Implies(hypotheses, goal) => {
1332+
hypotheses.hash_stable(hcx, hasher);
1333+
goal.hash_stable(hcx, hasher);
1334+
},
1335+
And(goal1, goal2) => {
1336+
goal1.hash_stable(hcx, hasher);
1337+
goal2.hash_stable(hcx, hasher);
1338+
}
1339+
Not(goal) => goal.hash_stable(hcx, hasher),
1340+
DomainGoal(domain_goal) => domain_goal.hash_stable(hcx, hasher),
1341+
Quantified(quantifier, goal) => {
1342+
quantifier.hash_stable(hcx, hasher);
1343+
goal.hash_stable(hcx, hasher);
1344+
},
1345+
}
1346+
}
1347+
}
1348+
1349+
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Clause<'tcx> {
1350+
fn hash_stable<W: StableHasherResult>(&self,
1351+
hcx: &mut StableHashingContext<'a>,
1352+
hasher: &mut StableHasher<W>) {
1353+
use traits::Clause::*;
1354+
1355+
mem::discriminant(self).hash_stable(hcx, hasher);
1356+
match self {
1357+
Implies(hypotheses, goal) => {
1358+
hypotheses.hash_stable(hcx, hasher);
1359+
goal.hash_stable(hcx, hasher);
1360+
}
1361+
DomainGoal(domain_goal) => domain_goal.hash_stable(hcx, hasher),
1362+
ForAll(clause) => clause.hash_stable(hcx, hasher),
1363+
}
1364+
}
1365+
}
1366+
1367+
impl_stable_hash_for!(enum traits::QuantifierKind {
1368+
Universal,
1369+
Existential
1370+
});

Diff for: ‎src/librustc/traits/mod.rs

+64
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ use infer::{InferCtxt};
2929

3030
use rustc_data_structures::sync::Lrc;
3131
use std::rc::Rc;
32+
use std::convert::From;
3233
use syntax::ast;
3334
use syntax_pos::{Span, DUMMY_SP};
3435

@@ -244,6 +245,69 @@ pub type Obligations<'tcx, O> = Vec<Obligation<'tcx, O>>;
244245
pub type PredicateObligations<'tcx> = Vec<PredicateObligation<'tcx>>;
245246
pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
246247

248+
/// The following types:
249+
/// * `WhereClauseAtom`
250+
/// * `DomainGoal`
251+
/// * `Goal`
252+
/// * `Clause`
253+
/// are used for representing the trait system in the form of
254+
/// logic programming clauses. They are part of the interface
255+
/// for the chalk SLG solver.
256+
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
257+
pub enum WhereClauseAtom<'tcx> {
258+
Implemented(ty::TraitPredicate<'tcx>),
259+
ProjectionEq(ty::ProjectionPredicate<'tcx>),
260+
}
261+
262+
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
263+
pub enum DomainGoal<'tcx> {
264+
Holds(WhereClauseAtom<'tcx>),
265+
WellFormed(WhereClauseAtom<'tcx>),
266+
FromEnv(WhereClauseAtom<'tcx>),
267+
WellFormedTy(Ty<'tcx>),
268+
FromEnvTy(Ty<'tcx>),
269+
RegionOutlives(ty::RegionOutlivesPredicate<'tcx>),
270+
TypeOutlives(ty::TypeOutlivesPredicate<'tcx>),
271+
}
272+
273+
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
274+
pub enum QuantifierKind {
275+
Universal,
276+
Existential,
277+
}
278+
279+
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
280+
pub enum Goal<'tcx> {
281+
// FIXME: use interned refs instead of `Box`
282+
Implies(Vec<Clause<'tcx>>, Box<Goal<'tcx>>),
283+
And(Box<Goal<'tcx>>, Box<Goal<'tcx>>),
284+
Not(Box<Goal<'tcx>>),
285+
DomainGoal(DomainGoal<'tcx>),
286+
Quantified(QuantifierKind, Box<ty::Binder<Goal<'tcx>>>)
287+
}
288+
289+
impl<'tcx> From<DomainGoal<'tcx>> for Goal<'tcx> {
290+
fn from(domain_goal: DomainGoal<'tcx>) -> Self {
291+
Goal::DomainGoal(domain_goal)
292+
}
293+
}
294+
295+
impl<'tcx> From<DomainGoal<'tcx>> for Clause<'tcx> {
296+
fn from(domain_goal: DomainGoal<'tcx>) -> Self {
297+
Clause::DomainGoal(domain_goal)
298+
}
299+
}
300+
301+
/// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
302+
/// Harrop Formulas".
303+
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
304+
pub enum Clause<'tcx> {
305+
// FIXME: again, use interned refs instead of `Box`
306+
Implies(Vec<Goal<'tcx>>, DomainGoal<'tcx>),
307+
DomainGoal(DomainGoal<'tcx>),
308+
ForAll(Box<ty::Binder<Clause<'tcx>>>),
309+
}
310+
247311
pub type Selection<'tcx> = Vtable<'tcx, PredicateObligation<'tcx>>;
248312

249313
#[derive(Clone,Debug)]

Diff for: ‎src/librustc/traits/structural_impls.rs

+135
Original file line numberDiff line numberDiff line change
@@ -425,3 +425,138 @@ BraceStructTypeFoldableImpl! {
425425
obligations
426426
} where T: TypeFoldable<'tcx>
427427
}
428+
429+
impl<'tcx> fmt::Display for traits::WhereClauseAtom<'tcx> {
430+
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
431+
use traits::WhereClauseAtom::*;
432+
433+
match self {
434+
Implemented(trait_ref) => write!(fmt, "Implemented({})", trait_ref),
435+
ProjectionEq(projection) => write!(fmt, "ProjectionEq({})", projection),
436+
}
437+
}
438+
}
439+
440+
impl<'tcx> fmt::Display for traits::DomainGoal<'tcx> {
441+
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
442+
use traits::DomainGoal::*;
443+
use traits::WhereClauseAtom::*;
444+
445+
match self {
446+
Holds(wc) => write!(fmt, "{}", wc),
447+
WellFormed(Implemented(trait_ref)) => write!(fmt, "WellFormed({})", trait_ref),
448+
WellFormed(ProjectionEq(projection)) => write!(fmt, "WellFormed({})", projection),
449+
FromEnv(Implemented(trait_ref)) => write!(fmt, "FromEnv({})", trait_ref),
450+
FromEnv(ProjectionEq(projection)) => write!(fmt, "FromEnv({})", projection),
451+
WellFormedTy(ty) => write!(fmt, "WellFormed({})", ty),
452+
FromEnvTy(ty) => write!(fmt, "FromEnv({})", ty),
453+
RegionOutlives(predicate) => write!(fmt, "RegionOutlives({})", predicate),
454+
TypeOutlives(predicate) => write!(fmt, "TypeOutlives({})", predicate),
455+
}
456+
}
457+
}
458+
459+
impl fmt::Display for traits::QuantifierKind {
460+
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
461+
use traits::QuantifierKind::*;
462+
463+
match self {
464+
Universal => write!(fmt, "forall"),
465+
Existential => write!(fmt, "exists"),
466+
}
467+
}
468+
}
469+
470+
impl<'tcx> fmt::Display for traits::Goal<'tcx> {
471+
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
472+
use traits::Goal::*;
473+
474+
match self {
475+
Implies(hypotheses, goal) => {
476+
write!(fmt, "if (")?;
477+
for (index, hyp) in hypotheses.iter().enumerate() {
478+
if index > 0 {
479+
write!(fmt, ", ")?;
480+
}
481+
write!(fmt, "{}", hyp)?;
482+
}
483+
write!(fmt, ") {{ {} }}", goal)
484+
}
485+
And(goal1, goal2) => write!(fmt, "({} && {})", goal1, goal2),
486+
Not(goal) => write!(fmt, "not {{ {} }}", goal),
487+
DomainGoal(goal) => write!(fmt, "{}", goal),
488+
Quantified(qkind, goal) => {
489+
// FIXME: appropriate binder names
490+
write!(fmt, "{}<> {{ {} }}", qkind, goal.skip_binder())
491+
}
492+
}
493+
}
494+
}
495+
496+
impl<'tcx> fmt::Display for traits::Clause<'tcx> {
497+
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
498+
use traits::Clause::*;
499+
500+
match self {
501+
Implies(hypotheses, goal) => {
502+
write!(fmt, "{}", goal)?;
503+
if !hypotheses.is_empty() {
504+
write!(fmt, " :- ")?;
505+
for (index, condition) in hypotheses.iter().enumerate() {
506+
if index > 0 {
507+
write!(fmt, ", ")?;
508+
}
509+
write!(fmt, "{}", condition)?;
510+
}
511+
}
512+
write!(fmt, ".")
513+
}
514+
DomainGoal(domain_goal) => write!(fmt, "{}.", domain_goal),
515+
ForAll(clause) => {
516+
// FIXME: appropriate binder names
517+
write!(fmt, "forall<> {{ {} }}", clause.skip_binder())
518+
}
519+
}
520+
}
521+
}
522+
523+
EnumTypeFoldableImpl! {
524+
impl<'tcx> TypeFoldable<'tcx> for traits::WhereClauseAtom<'tcx> {
525+
(traits::WhereClauseAtom::Implemented)(trait_ref),
526+
(traits::WhereClauseAtom::ProjectionEq)(projection),
527+
}
528+
}
529+
530+
EnumTypeFoldableImpl! {
531+
impl<'tcx> TypeFoldable<'tcx> for traits::DomainGoal<'tcx> {
532+
(traits::DomainGoal::Holds)(wc),
533+
(traits::DomainGoal::WellFormed)(wc),
534+
(traits::DomainGoal::FromEnv)(wc),
535+
(traits::DomainGoal::WellFormedTy)(ty),
536+
(traits::DomainGoal::FromEnvTy)(ty),
537+
(traits::DomainGoal::RegionOutlives)(predicate),
538+
(traits::DomainGoal::TypeOutlives)(predicate),
539+
}
540+
}
541+
542+
CloneTypeFoldableImpls! {
543+
traits::QuantifierKind,
544+
}
545+
546+
EnumTypeFoldableImpl! {
547+
impl<'tcx> TypeFoldable<'tcx> for traits::Goal<'tcx> {
548+
(traits::Goal::Implies)(hypotheses, goal),
549+
(traits::Goal::And)(goal1, goal2),
550+
(traits::Goal::Not)(goal),
551+
(traits::Goal::DomainGoal)(domain_goal),
552+
(traits::Goal::Quantified)(qkind, goal),
553+
}
554+
}
555+
556+
EnumTypeFoldableImpl! {
557+
impl<'tcx> TypeFoldable<'tcx> for traits::Clause<'tcx> {
558+
(traits::Clause::Implies)(hypotheses, goal),
559+
(traits::Clause::DomainGoal)(domain_goal),
560+
(traits::Clause::ForAll)(clause),
561+
}
562+
}

Diff for: ‎src/librustc/ty/maps/config.rs

+6
Original file line numberDiff line numberDiff line change
@@ -693,6 +693,12 @@ impl<'tcx> QueryDescription<'tcx> for queries::generics_of<'tcx> {
693693
}
694694
}
695695

696+
impl<'tcx> QueryDescription<'tcx> for queries::program_clauses_for<'tcx> {
697+
fn describe(_tcx: TyCtxt, _: DefId) -> String {
698+
format!("generating chalk-style clauses")
699+
}
700+
}
701+
696702
macro_rules! impl_disk_cacheable_query(
697703
($query_name:ident, |$key:tt| $cond:expr) => {
698704
impl<'tcx> QueryDescription<'tcx> for queries::$query_name<'tcx> {

Diff for: ‎src/librustc/ty/maps/mod.rs

+3
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ use traits::query::{CanonicalProjectionGoal, CanonicalTyGoal, NoSolution};
3838
use traits::query::dropck_outlives::{DtorckConstraint, DropckOutlivesResult};
3939
use traits::query::normalize::NormalizationResult;
4040
use traits::specialization_graph;
41+
use traits::Clause;
4142
use ty::{self, CrateInherentImpls, ParamEnvAnd, Ty, TyCtxt};
4243
use ty::steal::Steal;
4344
use ty::subst::Substs;
@@ -417,6 +418,8 @@ define_maps! { <'tcx>
417418
-> usize,
418419

419420
[] fn features_query: features_node(CrateNum) -> Lrc<feature_gate::Features>,
421+
422+
[] fn program_clauses_for: ProgramClausesFor(DefId) -> Lrc<Vec<Clause<'tcx>>>,
420423
}
421424

422425
//////////////////////////////////////////////////////////////////////

Diff for: ‎src/librustc/ty/maps/plumbing.rs

+2
Original file line numberDiff line numberDiff line change
@@ -935,6 +935,8 @@ pub fn force_from_dep_node<'a, 'gcx, 'lcx>(tcx: TyCtxt<'a, 'gcx, 'lcx>,
935935

936936
DepKind::GetSymbolExportLevel => { force!(symbol_export_level, def_id!()); }
937937
DepKind::Features => { force!(features_query, LOCAL_CRATE); }
938+
939+
DepKind::ProgramClausesFor => { force!(program_clauses_for, def_id!()); }
938940
}
939941

940942
true

Diff for: ‎src/librustc/ty/mod.rs

+6-3
Original file line numberDiff line numberDiff line change
@@ -1073,9 +1073,12 @@ impl<'tcx> PolyTraitPredicate<'tcx> {
10731073
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, RustcEncodable, RustcDecodable)]
10741074
pub struct OutlivesPredicate<A,B>(pub A, pub B); // `A : B`
10751075
pub type PolyOutlivesPredicate<A,B> = ty::Binder<OutlivesPredicate<A,B>>;
1076-
pub type PolyRegionOutlivesPredicate<'tcx> = PolyOutlivesPredicate<ty::Region<'tcx>,
1077-
ty::Region<'tcx>>;
1078-
pub type PolyTypeOutlivesPredicate<'tcx> = PolyOutlivesPredicate<Ty<'tcx>, ty::Region<'tcx>>;
1076+
pub type RegionOutlivesPredicate<'tcx> = OutlivesPredicate<ty::Region<'tcx>,
1077+
ty::Region<'tcx>>;
1078+
pub type TypeOutlivesPredicate<'tcx> = OutlivesPredicate<Ty<'tcx>,
1079+
ty::Region<'tcx>>;
1080+
pub type PolyRegionOutlivesPredicate<'tcx> = ty::Binder<RegionOutlivesPredicate<'tcx>>;
1081+
pub type PolyTypeOutlivesPredicate<'tcx> = ty::Binder<TypeOutlivesPredicate<'tcx>>;
10791082

10801083
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, RustcEncodable, RustcDecodable)]
10811084
pub struct SubtypePredicate<'tcx> {

Diff for: ‎src/librustc_driver/driver.rs

+4
Original file line numberDiff line numberDiff line change
@@ -1091,6 +1091,10 @@ pub fn phase_3_run_analysis_passes<'tcx, F, R>(trans: &TransCrate,
10911091

10921092
time(sess, "lint checking", || lint::check_crate(tcx));
10931093

1094+
time(sess,
1095+
"dumping chalk-like clauses",
1096+
|| rustc_traits::lowering::dump_program_clauses(tcx));
1097+
10941098
return Ok(f(tcx, analysis, rx, tcx.sess.compile_status()));
10951099
})
10961100
}

Diff for: ‎src/librustc_traits/lib.rs

+2
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ mod dropck_outlives;
2929
mod normalize_projection_ty;
3030
mod normalize_erasing_regions;
3131
mod util;
32+
pub mod lowering;
3233

3334
use rustc::ty::maps::Providers;
3435

@@ -39,6 +40,7 @@ pub fn provide(p: &mut Providers) {
3940
normalize_projection_ty: normalize_projection_ty::normalize_projection_ty,
4041
normalize_ty_after_erasing_regions:
4142
normalize_erasing_regions::normalize_ty_after_erasing_regions,
43+
program_clauses_for: lowering::program_clauses_for,
4244
..*p
4345
};
4446
}

0 commit comments

Comments
 (0)