convert prove_predicate
into a query
This commit is contained in:
parent
d6136837b7
commit
de7e941e4e
8 changed files with 92 additions and 17 deletions
|
@ -72,7 +72,7 @@ use std::hash::Hash;
|
||||||
use syntax_pos::symbol::InternedString;
|
use syntax_pos::symbol::InternedString;
|
||||||
use traits::query::{
|
use traits::query::{
|
||||||
CanonicalProjectionGoal, CanonicalTyGoal, CanonicalTypeOpEqGoal, CanonicalTypeOpSubtypeGoal,
|
CanonicalProjectionGoal, CanonicalTyGoal, CanonicalTypeOpEqGoal, CanonicalTypeOpSubtypeGoal,
|
||||||
CanonicalPredicateGoal,
|
CanonicalPredicateGoal, CanonicalTypeOpProvePredicateGoal,
|
||||||
};
|
};
|
||||||
use ty::{TyCtxt, Instance, InstanceDef, ParamEnv, ParamEnvAnd, PolyTraitRef, Ty};
|
use ty::{TyCtxt, Instance, InstanceDef, ParamEnv, ParamEnvAnd, PolyTraitRef, Ty};
|
||||||
use ty::subst::Substs;
|
use ty::subst::Substs;
|
||||||
|
@ -651,6 +651,7 @@ define_dep_nodes!( <'tcx>
|
||||||
[] EvaluateObligation(CanonicalPredicateGoal<'tcx>),
|
[] EvaluateObligation(CanonicalPredicateGoal<'tcx>),
|
||||||
[] TypeOpEq(CanonicalTypeOpEqGoal<'tcx>),
|
[] TypeOpEq(CanonicalTypeOpEqGoal<'tcx>),
|
||||||
[] TypeOpSubtype(CanonicalTypeOpSubtypeGoal<'tcx>),
|
[] TypeOpSubtype(CanonicalTypeOpSubtypeGoal<'tcx>),
|
||||||
|
[] TypeOpProvePredicate(CanonicalTypeOpProvePredicateGoal<'tcx>),
|
||||||
|
|
||||||
[] SubstituteNormalizeAndTestPredicates { key: (DefId, &'tcx Substs<'tcx>) },
|
[] SubstituteNormalizeAndTestPredicates { key: (DefId, &'tcx Substs<'tcx>) },
|
||||||
|
|
||||||
|
|
|
@ -38,6 +38,9 @@ pub type CanonicalTypeOpEqGoal<'tcx> =
|
||||||
pub type CanonicalTypeOpSubtypeGoal<'tcx> =
|
pub type CanonicalTypeOpSubtypeGoal<'tcx> =
|
||||||
Canonical<'tcx, type_op::subtype::Subtype<'tcx>>;
|
Canonical<'tcx, type_op::subtype::Subtype<'tcx>>;
|
||||||
|
|
||||||
|
pub type CanonicalTypeOpProvePredicateGoal<'tcx> =
|
||||||
|
Canonical<'tcx, type_op::prove_predicate::ProvePredicate<'tcx>>;
|
||||||
|
|
||||||
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
|
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
|
||||||
pub struct NoSolution;
|
pub struct NoSolution;
|
||||||
|
|
||||||
|
|
|
@ -8,14 +8,13 @@
|
||||||
// option. This file may not be copied, modified, or distributed
|
// option. This file may not be copied, modified, or distributed
|
||||||
// except according to those terms.
|
// except according to those terms.
|
||||||
|
|
||||||
use infer::{InferCtxt, InferOk, InferResult};
|
use infer::canonical::{Canonical, CanonicalizedQueryResult};
|
||||||
use traits::{Obligation, ObligationCause};
|
|
||||||
use ty::{ParamEnv, Predicate, TyCtxt};
|
use ty::{ParamEnv, Predicate, TyCtxt};
|
||||||
|
|
||||||
#[derive(Debug)]
|
#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
|
||||||
pub struct ProvePredicate<'tcx> {
|
pub struct ProvePredicate<'tcx> {
|
||||||
param_env: ParamEnv<'tcx>,
|
pub param_env: ParamEnv<'tcx>,
|
||||||
predicate: Predicate<'tcx>,
|
pub predicate: Predicate<'tcx>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> ProvePredicate<'tcx> {
|
impl<'tcx> ProvePredicate<'tcx> {
|
||||||
|
@ -27,18 +26,40 @@ impl<'tcx> ProvePredicate<'tcx> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'gcx, 'tcx> super::TypeOp<'gcx, 'tcx> for ProvePredicate<'tcx> {
|
impl<'gcx: 'tcx, 'tcx> super::QueryTypeOp<'gcx, 'tcx> for ProvePredicate<'tcx> {
|
||||||
type Output = ();
|
type QueryResult = ();
|
||||||
|
|
||||||
fn trivial_noop(self, _tcx: TyCtxt<'_, 'gcx, 'tcx>) -> Result<Self::Output, Self> {
|
fn trivial_noop(self, _tcx: TyCtxt<'_, 'gcx, 'tcx>) -> Result<Self::QueryResult, Self> {
|
||||||
Err(self)
|
Err(self)
|
||||||
}
|
}
|
||||||
|
|
||||||
fn perform(self, _infcx: &InferCtxt<'_, 'gcx, 'tcx>) -> InferResult<'tcx, Self::Output> {
|
fn param_env(&self) -> ParamEnv<'tcx> {
|
||||||
let obligation = Obligation::new(ObligationCause::dummy(), self.param_env, self.predicate);
|
self.param_env
|
||||||
Ok(InferOk {
|
}
|
||||||
value: (),
|
|
||||||
obligations: vec![obligation],
|
fn perform_query(
|
||||||
})
|
tcx: TyCtxt<'_, 'gcx, 'tcx>,
|
||||||
|
canonicalized: Canonical<'gcx, ProvePredicate<'gcx>>,
|
||||||
|
) -> CanonicalizedQueryResult<'gcx, ()> {
|
||||||
|
tcx.type_op_prove_predicate(canonicalized).unwrap()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
BraceStructTypeFoldableImpl! {
|
||||||
|
impl<'tcx> TypeFoldable<'tcx> for ProvePredicate<'tcx> {
|
||||||
|
param_env,
|
||||||
|
predicate,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
BraceStructLiftImpl! {
|
||||||
|
impl<'a, 'tcx> Lift<'tcx> for ProvePredicate<'a> {
|
||||||
|
type Lifted = ProvePredicate<'tcx>;
|
||||||
|
param_env,
|
||||||
|
predicate,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl_stable_hash_for! {
|
||||||
|
struct ProvePredicate<'tcx> { param_env, predicate }
|
||||||
|
}
|
||||||
|
|
|
@ -14,7 +14,7 @@ use hir::def_id::{CrateNum, DefId, DefIndex};
|
||||||
use mir::interpret::{GlobalId, ConstValue};
|
use mir::interpret::{GlobalId, ConstValue};
|
||||||
use traits::query::{
|
use traits::query::{
|
||||||
CanonicalPredicateGoal, CanonicalProjectionGoal, CanonicalTyGoal, CanonicalTypeOpEqGoal,
|
CanonicalPredicateGoal, CanonicalProjectionGoal, CanonicalTyGoal, CanonicalTypeOpEqGoal,
|
||||||
CanonicalTypeOpSubtypeGoal,
|
CanonicalTypeOpProvePredicateGoal, CanonicalTypeOpSubtypeGoal,
|
||||||
};
|
};
|
||||||
use ty::{self, ParamEnvAnd, Ty, TyCtxt};
|
use ty::{self, ParamEnvAnd, Ty, TyCtxt};
|
||||||
use ty::subst::Substs;
|
use ty::subst::Substs;
|
||||||
|
@ -117,6 +117,12 @@ impl<'tcx> QueryDescription<'tcx> for queries::type_op_subtype<'tcx> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl<'tcx> QueryDescription<'tcx> for queries::type_op_prove_predicate<'tcx> {
|
||||||
|
fn describe(_tcx: TyCtxt, goal: CanonicalTypeOpProvePredicateGoal<'tcx>) -> String {
|
||||||
|
format!("evaluating `type_op_prove_predicate` `{:?}`", goal)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
impl<'tcx> QueryDescription<'tcx> for queries::is_copy_raw<'tcx> {
|
impl<'tcx> QueryDescription<'tcx> for queries::is_copy_raw<'tcx> {
|
||||||
fn describe(_tcx: TyCtxt, env: ty::ParamEnvAnd<'tcx, Ty<'tcx>>) -> String {
|
fn describe(_tcx: TyCtxt, env: ty::ParamEnvAnd<'tcx, Ty<'tcx>>) -> String {
|
||||||
format!("computing whether `{}` is `Copy`", env.value)
|
format!("computing whether `{}` is `Copy`", env.value)
|
||||||
|
|
|
@ -34,7 +34,8 @@ use session::{CompileResult, CrateDisambiguator};
|
||||||
use session::config::OutputFilenames;
|
use session::config::OutputFilenames;
|
||||||
use traits::{self, Vtable};
|
use traits::{self, Vtable};
|
||||||
use traits::query::{CanonicalPredicateGoal, CanonicalProjectionGoal,
|
use traits::query::{CanonicalPredicateGoal, CanonicalProjectionGoal,
|
||||||
CanonicalTyGoal, CanonicalTypeOpEqGoal, CanonicalTypeOpSubtypeGoal, NoSolution};
|
CanonicalTyGoal, CanonicalTypeOpEqGoal, CanonicalTypeOpSubtypeGoal,
|
||||||
|
CanonicalTypeOpProvePredicateGoal, NoSolution};
|
||||||
use traits::query::dropck_outlives::{DtorckConstraint, DropckOutlivesResult};
|
use traits::query::dropck_outlives::{DtorckConstraint, DropckOutlivesResult};
|
||||||
use traits::query::normalize::NormalizationResult;
|
use traits::query::normalize::NormalizationResult;
|
||||||
use traits::specialization_graph;
|
use traits::specialization_graph;
|
||||||
|
@ -462,6 +463,14 @@ define_queries! { <'tcx>
|
||||||
NoSolution,
|
NoSolution,
|
||||||
>,
|
>,
|
||||||
|
|
||||||
|
/// Do not call this query directly: invoke `infcx.at().prove_predicates()` instead.
|
||||||
|
[] fn type_op_prove_predicate: TypeOpProvePredicate(
|
||||||
|
CanonicalTypeOpProvePredicateGoal<'tcx>
|
||||||
|
) -> Result<
|
||||||
|
Lrc<Canonical<'tcx, canonical::QueryResult<'tcx, ()>>>,
|
||||||
|
NoSolution,
|
||||||
|
>,
|
||||||
|
|
||||||
[] fn substitute_normalize_and_test_predicates:
|
[] fn substitute_normalize_and_test_predicates:
|
||||||
substitute_normalize_and_test_predicates_node((DefId, &'tcx Substs<'tcx>)) -> bool,
|
substitute_normalize_and_test_predicates_node((DefId, &'tcx Substs<'tcx>)) -> bool,
|
||||||
|
|
||||||
|
|
|
@ -1030,6 +1030,7 @@ pub fn force_from_dep_node<'a, 'gcx, 'lcx>(tcx: TyCtxt<'a, 'gcx, 'lcx>,
|
||||||
DepKind::EvaluateObligation |
|
DepKind::EvaluateObligation |
|
||||||
DepKind::TypeOpEq |
|
DepKind::TypeOpEq |
|
||||||
DepKind::TypeOpSubtype |
|
DepKind::TypeOpSubtype |
|
||||||
|
DepKind::TypeOpProvePredicate |
|
||||||
DepKind::SubstituteNormalizeAndTestPredicates |
|
DepKind::SubstituteNormalizeAndTestPredicates |
|
||||||
DepKind::InstanceDefSizeEstimate |
|
DepKind::InstanceDefSizeEstimate |
|
||||||
DepKind::ProgramClausesForEnv |
|
DepKind::ProgramClausesForEnv |
|
||||||
|
|
|
@ -35,6 +35,7 @@ mod normalize_projection_ty;
|
||||||
mod normalize_erasing_regions;
|
mod normalize_erasing_regions;
|
||||||
pub mod lowering;
|
pub mod lowering;
|
||||||
mod type_op_eq;
|
mod type_op_eq;
|
||||||
|
mod type_op_prove_predicate;
|
||||||
mod type_op_subtype;
|
mod type_op_subtype;
|
||||||
|
|
||||||
use rustc::ty::query::Providers;
|
use rustc::ty::query::Providers;
|
||||||
|
@ -50,6 +51,7 @@ pub fn provide(p: &mut Providers) {
|
||||||
program_clauses_for_env: lowering::program_clauses_for_env,
|
program_clauses_for_env: lowering::program_clauses_for_env,
|
||||||
evaluate_obligation: evaluate_obligation::evaluate_obligation,
|
evaluate_obligation: evaluate_obligation::evaluate_obligation,
|
||||||
type_op_eq: type_op_eq::type_op_eq,
|
type_op_eq: type_op_eq::type_op_eq,
|
||||||
|
type_op_prove_predicate: type_op_prove_predicate::type_op_prove_predicate,
|
||||||
type_op_subtype: type_op_subtype::type_op_subtype,
|
type_op_subtype: type_op_subtype::type_op_subtype,
|
||||||
..*p
|
..*p
|
||||||
};
|
};
|
||||||
|
|
32
src/librustc_traits/type_op_prove_predicate.rs
Normal file
32
src/librustc_traits/type_op_prove_predicate.rs
Normal file
|
@ -0,0 +1,32 @@
|
||||||
|
// Copyright 2014 The Rust Project Developers. See the COPYRIGHT
|
||||||
|
// file at the top-level directory of this distribution and at
|
||||||
|
// http://rust-lang.org/COPYRIGHT.
|
||||||
|
//
|
||||||
|
// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
|
||||||
|
// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
|
||||||
|
// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
|
||||||
|
// option. This file may not be copied, modified, or distributed
|
||||||
|
// except according to those terms.
|
||||||
|
|
||||||
|
use rustc::infer::canonical::{Canonical, QueryResult};
|
||||||
|
use rustc::traits::query::type_op::prove_predicate::ProvePredicate;
|
||||||
|
use rustc::traits::query::NoSolution;
|
||||||
|
use rustc::traits::{FulfillmentContext, Obligation, ObligationCause, TraitEngine};
|
||||||
|
use rustc::ty::TyCtxt;
|
||||||
|
use rustc_data_structures::sync::Lrc;
|
||||||
|
use syntax::codemap::DUMMY_SP;
|
||||||
|
|
||||||
|
crate fn type_op_prove_predicate<'tcx>(
|
||||||
|
tcx: TyCtxt<'_, 'tcx, 'tcx>,
|
||||||
|
canonicalized: Canonical<'tcx, ProvePredicate<'tcx>>,
|
||||||
|
) -> Result<Lrc<Canonical<'tcx, QueryResult<'tcx, ()>>>, NoSolution> {
|
||||||
|
let tcx = tcx.global_tcx();
|
||||||
|
tcx.infer_ctxt().enter(|ref infcx| {
|
||||||
|
let (ProvePredicate { param_env, predicate }, canonical_inference_vars) =
|
||||||
|
infcx.instantiate_canonical_with_fresh_inference_vars(DUMMY_SP, &canonicalized);
|
||||||
|
let fulfill_cx = &mut FulfillmentContext::new();
|
||||||
|
let obligation = Obligation::new(ObligationCause::dummy(), param_env, predicate);
|
||||||
|
fulfill_cx.register_predicate_obligation(infcx, obligation);
|
||||||
|
infcx.make_canonicalized_query_result(canonical_inference_vars, (), fulfill_cx)
|
||||||
|
})
|
||||||
|
}
|
Loading…
Add table
Add a link
Reference in a new issue