implement the chalk traits, albeit with many placeholders

This commit is contained in:
Niko Matsakis 2018-05-08 18:15:48 -03:00
parent d022dd48cc
commit 6f425a9201
10 changed files with 881 additions and 155 deletions

View File

@ -26,6 +26,7 @@ syntax = { path = "../libsyntax" }
syntax_pos = { path = "../libsyntax_pos" }
backtrace = "0.3.3"
byteorder = { version = "1.1", features = ["i128"]}
chalk-engine = { version = "0.6.0", default-features=false }
# Note that these dependencies are a lie, they're just here to get linkage to
# work.
@ -56,3 +57,5 @@ byteorder = { version = "1.1", features = ["i128"]}
# compiles, then please feel free to do so!
flate2 = "1.0"
tempdir = "0.3"

View File

@ -89,6 +89,7 @@ extern crate rustc_errors as errors;
extern crate syntax_pos;
extern crate jobserver;
extern crate proc_macro;
extern crate chalk_engine;
extern crate serialize as rustc_serialize; // used by deriving

View File

@ -250,10 +250,7 @@ macro_rules! BraceStructLiftImpl {
macro_rules! EnumLiftImpl {
(impl<$($p:tt),*> Lift<$tcx:tt> for $s:path {
type Lifted = $lifted:ty;
$(
($variant:path) ( $( $variant_arg:ident),* )
),*
$(,)*
$($variants:tt)*
} $(where $($wc:tt)*)*) => {
impl<$($p),*> $crate::ty::Lift<$tcx> for $s
$(where $($wc)*)*
@ -261,14 +258,44 @@ macro_rules! EnumLiftImpl {
type Lifted = $lifted;
fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<$lifted> {
match self {
$($variant ( $($variant_arg),* ) => {
Some($variant ( $(tcx.lift($variant_arg)?),* ))
})*
}
EnumLiftImpl!(@Variants(self, tcx) input($($variants)*) output())
}
}
};
(@Variants($this:expr, $tcx:expr) input() output($($output:tt)*)) => {
match $this {
$($output)*
}
};
(@Variants($this:expr, $tcx:expr)
input( ($variant:path) ( $($variant_arg:ident),* ) , $($input:tt)*)
output( $($output:tt)*) ) => {
EnumLiftImpl!(
@Variants($this, $tcx)
input($($input)*)
output(
$variant ( $($variant_arg),* ) => {
Some($variant ( $($tcx.lift($variant_arg)?),* ))
}
$($output)*
)
)
};
(@Variants($this:expr, $tcx:expr)
input( ($variant:path), $($input:tt)*)
output( $($output:tt)*) ) => {
EnumLiftImpl!(
@Variants($this, $tcx)
input($($input)*)
output(
$variant => { Some($variant) }
$($output)*
)
)
};
}
#[macro_export]

View File

@ -17,17 +17,21 @@ pub use self::FulfillmentErrorCode::*;
pub use self::Vtable::*;
pub use self::ObligationCauseCode::*;
use chalk_engine;
use hir;
use hir::def_id::DefId;
use infer::outlives::env::OutlivesEnvironment;
use middle::region;
use middle::const_val::ConstEvalErr;
use ty::subst::Substs;
use ty::{self, AdtKind, Slice, Ty, TyCtxt, GenericParamDefKind, TypeFoldable, ToPredicate};
use ty::{self, AdtKind, Slice, Ty, TyCtxt, GenericParamDefKind, ToPredicate};
use ty::error::{ExpectedFound, TypeError};
use ty::fold::{TypeFolder, TypeFoldable, TypeVisitor};
use infer::canonical::{Canonical, Canonicalize};
use infer::{InferCtxt};
use rustc_data_structures::sync::Lrc;
use std::fmt::Debug;
use std::rc::Rc;
use syntax::ast;
use syntax_pos::{Span, DUMMY_SP};
@ -1003,3 +1007,59 @@ pub fn provide(providers: &mut ty::maps::Providers) {
..*providers
};
}
impl<'gcx: 'tcx, 'tcx> Canonicalize<'gcx, 'tcx> for ty::ParamEnvAnd<'tcx, Goal<'tcx>> {
// we ought to intern this, but I'm too lazy just now
type Canonicalized = Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>;
fn intern(
_gcx: TyCtxt<'_, 'gcx, 'gcx>,
value: Canonical<'gcx, Self::Lifted>,
) -> Self::Canonicalized {
value
}
}
pub trait ExClauseFold<'tcx>
where
Self: chalk_engine::context::Context + Clone,
{
fn fold_ex_clause_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(
ex_clause: &chalk_engine::ExClause<Self>,
folder: &mut F,
) -> chalk_engine::ExClause<Self>;
fn visit_ex_clause_with<'gcx: 'tcx, V: TypeVisitor<'tcx>>(
ex_clause: &chalk_engine::ExClause<Self>,
visitor: &mut V,
) -> bool;
}
pub trait ExClauseLift<'tcx>
where
Self: chalk_engine::context::Context + Clone,
{
type LiftedExClause: Debug + 'tcx;
fn lift_ex_clause_to_tcx<'a, 'gcx>(
ex_clause: &chalk_engine::ExClause<Self>,
tcx: TyCtxt<'a, 'gcx, 'tcx>,
) -> Option<Self::LiftedExClause>;
}
impl<'gcx: 'tcx, 'tcx, C> Canonicalize<'gcx, 'tcx> for chalk_engine::ExClause<C>
where
C: chalk_engine::context::Context + Clone,
C: ExClauseLift<'gcx> + ExClauseFold<'tcx>,
C::Substitution: Clone,
C::RegionConstraint: Clone,
{
type Canonicalized = Canonical<'gcx, C::LiftedExClause>;
fn intern(
_gcx: TyCtxt<'_, 'gcx, 'gcx>,
value: Canonical<'gcx, Self::Lifted>,
) -> Self::Canonicalized {
value
}
}

