Skip to content

proof tree nits #112835

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Jun 20, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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 @@ -866,17 +841,20 @@ 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)?;
}
ecx.eq(param_env, candidate_ty, ty)?;
ecx.add_item_bounds_for_hidden_type(candidate_key, param_env, 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