Implement display logic for readback errors

This commit is contained in:
imaqtkatt 2024-01-24 11:14:29 -03:00
parent 9cd2bac3d0
commit 08cd61c069
8 changed files with 115 additions and 16 deletions

View File

@ -11,7 +11,7 @@ use std::time::Instant;
use term::{
book_to_nets, net_to_term,
term_to_net::{HvmcNames, Labels},
Book, DefId, DefNames, Name, ReadbackError, Term,
Book, DefId, DefNames, Name, Term,
};
pub mod hvmc_net;
@ -20,6 +20,8 @@ pub mod term;
pub use term::load_book::load_file_to_book;
use crate::term::net_to_term::ReadbackErrors;
pub fn check_book(mut book: Book) -> Result<(), String> {
// TODO: Do the checks without having to do full compilation
compile_book(&mut book, Opts::light())?;
@ -107,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", errors) },
if errors.is_empty() { "".to_string() } else { format!("Invalid readback:\n{}\n", errors) },
res_term.display(&book.def_names)
);
}
@ -256,7 +258,7 @@ impl std::fmt::Display for Warning {
pub struct RunInfo {
pub stats: RunStats,
pub readback_errors: Vec<ReadbackError>,
pub readback_errors: ReadbackErrors,
pub net: Net,
}

View File

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

View File

@ -1,19 +1,20 @@
use super::{
term_to_net::Labels,
transform::encode_strs::{SCONS, SNIL},
var_id_to_name, Book, DefId, MatchNum, Name, Op, Tag, Term, Val,
var_id_to_name, Book, DefId, DefNames, 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};
// TODO: Display scopeless lambdas as such
/// Converts an Interaction-INet to a Lambda Calculus term
pub fn net_to_term(net: &INet, book: &Book, labels: &Labels, linear: bool) -> (Term, Vec<ReadbackError>) {
pub fn net_to_term(net: &INet, book: &Book, labels: &Labels, linear: bool) -> (Term, ReadbackErrors) {
let mut reader = Reader {
net,
labels,
@ -47,7 +48,7 @@ pub fn net_to_term(net: &INet, book: &Book, labels: &Labels, linear: bool) -> (T
reader.resugar_adts(&mut term);
(term, reader.errors)
(term, ReadbackErrors::new(reader.errors, book.def_names.clone()))
}
#[derive(Debug)]
@ -58,7 +59,7 @@ pub enum ReadbackError {
InvalidBind,
InvalidAdt,
InvalidAdtMatch,
InvalidStrTerm,
InvalidStrTerm(Term),
}
struct Reader<'a> {
@ -292,10 +293,11 @@ impl<'a> Reader<'a> {
}
Term::Var { nam } => recover_string_cons(str_term, Term::Var { nam: nam.clone() }),
Term::Lam { tag, bod, .. } if *tag == Tag::string() => {
recover_string_cons(str_term, rd.resugar_string(bod));
rd.error(ReadbackError::InvalidStrTerm)
let string = rd.resugar_string(bod);
recover_string_cons(str_term, string.clone());
rd.error(ReadbackError::InvalidStrTerm(string))
},
_ => rd.error(ReadbackError::InvalidStrTerm),
_ => rd.error(ReadbackError::InvalidStrTerm(*arg.clone())),
}
}
Term::App { fun, arg, .. } => {
@ -315,7 +317,7 @@ impl<'a> Reader<'a> {
| Term::Opx { .. }
| Term::Match { .. }
| Term::Ref { .. }
| Term::Era => rd.error(ReadbackError::InvalidStrTerm),
| Term::Era => rd.error(ReadbackError::InvalidStrTerm(term.clone())),
}
}
let mut str = Term::Str { val: String::new() };
@ -722,3 +724,81 @@ impl<'a> Reader<'a> {
T::default()
}
}
/// A structure that implements display logic for Readback Errors.
pub struct ReadbackErrors(Vec<ReadbackError>, DefNames);
impl ReadbackErrors {
pub fn new(errs: Vec<ReadbackError>, def_names: DefNames) -> Self {
Self(errs, def_names)
}
pub fn is_empty(&self) -> bool {
self.0.is_empty()
}
}
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 {
match self {
ReadbackError::InvalidNumericMatch => true,
ReadbackError::ReachedRoot => true,
ReadbackError::Cyclic => true,
ReadbackError::InvalidBind => true,
ReadbackError::InvalidAdt => true,
ReadbackError::InvalidAdtMatch => true,
ReadbackError::InvalidStrTerm(..) => false,
}
}
}
impl PartialEq for ReadbackError {
fn eq(&self, other: &Self) -> bool {
core::mem::discriminant(self) == core::mem::discriminant(other)
}
}
impl Eq for ReadbackError {}
impl std::hash::Hash for ReadbackError {
fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
core::mem::discriminant(self).hash(state);
}
}

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{}", info.readback_errors, res.display(&def_names))
format!("Invalid readback:\n{}\n{}", info.readback_errors, 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{}", errors, term.display(&book.def_names)))
Ok(format!("Invalid readback:\n{}\n{}", errors, term.display(&book.def_names)))
}
})
}

View File

@ -0,0 +1 @@
Main = (SCons (*, 4) (SCons * SNil))

View File

@ -2,5 +2,6 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/readback_lnet/bad_net.hvm
---
Invalid readback: [ReachedRoot]
Invalid readback:
Reached Root
*

View File

@ -2,5 +2,11 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/nested_str.hvm
---
Invalid readback: [InvalidStrTerm, InvalidStrTerm, InvalidStrTerm, InvalidStrTerm, InvalidStrTerm]
Invalid readback:
Invalid String Character value '"a"'
Invalid String Character value '"bc"'
Invalid String Character value '"ab"'
Invalid String Character value '"ab"'
Invalid String Character value '"cd"'
(((SCons "a" SNil), (SCons 97 (SCons "bc" SNil))), ((SCons "ab" (SCons 99 SNil)), (SCons "ab" (SCons "cd" SNil))))

View File

@ -0,0 +1,9 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/wrong_string.hvm
---
Invalid readback:
Invalid String Character value '(*, 4)'
Invalid String Character value '*'
""