]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgELPI.ml
command line options rearranged
[helm.git] / helm / software / helena / src / basic_rg / brgELPI.ml
index 969cb8ae99f8c7e298abe89699a3ee021bd0d34e..4e78eac13a0986eef5e98510b568a3333442c5fd 100644 (file)
@@ -111,8 +111,7 @@ let rec out_term st e och = function
 (* variant 1 *************************************************)
 
 let output_entity_1 och st (_, na, s, b) =
-(*   if na.E.n_apix <= 4500 then begin *)
-(*   out_comment och (KP.sprintf "constant %u" na.E.n_apix); *)
+   if na.E.n_apix <= !G.last then begin
    match b with
       | E.Abbr t ->
          KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s;
@@ -121,7 +120,7 @@ let output_entity_1 och st (_, na, s, b) =
          KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s;
          uris := (false, s) :: !uris; !ok
       | E.Void   -> C.err ()
-(*   end else !ok *)
+   end else !ok
 
 let close_out_1 och () =
    let aux_sep _ = KP.fprintf och "%s" ")" in
@@ -133,8 +132,7 @@ let close_out_1 och () =
 (* Variant 2 *************************************************)
 
 let output_entity_2 och st (_, na, s, b) =
-(*   out_comment och (KP.sprintf "constant %u" na.E.n_apix); *)
-(*   if na.E.n_apix <= 9 then begin *)
+   if na.E.n_apix <= !G.last then begin
    match b with
       | E.Abbr t ->
          KP.fprintf och "g+line %a c+%u\n       %a\n.\n\n"
@@ -145,7 +143,7 @@ let output_entity_2 och st (_, na, s, b) =
             out_uri s na.E.n_apix (out_term st B.empty) u;
          uris := (false, s) :: !uris; !ok
       | E.Void   -> C.err ()
-(*   end else !ok *)
+   end else !ok
 
 let close_out_2 och () =
    let aux_name (b, s) =
@@ -153,6 +151,11 @@ let close_out_2 och () =
       KP.fprintf och "(%s %a\n" gde out_uri s
    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;
    out_clause och "main :- grundlagen.";
    out_clause och "grundlagen :- (gv+ ";
    List.iter aux_name (List.rev !uris);