]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/grafiteParser.ml
added a minimal parser to extract informations relevant to dependencies calculation
[helm.git] / helm / ocaml / cic_notation / grafiteParser.ml
index 4a21e10b5a9e6334ce022bbb430b6ba6739fb08f..65df218d4f4bf22a1f8d519bcad35f2846c839bf 100644 (file)
@@ -508,3 +508,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 [])
+