mirror of https://github.com/rust-lang/rust.git
Pass around interned refs to goals and not goals
This commit is contained in:
parent
25a75a4d86
commit
663002f222
|
@ -270,7 +270,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "chalk-engine"
|
name = "chalk-engine"
|
||||||
version = "0.7.0"
|
version = "0.8.0"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"chalk-macros 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)",
|
"chalk-macros 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||||
|
@ -1898,7 +1898,7 @@ dependencies = [
|
||||||
"backtrace 0.3.9 (registry+https://github.com/rust-lang/crates.io-index)",
|
"backtrace 0.3.9 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||||
"bitflags 1.0.4 (registry+https://github.com/rust-lang/crates.io-index)",
|
"bitflags 1.0.4 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||||
"byteorder 1.2.3 (registry+https://github.com/rust-lang/crates.io-index)",
|
"byteorder 1.2.3 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||||
"chalk-engine 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)",
|
"chalk-engine 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||||
"flate2 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
|
"flate2 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||||
"fmt_macros 0.0.0",
|
"fmt_macros 0.0.0",
|
||||||
"graphviz 0.0.0",
|
"graphviz 0.0.0",
|
||||||
|
@ -2434,7 +2434,7 @@ name = "rustc_traits"
|
||||||
version = "0.0.0"
|
version = "0.0.0"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"bitflags 1.0.4 (registry+https://github.com/rust-lang/crates.io-index)",
|
"bitflags 1.0.4 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||||
"chalk-engine 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)",
|
"chalk-engine 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||||
"graphviz 0.0.0",
|
"graphviz 0.0.0",
|
||||||
"log 0.4.4 (registry+https://github.com/rust-lang/crates.io-index)",
|
"log 0.4.4 (registry+https://github.com/rust-lang/crates.io-index)",
|
||||||
"rustc 0.0.0",
|
"rustc 0.0.0",
|
||||||
|
@ -3195,7 +3195,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
"checksum cargo_metadata 0.6.0 (registry+https://github.com/rust-lang/crates.io-index)" = "2d6809b327f87369e6f3651efd2c5a96c49847a3ed2559477ecba79014751ee1"
|
"checksum cargo_metadata 0.6.0 (registry+https://github.com/rust-lang/crates.io-index)" = "2d6809b327f87369e6f3651efd2c5a96c49847a3ed2559477ecba79014751ee1"
|
||||||
"checksum cc 1.0.25 (registry+https://github.com/rust-lang/crates.io-index)" = "f159dfd43363c4d08055a07703eb7a3406b0dac4d0584d96965a3262db3c9d16"
|
"checksum cc 1.0.25 (registry+https://github.com/rust-lang/crates.io-index)" = "f159dfd43363c4d08055a07703eb7a3406b0dac4d0584d96965a3262db3c9d16"
|
||||||
"checksum cfg-if 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "0c4e7bb64a8ebb0d856483e1e682ea3422f883c5f5615a90d51a2c82fe87fdd3"
|
"checksum cfg-if 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "0c4e7bb64a8ebb0d856483e1e682ea3422f883c5f5615a90d51a2c82fe87fdd3"
|
||||||
"checksum chalk-engine 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "25ce2f28f55ed544a2a3756b7acf41dd7d6f27acffb2086439950925506af7d0"
|
"checksum chalk-engine 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)" = "6749eb72e7d4355d944a99f15fbaea701b978c18c5e184a025fcde942b0c9779"
|
||||||
"checksum chalk-macros 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)" = "295635afd6853aa9f20baeb7f0204862440c0fe994c5a253d5f479dac41d047e"
|
"checksum chalk-macros 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)" = "295635afd6853aa9f20baeb7f0204862440c0fe994c5a253d5f479dac41d047e"
|
||||||
"checksum chrono 0.4.4 (registry+https://github.com/rust-lang/crates.io-index)" = "6962c635d530328acc53ac6a955e83093fedc91c5809dfac1fa60fa470830a37"
|
"checksum chrono 0.4.4 (registry+https://github.com/rust-lang/crates.io-index)" = "6962c635d530328acc53ac6a955e83093fedc91c5809dfac1fa60fa470830a37"
|
||||||
"checksum clap 2.32.0 (registry+https://github.com/rust-lang/crates.io-index)" = "b957d88f4b6a63b9d70d5f454ac8011819c6efa7727858f458ab71c756ce2d3e"
|
"checksum clap 2.32.0 (registry+https://github.com/rust-lang/crates.io-index)" = "b957d88f4b6a63b9d70d5f454ac8011819c6efa7727858f458ab71c756ce2d3e"
|
||||||
|
|
|
@ -31,7 +31,7 @@ syntax_pos = { path = "../libsyntax_pos" }
|
||||||
backtrace = "0.3.3"
|
backtrace = "0.3.3"
|
||||||
parking_lot = "0.6"
|
parking_lot = "0.6"
|
||||||
byteorder = { version = "1.1", features = ["i128"]}
|
byteorder = { version = "1.1", features = ["i128"]}
|
||||||
chalk-engine = { version = "0.7.0", default-features=false }
|
chalk-engine = { version = "0.8.0", default-features=false }
|
||||||
rustc_fs_util = { path = "../librustc_fs_util" }
|
rustc_fs_util = { path = "../librustc_fs_util" }
|
||||||
smallvec = { version = "0.6.5", features = ["union"] }
|
smallvec = { version = "0.6.5", features = ["union"] }
|
||||||
|
|
||||||
|
|
|
@ -1356,7 +1356,7 @@ impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Goal<'tcx> {
|
||||||
fn hash_stable<W: StableHasherResult>(&self,
|
fn hash_stable<W: StableHasherResult>(&self,
|
||||||
hcx: &mut StableHashingContext<'a>,
|
hcx: &mut StableHashingContext<'a>,
|
||||||
hasher: &mut StableHasher<W>) {
|
hasher: &mut StableHasher<W>) {
|
||||||
use traits::Goal::*;
|
use traits::GoalKind::*;
|
||||||
|
|
||||||
mem::discriminant(self).hash_stable(hcx, hasher);
|
mem::discriminant(self).hash_stable(hcx, hasher);
|
||||||
match self {
|
match self {
|
||||||
|
|
|
@ -318,31 +318,33 @@ pub enum QuantifierKind {
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
|
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
|
||||||
pub enum Goal<'tcx> {
|
pub enum GoalKind<'tcx> {
|
||||||
Implies(Clauses<'tcx>, &'tcx Goal<'tcx>),
|
Implies(Clauses<'tcx>, Goal<'tcx>),
|
||||||
And(&'tcx Goal<'tcx>, &'tcx Goal<'tcx>),
|
And(Goal<'tcx>, Goal<'tcx>),
|
||||||
Not(&'tcx Goal<'tcx>),
|
Not(Goal<'tcx>),
|
||||||
DomainGoal(DomainGoal<'tcx>),
|
DomainGoal(DomainGoal<'tcx>),
|
||||||
Quantified(QuantifierKind, ty::Binder<&'tcx Goal<'tcx>>),
|
Quantified(QuantifierKind, ty::Binder<Goal<'tcx>>),
|
||||||
CannotProve,
|
CannotProve,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub type Goal<'tcx> = &'tcx GoalKind<'tcx>;
|
||||||
|
|
||||||
pub type Goals<'tcx> = &'tcx List<Goal<'tcx>>;
|
pub type Goals<'tcx> = &'tcx List<Goal<'tcx>>;
|
||||||
|
|
||||||
impl<'tcx> DomainGoal<'tcx> {
|
impl<'tcx> DomainGoal<'tcx> {
|
||||||
pub fn into_goal(self) -> Goal<'tcx> {
|
pub fn into_goal(self) -> GoalKind<'tcx> {
|
||||||
Goal::DomainGoal(self)
|
GoalKind::DomainGoal(self)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> Goal<'tcx> {
|
impl<'tcx> GoalKind<'tcx> {
|
||||||
pub fn from_poly_domain_goal<'a>(
|
pub fn from_poly_domain_goal<'a>(
|
||||||
domain_goal: PolyDomainGoal<'tcx>,
|
domain_goal: PolyDomainGoal<'tcx>,
|
||||||
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
||||||
) -> Goal<'tcx> {
|
) -> GoalKind<'tcx> {
|
||||||
match domain_goal.no_late_bound_regions() {
|
match domain_goal.no_late_bound_regions() {
|
||||||
Some(p) => p.into_goal(),
|
Some(p) => p.into_goal(),
|
||||||
None => Goal::Quantified(
|
None => GoalKind::Quantified(
|
||||||
QuantifierKind::Universal,
|
QuantifierKind::Universal,
|
||||||
domain_goal.map_bound(|p| tcx.mk_goal(p.into_goal()))
|
domain_goal.map_bound(|p| tcx.mk_goal(p.into_goal()))
|
||||||
),
|
),
|
||||||
|
|
|
@ -469,7 +469,7 @@ impl fmt::Display for traits::QuantifierKind {
|
||||||
|
|
||||||
impl<'tcx> fmt::Display for traits::Goal<'tcx> {
|
impl<'tcx> fmt::Display for traits::Goal<'tcx> {
|
||||||
fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
|
fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||||
use traits::Goal::*;
|
use traits::GoalKind::*;
|
||||||
|
|
||||||
match self {
|
match self {
|
||||||
Implies(hypotheses, goal) => {
|
Implies(hypotheses, goal) => {
|
||||||
|
@ -598,25 +598,25 @@ CloneTypeFoldableAndLiftImpls! {
|
||||||
}
|
}
|
||||||
|
|
||||||
EnumTypeFoldableImpl! {
|
EnumTypeFoldableImpl! {
|
||||||
impl<'tcx> TypeFoldable<'tcx> for traits::Goal<'tcx> {
|
impl<'tcx> TypeFoldable<'tcx> for traits::GoalKind<'tcx> {
|
||||||
(traits::Goal::Implies)(hypotheses, goal),
|
(traits::GoalKind::Implies)(hypotheses, goal),
|
||||||
(traits::Goal::And)(goal1, goal2),
|
(traits::GoalKind::And)(goal1, goal2),
|
||||||
(traits::Goal::Not)(goal),
|
(traits::GoalKind::Not)(goal),
|
||||||
(traits::Goal::DomainGoal)(domain_goal),
|
(traits::GoalKind::DomainGoal)(domain_goal),
|
||||||
(traits::Goal::Quantified)(qkind, goal),
|
(traits::GoalKind::Quantified)(qkind, goal),
|
||||||
(traits::Goal::CannotProve),
|
(traits::GoalKind::CannotProve),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
EnumLiftImpl! {
|
EnumLiftImpl! {
|
||||||
impl<'a, 'tcx> Lift<'tcx> for traits::Goal<'a> {
|
impl<'a, 'tcx> Lift<'tcx> for traits::GoalKind<'a> {
|
||||||
type Lifted = traits::Goal<'tcx>;
|
type Lifted = traits::GoalKind<'tcx>;
|
||||||
(traits::Goal::Implies)(hypotheses, goal),
|
(traits::GoalKind::Implies)(hypotheses, goal),
|
||||||
(traits::Goal::And)(goal1, goal2),
|
(traits::GoalKind::And)(goal1, goal2),
|
||||||
(traits::Goal::Not)(goal),
|
(traits::GoalKind::Not)(goal),
|
||||||
(traits::Goal::DomainGoal)(domain_goal),
|
(traits::GoalKind::DomainGoal)(domain_goal),
|
||||||
(traits::Goal::Quantified)(kind, goal),
|
(traits::GoalKind::Quantified)(kind, goal),
|
||||||
(traits::Goal::CannotProve),
|
(traits::GoalKind::CannotProve),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -633,7 +633,7 @@ impl<'tcx> TypeFoldable<'tcx> for &'tcx ty::List<traits::Goal<'tcx>> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> TypeFoldable<'tcx> for &'tcx traits::Goal<'tcx> {
|
impl<'tcx> TypeFoldable<'tcx> for traits::Goal<'tcx> {
|
||||||
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
|
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
|
||||||
let v = (**self).fold_with(folder);
|
let v = (**self).fold_with(folder);
|
||||||
folder.tcx().mk_goal(v)
|
folder.tcx().mk_goal(v)
|
||||||
|
|
|
@ -36,7 +36,7 @@ use mir::interpret::Allocation;
|
||||||
use ty::subst::{CanonicalSubsts, Kind, Substs, Subst};
|
use ty::subst::{CanonicalSubsts, Kind, Substs, Subst};
|
||||||
use ty::ReprOptions;
|
use ty::ReprOptions;
|
||||||
use traits;
|
use traits;
|
||||||
use traits::{Clause, Clauses, Goal, Goals};
|
use traits::{Clause, Clauses, GoalKind, Goal, Goals};
|
||||||
use ty::{self, Ty, TypeAndMut};
|
use ty::{self, Ty, TypeAndMut};
|
||||||
use ty::{TyS, TyKind, List};
|
use ty::{TyS, TyKind, List};
|
||||||
use ty::{AdtKind, AdtDef, ClosureSubsts, GeneratorSubsts, Region, Const};
|
use ty::{AdtKind, AdtDef, ClosureSubsts, GeneratorSubsts, Region, Const};
|
||||||
|
@ -143,7 +143,8 @@ pub struct CtxtInterners<'tcx> {
|
||||||
predicates: InternedSet<'tcx, List<Predicate<'tcx>>>,
|
predicates: InternedSet<'tcx, List<Predicate<'tcx>>>,
|
||||||
const_: InternedSet<'tcx, Const<'tcx>>,
|
const_: InternedSet<'tcx, Const<'tcx>>,
|
||||||
clauses: InternedSet<'tcx, List<Clause<'tcx>>>,
|
clauses: InternedSet<'tcx, List<Clause<'tcx>>>,
|
||||||
goals: InternedSet<'tcx, List<Goal<'tcx>>>,
|
goal: InternedSet<'tcx, GoalKind<'tcx>>,
|
||||||
|
goal_list: InternedSet<'tcx, List<Goal<'tcx>>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'gcx: 'tcx, 'tcx> CtxtInterners<'tcx> {
|
impl<'gcx: 'tcx, 'tcx> CtxtInterners<'tcx> {
|
||||||
|
@ -159,7 +160,8 @@ impl<'gcx: 'tcx, 'tcx> CtxtInterners<'tcx> {
|
||||||
predicates: Default::default(),
|
predicates: Default::default(),
|
||||||
const_: Default::default(),
|
const_: Default::default(),
|
||||||
clauses: Default::default(),
|
clauses: Default::default(),
|
||||||
goals: Default::default(),
|
goal: Default::default(),
|
||||||
|
goal_list: Default::default(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1731,9 +1733,9 @@ impl<'a, 'tcx> Lift<'tcx> for Region<'a> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'a, 'tcx> Lift<'tcx> for &'a Goal<'a> {
|
impl<'a, 'tcx> Lift<'tcx> for Goal<'a> {
|
||||||
type Lifted = &'tcx Goal<'tcx>;
|
type Lifted = Goal<'tcx>;
|
||||||
fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<&'tcx Goal<'tcx>> {
|
fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Goal<'tcx>> {
|
||||||
if tcx.interners.arena.in_arena(*self as *const _) {
|
if tcx.interners.arena.in_arena(*self as *const _) {
|
||||||
return Some(unsafe { mem::transmute(*self) });
|
return Some(unsafe { mem::transmute(*self) });
|
||||||
}
|
}
|
||||||
|
@ -2304,6 +2306,12 @@ impl<'tcx> Borrow<RegionKind> for Interned<'tcx, RegionKind> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl<'tcx: 'lcx, 'lcx> Borrow<GoalKind<'lcx>> for Interned<'tcx, GoalKind<'tcx>> {
|
||||||
|
fn borrow<'a>(&'a self) -> &'a GoalKind<'lcx> {
|
||||||
|
&self.0
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
impl<'tcx: 'lcx, 'lcx> Borrow<[ExistentialPredicate<'lcx>]>
|
impl<'tcx: 'lcx, 'lcx> Borrow<[ExistentialPredicate<'lcx>]>
|
||||||
for Interned<'tcx, List<ExistentialPredicate<'tcx>>> {
|
for Interned<'tcx, List<ExistentialPredicate<'tcx>>> {
|
||||||
fn borrow<'a>(&'a self) -> &'a [ExistentialPredicate<'lcx>] {
|
fn borrow<'a>(&'a self) -> &'a [ExistentialPredicate<'lcx>] {
|
||||||
|
@ -2419,7 +2427,8 @@ pub fn keep_local<'tcx, T: ty::TypeFoldable<'tcx>>(x: &T) -> bool {
|
||||||
|
|
||||||
direct_interners!('tcx,
|
direct_interners!('tcx,
|
||||||
region: mk_region(|r: &RegionKind| r.keep_in_local_tcx()) -> RegionKind,
|
region: mk_region(|r: &RegionKind| r.keep_in_local_tcx()) -> RegionKind,
|
||||||
const_: mk_const(|c: &Const<'_>| keep_local(&c.ty) || keep_local(&c.val)) -> Const<'tcx>
|
const_: mk_const(|c: &Const<'_>| keep_local(&c.ty) || keep_local(&c.val)) -> Const<'tcx>,
|
||||||
|
goal: mk_goal(|c: &GoalKind<'_>| keep_local(c)) -> GoalKind<'tcx>
|
||||||
);
|
);
|
||||||
|
|
||||||
macro_rules! slice_interners {
|
macro_rules! slice_interners {
|
||||||
|
@ -2438,7 +2447,7 @@ slice_interners!(
|
||||||
type_list: _intern_type_list(Ty),
|
type_list: _intern_type_list(Ty),
|
||||||
substs: _intern_substs(Kind),
|
substs: _intern_substs(Kind),
|
||||||
clauses: _intern_clauses(Clause),
|
clauses: _intern_clauses(Clause),
|
||||||
goals: _intern_goals(Goal)
|
goal_list: _intern_goals(Goal)
|
||||||
);
|
);
|
||||||
|
|
||||||
// This isn't a perfect fit: CanonicalVarInfo slices are always
|
// This isn't a perfect fit: CanonicalVarInfo slices are always
|
||||||
|
@ -2818,10 +2827,6 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
|
||||||
iter.intern_with(|xs| self.intern_goals(xs))
|
iter.intern_with(|xs| self.intern_goals(xs))
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn mk_goal(self, goal: Goal<'tcx>) -> &'tcx Goal<'_> {
|
|
||||||
&self.intern_goals(&[goal])[0]
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn lint_hir<S: Into<MultiSpan>>(self,
|
pub fn lint_hir<S: Into<MultiSpan>>(self,
|
||||||
lint: &'static Lint,
|
lint: &'static Lint,
|
||||||
hir_id: HirId,
|
hir_id: HirId,
|
||||||
|
|
|
@ -16,5 +16,5 @@ rustc = { path = "../librustc" }
|
||||||
rustc_data_structures = { path = "../librustc_data_structures" }
|
rustc_data_structures = { path = "../librustc_data_structures" }
|
||||||
syntax = { path = "../libsyntax" }
|
syntax = { path = "../libsyntax" }
|
||||||
syntax_pos = { path = "../libsyntax_pos" }
|
syntax_pos = { path = "../libsyntax_pos" }
|
||||||
chalk-engine = { version = "0.7.0", default-features=false }
|
chalk-engine = { version = "0.8.0", default-features=false }
|
||||||
smallvec = { version = "0.6.5", features = ["union"] }
|
smallvec = { version = "0.6.5", features = ["union"] }
|
||||||
|
|
|
@ -19,6 +19,7 @@ use rustc::traits::{
|
||||||
ExClauseFold,
|
ExClauseFold,
|
||||||
ExClauseLift,
|
ExClauseLift,
|
||||||
Goal,
|
Goal,
|
||||||
|
GoalKind,
|
||||||
ProgramClause,
|
ProgramClause,
|
||||||
QuantifierKind
|
QuantifierKind
|
||||||
};
|
};
|
||||||
|
@ -92,7 +93,7 @@ impl context::Context for ChalkArenas<'tcx> {
|
||||||
|
|
||||||
type DomainGoal = DomainGoal<'tcx>;
|
type DomainGoal = DomainGoal<'tcx>;
|
||||||
|
|
||||||
type BindersGoal = ty::Binder<&'tcx Goal<'tcx>>;
|
type BindersGoal = ty::Binder<Goal<'tcx>>;
|
||||||
|
|
||||||
type Parameter = Kind<'tcx>;
|
type Parameter = Kind<'tcx>;
|
||||||
|
|
||||||
|
@ -102,14 +103,6 @@ impl context::Context for ChalkArenas<'tcx> {
|
||||||
|
|
||||||
type UnificationResult = InferOk<'tcx, ()>;
|
type UnificationResult = InferOk<'tcx, ()>;
|
||||||
|
|
||||||
fn into_goal(domain_goal: DomainGoal<'tcx>) -> Goal<'tcx> {
|
|
||||||
Goal::DomainGoal(domain_goal)
|
|
||||||
}
|
|
||||||
|
|
||||||
fn cannot_prove() -> Goal<'tcx> {
|
|
||||||
Goal::CannotProve
|
|
||||||
}
|
|
||||||
|
|
||||||
fn goal_in_environment(
|
fn goal_in_environment(
|
||||||
env: &ty::ParamEnv<'tcx>,
|
env: &ty::ParamEnv<'tcx>,
|
||||||
goal: Goal<'tcx>,
|
goal: Goal<'tcx>,
|
||||||
|
@ -251,15 +244,23 @@ impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
|
||||||
impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||||
for ChalkInferenceContext<'cx, 'gcx, 'tcx>
|
for ChalkInferenceContext<'cx, 'gcx, 'tcx>
|
||||||
{
|
{
|
||||||
|
fn into_goal(&self, domain_goal: DomainGoal<'tcx>) -> Goal<'tcx> {
|
||||||
|
self.infcx.tcx.mk_goal(GoalKind::DomainGoal(domain_goal))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn cannot_prove(&self) -> Goal<'tcx> {
|
||||||
|
self.infcx.tcx.mk_goal(GoalKind::CannotProve)
|
||||||
|
}
|
||||||
|
|
||||||
fn into_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
|
fn into_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
|
||||||
match goal {
|
match *goal {
|
||||||
Goal::Implies(..) => panic!("FIXME rust-lang-nursery/chalk#94"),
|
GoalKind::Implies(..) => panic!("FIXME rust-lang-nursery/chalk#94"),
|
||||||
Goal::And(left, right) => HhGoal::And(*left, *right),
|
GoalKind::And(left, right) => HhGoal::And(left, right),
|
||||||
Goal::Not(subgoal) => HhGoal::Not(*subgoal),
|
GoalKind::Not(subgoal) => HhGoal::Not(subgoal),
|
||||||
Goal::DomainGoal(d) => HhGoal::DomainGoal(d),
|
GoalKind::DomainGoal(d) => HhGoal::DomainGoal(d),
|
||||||
Goal::Quantified(QuantifierKind::Universal, binder) => HhGoal::ForAll(binder),
|
GoalKind::Quantified(QuantifierKind::Universal, binder) => HhGoal::ForAll(binder),
|
||||||
Goal::Quantified(QuantifierKind::Existential, binder) => HhGoal::Exists(binder),
|
GoalKind::Quantified(QuantifierKind::Existential, binder) => HhGoal::Exists(binder),
|
||||||
Goal::CannotProve => HhGoal::CannotProve,
|
GoalKind::CannotProve => HhGoal::CannotProve,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -363,21 +364,21 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||||
|
|
||||||
fn instantiate_binders_universally(
|
fn instantiate_binders_universally(
|
||||||
&mut self,
|
&mut self,
|
||||||
_arg: &ty::Binder<&'tcx Goal<'tcx>>,
|
_arg: &ty::Binder<Goal<'tcx>>,
|
||||||
) -> Goal<'tcx> {
|
) -> Goal<'tcx> {
|
||||||
panic!("FIXME -- universal instantiation needs sgrif's branch")
|
panic!("FIXME -- universal instantiation needs sgrif's branch")
|
||||||
}
|
}
|
||||||
|
|
||||||
fn instantiate_binders_existentially(
|
fn instantiate_binders_existentially(
|
||||||
&mut self,
|
&mut self,
|
||||||
arg: &ty::Binder<&'tcx Goal<'tcx>>,
|
arg: &ty::Binder<Goal<'tcx>>,
|
||||||
) -> Goal<'tcx> {
|
) -> Goal<'tcx> {
|
||||||
let (value, _map) = self.infcx.replace_late_bound_regions_with_fresh_var(
|
let (value, _map) = self.infcx.replace_late_bound_regions_with_fresh_var(
|
||||||
DUMMY_SP,
|
DUMMY_SP,
|
||||||
LateBoundRegionConversionTime::HigherRankedType,
|
LateBoundRegionConversionTime::HigherRankedType,
|
||||||
arg,
|
arg,
|
||||||
);
|
);
|
||||||
*value
|
value
|
||||||
}
|
}
|
||||||
|
|
||||||
fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
|
fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
|
||||||
|
|
|
@ -13,7 +13,14 @@ use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
|
||||||
use rustc::hir::map::definitions::DefPathData;
|
use rustc::hir::map::definitions::DefPathData;
|
||||||
use rustc::hir::{self, ImplPolarity};
|
use rustc::hir::{self, ImplPolarity};
|
||||||
use rustc::traits::{
|
use rustc::traits::{
|
||||||
Clause, Clauses, DomainGoal, FromEnv, Goal, PolyDomainGoal, ProgramClause, WellFormed,
|
Clause,
|
||||||
|
Clauses,
|
||||||
|
DomainGoal,
|
||||||
|
FromEnv,
|
||||||
|
GoalKind,
|
||||||
|
PolyDomainGoal,
|
||||||
|
ProgramClause,
|
||||||
|
WellFormed,
|
||||||
WhereClause,
|
WhereClause,
|
||||||
};
|
};
|
||||||
use rustc::ty::query::Providers;
|
use rustc::ty::query::Providers;
|
||||||
|
@ -249,7 +256,7 @@ fn program_clauses_for_trait<'a, 'tcx>(
|
||||||
let impl_trait: DomainGoal = trait_pred.lower();
|
let impl_trait: DomainGoal = trait_pred.lower();
|
||||||
|
|
||||||
// `FromEnv(Self: Trait<P1..Pn>)`
|
// `FromEnv(Self: Trait<P1..Pn>)`
|
||||||
let from_env_goal = impl_trait.into_from_env_goal().into_goal();
|
let from_env_goal = tcx.mk_goal(impl_trait.into_from_env_goal().into_goal());
|
||||||
let hypotheses = tcx.intern_goals(&[from_env_goal]);
|
let hypotheses = tcx.intern_goals(&[from_env_goal]);
|
||||||
|
|
||||||
// `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
|
// `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
|
||||||
|
@ -308,7 +315,7 @@ fn program_clauses_for_trait<'a, 'tcx>(
|
||||||
let wf_clause = ProgramClause {
|
let wf_clause = ProgramClause {
|
||||||
goal: DomainGoal::WellFormed(WellFormed::Trait(trait_pred)),
|
goal: DomainGoal::WellFormed(WellFormed::Trait(trait_pred)),
|
||||||
hypotheses: tcx.mk_goals(
|
hypotheses: tcx.mk_goals(
|
||||||
wf_conditions.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
|
wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
||||||
),
|
),
|
||||||
};
|
};
|
||||||
let wf_clause = iter::once(Clause::ForAll(ty::Binder::dummy(wf_clause)));
|
let wf_clause = iter::once(Clause::ForAll(ty::Binder::dummy(wf_clause)));
|
||||||
|
@ -352,7 +359,7 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
|
||||||
hypotheses: tcx.mk_goals(
|
hypotheses: tcx.mk_goals(
|
||||||
where_clauses
|
where_clauses
|
||||||
.into_iter()
|
.into_iter()
|
||||||
.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
|
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
||||||
),
|
),
|
||||||
};
|
};
|
||||||
tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))])
|
tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))])
|
||||||
|
@ -388,7 +395,7 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
|
||||||
where_clauses
|
where_clauses
|
||||||
.iter()
|
.iter()
|
||||||
.cloned()
|
.cloned()
|
||||||
.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
|
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
||||||
),
|
),
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -404,7 +411,7 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
|
||||||
// ```
|
// ```
|
||||||
|
|
||||||
// `FromEnv(Ty<...>)`
|
// `FromEnv(Ty<...>)`
|
||||||
let from_env_goal = DomainGoal::FromEnv(FromEnv::Ty(ty)).into_goal();
|
let from_env_goal = tcx.mk_goal(DomainGoal::FromEnv(FromEnv::Ty(ty)).into_goal());
|
||||||
let hypotheses = tcx.intern_goals(&[from_env_goal]);
|
let hypotheses = tcx.intern_goals(&[from_env_goal]);
|
||||||
|
|
||||||
// For each where clause `WC`:
|
// For each where clause `WC`:
|
||||||
|
@ -482,7 +489,7 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
|
||||||
hypotheses: tcx.mk_goals(
|
hypotheses: tcx.mk_goals(
|
||||||
hypotheses
|
hypotheses
|
||||||
.into_iter()
|
.into_iter()
|
||||||
.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
|
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
||||||
),
|
),
|
||||||
};
|
};
|
||||||
tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))])
|
tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))])
|
||||||
|
|
Loading…
Reference in New Issue