From: Ferruccio Guidi Date: Mon, 29 Jun 2015 20:29:12 +0000 (+0000) Subject: we are optimizing the code by conditional compilation. X-Git-Tag: make_still_working~714 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b37863d4598516a06241f18ad0db963399015bf2;p=helm.git we are optimizing the code by conditional compilation. three tags introduced so far: EXPAND, PREPROCESS, MANAGER --- diff --git a/helm/software/helena/Makefile.common b/helm/software/helena/Makefile.common index 0db660fe6..0fdcc05d6 100644 --- a/helm/software/helena/Makefile.common +++ b/helm/software/helena/Makefile.common @@ -13,8 +13,12 @@ DIRECTORIES = $(addprefix $(SRC)/,$(shell cat $(SRC)/Make)) INCLUDES = $(DIRECTORIES:%=-I %) -OCAMLDEP = $(OCAMLFIND) ocamldep -native $(INCLUDES) -OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(INCLUDES) +CAMLP = -pp "camlp5o pa_macro.cmo $(CAMLPOPTIONS)" + +CAMLPOPTIONS = $(F:%=-D%) + +OCAMLDEP = $(OCAMLFIND) ocamldep $(CAMLP) -native $(INCLUDES) +OCAMLOPT = $(OCAMLFIND) opt $(CAMLP) $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(INCLUDES) OCAMLLEX = ocamllex.opt OCAMLYACC = ocamlyacc -v TAR = tar -czf etc/$(MAIN:%=%.tgz) diff --git a/helm/software/helena/README b/helm/software/helena/README index ddbd506ad..88067dee8 100644 --- a/helm/software/helena/README +++ b/helm/software/helena/README @@ -1,6 +1,13 @@ -Helena 0.8.2 M +Helena 0.8.3 M + + ::= + +EXPAND enable option -g (if unset, -g is disabled) +MANAGER enable options -M -m -p (if unset, -m is disabled) +PREPROCESS enable option (if unset, -0 is disabled) * type "make" or "make opt" to compile the native executable + with the desired features listed in the variable F * type "make clean" to remove the products of compilation diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 22b3e799c..637aa4a89 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -119,8 +119,11 @@ let add_proj at e t = match e with | D.ESort -> t | D.EBind (D.ESort, a, b) -> D.TBind (E.compose a at, b, t) | _ -> - let e = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start at e else e in +IFDEF MANAGER OR OBJS THEN + D.TProj (at, D.set_attrs C.start at e, t) +ELSE D.TProj (at, e, t) +END (* this is not tail recursive in the GRef branch *) let rec xlate_term f st lst y lenv = function @@ -170,8 +173,11 @@ let rec xlate_term f st lst y lenv = function let a = E.compose av a in f a (D.TAppl (a, x, v, gref)) | args -> - let args = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start a args else args in +IFDEF MANAGER OR OBJS THEN + f a (D.TProj (a, D.set_attrs C.start a args, gref)) +ELSE f a (D.TProj (a, args, gref)) +END in let f args = C.list_fold_right f map2 args D.ESort in D.sub_list_strict (D.fold_names f map1 args) cnt args diff --git a/helm/software/helena/src/basic_rg/brgEnvironment.ml b/helm/software/helena/src/basic_rg/brgEnvironment.ml index 1b3f744e2..231027ad8 100644 --- a/helm/software/helena/src/basic_rg/brgEnvironment.ml +++ b/helm/software/helena/src/basic_rg/brgEnvironment.ml @@ -21,9 +21,14 @@ let env = UH.create hsize (* decps *) let set_entity entity = +IFDEF EXPAND THEN let ra, na, uri, b = entity in let entity0 = if !G.expand then ra, {na with E.n_apix = 0}, uri, b else entity in UH.add env uri entity0; entity +ELSE + let _, _, uri, _ = entity in + UH.add env uri entity; entity +END let get_entity uri = try UH.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml index bdb78144a..b8274ca30 100644 --- a/helm/software/helena/src/basic_rg/brgGallina.ml +++ b/helm/software/helena/src/basic_rg/brgGallina.ml @@ -20,6 +20,8 @@ module E = Entity module R = Alpha module B = Brg +IFDEF MANAGER THEN + (* Internal functions *******************************************************) let ok = ref true @@ -130,3 +132,5 @@ let open_out fname = out_preamble och; out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string); output_entity och, close_out och + +END diff --git a/helm/software/helena/src/basic_rg/brgGallina.mli b/helm/software/helena/src/basic_rg/brgGallina.mli index d96b7f45d..1b68ccedb 100644 --- a/helm/software/helena/src/basic_rg/brgGallina.mli +++ b/helm/software/helena/src/basic_rg/brgGallina.mli @@ -9,4 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF MANAGER THEN + val open_out: string -> Brg.manager + +END diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml index b1cfe21ca..6aa4ac34d 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.ml +++ b/helm/software/helena/src/basic_rg/brgGrafite.ml @@ -20,6 +20,8 @@ module E = Entity module R = Alpha module B = Brg +IFDEF MANAGER THEN + (* Internal functions *******************************************************) let ok = ref true @@ -125,3 +127,5 @@ let open_out fname = out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string); out_include och "basics/pts"; output_entity och, close_out och + +END diff --git a/helm/software/helena/src/basic_rg/brgGrafite.mli b/helm/software/helena/src/basic_rg/brgGrafite.mli index d96b7f45d..1b68ccedb 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.mli +++ b/helm/software/helena/src/basic_rg/brgGrafite.mli @@ -9,4 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF MANAGER THEN + val open_out: string -> Brg.manager + +END diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml index 0eb193b7d..857d5ccac 100644 --- a/helm/software/helena/src/basic_rg/brgLP.ml +++ b/helm/software/helena/src/basic_rg/brgLP.ml @@ -20,6 +20,8 @@ module E = Entity module R = Alpha module B = Brg +IFDEF MANAGER THEN + (* Internal functions *******************************************************) let ok = ref true @@ -281,3 +283,5 @@ let open_out_tj3 fname = out_clause och "module grundlagen."; out_clause och "accumulate helena."; output_entity_tj3 och, close_out_tj3 och + +END diff --git a/helm/software/helena/src/basic_rg/brgLP.mli b/helm/software/helena/src/basic_rg/brgLP.mli index 1fb878c17..c56c6c079 100644 --- a/helm/software/helena/src/basic_rg/brgLP.mli +++ b/helm/software/helena/src/basic_rg/brgLP.mli @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF MANAGER THEN + val open_out_lp1: string -> Brg.manager val open_out_lp2: string -> Brg.manager @@ -16,3 +18,5 @@ val open_out_lp2: string -> Brg.manager val open_out_tj2: string -> Brg.manager val open_out_tj3: string -> Brg.manager + +END diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index b2dc97292..415d0b02a 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -49,8 +49,6 @@ let cover = ref "" (* initial uri segment *) let cc = ref false (* activate conversion constraints *) -let expand = ref false (* always expand global definitions *) - let indexes = ref false (* show de Bruijn indexes *) let icm = ref 0 (* complexity measure of relocated terms *) @@ -61,12 +59,6 @@ let debug_parser = ref false (* output parser debug information *) let debug_lexer = ref false (* output lexer debug information *) -let manager_dir = ref "" (* output directory for manager *) - -let manager = ref Quiet (* manager *) - -let preamble = ref "" (* preamble file for manager *) - let alpha = ref "" (* prefix of numeric identifiers *) let first = ref 0 (* begin trace here *) @@ -79,6 +71,20 @@ let infinity = ref false (* use ∞-abstractions in contexts *) let short = ref false (* short global constants *) +IFDEF EXPAND THEN +let expand = ref false (* always expand global definitions *) +END + +IFDEF PREPROCESS THEN +let preprocess = ref false (* preprocess source *) +END + +IFDEF MANAGER THEN +let manager_dir = ref "" (* output directory for manager *) +let manager = ref Quiet (* manager *) +let preamble = ref "" (* preamble file for manager *) +END + let set_current_trace n = ct := if !first <= n && n <= !last then !trace else 0 @@ -102,6 +108,8 @@ let get_mk_uri () = let clear () = stage := 3; trace := 0; summary := false; export := false; first := 0; last := max_int; xdir := ""; kernel := V3; si := false; extended := false; infinity := false; cover := ""; - expand := false; indexes := false; icm := 0; unquote := false; short := false; + indexes := false; icm := 0; unquote := false; short := false; debug_parser := false; debug_lexer := false; - manager_dir := ""; manager := Quiet + IFDEF EXPAND THEN expand := false ELSE () END; + IFDEF MANAGER THEN manager_dir := ""; manager := Quiet; preamble := "" ELSE () END; + IFDEF PREPROCESS THEN preprocess := false ELSE () END diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index 641871603..4641af458 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -10,8 +10,10 @@ V_______________________________________________________________ *) module KF = Filename +module KL = List module KP = Printf module KS = String +module KT = String module U = NUri module C = Cps @@ -137,6 +139,8 @@ let validate st k = | BagEntity _ -> st | CrgEntity _ -> st +IFDEF MANAGER THEN + let manager st output_entity = function | BrgEntity entity -> if output_entity st.kst entity then st else @@ -144,6 +148,8 @@ let manager st output_entity = function | BagEntity _ -> st | CrgEntity _ -> st +END + (* extended lexer ***********************************************************) type 'token lexer = { @@ -217,7 +223,6 @@ let count_input st = function (****************************************************************************) let version = ref true -let preprocess = ref false let root = ref "" let st = ref (initial_status ()) let streaming = ref false (* parsing style (temporary) *) @@ -230,9 +235,13 @@ let process_2 st entity = else st in if !G.export then export_entity st entity; +IFDEF MANAGER THEN match st.mst with | None -> st | Some (export_entity, _) -> manager st export_entity entity +ELSE + st +END let process_1 st entity = if !G.ct >= 3 then pp_progress entity; @@ -255,7 +264,11 @@ let process_0 st entity = | NoEntity -> assert false in let st = if !G.summary then count_input st entity else st in - if !preprocess then process_input f st entity else f st entity +IFDEF PREPROCESS THEN + if !G.preprocess then process_input f st entity else f st entity +ELSE + f st entity +END let process_nostreaming st lexbuf input = let id x = x in @@ -278,6 +291,26 @@ let process_streaming st lexbuf input = (****************************************************************************) +IFDEF PREPROCESS THEN + +let set_preprocess () = + if !G.trace >= 2 then begin G.preprocess := true; G.summary := true end + +END + +IFDEF MANAGER THEN + +let set_manager s = match KS.lowercase s with + | "v8" -> G.manager := G.Coq + | "ma2" -> G.manager := G.Matita + | "lp1" -> G.manager := G.LP1 + | "lp2" -> G.manager := G.LP2 + | "tj2" -> G.manager := G.TJ2 + | "tj3" -> G.manager := G.TJ3 + | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) + +END + let process st name = let process = if !streaming then process_streaming else process_nostreaming in let input = type_of_input name in @@ -288,7 +321,17 @@ let process st name = st, input let main = - let print_version () = L.warn level (G.version_string ^ "\n"); exit 0 in + let print_version () = + let features = [ +(IFDEF EXPAND THEN "EXPAND" ELSE "" END); +(IFDEF MANAGER THEN "MANAGER" ELSE "" END); +(IFDEF PREPROCESS THEN "PREPROCESS" ELSE "" END); + ] in + let map s = s <> "" in + let features_string = KT.concat " " (KL.filter map features) in + L.warn level (KP.sprintf "%s [%s]" G.version_string features_string); + exit 0 + in let set_hierarchy s = if H.set_graph s then () else L.warn level (KP.sprintf "Unknown type hierarchy: %s" s) @@ -303,30 +346,26 @@ let main = if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit"; G.trace := i; if i <= 1 then G.summary := false; - if i <= 1 then preprocess := false +IFDEF PREPROCESS THEN + if i <= 1 then G.preprocess := false +ELSE + () +END in let set_summary () = if !G.trace >= 2 then G.summary := true - in - let set_preprocess () = - if !G.trace >= 2 then begin preprocess := true; G.summary := true end - in - let set_manager s = match KS.lowercase s with - | "v8" -> G.manager := G.Coq - | "ma2" -> G.manager := G.Matita - | "lp1" -> G.manager := G.LP1 - | "lp2" -> G.manager := G.LP2 - | "tj2" -> G.manager := G.TJ2 - | "tj3" -> G.manager := G.TJ3 - | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) in let clear_options () = - preprocess := false; root := ""; G.clear (); H.clear (); O.clear_reductions (); streaming := false; version := true in + let undefined opt () = + L.warn level (KP.sprintf "%s was compiled without the support for option %s" G.version_string opt); + exit 0 + in + let arg_undefined opt = Arg.Unit (undefined opt) in let process_file name = if !G.trace >= 2 then L.warn 1 (KP.sprintf "Processing file: %s" name); if !G.trace >= 2 then Y.utime_stamp "started"; @@ -334,6 +373,7 @@ let main = let cover = KF.concat !root base_name in if !G.stage <= 1 then G.kernel := G.V4; G.cover := cover; +IFDEF MANAGER THEN begin match !G.manager with | G.Coq -> st := {!st with mst = Some (BA.open_out base_name)} | G.Matita -> st := {!st with mst = Some (BG.open_out base_name)} @@ -342,7 +382,10 @@ let main = | G.TJ2 -> st := {!st with mst = Some (BP.open_out_tj2 base_name)} | G.TJ3 -> st := {!st with mst = Some (BP.open_out_tj3 base_name)} | G.Quiet -> () - end; + end +ELSE + () +END; P.clear_marks (); let sst, input = process (refresh_status !st) name in st := begin match sst.mst with @@ -352,7 +395,11 @@ let main = if !G.trace >= 2 then Y.utime_stamp "processed"; if !G.summary then begin AO.print_counters C.start !st.ac; - if !preprocess then AO.print_process_counters C.start !st.pst; +IFDEF PREPROCESS THEN + if !G.preprocess then AO.print_process_counters C.start !st.pst +ELSE + () +END; if !G.stage >= 1 then print_counters !st G.V4; if !G.stage >= 2 then print_counters !st !G.kernel; if !G.stage >= 3 then O.print_reductions () @@ -402,7 +449,7 @@ let main = at_exit exit; Arg.parse [ ("-L", Arg.Set G.debug_lexer, help_L); - ("-M", Arg.String ((:=) G.manager_dir), help_M); + ("-M", (IFDEF MANAGER THEN Arg.String ((:=) G.manager_dir) ELSE arg_undefined "-M" END), help_M); ("-O", Arg.String ((:=) G.xdir), help_O); ("-P", Arg.Set G.debug_parser, help_P); ("-T", Arg.Int set_trace, help_T); @@ -412,15 +459,15 @@ let main = ("-b", Arg.Int ((:=) G.first), help_b); ("-d", Arg.Unit set_summary, help_d); ("-e", Arg.Int ((:=) G.last), help_e); - ("-g", Arg.Set G.expand, help_g); + ("-g", (IFDEF EXPAND THEN Arg.Set G.expand ELSE arg_undefined "-g" END), help_g); ("-h", Arg.String set_hierarchy, help_h); ("-i", Arg.Set G.indexes, help_i); ("-k", Arg.String set_kernel, help_k); ("-l", Arg.Set G.cc, help_l); - ("-m", Arg.String set_manager, help_m); + ("-m", (IFDEF MANAGER THEN Arg.String set_manager ELSE arg_undefined "-m" END), help_m); ("-n", Arg.Set G.short, help_n); ("-o", Arg.Set G.export, help_o); - ("-p", Arg.String ((:=) G.preamble), help_p); + ("-p", (IFDEF MANAGER THEN Arg.String ((:=) G.preamble) ELSE arg_undefined "-p" END), help_p); ("-q", Arg.Set G.unquote, help_q); ("-r", Arg.String ((:=) root), help_r); ("-s", Arg.Int ((:=) G.stage), help_s); @@ -428,6 +475,6 @@ let main = ("-u", Arg.Set G.si, help_u); ("-x", Arg.Set G.extended, help_x); ("-y", Arg.Set G.infinity, help_y); - ("-0", Arg.Unit set_preprocess, help_0); + ("-0", (IFDEF PREPROCESS THEN Arg.Unit set_preprocess ELSE arg_undefined "-0" END), help_0); ("-1", Arg.Set streaming, help_1); ] process_file help