nordic-dev.net/rust
nordic-dev.net/rust
2
0
Fork 0
mirror of https://github.com/rust-lang/rust.git synced 2025-04-28 02:57:37 +00:00
Code Issues Packages Projects Releases Wiki Activity

refactor proof tree formatting

Browse Source
This commit is contained in:
lcnr 2023-07-11 13:34:55 +02:00
parent 33a2c2487a
commit f446894804
2 changed files with 63 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
compiler/rustc_middle/src/traits/solve/inspect.rs
View File

@ -32,7 +32,7 @@ pub enum GoalEvaluationKind<'tcx> {
}
impl Debug for GoalEvaluation<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter { f, on_newline: true }.format_goal_evaluation(self)
ProofTreeFormatter::new(f).format_goal_evaluation(self)
}
}
@ -43,7 +43,7 @@ pub struct AddedGoalsEvaluation<'tcx> {
}
impl Debug for AddedGoalsEvaluation<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter { f, on_newline: true }.format_nested_goal_evaluation(self)
ProofTreeFormatter::new(f).format_nested_goal_evaluation(self)
}
}
@ -58,7 +58,7 @@ pub struct GoalEvaluationStep<'tcx> {
}
impl Debug for GoalEvaluationStep<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter { f, on_newline: true }.format_evaluation_step(self)
ProofTreeFormatter::new(f).format_evaluation_step(self)
}
}
@ -78,6 +78,6 @@ pub enum CandidateKind<'tcx> {
}
impl Debug for GoalCandidate<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter { f, on_newline: true }.format_candidate(self)
ProofTreeFormatter::new(f).format_candidate(self)
}
}

112
compiler/rustc_middle/src/traits/solve/inspect/format.rs
View File

