Make ProofTreeBuilder actually generic over interner
This commit is contained in:
parent
50a5da16b8
commit
f494036530
@ -218,6 +218,13 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
|
|||||||
self.check_and_mk_args(def_id, args)
|
self.check_and_mk_args(def_id, args)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn intern_canonical_goal_evaluation_step(
|
||||||
|
self,
|
||||||
|
step: solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>,
|
||||||
|
) -> &'tcx solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>> {
|
||||||
|
self.arena.alloc(step)
|
||||||
|
}
|
||||||
|
|
||||||
fn parent(self, def_id: Self::DefId) -> Self::DefId {
|
fn parent(self, def_id: Self::DefId) -> Self::DefId {
|
||||||
self.parent(def_id)
|
self.parent(def_id)
|
||||||
}
|
}
|
||||||
|
@ -16,7 +16,6 @@ use crate::solve::{
|
|||||||
use rustc_data_structures::fx::FxHashSet;
|
use rustc_data_structures::fx::FxHashSet;
|
||||||
use rustc_index::IndexVec;
|
use rustc_index::IndexVec;
|
||||||
use rustc_infer::infer::canonical::query_response::make_query_region_constraints;
|
use rustc_infer::infer::canonical::query_response::make_query_region_constraints;
|
||||||
use rustc_infer::infer::canonical::CanonicalVarValues;
|
|
||||||
use rustc_infer::infer::canonical::{CanonicalExt, QueryRegionConstraints};
|
use rustc_infer::infer::canonical::{CanonicalExt, QueryRegionConstraints};
|
||||||
use rustc_infer::infer::RegionVariableOrigin;
|
use rustc_infer::infer::RegionVariableOrigin;
|
||||||
use rustc_infer::infer::{InferCtxt, InferOk};
|
use rustc_infer::infer::{InferCtxt, InferOk};
|
||||||
@ -32,22 +31,24 @@ use rustc_middle::ty::{self, BoundVar, GenericArgKind, Ty, TyCtxt, TypeFoldable}
|
|||||||
use rustc_next_trait_solver::canonicalizer::{CanonicalizeMode, Canonicalizer};
|
use rustc_next_trait_solver::canonicalizer::{CanonicalizeMode, Canonicalizer};
|
||||||
use rustc_next_trait_solver::resolve::EagerResolver;
|
use rustc_next_trait_solver::resolve::EagerResolver;
|
||||||
use rustc_span::{Span, DUMMY_SP};
|
use rustc_span::{Span, DUMMY_SP};
|
||||||
|
use rustc_type_ir::CanonicalVarValues;
|
||||||
|
use rustc_type_ir::{InferCtxtLike, Interner};
|
||||||
use std::assert_matches::assert_matches;
|
use std::assert_matches::assert_matches;
|
||||||
use std::iter;
|
use std::iter;
|
||||||
use std::ops::Deref;
|
use std::ops::Deref;
|
||||||
|
|
||||||
trait ResponseT<'tcx> {
|
trait ResponseT<'tcx> {
|
||||||
fn var_values(&self) -> CanonicalVarValues<'tcx>;
|
fn var_values(&self) -> CanonicalVarValues<TyCtxt<'tcx>>;
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx> ResponseT<'tcx> for Response<TyCtxt<'tcx>> {
|
impl<'tcx> ResponseT<'tcx> for Response<TyCtxt<'tcx>> {
|
||||||
fn var_values(&self) -> CanonicalVarValues<'tcx> {
|
fn var_values(&self) -> CanonicalVarValues<TyCtxt<'tcx>> {
|
||||||
self.var_values
|
self.var_values
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'tcx, T> ResponseT<'tcx> for inspect::State<TyCtxt<'tcx>, T> {
|
impl<'tcx, T> ResponseT<'tcx> for inspect::State<TyCtxt<'tcx>, T> {
|
||||||
fn var_values(&self) -> CanonicalVarValues<'tcx> {
|
fn var_values(&self) -> CanonicalVarValues<TyCtxt<'tcx>> {
|
||||||
self.var_values
|
self.var_values
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -260,7 +261,7 @@ impl<'tcx> EvalCtxt<'_, InferCtxt<'tcx>> {
|
|||||||
infcx: &InferCtxt<'tcx>,
|
infcx: &InferCtxt<'tcx>,
|
||||||
original_values: &[ty::GenericArg<'tcx>],
|
original_values: &[ty::GenericArg<'tcx>],
|
||||||
response: &Canonical<'tcx, T>,
|
response: &Canonical<'tcx, T>,
|
||||||
) -> CanonicalVarValues<'tcx> {
|
) -> CanonicalVarValues<TyCtxt<'tcx>> {
|
||||||
// FIXME: Longterm canonical queries should deal with all placeholders
|
// FIXME: Longterm canonical queries should deal with all placeholders
|
||||||
// created inside of the query directly instead of returning them to the
|
// created inside of the query directly instead of returning them to the
|
||||||
// caller.
|
// caller.
|
||||||
@ -354,7 +355,7 @@ impl<'tcx> EvalCtxt<'_, InferCtxt<'tcx>> {
|
|||||||
infcx: &InferCtxt<'tcx>,
|
infcx: &InferCtxt<'tcx>,
|
||||||
param_env: ty::ParamEnv<'tcx>,
|
param_env: ty::ParamEnv<'tcx>,
|
||||||
original_values: &[ty::GenericArg<'tcx>],
|
original_values: &[ty::GenericArg<'tcx>],
|
||||||
var_values: CanonicalVarValues<'tcx>,
|
var_values: CanonicalVarValues<TyCtxt<'tcx>>,
|
||||||
) {
|
) {
|
||||||
assert_eq!(original_values.len(), var_values.len());
|
assert_eq!(original_values.len(), var_values.len());
|
||||||
|
|
||||||
@ -393,13 +394,18 @@ impl<'tcx> EvalCtxt<'_, InferCtxt<'tcx>> {
|
|||||||
/// evaluating a goal. The `var_values` not only include the bound variables
|
/// evaluating a goal. The `var_values` not only include the bound variables
|
||||||
/// of the query input, but also contain all unconstrained inference vars
|
/// of the query input, but also contain all unconstrained inference vars
|
||||||
/// created while evaluating this goal.
|
/// created while evaluating this goal.
|
||||||
pub(in crate::solve) fn make_canonical_state<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(
|
pub(in crate::solve) fn make_canonical_state<Infcx, T, I>(
|
||||||
infcx: &InferCtxt<'tcx>,
|
infcx: &Infcx,
|
||||||
var_values: &[ty::GenericArg<'tcx>],
|
var_values: &[I::GenericArg],
|
||||||
max_input_universe: ty::UniverseIndex,
|
max_input_universe: ty::UniverseIndex,
|
||||||
data: T,
|
data: T,
|
||||||
) -> inspect::CanonicalState<TyCtxt<'tcx>, T> {
|
) -> inspect::CanonicalState<I, T>
|
||||||
let var_values = CanonicalVarValues { var_values: infcx.tcx.mk_args(var_values) };
|
where
|
||||||
|
Infcx: InferCtxtLike<Interner = I>,
|
||||||
|
I: Interner,
|
||||||
|
T: TypeFoldable<I>,
|
||||||
|
{
|
||||||
|
let var_values = CanonicalVarValues { var_values: infcx.interner().mk_args(var_values) };
|
||||||
let state = inspect::State { var_values, data };
|
let state = inspect::State { var_values, data };
|
||||||
let state = state.fold_with(&mut EagerResolver::new(infcx));
|
let state = state.fold_with(&mut EagerResolver::new(infcx));
|
||||||
Canonicalizer::canonicalize(
|
Canonicalizer::canonicalize(
|
||||||
|
@ -98,7 +98,7 @@ pub struct EvalCtxt<
|
|||||||
// evaluation code.
|
// evaluation code.
|
||||||
tainted: Result<(), NoSolution>,
|
tainted: Result<(), NoSolution>,
|
||||||
|
|
||||||
pub(super) inspect: ProofTreeBuilder<I>,
|
pub(super) inspect: ProofTreeBuilder<Infcx>,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(derivative::Derivative)]
|
#[derive(derivative::Derivative)]
|
||||||
@ -218,7 +218,7 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
|
|||||||
tcx: TyCtxt<'tcx>,
|
tcx: TyCtxt<'tcx>,
|
||||||
search_graph: &'a mut search_graph::SearchGraph<TyCtxt<'tcx>>,
|
search_graph: &'a mut search_graph::SearchGraph<TyCtxt<'tcx>>,
|
||||||
canonical_input: CanonicalInput<'tcx>,
|
canonical_input: CanonicalInput<'tcx>,
|
||||||
canonical_goal_evaluation: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
|
canonical_goal_evaluation: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
|
||||||
f: impl FnOnce(&mut EvalCtxt<'_, InferCtxt<'tcx>>, Goal<'tcx, ty::Predicate<'tcx>>) -> R,
|
f: impl FnOnce(&mut EvalCtxt<'_, InferCtxt<'tcx>>, Goal<'tcx, ty::Predicate<'tcx>>) -> R,
|
||||||
) -> R {
|
) -> R {
|
||||||
let intercrate = match search_graph.solver_mode() {
|
let intercrate = match search_graph.solver_mode() {
|
||||||
@ -280,7 +280,7 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
|
|||||||
tcx: TyCtxt<'tcx>,
|
tcx: TyCtxt<'tcx>,
|
||||||
search_graph: &'a mut search_graph::SearchGraph<TyCtxt<'tcx>>,
|
search_graph: &'a mut search_graph::SearchGraph<TyCtxt<'tcx>>,
|
||||||
canonical_input: CanonicalInput<'tcx>,
|
canonical_input: CanonicalInput<'tcx>,
|
||||||
goal_evaluation: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
|
goal_evaluation: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
|
||||||
) -> QueryResult<'tcx> {
|
) -> QueryResult<'tcx> {
|
||||||
let mut canonical_goal_evaluation =
|
let mut canonical_goal_evaluation =
|
||||||
goal_evaluation.new_canonical_goal_evaluation(canonical_input);
|
goal_evaluation.new_canonical_goal_evaluation(canonical_input);
|
||||||
@ -1114,7 +1114,7 @@ struct ReplaceAliasWithInfer<'me, 'a, 'tcx> {
|
|||||||
|
|
||||||
impl<'tcx> TypeFolder<TyCtxt<'tcx>> for ReplaceAliasWithInfer<'_, '_, 'tcx> {
|
impl<'tcx> TypeFolder<TyCtxt<'tcx>> for ReplaceAliasWithInfer<'_, '_, 'tcx> {
|
||||||
fn interner(&self) -> TyCtxt<'tcx> {
|
fn interner(&self) -> TyCtxt<'tcx> {
|
||||||
self.ecx.tcx()
|
self.ecx.interner()
|
||||||
}
|
}
|
||||||
|
|
||||||
fn fold_ty(&mut self, ty: Ty<'tcx>) -> Ty<'tcx> {
|
fn fold_ty(&mut self, ty: Ty<'tcx>) -> Ty<'tcx> {
|
||||||
|
@ -3,18 +3,16 @@
|
|||||||
//! This code is *a bit* of a mess and can hopefully be
|
//! This code is *a bit* of a mess and can hopefully be
|
||||||
//! mostly ignored. For a general overview of how it works,
|
//! mostly ignored. For a general overview of how it works,
|
||||||
//! see the comment on [ProofTreeBuilder].
|
//! see the comment on [ProofTreeBuilder].
|
||||||
|
use std::marker::PhantomData;
|
||||||
use std::mem;
|
use std::mem;
|
||||||
|
|
||||||
use crate::solve::eval_ctxt::canonical;
|
use crate::solve::eval_ctxt::canonical;
|
||||||
use crate::solve::{self, inspect, GenerateProofTree};
|
use crate::solve::{self, inspect, GenerateProofTree};
|
||||||
use rustc_infer::infer::InferCtxt;
|
|
||||||
use rustc_middle::bug;
|
use rustc_middle::bug;
|
||||||
use rustc_middle::infer::canonical::CanonicalVarValues;
|
|
||||||
use rustc_middle::ty::{self, TyCtxt};
|
|
||||||
use rustc_next_trait_solver::solve::{
|
use rustc_next_trait_solver::solve::{
|
||||||
CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
|
CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
|
||||||
};
|
};
|
||||||
use rustc_type_ir::Interner;
|
use rustc_type_ir::{self as ty, InferCtxtLike, Interner};
|
||||||
|
|
||||||
/// The core data structure when building proof trees.
|
/// The core data structure when building proof trees.
|
||||||
///
|
///
|
||||||
@ -36,7 +34,11 @@ use rustc_type_ir::Interner;
|
|||||||
/// trees. At the end of trait solving `ProofTreeBuilder::finalize`
|
/// trees. At the end of trait solving `ProofTreeBuilder::finalize`
|
||||||
/// is called to recursively convert the whole structure to a
|
/// is called to recursively convert the whole structure to a
|
||||||
/// finished proof tree.
|
/// finished proof tree.
|
||||||
pub(in crate::solve) struct ProofTreeBuilder<I: Interner> {
|
pub(in crate::solve) struct ProofTreeBuilder<
|
||||||
|
Infcx: InferCtxtLike<Interner = I>,
|
||||||
|
I: Interner = <Infcx as InferCtxtLike>::Interner,
|
||||||
|
> {
|
||||||
|
_infcx: PhantomData<Infcx>,
|
||||||
state: Option<Box<DebugSolver<I>>>,
|
state: Option<Box<DebugSolver<I>>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -229,36 +231,36 @@ impl<I: Interner> WipProbeStep<I> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// FIXME: Genericize this impl.
|
impl<Infcx: InferCtxtLike<Interner = I>, I: Interner> ProofTreeBuilder<Infcx> {
|
||||||
impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
fn new(state: impl Into<DebugSolver<I>>) -> ProofTreeBuilder<Infcx> {
|
||||||
fn new(state: impl Into<DebugSolver<TyCtxt<'tcx>>>) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
ProofTreeBuilder { state: Some(Box::new(state.into())), _infcx: PhantomData }
|
||||||
ProofTreeBuilder { state: Some(Box::new(state.into())) }
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn opt_nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(
|
fn opt_nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> Option<T>) -> Self {
|
||||||
&self,
|
|
||||||
state: impl FnOnce() -> Option<T>,
|
|
||||||
) -> Self {
|
|
||||||
ProofTreeBuilder {
|
ProofTreeBuilder {
|
||||||
state: self.state.as_ref().and_then(|_| Some(state()?.into())).map(Box::new),
|
state: self.state.as_ref().and_then(|_| Some(state()?.into())).map(Box::new),
|
||||||
|
_infcx: PhantomData,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(&self, state: impl FnOnce() -> T) -> Self {
|
fn nested<T: Into<DebugSolver<I>>>(&self, state: impl FnOnce() -> T) -> Self {
|
||||||
ProofTreeBuilder { state: self.state.as_ref().map(|_| Box::new(state().into())) }
|
ProofTreeBuilder {
|
||||||
|
state: self.state.as_ref().map(|_| Box::new(state().into())),
|
||||||
|
_infcx: PhantomData,
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn as_mut(&mut self) -> Option<&mut DebugSolver<TyCtxt<'tcx>>> {
|
fn as_mut(&mut self) -> Option<&mut DebugSolver<I>> {
|
||||||
self.state.as_deref_mut()
|
self.state.as_deref_mut()
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
pub fn take_and_enter_probe(&mut self) -> ProofTreeBuilder<Infcx> {
|
||||||
let mut nested = ProofTreeBuilder { state: self.state.take() };
|
let mut nested = ProofTreeBuilder { state: self.state.take(), _infcx: PhantomData };
|
||||||
nested.enter_probe();
|
nested.enter_probe();
|
||||||
nested
|
nested
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn finalize(self) -> Option<inspect::GoalEvaluation<TyCtxt<'tcx>>> {
|
pub fn finalize(self) -> Option<inspect::GoalEvaluation<I>> {
|
||||||
match *self.state? {
|
match *self.state? {
|
||||||
DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
|
DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
|
||||||
Some(wip_goal_evaluation.finalize())
|
Some(wip_goal_evaluation.finalize())
|
||||||
@ -267,21 +269,19 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn new_maybe_root(
|
pub fn new_maybe_root(generate_proof_tree: GenerateProofTree) -> ProofTreeBuilder<Infcx> {
|
||||||
generate_proof_tree: GenerateProofTree,
|
|
||||||
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|
||||||
match generate_proof_tree {
|
match generate_proof_tree {
|
||||||
GenerateProofTree::No => ProofTreeBuilder::new_noop(),
|
GenerateProofTree::No => ProofTreeBuilder::new_noop(),
|
||||||
GenerateProofTree::Yes => ProofTreeBuilder::new_root(),
|
GenerateProofTree::Yes => ProofTreeBuilder::new_root(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn new_root() -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
pub fn new_root() -> ProofTreeBuilder<Infcx> {
|
||||||
ProofTreeBuilder::new(DebugSolver::Root)
|
ProofTreeBuilder::new(DebugSolver::Root)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn new_noop() -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
pub fn new_noop() -> ProofTreeBuilder<Infcx> {
|
||||||
ProofTreeBuilder { state: None }
|
ProofTreeBuilder { state: None, _infcx: PhantomData }
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn is_noop(&self) -> bool {
|
pub fn is_noop(&self) -> bool {
|
||||||
@ -290,10 +290,10 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
|
|
||||||
pub(in crate::solve) fn new_goal_evaluation(
|
pub(in crate::solve) fn new_goal_evaluation(
|
||||||
&mut self,
|
&mut self,
|
||||||
goal: Goal<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
|
goal: Goal<I, I::Predicate>,
|
||||||
orig_values: &[ty::GenericArg<'tcx>],
|
orig_values: &[I::GenericArg],
|
||||||
kind: solve::GoalEvaluationKind,
|
kind: solve::GoalEvaluationKind,
|
||||||
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
) -> ProofTreeBuilder<Infcx> {
|
||||||
self.opt_nested(|| match kind {
|
self.opt_nested(|| match kind {
|
||||||
solve::GoalEvaluationKind::Root => Some(WipGoalEvaluation {
|
solve::GoalEvaluationKind::Root => Some(WipGoalEvaluation {
|
||||||
uncanonicalized_goal: goal,
|
uncanonicalized_goal: goal,
|
||||||
@ -306,8 +306,8 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
|
|
||||||
pub fn new_canonical_goal_evaluation(
|
pub fn new_canonical_goal_evaluation(
|
||||||
&mut self,
|
&mut self,
|
||||||
goal: CanonicalInput<TyCtxt<'tcx>>,
|
goal: CanonicalInput<I>,
|
||||||
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
) -> ProofTreeBuilder<Infcx> {
|
||||||
self.nested(|| WipCanonicalGoalEvaluation {
|
self.nested(|| WipCanonicalGoalEvaluation {
|
||||||
goal,
|
goal,
|
||||||
kind: None,
|
kind: None,
|
||||||
@ -318,12 +318,13 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
|
|
||||||
pub fn finalize_canonical_goal_evaluation(
|
pub fn finalize_canonical_goal_evaluation(
|
||||||
&mut self,
|
&mut self,
|
||||||
tcx: TyCtxt<'tcx>,
|
tcx: I,
|
||||||
) -> Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>> {
|
) -> Option<I::CanonicalGoalEvaluationStepRef> {
|
||||||
self.as_mut().map(|this| match this {
|
self.as_mut().map(|this| match this {
|
||||||
DebugSolver::CanonicalGoalEvaluation(evaluation) => {
|
DebugSolver::CanonicalGoalEvaluation(evaluation) => {
|
||||||
let final_revision = mem::take(&mut evaluation.final_revision).unwrap();
|
let final_revision = mem::take(&mut evaluation.final_revision).unwrap();
|
||||||
let final_revision = &*tcx.arena.alloc(final_revision.finalize());
|
let final_revision =
|
||||||
|
tcx.intern_canonical_goal_evaluation_step(final_revision.finalize());
|
||||||
let kind = WipCanonicalGoalEvaluationKind::Interned { final_revision };
|
let kind = WipCanonicalGoalEvaluationKind::Interned { final_revision };
|
||||||
assert_eq!(evaluation.kind.replace(kind), None);
|
assert_eq!(evaluation.kind.replace(kind), None);
|
||||||
final_revision
|
final_revision
|
||||||
@ -334,7 +335,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
|
|
||||||
pub fn canonical_goal_evaluation(
|
pub fn canonical_goal_evaluation(
|
||||||
&mut self,
|
&mut self,
|
||||||
canonical_goal_evaluation: ProofTreeBuilder<TyCtxt<'tcx>>,
|
canonical_goal_evaluation: ProofTreeBuilder<Infcx>,
|
||||||
) {
|
) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match (this, *canonical_goal_evaluation.state.unwrap()) {
|
match (this, *canonical_goal_evaluation.state.unwrap()) {
|
||||||
@ -350,10 +351,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn canonical_goal_evaluation_kind(
|
pub fn canonical_goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind<I>) {
|
||||||
&mut self,
|
|
||||||
kind: WipCanonicalGoalEvaluationKind<TyCtxt<'tcx>>,
|
|
||||||
) {
|
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match this {
|
match this {
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||||
@ -364,7 +362,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<TyCtxt<'tcx>>) {
|
pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<Infcx>) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match this {
|
match this {
|
||||||
DebugSolver::Root => *this = *goal_evaluation.state.unwrap(),
|
DebugSolver::Root => *this = *goal_evaluation.state.unwrap(),
|
||||||
@ -378,9 +376,9 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
|
|
||||||
pub fn new_goal_evaluation_step(
|
pub fn new_goal_evaluation_step(
|
||||||
&mut self,
|
&mut self,
|
||||||
var_values: CanonicalVarValues<'tcx>,
|
var_values: ty::CanonicalVarValues<I>,
|
||||||
instantiated_goal: QueryInput<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
|
instantiated_goal: QueryInput<I, I::Predicate>,
|
||||||
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
) -> ProofTreeBuilder<Infcx> {
|
||||||
self.nested(|| WipCanonicalGoalEvaluationStep {
|
self.nested(|| WipCanonicalGoalEvaluationStep {
|
||||||
var_values: var_values.var_values.to_vec(),
|
var_values: var_values.var_values.to_vec(),
|
||||||
instantiated_goal,
|
instantiated_goal,
|
||||||
@ -394,7 +392,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<TyCtxt<'tcx>>) {
|
pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<Infcx>) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match (this, *goal_evaluation_step.state.unwrap()) {
|
match (this, *goal_evaluation_step.state.unwrap()) {
|
||||||
(
|
(
|
||||||
@ -408,7 +406,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn add_var_value<T: Into<ty::GenericArg<'tcx>>>(&mut self, arg: T) {
|
pub fn add_var_value<T: Into<I::GenericArg>>(&mut self, arg: T) {
|
||||||
match self.as_mut() {
|
match self.as_mut() {
|
||||||
None => {}
|
None => {}
|
||||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||||
@ -435,7 +433,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<TyCtxt<'tcx>>) {
|
pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<I>) {
|
||||||
match self.as_mut() {
|
match self.as_mut() {
|
||||||
None => {}
|
None => {}
|
||||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||||
@ -446,11 +444,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn probe_final_state(
|
pub fn probe_final_state(&mut self, infcx: &Infcx, max_input_universe: ty::UniverseIndex) {
|
||||||
&mut self,
|
|
||||||
infcx: &InferCtxt<'tcx>,
|
|
||||||
max_input_universe: ty::UniverseIndex,
|
|
||||||
) {
|
|
||||||
match self.as_mut() {
|
match self.as_mut() {
|
||||||
None => {}
|
None => {}
|
||||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||||
@ -469,24 +463,24 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
|
|
||||||
pub fn add_normalizes_to_goal(
|
pub fn add_normalizes_to_goal(
|
||||||
&mut self,
|
&mut self,
|
||||||
infcx: &InferCtxt<'tcx>,
|
infcx: &Infcx,
|
||||||
max_input_universe: ty::UniverseIndex,
|
max_input_universe: ty::UniverseIndex,
|
||||||
goal: Goal<TyCtxt<'tcx>, ty::NormalizesTo<'tcx>>,
|
goal: Goal<I, ty::NormalizesTo<I>>,
|
||||||
) {
|
) {
|
||||||
self.add_goal(
|
self.add_goal(
|
||||||
infcx,
|
infcx,
|
||||||
max_input_universe,
|
max_input_universe,
|
||||||
GoalSource::Misc,
|
GoalSource::Misc,
|
||||||
goal.with(infcx.tcx, goal.predicate),
|
goal.with(infcx.interner(), goal.predicate),
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn add_goal(
|
pub fn add_goal(
|
||||||
&mut self,
|
&mut self,
|
||||||
infcx: &InferCtxt<'tcx>,
|
infcx: &Infcx,
|
||||||
max_input_universe: ty::UniverseIndex,
|
max_input_universe: ty::UniverseIndex,
|
||||||
source: GoalSource,
|
source: GoalSource,
|
||||||
goal: Goal<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
|
goal: Goal<I, I::Predicate>,
|
||||||
) {
|
) {
|
||||||
match self.as_mut() {
|
match self.as_mut() {
|
||||||
None => {}
|
None => {}
|
||||||
@ -505,9 +499,9 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
|
|
||||||
pub(crate) fn record_impl_args(
|
pub(crate) fn record_impl_args(
|
||||||
&mut self,
|
&mut self,
|
||||||
infcx: &InferCtxt<'tcx>,
|
infcx: &Infcx,
|
||||||
max_input_universe: ty::UniverseIndex,
|
max_input_universe: ty::UniverseIndex,
|
||||||
impl_args: ty::GenericArgsRef<'tcx>,
|
impl_args: I::GenericArgs,
|
||||||
) {
|
) {
|
||||||
match self.as_mut() {
|
match self.as_mut() {
|
||||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||||
@ -540,7 +534,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn finish_probe(mut self) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
pub fn finish_probe(mut self) -> ProofTreeBuilder<Infcx> {
|
||||||
match self.as_mut() {
|
match self.as_mut() {
|
||||||
None => {}
|
None => {}
|
||||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||||
@ -555,7 +549,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||||||
self
|
self
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn query_result(&mut self, result: QueryResult<TyCtxt<'tcx>>) {
|
pub fn query_result(&mut self, result: QueryResult<I>) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match this {
|
match this {
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||||
|
@ -3,6 +3,7 @@ use std::mem;
|
|||||||
use rustc_data_structures::fx::{FxHashMap, FxHashSet};
|
use rustc_data_structures::fx::{FxHashMap, FxHashSet};
|
||||||
use rustc_index::Idx;
|
use rustc_index::Idx;
|
||||||
use rustc_index::IndexVec;
|
use rustc_index::IndexVec;
|
||||||
|
use rustc_infer::infer::InferCtxt;
|
||||||
use rustc_middle::dep_graph::dep_kinds;
|
use rustc_middle::dep_graph::dep_kinds;
|
||||||
use rustc_middle::traits::solve::CacheData;
|
use rustc_middle::traits::solve::CacheData;
|
||||||
use rustc_middle::traits::solve::EvaluationCache;
|
use rustc_middle::traits::solve::EvaluationCache;
|
||||||
@ -261,10 +262,10 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
|
|||||||
&mut self,
|
&mut self,
|
||||||
tcx: TyCtxt<'tcx>,
|
tcx: TyCtxt<'tcx>,
|
||||||
input: CanonicalInput<TyCtxt<'tcx>>,
|
input: CanonicalInput<TyCtxt<'tcx>>,
|
||||||
inspect: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
|
inspect: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
|
||||||
mut prove_goal: impl FnMut(
|
mut prove_goal: impl FnMut(
|
||||||
&mut Self,
|
&mut Self,
|
||||||
&mut ProofTreeBuilder<TyCtxt<'tcx>>,
|
&mut ProofTreeBuilder<InferCtxt<'tcx>>,
|
||||||
) -> QueryResult<TyCtxt<'tcx>>,
|
) -> QueryResult<TyCtxt<'tcx>>,
|
||||||
) -> QueryResult<TyCtxt<'tcx>> {
|
) -> QueryResult<TyCtxt<'tcx>> {
|
||||||
self.check_invariants();
|
self.check_invariants();
|
||||||
@ -426,7 +427,7 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
|
|||||||
tcx: TyCtxt<'tcx>,
|
tcx: TyCtxt<'tcx>,
|
||||||
input: CanonicalInput<TyCtxt<'tcx>>,
|
input: CanonicalInput<TyCtxt<'tcx>>,
|
||||||
available_depth: Limit,
|
available_depth: Limit,
|
||||||
inspect: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
|
inspect: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
|
||||||
) -> Option<QueryResult<TyCtxt<'tcx>>> {
|
) -> Option<QueryResult<TyCtxt<'tcx>>> {
|
||||||
let CacheData { result, proof_tree, additional_depth, encountered_overflow } = self
|
let CacheData { result, proof_tree, additional_depth, encountered_overflow } = self
|
||||||
.global_cache(tcx)
|
.global_cache(tcx)
|
||||||
@ -473,11 +474,11 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
|
|||||||
&mut self,
|
&mut self,
|
||||||
tcx: TyCtxt<'tcx>,
|
tcx: TyCtxt<'tcx>,
|
||||||
input: CanonicalInput<TyCtxt<'tcx>>,
|
input: CanonicalInput<TyCtxt<'tcx>>,
|
||||||
inspect: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
|
inspect: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
|
||||||
prove_goal: &mut F,
|
prove_goal: &mut F,
|
||||||
) -> StepResult<TyCtxt<'tcx>>
|
) -> StepResult<TyCtxt<'tcx>>
|
||||||
where
|
where
|
||||||
F: FnMut(&mut Self, &mut ProofTreeBuilder<TyCtxt<'tcx>>) -> QueryResult<TyCtxt<'tcx>>,
|
F: FnMut(&mut Self, &mut ProofTreeBuilder<InferCtxt<'tcx>>) -> QueryResult<TyCtxt<'tcx>>,
|
||||||
{
|
{
|
||||||
let result = prove_goal(self, inspect);
|
let result = prove_goal(self, inspect);
|
||||||
let stack_entry = self.pop_stack();
|
let stack_entry = self.pop_stack();
|
||||||
|
@ -132,7 +132,14 @@ pub trait GenericArgs<I: Interner<GenericArgs = Self>>:
|
|||||||
}
|
}
|
||||||
|
|
||||||
pub trait Predicate<I: Interner<Predicate = Self>>:
|
pub trait Predicate<I: Interner<Predicate = Self>>:
|
||||||
Copy + Debug + Hash + Eq + TypeSuperVisitable<I> + TypeSuperFoldable<I> + Flags
|
Copy
|
||||||
|
+ Debug
|
||||||
|
+ Hash
|
||||||
|
+ Eq
|
||||||
|
+ TypeSuperVisitable<I>
|
||||||
|
+ TypeSuperFoldable<I>
|
||||||
|
+ Flags
|
||||||
|
+ UpcastFrom<I, ty::NormalizesTo<I>>
|
||||||
{
|
{
|
||||||
fn is_coinductive(self, interner: I) -> bool;
|
fn is_coinductive(self, interner: I) -> bool;
|
||||||
}
|
}
|
||||||
|
@ -3,6 +3,7 @@ use std::fmt::Debug;
|
|||||||
use std::hash::Hash;
|
use std::hash::Hash;
|
||||||
use std::ops::Deref;
|
use std::ops::Deref;
|
||||||
|
|
||||||
|
use crate::fold::TypeFoldable;
|
||||||
use crate::inherent::*;
|
use crate::inherent::*;
|
||||||
use crate::ir_print::IrPrint;
|
use crate::ir_print::IrPrint;
|
||||||
use crate::solve::inspect::CanonicalGoalEvaluationStep;
|
use crate::solve::inspect::CanonicalGoalEvaluationStep;
|
||||||
@ -90,7 +91,7 @@ pub trait Interner:
|
|||||||
type PlaceholderRegion: PlaceholderLike;
|
type PlaceholderRegion: PlaceholderLike;
|
||||||
|
|
||||||
// Predicates
|
// Predicates
|
||||||
type ParamEnv: Copy + Debug + Hash + Eq;
|
type ParamEnv: Copy + Debug + Hash + Eq + TypeFoldable<Self>;
|
||||||
type Predicate: Predicate<Self>;
|
type Predicate: Predicate<Self>;
|
||||||
type Clause: Clause<Self>;
|
type Clause: Clause<Self>;
|
||||||
type Clauses: Copy + Debug + Hash + Eq + TypeSuperVisitable<Self> + Flags;
|
type Clauses: Copy + Debug + Hash + Eq + TypeSuperVisitable<Self> + Flags;
|
||||||
@ -114,15 +115,18 @@ pub trait Interner:
|
|||||||
) -> (ty::TraitRef<Self>, Self::OwnItemArgs);
|
) -> (ty::TraitRef<Self>, Self::OwnItemArgs);
|
||||||
|
|
||||||
fn mk_args(self, args: &[Self::GenericArg]) -> Self::GenericArgs;
|
fn mk_args(self, args: &[Self::GenericArg]) -> Self::GenericArgs;
|
||||||
|
|
||||||
fn mk_args_from_iter(self, args: impl Iterator<Item = Self::GenericArg>) -> Self::GenericArgs;
|
fn mk_args_from_iter(self, args: impl Iterator<Item = Self::GenericArg>) -> Self::GenericArgs;
|
||||||
|
|
||||||
fn check_and_mk_args(
|
fn check_and_mk_args(
|
||||||
self,
|
self,
|
||||||
def_id: Self::DefId,
|
def_id: Self::DefId,
|
||||||
args: impl IntoIterator<Item: Into<Self::GenericArg>>,
|
args: impl IntoIterator<Item: Into<Self::GenericArg>>,
|
||||||
) -> Self::GenericArgs;
|
) -> Self::GenericArgs;
|
||||||
|
|
||||||
|
fn intern_canonical_goal_evaluation_step(
|
||||||
|
self,
|
||||||
|
step: CanonicalGoalEvaluationStep<Self>,
|
||||||
|
) -> Self::CanonicalGoalEvaluationStepRef;
|
||||||
|
|
||||||
fn parent(self, def_id: Self::DefId) -> Self::DefId;
|
fn parent(self, def_id: Self::DefId) -> Self::DefId;
|
||||||
|
|
||||||
fn recursion_limit(self) -> usize;
|
fn recursion_limit(self) -> usize;
|
||||||
|
Loading…
x
Reference in New Issue
Block a user