]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgLP.ml
more flexibility in the exported data for Teyjus
[helm.git] / helm / software / helena / src / basic_rg / brgLP.ml
index 1eb1bae3d3ca318460966533aced18a80525e127..9b832b20e1b546ed1bc8b682a96dcf36300fb77e 100644 (file)
@@ -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 ******************************************************)