-cicNotationUtil.cmi: cicNotationPt.cmo
+cicNotationUtil.cmi: grafiteAst.cmo cicNotationPt.cmo
cicNotationTag.cmi: cicNotationPt.cmo
cicNotationEnv.cmi: cicNotationPt.cmo
cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi
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
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 \
$(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)
| 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
+
| 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 ^ "\""
+
val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string
+val pp_dependency: GrafiteAst.dependency -> string
+
+
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 [])
+
GrafiteAst.obj, string)
GrafiteAst.statement
+ (** @raise End_of_file *)
+val parse_dependencies: char Stream.t -> GrafiteAst.dependency list
+
--- /dev/null
+(* 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