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
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
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
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
)
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
@echo " OCAMLOPT $<"
$(H)$(OCAMLOPT) -c $<
-ifeq ($(MAKECMDGOALS), $(MAIN).opt)
- include .depend.opt
-endif
+TAGS += $(MAIN).opt
+
+$(foreach TAG, $(TAGS), $(eval $(call INCLUDE_TEMPLATE, $(TAG))))
module L = Log
module H = Hierarchy
module O = Output
+module CL = CommonLibrary
module B = Brg
(* nodes count **************************************************************)
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 "<Sort position=%S%a/>" (string_of_int l) id a
+ | B.LRef (a, i) ->
+ F.fprintf frm "<LRef position=%S%a/>" (string_of_int i) id a
+ | B.GRef (a, u) ->
+ F.fprintf frm "<GRef uri=%S%a/>" (U.string_of_uri u) id a
+ | B.Cast (a, w, t) ->
+ F.fprintf frm "<Cast%a/>%a%a" id a exp_boxed w exp_term t
+ | B.Appl (a, v, t) ->
+ F.fprintf frm "<Appl%a/>%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 "@,@[<v3> %a@]@," exp_term t
+
+and exp_bind a frm = function
+ | B.Abst w ->
+ F.fprintf frm "<Abst%a/>%a" id a exp_boxed w
+ | B.Abbr v ->
+ F.fprintf frm "<Abbr%a/>%a" id a exp_boxed v
+ | B.Void ->
+ F.fprintf frm "<Void%a/>" id a
+
+let export_obj frm = function
+ | _, uri, B.Abst w ->
+ let str = U.string_of_uri uri in
+ F.fprintf frm "%s@,@,<ABST uri=%S>%a</ABST>"
+ (CL.doctype "ABST") str exp_boxed w
+ | _, uri, B.Abbr v ->
+ let str = U.string_of_uri uri in
+ F.fprintf frm "%s@,@,<ABBR uri=%S>%a</ABBR>"
+ (CL.doctype "ABBR") str exp_boxed v
+ | _, uri, B.Void ->
+ let str = U.string_of_uri uri in
+ F.fprintf frm "%s@,@,<VOID uri=%S/>"
+ (CL.doctype "VOID") str
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
-common
+common commonLibrary
--- /dev/null
+(*
+ ||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 "<?xml version=%S encoding=%S?>" "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 "<!DOCTYPE %s SYSTEM %S>" 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 "@[<v>%s@,@,%a@]@." xml_head export_obj obj;
+ close_out och
+ | None -> ()
--- /dev/null
+(*
+ ||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
module MA = MetaAut
module MO = MetaOutput
module MBrg = MetaBrg
+module CL = CommonLibrary
module BrgO = BrgOutput
module BrgR = BrgReduction
module BrgU = BrgUntrusted
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 =
| 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
(****************************************************************************)
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
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
(* 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 =
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;
let help_p = " activate progress indicator" in
let help_u = " activate sort inclusion" in
let help_s = "<number> Set translation stage" in
+ let help_x = "<directory> export kernel objects (XML)" in
L.box 0; L.box_err ();
H.set_new_sorts ignore ["Set"; "Prop"];
Arg.parse [
("-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 ()
projects / helm.git / commitdiff