added a minimal parser to extract informations relevant to dependencies calculation

diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend
index 3a17410ddb4b1a406f83a104547d43024d431fe7..95eb76c4da009117e6416e6162f104d379db81a9 100644 (file)
--- a/helm/ocaml/cic_notation/.depend
+++ b/helm/ocaml/cic_notation/.depend
@@ -1,4 +1,4 @@
-cicNotationUtil.cmi: cicNotationPt.cmo 
+cicNotationUtil.cmi: grafiteAst.cmo cicNotationPt.cmo 
 cicNotationTag.cmi: cicNotationPt.cmo 
 cicNotationEnv.cmi: cicNotationPt.cmo 
 cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi 
@@ -15,8 +15,8 @@ grafiteAst.cmo: cicNotationPt.cmo
 grafiteAst.cmx: cicNotationPt.cmx 
 renderingAttrs.cmo: renderingAttrs.cmi 
 renderingAttrs.cmx: renderingAttrs.cmi 
-cicNotationUtil.cmo: cicNotationPt.cmo cicNotationUtil.cmi 
-cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi 
+cicNotationUtil.cmo: grafiteAst.cmo cicNotationPt.cmo cicNotationUtil.cmi 
+cicNotationUtil.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationUtil.cmi 
 cicNotationTag.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationTag.cmi 
 cicNotationTag.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationTag.cmi 
 cicNotationLexer.cmo: cicNotationLexer.cmi 
@@ -52,19 +52,17 @@ cicNotationParser.cmx: cicNotationUtil.cmx cicNotationPt.cmx \
     cicNotationPp.cmx cicNotationLexer.cmx cicNotationEnv.cmx \
     cicNotationParser.cmi 
 grafiteParser.cmo: grafiteAst.cmo cicNotationPt.cmo cicNotationParser.cmi \
-    grafiteParser.cmi 
+    cicNotationLexer.cmi grafiteParser.cmi 
 grafiteParser.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationParser.cmx \
-    grafiteParser.cmi 
+    cicNotationLexer.cmx grafiteParser.cmi 
 mpresentation.cmo: mpresentation.cmi 
 mpresentation.cmx: mpresentation.cmi 
 box.cmo: renderingAttrs.cmi box.cmi 
 box.cmx: renderingAttrs.cmx box.cmi 
 cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationUtil.cmi \
-    cicNotationPt.cmo cicNotationPres.cmi cicNotationPp.cmi box.cmi \
-    cicNotationPres.cmi 
+    cicNotationPt.cmo cicNotationPp.cmi box.cmi cicNotationPres.cmi 
 cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationUtil.cmx \
-    cicNotationPt.cmx cicNotationPres.cmx cicNotationPp.cmx box.cmx \
-    cicNotationPres.cmi 
+    cicNotationPt.cmx cicNotationPp.cmx box.cmx cicNotationPres.cmi 
 boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
     boxPp.cmi 
 boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \

diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile
index 61c3f6d08f22a9291434ff3939d863937f0fbacc..65251b820acab3c18c5a024ab53fb981c2f9f37f 100644 (file)
--- a/helm/ocaml/cic_notation/Makefile
+++ b/helm/ocaml/cic_notation/Makefile
@@ -33,15 +33,18 @@ IMPLEMENTATION_FILES = \
        $(patsubst %.mli, %.ml, $(INTERFACE_FILES))     \
        $(NULL)
 
-all: test_lexer test_parser
+all: test_lexer test_parser test_dep
 
 LOCAL_LINKOPTS = -package helm-cic_notation -linkpkg
-test: test_lexer test_parser
+test: test_lexer test_parser test_dep
 test_lexer: test_lexer.ml $(PACKAGE).cma
        $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
 test_parser: REQUIRES += helm-cic_omdoc
 test_parser: test_parser.ml $(PACKAGE).cma
        $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+test_dep: test_dep.ml $(PACKAGE).cma
+       $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+
 
 cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4)
 cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4)

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index 4697ab6adceca84e0d566ffb66374458a6dbc844..f406c44a885d4870333c21b7dfc0e55cef24f803 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -190,3 +190,9 @@ type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
   | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
   | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment
 
+  (* statements meaningful for matitadep *)
+type dependency =
+  | IncludeDep of string
+  | BaseuriDep of string
+  | UriDep of UriManager.uri
+  

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml
index 0c63d2594d0ea4e4398a7902981302ee2e7aa47c..6a8e79bc10722535c8dff3df30ab016144ace9fe 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -341,3 +341,8 @@ let pp_cic_command = function
   | Notation _
   | Obj _ -> assert false (* not implemented *)
 
+let pp_dependency = function
+  | IncludeDep str -> "include \"" ^ str ^ "\""
+  | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\""
+  | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
+

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.mli b/helm/ocaml/cic_notation/grafiteAstPp.mli
index ad6c26db1a5779b9eb6c6971ff64535b3defc038..bf4d2cdab41dfbe2847a5c42f99da1e4ce16bb51 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAstPp.mli
+++ b/helm/ocaml/cic_notation/grafiteAstPp.mli
@@ -62,3 +62,6 @@ val pp_alias: GrafiteAst.alias_spec -> string
 
 val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string
 
+val pp_dependency:  GrafiteAst.dependency -> string
+
+  

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 4a21e10b5a9e6334ce022bbb430b6ba6739fb08f..65df218d4f4bf22a1f8d519bcad35f2846c839bf 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -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 [])
+

diff --git a/helm/ocaml/cic_notation/grafiteParser.mli b/helm/ocaml/cic_notation/grafiteParser.mli
index 3d411201629ed26f84a51c4fc6683468daf292b8..e6b549dabfdbaba589f9ec011c73d8a35b9d5666 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.mli
+++ b/helm/ocaml/cic_notation/grafiteParser.mli
@@ -30,3 +30,6 @@ val parse_statement:
      GrafiteAst.obj, string)
     GrafiteAst.statement
 
+  (** @raise End_of_file *)
+val parse_dependencies: char Stream.t -> GrafiteAst.dependency list
+    

diff --git a/helm/ocaml/cic_notation/test_dep.ml b/helm/ocaml/cic_notation/test_dep.ml
new file mode 100644 (file)
index 0000000..c40b6e7
--- /dev/null
+++ b/helm/ocaml/cic_notation/test_dep.ml
@@ -0,0 +1,35 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+let _ =
+  let ic = ref stdin in
+  let usage = "test_coarse_parser [ file ]" in
+  let open_file fname =
+    if !ic <> stdin then close_in !ic;
+    ic := open_in fname
+  in
+  Arg.parse [] open_file usage;
+  let deps = GrafiteParser.parse_dependencies (Stream.of_channel !ic) in
+  List.iter (fun dep -> print_endline (GrafiteAstPp.pp_dependency dep)) deps