View File

@ -8,11 +8,12 @@
// option. This file may not be copied, modified, or distributed
// except according to those terms.
use chalk_engine;
use rustc_data_structures::accumulate_vec::AccumulateVec;
use traits;
use traits::project::Normalized;
use ty::{self, Lift, TyCtxt};
use ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
use ty::{self, Lift, TyCtxt};
use std::fmt;
use std::rc::Rc;
@ -21,23 +22,24 @@ use std::rc::Rc;
impl<'tcx, T: fmt::Debug> fmt::Debug for Normalized<'tcx, T> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "Normalized({:?},{:?})",
self.value,
self.obligations)
write!(f, "Normalized({:?},{:?})", self.value, self.obligations)
}
}
impl<'tcx, O: fmt::Debug> fmt::Debug for traits::Obligation<'tcx, O> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
if ty::tls::with(|tcx| tcx.sess.verbose()) {
write!(f, "Obligation(predicate={:?},cause={:?},depth={})",
self.predicate,
self.cause,
self.recursion_depth)
write!(
f,
"Obligation(predicate={:?},cause={:?},depth={})",
self.predicate, self.cause, self.recursion_depth
)
} else {
write!(f, "Obligation(predicate={:?},depth={})",
self.predicate,
self.recursion_depth)
write!(
f,
"Obligation(predicate={:?},depth={})",
self.predicate, self.recursion_depth
)
}
}
}
@ -45,57 +47,52 @@ impl<'tcx, O: fmt::Debug> fmt::Debug for traits::Obligation<'tcx, O> {
impl<'tcx, N: fmt::Debug> fmt::Debug for traits::Vtable<'tcx, N> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
super::VtableImpl(ref v) =>
write!(f, "{:?}", v),
super::VtableImpl(ref v) => write!(f, "{:?}", v),
super::VtableAutoImpl(ref t) =>
write!(f, "{:?}", t),
super::VtableAutoImpl(ref t) => write!(f, "{:?}", t),
super::VtableClosure(ref d) =>
write!(f, "{:?}", d),
super::VtableClosure(ref d) => write!(f, "{:?}", d),
super::VtableGenerator(ref d) =>
write!(f, "{:?}", d),
super::VtableGenerator(ref d) => write!(f, "{:?}", d),
super::VtableFnPointer(ref d) =>
write!(f, "VtableFnPointer({:?})", d),
super::VtableFnPointer(ref d) => write!(f, "VtableFnPointer({:?})", d),
super::VtableObject(ref d) =>
write!(f, "{:?}", d),
super::VtableObject(ref d) => write!(f, "{:?}", d),
super::VtableParam(ref n) =>
write!(f, "VtableParam({:?})", n),
super::VtableParam(ref n) => write!(f, "VtableParam({:?})", n),
super::VtableBuiltin(ref d) =>
write!(f, "{:?}", d)
super::VtableBuiltin(ref d) => write!(f, "{:?}", d),
}
}
}
impl<'tcx, N: fmt::Debug> fmt::Debug for traits::VtableImplData<'tcx, N> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "VtableImpl(impl_def_id={:?}, substs={:?}, nested={:?})",
self.impl_def_id,
self.substs,
self.nested)
write!(
f,
"VtableImpl(impl_def_id={:?}, substs={:?}, nested={:?})",
self.impl_def_id, self.substs, self.nested
)
}
}
impl<'tcx, N: fmt::Debug> fmt::Debug for traits::VtableGeneratorData<'tcx, N> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "VtableGenerator(generator_def_id={:?}, substs={:?}, nested={:?})",
self.generator_def_id,
self.substs,
self.nested)
write!(
f,
"VtableGenerator(generator_def_id={:?}, substs={:?}, nested={:?})",
self.generator_def_id, self.substs, self.nested
)
}
}
impl<'tcx, N: fmt::Debug> fmt::Debug for traits::VtableClosureData<'tcx, N> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "VtableClosure(closure_def_id={:?}, substs={:?}, nested={:?})",
self.closure_def_id,
self.substs,
self.nested)
write!(
f,
"VtableClosure(closure_def_id={:?}, substs={:?}, nested={:?})",
self.closure_def_id, self.substs, self.nested
)
}
}
@ -107,34 +104,37 @@ impl<'tcx, N: fmt::Debug> fmt::Debug for traits::VtableBuiltinData<N> {
impl<'tcx, N: fmt::Debug> fmt::Debug for traits::VtableAutoImplData<N> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "VtableAutoImplData(trait_def_id={:?}, nested={:?})",
self.trait_def_id,
self.nested)
write!(
f,
"VtableAutoImplData(trait_def_id={:?}, nested={:?})",
self.trait_def_id, self.nested
)
}
}
impl<'tcx, N: fmt::Debug> fmt::Debug for traits::VtableObjectData<'tcx, N> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "VtableObject(upcast={:?}, vtable_base={}, nested={:?})",
self.upcast_trait_ref,
self.vtable_base,
self.nested)
write!(
f,
"VtableObject(upcast={:?}, vtable_base={}, nested={:?})",
self.upcast_trait_ref, self.vtable_base, self.nested
)
}
}
impl<'tcx, N: fmt::Debug> fmt::Debug for traits::VtableFnPointerData<'tcx, N> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "VtableFnPointer(fn_ty={:?}, nested={:?})",
self.fn_ty,
self.nested)
write!(
f,
"VtableFnPointer(fn_ty={:?}, nested={:?})",
self.fn_ty, self.nested
)
}
}
impl<'tcx> fmt::Debug for traits::FulfillmentError<'tcx> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "FulfillmentError({:?},{:?})",
self.obligation,
self.code)
write!(f, "FulfillmentError({:?},{:?})", self.obligation, self.code)
}
}
@ -143,9 +143,10 @@ impl<'tcx> fmt::Debug for traits::FulfillmentErrorCode<'tcx> {
match *self {
super::CodeSelectionError(ref e) => write!(f, "{:?}", e),
super::CodeProjectionError(ref e) => write!(f, "{:?}", e),
super::CodeSubtypeError(ref a, ref b) =>
write!(f, "CodeSubtypeError({:?}, {:?})", a, b),
super::CodeAmbiguity => write!(f, "Ambiguity")
super::CodeSubtypeError(ref a, ref b) => {
write!(f, "CodeSubtypeError({:?}, {:?})", a, b)
}
super::CodeAmbiguity => write!(f, "Ambiguity"),
}
}
}
@ -166,18 +167,13 @@ impl<'a, 'tcx> Lift<'tcx> for traits::SelectionError<'a> {
super::Unimplemented => Some(super::Unimplemented),
super::OutputTypeParameterMismatch(a, b, ref err) => {
tcx.lift(&(a, b)).and_then(|(a, b)| {
tcx.lift(err).map(|err| {
super::OutputTypeParameterMismatch(a, b, err)
})
tcx.lift(err)
.map(|err| super::OutputTypeParameterMismatch(a, b, err))
})
}
super::TraitNotObjectSafe(def_id) => {
Some(super::TraitNotObjectSafe(def_id))
}
super::ConstEvalFailure(ref err) => {
tcx.lift(err).map(super::ConstEvalFailure)
}
super::Overflow => bug!() // FIXME: ape ConstEvalFailure?
super::TraitNotObjectSafe(def_id) => Some(super::TraitNotObjectSafe(def_id)),
super::ConstEvalFailure(ref err) => tcx.lift(err).map(super::ConstEvalFailure),
super::Overflow => bug!(), // FIXME: ape ConstEvalFailure?
}
}
}
@ -195,16 +191,11 @@ impl<'a, 'tcx> Lift<'tcx> for traits::ObligationCauseCode<'a> {
super::ReferenceOutlivesReferent(ty) => {
tcx.lift(&ty).map(super::ReferenceOutlivesReferent)
}
super::ObjectTypeBound(ty, r) => {
tcx.lift(&ty).and_then(|ty| {
tcx.lift(&r).and_then(|r| {
Some(super::ObjectTypeBound(ty, r))
})
})
}
super::ObjectCastObligation(ty) => {
tcx.lift(&ty).map(super::ObjectCastObligation)
}
super::ObjectTypeBound(ty, r) => tcx.lift(&ty).and_then(|ty| {
tcx.lift(&r)
.and_then(|r| Some(super::ObjectTypeBound(ty, r)))
}),
super::ObjectCastObligation(ty) => tcx.lift(&ty).map(super::ObjectCastObligation),
super::AssignmentLhsSized => Some(super::AssignmentLhsSized),
super::TupleInitializerSized => Some(super::TupleInitializerSized),
super::StructInitializerSized => Some(super::StructInitializerSized),
@ -222,20 +213,20 @@ impl<'a, 'tcx> Lift<'tcx> for traits::ObligationCauseCode<'a> {
super::ImplDerivedObligation(ref cause) => {
tcx.lift(cause).map(super::ImplDerivedObligation)
}
super::CompareImplMethodObligation { item_name,
impl_item_def_id,
trait_item_def_id } => {
Some(super::CompareImplMethodObligation {
item_name,
impl_item_def_id,
trait_item_def_id,
})
}
super::CompareImplMethodObligation {
item_name,
impl_item_def_id,
trait_item_def_id,
} => Some(super::CompareImplMethodObligation {
item_name,
impl_item_def_id,
trait_item_def_id,
}),
super::ExprAssignable => Some(super::ExprAssignable),
super::MatchExpressionArm { arm_span, source } => {
Some(super::MatchExpressionArm { arm_span,
source: source })
}
super::MatchExpressionArm { arm_span, source } => Some(super::MatchExpressionArm {
arm_span,
source: source,
}),
super::IfExpression => Some(super::IfExpression),
super::IfExpressionWithNoElse => Some(super::IfExpressionWithNoElse),
super::MainFunctionType => Some(super::MainFunctionType),
@ -252,12 +243,11 @@ impl<'a, 'tcx> Lift<'tcx> for traits::DerivedObligationCause<'a> {
type Lifted = traits::DerivedObligationCause<'tcx>;
fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
tcx.lift(&self.parent_trait_ref).and_then(|trait_ref| {
tcx.lift(&*self.parent_code).map(|code| {
traits::DerivedObligationCause {
tcx.lift(&*self.parent_code)
.map(|code| traits::DerivedObligationCause {
parent_trait_ref: trait_ref,
parent_code: Rc::new(code)
}
})
parent_code: Rc::new(code),
})
})
}
}
@ -265,12 +255,10 @@ impl<'a, 'tcx> Lift<'tcx> for traits::DerivedObligationCause<'a> {
impl<'a, 'tcx> Lift<'tcx> for traits::ObligationCause<'a> {
type Lifted = traits::ObligationCause<'tcx>;
fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
tcx.lift(&self.code).map(|code| {
traits::ObligationCause {
span: self.span,
body_id: self.body_id,
code,
}
tcx.lift(&self.code).map(|code| traits::ObligationCause {
span: self.span,
body_id: self.body_id,
code,
})
}
}
@ -283,49 +271,40 @@ impl<'a, 'tcx> Lift<'tcx> for traits::Vtable<'a, ()> {
traits::VtableImpl(traits::VtableImplData {
impl_def_id,
substs,
nested
}) => {
tcx.lift(&substs).map(|substs| {
traits::VtableImpl(traits::VtableImplData {
impl_def_id,
substs,
nested,
})
nested,
}) => tcx.lift(&substs).map(|substs| {
traits::VtableImpl(traits::VtableImplData {
impl_def_id,
substs,
nested,
})
}
}),
traits::VtableAutoImpl(t) => Some(traits::VtableAutoImpl(t)),
traits::VtableGenerator(traits::VtableGeneratorData {
generator_def_id,
substs,
nested
}) => {
tcx.lift(&substs).map(|substs| {
traits::VtableGenerator(traits::VtableGeneratorData {
generator_def_id: generator_def_id,
substs: substs,
nested: nested
})
nested,
}) => tcx.lift(&substs).map(|substs| {
traits::VtableGenerator(traits::VtableGeneratorData {
generator_def_id: generator_def_id,
substs: substs,
nested: nested,
})
}
}),
traits::VtableClosure(traits::VtableClosureData {
closure_def_id,
substs,
nested
}) => {
tcx.lift(&substs).map(|substs| {
traits::VtableClosure(traits::VtableClosureData {
closure_def_id,
substs,
nested,
})
nested,
}) => tcx.lift(&substs).map(|substs| {
traits::VtableClosure(traits::VtableClosureData {
closure_def_id,
substs,
nested,
})
}
}),
traits::VtableFnPointer(traits::VtableFnPointerData { fn_ty, nested }) => {
tcx.lift(&fn_ty).map(|fn_ty| {
traits::VtableFnPointer(traits::VtableFnPointerData {
fn_ty,
nested,
})
traits::VtableFnPointer(traits::VtableFnPointerData { fn_ty, nested })
})
}
traits::VtableParam(n) => Some(traits::VtableParam(n)),
@ -333,16 +312,14 @@ impl<'a, 'tcx> Lift<'tcx> for traits::Vtable<'a, ()> {
traits::VtableObject(traits::VtableObjectData {
upcast_trait_ref,
vtable_base,
nested
}) => {
tcx.lift(&upcast_trait_ref).map(|trait_ref| {
traits::VtableObject(traits::VtableObjectData {
upcast_trait_ref: trait_ref,
vtable_base,
nested,
})
nested,
}) => tcx.lift(&upcast_trait_ref).map(|trait_ref| {
traits::VtableObject(traits::VtableObjectData {
upcast_trait_ref: trait_ref,
vtable_base,
nested,
})
}
}),
}
}
}
@ -350,8 +327,7 @@ impl<'a, 'tcx> Lift<'tcx> for traits::Vtable<'a, ()> {
///////////////////////////////////////////////////////////////////////////
// TypeFoldable implementations.
impl<'tcx, O: TypeFoldable<'tcx>> TypeFoldable<'tcx> for traits::Obligation<'tcx, O>
{
impl<'tcx, O: TypeFoldable<'tcx>> TypeFoldable<'tcx> for traits::Obligation<'tcx, O> {
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
traits::Obligation {
cause: self.cause.clone(),
@ -536,6 +512,14 @@ EnumTypeFoldableImpl! {
}
}
EnumLiftImpl! {
impl<'a, 'tcx> Lift<'tcx> for traits::WhereClauseAtom<'a> {
type Lifted = traits::WhereClauseAtom<'tcx>;
(traits::WhereClauseAtom::Implemented)(trait_ref),
(traits::WhereClauseAtom::ProjectionEq)(projection),
}
}
EnumTypeFoldableImpl! {
impl<'tcx> TypeFoldable<'tcx> for traits::DomainGoal<'tcx> {
(traits::DomainGoal::Holds)(wc),
@ -549,7 +533,21 @@ EnumTypeFoldableImpl! {
}
}
CloneTypeFoldableImpls! {
EnumLiftImpl! {
impl<'a, 'tcx> Lift<'tcx> for traits::DomainGoal<'a> {
type Lifted = traits::DomainGoal<'tcx>;
(traits::DomainGoal::Holds)(wc),
(traits::DomainGoal::WellFormed)(wc),
(traits::DomainGoal::FromEnv)(wc),
(traits::DomainGoal::WellFormedTy)(ty),
(traits::DomainGoal::Normalize)(projection),
(traits::DomainGoal::FromEnvTy)(ty),
(traits::DomainGoal::RegionOutlives)(predicate),
(traits::DomainGoal::TypeOutlives)(predicate),
}
}
CloneTypeFoldableAndLiftImpls! {
traits::QuantifierKind,
}
@ -564,9 +562,23 @@ EnumTypeFoldableImpl! {
}
}
EnumLiftImpl! {
impl<'a, 'tcx> Lift<'tcx> for traits::Goal<'a> {
type Lifted = traits::Goal<'tcx>;
(traits::Goal::Implies)(hypotheses, goal),
(traits::Goal::And)(goal1, goal2),
(traits::Goal::Not)(goal),
(traits::Goal::DomainGoal)(domain_goal),
(traits::Goal::Quantified)(kind, goal),
(traits::Goal::CannotProve),
}
}
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]>>();
let v = self.iter()
.map(|t| t.fold_with(folder))
.collect::<AccumulateVec<[_; 8]>>();
folder.tcx().intern_goals(&v)
}
@ -602,7 +614,9 @@ EnumTypeFoldableImpl! {
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]>>();
let v = self.iter()
.map(|t| t.fold_with(folder))
.collect::<AccumulateVec<[_; 8]>>();
folder.tcx().intern_clauses(&v)
}
@ -610,3 +624,59 @@ impl<'tcx> TypeFoldable<'tcx> for &'tcx ty::Slice<traits::Clause<'tcx>> {
self.iter().any(|t| t.visit_with(visitor))
}
}
impl<'tcx, C> TypeFoldable<'tcx> for chalk_engine::ExClause<C>
where
C: traits::ExClauseFold<'tcx>,
C::Substitution: Clone,
C::RegionConstraint: Clone,
{
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
<C as traits::ExClauseFold>::fold_ex_clause_with(
self,
folder,
)
}
fn super_visit_with<V: TypeVisitor<'tcx>>(&self, visitor: &mut V) -> bool {
<C as traits::ExClauseFold>::visit_ex_clause_with(
self,
visitor,
)
}
}
impl<'tcx, C> Lift<'tcx> for chalk_engine::ExClause<C>
where
C: chalk_engine::context::Context + Clone,
C: traits::ExClauseLift<'tcx>,
{
type Lifted = C::LiftedExClause;
fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
<C as traits::ExClauseLift>::lift_ex_clause_to_tcx(self, tcx)
}
}
EnumTypeFoldableImpl! {
impl<'tcx, C> TypeFoldable<'tcx> for chalk_engine::DelayedLiteral<C> {
(chalk_engine::DelayedLiteral::CannotProve)(a),
(chalk_engine::DelayedLiteral::Negative)(a),
(chalk_engine::DelayedLiteral::Positive)(a, b),
} where
C: chalk_engine::context::Context + Clone,
C::CanonicalConstrainedSubst: TypeFoldable<'tcx>,
}
EnumTypeFoldableImpl! {
impl<'tcx, C> TypeFoldable<'tcx> for chalk_engine::Literal<C> {
(chalk_engine::Literal::Negative)(a),
(chalk_engine::Literal::Positive)(a),
} where
C: chalk_engine::context::Context + Clone,
C::GoalInEnvironment: Clone + TypeFoldable<'tcx>,
}
CloneTypeFoldableAndLiftImpls! {
chalk_engine::TableIndex,
}

