X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2FbagOutput.ml;h=0bfc13ee64c3b4de9274a62f450cf583e9fc2369;hb=85521efd364ec494e4cc024bbf87182a312e1b7b;hp=3eb96a2d56e877c16c94af49c5d7602d90961dbc;hpb=13c3708fc59d999727ee214e8ece1f03661a9737;p=helm.git

diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml
index 3eb96a2d5..0bfc13ee6 100644
--- a/helm/software/lambda-delta/basic_ag/bagOutput.ml
+++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml
@@ -12,8 +12,9 @@
 module P = Printf
 module F = Format
 module U = NUri
-module C = Cps
 module L = Log
+module O = Options
+module Y = Entity
 module H = Hierarchy
 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 =
@@ -100,24 +94,20 @@ let print_counters f c =
    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                 -> 
-      let f = function 
-         | Some s -> F.fprintf frm "@[%s@]" s
-	 | None   -> F.fprintf frm "@[*%u@]" h
-      in
-      H.get_sort f h 
+      let err () = F.fprintf frm "@[*%u@]" h in
+      let f s = F.fprintf frm "@[%s@]" s in
+      H.string_of_sort err f h 
    | B.LRef i                 -> 
       let f = 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
@@ -137,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
@@ -151,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
 }