Skip to content

Commit

Permalink
Auto merge of rust-lang#112835 - lcnr:proof-tree-nits, r=BoxyUwU
Browse files Browse the repository at this point in the history
proof tree nits

r? `@BoxyUwU`
  • Loading branch information
bors committed Jun 20, 2023
2 parents a34cead + e4b171a commit 4651421
Show file tree
Hide file tree
Showing 10 changed files with 310 additions and 295 deletions.
6 changes: 0 additions & 6 deletions compiler/rustc_middle/src/traits/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -991,9 +991,3 @@ pub enum DefiningAnchor {
/// Used to catch type mismatch errors when handling opaque types.
Error,
}

#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, HashStable)]
pub enum IsNormalizesToHack {
Yes,
No,
}
6 changes: 6 additions & 0 deletions compiler/rustc_middle/src/traits/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -228,3 +228,9 @@ impl<'tcx> TypeVisitable<TyCtxt<'tcx>> for PredefinedOpaques<'tcx> {
self.opaque_types.visit_with(visitor)
}
}

#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, HashStable)]
pub enum IsNormalizesToHack {
Yes,
No,
}
8 changes: 6 additions & 2 deletions compiler/rustc_middle/src/traits/solve/inspect.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
use super::{CanonicalInput, Certainty, Goal, NoSolution, QueryInput, QueryResult};
use crate::{traits::IsNormalizesToHack, ty};
use super::{
CanonicalInput, Certainty, Goal, IsNormalizesToHack, NoSolution, QueryInput, QueryResult,
};
use crate::ty;
use format::ProofTreeFormatter;
use std::fmt::{Debug, Write};

Expand All @@ -22,6 +24,7 @@ pub struct GoalEvaluation<'tcx> {

pub result: QueryResult<'tcx>,
}

#[derive(Eq, PartialEq, Hash, HashStable)]
pub enum GoalEvaluationKind<'tcx> {
CacheHit(CacheHit),
Expand Down Expand Up @@ -65,6 +68,7 @@ pub struct GoalCandidate<'tcx> {
pub candidates: Vec<GoalCandidate<'tcx>>,
pub kind: CandidateKind<'tcx>,
}

#[derive(Eq, PartialEq, Debug, Hash, HashStable)]
pub enum CandidateKind<'tcx> {
/// Probe entered when normalizing the self ty during candidate assembly
Expand Down
14 changes: 5 additions & 9 deletions compiler/rustc_trait_selection/src/solve/alias_relate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -110,12 +110,11 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
direction: ty::AliasRelationDirection,
invert: Invert,
) -> QueryResult<'tcx> {
self.probe(
self.probe(|r| CandidateKind::Candidate { name: "normalizes-to".into(), result: *r }).enter(
|ecx| {
ecx.normalizes_to_inner(param_env, alias, other, direction, invert)?;
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
},
|r| CandidateKind::Candidate { name: "normalizes-to".into(), result: *r },
)
}

Expand Down Expand Up @@ -157,7 +156,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
alias_rhs: ty::AliasTy<'tcx>,
direction: ty::AliasRelationDirection,
) -> QueryResult<'tcx> {
self.probe(
self.probe(|r| CandidateKind::Candidate { name: "substs relate".into(), result: *r }).enter(
|ecx| {
match direction {
ty::AliasRelationDirection::Equate => {
Expand All @@ -170,7 +169,6 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {

ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
},
|r| CandidateKind::Candidate { name: "substs relate".into(), result: *r },
)
}

Expand All @@ -181,8 +179,8 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
rhs: ty::Term<'tcx>,
direction: ty::AliasRelationDirection,
) -> QueryResult<'tcx> {
self.probe(
|ecx| {
self.probe(|r| CandidateKind::Candidate { name: "bidir normalizes-to".into(), result: *r })
.enter(|ecx| {
ecx.normalizes_to_inner(
param_env,
lhs.to_alias_ty(ecx.tcx()).unwrap(),
Expand All @@ -198,8 +196,6 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
Invert::Yes,
)?;
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
},
|r| CandidateKind::Candidate { name: "bidir normalizes-to".into(), result: *r },
)
})
}
}
8 changes: 3 additions & 5 deletions compiler/rustc_trait_selection/src/solve/assembly/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -337,8 +337,8 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
return
};

