use anstyle::{AnsiColor, Style};
use std::fmt::Write as _;
use std::io::Write;
use tess::analysis::{AnalysisProgress, AnalysisProgressPhase, AnalysisReport};
const SUCCESS_STYLE: Style = AnsiColor::Green.on_default().bold();
const FAILURE_STYLE: Style = AnsiColor::Red.on_default().bold();
const INCONCLUSIVE_STYLE: Style = AnsiColor::Yellow.on_default().bold();
const WARNING_STYLE: Style = AnsiColor::Yellow.on_default().bold();
const COUNTEREXAMPLE_STYLE: Style = AnsiColor::Red.on_default().bold();
const DETAIL_STYLE: Style = AnsiColor::BrightBlack.on_default();
pub(crate) struct ProgressRenderer<W: Write> {
writer: W,
line_open: bool,
writable: bool,
}
impl<W: Write> ProgressRenderer<W> {
pub(crate) const fn new(writer: W) -> Self {
Self {
writer,
line_open: false,
writable: true,
}
}
pub(crate) fn update(&mut self, progress: &AnalysisProgress) {
if !self.writable {
return;
}
if matches!(&progress.phase, AnalysisProgressPhase::Finished { .. }) {
self.finish();
return;
}
let line = render_progress(progress);
if write!(self.writer, "\r{line}")
.and_then(|()| self.writer.flush())
.is_err()
{
self.writable = false;
self.line_open = false;
} else {
self.line_open = true;
}
}
pub(crate) fn finish(&mut self) {
if !self.writable || !self.line_open {
return;
}
if self
.writer
.write_all(b"\n")
.and_then(|()| self.writer.flush())
.is_err()
{
self.writable = false;
}
self.line_open = false;
}
}
fn render_progress(progress: &AnalysisProgress) -> String {
let prefix = format!(
"verifying [{}/{}] {}",
progress.position, progress.total, progress.invariant
);
match &progress.phase {
AnalysisProgressPhase::Planning => format!("{prefix} · planning"),
AnalysisProgressPhase::Solving => format!("{prefix} · trying exact solver"),
AnalysisProgressPhase::Evaluating {
evaluated,
evaluation_limit,
planned_evaluations,
} => {
let percentage = progress_percentage(*evaluated, *evaluation_limit);
let mut line = format!(
"{prefix} · {}/{} evaluations ({percentage}%)",
format_count(*evaluated),
format_count(*evaluation_limit)
);
if planned_evaluations > evaluation_limit {
let _ = write!(line, " · {} planned", format_count(*planned_evaluations));
}
line
}
_ => prefix,
}
}
fn progress_percentage(evaluated: usize, evaluation_limit: usize) -> usize {
if evaluation_limit == 0 {
return 0;
}
let percentage = u128::try_from(evaluated).expect("usize fits in u128") * 100
/ u128::try_from(evaluation_limit).expect("usize fits in u128");
usize::try_from(percentage.min(100)).expect("a percentage fits in usize")
}
fn format_count(count: usize) -> String {
let digits = count.to_string();
let mut grouped = String::with_capacity(digits.len() + digits.len() / 3);
for (index, digit) in digits.chars().enumerate() {
if index > 0 && (digits.len() - index) % 3 == 0 {
grouped.push(',');
}
grouped.push(digit);
}
grouped
}
pub(crate) fn render_report(report: &AnalysisReport, color: bool) -> String {
let plain = report.render_text();
if !color {
return plain;
}
let mut output = String::with_capacity(plain.len());
for line in plain.split_inclusive('\n') {
let (content, newline) = line
.strip_suffix('\n')
.map_or((line, ""), |content| (content, "\n"));
if let Some(style) = line_style(content) {
let _ = write!(output, "{style}{content}{style:#}");
} else {
output.push_str(content);
}
output.push_str(newline);
}
output
}
fn line_style(line: &str) -> Option<Style> {
if line.starts_with("✓ ") {
Some(SUCCESS_STYLE)
} else if line.starts_with("✗ ") {
Some(FAILURE_STYLE)
} else if line.starts_with("? ") {
Some(INCONCLUSIVE_STYLE)
} else if line.starts_with("! ") {
Some(WARNING_STYLE)
} else if line.starts_with(" counterexample ·") {
Some(COUNTEREXAMPLE_STYLE)
} else if line.starts_with(" proved for all inputs")
|| line.starts_with(" satisfying input found")
|| line.starts_with(" no satisfying input exists")
|| line.starts_with(" counterexample found")
|| line.starts_with(" failed")
|| line.starts_with(" inconclusive")
|| line.starts_with(" reason ·")
|| line.starts_with(" reason ·")
{
Some(DETAIL_STYLE)
} else {
None
}
}
#[cfg(test)]
mod tests {
use super::*;
fn progress(phase: AnalysisProgressPhase) -> AnalysisProgress {
AnalysisProgress {
invariant: "층간소음검토는_여러결론허용".into(),
position: 3,
total: 5,
phase,
}
}
#[test]
fn existential_summaries_use_detail_styling() {
assert_eq!(
line_style(" satisfying input found · after 2 evaluations"),
Some(DETAIL_STYLE)
);
assert_eq!(
line_style(" no satisfying input exists · all 3 combinations checked"),
Some(DETAIL_STYLE)
);
}
#[test]
fn progress_renderer_rewrites_one_plain_line_and_finishes_it() {
let mut output = Vec::new();
{
let mut renderer = ProgressRenderer::new(&mut output);
renderer.update(&progress(AnalysisProgressPhase::Planning));
renderer.update(&progress(AnalysisProgressPhase::Solving));
renderer.update(&progress(AnalysisProgressPhase::Evaluating {
evaluated: 42_000,
evaluation_limit: 100_000,
planned_evaluations: 2_478_669_167_520,
}));
renderer.update(&progress(AnalysisProgressPhase::Finished {
evaluated: 100_000,
}));
}
let output = String::from_utf8(output).unwrap();
assert!(output.starts_with("\rverifying [3/5] 층간소음검토는_여러결론허용 · planning"));
assert!(output.contains("· trying exact solver"));
assert!(output.contains("· 42,000/100,000 evaluations (42%) · 2,478,669,167,520 planned"));
assert!(output.ends_with('\n'));
assert!(!output.contains("\u{1b}["));
}
#[test]
fn progress_percentage_does_not_overflow() {
let line = render_progress(&progress(AnalysisProgressPhase::Evaluating {
evaluated: usize::MAX,
evaluation_limit: usize::MAX,
planned_evaluations: usize::MAX,
}));
assert!(line.ends_with("evaluations (100%)"), "{line}");
}
}