X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2FbagOutput.ml;h=17bfe06596472933fb8a1522009d97fff2624a79;hb=d8c297847d28b8648c1b3728d5763112ae6472ad;hp=589ce60f0f89912bfdf2eba98c448c01345ebceb;hpb=338e3e5c639fbcfeeb347a0121cacc6c0f1fc42a;p=helm.git

diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml
index 589ce60f0..17bfe0659 100644
--- a/helm/software/lambda-delta/basic_ag/bagOutput.ml
+++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml
@@ -12,9 +12,9 @@
 module P = Printf
 module F = Format
 module U = NUri
-module C = Cps
 module L = Log
 module H = Hierarchy
+module O = Output
 module B = Bag
 
 type counters = {
@@ -84,24 +84,24 @@ let print_counters f c =
       c.tabbrs
    in
    let items = c.eabsts + c.eabbrs in
+   let locations = B.locations () in
    L.warn (P.sprintf "  Kernel representation summary (basic_ag)");
-   L.warn (P.sprintf "    Total entry items:        %6u" items);
-   L.warn (P.sprintf "      Declaration items:      %6u" c.eabsts);
-   L.warn (P.sprintf "      Definition items:       %6u" c.eabbrs);
-   L.warn (P.sprintf "    Total term items:         %6u" terms);
-   L.warn (P.sprintf "      Sort items:             %6u" c.tsorts);
-   L.warn (P.sprintf "      Local reference items:  %6u" c.tlrefs);
-   L.warn (P.sprintf "      Global reference items: %6u" c.tgrefs);
-   L.warn (P.sprintf "      Explicit Cast items:    %6u" c.tcasts);
-   L.warn (P.sprintf "      Application items:      %6u" c.tappls);
-   L.warn (P.sprintf "      Abstraction items:      %6u" c.tabsts);
-   L.warn (P.sprintf "      Abbreviation items:     %6u" c.tabbrs);
+   L.warn (P.sprintf "    Total entry items:        %7u" items);
+   L.warn (P.sprintf "      Declaration items:      %7u" c.eabsts);
+   L.warn (P.sprintf "      Definition items:       %7u" c.eabbrs);
+   L.warn (P.sprintf "    Total term items:         %7u" terms);
+   L.warn (P.sprintf "      Sort items:             %7u" c.tsorts);
+   L.warn (P.sprintf "      Local reference items:  %7u" c.tlrefs);
+   L.warn (P.sprintf "      Global reference items: %7u" c.tgrefs);
+   L.warn (P.sprintf "      Explicit Cast items:    %7u" c.tcasts);
+   L.warn (P.sprintf "      Application items:      %7u" c.tappls);
+   L.warn (P.sprintf "      Abstraction items:      %7u" c.tabsts);
+   L.warn (P.sprintf "      Abbreviation items:     %7u" c.tabbrs);
+   L.warn (P.sprintf "    Total binder locations:   %7u" locations);   
    f ()
 
-let indexes = ref false
-
 let res l id =
-   if !indexes then P.sprintf "#%u" l else id
+   if !O.indexes then P.sprintf "#%u" l else id
 
 let rec pp_term c frm = function
    | B.Sort h                 -> 
@@ -115,7 +115,7 @@ let rec pp_term c frm = function
          | Some (id, _) -> F.fprintf frm "@[%s@]" id
          | None         -> F.fprintf frm "@[#%u@]" i
       in
-      if !indexes then f None else B.get f c i
+      if !O.indexes then f None else B.get f c i
    | B.GRef s                    -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
    | B.Cast (u, t)               ->
       F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
@@ -125,15 +125,15 @@ let rec pp_term c frm = function
       let f cc =
          F.fprintf frm "@[[%s:%a].%a@]" (res l id) (pp_term c) w (pp_term cc) t
       in
-      B.push f c l id (B.Abst w)
+      B.push "output abst" f c l id (B.Abst w)
    | B.Bind (l, id, B.Abbr v, t) ->
       let f cc = 
          F.fprintf frm "@[[%s=%a].%a@]" (res l id) (pp_term c) v (pp_term cc) t
       in
-      B.push f c l id (B.Abbr v)
+      B.push "output abbr" f c l id (B.Abbr v)
    | B.Bind (l, id, B.Void, t)   ->
       let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in
-      B.push f c l id B.Void
+      B.push "output void" f c l id B.Void
 
 let pp_context frm c =
    let pp_entry frm = function