More notation here and there.

[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 4a21e10b5a9e6334ce022bbb430b6ba6739fb08f..5caba868b1e220b2392f337f17e56317baaa2d2f 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -352,9 +352,8 @@ EXTEND
     ]
   ];
   argument: [
-    [ id = IDENT -> Ast.IdentArg (0, id)
-    | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
-      SYMBOL "."; id = IDENT ->
+    [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
+      id = IDENT ->
         Ast.IdentArg (List.length l, id)
     ]
   ];
@@ -374,10 +373,12 @@ EXTEND
       p2 = 
         [ blob = UNPARSED_AST ->
             add_raw_attribute ~text:(sprintf "@{%s}" blob)
-              (CicNotationParser.parse_level2_ast (Stream.of_string blob))
+              (CicNotationParser.parse_level2_ast
+                (Ulexing.from_utf8_string blob))
         | blob = UNPARSED_META ->
             add_raw_attribute ~text:(sprintf "${%s}" blob)
-              (CicNotationParser.parse_level2_meta (Stream.of_string blob))
+              (CicNotationParser.parse_level2_meta
+                (Ulexing.from_utf8_string blob))
         ] ->
           let assoc =
             match assoc with
@@ -391,7 +392,8 @@ EXTEND
           in
           let p1 =
             add_raw_attribute ~text:s
-              (CicNotationParser.parse_level1_pattern (Stream.of_string s))
+              (CicNotationParser.parse_level1_pattern
+                (Ulexing.from_utf8_string s))
           in
           (dir, p1, assoc, prec, p2)
     ]
@@ -505,6 +507,25 @@ let exc_located_wrapper f =
   | Stdpp.Exc_located (floc, exn) ->
       raise (CicNotationParser.Parse_error (floc, (Printexc.to_string exn)))
 
-let parse_statement stream =
-  exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
+let parse_statement lexbuf =
+  exc_located_wrapper
+    (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
+
+let parse_dependencies lexbuf = 
+  let tok_stream,_ =
+    CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf)
+  in
+  let rec parse acc = 
+    (parser
+    | [< '("URI", u) >] ->
+        parse (GrafiteAst.UriDep (UriManager.uri_of_string u) :: acc)
+    | [< '("IDENT", "include"); '("QSTRING", fname) >] ->
+        parse (GrafiteAst.IncludeDep fname :: acc)
+    | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] ->
+        parse (GrafiteAst.BaseuriDep baseuri :: acc)
+    | [< '("EOI", _) >] -> acc
+    | [< 'tok >] -> parse acc
+    | [<  >] -> acc) tok_stream
+  in
+  List.rev (parse [])