snapshot (first working implementation of parttern matching from level 2

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index d282e3d708f7bf406093625284cce6d548f744a8..767aa3d1579d80ae74ff5ddda550f00251fe75c8 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -510,6 +510,7 @@ EXTEND
     [ "90" NONA
       [ id = IDENT -> return_term loc (Ident (id, None))
       | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
+      | s = CSYMBOL -> return_term loc (Symbol (s, 0))
       | u = URI -> return_term loc (Uri (u, None))
       | n = NUMBER -> prerr_endline "number"; return_term loc (Num (n, 0))
       | IMPLICIT -> return_term loc (Implicit)
@@ -565,25 +566,26 @@ EXTEND
     [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
   ];
   notation: [
-    [ IDENT "notation";
-      p1 = level1_pattern;
+    [ p1 = level1_pattern;
       assoc = OPT associativity; prec = OPT precedence;
       IDENT "for"; p2 = level2_pattern ->
         (p1, assoc, prec, p2)
     ]
   ];
   interpretation: [
-    [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
-      t = level3_term ->
-        ()
+    [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
+        (s, args, t)
     ]
   ];
 (* }}} *)
 (* {{{ Top-level phrases *)
   phrase: [
     [ IDENT "print"; p2 = level2_pattern; SYMBOL "." -> Print p2
-    | (l1, assoc, prec, l2) = notation; SYMBOL "." ->
+    | IDENT "notation"; (l1, assoc, prec, l2) = notation; SYMBOL "." ->
         Notation (l1, assoc, prec, l2)
+    | IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." ->
+        Interpretation ((symbol, args), l3)
+    | IDENT "render"; u = URI; SYMBOL "." -> Render (UriManager.uri_of_string u)
     ]
   ];
 (* }}} *)