Better handling of idref propagation, no more Href hack, multiple idrefs are

[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 ae7e5229d1941d2809023f51863295cace796659..c3a4b7f01ef998e30c5debd31d5ee34a032725bb 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -69,9 +69,10 @@ EXTEND
        SEP SYMBOL ";";
      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
       let goal_path =
-       match goal_path with
-          None -> Ast.UserInput
-        | Some goal_path -> goal_path
+       match goal_path, hyp_paths with
+          None, [] -> Ast.UserInput
+        | None, _::_ -> Ast.Implicit
+        | Some goal_path, _ -> goal_path
       in
        hyp_paths,goal_path
    ]
@@ -111,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 ->
@@ -351,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)
     ]
   ];
@@ -373,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
@@ -390,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)
     ]
@@ -504,6 +508,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 [])