]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgLP.ml
new semantics of the -g option completed
[helm.git] / helm / software / helena / src / basic_rg / brgLP.ml
index d4ed3c9dd3d98d7b1c99a9010f8d65423e9ae11b..0eb193b7d1521c2662d4b4635d7112da0e6b6e38 100644 (file)
@@ -113,15 +113,15 @@ let rec out_term st e och = function
 
 (* elpi variant 1 ***********************************************************)
 
-let output_entity_lp1 och st (_, na, s, b) =
+let output_entity_lp1 och st (_, na, u, b) =
    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;
-         uris := (true, s) :: !uris; !ok
-      | E.Abst u ->
-         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.Abbr v ->
+         KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) v out_uri u;
+         uris := (true, u) :: !uris; !ok
+      | E.Abst w ->
+         KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) w out_uri u;
+         uris := (false, u) :: !uris; !ok
       | E.Void   -> C.err ()
    end else !ok
 
@@ -134,17 +134,17 @@ let close_out_lp1 och () =
 
 (* elpi variant 2 ***********************************************************)
 
-let output_entity_lp2 och st (_, na, s, b) =
+let output_entity_lp2 och st (_, na, u, b) =
    if na.E.n_apix <= !G.last then begin
    match b with
-      | E.Abbr t ->
+      | E.Abbr v ->
          KP.fprintf och "g+line %a c+%u\n       %a\n.\n\n"
-            out_uri s na.E.n_apix (out_term st B.empty) t;
-         uris := (true, s) :: !uris; !ok
-      | E.Abst u ->
+            out_uri u na.E.n_apix (out_term st B.empty) v;
+         uris := (true, u) :: !uris; !ok
+      | E.Abst w ->
          KP.fprintf och "g+line %a c+%u\n       %a\n.\n\n"
-            out_uri s na.E.n_apix (out_term st B.empty) u;
-         uris := (false, s) :: !uris; !ok
+            out_uri u na.E.n_apix (out_term st B.empty) w;
+         uris := (false, u) :: !uris; !ok
       | E.Void   -> C.err ()
    end else !ok
 
@@ -160,7 +160,7 @@ let close_out_lp2 och () =
       out_clause och "tv+c C T :- tv+ T."
    end;
    out_clause och "main :- grundlagen.";
-   out_clause och "grundlagen :- gv+ ";
+   out_clause och "grundlagen :- gv+";
    List.iter aux_name (List.rev !uris);
    KP.fprintf och "%s" "gtop";
    List.iter aux_sep !uris;
@@ -169,25 +169,25 @@ let close_out_lp2 och () =
 
 (* teyjus variant 2 *************************************************)
 
-let output_entity_tj2 och st (_, na, s, b) =
+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); 
    match b with
-      | E.Abbr t ->
+      | E.Abbr v ->
          KP.fprintf och "g+line %a %u\n       %a\n.\n\n"
-            out_uri s (top_age - na.E.n_apix) (out_term st B.empty) t;
-         uris := (true, s) :: !uris; !ok
-      | E.Abst u ->
+            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 s (top_age - na.E.n_apix) (out_term st B.empty) u;
-         uris := (false, s) :: !uris; !ok
+            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, s) =
+   let aux_name (b, u) =
       let gde = if b then "gdef+2" else "gdec+2" in 
-      KP.fprintf och "(%s %a\n" gde out_uri s
+      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
@@ -196,7 +196,7 @@ let close_out_tj2 och () =
       out_clause och "tv+c C T :- tv+ T."
    end;
    out_clause och "main :- grundlagen.";
-   out_clause och "grundlagen :- gv+ ";
+   out_clause och "grundlagen :- gv+";
    List.iter aux_name (List.rev !uris);
    KP.fprintf och "%s" "gtop";
    List.iter aux_sep !uris;