]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_ag/bagOutput.ml
freescale porting
[helm.git] / helm / software / lambda-delta / basic_ag / bagOutput.ml
index c315b1ec7a599052cfd877c7666d8cad09af8be0..763f61af41f62acd3de5fad75584834437490eae 100644 (file)
@@ -13,6 +13,7 @@ module P = Printf
 module F = Format
 module U = NUri
 module L = Log
+module Y = Entity
 module H = Hierarchy
 module O = Output
 module B = Bag
@@ -62,21 +63,14 @@ and count_term f c = function
       let f c = count_term_binder f c b in
       count_term f c t
 
-let count_obj_binder f c = function
-   | B.Abst w -> 
+let count_entity f c = function
+   | _, _, Y.Abst w -> 
       let c = {c with eabsts = succ c.eabsts} in
       count_term f c w
-   | B.Abbr v -> 
+   | _, _, Y.Abbr v -> 
       let c = {c with eabbrs = succ c.eabbrs} in
       count_term f c v
-   | B.Void   -> f c
-
-let count_obj f c (_, _, b) =
-   count_obj_binder f c b
-
-let count_item f c = function
-   | Some obj -> count_obj f c obj
-   | None     -> f c
+   | _, _, Y.Void   -> assert false
 
 let print_counters f c =
    let terms =
@@ -133,7 +127,7 @@ let rec pp_term c frm = function
       let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in
       B.push "output void" f c l id B.Void
 
-let pp_context frm c =
+let pp_lenv frm c =
    let pp_entry frm = function
       | l, id, B.Abst w -> 
          F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w
@@ -147,5 +141,5 @@ let pp_context frm c =
    B.contents f c
 
 let specs = {
-   L.pp_term = pp_term; L.pp_context = pp_context
+   L.pp_term = pp_term; L.pp_lenv = pp_lenv
 }