Integrate chalk engine
This commit is contained in:
parent
ea4187a842
commit
ba6314a0d6
@ -648,6 +648,7 @@ define_dep_nodes!( <'tcx>
|
||||
[] ImpliedOutlivesBounds(CanonicalTyGoal<'tcx>),
|
||||
[] DropckOutlives(CanonicalTyGoal<'tcx>),
|
||||
[] EvaluateObligation(CanonicalPredicateGoal<'tcx>),
|
||||
[] EvaluateGoal(traits::ChalkCanonicalGoal<'tcx>),
|
||||
[] TypeOpAscribeUserType(CanonicalTypeOpAscribeUserTypeGoal<'tcx>),
|
||||
[] TypeOpEq(CanonicalTypeOpEqGoal<'tcx>),
|
||||
[] TypeOpSubtype(CanonicalTypeOpSubtypeGoal<'tcx>),
|
||||
|
@ -1240,3 +1240,10 @@ impl_stable_hash_for!(
|
||||
clauses,
|
||||
}
|
||||
);
|
||||
|
||||
impl_stable_hash_for!(
|
||||
impl<'tcx, G> for struct traits::InEnvironment<'tcx, G> {
|
||||
environment,
|
||||
goal,
|
||||
}
|
||||
);
|
||||
|
@ -330,9 +330,13 @@ impl<'cx, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Canonicalizer<'cx, 'gcx, 'tcx>
|
||||
fn fold_ty(&mut self, t: Ty<'tcx>) -> Ty<'tcx> {
|
||||
match t.sty {
|
||||
ty::Infer(ty::TyVar(vid)) => {
|
||||
debug!("canonical: type var found with vid {:?}", vid);
|
||||
match self.infcx.unwrap().probe_ty_var(vid) {
|
||||
// `t` could be a float / int variable: canonicalize that instead
|
||||
Ok(t) => self.fold_ty(t),
|
||||
Ok(t) => {
|
||||
debug!("(resolved to {:?})", t);
|
||||
self.fold_ty(t)
|
||||
}
|
||||
|
||||
// `TyVar(vid)` is unresolved, track its universe index in the canonicalized
|
||||
// result
|
||||
@ -448,7 +452,12 @@ impl<'cx, 'gcx, 'tcx> Canonicalizer<'cx, 'gcx, 'tcx> {
|
||||
|
||||
// Fast path: nothing that needs to be canonicalized.
|
||||
if !value.has_type_flags(needs_canonical_flags) {
|
||||
let out_value = gcx.lift(value).unwrap();
|
||||
let out_value = gcx.lift(value).unwrap_or_else(|| {
|
||||
bug!(
|
||||
"failed to lift `{:?}` (nothing to canonicalize)",
|
||||
value
|
||||
)
|
||||
});
|
||||
let canon_value = Canonical {
|
||||
max_universe: ty::UniverseIndex::ROOT,
|
||||
variables: List::empty(),
|
||||
|
@ -420,9 +420,33 @@ BraceStructLiftImpl! {
|
||||
}
|
||||
|
||||
impl<'tcx> CanonicalVarValues<'tcx> {
|
||||
fn len(&self) -> usize {
|
||||
pub fn len(&self) -> usize {
|
||||
self.var_values.len()
|
||||
}
|
||||
|
||||
/// Make an identity substitution from this one: each bound var
|
||||
/// is matched to the same bound var, preserving the original kinds.
|
||||
/// For example, if we have:
|
||||
/// `self.var_values == [Type(u32), Lifetime('a), Type(u64)]`
|
||||
/// we'll return a substitution `subst` with:
|
||||
/// `subst.var_values == [Type(^0), Lifetime(^1), Type(^2)]`.
|
||||
pub fn make_identity<'a>(&self, tcx: TyCtxt<'a, 'tcx, 'tcx>) -> Self {
|
||||
use ty::subst::UnpackedKind;
|
||||
|
||||
CanonicalVarValues {
|
||||
var_values: self.var_values.iter()
|
||||
.zip(0..)
|
||||
.map(|(kind, i)| match kind.unpack() {
|
||||
UnpackedKind::Type(..) => tcx.mk_ty(
|
||||
ty::Bound(ty::INNERMOST, ty::BoundVar::from_u32(i).into())
|
||||
).into(),
|
||||
UnpackedKind::Lifetime(..) => tcx.mk_region(
|
||||
ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(i))
|
||||
).into(),
|
||||
})
|
||||
.collect()
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, 'tcx> IntoIterator for &'a CanonicalVarValues<'tcx> {
|
||||
|
165
src/librustc/traits/chalk_fulfill.rs
Normal file
165
src/librustc/traits/chalk_fulfill.rs
Normal file
@ -0,0 +1,165 @@
|
||||
use traits::{
|
||||
Environment,
|
||||
InEnvironment,
|
||||
TraitEngine,
|
||||
ObligationCause,
|
||||
PredicateObligation,
|
||||
FulfillmentError,
|
||||
FulfillmentErrorCode,
|
||||
SelectionError,
|
||||
};
|
||||
use traits::query::NoSolution;
|
||||
use infer::InferCtxt;
|
||||
use infer::canonical::{Canonical, OriginalQueryValues};
|
||||
use ty::{self, Ty};
|
||||
use rustc_data_structures::fx::FxHashSet;
|
||||
|
||||
pub type CanonicalGoal<'tcx> = Canonical<'tcx, InEnvironment<'tcx, ty::Predicate<'tcx>>>;
|
||||
|
||||
pub struct FulfillmentContext<'tcx> {
|
||||
obligations: FxHashSet<InEnvironment<'tcx, PredicateObligation<'tcx>>>,
|
||||
}
|
||||
|
||||
impl FulfillmentContext<'tcx> {
|
||||
crate fn new() -> Self {
|
||||
FulfillmentContext {
|
||||
obligations: FxHashSet::default(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn in_environment(
|
||||
infcx: &InferCtxt<'_, 'gcx, 'tcx>,
|
||||
obligation: PredicateObligation<'tcx>
|
||||
) -> InEnvironment<'tcx, PredicateObligation<'tcx>> {
|
||||
assert!(!infcx.is_in_snapshot());
|
||||
let obligation = infcx.resolve_type_vars_if_possible(&obligation);
|
||||
|
||||
let environment = match obligation.param_env.def_id {
|
||||
Some(def_id) => infcx.tcx.environment(def_id),
|
||||
None if obligation.param_env.caller_bounds.is_empty() => Environment {
|
||||
clauses: ty::List::empty(),
|
||||
},
|
||||
_ => bug!("non-empty `ParamEnv` with no def-id"),
|
||||
};
|
||||
|
||||
InEnvironment {
|
||||
environment,
|
||||
goal: obligation,
|
||||
}
|
||||
}
|
||||
|
||||
impl TraitEngine<'tcx> for FulfillmentContext<'tcx> {
|
||||
fn normalize_projection_type(
|
||||
&mut self,
|
||||
infcx: &InferCtxt<'_, 'gcx, 'tcx>,
|
||||
_param_env: ty::ParamEnv<'tcx>,
|
||||
projection_ty: ty::ProjectionTy<'tcx>,
|
||||
_cause: ObligationCause<'tcx>,
|
||||
) -> Ty<'tcx> {
|
||||
infcx.tcx.mk_ty(ty::Projection(projection_ty))
|
||||
}
|
||||
|
||||
fn register_predicate_obligation(
|
||||
&mut self,
|
||||
infcx: &InferCtxt<'_, 'gcx, 'tcx>,
|
||||
obligation: PredicateObligation<'tcx>,
|
||||
) {
|
||||
self.obligations.insert(in_environment(infcx, obligation));
|
||||
}
|
||||
|
||||
fn select_all_or_error(
|
||||
&mut self,
|
||||
infcx: &InferCtxt<'_, 'gcx, 'tcx>,
|
||||
) -> Result<(), Vec<FulfillmentError<'tcx>>> {
|
||||
self.select_where_possible(infcx)?;
|
||||
|
||||
if self.obligations.is_empty() {
|
||||
Ok(())
|
||||
} else {
|
||||
let errors = self.obligations.iter()
|
||||
.map(|obligation| FulfillmentError {
|
||||
obligation: obligation.goal.clone(),
|
||||
code: FulfillmentErrorCode::CodeAmbiguity,
|
||||
})
|
||||
.collect();
|
||||
Err(errors)
|
||||
}
|
||||
}
|
||||
|
||||
fn select_where_possible(
|
||||
&mut self,
|
||||
infcx: &InferCtxt<'_, 'gcx, 'tcx>,
|
||||
) -> Result<(), Vec<FulfillmentError<'tcx>>> {
|
||||
let mut errors = Vec::new();
|
||||
let mut next_round = FxHashSet::default();
|
||||
let mut making_progress;
|
||||
|
||||
loop {
|
||||
making_progress = false;
|
||||
|
||||
// We iterate over all obligations, and record if we are able
|
||||
// to unambiguously prove at least one obligation.
|
||||
for obligation in self.obligations.drain() {
|
||||
let mut orig_values = OriginalQueryValues::default();
|
||||
let canonical_goal = infcx.canonicalize_query(&InEnvironment {
|
||||
environment: obligation.environment,
|
||||
goal: obligation.goal.predicate,
|
||||
}, &mut orig_values);
|
||||
|
||||
match infcx.tcx.global_tcx().evaluate_goal(canonical_goal) {
|
||||
Ok(response) => {
|
||||
if response.is_proven() {
|
||||
making_progress = true;
|
||||
|
||||
match infcx.instantiate_query_response_and_region_obligations(
|
||||
&obligation.goal.cause,
|
||||
obligation.goal.param_env,
|
||||
&orig_values,
|
||||
&response
|
||||
) {
|
||||
Ok(infer_ok) => next_round.extend(
|
||||
infer_ok.obligations
|
||||
.into_iter()
|
||||
.map(|obligation| in_environment(infcx, obligation))
|
||||
),
|
||||
|
||||
Err(_err) => errors.push(FulfillmentError {
|
||||
obligation: obligation.goal,
|
||||
code: FulfillmentErrorCode::CodeSelectionError(
|
||||
SelectionError::Unimplemented
|
||||
),
|
||||
}),
|
||||
}
|
||||
} else {
|
||||
// Ambiguous: retry at next round.
|
||||
next_round.insert(obligation);
|
||||
}
|
||||
}
|
||||
|
||||
Err(NoSolution) => errors.push(FulfillmentError {
|
||||
obligation: obligation.goal,
|
||||
code: FulfillmentErrorCode::CodeSelectionError(
|
||||
SelectionError::Unimplemented
|
||||
),
|
||||
})
|
||||
}
|
||||
}
|
||||
next_round = std::mem::replace(&mut self.obligations, next_round);
|
||||
|
||||
if !making_progress {
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if errors.is_empty() {
|
||||
Ok(())
|
||||
} else {
|
||||
Err(errors)
|
||||
}
|
||||
}
|
||||
|
||||
fn pending_obligations(&self) -> Vec<PredicateObligation<'tcx>> {
|
||||
self.obligations.iter().map(|obligation| obligation.goal.clone()).collect()
|
||||
}
|
||||
}
|
@ -1,8 +1,9 @@
|
||||
use infer::InferCtxt;
|
||||
use ty::{self, Ty, TyCtxt};
|
||||
use ty::{self, Ty, TyCtxt, ToPredicate};
|
||||
use traits::Obligation;
|
||||
use hir::def_id::DefId;
|
||||
|
||||
use super::{FulfillmentContext, FulfillmentError};
|
||||
use super::{ChalkFulfillmentContext, FulfillmentContext, FulfillmentError};
|
||||
use super::{ObligationCause, PredicateObligation};
|
||||
|
||||
pub trait TraitEngine<'tcx>: 'tcx {
|
||||
@ -14,6 +15,9 @@ pub trait TraitEngine<'tcx>: 'tcx {
|
||||
cause: ObligationCause<'tcx>,
|
||||
) -> Ty<'tcx>;
|
||||
|
||||
/// Requires that `ty` must implement the trait with `def_id` in
|
||||
/// the given environment. This trait must not have any type
|
||||
/// parameters (except for `Self`).
|
||||
fn register_bound(
|
||||
&mut self,
|
||||
infcx: &InferCtxt<'_, 'gcx, 'tcx>,
|
||||
@ -21,7 +25,18 @@ pub trait TraitEngine<'tcx>: 'tcx {
|
||||
ty: Ty<'tcx>,
|
||||
def_id: DefId,
|
||||
cause: ObligationCause<'tcx>,
|
||||
);
|
||||
) {
|
||||
let trait_ref = ty::TraitRef {
|
||||
def_id,
|
||||
substs: infcx.tcx.mk_substs_trait(ty, &[]),
|
||||
};
|
||||
self.register_predicate_obligation(infcx, Obligation {
|
||||
cause,
|
||||
recursion_depth: 0,
|
||||
param_env,
|
||||
predicate: trait_ref.to_predicate()
|
||||
});
|
||||
}
|
||||
|
||||
fn register_predicate_obligation(
|
||||
&mut self,
|
||||
@ -63,7 +78,11 @@ impl<T: ?Sized + TraitEngine<'tcx>> TraitEngineExt<'tcx> for T {
|
||||
}
|
||||
|
||||
impl dyn TraitEngine<'tcx> {
|
||||
pub fn new(_tcx: TyCtxt<'_, '_, 'tcx>) -> Box<Self> {
|
||||
Box::new(FulfillmentContext::new())
|
||||
pub fn new(tcx: TyCtxt<'_, '_, 'tcx>) -> Box<Self> {
|
||||
if tcx.sess.opts.debugging_opts.chalk {
|
||||
Box::new(ChalkFulfillmentContext::new())
|
||||
} else {
|
||||
Box::new(FulfillmentContext::new())
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -796,12 +796,21 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
|
||||
}
|
||||
|
||||
ty::Predicate::WellFormed(ty) => {
|
||||
// WF predicates cannot themselves make
|
||||
// errors. They can only block due to
|
||||
// ambiguity; otherwise, they always
|
||||
// degenerate into other obligations
|
||||
// (which may fail).
|
||||
span_bug!(span, "WF predicate not satisfied for {:?}", ty);
|
||||
if !self.tcx.sess.opts.debugging_opts.chalk {
|
||||
// WF predicates cannot themselves make
|
||||
// errors. They can only block due to
|
||||
// ambiguity; otherwise, they always
|
||||
// degenerate into other obligations
|
||||
// (which may fail).
|
||||
span_bug!(span, "WF predicate not satisfied for {:?}", ty);
|
||||
} else {
|
||||
// FIXME: we'll need a better message which takes into account
|
||||
// which bounds actually failed to hold.
|
||||
self.tcx.sess.struct_span_err(
|
||||
span,
|
||||
&format!("the type `{}` is not well-formed (chalk)", ty)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
ty::Predicate::ConstEvaluatable(..) => {
|
||||
|
@ -1,19 +1,18 @@
|
||||
use infer::InferCtxt;
|
||||
use mir::interpret::{GlobalId, ErrorHandled};
|
||||
use ty::{self, Ty, TypeFoldable, ToPolyTraitRef, ToPredicate};
|
||||
use ty::{self, Ty, TypeFoldable, ToPolyTraitRef};
|
||||
use ty::error::ExpectedFound;
|
||||
use rustc_data_structures::obligation_forest::{DoCompleted, Error, ForestObligation};
|
||||
use rustc_data_structures::obligation_forest::{ObligationForest, ObligationProcessor};
|
||||
use rustc_data_structures::obligation_forest::{ProcessResult};
|
||||
use std::marker::PhantomData;
|
||||
use hir::def_id::DefId;
|
||||
|
||||
use super::CodeAmbiguity;
|
||||
use super::CodeProjectionError;
|
||||
use super::CodeSelectionError;
|
||||
use super::engine::{TraitEngine, TraitEngineExt};
|
||||
use super::{FulfillmentError, FulfillmentErrorCode};
|
||||
use super::{ObligationCause, PredicateObligation, Obligation};
|
||||
use super::{ObligationCause, PredicateObligation};
|
||||
use super::project;
|
||||
use super::select::SelectionContext;
|
||||
use super::{Unimplemented, ConstEvalFailure};
|
||||
@ -173,28 +172,6 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentContext<'tcx> {
|
||||
normalized_ty
|
||||
}
|
||||
|
||||
/// Requires that `ty` must implement the trait with `def_id` in
|
||||
/// the given environment. This trait must not have any type
|
||||
/// parameters (except for `Self`).
|
||||
fn register_bound<'a, 'gcx>(&mut self,
|
||||
infcx: &InferCtxt<'a, 'gcx, 'tcx>,
|
||||
param_env: ty::ParamEnv<'tcx>,
|
||||
ty: Ty<'tcx>,
|
||||
def_id: DefId,
|
||||
cause: ObligationCause<'tcx>)
|
||||
{
|
||||
let trait_ref = ty::TraitRef {
|
||||
def_id,
|
||||
substs: infcx.tcx.mk_substs_trait(ty, &[]),
|
||||
};
|
||||
self.register_predicate_obligation(infcx, Obligation {
|
||||
cause,
|
||||
recursion_depth: 0,
|
||||
param_env,
|
||||
predicate: trait_ref.to_predicate()
|
||||
});
|
||||
}
|
||||
|
||||
fn register_predicate_obligation<'a, 'gcx>(&mut self,
|
||||
infcx: &InferCtxt<'a, 'gcx, 'tcx>,
|
||||
obligation: PredicateObligation<'tcx>)
|
||||
@ -213,9 +190,10 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentContext<'tcx> {
|
||||
});
|
||||
}
|
||||
|
||||
fn select_all_or_error<'a, 'gcx>(&mut self,
|
||||
infcx: &InferCtxt<'a, 'gcx, 'tcx>)
|
||||
-> Result<(),Vec<FulfillmentError<'tcx>>>
|
||||
fn select_all_or_error<'a, 'gcx>(
|
||||
&mut self,
|
||||
infcx: &InferCtxt<'a, 'gcx, 'tcx>
|
||||
) -> Result<(),Vec<FulfillmentError<'tcx>>>
|
||||
{
|
||||
self.select_where_possible(infcx)?;
|
||||
|
||||
|
@ -4,6 +4,7 @@
|
||||
|
||||
#[allow(dead_code)]
|
||||
pub mod auto_trait;
|
||||
mod chalk_fulfill;
|
||||
mod coherence;
|
||||
pub mod error_reporting;
|
||||
mod engine;
|
||||
@ -61,6 +62,11 @@ pub use self::util::{elaborate_predicates, elaborate_trait_ref, elaborate_trait_
|
||||
pub use self::util::{supertraits, supertrait_def_ids, transitive_bounds,
|
||||
Supertraits, SupertraitDefIds};
|
||||
|
||||
pub use self::chalk_fulfill::{
|
||||
CanonicalGoal as ChalkCanonicalGoal,
|
||||
FulfillmentContext as ChalkFulfillmentContext
|
||||
};
|
||||
|
||||
pub use self::ObligationCauseCode::*;
|
||||
pub use self::FulfillmentErrorCode::*;
|
||||
pub use self::SelectionError::*;
|
||||
@ -340,9 +346,9 @@ impl<'tcx> DomainGoal<'tcx> {
|
||||
}
|
||||
|
||||
impl<'tcx> GoalKind<'tcx> {
|
||||
pub fn from_poly_domain_goal<'a>(
|
||||
pub fn from_poly_domain_goal<'a, 'gcx>(
|
||||
domain_goal: PolyDomainGoal<'tcx>,
|
||||
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
||||
tcx: TyCtxt<'a, 'gcx, 'tcx>,
|
||||
) -> GoalKind<'tcx> {
|
||||
match domain_goal.no_bound_vars() {
|
||||
Some(p) => p.into_goal(),
|
||||
|
@ -106,6 +106,15 @@ impl<'tcx> QueryDescription<'tcx> for queries::evaluate_obligation<'tcx> {
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> QueryDescription<'tcx> for queries::evaluate_goal<'tcx> {
|
||||
fn describe(
|
||||
_tcx: TyCtxt<'_, '_, '_>,
|
||||
goal: traits::ChalkCanonicalGoal<'tcx>
|
||||
) -> Cow<'static, str> {
|
||||
format!("evaluating trait selection obligation `{}`", goal.value.goal).into()
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> QueryDescription<'tcx> for queries::type_op_ascribe_user_type<'tcx> {
|
||||
fn describe(
|
||||
_tcx: TyCtxt<'_, '_, '_>,
|
||||
|
@ -593,6 +593,13 @@ define_queries! { <'tcx>
|
||||
CanonicalPredicateGoal<'tcx>
|
||||
) -> Result<traits::EvaluationResult, traits::OverflowError>,
|
||||
|
||||
[] fn evaluate_goal: EvaluateGoal(
|
||||
traits::ChalkCanonicalGoal<'tcx>
|
||||
) -> Result<
|
||||
Lrc<Canonical<'tcx, canonical::QueryResponse<'tcx, ()>>>,
|
||||
NoSolution
|
||||
>,
|
||||
|
||||
/// Do not call this query directly: part of the `Eq` type-op
|
||||
[] fn type_op_ascribe_user_type: TypeOpAscribeUserType(
|
||||
CanonicalTypeOpAscribeUserTypeGoal<'tcx>
|
||||
|
@ -1103,6 +1103,7 @@ pub fn force_from_dep_node<'a, 'gcx, 'lcx>(tcx: TyCtxt<'a, 'gcx, 'lcx>,
|
||||
DepKind::ImpliedOutlivesBounds |
|
||||
DepKind::DropckOutlives |
|
||||
DepKind::EvaluateObligation |
|
||||
DepKind::EvaluateGoal |
|
||||
DepKind::TypeOpAscribeUserType |
|
||||
DepKind::TypeOpEq |
|
||||
DepKind::TypeOpSubtype |
|
||||
|
@ -2,14 +2,15 @@ mod program_clauses;
|
||||
mod resolvent_ops;
|
||||
mod unify;
|
||||
|
||||
use chalk_engine::fallible::{Fallible, NoSolution};
|
||||
use chalk_engine::fallible::Fallible;
|
||||
use chalk_engine::{
|
||||
context,
|
||||
hh::HhGoal,
|
||||
DelayedLiteral,
|
||||
Literal,
|
||||
ExClause
|
||||
ExClause,
|
||||
};
|
||||
use chalk_engine::forest::Forest;
|
||||
use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
|
||||
use rustc::infer::canonical::{
|
||||
Canonical,
|
||||
@ -19,6 +20,7 @@ use rustc::infer::canonical::{
|
||||
Certainty,
|
||||
};
|
||||
use rustc::traits::{
|
||||
self,
|
||||
DomainGoal,
|
||||
ExClauseFold,
|
||||
ChalkContextLift,
|
||||
@ -28,10 +30,13 @@ use rustc::traits::{
|
||||
QuantifierKind,
|
||||
Environment,
|
||||
InEnvironment,
|
||||
ChalkCanonicalGoal,
|
||||
};
|
||||
use rustc::ty::{self, TyCtxt};
|
||||
use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
|
||||
use rustc::ty::query::Providers;
|
||||
use rustc::ty::subst::{Kind, UnpackedKind};
|
||||
use rustc_data_structures::sync::Lrc;
|
||||
use syntax_pos::DUMMY_SP;
|
||||
|
||||
use std::fmt::{self, Debug};
|
||||
@ -122,35 +127,50 @@ impl context::Context for ChalkArenas<'tcx> {
|
||||
impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
|
||||
fn make_solution(
|
||||
&self,
|
||||
_root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
|
||||
root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
|
||||
mut simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
|
||||
) -> Option<Canonical<'gcx, QueryResponse<'gcx, ()>>> {
|
||||
use chalk_engine::SimplifiedAnswer;
|
||||
|
||||
debug!("make_solution(root_goal = {:?})", root_goal);
|
||||
|
||||
if simplified_answers.peek_answer().is_none() {
|
||||
return None;
|
||||
}
|
||||
|
||||
let SimplifiedAnswer { subst, ambiguous } = simplified_answers
|
||||
let SimplifiedAnswer { subst: constrained_subst, ambiguous } = simplified_answers
|
||||
.next_answer()
|
||||
.unwrap();
|
||||
|
||||
debug!("make_solution: ambiguous flag = {}", ambiguous);
|
||||
|
||||
let ambiguous = simplified_answers.peek_answer().is_some() || ambiguous;
|
||||
|
||||
Some(subst.unchecked_map(|subst| {
|
||||
QueryResponse {
|
||||
var_values: subst.subst,
|
||||
region_constraints: subst.constraints
|
||||
.into_iter()
|
||||
.map(|c| ty::Binder::bind(c))
|
||||
.collect(),
|
||||
certainty: match ambiguous {
|
||||
true => Certainty::Ambiguous,
|
||||
false => Certainty::Proven,
|
||||
},
|
||||
let solution = constrained_subst.unchecked_map(|cs| match ambiguous {
|
||||
true => QueryResponse {
|
||||
var_values: cs.subst.make_identity(self.tcx),
|
||||
region_constraints: Vec::new(),
|
||||
certainty: Certainty::Ambiguous,
|
||||
value: (),
|
||||
}
|
||||
}))
|
||||
},
|
||||
|
||||
false => QueryResponse {
|
||||
var_values: cs.subst,
|
||||
region_constraints: Vec::new(),
|
||||
|
||||
// FIXME: restore this later once we get better at handling regions
|
||||
// region_constraints: cs.constraints
|
||||
// .into_iter()
|
||||
// .map(|c| ty::Binder::bind(c))
|
||||
// .collect(),
|
||||
certainty: Certainty::Proven,
|
||||
value: (),
|
||||
},
|
||||
});
|
||||
|
||||
debug!("make_solution: solution = {:?}", solution);
|
||||
|
||||
Some(solution)
|
||||
}
|
||||
}
|
||||
|
||||
@ -334,16 +354,16 @@ impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
{
|
||||
fn truncate_goal(
|
||||
&mut self,
|
||||
subgoal: &InEnvironment<'tcx, Goal<'tcx>>,
|
||||
_subgoal: &InEnvironment<'tcx, Goal<'tcx>>,
|
||||
) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
|
||||
Some(*subgoal) // FIXME we should truncate at some point!
|
||||
None // FIXME we should truncate at some point!
|
||||
}
|
||||
|
||||
fn truncate_answer(
|
||||
&mut self,
|
||||
subst: &CanonicalVarValues<'tcx>,
|
||||
_subst: &CanonicalVarValues<'tcx>,
|
||||
) -> Option<CanonicalVarValues<'tcx>> {
|
||||
Some(subst.clone()) // FIXME we should truncate at some point!
|
||||
None // FIXME we should truncate at some point!
|
||||
}
|
||||
}
|
||||
|
||||
@ -428,7 +448,7 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
b: &Kind<'tcx>,
|
||||
) -> Fallible<UnificationResult<'tcx>> {
|
||||
self.infcx.commit_if_ok(|_| {
|
||||
unify(self.infcx, *environment, a, b).map_err(|_| NoSolution)
|
||||
unify(self.infcx, *environment, a, b).map_err(|_| chalk_engine::fallible::NoSolution)
|
||||
})
|
||||
}
|
||||
|
||||
@ -462,7 +482,10 @@ crate fn into_ex_clause(result: UnificationResult<'tcx>, ex_clause: &mut ChalkEx
|
||||
ex_clause.subgoals.extend(
|
||||
result.goals.into_iter().map(Literal::Positive)
|
||||
);
|
||||
ex_clause.constraints.extend(result.constraints);
|
||||
|
||||
// FIXME: restore this later once we get better at handling regions
|
||||
let _ = result.constraints.len(); // trick `-D dead-code`
|
||||
// ex_clause.constraints.extend(result.constraints);
|
||||
}
|
||||
|
||||
type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
|
||||
@ -625,3 +648,52 @@ impl<'tcx, 'gcx: 'tcx, T> Upcast<'tcx, 'gcx> for Canonical<'gcx, T>
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
crate fn provide(p: &mut Providers) {
|
||||
*p = Providers {
|
||||
evaluate_goal,
|
||||
..*p
|
||||
};
|
||||
}
|
||||
|
||||
crate fn evaluate_goal<'a, 'tcx>(
|
||||
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
||||
goal: ChalkCanonicalGoal<'tcx>
|
||||
) -> Result<
|
||||
Lrc<Canonical<'tcx, QueryResponse<'tcx, ()>>>,
|
||||
traits::query::NoSolution
|
||||
> {
|
||||
use crate::lowering::Lower;
|
||||
use rustc::traits::WellFormed;
|
||||
|
||||
let goal = goal.unchecked_map(|goal| InEnvironment {
|
||||
environment: goal.environment,
|
||||
goal: match goal.goal {
|
||||
ty::Predicate::WellFormed(ty) => tcx.mk_goal(
|
||||
GoalKind::DomainGoal(DomainGoal::WellFormed(WellFormed::Ty(ty)))
|
||||
),
|
||||
|
||||
other => tcx.mk_goal(
|
||||
GoalKind::from_poly_domain_goal(other.lower(), tcx)
|
||||
),
|
||||
},
|
||||
});
|
||||
|
||||
|
||||
debug!("evaluate_goal(goal = {:?})", goal);
|
||||
|
||||
let context = ChalkContext {
|
||||
_arenas: ChalkArenas {
|
||||
_phantom: PhantomData,
|
||||
},
|
||||
tcx,
|
||||
};
|
||||
|
||||
let mut forest = Forest::new(context);
|
||||
let solution = forest.solve(&goal);
|
||||
|
||||
debug!("evaluate_goal: solution = {:?}", solution);
|
||||
|
||||
solution.map(|ok| Ok(Lrc::new(ok)))
|
||||
.unwrap_or(Err(traits::query::NoSolution))
|
||||
}
|
||||
|
@ -350,6 +350,9 @@ impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
|
||||
goal: &DomainGoal<'tcx>,
|
||||
) -> Vec<Clause<'tcx>> {
|
||||
use rustc::traits::WhereClause::*;
|
||||
use rustc::infer::canonical::OriginalQueryValues;
|
||||
|
||||
let goal = self.infcx.resolve_type_vars_if_possible(goal);
|
||||
|
||||
debug!("program_clauses(goal = {:?})", goal);
|
||||
|
||||
@ -582,10 +585,12 @@ impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
|
||||
debug!("program_clauses: clauses = {:?}", clauses);
|
||||
debug!("program_clauses: adding clauses from environment = {:?}", environment);
|
||||
|
||||
let environment = self.infcx.tcx.lift_to_global(environment)
|
||||
.expect("environment is not global");
|
||||
|
||||
let env_clauses = self.infcx.tcx.program_clauses_for_env(environment);
|
||||
let mut _orig_query_values = OriginalQueryValues::default();
|
||||
let canonical_environment = self.infcx.canonicalize_query(
|
||||
environment,
|
||||
&mut _orig_query_values
|
||||
).value;
|
||||
let env_clauses = self.infcx.tcx.program_clauses_for_env(canonical_environment);
|
||||
|
||||
debug!("program_clauses: env_clauses = {:?}", env_clauses);
|
||||
|
||||
|
@ -35,7 +35,9 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
) -> Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
|
||||
use chalk_engine::context::UnificationOps;
|
||||
|
||||
self.infcx.probe(|_| {
|
||||
debug!("resolvent_clause(goal = {:?}, clause = {:?})", goal, clause);
|
||||
|
||||
let result = self.infcx.probe(|_| {
|
||||
let ProgramClause {
|
||||
goal: consequence,
|
||||
hypotheses,
|
||||
@ -70,7 +72,10 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
|
||||
let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
|
||||
Ok(canonical_ex_clause)
|
||||
})
|
||||
});
|
||||
|
||||
debug!("resolvent_clause: result = {:?}", result);
|
||||
result
|
||||
}
|
||||
|
||||
fn apply_answer_subst(
|
||||
@ -80,6 +85,12 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
|
||||
canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
|
||||
) -> Fallible<ChalkExClause<'tcx>> {
|
||||
debug!(
|
||||
"apply_answer_subst(ex_clause = {:?}, selected_goal = {:?})",
|
||||
self.infcx.resolve_type_vars_if_possible(&ex_clause),
|
||||
self.infcx.resolve_type_vars_if_possible(selected_goal)
|
||||
);
|
||||
|
||||
let (answer_subst, _) = self.infcx.instantiate_canonical_with_fresh_inference_vars(
|
||||
DUMMY_SP,
|
||||
canonical_answer_subst
|
||||
@ -96,8 +107,12 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
||||
substitutor.relate(&answer_table_goal.value, &selected_goal)
|
||||
.map_err(|_| NoSolution)?;
|
||||
|
||||
let mut ex_clause = substitutor.ex_clause;
|
||||
ex_clause.constraints.extend(answer_subst.constraints);
|
||||
let ex_clause = substitutor.ex_clause;
|
||||
|
||||
// FIXME: restore this later once we get better at handling regions
|
||||
// ex_clause.constraints.extend(answer_subst.constraints);
|
||||
|
||||
debug!("apply_answer_subst: ex_clause = {:?}", ex_clause);
|
||||
Ok(ex_clause)
|
||||
}
|
||||
}
|
||||
@ -172,6 +187,7 @@ impl TypeRelation<'cx, 'gcx, 'tcx> for AnswerSubstitutor<'cx, 'gcx, 'tcx> {
|
||||
|
||||
fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
|
||||
let b = self.infcx.shallow_resolve(b);
|
||||
debug!("AnswerSubstitutor::tys(a = {:?}, b = {:?})", a, b);
|
||||
|
||||
if let &ty::Bound(debruijn, bound_ty) = &a.sty {
|
||||
// Free bound var
|
||||
|
@ -16,6 +16,12 @@ crate fn unify<'me, 'gcx, 'tcx, T: Relate<'tcx>>(
|
||||
a: &T,
|
||||
b: &T
|
||||
) -> RelateResult<'tcx, UnificationResult<'tcx>> {
|
||||
debug!("unify(
|
||||
a = {:?},
|
||||
b = {:?},
|
||||
environment = {:?},
|
||||
)", a, b, environment);
|
||||
|
||||
let mut delegate = ChalkTypeRelatingDelegate::new(
|
||||
infcx,
|
||||
environment
|
||||
@ -27,6 +33,8 @@ crate fn unify<'me, 'gcx, 'tcx, T: Relate<'tcx>>(
|
||||
ty::Variance::Invariant
|
||||
).relate(a, b)?;
|
||||
|
||||
debug!("unify: goals = {:?}, constraints = {:?}", delegate.goals, delegate.constraints);
|
||||
|
||||
Ok(UnificationResult {
|
||||
goals: delegate.goals,
|
||||
constraints: delegate.constraints,
|
||||
|
@ -35,6 +35,7 @@ pub fn provide(p: &mut Providers) {
|
||||
evaluate_obligation::provide(p);
|
||||
implied_outlives_bounds::provide(p);
|
||||
lowering::provide(p);
|
||||
chalk_context::provide(p);
|
||||
normalize_projection_ty::provide(p);
|
||||
normalize_erasing_regions::provide(p);
|
||||
type_op::provide(p);
|
||||
|
Loading…
x
Reference in New Issue
Block a user