incomplete snapshot ....

[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 65df218d4f4bf22a1f8d519bcad35f2846c839bf..c3a4b7f01ef998e30c5debd31d5ee34a032725bb 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -112,8 +112,9 @@ EXTEND
     | IDENT "auto";
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
       width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ];
-      paramodulation = OPT [ IDENT "paramodulation" ] ->  (* ALB *)
-          GrafiteAst.Auto (loc,depth,width,paramodulation)
+      paramodulation = OPT [ IDENT "paramodulation" ];
+      full = OPT [ IDENT "full" ] ->  (* ALB *)
+          GrafiteAst.Auto (loc,depth,width,paramodulation,full)
     | IDENT "clear"; id = IDENT ->
         GrafiteAst.Clear (loc,id)
     | IDENT "clearbody"; id = IDENT ->
@@ -352,9 +353,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 +374,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 +393,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,11 +508,14 @@ 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 stream = 
-  let tok_stream,_ = CicNotationLexer.level2_ast_lexer.Token.tok_func stream in
+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) >] ->