X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2FbagOutput.ml;h=689423167690dba237ec4d46e605e1bdc94aaae4;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=0fbc039b20a228821108cc86d911c806fc1ca06a;hpb=977faf4820cd8ff5e2f0a5249161bbb92ae4b097;p=helm.git

diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml
index 0fbc039b2..689423167 100644
--- a/helm/software/helena/src/basic_ag/bagOutput.ml
+++ b/helm/software/helena/src/basic_ag/bagOutput.ml
@@ -9,13 +9,14 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module P  = Printf
+module KP = Printf
+
 module U  = NUri
 module L  = Log
+module P  = Marks
 module G  = Options
-module E  = Entity
-module J  = Marks
 module H  = Hierarchy
+module E  = Entity
 module XD = XmlCrg
 module Z  = Bag
 module ZD = BagCrg
@@ -39,6 +40,8 @@ let initial_counters = {
    tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
 }
 
+IFDEF SUMMARY THEN
+
 let rec count_term_binder f c = function
    | Z.Abst w ->
       let c = {c with tabsts = succ c.tabsts} in
@@ -68,13 +71,13 @@ and count_term f c = function
       count_term f c t
 
 let count_entity f c = function
-   | _, _, _, E.Abst w -> 
+   | _, _, _, E.Abst (_, w) -> 
       let c = {c with eabsts = succ c.eabsts} in
       count_term f c w
-   | _, _, _, E.Abbr v -> 
+   | _, _, _, E.Abbr (_, v) -> 
       let c = {c with eabbrs = succ c.eabbrs} in
       count_term f c v
-   | _, _, _, E.Void   -> assert false
+   | _, _, _, E.Void        -> assert false
 
 let print_counters f c =
    let terms =
@@ -82,79 +85,85 @@ let print_counters f c =
       c.tabbrs
    in
    let items = c.eabsts + c.eabbrs in
-   let locations = J.marks () in
-   L.warn level (P.sprintf "Kernel representation summary (basic_ag)");
-   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 "  Total binder locations:   %7u" locations);   
+   let locations = P.marks () in
+   L.warn level (KP.sprintf "Kernel representation summary (basic_ag)");
+   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 "  Total binder locations:   %7u" locations);   
    f ()
 
+END
+
 let name err och a =
    let f n = function 
-      | true  -> P.fprintf och "%s" n
-      | false -> P.fprintf och "-%s" n
+      | true  -> KP.fprintf och "%s" n
+      | false -> KP.fprintf och "-%s" n
    in      
    E.name err f a
 
 let res a l och =
-   let err () = P.fprintf och "#%s" (J.to_string l) in
+   let err () = KP.fprintf och "#%s" (P.string_of_mark l) in
    if !G.indexes then err () else name err och a
 
-let rec pp_term c och = function
-   | Z.Sort h                 -> 
-      let err () = P.fprintf och "*%u" h in
-      let f s = P.fprintf och "%s" s in
+let rec pp_term st c och = function
+   | Z.Sort h                   -> 
+      let err () = KP.fprintf och "*%u" h in
+      let f s = KP.fprintf och "%s" s in
       H.string_of_sort err f h 
-   | Z.LRef i                 -> 
-      let err () = P.fprintf och "#%s" (J.to_string i) in
+   | Z.LRef i                   -> 
+      let err () = KP.fprintf och "#%s" (P.string_of_mark i) in
       let f a _ = name err och a in
       if !G.indexes then err () else Z.get err f c i
-   | Z.GRef s                    -> P.fprintf och "$%s" (U.string_of_uri s)
-   | Z.Cast (u, t)               ->
-      P.fprintf och "{%a}.%a" (pp_term c) u (pp_term c) t
-   | Z.Appl (v, t)               ->
-      P.fprintf och "(%a).%a" (pp_term c) v (pp_term c) t
-   | Z.Bind (a, l, Z.Abst w, t) ->
+   | Z.GRef s                   -> KP.fprintf och "$%s" (U.string_of_uri s)
+   | Z.Cast (u, t)              ->
+      KP.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t
+   | Z.Appl (v, t)              ->
+      KP.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t
+   | Z.Bind (y, l, Z.Abst w, t) ->
       let f cc =
-         P.fprintf och "[%t:%a].%a" (res a l) (pp_term c) w (pp_term cc) t
+         KP.fprintf och "[%t:%a].%a" (res y l) (pp_term st c) w (pp_term st cc) t
       in
-      Z.push "output abst" f c a l (Z.Abst w)
-   | Z.Bind (a, l, Z.Abbr v, t) ->
+      Z.push "output abst" f c y l (Z.Abst w)
+   | Z.Bind (y, l, Z.Abbr v, t) ->
       let f cc = 
-         P.fprintf och "[%t=%a].%a" (res a l) (pp_term c) v (pp_term cc) t
+         KP.fprintf och "[%t=%a].%a" (res y l) (pp_term st c) v (pp_term st cc) t
       in
-      Z.push "output abbr" f c a l (Z.Abbr v)
-   | Z.Bind (a, l, Z.Void, t)   ->
-      let f cc = P.fprintf och "[%t].%a" (res a l) (pp_term cc) t in
-      Z.push "output void" f c a l Z.Void
+      Z.push "output abbr" f c y l (Z.Abbr v)
+   | Z.Bind (y, l, Z.Void, t)   ->
+      let f cc = KP.fprintf och "[%t].%a" (res y l) (pp_term st cc) t in
+      Z.push "output void" f c y l Z.Void
 
-let pp_lenv och c =
+let pp_lenv st och c =
    let pp_entry och = function
-      | a, l, Z.Abst w -> 
-         P.fprintf och "%t : %a\n" (res a l) (pp_term c) w
-      | a, l, Z.Abbr v -> 
-         P.fprintf och "%t = %a\n" (res a l) (pp_term c) v
-      | a, l, Z.Void   -> 
-         P.fprintf och "%t\n" (res a l)
+      | y, l, Z.Abst w -> 
+         KP.fprintf och "%t : %a\n" (res y l) (pp_term st c) w
+      | y, l, Z.Abbr v -> 
+         KP.fprintf och "%t = %a\n" (res y l) (pp_term st c) v
+      | y, l, Z.Void   -> 
+         KP.fprintf och "%t\n" (res y l)
    in
    let iter map och l = List.iter (map och) l in
-   let f es = P.fprintf och "%a" (iter pp_entry) (List.rev es) in
+   let f es = KP.fprintf och "%a" (iter pp_entry) (List.rev es) in
    Z.contents f c
 
 let specs = {
    L.pp_term = pp_term; L.pp_lenv = pp_lenv
 }
 
+IFDEF OBJECTS THEN
+
 (* term xml printing ********************************************************)
 
-let export_term =
-   ZD.crg_of_bag XD.export_term  
+let export_term st =
+   ZD.crg_of_bag (XD.export_term st)  
+
+END