X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgLP.ml;h=8a8f9d4f296d160550d91cf5e6320f26ce67f003;hb=fdb80b08af83b86759833142456ce3c4f84cd80e;hp=857d5ccacb121efc3f9161066db552292b4a2486;hpb=b37863d4598516a06241f18ad0db963399015bf2;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml
index 857d5ccac..8a8f9d4f2 100644
--- a/helm/software/helena/src/basic_rg/brgLP.ml
+++ b/helm/software/helena/src/basic_rg/brgLP.ml
@@ -24,16 +24,25 @@ IFDEF MANAGER THEN
 
 (* Internal functions *******************************************************)
 
+let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
+
 let ok = ref true
 
+let uris = ref []
+
+let chunk = ref 0
+
+let sub_och = ref stdout
+
 let top_age = 7000
 
-let uris = ref []
+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"]
 
@@ -78,22 +87,22 @@ let out_name och a =
    E.name err f a
 
 let rec out_term st e och = function
-   | B.Sort (_, h)                   ->
-      let sort = if h = 0 then "k+set" else if h = 1 then "k+prop" else assert false in
+   | B.Sort k                        ->
+      let sort = if k = 0 then "k+set" else if k = 1 then "k+prop" else assert false in
       KP.fprintf och "(sort %s)" sort
    | B.LRef (_, i)                   ->
-      let _, _, a, b = B.get e i in
-      KP.fprintf och "%a" out_name a
+      let _, _, _, y, b = B.get e i in
+      KP.fprintf och "%a" out_name y
    | B.GRef (_, s)                   ->
       KP.fprintf och "%a" out_uri s
-   | B.Cast (_, u, t)                ->
+   | B.Cast (u, t)                   ->
       KP.fprintf och "(cast %a %a)" (out_term st e) u (out_term st e) t 
-   | B.Appl (_, x, v, t)             ->
+   | B.Appl (x, v, t)                ->
       let c = if x then "appx" else "appr" in
       KP.fprintf och "(%s %a %a)" c (out_term st e) v (out_term st e) t
-   | B.Bind (a, B.Abst (r, n, w), t) ->
-      let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.abst r n w) in
+   | B.Bind (y, B.Abst (r, n, w), t) ->
+      let y = R.alpha B.mem e y in
+      let ee = B.push e B.empty E.empty_node y (B.abst r n w) in
       let c = if r then "prod" else "abst" in
       let l = match N.to_string st n with
          | "1" -> "l+1"
@@ -101,17 +110,13 @@ let rec out_term st e och = function
          | _   -> ok := false; "?"
       in
       KP.fprintf och "(%s %s %a %a\\ %a)"
-         c l (out_term st e) w out_name a (out_term st ee) t
-   | B.Bind (a, B.Abbr v, t)         ->
-      let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.abbr v) in
+         c l (out_term st e) w out_name y (out_term st ee) t
+   | B.Bind (y, B.Abbr v, t)         ->
+      let y = R.alpha B.mem e y in
+      let ee = B.push e B.empty E.empty_node y (B.abbr v) in
       KP.fprintf och "(abbr %a %a\\ %a)"
-          (out_term st e) v out_name a (out_term st ee) t
-   | B.Bind (a, B.Void, t)   ->
-      let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.Void) in
-      KP.fprintf och "(void %a\\ %a)"
-          out_name a (out_term st ee) t
+          (out_term st e) v out_name y (out_term st ee) t
+   | B.Bind (_, B.Void, _)           -> C.err ()
 
 (* elpi variant 1 ***********************************************************)
 
@@ -171,38 +176,87 @@ 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 version;
+      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 version;
+      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 aux_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 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;
+   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 chunk pars first items uris = match first, items, uris with
+      | true, _, _         ->
+         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 !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 !sub_och hd; out_list chunk (succ pars) false (pred items) tl
+   in
+   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+";
-   List.iter aux_name (List.rev !uris);
-   KP.fprintf och "%s" "gtop";
-   List.iter aux_sep !uris;
-   out_clause och "\n\n.";
+   out_clause och "grundlagen :- gv+ (genv 1).";
    close_out och
 
 (* teyjus variant 3 *************************************************)
@@ -230,18 +284,29 @@ let output_entity_tj3 och st (_, na, u, b) =
    end else !ok
 
 let close_out_tj3 och () =
-   let aux_name (_, u) =
+   let out_name (_, u) =
       KP.fprintf och "gv+3 %a,\n" out_uri u
    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;
+   let rec out_list och chunk first items uris = match first, items, uris with
+      | true, _, _         ->
+         KP.fprintf och "chunk %u :-\n" chunk;
+         out_list och (succ chunk) false items uris
+      | false, _, []       -> KP.fprintf och "!.\n\n"; chunk
+      | false, 0, _        ->
+         KP.fprintf och "!.\n\n";
+         out_list och chunk true size uris
+      | false, _, hd :: tl ->
+         out_name hd; out_list och chunk false (pred items) tl
+   in
+   let rec out_chunks och chunks c =
+      if chunks < c then out_clause och "!." else begin
+         KP.fprintf och "chunk %u,\n" c; out_chunks och chunks (succ c)
+      end
+   in
+   let chunks = out_list och 1 true size (List.rev !uris) in
    out_clause och "main :- grundlagen.";
-   out_clause och "grundlagen :-";
-   List.iter aux_name (List.rev !uris);
-   out_clause och "!.";
+   KP.fprintf och "grundlagen :-\n";
+   out_chunks och (pred chunks) 1;
    close_out och
 
 (* Interface functions ******************************************************)
@@ -251,7 +316,8 @@ let open_out_lp1 fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ "1" ^ ext_lp) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
+   out_clause och "accumulate helena.";
    out_clause och "main :- grundlagen.";
    out_clause och "grundlagen :- gv+";
    output_entity_lp1 och, close_out_lp1 och
@@ -261,17 +327,17 @@ let open_out_lp2 fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ "2" ^ ext_lp) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
+   out_clause och "accumulate helena.";
    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_top_comment och version;
    out_clause och "module grundlagen.";
-   out_clause och "accumulate helena.";
    output_entity_tj2 och, close_out_tj2 och
 
 let open_out_tj3 fname =
@@ -279,7 +345,7 @@ let open_out_tj3 fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ "3" ^ 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_top_comment och version;
    out_clause och "module grundlagen.";
    out_clause och "accumulate helena.";
    output_entity_tj3 och, close_out_tj3 och