From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 5 Jul 2015 14:36:36 +0000 (+0000)
Subject: more flexibility in the exported data for Teyjus
X-Git-Tag: make_still_working~710
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c88b410bfaf8d232402511b81e88625309c42412;p=helm.git

more flexibility in the exported data for Teyjus
---

diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 137084bf9..02604aae8 100644
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -155,8 +155,8 @@ export-lp2 lp/$(LP2): $(MAIN).opt etc
 	$(H)./$(MAIN).opt -a n -m LP2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt
 
 export-tj2 lp/$(TJ2): $(MAIN).opt etc
-	@echo "  HELENA -l -m TJ2 -u $(INPUT)"
-	$(H)./$(MAIN).opt -a n -e 253 -m TJ2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt
+	@echo "  HELENA -m TJ2 $(INPUT)"
+	$(H)./$(MAIN).opt -a n -m TJ2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt
 
 export-tj3 lp/$(TJ3): $(MAIN).opt etc
 	@echo "  HELENA -m TJ3 $(INPUT)"
diff --git a/helm/software/helena/profile.txt b/helm/software/helena/profile.txt
index 65c909fe6..a0ff3f28c 100644
--- a/helm/software/helena/profile.txt
+++ b/helm/software/helena/profile.txt
@@ -10,11 +10,11 @@ coqtop.opt : 27.73 to 28.07 ages
 
 coqtop.opt : 28.64 to 28.83 reversed ages
 
-elpi       : 00.19 to 00.20 exex, 253 lines
-elpi       : 00.26 to 00.28 user, 253 lines
+elpi       : 00.20 to 00.22 exex, 255 lines
+elpi       : 00.27 to 00.31 user, 255 lines
 
-teyjus     : 02.03 to 02.18 exec, 253 lines
-teyjus     : 01.63 to 01.68 link, 253 lines
+teyjus     : 02.13 to 02.26 exec, 255 lines
+teyjus     : 03.24 to 03.31 link, 255 lines
 
 elpi       : 21.15 to 21.45 exec, full
 elpi       : 27.52 to 27.82 user, full
diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml
index 1eb1bae3d..9b832b20e 100644
--- a/helm/software/helena/src/basic_rg/brgLP.ml
+++ b/helm/software/helena/src/basic_rg/brgLP.ml
@@ -26,9 +26,11 @@ IFDEF MANAGER THEN
 
 let ok = ref true
 
+let uris = ref []
+
 let top_age = 7000
 
-let uris = ref []
+let size = 16
 
 let base = "lp"
 
@@ -183,22 +185,27 @@ let output_entity_tj2 och st (_, na, u, b) =
    end else !ok
 
 let close_out_tj2 och () =
-   let aux_name (b, u) =
+   let out_name (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 och 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
+      | false, 0, _        ->
+         KP.fprintf och "(genv %u)%a.\n\n" chunk out_pars pars;
+         out_list och chunk 0 true size uris
+      | false, _, hd :: tl ->
+         out_name hd; out_list och chunk (succ pars) false (pred items) tl
+   in
+   out_list och 1 0 true size (List.rev !uris);
    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 *************************************************)
@@ -226,18 +233,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 ******************************************************)