let normalized_self_candidates: Result<_, NoSolution> = self.probe(
|ecx| {
let normalized_self_candidates: Result<_, NoSolution> =
self.probe(|_| CandidateKind::NormalizedSelfTyAssembly).enter(|ecx| {
ecx.with_incremented_depth(
|ecx| {
let result = ecx.evaluate_added_goals_and_make_canonical_response(
Expand Down Expand Up @@ -368,9 +368,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
Ok(ecx.assemble_and_evaluate_candidates(goal))
},
)
},
|_| CandidateKind::NormalizedSelfTyAssembly,
);
});

if let Ok(normalized_self_candidates) = normalized_self_candidates {
candidates.extend(normalized_self_candidates);
Expand Down
46 changes: 12 additions & 34 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,10 @@ use rustc_infer::traits::ObligationCause;
use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind};
use rustc_middle::traits::solve::inspect::{self, CandidateKind};
use rustc_middle::traits::solve::{
CanonicalInput, CanonicalResponse, Certainty, MaybeCause, PredefinedOpaques,
PredefinedOpaquesData, QueryResult,
CanonicalInput, CanonicalResponse, Certainty, IsNormalizesToHack, MaybeCause,
PredefinedOpaques, PredefinedOpaquesData, QueryResult,
};
use rustc_middle::traits::{DefiningAnchor, IsNormalizesToHack};
use rustc_middle::traits::DefiningAnchor;
use rustc_middle::ty::{
self, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable, TypeVisitable,
TypeVisitableExt, TypeVisitor,
Expand All @@ -30,6 +30,7 @@ use super::SolverMode;
use super::{search_graph::SearchGraph, Goal};

mod canonical;
mod probe;

pub struct EvalCtxt<'a, 'tcx> {
/// The inference context that backs (mostly) inference and placeholder terms
Expand Down Expand Up @@ -529,32 +530,6 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}

impl<'tcx> EvalCtxt<'_, 'tcx> {
/// `probe_kind` is only called when proof tree building is enabled so it can be
/// as expensive as necessary to output the desired information.
pub(super) fn probe<T>(
&mut self,
f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> T,
probe_kind: impl FnOnce(&T) -> CandidateKind<'tcx>,
) -> T {
let mut ecx = EvalCtxt {
infcx: self.infcx,
var_values: self.var_values,
predefined_opaques_in_body: self.predefined_opaques_in_body,
max_input_universe: self.max_input_universe,
search_graph: self.search_graph,
nested_goals: self.nested_goals.clone(),
tainted: self.tainted,
inspect: self.inspect.new_goal_candidate(),
};
let r = self.infcx.probe(|_| f(&mut ecx));
if !self.inspect.is_noop() {
let cand_kind = probe_kind(&r);
ecx.inspect.candidate_kind(cand_kind);
self.inspect.goal_candidate(ecx.inspect);
}
r
}

pub(super) fn tcx(&self) -> TyCtxt<'tcx> {
self.infcx.tcx
}
Expand Down Expand Up @@ -868,8 +843,12 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
if candidate_key.def_id != key.def_id {
continue;
}
values.extend(self.probe(
|ecx| {
values.extend(
self.probe(|r| CandidateKind::Candidate {
name: "opaque type storage".into(),
result: *r,
})
.enter(|ecx| {
for (a, b) in std::iter::zip(candidate_key.substs, key.substs) {
ecx.eq(param_env, a, b)?;
}
Expand All @@ -881,9 +860,8 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
candidate_ty,
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
},
|r| CandidateKind::Candidate { name: "opaque type storage".into(), result: *r },
));
}),
);
}
values
}
Expand Down
47 changes: 47 additions & 0 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
use super::EvalCtxt;
use rustc_middle::traits::solve::inspect;
use std::marker::PhantomData;

pub(in crate::solve) struct ProbeCtxt<'me, 'a, 'tcx, F, T> {
ecx: &'me mut EvalCtxt<'a, 'tcx>,
probe_kind: F,
_result: PhantomData<T>,
}

impl<'tcx, F, T> ProbeCtxt<'_, '_, 'tcx, F, T>
where
F: FnOnce(&T) -> inspect::CandidateKind<'tcx>,
{
pub(in crate::solve) fn enter(self, f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> T) -> T {
let ProbeCtxt { ecx: outer_ecx, probe_kind, _result } = self;

let mut nested_ecx = EvalCtxt {
infcx: outer_ecx.infcx,
var_values: outer_ecx.var_values,
predefined_opaques_in_body: outer_ecx.predefined_opaques_in_body,
max_input_universe: outer_ecx.max_input_universe,
search_graph: outer_ecx.search_graph,
nested_goals: outer_ecx.nested_goals.clone(),
tainted: outer_ecx.tainted,
inspect: outer_ecx.inspect.new_goal_candidate(),
};
let r = nested_ecx.infcx.probe(|_| f(&mut nested_ecx));
if !outer_ecx.inspect.is_noop() {
let cand_kind = probe_kind(&r);
nested_ecx.inspect.candidate_kind(cand_kind);
outer_ecx.inspect.goal_candidate(nested_ecx.inspect);
}
r
}
}

impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
/// `probe_kind` is only called when proof tree building is enabled so it can be
/// as expensive as necessary to output the desired information.
pub(in crate::solve) fn probe<F, T>(&mut self, probe_kind: F) -> ProbeCtxt<'_, 'a, 'tcx, F, T>
where
F: FnOnce(&T) -> inspect::CandidateKind<'tcx>,
{
ProbeCtxt { ecx: self, probe_kind, _result: PhantomData }
}
}
Loading

0 comments on commit 4651421

Please sign in to comment.