From e7cbf3ee4fc73e3e95f337f020186652315cf4a8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 6 Jul 2015 21:52:17 +0000 Subject: [PATCH] - multi-file exportation for teyjus - more profiling for helena and coq --- helm/software/helena/profile.txt | 10 +++ helm/software/helena/src/basic_rg/brgLP.ml | 86 +++++++++++++++++----- 2 files changed, 77 insertions(+), 19 deletions(-) diff --git a/helm/software/helena/profile.txt b/helm/software/helena/profile.txt index a0ff3f28c..28c8b8950 100644 --- a/helm/software/helena/profile.txt +++ b/helm/software/helena/profile.txt @@ -1,11 +1,21 @@ helena.opt : 01.14 to 01.18 (optimized, 2nd run) ages => 904871 beta-steps helena.byte: 08.73 to 08.77 (optimized, 2nd run) ages +helena.opt : 00.44 to 00.52 (optimized, 1st run) ages (just validation) +helena.opt : 00.50 to 00.53 (optimized, 2st run) ages (just validation) +helena.byte: 05.33 to 05.40 (optimized, 1st run) ages (just validation) +helena.byte: 05.54 to 05.58 (optimized, 2nd run) ages (just validation) + helena.opt : 01.50 to 01.54 (optimized, 2nd run) no ages => 1423268 beta-steps coqtop.opt : 24.26 to 24.43 no ages coqtop.byte: 94.18 to 95.78 no ages +coqtop.opt : 14.91 to 15.79 no ages (just validation) +coqtop.byte: 51.63 to 53.76 no ages (just validation) + +coqtop.opt : 29.55 to 31.33 no ages, typed definitions + coqtop.opt : 27.73 to 28.07 ages coqtop.opt : 28.64 to 28.83 reversed ages diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml index 9b832b20e..ac7acd908 100644 --- a/helm/software/helena/src/basic_rg/brgLP.ml +++ b/helm/software/helena/src/basic_rg/brgLP.ml @@ -28,14 +28,19 @@ let ok = ref true let uris = ref [] +let chunk = ref 0 + +let sub_och = ref stdout + let top_age = 7000 -let size = 16 +let size = 250 let base = "lp" let ext_lp = ".elpi" let ext_tj = ".mod" +let ext_tj_sig = ".sig" let reserved = ["pi"; "sigma"; "nil"; "delay"; "in"; "with"; "resume"; "context"] @@ -169,41 +174,85 @@ let close_out_lp2 och () = (* teyjus variant 2 *************************************************) +let append_out name = + open_out_gen [Open_append; Open_creat; Open_text] 0o666 name + +let sub_close () = if !sub_och <> stdout then close_out !sub_och + +let mk_name chunk = + let dir = KF.concat !G.manager_dir base in + let name = KP.sprintf "grundlagen%02u" chunk in + dir, name + let output_entity_tj2 och st (_, na, u, b) = if na.E.n_apix <= !G.last then begin - out_comment och (KP.sprintf "constant %u" na.E.n_apix); + if pred na.E.n_apix mod size = 0 then begin + sub_close (); + incr chunk; + let dir, name = mk_name !chunk in + let soch = open_out (KF.concat dir name ^ ext_tj_sig) in + out_preamble soch; + out_top_comment soch (KP.sprintf "This file was generated by %s: do not edit" G.version_string); + out_clause soch (KP.sprintf "sig %s." name); + out_clause soch "accum_sig grundlagen."; + out_clause soch (KP.sprintf "type line+%02u t -> int -> t -> o." !chunk); + close_out soch; + let soch = open_out (KF.concat dir name ^ ext_tj) in + out_preamble soch; + out_top_comment soch (KP.sprintf "This file was generated by %s: do not edit" G.version_string); + out_clause soch (KP.sprintf "module %s." name); + sub_och := soch + end; + out_comment !sub_och (KP.sprintf "constant %u" na.E.n_apix); match b with | E.Abbr v -> - KP.fprintf och "g+line %a %u\n %a\n.\n\n" - out_uri u (top_age - na.E.n_apix) (out_term st B.empty) v; + KP.fprintf !sub_och "line+%02u %a %u\n %a\n.\n\n" + !chunk out_uri u (top_age - na.E.n_apix) (out_term st B.empty) v; uris := (true, u) :: !uris; !ok | E.Abst w -> - KP.fprintf och "g+line %a %u\n %a\n.\n\n" - out_uri u (top_age - na.E.n_apix) (out_term st B.empty) w; + KP.fprintf !sub_och "line+%02u %a %u\n %a\n.\n\n" + !chunk out_uri u (top_age - na.E.n_apix) (out_term st B.empty) w; uris := (false, u) :: !uris; !ok | E.Void -> C.err () end else !ok let close_out_tj2 och () = - let out_name (b, u) = + let out_name och (b, u) = let gde = if b then "gdef+2" else "gdec+2" in KP.fprintf och "(%s %a\n" gde out_uri u in let rec out_pars och p = if p > 0 then begin KP.fprintf och "%s" ")"; out_pars och (pred p) end in - let rec out_list och chunk pars first items uris = match first, items, uris with + let rec out_list chunk pars first items uris = match first, items, uris with | true, _, _ -> - KP.fprintf och "g+list %u\n" chunk; - out_list och (succ chunk) pars false items uris - | false, _, [] -> KP.fprintf och "gtop%a.\n\n" out_pars pars + let dir, name = mk_name chunk in + let soch = append_out (KF.concat dir name ^ ext_tj) in + out_clause soch (KP.sprintf "g+line R C T :- line+%02u R C T, !." chunk); + KP.fprintf soch "g+list %u\n" chunk; + sub_och := soch; + out_list (succ chunk) pars false items uris + | false, _, [] -> + KP.fprintf !sub_och "gtop%a.\n\n" out_pars pars; + sub_close () | false, 0, _ -> - KP.fprintf och "(genv %u)%a.\n\n" chunk out_pars pars; - out_list och chunk 0 true size uris + KP.fprintf !sub_och "(genv %u)%a.\n\n" chunk out_pars pars; + sub_close (); + out_list chunk 0 true size uris | false, _, hd :: tl -> - out_name hd; out_list och chunk (succ pars) false (pred items) tl + out_name !sub_och hd; out_list chunk (succ pars) false (pred items) tl in - out_list och 1 0 true size (List.rev !uris); + let rec out_accumulate c = + if !chunk < c then KP.fprintf och "\n" else begin + let _, name = mk_name c in + KP.fprintf och "accumulate %s.\n" name; + out_accumulate (succ c) + end + in + sub_close (); + out_list 1 0 true size (List.rev !uris); + KP.fprintf och "accumulate helena.\n"; + out_accumulate 1; out_clause och "main :- grundlagen."; out_clause och "grundlagen :- gv+ (genv 1)."; close_out och @@ -279,13 +328,12 @@ let open_out_lp2 fname = output_entity_lp2 och, close_out_lp2 och let open_out_tj2 fname = - let dir = KF.concat !G.manager_dir base in - let path = KF.concat dir fname in - let och = open_out (path ^ "2" ^ ext_tj) in + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname ^ "2" in + let och = open_out (path ^ ext_tj) in out_preamble och; out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string); out_clause och "module grundlagen."; - out_clause och "accumulate helena."; output_entity_tj2 och, close_out_tj2 och let open_out_tj3 fname = -- 2.39.2