View File

@ -1512,6 +1512,51 @@ impl<'a, 'tcx> Lift<'tcx> for Region<'a> {
}
}
impl<'a, 'tcx> Lift<'tcx> for &'a Goal<'a> {
type Lifted = &'tcx Goal<'tcx>;
fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<&'tcx Goal<'tcx>> {
if tcx.interners.arena.in_arena(*self as *const _) {
return Some(unsafe { mem::transmute(*self) });
}
// Also try in the global tcx if we're not that.
if !tcx.is_global() {
self.lift_to_tcx(tcx.global_tcx())
} else {
None
}
}
}
impl<'a, 'tcx> Lift<'tcx> for &'a Slice<Goal<'a>> {
type Lifted = &'tcx Slice<Goal<'tcx>>;
fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<&'tcx Slice<Goal<'tcx>>> {
if tcx.interners.arena.in_arena(*self as *const _) {
return Some(unsafe { mem::transmute(*self) });
}
// Also try in the global tcx if we're not that.
if !tcx.is_global() {
self.lift_to_tcx(tcx.global_tcx())
} else {
None
}
}
}
impl<'a, 'tcx> Lift<'tcx> for &'a Slice<Clause<'a>> {
type Lifted = &'tcx Slice<Clause<'tcx>>;
fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<&'tcx Slice<Clause<'tcx>>> {
if tcx.interners.arena.in_arena(*self as *const _) {
return Some(unsafe { mem::transmute(*self) });
}
// Also try in the global tcx if we're not that.
if !tcx.is_global() {
self.lift_to_tcx(tcx.global_tcx())
} else {
None
}
}
}
impl<'a, 'tcx> Lift<'tcx> for &'a Const<'a> {
type Lifted = &'tcx Const<'tcx>;
fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<&'tcx Const<'tcx>> {

View File

@ -16,3 +16,4 @@ rustc = { path = "../librustc" }
rustc_data_structures = { path = "../librustc_data_structures" }
syntax = { path = "../libsyntax" }
syntax_pos = { path = "../libsyntax_pos" }
chalk-engine = { version = "0.6.0", default-features=false }

View File

@ -0,0 +1,514 @@
use chalk_engine::fallible::Fallible as ChalkEngineFallible;
use chalk_engine::{context, hh::HhGoal, DelayedLiteral, ExClause};
use rustc::infer::canonical::{
Canonical, CanonicalVarValues, Canonicalize, QueryRegionConstraint, QueryResult,
};
use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime};
use rustc::traits::{DomainGoal, ExClauseFold, ExClauseLift, Goal, ProgramClause, QuantifierKind};
use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
use rustc::ty::subst::Kind;
use rustc::ty::{self, TyCtxt};
use std::fmt::{self, Debug};
use std::marker::PhantomData;
use syntax_pos::DUMMY_SP;
#[derive(Copy, Clone, Debug)]
crate struct ChalkArenas<'gcx> {
_phantom: PhantomData<&'gcx ()>,
}
#[derive(Copy, Clone)]
crate struct ChalkContext<'cx, 'gcx: 'cx> {
_arenas: ChalkArenas<'gcx>,
_tcx: TyCtxt<'cx, 'gcx, 'gcx>,
}
#[derive(Copy, Clone)]
crate struct ChalkInferenceContext<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
}
#[derive(Copy, Clone, Debug)]
crate struct UniverseMap;
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
crate struct ConstrainedSubst<'tcx> {
subst: CanonicalVarValues<'tcx>,
constraints: Vec<QueryRegionConstraint<'tcx>>,
}
BraceStructTypeFoldableImpl! {
impl<'tcx> TypeFoldable<'tcx> for ConstrainedSubst<'tcx> {
subst, constraints
}
}
impl context::Context for ChalkArenas<'tcx> {
type CanonicalExClause = Canonical<'tcx, ExClause<Self>>;
type CanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
// u-canonicalization not yet implemented
type UCanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
type CanonicalConstrainedSubst = Canonical<'tcx, ConstrainedSubst<'tcx>>;
// u-canonicalization not yet implemented
type UniverseMap = UniverseMap;
type Solution = Canonical<'tcx, QueryResult<'tcx, ()>>;
type InferenceNormalizedSubst = CanonicalVarValues<'tcx>;
type GoalInEnvironment = ty::ParamEnvAnd<'tcx, Goal<'tcx>>;
type RegionConstraint = QueryRegionConstraint<'tcx>;
type Substitution = CanonicalVarValues<'tcx>;
type Environment = ty::ParamEnv<'tcx>;
type Goal = Goal<'tcx>;
type DomainGoal = DomainGoal<'tcx>;
type BindersGoal = ty::Binder<&'tcx Goal<'tcx>>;
type Parameter = Kind<'tcx>;
type ProgramClause = ProgramClause<'tcx>;
type ProgramClauses = Vec<ProgramClause<'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(
env: &ty::ParamEnv<'tcx>,
goal: Goal<'tcx>,
) -> ty::ParamEnvAnd<'tcx, Goal<'tcx>> {
env.and(goal)
}
}
impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
fn make_solution(
&self,
_root_goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
_simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
) -> Option<Canonical<'gcx, QueryResult<'gcx, ()>>> {
unimplemented!()
}
}
impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
/// True if this is a coinductive goal -- e.g., proving an auto trait.
fn is_coinductive(&self, _goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> bool {
unimplemented!()
}
/// Create an inference table for processing a new goal and instantiate that goal
/// in that context, returning "all the pieces".
///
/// More specifically: given a u-canonical goal `arg`, creates a
/// new inference table `T` and populates it with the universes
/// found in `arg`. Then, creates a substitution `S` that maps
/// each bound variable in `arg` to a fresh inference variable
/// from T. Returns:
///
/// - the table `T`
/// - the substitution `S`
/// - the environment and goal found by substitution `S` into `arg`
fn instantiate_ucanonical_goal<R>(
&self,
_arg: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
_op: impl context::WithInstantiatedUCanonicalGoal<ChalkArenas<'gcx>, Output = R>,
) -> R {
unimplemented!()
}
fn instantiate_ex_clause<R>(
&self,
_num_universes: usize,
_canonical_ex_clause: &Canonical<'gcx, ChalkExClause<'gcx>>,
_op: impl context::WithInstantiatedExClause<ChalkArenas<'gcx>, Output = R>,
) -> R {
unimplemented!()
}
/// True if this solution has no region constraints.
fn empty_constraints(ccs: &Canonical<'gcx, ConstrainedSubst<'gcx>>) -> bool {
ccs.value.constraints.is_empty()
}
fn inference_normalized_subst_from_ex_clause(
canon_ex_clause: &'a Canonical<'gcx, ChalkExClause<'gcx>>,
) -> &'a CanonicalVarValues<'gcx> {
&canon_ex_clause.value.subst
}
fn inference_normalized_subst_from_subst(
canon_subst: &'a Canonical<'gcx, ConstrainedSubst<'gcx>>,
) -> &'a CanonicalVarValues<'gcx> {
&canon_subst.value.subst
}
fn canonical(
u_canon: &'a Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
) -> &'a Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
u_canon
}
fn is_trivial_substitution(
_u_canon: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
_canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
) -> bool {
unimplemented!()
}
fn num_universes(_: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> usize {
0 // FIXME
}
/// Convert a goal G *from* the canonical universes *into* our
/// local universes. This will yield a goal G' that is the same
/// but for the universes of universally quantified names.
fn map_goal_from_canonical(
_map: &UniverseMap,
value: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
) -> Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
*value // FIXME universe maps not implemented yet
}
fn map_subst_from_canonical(
_map: &UniverseMap,
value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
value.clone() // FIXME universe maps not implemented yet
}
}
//impl context::UCanonicalGoalInEnvironment<ChalkContext<'cx, 'gcx>>
// for Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>
//{
// fn canonical(&self) -> &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
// self
// }
//
// fn is_trivial_substitution(
// &self,
// canonical_subst: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
// ) -> bool {
// let subst = &canonical_subst.value.subst;
// assert_eq!(self.canonical.variables.len(), subst.var_values.len());
// subst
// .var_values
// .iter_enumerated()
// .all(|(cvar, kind)| match kind.unpack() {
// Kind::Lifetime(r) => match r {
// ty::ReCanonical(cvar1) => cvar == cvar1,
// _ => false,
// },
// Kind::Type(ty) => match ty.sty {
// ty::TyInfer(ty::InferTy::CanonicalTy(cvar1)) => cvar == cvar1,
// _ => false,
// },
// })
// }
//
// fn num_universes(&self) -> usize {
// 0 // FIXME
// }
//}
impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
for ChalkInferenceContext<'cx, 'gcx, 'tcx>
{
fn into_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
match goal {
Goal::Implies(..) => panic!("FIXME rust-lang-nursery/chalk#94"),
Goal::And(left, right) => HhGoal::And(*left, *right),
Goal::Not(subgoal) => HhGoal::Not(*subgoal),
Goal::DomainGoal(d) => HhGoal::DomainGoal(d),
Goal::Quantified(QuantifierKind::Universal, binder) => HhGoal::ForAll(binder),
Goal::Quantified(QuantifierKind::Existential, binder) => HhGoal::Exists(binder),
Goal::CannotProve => HhGoal::CannotProve,
}
}
fn add_clauses(
&mut self,
_env: &ty::ParamEnv<'tcx>,
_clauses: Vec<ProgramClause<'tcx>>,
) -> ty::ParamEnv<'tcx> {
panic!("FIXME no method to add clauses to ParamEnv yet")
}
}
impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
for ChalkInferenceContext<'cx, 'gcx, 'tcx>
{
fn resolvent_clause(
&mut self,
_environment: &ty::ParamEnv<'tcx>,
_goal: &DomainGoal<'tcx>,
_subst: &CanonicalVarValues<'tcx>,
_clause: &ProgramClause<'tcx>,
) -> chalk_engine::fallible::Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
panic!()
}
fn apply_answer_subst(
&mut self,
_ex_clause: ChalkExClause<'tcx>,
_selected_goal: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
_answer_table_goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
_canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
) -> chalk_engine::fallible::Fallible<ChalkExClause<'tcx>> {
panic!()
}
}
impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
for ChalkInferenceContext<'cx, 'gcx, 'tcx>
{
fn truncate_goal(
&mut self,
subgoal: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
Some(*subgoal) // FIXME we should truncate at some point!
}
fn truncate_answer(
&mut self,
subst: &CanonicalVarValues<'tcx>,
) -> Option<CanonicalVarValues<'tcx>> {
Some(subst.clone()) // FIXME we should truncate at some point!
}
}
impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
for ChalkInferenceContext<'cx, 'gcx, 'tcx>
{
fn program_clauses(
&self,
_environment: &ty::ParamEnv<'tcx>,
goal: &DomainGoal<'tcx>,
) -> Vec<ProgramClause<'tcx>> {
use rustc::traits::DomainGoal::*;
use rustc::traits::WhereClauseAtom::*;
match goal {
Holds(Implemented(_trait_predicate)) => {
// These come from:
//
// - Trait definitions (implied bounds)
// - Implementations of the trait itself
panic!()
}
Holds(ProjectionEq(_projection_predicate)) => {
// These come from:
panic!()
}
WellFormed(Implemented(_trait_predicate)) => {
// These come from -- the trait decl.
panic!()
}
WellFormed(ProjectionEq(_projection_predicate)) => panic!(),
FromEnv(Implemented(_trait_predicate)) => panic!(),
FromEnv(ProjectionEq(_projection_predicate)) => panic!(),
WellFormedTy(_ty) => panic!(),
FromEnvTy(_ty) => panic!(),
RegionOutlives(_region_outlives) => panic!(),
TypeOutlives(_type_outlives) => panic!(),
Normalize(_) => panic!(),
}
}
fn instantiate_binders_universally(
&mut self,
_arg: &ty::Binder<&'tcx Goal<'tcx>>,
) -> Goal<'tcx> {
panic!("FIXME -- universal instantiation needs sgrif's branch")
}
fn instantiate_binders_existentially(
&mut self,
arg: &ty::Binder<&'tcx Goal<'tcx>>,
) -> Goal<'tcx> {
let (value, _map) = self.infcx.replace_late_bound_regions_with_fresh_var(
DUMMY_SP,
LateBoundRegionConversionTime::HigherRankedType,
arg,
);
*value
}
fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
let string = format!("{:?}", self.infcx.resolve_type_vars_if_possible(value));
Box::new(string)
}
fn canonicalize_goal(
&mut self,
value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
) -> Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
self.infcx.canonicalize_query(value).0
}
fn canonicalize_ex_clause(
&mut self,
value: &ChalkExClause<'tcx>,
) -> Canonical<'gcx, ChalkExClause<'gcx>> {
self.infcx.canonicalize_response(value).0
}
fn canonicalize_constrained_subst(
&mut self,
subst: CanonicalVarValues<'tcx>,
constraints: Vec<QueryRegionConstraint<'tcx>>,
) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
self.infcx
.canonicalize_response(&ConstrainedSubst { subst, constraints })
.0
}
fn u_canonicalize_goal(
&mut self,
value: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
) -> (
Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
UniverseMap,
) {
(value.clone(), UniverseMap)
}
fn invert_goal(
&mut self,
_value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
panic!("goal inversion not yet implemented")
}
fn unify_parameters(
&mut self,
_environment: &ty::ParamEnv<'tcx>,
_a: &Kind<'tcx>,
_b: &Kind<'tcx>,
) -> ChalkEngineFallible<InferOk<'tcx, ()>> {
panic!()
}
fn sink_answer_subset(
&self,
value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
value.clone()
}
fn lift_delayed_literal(
&self,
_value: DelayedLiteral<ChalkArenas<'tcx>>,
) -> DelayedLiteral<ChalkArenas<'gcx>> {
panic!("lift")
}
fn into_ex_clause(&mut self, _result: InferOk<'tcx, ()>, _ex_clause: &mut ChalkExClause<'tcx>) {
panic!("TBD")
}
}
type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
type ChalkExClause<'tcx> = ExClause<ChalkArenas<'tcx>>;
impl Debug for ChalkContext<'cx, 'gcx> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "ChalkContext")
}
}
impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "ChalkInferenceContext")
}
}
impl ExClauseLift<'gcx> for ChalkArenas<'a> {
type LiftedExClause = ChalkExClause<'gcx>;
fn lift_ex_clause_to_tcx(
_ex_clause: &ChalkExClause<'a>,
_tcx: TyCtxt<'_, '_, 'tcx>,
) -> Option<Self::LiftedExClause> {
panic!()
}
}
impl ExClauseFold<'tcx> for ChalkArenas<'tcx> {
fn fold_ex_clause_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(
ex_clause: &ChalkExClause<'tcx>,
folder: &mut F,
) -> ChalkExClause<'tcx> {
ExClause {
subst: ex_clause.subst.fold_with(folder),
delayed_literals: ex_clause.delayed_literals.fold_with(folder),
constraints: ex_clause.constraints.fold_with(folder),
subgoals: ex_clause.subgoals.fold_with(folder),
}
}
fn visit_ex_clause_with<'gcx: 'tcx, V: TypeVisitor<'tcx>>(
ex_clause: &ExClause<Self>,
visitor: &mut V,
) -> bool {
let ExClause {
subst,
delayed_literals,
constraints,
subgoals,
} = ex_clause;
subst.visit_with(visitor)
&& delayed_literals.visit_with(visitor)
&& constraints.visit_with(visitor)
&& subgoals.visit_with(visitor)
}
}
BraceStructLiftImpl! {
impl<'a, 'tcx> Lift<'tcx> for ConstrainedSubst<'a> {
type Lifted = ConstrainedSubst<'tcx>;
subst, constraints
}
}
impl<'gcx: 'tcx, 'tcx> Canonicalize<'gcx, 'tcx> for ConstrainedSubst<'tcx> {
type Canonicalized = Canonical<'gcx, ConstrainedSubst<'gcx>>;
fn intern(
_gcx: TyCtxt<'_, 'gcx, 'gcx>,
value: Canonical<'gcx, ConstrainedSubst<'gcx>>,
) -> Self::Canonicalized {
value
}
}

View File

@ -11,9 +11,13 @@
//! New recursive solver modeled on Chalk's recursive solver. Most of
//! the guts are broken up into modules; see the comments in those modules.
#![feature(crate_in_paths)]
#![feature(crate_visibility_modifier)]
#![feature(extern_prelude)]
#![feature(iterator_find_map)]
#![feature(in_band_lifetimes)]
extern crate chalk_engine;
#[macro_use]
extern crate log;
#[macro_use]
@ -22,6 +26,7 @@ extern crate rustc_data_structures;
extern crate syntax;
extern crate syntax_pos;
mod chalk_context;
mod dropck_outlives;
mod evaluate_obligation;
mod normalize_projection_ty;

View File

@ -22,7 +22,7 @@ use syntax::ast;
use std::iter;
trait Lower<T> {
crate trait Lower<T> {
/// Lower a rustc construction (e.g. `ty::TraitPredicate`) to a chalk-like type.
fn lower(&self) -> T;
}