- synced notation pretty printing with parsing syntax

[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 41c3fd054bb411936e8289f386addbfe93933e5e..984635ec60cc44433df2b847ee3f877f1ff9edc6 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -29,10 +29,12 @@ let grammar = CicNotationParser.level2_ast_grammar
 
 let term = CicNotationParser.term
 let statement = Grammar.Entry.create grammar "statement"
-let statements = Grammar.Entry.create grammar "statements"
+
+let add_raw_attribute ?context ~text term =
+  CicNotationPt.AttributedTerm (`Raw (text, context), term)
 
 EXTEND
-  GLOBAL: term statement statements;
+  GLOBAL: term statement;
   arg: [
    [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN -> names,ty
@@ -338,10 +340,10 @@ EXTEND
     ]
   ];
   argument: [
-    [ id = IDENT -> GrafiteAst.IdentArg (0, id)
+    [ id = IDENT -> CicNotationPt.IdentArg (0, id)
     | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
       SYMBOL "."; id = IDENT ->
-        GrafiteAst.IdentArg (List.length l, id)
+        CicNotationPt.IdentArg (List.length l, id)
     ]
   ];
   associativity: [
@@ -359,21 +361,26 @@ EXTEND
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
-            CicNotationParser.parse_level2_ast (Stream.of_string blob)
+            add_raw_attribute ~context:`Ast ~text:blob
+              (CicNotationParser.parse_level2_ast (Stream.of_string blob))
         | blob = UNPARSED_META ->
-            CicNotationParser.parse_level2_meta (Stream.of_string blob) ]
-      ->
-        (CicNotationParser.parse_level1_pattern (Stream.of_string s), assoc, prec, p2)
+            add_raw_attribute ~context:`Meta ~text:blob
+              (CicNotationParser.parse_level2_meta (Stream.of_string blob))
+        ] ->
+          (add_raw_attribute ~text:s
+            (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
+           assoc, prec, p2)
     ]
   ];
   level3_term: [
-    [ u = URI -> GrafiteAst.UriPattern (UriManager.uri_of_string u)
-    | id = IDENT -> GrafiteAst.VarPattern id
+    [ u = URI -> CicNotationPt.UriPattern (UriManager.uri_of_string u)
+    | id = IDENT -> CicNotationPt.VarPattern id
+    | SYMBOL "_" -> CicNotationPt.ImplicitPattern
     | LPAREN; terms = LIST1 SELF; RPAREN ->
         (match terms with
         | [] -> assert false
         | [term] -> term
-        | terms -> GrafiteAst.ApplPattern terms)
+        | terms -> CicNotationPt.ApplPattern terms)
     ]
   ];
   interpretation: [
@@ -435,11 +442,13 @@ EXTEND
         GrafiteAst.Default (loc,what,uris)
     | IDENT "notation"; (l1, assoc, prec, l2) = notation ->
         GrafiteAst.Notation (loc, l1, assoc, prec, l2)
-    | IDENT "interpretation"; (symbol, args, l3) = interpretation ->
-        GrafiteAst.Interpretation (loc, (symbol, args), l3)
+    | IDENT "interpretation"; id = QSTRING;
+      (symbol, args, l3) = interpretation ->
+        GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
 
     | IDENT "dump" -> GrafiteAst.Dump loc
-    | IDENT "render"; u = URI -> GrafiteAst.Render (loc, UriManager.uri_of_string u)
+    | IDENT "render"; u = URI ->
+        GrafiteAst.Render (loc, UriManager.uri_of_string u)
   ]];
   executable: [
     [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
@@ -457,18 +466,16 @@ EXTEND
   statement: [
     [ ex = executable -> GrafiteAst.Executable (loc,ex)
     | com = comment -> GrafiteAst.Comment (loc, com)
+    | EOI -> raise End_of_file
     ]
   ];
-  statements: [
-    [ l = LIST0 statement ; EOI -> l 
-    ]  
-  ];
 END
 
 let exc_located_wrapper f =
   try
     f ()
   with
+  | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
   | Stdpp.Exc_located (floc, Stream.Error msg) ->
       raise (CicNotationParser.Parse_error (floc, msg))
   | Stdpp.Exc_located (floc, exn) ->
@@ -476,6 +483,4 @@ let exc_located_wrapper f =
 
 let parse_statement stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
-let parse_statements stream =
-  exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))