1
Fork 0

inspect formatter: add braces

This commit is contained in:
lcnr 2024-03-08 17:03:04 +01:00
parent 42825768b1
commit 309d85b06f

View file

@ -4,22 +4,31 @@ pub(super) struct ProofTreeFormatter<'a, 'b> {
f: &'a mut (dyn Write + 'b), f: &'a mut (dyn Write + 'b),
} }
enum IndentorState {
StartWithNewline,
OnNewline,
Inline,
}
/// A formatter which adds 4 spaces of indentation to its input before /// A formatter which adds 4 spaces of indentation to its input before
/// passing it on to its nested formatter. /// passing it on to its nested formatter.
/// ///
/// We can use this for arbitrary levels of indentation by nesting it. /// We can use this for arbitrary levels of indentation by nesting it.
struct Indentor<'a, 'b> { struct Indentor<'a, 'b> {
f: &'a mut (dyn Write + 'b), f: &'a mut (dyn Write + 'b),
on_newline: bool, state: IndentorState,
} }
impl Write for Indentor<'_, '_> { impl Write for Indentor<'_, '_> {
fn write_str(&mut self, s: &str) -> std::fmt::Result { fn write_str(&mut self, s: &str) -> std::fmt::Result {
for line in s.split_inclusive('\n') { for line in s.split_inclusive('\n') {
if self.on_newline { match self.state {
self.f.write_str(" ")?; 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)?; self.f.write_str(line)?;
} }
@ -32,11 +41,15 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
ProofTreeFormatter { f } ProofTreeFormatter { f }
} }
fn nested<F, R>(&mut self, func: F) -> R fn nested<F>(&mut self, func: F) -> std::fmt::Result
where 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 { 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", 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)) self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))
} }
@ -69,7 +82,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
} }
CanonicalGoalEvaluationKind::Evaluation { revisions } => { CanonicalGoalEvaluationKind::Evaluation { revisions } => {
for (n, step) in revisions.iter().enumerate() { 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))?; self.nested(|this| this.format_evaluation_step(step))?;
} }
writeln!(self.f, "RESULT: {:?}", eval.result) 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 { pub(super) fn format_probe(&mut self, probe: &Probe<'_>) -> std::fmt::Result {
match &probe.kind { match &probe.kind {
ProbeKind::Root { result } => { ProbeKind::Root { result } => {
writeln!(self.f, "ROOT RESULT: {result:?}") write!(self.f, "ROOT RESULT: {result:?}")
} }
ProbeKind::NormalizedSelfTyAssembly => { ProbeKind::NormalizedSelfTyAssembly => {
writeln!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:") write!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
} }
ProbeKind::UnsizeAssembly => { ProbeKind::UnsizeAssembly => {
writeln!(self.f, "ASSEMBLING CANDIDATES FOR UNSIZING:") write!(self.f, "ASSEMBLING CANDIDATES FOR UNSIZING:")
} }
ProbeKind::UpcastProjectionCompatibility => { ProbeKind::UpcastProjectionCompatibility => {
writeln!(self.f, "PROBING FOR PROJECTION COMPATIBILITY FOR UPCASTING:") write!(self.f, "PROBING FOR PROJECTION COMPATIBILITY FOR UPCASTING:")
} }
ProbeKind::CommitIfOk => { ProbeKind::CommitIfOk => {
writeln!(self.f, "COMMIT_IF_OK:") write!(self.f, "COMMIT_IF_OK:")
} }
ProbeKind::MiscCandidate { name, result } => { ProbeKind::MiscCandidate { name, result } => {
writeln!(self.f, "CANDIDATE {name}: {result:?}") write!(self.f, "CANDIDATE {name}: {result:?}")
} }
ProbeKind::TraitCandidate { source, 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)?; writeln!(self.f, "TRY_EVALUATE_ADDED_GOALS: {:?}", added_goals_evaluation.result)?;
for (n, iterations) in added_goals_evaluation.evaluations.iter().enumerate() { for (n, iterations) in added_goals_evaluation.evaluations.iter().enumerate() {
writeln!(self.f, "ITERATION {n}")?; write!(self.f, "ITERATION {n}")?;
self.nested(|this| { self.nested(|this| {
for goal_evaluation in iterations { for goal_evaluation in iterations {
this.format_goal_evaluation(goal_evaluation)?; this.format_goal_evaluation(goal_evaluation)?;