From: Enrico Tassi Date: Tue, 20 Sep 2005 14:15:09 +0000 (+0000) Subject: added a minimal parser to extract informations relevant to dependencies calculation X-Git-Tag: LAST_BEFORE_NEW~85 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3e5a3049534e6b5a091598a079b61c91134650f1;p=helm.git 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 3a17410dd..95eb76c4d 100644 --- 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 61c3f6d08..65251b820 100644 --- 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 4697ab6ad..f406c44a8 100644 --- 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 0c63d2594..6a8e79bc1 100644 --- 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 ad6c26db1..bf4d2cdab 100644 --- 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 4a21e10b5..65df218d4 100644 --- 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 3d4112016..e6b549dab 100644 --- 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 index 000000000..c40b6e7de --- /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