- we are moving from old (patched) management of sort inclusion

[helm.git] / helm / software / helena / src / basic_rg / brgReduction.ml

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 7f7dd4e788e6d64fac9f416f0b959e28378b5363..002f12ce11e028bf01dcbc7e89b1c7c9add21a29 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -10,14 +10,13 @@
       V_______________________________________________________________ *)
 
 module U  = NUri
-module W  = Share
+module S  = Share
 module L  = Log
 module G  = Options
 module H  = Hierarchy
-module N  = Level
+module N  = Layer
 module E  = Entity
 module O  = Output
-module S  = Status
 module B  = Brg
 module BO = BrgOutput
 module BE = BrgEnvironment
@@ -75,7 +74,7 @@ let are_alpha_convertible err f t1 t2 =
       | B.Void, B.Void                                -> f ()
       | _                                             -> err ()
    in
-   if W.eq t1 t2 then f () else aux f (t1, t2)
+   if S.eq t1 t2 then f () else aux f (t1, t2)
 
 let assert_tstep m vo = match m.n with
    | Some n -> n > m.d
@@ -93,7 +92,7 @@ let get m i =
 (* to share *)
 let rec step st m x = 
    if !G.trace >= sublevel then 
-   log1 st.S.lenv (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x;
+   log1 st (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x;
    match x with
    | B.Sort (a, h)                ->
       if assert_tstep m false then
@@ -149,10 +148,10 @@ let rec step st m x =
          | []          ->
             let i = tsteps m in
             if i = 0 then m, x, None else
-            let n = N.minus st.S.lenv n i in
+            let n = N.minus st n i in
             m, B.Bind (a, B.Abst (n, w), t), None
         | (c, v) :: s ->
-            if !G.cc && not (N.assert_not_zero st.S.lenv n) then assert false;
+            if !G.cc && not (N.assert_not_zero st n) then assert false;
            if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
            let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in
             let e = B.push m.e c a (B.abbr v) in
@@ -179,7 +178,7 @@ let push m a b =
    {m with e = e; l = l}
 
 let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
-   if !G.trace >= level then log2 st.S.lenv "Now converting nfs" m1.e t1 m2.e t2;
+   if !G.trace >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
    match t1, r1, t2, r2 with
       | B.Sort (_, h1), _, B.Sort (_, h2), _         ->
          h1 = h2
@@ -209,13 +208,13 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
         ac_nfs st (step st m1 v1) (m2, t2, r2)
       | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _, 
         B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _  ->
-        if !G.cc && not (N.assert_equal st.S.lenv n1 n2) then false else
-         if ac {st with S.si = false} (reset m1 zero) w1 (reset m2 zero) w2 then
+        if !G.cc && not (N.assert_equal st n1 n2) then false else
+         if ac st (reset m1 zero) w1 (reset m2 zero) w2 then
            ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false
       | B.Sort _, _, B.Bind (a, B.Abst (n, _), t), _ ->
-         if st.S.si then
-            if !G.cc && not (N.assert_zero st.S.lenv n) then false else begin
+         if !G.si then
+            if !G.cc && not (N.assert_zero st n) then false else begin
            if !G.summary then O.add ~upsilon:1 ();
            ac st (push m1 a B.Void) t1 (push m2 a B.Void) t end
          else false
@@ -230,7 +229,7 @@ and ac_stacks st m1 m2 =
    if List.length m1.s <> List.length m2.s then false else
    let map (c1, v1) (c2, v2) =
       let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in
-      ac {st with S.si = false} m1 v1 m2 v2
+      ac st m1 v1 m2 v2
    in
    list_and map (m1.s, m2.s)
 
@@ -245,16 +244,16 @@ let get m i =
    let _, _, _, b = B.get m.e i in b
 
 let xwhd st m n t =
-   if !G.trace >= level then log1 st.S.lenv "Now scanning" m.e t;   
+   if !G.trace >= level then log1 st "Now scanning" m.e t;   
    let m, t, _ = step st (reset m n) t in
    m, t
 
 let are_convertible st m1 n1 t1 m2 n2 t2 = 
-   if !G.trace >= level then log2 st.S.lenv "Now converting" m1.e t1 m2.e t2;
+   if !G.trace >= level then log2 st "Now converting" m1.e t1 m2.e t2;
    let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in
    r
 (*    let err _ = in 
-      if W.eq mu mw then are_alpha_convertible err f u w else err () *)
+      if S.eq mu mw then are_alpha_convertible err f u w else err () *)
 
 (* error reporting **********************************************************)