merged cic_notation with disambiguation: good luck!

[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..8bd5cc04e3e976c62dcc2f07e4cecbdfc36ec0a7 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -29,10 +29,9 @@ let grammar = CicNotationParser.level2_ast_grammar
 
 let term = CicNotationParser.term
 let statement = Grammar.Entry.create grammar "statement"
-let statements = Grammar.Entry.create grammar "statements"
 
 EXTEND
-  GLOBAL: term statement statements;
+  GLOBAL: term statement;
   arg: [
    [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN -> names,ty
@@ -338,10 +337,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: [
@@ -367,13 +366,14 @@ EXTEND
     ]
   ];
   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 +435,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 +459,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 +476,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))