@ -1,11 +1,19 @@
use super::*;
pub(super) struct ProofTreeFormatter<'a, 'b> {
pub(super) f: &'a mut (dyn Write + 'b),
pub(super) on_newline: bool,
f: &'a mut (dyn Write + 'b),
}
impl Write for ProofTreeFormatter<'_, '_> {
/// A formatter which adds 4 spaces of identation 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,
}
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 {
@ -19,49 +27,52 @@ impl Write for ProofTreeFormatter<'_, '_> {
}
}
impl ProofTreeFormatter<'_, '_> {
fn nested(&mut self) -> ProofTreeFormatter<'_, '_> {
ProofTreeFormatter { f: self, on_newline: true }
impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
pub(super) fn new(f: &'a mut (dyn Write + 'b)) -> Self {
ProofTreeFormatter { f }
}
fn nested<F, R>(&mut self, func: F) -> R
where
F: FnOnce(&mut ProofTreeFormatter<'_, '_>) -> R,
{
func(&mut ProofTreeFormatter { f: &mut Indentor { f: self.f, on_newline: true } })
}
pub(super) fn format_goal_evaluation(&mut self, goal: &GoalEvaluation<'_>) -> std::fmt::Result {
let f = &mut *self.f;
let goal_text = match goal.is_normalizes_to_hack {
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
IsNormalizesToHack::No => "GOAL",
};
writeln!(f, "{}: {:?}", goal_text, goal.uncanonicalized_goal,)?;
writeln!(f, "CANONICALIZED: {:?}", goal.canonicalized_goal)?;
writeln!(self.f, "{}: {:?}", goal_text, goal.uncanonicalized_goal)?;
writeln!(self.f, "CANONICALIZED: {:?}", goal.canonicalized_goal)?;
match &goal.kind {
GoalEvaluationKind::CacheHit(CacheHit::Global) => {
writeln!(f, "GLOBAL CACHE HIT: {:?}", goal.result)
writeln!(self.f, "GLOBAL CACHE HIT: {:?}", goal.result)
}
GoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
writeln!(f, "PROVISIONAL CACHE HIT: {:?}", goal.result)
writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", goal.result)
}
GoalEvaluationKind::Uncached { revisions } => {
for (n, step) in revisions.iter().enumerate() {
let f = &mut *self.f;
writeln!(f, "REVISION {n}: {:?}", step.result)?;
let mut f = self.nested();
f.format_evaluation_step(step)?;
writeln!(self.f, "REVISION {n}: {:?}", step.result)?;
self.nested(|this| this.format_evaluation_step(step))?;
}
let f = &mut *self.f;
writeln!(f, "RESULT: {:?}", goal.result)
writeln!(self.f, "RESULT: {:?}", goal.result)
}
}?;
if goal.returned_goals.len() > 0 {
let f = &mut *self.f;
writeln!(f, "NESTED GOALS ADDED TO CALLER: [")?;
let mut f = self.nested();
for goal in goal.returned_goals.iter() {
writeln!(f, "ADDED GOAL: {:?},", goal)?;
}
writeln!(self.f, "NESTED GOALS ADDED TO CALLER: [")?;
self.nested(|this| {
for goal in goal.returned_goals.iter() {
writeln!(this.f, "ADDED GOAL: {:?},", goal)?;
}
Ok(())
})?;
writeln!(self.f, "]")?;
}
@ -72,58 +83,53 @@ impl ProofTreeFormatter<'_, '_> {
&mut self,
evaluation_step: &GoalEvaluationStep<'_>,
) -> std::fmt::Result {
let f = &mut *self.f;
writeln!(f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
for candidate in &evaluation_step.candidates {
let mut f = self.nested();
f.format_candidate(candidate)?;
self.nested(|this| this.format_candidate(candidate))?;
}
for nested_goal_evaluation in &evaluation_step.nested_goal_evaluations {
let mut f = self.nested();
f.format_nested_goal_evaluation(nested_goal_evaluation)?;
for nested in &evaluation_step.nested_goal_evaluations {
self.nested(|this| this.format_nested_goal_evaluation(nested))?;
}
Ok(())
}
pub(super) fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result {
let f = &mut *self.f;
match &candidate.kind {
CandidateKind::NormalizedSelfTyAssembly => {
writeln!(f, "NORMALIZING SELF TY FOR ASSEMBLY:")
writeln!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
}
CandidateKind::Candidate { name, result } => {
writeln!(f, "CANDIDATE {}: {:?}", name, result)
writeln!(self.f, "CANDIDATE {}: {:?}", name, result)
}
}?;
let mut f = self.nested();
for candidate in &candidate.candidates {
f.format_candidate(candidate)?;
}
for nested_evaluations in &candidate.nested_goal_evaluations {
f.format_nested_goal_evaluation(nested_evaluations)?;
}
Ok(())
self.nested(|this| {
for candidate in &candidate.candidates {
this.format_candidate(candidate)?;
}
for nested in &candidate.nested_goal_evaluations {
this.format_nested_goal_evaluation(nested)?;
}
Ok(())
})
}
pub(super) fn format_nested_goal_evaluation(
&mut self,
nested_goal_evaluation: &AddedGoalsEvaluation<'_>,
) -> std::fmt::Result {
let f = &mut *self.f;
writeln!(f, "TRY_EVALUATE_ADDED_GOALS: {:?}", nested_goal_evaluation.result)?;
writeln!(self.f, "TRY_EVALUATE_ADDED_GOALS: {:?}", nested_goal_evaluation.result)?;
for (n, revision) in nested_goal_evaluation.evaluations.iter().enumerate() {
let f = &mut *self.f;
writeln!(f, "REVISION {n}")?;
let mut f = self.nested();
for goal_evaluation in revision {
f.format_goal_evaluation(goal_evaluation)?;
}
writeln!(self.f, "REVISION {n}")?;
self.nested(|this| {
for goal_evaluation in revision {
this.format_goal_evaluation(goal_evaluation)?;
}
Ok(())
})?;
}
Ok(())