- revision of ground_2 and basic_2

[helm.git] / helm / software / helena / src / complete_rg / crgOutput.ml

diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml
index 3ad78a37be6f22835e65140deb3347ed9042478b..7c9ab81724ec0befa9d37f77bf44ab07cc5a4ce1 100644 (file)
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -9,12 +9,13 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module P = Printf
+module KP = Printf
+
 module U = NUri
 module C = Cps
 module L = Log
-module J = Marks
-module N = Level
+module P = Marks
+module N = Layer
 module E = Entity
 module D = Crg
 
@@ -108,36 +109,35 @@ let print_counters f c =
    in
    let items = c.eabsts + c.eabbrs in
    let nodes = c.nodes + c.xnodes in
-   let marks = J.marks () in
-   L.warn level (P.sprintf "Intermediate representation summary (complete_rg)");
-   L.warn level (P.sprintf "  Total entry items:        %7u" items);
-   L.warn level (P.sprintf "    Declaration items:      %7u" c.eabsts);
-   L.warn level (P.sprintf "    Definition items:       %7u" c.eabbrs);
-   L.warn level (P.sprintf "  Total term items:         %7u" terms);
-   L.warn level (P.sprintf "    Sort items:             %7u" c.tsorts);
-   L.warn level (P.sprintf "    Local reference items:  %7u" c.tlrefs);
-   L.warn level (P.sprintf "    Global reference items: %7u" c.tgrefs);
-   L.warn level (P.sprintf "    Explicit Cast items:    %7u" c.tcasts);
-   L.warn level (P.sprintf "    Application items:      %7u" c.tappls);
-   L.warn level (P.sprintf "    Abstraction items:      %7u" c.tabsts);
-   L.warn level (P.sprintf "    Abbreviation items:     %7u" c.tabbrs);
-   L.warn level (P.sprintf "  Ambiguous abstractions:   %7u" marks);   
-   L.warn level (P.sprintf "  Global Int. Complexity:   %7u" c.nodes);
-   L.warn level (P.sprintf "    + Abbreviation nodes:   %7u" nodes);
+   let marks = P.marks () in
+   L.warn level (KP.sprintf "Intermediate representation summary (complete_rg)");
+   L.warn level (KP.sprintf "  Total entry items:        %7u" items);
+   L.warn level (KP.sprintf "    Declaration items:      %7u" c.eabsts);
+   L.warn level (KP.sprintf "    Definition items:       %7u" c.eabbrs);
+   L.warn level (KP.sprintf "  Total term items:         %7u" terms);
+   L.warn level (KP.sprintf "    Sort items:             %7u" c.tsorts);
+   L.warn level (KP.sprintf "    Local reference items:  %7u" c.tlrefs);
+   L.warn level (KP.sprintf "    Global reference items: %7u" c.tgrefs);
+   L.warn level (KP.sprintf "    Explicit Cast items:    %7u" c.tcasts);
+   L.warn level (KP.sprintf "    Application items:      %7u" c.tappls);
+   L.warn level (KP.sprintf "    Abstraction items:      %7u" c.tabsts);
+   L.warn level (KP.sprintf "    Abbreviation items:     %7u" c.tabbrs);
+   L.warn level (KP.sprintf "  Ambiguous abstractions:   %7u" marks);   
+   L.warn level (KP.sprintf "  Global Int. Complexity:   %7u" c.nodes);
+   L.warn level (KP.sprintf "    + Abbreviation nodes:   %7u" nodes);
    f ()
 
 (* term/environment pretty printer ******************************************)
 
 let pp_attrs out a =
-   let f s b = if b then out (P.sprintf "%s;" s) else out (P.sprintf "~%s;" s) in
+   let f s b = if b then out (KP.sprintf "%s;" s) else out (KP.sprintf "~%s;" s) in
    E.name ignore f a;
-   let f i = out (P.sprintf "+%i;" i) in
-   E.apix ignore f a
+   out (KP.sprintf "+%i;" a.E.n_apix)
 
 let rec pp_term out st = function
-   | D.TSort (a, l)    -> pp_attrs out a; out (P.sprintf "*%u" l)
-   | D.TLRef (a, i   ) -> pp_attrs out a; out (P.sprintf "#%u" i)
-   | D.TGRef (a, u)    -> pp_attrs out a; out (P.sprintf "$")
+   | D.TSort (a, l)    -> pp_attrs out a; out (KP.sprintf "*%u" l)
+   | D.TLRef (a, i   ) -> pp_attrs out a; out (KP.sprintf "#%u" i)
+   | D.TGRef (a, u)    -> pp_attrs out a; out (KP.sprintf "$")
    | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out st x; out ">."; pp_term out st y
    | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out st x; out ")."; pp_term out st y
    | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out st x; out "."; pp_term out st y
@@ -145,12 +145,12 @@ let rec pp_term out st = function
 
 and pp_bind out st = function
    | D.Abst (n, x) ->
-      out "[:"; pp_term out st x; out "]"; out (N.to_string st n)  
-   | D.Abbr x      -> out "[="; pp_term out st x; out "]";
-   | D.Void        -> out "[]"
+      out "[:"; pp_term out st x; out "]"; out (N.to_string st n); out " "  
+   | D.Abbr x      -> out "[="; pp_term out st x; out "] ";
+   | D.Void        -> out "[] "
 
 and pp_lenv out st = function
    | D.ESort           -> ()
    | D.EBind (x, a, y) -> pp_lenv out st x; pp_attrs out a; pp_bind out st y
-   | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ")"
-   | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "}"
+   | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ") "
+   | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "} "