From de66af7241ad8ab71d5857d14570e4662f2488dc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 16 Aug 2009 21:13:06 +0000 Subject: [PATCH] - performance data added for reference - interface of the Hierarchy module improved - library for managining abstract layer representation files added - toplevel improved: the analysis of the automath source is now optional --- helm/software/lambda-delta/.depend.opt | 41 ++++---- helm/software/lambda-delta/Makefile | 27 +++--- helm/software/lambda-delta/Makefile.common | 1 - .../lambda-delta/basic_ag/bagOutput.ml | 8 +- .../lambda-delta/basic_rg/brgOutput.ml | 11 +-- .../lambda-delta/basic_rg/brgReduction.ml | 4 +- .../software/lambda-delta/common/hierarchy.ml | 14 +-- .../lambda-delta/common/hierarchy.mli | 6 +- helm/software/lambda-delta/common/library.ml | 10 +- helm/software/lambda-delta/common/library.mli | 2 +- helm/software/lambda-delta/lib/cps.ml | 2 + helm/software/lambda-delta/performance.txt | 6 ++ helm/software/lambda-delta/toplevel/Make | 2 +- .../lambda-delta/toplevel/metaLibrary.ml | 36 +++++++ .../lambda-delta/toplevel/metaLibrary.mli | 18 ++++ helm/software/lambda-delta/toplevel/top.ml | 93 +++++++++---------- 16 files changed, 163 insertions(+), 118 deletions(-) create mode 100644 helm/software/lambda-delta/performance.txt create mode 100644 helm/software/lambda-delta/toplevel/metaLibrary.ml create mode 100644 helm/software/lambda-delta/toplevel/metaLibrary.mli diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index bcaca037f..740fce2ce 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,17 +1,9 @@ -lib/nUri.cmi: lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi -lib/cps.cmo: -lib/cps.cmx: -lib/share.cmo: -lib/share.cmx: -lib/log.cmi: lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx -automath/aut.cmo: -automath/aut.cmx: automath/autProcess.cmi: automath/aut.cmx automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi @@ -25,10 +17,8 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx -common/hierarchy.cmi: common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi -common/output.cmi: common/output.cmo: lib/log.cmi common/output.cmi common/output.cmx: lib/log.cmx common/output.cmi common/item.cmo: lib/nUri.cmi automath/aut.cmx @@ -120,6 +110,9 @@ toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/log.cmi \ lib/cps.cmx toplevel/metaOutput.cmi toplevel/metaOutput.cmx: lib/nUri.cmx toplevel/meta.cmx lib/log.cmx \ lib/cps.cmx toplevel/metaOutput.cmi +toplevel/metaLibrary.cmi: toplevel/meta.cmx +toplevel/metaLibrary.cmo: toplevel/metaOutput.cmi toplevel/metaLibrary.cmi +toplevel/metaLibrary.cmx: toplevel/metaOutput.cmx toplevel/metaLibrary.cmi toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \ automath/aut.cmx toplevel/metaAut.cmi @@ -136,18 +129,18 @@ toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmi toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \ - toplevel/metaOutput.cmi toplevel/metaBrg.cmi toplevel/metaBag.cmi \ - toplevel/metaAut.cmi lib/log.cmi common/library.cmi common/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 + toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \ + toplevel/metaBag.cmi toplevel/metaAut.cmi lib/log.cmi common/library.cmi \ + common/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 toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \ - toplevel/metaOutput.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \ - toplevel/metaAut.cmx lib/log.cmx common/library.cmx common/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 + toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \ + toplevel/metaBag.cmx toplevel/metaAut.cmx lib/log.cmx common/library.cmx \ + common/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 diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index b158ae3e0..ac4183f72 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -6,7 +6,7 @@ KEEP = README automath/*.aut CLEAN = log.txt -TAGS = test test-si meta export-si +TAGS = test test-si test-si-fast hir xml-si include Makefile.common @@ -15,18 +15,21 @@ INPUT = automath/grundlagen.aut INPUT-ORIG = automath/grundlagen-orig.aut test: $(MAIN).opt - @echo " HELENA $(INPUT)" - $(H)./$(MAIN).opt -S 3 $(O) $(INPUT) > log.txt + @echo " HELENA -a -c $(INPUT)" + $(H)./$(MAIN).opt -a -c -S 3 $(O) $(INPUT) > log.txt test-si: $(MAIN).opt - @echo " HELENA -c -u $(INPUT)" - $(H)./$(MAIN).opt -c -u -S 3 $(O) $(INPUT) > log.txt + @echo " HELENA -a -c -u $(INPUT)" + $(H)./$(MAIN).opt -a -c -u -S 3 $(O) $(INPUT) > log.txt -meta: $(MAIN).opt - @echo " HELENA -m meta.txt $(INPUT)" - $(H)./$(MAIN).opt -m meta.txt -s 1 -S 1 $(INPUT) > log.txt - $(H)$(GZIP) meta.txt +test-si-fast: $(MAIN).opt + @echo " HELENA -u $(INPUT)" + $(H)./$(MAIN).opt -u -S 1 $(O) $(INPUT) > log.txt -export-si: $(MAIN).opt - @echo " HELENA -u -x xml $(INPUT)" - $(H)./$(MAIN).opt -u -x xml -s 2 -S 1 $(INPUT) > log.txt +hir: $(MAIN).opt + @echo " HELENA -m $(INPUT)" + $(H)./$(MAIN).opt -m -s 1 -S 1 $(INPUT) > log.txt + +xml-si: $(MAIN).opt + @echo " HELENA -u -x $(INPUT)" + $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > log.txt diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index f8b842909..7b8d0c3c3 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -9,7 +9,6 @@ OCAMLOPT = ocamlfind opt -linkpkg -package "$(REQUIRES)" $(INCLUDES) OCAMLLEX = ocamllex.opt OCAMLYACC = ocamlyacc -v TAR = tar -czf $(MAIN:%=%.tgz) -GZIP = gzip define DIR_TEMPLATE MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make)) diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index 17bfe0659..c315b1ec7 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -105,11 +105,9 @@ let res l id = let rec pp_term c frm = function | B.Sort h -> - let f = function - | Some s -> F.fprintf frm "@[%s@]" s - | None -> F.fprintf frm "@[*%u@]" h - in - H.get_sort f h + let err () = F.fprintf frm "@[*%u@]" h in + let f s = F.fprintf frm "@[%s@]" s in + H.get_sort err f h | B.LRef i -> let f = function | Some (id, _) -> F.fprintf frm "@[%s@]" id diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index dc697bff4..5dc3887c5 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -133,20 +133,17 @@ let print_counters f c = (* context/term pretty printing *********************************************) let id frm a = - let err () = assert false in let f n = function | true -> F.fprintf frm "%s" n | false -> F.fprintf frm "^%s" n in - B.name err f a + B.name C.err f a let rec pp_term c frm = function | B.Sort (_, h) -> - let f = function - | Some s -> F.fprintf frm "@[%s@]" s - | None -> F.fprintf frm "@[*%u@]" h - in - H.get_sort f h + let err () = F.fprintf frm "@[*%u@]" h in + let f s = F.fprintf frm "@[%s@]" s in + H.get_sort err f h | B.LRef (_, i) -> let err i = F.fprintf frm "@[#%u@]" i in let f _ a _ = F.fprintf frm "@[%a@]" id a in diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 4a1667862..8ac7021f9 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -51,8 +51,6 @@ let error3 c t1 t2 t3 = in raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) -let err () = assert false - let get f m i = B.get error0 f m.c i @@ -85,7 +83,7 @@ let rec step f ?(delta=false) ?(rt=false) m x = f {m with c = c} None x | b -> let f e = f {m with c = c} (Some (e, b)) x in - B.apix err f a + B.apix C.err f a in get f m i | B.Cast (_, _, t) -> diff --git a/helm/software/lambda-delta/common/hierarchy.ml b/helm/software/lambda-delta/common/hierarchy.ml index f916e1e43..abe23e10a 100644 --- a/helm/software/lambda-delta/common/hierarchy.ml +++ b/helm/software/lambda-delta/common/hierarchy.ml @@ -30,20 +30,16 @@ let set_new_sorts f ss = let f i = index := i; f i in C.list_fold_left f set_sort !index ss -let get_sort f h = - try f (Some (H.find sort h)) - with Not_found -> f None +let get_sort err f h = + try f (H.find sort h) with Not_found -> err () let string_of_graph f (s, _) = f s let apply f (_, g) h = f (g h) -let graph_of_string f s = +let graph_of_string err f s = try let x = S.sscanf s "Z%u" C.start in - if x > 0 then f (Some (s, fun h -> x + h)) else f None + if x > 0 then f (s, fun h -> x + h) else err () with - S.Scan_failure _ | Failure _ | End_of_file -> f None - -let graph = - ref (graph_of_string (function Some g -> g | None -> assert false) "Z2") + S.Scan_failure _ | Failure _ | End_of_file -> err () diff --git a/helm/software/lambda-delta/common/hierarchy.mli b/helm/software/lambda-delta/common/hierarchy.mli index 57413d909..5bebd28df 100644 --- a/helm/software/lambda-delta/common/hierarchy.mli +++ b/helm/software/lambda-delta/common/hierarchy.mli @@ -13,12 +13,10 @@ type graph val set_new_sorts: (int -> 'a) -> string list -> 'a -val get_sort: (string option -> 'a) -> int -> 'a +val get_sort: (unit -> 'a) -> (string -> 'a) -> int -> 'a -val graph_of_string: (graph option -> 'a) -> string -> 'a +val graph_of_string: (unit -> 'a) -> (graph -> 'a) -> string -> 'a val string_of_graph: (string -> 'a) -> graph -> 'a val apply: (int -> 'a) -> graph -> int -> 'a - -val graph: graph ref diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index 80e9c59da..23f156123 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -15,11 +15,13 @@ module H = Hierarchy (* internal functions *******************************************************) +let base = "xml" + let obj_ext = ".ld.xml" -let system = "http://helm.cs.unibo.it/lambda-delta/xml/ld.dtd" +let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd" -let path_of_uri base uri = +let path_of_uri uri = F.concat base (Str.string_after (U.string_of_uri uri) 3) let pp_head frm = @@ -40,10 +42,10 @@ let close_kernel frm = (* interface functions ******************************************************) -let export_item export_obj si g base = function +let export_item export_obj si g = function | Some obj -> let _, uri, bind = obj in - let path = path_of_uri base uri in + let path = path_of_uri 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 diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli index 3c89ab317..7e3ee1b82 100644 --- a/helm/software/lambda-delta/common/library.mli +++ b/helm/software/lambda-delta/common/library.mli @@ -11,4 +11,4 @@ val export_item: (Format.formatter -> 'bind Item.obj -> unit) -> - bool -> Hierarchy.graph -> string -> 'bind Item.item -> unit + bool -> Hierarchy.graph -> 'bind Item.item -> unit diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml index 38b249030..75f8bcd37 100644 --- a/helm/software/lambda-delta/lib/cps.ml +++ b/helm/software/lambda-delta/lib/cps.ml @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +let err () = assert false + let start x = x let id f x = f x diff --git a/helm/software/lambda-delta/performance.txt b/helm/software/lambda-delta/performance.txt new file mode 100644 index 000000000..5d674bd66 --- /dev/null +++ b/helm/software/lambda-delta/performance.txt @@ -0,0 +1,6 @@ +parsed : 0.7 +intermediate: 1.6 +untrusted : 0.4 +trusted : 6.5 + 3 with upsilon relocations +------------------ +total : 9.2 diff --git a/helm/software/lambda-delta/toplevel/Make b/helm/software/lambda-delta/toplevel/Make index c32bec6c7..a8a72e17f 100644 --- a/helm/software/lambda-delta/toplevel/Make +++ b/helm/software/lambda-delta/toplevel/Make @@ -1 +1 @@ -meta metaOutput metaAut metaBag metaBrg top +meta metaOutput metaLibrary metaAut metaBag metaBrg top diff --git a/helm/software/lambda-delta/toplevel/metaLibrary.ml b/helm/software/lambda-delta/toplevel/metaLibrary.ml new file mode 100644 index 000000000..e9192f598 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaLibrary.ml @@ -0,0 +1,36 @@ +(* + ||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 = Format +module O = MetaOutput + +type out_channel = Pervasives.out_channel * F.formatter + +(* internal functions *******************************************************) + +let hal_dir = "hal" + +let hal_ext = ".hal" + +(* interface functions ******************************************************) + +let open_out f name = + let _ = Sys.command (Printf.sprintf "mkdir -p %s" hal_dir) in + let och = open_out (Filename.concat hal_dir (name ^ hal_ext)) in + let frm = F.formatter_of_out_channel och in + F.pp_set_margin frm max_int; + f (och, frm) + +let write_item f (_, frm) item = + O.pp_item f frm item + +let close_out f (och, _) = + close_out och; f () diff --git a/helm/software/lambda-delta/toplevel/metaLibrary.mli b/helm/software/lambda-delta/toplevel/metaLibrary.mli new file mode 100644 index 000000000..d1c723436 --- /dev/null +++ b/helm/software/lambda-delta/toplevel/metaLibrary.mli @@ -0,0 +1,18 @@ +(* + ||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_______________________________________________________________ *) + +type out_channel + +val open_out: (out_channel -> 'a) -> string -> 'a + +val write_item: (unit -> 'a) -> out_channel -> Meta.item -> 'a + +val close_out: (unit -> 'a) -> out_channel -> 'a diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 6a45f06c5..3fa3c908c 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -20,6 +20,7 @@ module AP = AutProcess module AO = AutOutput module MA = MetaAut module MO = MetaOutput +module ML = MetaLibrary module MBrg = MetaBrg module G = Library module BrgO = BrgOutput @@ -88,8 +89,8 @@ 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 export_item si g base = function - | BrgItem item -> G.export_item BrgO.export_obj si g base item +let export_item si g = function + | BrgItem item -> G.export_item BrgO.export_obj si g item | BagItem _ -> () let type_check f st si g k = @@ -107,17 +108,18 @@ let main = try let version_string = "Helena 0.8.0 M - August 2009" in let stage = ref 3 in - let meta_file = ref None in + let moch = ref None in + let meta = ref false in let progress = ref false in + let process = ref false in let use_cover = ref true in let si = ref false in - let library_dir = ref None in + let export = ref false in + let graph = ref (H.graph_of_string C.err C.start "Z2") in let set_hierarchy s = - let f = function - | Some g -> H.graph := g - | None -> L.warn (P.sprintf "Unknown type hierarchy: %s" s) - in - H.graph_of_string f s + let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in + let f g = graph := g in + H.graph_of_string err f s in let set_kernel = function | "brg" -> kernel := Brg @@ -127,25 +129,21 @@ try let set_summary i = L.level := i in let print_version () = L.warn (version_string ^ "\n"); exit 0 in let set_stage i = stage := i in - let close = function - | None -> () - | Some (och, _) -> close_out och - in let set_meta_file name = - close !meta_file; - let och = open_out name in - let frm = Format.formatter_of_out_channel och in - Format.pp_set_margin frm max_int; - meta_file := Some (och, frm) + let f och = moch := Some och in + ML.open_out f name in - let set_library_dir name = - library_dir := Some name + let close = function + | None -> () + | Some och -> ML.close_out C.start och in let read_file name = if !L.level > 0 then T.gmtime version_string; if !L.level > 1 then L.warn (P.sprintf "Processing file: %s" name); if !L.level > 0 then T.utime_stamp "started"; + let base_name = Filename.chop_extension (Filename.basename name) in + if !meta then set_meta_file base_name; let ich = open_in name in let lexbuf = Lexing.from_channel ich in let book = AutParser.book AutLexer.token lexbuf in @@ -165,20 +163,17 @@ try (* stage 2 *) let f st item = let st = count_item st item in - begin match !library_dir with - | None -> () - | Some base -> export_item !si !H.graph base item - end; - if !stage > 2 then type_check f st !si !H.graph item else st + if !export then export_item !si !graph item; + if !stage > 2 then type_check f st !si !graph item else st in (* stage 1 *) let f st mst item = let st = {st with mst = mst; mc = count MO.count_item st.mc item } in - begin match !meta_file with - | None -> () - | Some (_, frm) -> MO.pp_item C.start frm item + begin match !moch with + | None -> () + | Some och -> ML.write_item C.start och item end; if !stage > 1 then kernel_of_meta f st item else st in @@ -190,54 +185,58 @@ try in aux st tl in - process_item f st item + if !process then process_item f st item else f st item in O.clear_reductions (); - let cover = - if !use_cover then Filename.chop_extension (Filename.basename name) - else "" - in + let cover = if !use_cover then base_name else "" 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; + if !L.level > 2 && !process then AO.print_process_counters C.start st.ast; if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc; if !L.level > 2 && !stage > 1 then print_counters st; if !L.level > 2 && !stage > 1 then O.print_reductions () in + let exit () = + close !moch; + if !L.level > 0 then T.utime_stamp "at exit"; + flush () + in let help = - "Usage: helena [ -Vcipu | -Ss | -m | -hk ] ...\n\n" ^ - "Summary levels: 0 just errors, 1 time stamps, 2 processed file names, \ + "Usage: helena [ -Vacimpux | -Ss | -hk ] ...\n\n" ^ + "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ - "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted\n" + "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" in - let help_S = " set summary level" in + let help_S = " set summary level (see above)" in let help_V = " show version information" in + + let help_a = " analyze source files" in let help_c = " disable initial segment of URI hierarchy" in - let help_h = " set type hierarchy" in + let help_h = " set type hierarchy (default: Z2)" in let help_i = " show local references by index" in - let help_k = " set kernel version" in - let help_m = " output intermediate representation" in + let help_k = " set kernel version (default: brg)" in + let help_m = " output intermediate representation (HAL)" in 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 + let help_s = " set translation stage (see above)" in + let help_x = " export kernel objects (XML)" in L.box 0; L.box_err (); H.set_new_sorts ignore ["Set"; "Prop"]; + at_exit exit; Arg.parse [ ("-S", Arg.Int set_summary, help_S); ("-V", Arg.Unit print_version, help_V); + ("-a", Arg.Set process, help_a); ("-c", Arg.Clear use_cover, help_c); ("-h", Arg.String set_hierarchy, help_h); ("-i", Arg.Set O.indexes, help_i); ("-k", Arg.String set_kernel, help_k); - ("-m", Arg.String set_meta_file, help_m); + ("-m", Arg.Set meta, help_m); ("-p", Arg.Set progress, help_p); ("-u", Arg.Set si, help_u); ("-s", Arg.Int set_stage, help_s); - ("-x", Arg.String set_library_dir, help_x) + ("-x", Arg.Set export, help_x) ] read_file help; - if !L.level > 0 then T.utime_stamp "at exit"; - flush () with BagR.TypeError msg -> bag_error "Type Error" msg | BrgR.TypeError msg -> brg_error "Type Error" msg -- 2.39.2