new experimental cic textual parser: checkin

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

diff --git a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml
new file mode 100644 (file)
index 0000000..044f8ae
--- /dev/null
+++ b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml
@@ -0,0 +1,36 @@
+
+let debug = false
+let debug_print = if debug then prerr_endline else ignore
+
+let loc = (0, 0)
+
+let expand_unicode_macro macro =
+  debug_print (Printf.sprintf "Expanding macro '%s' ..." macro);
+  let expansion = Macro.expand macro in
+  <:expr< $str:expansion$ >>
+
+let _ =
+  Quotation.add "unicode"
+    (Quotation.ExAst (expand_unicode_macro, (fun _ -> assert false)))
+
+open Pa_extend
+
+EXTEND
+  symbol: FIRST
+    [
+      [ x = UIDENT; q = QUOTATION ->
+        let (quotation, arg) =
+          let pos = String.index q ':' in
+          (String.sub q 0 pos,
+           String.sub q (pos + 1) (String.length q - pos - 1))
+        in
+        debug_print (Printf.sprintf "QUOTATION = %s; ARG = %s" quotation arg);
+        if quotation = "unicode" then
+          let text = TXtok (loc, x, expand_unicode_macro arg) in
+          {used = []; text = text; styp = STlid (loc, "string")}
+        else
+          assert false
+      ]
+    ];
+END
+