Refactor readback display

This commit is contained in:
imaqtkatt 2024-01-24 14:09:11 -03:00
parent 08cd61c069
commit 312c3c54b2
5 changed files with 56 additions and 49 deletions

View File

@ -109,7 +109,7 @@ pub fn run_book(
let (res_term, errors) = net_to_term(&net, book, labels, linear);
println!(
"{}{}\n---------------------------------------",
if errors.is_empty() { "".to_string() } else { format!("Invalid readback:\n{}\n", errors) },
if errors.is_empty() { "".to_string() } else { format!("Invalid readback:\n{}\n", errors.display(&book.def_names)) },
res_term.display(&book.def_names)
);
}

View File

@ -119,7 +119,7 @@ fn main() {
if readback_errors.is_empty() {
"".to_string()
} else {
format!("Invalid readback:\n{}\n", readback_errors)
format!("Invalid readback:\n{}\n", readback_errors.display(&def_names))
},
res_term.display(&def_names)
);

View File

@ -2,7 +2,10 @@ use std::fmt::{self, Display};
use crate::term::Name;
use super::{Book, DefId, DefNames, Definition, MatchNum, Op, Pattern, Rule, Tag, Term, Type};
use super::{
net_to_term::{ReadbackError, ReadbackErrors},
Book, DefId, DefNames, Definition, MatchNum, Op, Pattern, Rule, Tag, Term, Type,
};
macro_rules! display {
($($x:tt)*) => {
@ -215,3 +218,45 @@ where
Ok(())
}
}
impl ReadbackErrors {
pub fn display<'a>(&'a self, def_names: &'a DefNames) -> impl fmt::Display + '_ {
use std::collections::HashMap;
DisplayFn(move |f| {
let mut err_counts = HashMap::new();
for err in &self.0 {
if err.can_count() {
*err_counts.entry(err).or_insert(0) += 1;
} else {
writeln!(f, "{}", err.display(def_names))?;
}
}
for (err, count) in err_counts {
write!(f, "{}", err.display(def_names))?;
if count > 1 {
writeln!(f, " with {} occurrences", count)?;
}
}
Ok(())
})
}
}
impl ReadbackError {
pub fn display<'a>(&'a self, def_names: &'a DefNames) -> impl Display + '_ {
DisplayFn(move |f| match self {
ReadbackError::InvalidNumericMatch => write!(f, "Invalid Numeric Match"),
ReadbackError::ReachedRoot => write!(f, "Reached Root"),
ReadbackError::Cyclic => write!(f, "Cyclic Term"),
ReadbackError::InvalidBind => write!(f, "Invalid Bind"),
ReadbackError::InvalidAdt => write!(f, "Invalid Adt"),
ReadbackError::InvalidAdtMatch => write!(f, "Invalid Adt Match"),
ReadbackError::InvalidStrTerm(term) => {
write!(f, "Invalid String Character value '{}'", term.display(def_names))
}
})
}
}

View File

@ -1,13 +1,12 @@
use super::{
term_to_net::Labels,
transform::encode_strs::{SCONS, SNIL},
var_id_to_name, Book, DefId, DefNames, MatchNum, Name, Op, Tag, Term, Val,
var_id_to_name, Book, DefId, MatchNum, Name, Op, Tag, Term, Val,
};
use crate::{
net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT},
term::Pattern,
};
use core::fmt;
use hvmc::run::Loc;
use indexmap::IndexSet;
use std::collections::{HashMap, HashSet};
@ -48,7 +47,7 @@ pub fn net_to_term(net: &INet, book: &Book, labels: &Labels, linear: bool) -> (T
reader.resugar_adts(&mut term);
(term, ReadbackErrors::new(reader.errors, book.def_names.clone()))
(term, ReadbackErrors::new(reader.errors))
}
#[derive(Debug)]
@ -726,11 +725,11 @@ impl<'a> Reader<'a> {
}
/// A structure that implements display logic for Readback Errors.
pub struct ReadbackErrors(Vec<ReadbackError>, DefNames);
pub struct ReadbackErrors(pub Vec<ReadbackError>);
impl ReadbackErrors {
pub fn new(errs: Vec<ReadbackError>, def_names: DefNames) -> Self {
Self(errs, def_names)
pub fn new(errs: Vec<ReadbackError>) -> Self {
Self(errs)
}
pub fn is_empty(&self) -> bool {
@ -738,45 +737,8 @@ impl ReadbackErrors {
}
}
impl fmt::Display for ReadbackErrors {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
let mut err_counts = HashMap::new();
for err in &self.0 {
if err.can_count() {
*err_counts.entry(err).or_insert(0) += 1;
} else {
err.pretty(f, &self.1)?;
writeln!(f)?;
}
}
for (err, count) in err_counts {
err.pretty(f, &self.1)?;
if count > 1 {
write!(f, " with {} occurrences", count)?;
}
}
Ok(())
}
}
impl ReadbackError {
fn pretty(&self, f: &mut fmt::Formatter<'_>, def_names: &DefNames) -> fmt::Result {
match self {
ReadbackError::InvalidNumericMatch => write!(f, "Invalid Numeric Match"),
ReadbackError::ReachedRoot => write!(f, "Reached Root"),
ReadbackError::Cyclic => write!(f, "Cyclic Term"),
ReadbackError::InvalidBind => write!(f, "Invalid Bind"),
ReadbackError::InvalidAdt => write!(f, "Invalid Adt"),
ReadbackError::InvalidAdtMatch => write!(f, "Invalid Adt Match"),
ReadbackError::InvalidStrTerm(term) => {
write!(f, "Invalid String Character value '{}'", term.display(def_names))
}
}
}
fn can_count(&self) -> bool {
pub fn can_count(&self) -> bool {
match self {
ReadbackError::InvalidNumericMatch => true,
ReadbackError::ReachedRoot => true,

View File

@ -117,7 +117,7 @@ fn run_file() {
let res = if info.readback_errors.is_empty() {
res.display(&def_names).to_string()
} else {
format!("Invalid readback:\n{}\n{}", info.readback_errors, res.display(&def_names))
format!("Invalid readback:\n{}\n{}", info.readback_errors.display(&def_names), res.display(&def_names))
};
Ok(res)
})
@ -133,7 +133,7 @@ fn readback_lnet() {
if errors.is_empty() {
Ok(term.display(&book.def_names).to_string())
} else {
Ok(format!("Invalid readback:\n{}\n{}", errors, term.display(&book.def_names)))
Ok(format!("Invalid readback:\n{}\n{}", errors.display(&book.def_names), term.display(&book.def_names)))
}
})
}