]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgOutput.ml
lambda-delta:
[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml
index b8fc2d0c2d4ab8a08bbc96797b7c2f057dea66c1..2d1fa96ae846b1f81cc10fa06ebc637af621ad2f 100644 (file)
@@ -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 = Brg
 
 (* nodes count **************************************************************)
@@ -97,35 +97,11 @@ let print_counters f c =
    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 "      Abbreviation items:     %7u" c.tabbrs);
    f ()
 
-(* reductions count *********************************************************)
-
-type reductions = {
-   beta   : int;
-   upsilon: int;
-   tau    : int;
-   ldelta : int;
-   gdelta : int
-}
-
-let initial_reductions = {
-   beta = 0; upsilon = 0; tau = 0; ldelta = 0; gdelta = 0
-}
-
-let add ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) r = {
-   beta = r.beta + beta;
-   upsilon = r.upsilon + upsilon;
-   tau = r.tau + tau;
-   ldelta = r.ldelta + ldelta;
-   gdelta = r.gdelta + gdelta
-}
-
 (* context/term pretty printing *********************************************)
 
-let indexes = ref false
-
 let id frm a =
    let f = function
       | None            -> assert false
@@ -146,7 +122,7 @@ let rec pp_term c frm = function
          | Some (a, _) -> F.fprintf frm "@[%a@]" id a
          | None        -> F.fprintf frm "@[#%u@]" i
       in
-      if !indexes then f 0 None else B.get f c i
+      if !O.indexes then f 0 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