basic_rg: reduction was not tail recursive by mistake

[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 58a407f04867041f157da26ab633b2966127c483..a9cec439ac06c5aafcc1719828e8f034db432244 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -86,8 +86,7 @@ and count_term f c e = function
       let f c = count_term f c e t in
       count_term f c e v
    | B.Bind (b, t) -> 
-      let f c e = count_term f c e t in
-      let f c = B.push (f c) e b in
+      let f c = count_term f c (B.push e b) t in
       count_term_binder f c e b
 
 let count_entity f c = function
@@ -99,6 +98,7 @@ let count_entity f c = function
    | _, _, Y.Abbr v ->  
       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
       count_term f c B.empty_lenv v
+   | _, _, Y.Void -> assert false
 
 let print_counters f c =
    let terms =
@@ -186,20 +186,22 @@ let rec pp_term c frm = function
    | B.Appl (_, v, t)          ->
       F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
    | B.Bind (B.Abst (a, w), t) ->
-      let f a cc =
-         F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t
+      let f a =
+         let cc = B.push c (B.abst a w) in
+        F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t
       in
-      let f a = B.push (f a) c (B.abst a w) in
       rename f c a
    | B.Bind (B.Abbr (a, v), t) ->
-      let f a cc = 
-         F.fprintf frm "@[[%a=%a].%a@]" name a (pp_term c) v (pp_term cc) t
+      let f a = 
+         let cc = B.push c (B.abbr a v) in
+        F.fprintf frm "@[[%a=%a].%a@]" name a (pp_term c) v (pp_term cc) t
       in
-      let f a = B.push (f a) c (B.abbr a v) in
       rename f c a
    | B.Bind (B.Void a, t)      ->
-      let f a cc = F.fprintf frm "@[[%a].%a@]" name a (pp_term cc) t in
-      let f a = B.push (f a) c (B.Void a) in
+      let f a = 
+         let cc = B.push c (B.Void a) in
+         F.fprintf frm "@[[%a].%a@]" name a (pp_term cc) t
+      in
       rename f c a
 
 let pp_lenv frm c =
@@ -255,7 +257,7 @@ let rec exp_term e t out tab = match t with
    | B.Bind (b, t)    ->
       let b = rename_bind C.start e b in
       exp_bind e b out tab; 
-      exp_term (B.push C.start e b) t out tab 
+      exp_term (B.push e b) t out tab 
 
 and exp_bind e b out tab = match b with
    | B.Abst (a, w) ->