From a7e986f3c381186e58aa1c6a65f03ee721deb9b1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 22 Jun 2015 17:53:25 +0000 Subject: [PATCH] command line options rearranged --- helm/software/helena/Makefile | 64 ++++++++--------- helm/software/helena/src/basic_rg/brgELPI.ml | 15 ++-- .../software/helena/src/basic_rg/brgOutput.ml | 6 +- .../helena/src/basic_rg/brgReduction.ml | 2 +- helm/software/helena/src/common/options.ml | 4 +- helm/software/helena/src/toplevel/top.ml | 69 ++++++++++--------- 6 files changed, 84 insertions(+), 76 deletions(-) diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 61891b69b..42cf240fc 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -39,73 +39,73 @@ PREAMBLE_V = coq/grundlagen.template PREAMBLE_ELPI = elpi/elpi.template test-si-fast: $(MAIN).opt etc - @echo " HELENA -o -q -1 $(INPUTFAST)" - $(H)./$(MAIN).opt -T 1 -n -o -q -1 $(O) $(INPUTFAST) > etc/log.txt + @echo " HELENA -q -u -x -1 $(INPUTFAST)" + $(H)./$(MAIN).opt -T 1 -q -u -x -1 $(O) $(INPUTFAST) > etc/log.txt test-si: $(MAIN).opt etc - @echo " HELENA -d -l -p -o $(INPUT)" - $(H)./$(MAIN).opt -T 2 -d -l -p -o $(O) $(INPUT) > etc/log.txt + @echo " HELENA -d -l -u -0 $(INPUT)" + $(H)./$(MAIN).opt -T 2 -d -l -u -0 $(O) $(INPUT) > etc/log.txt test2: $(MAIN).opt etc - @echo " HELENA -d -l $(INPUT)" - $(H)./$(MAIN).opt -l -o $(INPUT) -X -T 2 -d -l $(O) $(INPUT) > etc/log.txt + @echo " HELENA -T 2 -d -l $(INPUT)" + $(H)./$(MAIN).opt -l -u $(INPUT) -X -T 2 -d -l $(O) $(INPUT) > etc/log.txt test3: $(MAIN).opt etc - @echo " HELENA -d -l $(INPUT)" - $(H)./$(MAIN).opt -l -o $(INPUT) -X -T 3 -d -l $(O) $(INPUT) > etc/log.txt + @echo " HELENA -T 3 -d -l $(INPUT)" + $(H)./$(MAIN).opt -l -u $(INPUT) -X -T 3 -d -l $(O) $(INPUT) > etc/log.txt test6: $(MAIN).opt etc - @echo " HELENA -d -l $(INPUT)" - $(H)./$(MAIN).opt -l -o $(INPUT) -X -T 6 -d -l $(O) $(INPUT) > etc/log.txt + @echo " HELENA -T 6 -d -l -n $(INPUT)" + $(H)./$(MAIN).opt -l -u $(INPUT) -X -T 6 -d -l -n $(O) $(INPUT) > etc/log.txt xml-si: $(MAIN).opt etc - @echo " HELENA -l -o -s 1 -x $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -x $(INPUT) > etc/log.txt + @echo " HELENA -l -o -s 1 -u $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u $(INPUT) > etc/log.txt xml-si-v3: $(MAIN).opt etc - @echo " HELENA -l -o -s 2 -x $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -x $(INPUT) > etc/log.txt + @echo " HELENA -l -o -s 2 -u $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -u $(INPUT) > etc/log.txt xml: $(MAIN).opt etc - @echo " HELENA -l -s 1 -x $(INPUT)" - $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 1 -x $(INPUT) > etc/log.txt + @echo " HELENA -l -o -s 1 $(INPUT)" + $(H)./$(MAIN).opt -l -u $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 $(INPUT) > etc/log.txt xml-v3: $(MAIN).opt etc - @echo " HELENA -l -s 2 -x $(INPUT)" - $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 2 -x $(INPUT) > etc/log.txt + @echo " HELENA -l -o -s 2 $(INPUT)" + $(H)./$(MAIN).opt -l -u $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 $(INPUT) > etc/log.txt export-coq coq/$(V): $(MAIN).opt etc $(H)mkdir -p coq - @echo " HELENA -l -m V8 -o $(INPUT)" - $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_V) -l -m V8 -o $(O) $(INPUT) > etc/log.txt + @echo " HELENA -l -m V8 -u $(INPUT)" + $(H)./$(MAIN).opt -T 1 -a n -l -m V8 -p $(PREAMBLE_V) -u $(O) $(INPUT) > etc/log.txt export-matita matita/$(MA): $(MAIN).opt etc - @echo " HELENA -l -m MA2 -o $(INPUT)" + @echo " HELENA -l -m MA2 -u $(INPUT)" $(H)mkdir -p matita - $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_MA) -l -m MA2 -o $(O) $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -T 1 -a n -l -m MA2 -p $(PREAMBLE_MA) -u $(O) $(INPUT) > etc/log.txt export-elpi elpi/$(ELPI): $(MAIN).opt etc - @echo " HELENA -l -m ELPI -o $(INPUT)" + @echo " HELENA -l -m ELPI -u $(INPUT)" $(H)mkdir -p elpi - $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_ELPI) -l -m ELPI1 -o $(O) $(INPUT) > etc/log.txt - $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_ELPI) -l -m ELPI2 -o $(O) $(INPUT) >> etc/log.txt + $(H)./$(MAIN).opt -T 1 -a n -l -m ELPI1 -p $(PREAMBLE_ELPI) -u $(O) $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -T 1 -a n -l -m ELPI2 -p $(PREAMBLE_ELPI) -u $(O) $(INPUT) >> etc/log.txt profile-fast: $(MAIN).opt etc - @echo " HELENA -o -q $(INPUTFAST) (31 TIMES)" + @echo " HELENA -q -u -x $(INPUTFAST) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -n -o -q $(O) $(INPUTFAST) >> etc/log.txt; done + $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -q -u -x $(O) $(INPUTFAST) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt profile: $(MAIN).opt etc - @echo " HELENA -l -o $(INPUT) (31 TIMES)" + @echo " HELENA -l -u $(INPUT) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do ./$(MAIN).opt -T 1 -l -o $(O) $(INPUT) >> etc/log.txt; done + $(H)for _ in `seq 31`; do ./$(MAIN).opt -T 1 -l -u $(O) $(INPUT) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt profile-coq: $(MAIN).opt etc @echo " COQC $(V) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do `which time` -p -a -o etc/log.txt $(COQC) coq/$(V); done + $(H)for _ in `seq 31`; do `which time` -p -a -u etc/log.txt $(COQC) coq/$(V); done $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt matita: matita/$(MA) @@ -117,7 +117,7 @@ matitac: matita/$(MA) $(H)cd matita && $(MATITAC) $(MA) #profile-matita: $(MAIN).opt etc -# @echo " HELENA -o $(INPUT) (1 TIMES)" +# @echo " HELENA -u $(INPUT) (1 TIMES)" # $(H)rm -f etc/log.txt -# $(H)for T in `seq 1`; do ./$(MAIN).opt -T 1 -a n -l -m $(PREAMBLE) -o -x $(INPUT) >> etc/log.txt; done +# $(H)for T in `seq 1`; do ./$(MAIN).opt -T 1 -a n -l -m $(PREAMBLE) -o -u $(INPUT) >> etc/log.txt; done # $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt diff --git a/helm/software/helena/src/basic_rg/brgELPI.ml b/helm/software/helena/src/basic_rg/brgELPI.ml index 969cb8ae9..4e78eac13 100644 --- a/helm/software/helena/src/basic_rg/brgELPI.ml +++ b/helm/software/helena/src/basic_rg/brgELPI.ml @@ -111,8 +111,7 @@ let rec out_term st e och = function (* variant 1 *************************************************) let output_entity_1 och st (_, na, s, b) = -(* if na.E.n_apix <= 4500 then begin *) -(* out_comment och (KP.sprintf "constant %u" na.E.n_apix); *) + if na.E.n_apix <= !G.last then begin match b with | E.Abbr t -> KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s; @@ -121,7 +120,7 @@ let output_entity_1 och st (_, na, s, b) = KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s; uris := (false, s) :: !uris; !ok | E.Void -> C.err () -(* end else !ok *) + end else !ok let close_out_1 och () = let aux_sep _ = KP.fprintf och "%s" ")" in @@ -133,8 +132,7 @@ let close_out_1 och () = (* Variant 2 *************************************************) let output_entity_2 och st (_, na, s, b) = -(* out_comment och (KP.sprintf "constant %u" na.E.n_apix); *) -(* if na.E.n_apix <= 9 then begin *) + if na.E.n_apix <= !G.last then begin match b with | E.Abbr t -> KP.fprintf och "g+line %a c+%u\n %a\n.\n\n" @@ -145,7 +143,7 @@ let output_entity_2 och st (_, na, s, b) = out_uri s na.E.n_apix (out_term st B.empty) u; uris := (false, s) :: !uris; !ok | E.Void -> C.err () -(* end else !ok *) + end else !ok let close_out_2 och () = let aux_name (b, s) = @@ -153,6 +151,11 @@ let close_out_2 och () = KP.fprintf och "(%s %a\n" gde out_uri s in let aux_sep _ = KP.fprintf och "%s" ")" in + if !G.first > 0 then begin + let s = KP.sprintf "tv+c C T :- $lt C c+%u, !." !G.first in + out_clause och s; + out_clause och "tv+c C T :- tv+ T." + end; out_clause och "main :- grundlagen."; out_clause och "grundlagen :- (gv+ "; List.iter aux_name (List.rev !uris); diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index 5153ced07..6a40aecd4 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -9,6 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module KF = Filename module KP = Printf module U = NUri @@ -152,9 +153,10 @@ let rec pp_term st e och = function let _, _, a, b = B.get e i in KP.fprintf och "%a" (name err) a | B.GRef (_, s) -> - KP.fprintf och "$%s" (U.string_of_uri s) + let u = U.string_of_uri s in + KP.fprintf och "$%s" (if !G.short then KF.basename u else u) | B.Cast (_, u, t) -> - KP.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t + KP.fprintf och "<%a>.%a" (pp_term st e) u (pp_term st e) t | B.Appl (_, _, v, t) -> KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t | B.Bind (a, B.Abst (r, n, w), t) -> diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 6c5ac1e98..1a5a3f1cf 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -112,7 +112,7 @@ let rec step st m r = if !G.summary then O.add ~grt:1 (); step st (tstep m) w end else - m, r, None + m, r, None | _, _, _, E.Void -> assert false end diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index ffef0796e..89a085e5e 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -71,6 +71,8 @@ let last = ref max_int (* end trace here *) let extended = ref false (* extended applications *) +let short = ref false (* short global constants *) + let set_current_trace n = ct := if !first <= n && n <= !last then !trace else 0 @@ -94,6 +96,6 @@ let get_mk_uri () = let clear () = stage := 3; trace := 0; summary := false; first := 0; last := max_int; xdir := ""; kernel := V3; si := false; extended := false; cover := ""; - expand := false; indexes := false; icm := 0; unquote := false; + expand := false; indexes := false; icm := 0; unquote := false; short := false; debug_parser := false; debug_lexer := false; manager_dir := ""; manager := Quiet diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index 984933290..05320d3bc 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -359,42 +359,42 @@ let main = if !G.trace >= 1 then Y.utime_stamp "at exit" in let help = - "Usage: helena [ -LPVXdgilnopqtx1 | -Ts | -MO | -c | -ahkmr | -be ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXdgilnoqtux01 | -Ts | -MO | -p | -ahkmr | -be ]* [ ]*\n\n" ^ "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^ " 4 typing information, 5 conversion information, 6 reduction information,\n" ^ " 7 level disambiguation\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^ "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"elpi1\" \"elpi2\" (lambda-Prolog)\n" in - let help_L = " show lexer debug information" in - let help_M = " set location of output directory (manager) to (default: current directory)" in - let help_O = " set location of output directory (XML) to (default: current directory)" in - let help_P = " show parser debug information" in - let help_T = " set trace level (see above)" in - let help_V = " show version information" in - let help_X = " clear options" in + let help_L = " [lexer] Show lexer debug information" in + let help_M = " [manager] Set location of output directory (manager) to (default: current directory)" in + let help_O = " [output] Set location of output directory (XML) to (default: current directory)" in + let help_P = " [parser] Show parser debug information" in + let help_T = " [trace] Set trace level (see above)" in + let help_V = " [version] Show version information" in + let help_X = " Clear options" in - let help_a = " set prefix of numeric identifiers (default: empty)" in - let help_b = " begin trace at this global constant (default: first)" in - let help_c = " set preamble to this file (default: empty)" in - let help_d = " show summary information (requires trace >= 2)" in - let help_e = " end trace at this global constant (default: last)" in - let help_g = " always expand global definitions" in - let help_h = " set type hierarchy (default: \"Z1\")" in - let help_i = " show local references by index" in - let help_k = " set kernel version (default: \"V3\")" in - let help_l = " disambiguate binders layer (Automath)" in - let help_m = " export kernel entities for this manager (see above, default: no manager)" in - let help_n = " use extended (i.e. native) applications (Automath)" in - let help_o = " activate sort inclusion (default: false)" in - let help_p = " preprocess source (Automath)" in - let help_q = " disable quotation of identifiers" in - let help_r = " set initial segment of URI hierarchy (default: empty)" in - let help_s = " set translation stage (see above)" in - let help_t = " type check (version 1)" in - let help_x = " export kernel entities (XML)" in - - let help_1 = " parse files with streaming policy" in + let help_a = " [alpha] Set prefix of numeric identifiers (default: empty)" in + let help_b = " [begin] Begin trace at this global constant (default: first)" in + let help_d = " [data] Show summary information (requires trace >= 2)" in + let help_e = " [end] End trace at this global constant (default: last)" in + let help_g = " [global] Always expand global definitions (default: false)" in + let help_h = " [hierarchy] Set type hierarchy (default: \"Z1\")" in + let help_i = " [indexes] Show local references by index" in + let help_k = " [kernel] Set kernel version (default: \"V3\")" in + let help_l = " [layer] Disambiguate binders layer (Automath)" in + let help_m = " [manager] Export kernel entities for this manager (see above, default: no manager)" in + let help_n = " [names] Show short constants (default: qualified constants)" in + let help_o = " [objects] Export kernel entities (XML)" in + let help_p = " [preamble] Set preamble to this file (default: empty)" in + let help_q = " [quote] Disable quotation of identifiers (default: false)" in + let help_r = " [root] Set initial segment of URI hierarchy (default: empty)" in + let help_s = " [stage] Set translation stage (see above)" in + let help_t = " [type] Type check (default: validate)" in + let help_u = " [upsilon] Activate type comparison by sort inclusion (default: false)" in + let help_x = " [extended] Use extended applications (Automath)" in + let help_0 = " [zero] Preprocess source (Automath)" in + let help_1 = " [one] parse files with streaming policy" in at_exit exit; Arg.parse [ ("-L", Arg.Set G.debug_lexer, help_L); @@ -406,7 +406,6 @@ let main = ("-X", Arg.Unit clear_options, help_X); ("-a", Arg.String ((:=) G.alpha), help_a); ("-b", Arg.Int ((:=) G.first), help_b); - ("-c", Arg.String ((:=) G.preamble), help_c); ("-d", Arg.Unit set_summary, help_d); ("-e", Arg.Int ((:=) G.last), help_e); ("-g", Arg.Set G.expand, help_g); @@ -415,13 +414,15 @@ let main = ("-k", Arg.String set_kernel, help_k); ("-l", Arg.Set G.cc, help_l); ("-m", Arg.String set_manager, help_m); - ("-n", Arg.Set G.extended, help_n); - ("-o", Arg.Set G.si, help_o); - ("-p", Arg.Unit set_preprocess, help_p); + ("-n", Arg.Set G.short, help_n); + ("-o", Arg.Set export, help_o); + ("-p", Arg.String ((:=) G.preamble), help_p); ("-q", Arg.Set G.unquote, help_q); ("-r", Arg.String ((:=) root), help_r); ("-s", Arg.Int ((:=) G.stage), help_s); ("-t", Arg.Clear version, help_t); - ("-x", Arg.Set export, help_x); + ("-u", Arg.Set G.si, help_u); + ("-x", Arg.Set G.extended, help_x); + ("-0", Arg.Unit set_preprocess, help_0); ("-1", Arg.Set streaming, help_1); ] process_file help -- 2.39.2