diff options
Diffstat (limited to 'isabelle-dump/src/main.rs')
-rw-r--r-- | isabelle-dump/src/main.rs | 71 |
1 files changed, 71 insertions, 0 deletions
diff --git a/isabelle-dump/src/main.rs b/isabelle-dump/src/main.rs new file mode 100644 index 0000000..891108f --- /dev/null +++ b/isabelle-dump/src/main.rs @@ -0,0 +1,71 @@ +use std::io::{self, BufRead, Write}; + +use lrlex::lrlex_mod; +use lrpar::lrpar_mod; + +#[derive(Debug)] +pub enum Isabelle { + Symbol(String), + Text(String), +} + + +lrlex_mod!("calc.l"); +lrpar_mod!("calc.y"); + + +symbolmacro::make_symbols!(); + + +fn main() { + // Get the `LexerDef` for the `calc` language. + let lexerdef = calc_l::lexerdef(); + let stdin = io::stdin(); + loop { + io::stdout().flush().ok(); + match stdin.lock().lines().next() { + Some(Ok(ref l)) => { + if l.trim().is_empty() { + println!(""); + continue; + } + let lexer = lexerdef.lexer(l); + let (res, errs) = calc_y::parse(&lexer); + for e in errs { + eprintln!( + "{}", + e.pp(&lexer, &calc_y::token_epp) + ); + } + match res { + Some(r) => { + //eprintln!("Result: {:?}", r); + let rendered = r + .unwrap() + .iter() + .map(|token| match token { + Isabelle::Text(ref t) => + t, + Isabelle::Symbol(name) => + symbol(name) + .unwrap_or_else(|| { + Box::leak( + format!("\\<{}>", name) + .into() + ) + }) + }) + .collect::<Vec<&str>>() + .join(""); + println!("{}", rendered); + } + _ => { + eprintln!("could not parse file (probably spurious \\, <, or >)"); + std::process::exit(1); + } + } + } + _ => break, + } + } +} |