- proper KAM with closures implemented for the brg kernel

[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index fb33da537a7b59bc2eb4a6cf113e1641702e1dda..dc697bff424769f61b30522edbd1e13538fc0427 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -11,6 +11,7 @@
 
 module P = Printf
 module F = Format
+module C = Cps
 module U = NUri
 module L = Log
 module H = Hierarchy
@@ -58,15 +59,15 @@ and count_term f c e = function
    | B.Sort _         -> 
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
    | B.LRef (_, i)    -> 
-      let f _ = function
-         | None
-        | Some (_, B.Abst _) ->
+      let err _ = f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} in
+      let f _ _ = function
+        | B.Abst _ 
+        | B.Void   ->
            f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
-        | Some (_, B.Abbr _)
-        | Some (_, B.Void)   ->
+        | B.Abbr _ ->
            f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
       in        
-      B.get f e i
+      B.get err f e i
    | B.GRef (_, u)    -> 
       let c =    
         if Cps.list_mem ~eq:U.eq u c.uris
@@ -96,8 +97,10 @@ let count_obj f c = function
    | (_, _, B.Abbr v) ->  
       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
       count_term f c B.empty_context v
-   | (_, _, B.Void)   ->
-      let c = {c with evoids = succ c.evoids; xnodes = succ c.xnodes} in
+   | (_, u, B.Void)   ->
+      let c = {c with 
+         evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris
+      } in
       f c
 
 let count_item f c = function
@@ -130,12 +133,12 @@ let print_counters f c =
 (* context/term pretty printing *********************************************)
 
 let id frm a =
-   let f = function
-      | None            -> assert false
-      | Some (true, n)  -> F.fprintf frm "%s" n
-      | Some (false, n) -> F.fprintf frm "^%s" n
+   let err () = assert false in
+   let f n = function 
+      | true  -> F.fprintf frm "%s" n
+      | false -> F.fprintf frm "^%s" n
    in      
-   B.name f a
+   B.name err f a
 
 let rec pp_term c frm = function
    | B.Sort (_, h)           -> 
@@ -145,11 +148,9 @@ let rec pp_term c frm = function
       in
       H.get_sort f h 
    | B.LRef (_, i)           -> 
-      let f _ = function
-         | Some (a, _) -> F.fprintf frm "@[%a@]" id a
-         | None        -> F.fprintf frm "@[#%u@]" i
-      in
-      if !O.indexes then f 0 None else B.get f c i
+      let err i = F.fprintf frm "@[#%u@]" i in
+      let f _ a _ = F.fprintf frm "@[%a@]" id a in
+      if !O.indexes then err i else B.get err 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
@@ -170,17 +171,15 @@ let rec pp_term c frm = function
       B.push f c a B.Void
 
 let pp_context frm c =
-   let pp_entry frm = function
-      | a, B.Abst w -> 
-         F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w
-      | a, B.Abbr v -> 
-         F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v
-      | a, B.Void   -> 
-         F.fprintf frm "@,%a" id a
+   let pp_entry f c a = function
+      | B.Abst w -> 
+         F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f ()
+      | B.Abbr v -> 
+         F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v; f ()
+      | B.Void   -> 
+         F.fprintf frm "@,%a" id a; f ()
    in
-   let iter map frm l = List.iter (map frm) l in
-   let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in
-   B.contents f c
+   B.rev_iter C.start pp_entry c
 
 let specs = {
    L.pp_term = pp_term; L.pp_context = pp_context
@@ -189,12 +188,11 @@ let specs = {
 (* term xml printing ********************************************************)
 
 let id frm a =
-   let f = function
-      | None            -> ()
-      | Some (true, s)  -> F.fprintf frm " name=%S" s
-      | Some (false, n) -> F.fprintf frm " name=%S" ("^" ^ n)
+   let f s = function
+      | true  -> F.fprintf frm " name=%S" s
+      | false -> F.fprintf frm " name=%S" ("^" ^ s)
    in      
-   B.name f a
+   B.name C.start f a
 
 let rec exp_term frm = function
    | B.Sort (a, l)    ->