From 5780dca4cfcee57e680213186cf3eaae402b6c88 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 13 Aug 2009 20:36:49 +0000 Subject: [PATCH] - xml exportation activated for the brg kernel - improved Makefiles --- helm/software/lambda-delta/.depend.opt | 33 +++++++----- helm/software/lambda-delta/Makefile | 20 +++----- helm/software/lambda-delta/Makefile.common | 16 ++++-- .../lambda-delta/basic_rg/brgOutput.ml | 50 +++++++++++++++++++ .../lambda-delta/basic_rg/brgOutput.mli | 2 + helm/software/lambda-delta/common/Make | 2 +- .../lambda-delta/common/commonLibrary.ml | 44 ++++++++++++++++ .../lambda-delta/common/commonLibrary.mli | 16 ++++++ helm/software/lambda-delta/toplevel/top.ml | 35 +++++++++---- 9 files changed, 175 insertions(+), 43 deletions(-) create mode 100644 helm/software/lambda-delta/common/commonLibrary.ml create mode 100644 helm/software/lambda-delta/common/commonLibrary.mli diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index f1c7339ee..ce241a639 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -33,13 +33,20 @@ automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx common/common.cmo: lib/nUri.cmi automath/aut.cmx common/common.cmx: lib/nUri.cmx automath/aut.cmx +common/commonLibrary.cmi: common/common.cmx +common/commonLibrary.cmo: lib/nUri.cmi common/common.cmx \ + common/commonLibrary.cmi +common/commonLibrary.cmx: lib/nUri.cmx common/common.cmx \ + common/commonLibrary.cmi basic_rg/brg.cmo: lib/log.cmi lib/cps.cmx common/common.cmx basic_rg/brg.cmx: lib/log.cmx lib/cps.cmx common/common.cmx -basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx +basic_rg/brgOutput.cmi: lib/log.cmi common/common.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ - lib/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi + lib/hierarchy.cmi lib/cps.cmx common/commonLibrary.cmi basic_rg/brg.cmx \ + basic_rg/brgOutput.cmi basic_rg/brgOutput.cmx: lib/output.cmx lib/nUri.cmx lib/log.cmx \ - lib/hierarchy.cmx lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi + lib/hierarchy.cmx lib/cps.cmx common/commonLibrary.cmx basic_rg/brg.cmx \ + basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx basic_rg/brgEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi @@ -132,16 +139,16 @@ toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/top.cmo: lib/time.cmx lib/output.cmi lib/nUri.cmi \ toplevel/metaOutput.cmi toplevel/metaBrg.cmi toplevel/metaBag.cmi \ toplevel/metaAut.cmi lib/log.cmi lib/hierarchy.cmi lib/cps.cmx \ - basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \ - basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \ - basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \ - automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \ - automath/autLexer.cmx + common/commonLibrary.cmi basic_rg/brgUntrusted.cmi \ + basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \ + basic_ag/bagUntrusted.cmi basic_ag/bagReduction.cmi \ + basic_ag/bagOutput.cmi basic_ag/bag.cmx automath/autProcess.cmi \ + automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx toplevel/top.cmx: lib/time.cmx lib/output.cmx lib/nUri.cmx \ toplevel/metaOutput.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \ toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx lib/cps.cmx \ - basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \ - basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \ - basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \ - automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \ - automath/autLexer.cmx + common/commonLibrary.cmx basic_rg/brgUntrusted.cmx \ + basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \ + basic_ag/bagUntrusted.cmx basic_ag/bagReduction.cmx \ + basic_ag/bagOutput.cmx basic_ag/bag.cmx automath/autProcess.cmx \ + automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index c5f715d74..705dc89bd 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -1,11 +1,13 @@ MAIN = helena -REQUIRES = unix +REQUIRES = unix str KEEP = README automath/*.aut CLEAN = log.txt +TAGS = test test-si meta export + include Makefile.common INPUT = automath/grundlagen.aut @@ -22,17 +24,9 @@ test-si: $(MAIN).opt meta: $(MAIN).opt @echo " HELENA -m meta.txt $(INPUT)" - $(H)./$(MAIN).opt -m meta.txt -s 1 -S 3 $(INPUT) > /dev/null + $(H)./$(MAIN).opt -m meta.txt -s 1 -S 1 $(INPUT) > log.txt $(H)$(GZIP) meta.txt -ifeq ($(MAKECMDGOALS), test) - include .depend.opt -endif - -ifeq ($(MAKECMDGOALS), test-si) - include .depend.opt -endif - -ifeq ($(MAKECMDGOALS), meta) - include .depend.opt -endif +export: $(MAIN).opt + @echo " HELENA -x xml $(INPUT)" + $(H)./$(MAIN).opt -x xml -s 2 -S 1 $(INPUT) > log.txt diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index cf15ef85d..f8b842909 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -28,8 +28,14 @@ define MOD_TEMPLATE ) endef -$(foreach DIR,$(DIRECTORIES),$(eval $(call DIR_TEMPLATE, $(DIR)))) -$(foreach MOD,$(MODULES),$(eval $(call MOD_TEMPLATE, $(MOD)))) +define INCLUDE_TEMPLATE + ifeq ($(MAKECMDGOALS), $(1)) + include .depend.opt + endif +endef + +$(foreach DIR, $(DIRECTORIES), $(eval $(call DIR_TEMPLATE, $(DIR)))) +$(foreach MOD, $(MODULES), $(eval $(call MOD_TEMPLATE, $(MOD)))) OBJECTS = $(patsubst %.ml,%.cmx,$(SOURCES:%.mli=%.cmi)) CLEAN += $(MAIN).opt @@ -66,6 +72,6 @@ tgz: clean @echo " OCAMLOPT $<" $(H)$(OCAMLOPT) -c $< -ifeq ($(MAKECMDGOALS), $(MAIN).opt) - include .depend.opt -endif +TAGS += $(MAIN).opt + +$(foreach TAG, $(TAGS), $(eval $(call INCLUDE_TEMPLATE, $(TAG)))) diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index aaa559be6..1aa3f9db7 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -15,6 +15,7 @@ module U = NUri module L = Log module H = Hierarchy module O = Output +module CL = CommonLibrary module B = Brg (* nodes count **************************************************************) @@ -185,3 +186,52 @@ let pp_context frm c = let specs = { L.pp_term = pp_term; L.pp_context = pp_context } + +(* term xml printing ********************************************************) + +let id frm a = + let f = function + | None -> () + | Some (true, s) -> F.fprintf frm " name=%S" s + | Some (false, n) -> F.fprintf frm " name=%S" ("^" ^ n) + in + B.name f a + +let rec exp_term frm = function + | B.Sort (a, l) -> + F.fprintf frm "" (string_of_int l) id a + | B.LRef (a, i) -> + F.fprintf frm "" (string_of_int i) id a + | B.GRef (a, u) -> + F.fprintf frm "" (U.string_of_uri u) id a + | B.Cast (a, w, t) -> + F.fprintf frm "%a%a" id a exp_boxed w exp_term t + | B.Appl (a, v, t) -> + F.fprintf frm "%a%a" id a exp_boxed v exp_term t + | B.Bind (a, b, t) -> + F.fprintf frm "%a%a" (exp_bind a) b exp_term t + +and exp_boxed frm t = + F.fprintf frm "@,@[ %a@]@," exp_term t + +and exp_bind a frm = function + | B.Abst w -> + F.fprintf frm "%a" id a exp_boxed w + | B.Abbr v -> + F.fprintf frm "%a" id a exp_boxed v + | B.Void -> + F.fprintf frm "" id a + +let export_obj frm = function + | _, uri, B.Abst w -> + let str = U.string_of_uri uri in + F.fprintf frm "%s@,@,%a" + (CL.doctype "ABST") str exp_boxed w + | _, uri, B.Abbr v -> + let str = U.string_of_uri uri in + F.fprintf frm "%s@,@,%a" + (CL.doctype "ABBR") str exp_boxed v + | _, uri, B.Void -> + let str = U.string_of_uri uri in + F.fprintf frm "%s@,@," + (CL.doctype "VOID") str diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index 9fa180abd..f238af5d0 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -18,3 +18,5 @@ val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Brg.context, Brg.term) Log.specs + +val export_obj: Format.formatter -> Brg.bind Common.obj -> unit diff --git a/helm/software/lambda-delta/common/Make b/helm/software/lambda-delta/common/Make index 30e1159c2..da8537d07 100644 --- a/helm/software/lambda-delta/common/Make +++ b/helm/software/lambda-delta/common/Make @@ -1 +1 @@ -common +common commonLibrary diff --git a/helm/software/lambda-delta/common/commonLibrary.ml b/helm/software/lambda-delta/common/commonLibrary.ml new file mode 100644 index 000000000..d19f491ae --- /dev/null +++ b/helm/software/lambda-delta/common/commonLibrary.ml @@ -0,0 +1,44 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module F = Filename +module U = NUri +module P = Printf +module C = Common + +(* internal functions *******************************************************) + +let obj_ext = ".ld.xml" + +let xml_head = + P.sprintf "" "1.0" "UTF-8" + +let system = "http://helm.cs.unibo.it/lambda-delta/ld.dtd" + +let path_of_uri base uri = + F.concat base (Str.string_after (U.string_of_uri uri) 3) + +(* interface functions ******************************************************) + +let doctype s = + P.sprintf "" s system + +let export_item export_obj base = function + | Some obj -> + let _, uri, bind = obj in + let path = path_of_uri base uri in + let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in + let och = open_out (path ^ obj_ext) in + let frm = Format.formatter_of_out_channel och in + Format.pp_set_margin frm max_int; + Format.fprintf frm "@[%s@,@,%a@]@." xml_head export_obj obj; + close_out och + | None -> () diff --git a/helm/software/lambda-delta/common/commonLibrary.mli b/helm/software/lambda-delta/common/commonLibrary.mli new file mode 100644 index 000000000..9cf3c9f40 --- /dev/null +++ b/helm/software/lambda-delta/common/commonLibrary.mli @@ -0,0 +1,16 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val export_item: + (Format.formatter -> 'bind Common.obj -> unit) -> + string -> 'bind Common.item -> unit + +val doctype: string -> string diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 507d11908..23460410d 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -21,6 +21,7 @@ module AO = AutOutput module MA = MetaAut module MO = MetaOutput module MBrg = MetaBrg +module CL = CommonLibrary module BrgO = BrgOutput module BrgR = BrgReduction module BrgU = BrgUntrusted @@ -35,18 +36,16 @@ type status = { ac : AO.counters; mc : MO.counters; brgc: BrgO.counters; - bagc: BagO.counters; - si : bool + bagc: BagO.counters } -let initial_status cover si = { +let initial_status cover = { ac = AO.initial_counters; mc = MO.initial_counters; brgc = BrgO.initial_counters; bagc = BagO.initial_counters; mst = MA.initial_status ~cover (); - ast = AP.initial_status; - si = si + ast = AP.initial_status } let count count_fun c item = @@ -89,14 +88,18 @@ let count_item st = function | BrgItem item -> {st with brgc = count BrgO.count_item st.brgc item} | BagItem item -> {st with bagc = count BagO.count_item st.bagc item} -let type_check f st g k = +let export_item base = function + | BrgItem item -> CL.export_item BrgO.export_obj base item + | BagItem _ -> () + +let type_check f st si g k = let f _ = function | None -> f st None | Some (i, u, _) -> f st (Some (i, u)) in match k with - | BrgItem item -> BrgU.type_check f ~si:st.si g item - | BagItem item -> BagU.type_check f ~si:st.si g item + | BrgItem item -> BrgU.type_check f ~si g item + | BagItem item -> BagU.type_check f ~si g item (****************************************************************************) @@ -108,6 +111,7 @@ try let progress = ref false in let use_cover = ref true in let si = ref false in + let library_dir = ref None in let set_hierarchy s = let f = function | Some g -> H.graph := g @@ -134,6 +138,9 @@ try Format.pp_set_margin frm max_int; meta_file := Some (och, frm) in + let set_library_dir name = + library_dir := Some name + in let read_file name = if !L.level > 0 then T.gmtime version_string; if !L.level > 1 then @@ -158,7 +165,11 @@ try (* stage 2 *) let f st item = let st = count_item st item in - if !stage > 2 then type_check f st !H.graph item else st + begin match !library_dir with + | None -> () + | Some base -> export_item base item + end; + if !stage > 2 then type_check f st !si !H.graph item else st in (* stage 1 *) let f st mst item = @@ -186,7 +197,7 @@ try if !use_cover then Filename.chop_extension (Filename.basename name) else "" in - let st = aux (initial_status cover !si) book in + let st = aux (initial_status cover) book in if !L.level > 0 then T.utime_stamp "processed"; if !L.level > 2 then AO.print_counters C.start st.ac; if !L.level > 2 then AO.print_process_counters C.start st.ast; @@ -210,6 +221,7 @@ try let help_p = " activate progress indicator" in let help_u = " activate sort inclusion" in let help_s = " Set translation stage" in + let help_x = " export kernel objects (XML)" in L.box 0; L.box_err (); H.set_new_sorts ignore ["Set"; "Prop"]; Arg.parse [ @@ -222,7 +234,8 @@ try ("-m", Arg.String set_meta_file, help_m); ("-p", Arg.Set progress, help_p); ("-u", Arg.Set si, help_u); - ("-s", Arg.Int set_stage, help_s) + ("-s", Arg.Int set_stage, help_s); + ("-x", Arg.String set_library_dir, help_x) ] read_file help; if !L.level > 0 then T.utime_stamp "at exit"; flush () -- 2.39.2