From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 6 Jul 2015 21:52:17 +0000 (+0000)
Subject: - multi-file exportation for teyjus
X-Git-Tag: make_still_working~709
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e7cbf3ee4fc73e3e95f337f020186652315cf4a8;p=helm.git

- multi-file exportation for teyjus
- more profiling for helena and coq
---

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 =