summaryrefslogtreecommitdiff
path: root/isabelle-dump/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--isabelle-dump/src/calc.l5
-rw-r--r--isabelle-dump/src/calc.y54
-rw-r--r--isabelle-dump/src/main.rs71
3 files changed, 130 insertions, 0 deletions
diff --git a/isabelle-dump/src/calc.l b/isabelle-dump/src/calc.l
new file mode 100644
index 0000000..2bf98dc
--- /dev/null
+++ b/isabelle-dump/src/calc.l
@@ -0,0 +1,5 @@
+%%
+\\ "AOPEN"
+< "LT"
+<[^\\<>]+> "NAME"
+[^<\\][^\\]* "TEXT"
diff --git a/isabelle-dump/src/calc.y b/isabelle-dump/src/calc.y
new file mode 100644
index 0000000..2dd3bd3
--- /dev/null
+++ b/isabelle-dump/src/calc.y
@@ -0,0 +1,54 @@
+%start AbbrList
+
+%%
+
+AbbrList -> Result<Vec<Isabelle>, ()>:
+ Text { Ok(vec![Isabelle::Text($1?)]) }
+ | Abbr { Ok(vec![Isabelle::Symbol($1?)]) }
+ | AbbrList Abbr
+ {
+ let mut $1 = $1?;
+ $1.push(Isabelle::Symbol($2?));
+ Ok($1)
+ }
+ | AbbrList Text
+ {
+ let mut $1 = $1?;
+ $1.push(Isabelle::Text($2?));
+ Ok($1)
+ }
+ ;
+
+Abbr -> Result<String, ()>:
+ 'AOPEN' Name { Ok($2?) }
+ ;
+
+Text -> Result<String, ()>:
+ 'TEXT'
+ {
+ let v = $1.map_err(|_| ())?;
+ Ok($lexer.span_str(v.span()).to_string())
+ }
+ | 'AOPEN'
+ {
+ //let v = $2.map_err(|_| ())?;
+ Ok("\\".to_string())
+ }
+ | 'LT'
+ {
+ //let v = $2.map_err(|_| ())?;
+ Ok("<".to_string()) //format!("<{}", $lexer.span_str(v.span())))
+ }
+ ;
+
+Name -> Result<String, ()>:
+ 'NAME'
+ {
+ let v = $1.map_err(|_| ())?;
+ let name = $lexer.span_str(v.span());
+ Ok(name[1..name.len()-1].to_string())
+ }
+ ;
+%%
+
+use crate::Isabelle;
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,
+ }
+ }
+}