All the debug_print are now lazy.

[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..9f07baa4a77f62bc83394dd43425652d2289da36 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
    ]
@@ -351,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)
     ]
   ];
@@ -507,3 +507,19 @@ let exc_located_wrapper f =
 let parse_statement stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
 
+let parse_dependencies stream = 
+  let tok_stream,_ = CicNotationLexer.level2_ast_lexer.Token.tok_func stream 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 [])
+