new experimental cic textual parser: checkin

[helm.git] / helm / ocaml / cic_disambiguation / logic_notation.ml

diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml
new file mode 100644 (file)
index 0000000..35ce4b9
--- /dev/null
+++ b/helm/ocaml/cic_disambiguation/logic_notation.ml
@@ -0,0 +1,23 @@
+open Ast
+open Parser
+
+EXTEND
+  term: LEVEL "add"
+    [
+      [ t1 = term; SYMBOL "∨"; t2 = term ->
+          return_term loc (Appl [Ident ("or", []); t1; t2])
+      ]
+    ];
+  term: LEVEL "mult"
+    [
+      [ t1 = term; SYMBOL "∧"; t2 = term ->
+        return_term loc (Appl [Ident ("and", []); t1; t2])
+      ]
+    ];
+  term: LEVEL "inv"
+    [
+      [ SYMBOL "¬"; t = term ->
+        return_term loc (Appl [Ident ("not", []); t])
+      ]
+    ];
+END