Rollup merge of #122197 - lcnr:proof-tree-braces, r=BoxyUwU
inspect formatter: add braces
This makes it easier to hide subtrees when looking through proof trees. Looking at the proof tree for `usize: Clone`:
nightly:
```
ROOT GOAL: Goal { predicate: Binder { value: TraitPredicate(<usize as std::clone::Clone>, polarity:Positive), bound_vars: [] }, param_env: ParamEnv { caller_bounds: [], reveal: UserFacing } }
GOAL: Canonical { value: QueryInput { goal: Goal { predicate: Binder { value: TraitPredicate(<usize as std::clone::Clone>, polarity:Positive), bound_vars: [] }, param_env: ParamEnv { caller_bounds: [], reveal: UserFacing } }, anchor: Bind(DefId(0:5 ~ main[8e4b]::main)), predefined_opaques_in_body: PredefinedOpaques(PredefinedOpaquesData { opaque_types: [] }) }, max_universe: U0, variables: [] }
REVISION 0
INSTANTIATED: QueryInput { goal: Goal { predicate: Binder { value: TraitPredicate(<usize as std::clone::Clone>, polarity:Positive), bound_vars: [] }, param_env: ParamEnv { caller_bounds: [], reveal: UserFacing } }, anchor: Bind(DefId(0:5 ~ main[8e4b]::main)), predefined_opaques_in_body: PredefinedOpaques(PredefinedOpaquesData { opaque_types: [] }) }
ROOT RESULT: Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [] })
CANDIDATE Impl(DefId(2:30665 ~ core[a9f5]::clone::impls::{impl#5})): Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [] })
TRY_EVALUATE_ADDED_GOALS: Ok(Yes)
ITERATION 0
CANDIDATE constituent tys: Err(NoSolution)
NORMALIZING SELF TY FOR ASSEMBLY:
NORMALIZING SELF TY FOR ASSEMBLY:
RESULT: Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [] })
```
with this PR:
```
ROOT GOAL: Goal { predicate: Binder { value: TraitPredicate(<usize as std::clone::Clone>, polarity:Positive), bound_vars: [] }, param_env: ParamEnv { caller_bounds: [], reveal: UserFacing } } {
GOAL: Canonical { value: QueryInput { goal: Goal { predicate: Binder { value: TraitPredicate(<usize as std::clone::Clone>, polarity:Positive), bound_vars: [] }, param_env: ParamEnv { caller_bounds: [], reveal: UserFacing } }, anchor: Bind(DefId(0:5 ~ main[4f74]::main)), predefined_opaques_in_body: PredefinedOpaques(PredefinedOpaquesData { opaque_types: [] }) }, max_universe: U0, variables: [] }
REVISION 0: {
INSTANTIATED: QueryInput { goal: Goal { predicate: Binder { value: TraitPredicate(<usize as std::clone::Clone>, polarity:Positive), bound_vars: [] }, param_env: ParamEnv { caller_bounds: [], reveal: UserFacing } }, anchor: Bind(DefId(0:5 ~ main[4f74]::main)), predefined_opaques_in_body: PredefinedOpaques(PredefinedOpaquesData { opaque_types: [] }) }
ROOT RESULT: Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [] }) {
CANDIDATE Impl(DefId(2:30468 ~ core[d1d7]::clone::impls::{impl#5})): Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [] }) {
TRY_EVALUATE_ADDED_GOALS: Ok(Yes)
ITERATION 0 {}
}
CANDIDATE constituent tys: Err(NoSolution) {}
NORMALIZING SELF TY FOR ASSEMBLY: {}
NORMALIZING SELF TY FOR ASSEMBLY: {}
}
}
RESULT: Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [] })
}
```
r? `@BoxyUwU`
This commit is contained in:
Matthias Krüger
GitHub
commit
bf939fcb99
1 changed files with 30 additions and 17 deletions
|
|
@ -4,22 +4,31 @@ pub(super) struct ProofTreeFormatter<'a, 'b> {
|
|||
f: &'a mut (dyn Write + 'b),
|
||||
}
|
||||
|
||||
enum IndentorState {
|
||||
StartWithNewline,
|
||||
OnNewline,
|
||||
Inline,
|
||||
}
|
||||
|
||||
/// A formatter which adds 4 spaces of indentation to its input before
|
||||
/// passing it on to its nested formatter.
|
||||
///
|
||||
/// We can use this for arbitrary levels of indentation by nesting it.
|
||||
struct Indentor<'a, 'b> {
|
||||
f: &'a mut (dyn Write + 'b),
|
||||
on_newline: bool,
|
||||
state: IndentorState,
|
||||
}
|
||||
|
||||
impl Write for Indentor<'_, '_> {
|
||||
fn write_str(&mut self, s: &str) -> std::fmt::Result {
|
||||
for line in s.split_inclusive('\n') {
|
||||
if self.on_newline {
|
||||
self.f.write_str(" ")?;
|
||||
match self.state {
|
||||
IndentorState::StartWithNewline => self.f.write_str("\n ")?,
|
||||
IndentorState::OnNewline => self.f.write_str(" ")?,
|
||||
IndentorState::Inline => {}
|
||||
}
|
||||
self.on_newline = line.ends_with('\n');
|
||||
self.state =
|
||||
if line.ends_with('\n') { IndentorState::OnNewline } else { IndentorState::Inline };
|
||||
self.f.write_str(line)?;
|
||||
}
|
||||
|
||||
|
|
@ -32,11 +41,15 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
|||
ProofTreeFormatter { f }
|
||||
}
|
||||
|
||||
fn nested<F, R>(&mut self, func: F) -> R
|
||||
fn nested<F>(&mut self, func: F) -> std::fmt::Result
|
||||
where
|
||||
F: FnOnce(&mut ProofTreeFormatter<'_, '_>) -> R,
|
||||
F: FnOnce(&mut ProofTreeFormatter<'_, '_>) -> std::fmt::Result,
|
||||
{
|
||||
func(&mut ProofTreeFormatter { f: &mut Indentor { f: self.f, on_newline: true } })
|
||||
write!(self.f, " {{")?;
|
||||
func(&mut ProofTreeFormatter {
|
||||
f: &mut Indentor { f: self.f, state: IndentorState::StartWithNewline },
|
||||
})?;
|
||||
writeln!(self.f, "}}")
|
||||
}
|
||||
|
||||
pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
|
||||
|
|
@ -47,7 +60,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
|||
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
|
||||
},
|
||||
};
|
||||
writeln!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
|
||||
write!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
|
||||
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))
|
||||
}
|
||||
|
||||
|
|
@ -69,7 +82,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
|||
}
|
||||
CanonicalGoalEvaluationKind::Evaluation { revisions } => {
|
||||
for (n, step) in revisions.iter().enumerate() {
|
||||
writeln!(self.f, "REVISION {n}")?;
|
||||
write!(self.f, "REVISION {n}")?;
|
||||
self.nested(|this| this.format_evaluation_step(step))?;
|
||||
}
|
||||
writeln!(self.f, "RESULT: {:?}", eval.result)
|
||||
|
|
@ -88,25 +101,25 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
|||
pub(super) fn format_probe(&mut self, probe: &Probe<'_>) -> std::fmt::Result {
|
||||
match &probe.kind {
|
||||
ProbeKind::Root { result } => {
|
||||
writeln!(self.f, "ROOT RESULT: {result:?}")
|
||||
write!(self.f, "ROOT RESULT: {result:?}")
|
||||
}
|
||||
ProbeKind::NormalizedSelfTyAssembly => {
|
||||
writeln!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
|
||||
write!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
|
||||
}
|
||||
ProbeKind::UnsizeAssembly => {
|
||||
writeln!(self.f, "ASSEMBLING CANDIDATES FOR UNSIZING:")
|
||||
write!(self.f, "ASSEMBLING CANDIDATES FOR UNSIZING:")
|
||||
}
|
||||
ProbeKind::UpcastProjectionCompatibility => {
|
||||
writeln!(self.f, "PROBING FOR PROJECTION COMPATIBILITY FOR UPCASTING:")
|
||||
write!(self.f, "PROBING FOR PROJECTION COMPATIBILITY FOR UPCASTING:")
|
||||
}
|
||||
ProbeKind::CommitIfOk => {
|
||||
writeln!(self.f, "COMMIT_IF_OK:")
|
||||
write!(self.f, "COMMIT_IF_OK:")
|
||||
}
|
||||
ProbeKind::MiscCandidate { name, result } => {
|
||||
writeln!(self.f, "CANDIDATE {name}: {result:?}")
|
||||
write!(self.f, "CANDIDATE {name}: {result:?}")
|
||||
}
|
||||
ProbeKind::TraitCandidate { source, result } => {
|
||||
writeln!(self.f, "CANDIDATE {source:?}: {result:?}")
|
||||
write!(self.f, "CANDIDATE {source:?}: {result:?}")
|
||||
}
|
||||
}?;
|
||||
|
||||
|
|
@ -137,7 +150,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
|
|||
writeln!(self.f, "TRY_EVALUATE_ADDED_GOALS: {:?}", added_goals_evaluation.result)?;
|
||||
|
||||
for (n, iterations) in added_goals_evaluation.evaluations.iter().enumerate() {
|
||||
writeln!(self.f, "ITERATION {n}")?;
|
||||
write!(self.f, "ITERATION {n}")?;
|
||||
self.nested(|this| {
|
||||
for goal_evaluation in iterations {
|
||||
this.format_goal_evaluation(goal_evaluation)?;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue