dr

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

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 1ae73652d7d9f0778cba8ec7b6705bd5ad3319a0..03ed05b053a603985fea79550c313397b3cfe675 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -20,9 +20,9 @@ module O = BrgOutput
 module E = BrgEnvironment
 
 type kam = {
-   e: B.lenv;
-   s: (B.lenv * B.term) list;
-   i: int
+   e: B.lenv;                 (* environment *)
+   s: (B.lenv * B.term) list; (* stack       *)
+   d: int                     (* depth       *)
 }
 
 (* Internal functions *******************************************************)
@@ -122,12 +122,12 @@ let rec step st m x =
 
 let push m a b = 
    assert (m.s = []);
-   let a, i = match b with
-      | B.Abst _ -> Y.Apix m.i :: a, succ m.i
-      | b        -> a, m.i
+   let a, d = match b with
+      | B.Abst _ -> Y.Apix m.d :: a, succ m.d
+      | b        -> a, m.d
    in
    let e = B.push m.e m.e a b in
-   {m with e = e; i = i}
+   {m with e = e; d = d}
 
 let rec ac_nfs st (m1, r1, u) (m2, r2, t) =
    log2 "Now converting nfs" m1.e u m2.e t;
@@ -170,7 +170,7 @@ and ac st m1 t1 m2 t2 =
 
 and ac_stacks st m1 m2 =
 (*   L.warn "entering R.are_convertible_stacks"; *)
-(*   if List.length m1.s <> List.length m2.s then false else *)
+   if List.length m1.s <> List.length m2.s then false else
    let map (c1, v1) (c2, v2) =
       let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in
       ac {st with Y.si = false} m1 v1 m2 v2
@@ -180,7 +180,7 @@ and ac_stacks st m1 m2 =
 (* Interface functions ******************************************************)
 
 let empty_kam = { 
-   e = B.empty; s = []; i = 0
+   e = B.empty; s = []; d = 0
 }
 
 let get m i =
@@ -194,7 +194,7 @@ let xwhd st m t =
 
 let are_convertible st mu u mw w = 
    L.box level; log2 "Now converting" mu.e u mw.e w;
-   let r = ac {st with Y.delta = false; Y.rt = false} mu u mw w in   
+   let r = ac {st with Y.delta = st.Y.expand; Y.rt = false} mu u mw w in   
    L.unbox level; r
 (*    let err _ = in 
       if S.eq mu mw then are_alpha_convertible err f u w else err () *)