initial commit

1 files changed, 54 insertions, 0 deletions

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;