implemented transformations on top of notation code

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

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 056e595e7ed8b8fc5eaf3867a47a1072e53058f9..fae3df93d4eb3eea3005a63646ddf68e437af6f3 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -364,7 +364,7 @@ EXTEND
     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
   ];
   notation: [
-    [ s = QSTRING;
+    [ dir = OPT direction; s = QSTRING;
       assoc = OPT associativity; prec = OPT precedence;
       IDENT "for";
       p2 = 
@@ -385,9 +385,11 @@ EXTEND
             | None -> default_precedence
             | Some prec -> prec
           in
-          (add_raw_attribute ~text:s
-            (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
-           assoc, prec, p2)
+          let p1 =
+            add_raw_attribute ~text:s
+              (CicNotationParser.parse_level1_pattern (Stream.of_string s))
+          in
+          (dir, p1, assoc, prec, p2)
     ]
   ];
   level3_term: [
@@ -402,7 +404,7 @@ EXTEND
     ]
   ];
   interpretation: [
-    [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
+    [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
         (s, args, t)
     ]
   ];
@@ -458,8 +460,8 @@ EXTEND
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
        let uris = List.map UriManager.uri_of_string uris in
         GrafiteAst.Default (loc,what,uris)
-    | IDENT "notation"; (l1, assoc, prec, l2) = notation ->
-        GrafiteAst.Notation (loc, l1, assoc, prec, l2)
+    | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
+        GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2)
     | IDENT "interpretation"; id = QSTRING;
       (symbol, args, l3) = interpretation ->
         GrafiteAst.Interpretation (loc, id, (symbol, args), l3)