- we removed a flag from the kernel status

[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 1fd77cd5140b3cdaf7fb1638244fff726dc5b36b..7f7dd4e788e6d64fac9f416f0b959e28378b5363 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -22,7 +22,7 @@ module B  = Brg
 module BO = BrgOutput
 module BE = BrgEnvironment
 
-type kam = {
+type rtm = {
    e: B.lenv;                 (* environment              *)
    s: (B.lenv * B.term) list; (* stack                    *)
    l: int;                    (* level                    *)
@@ -30,7 +30,7 @@ type kam = {
    n: int option;             (* expected type iterations *)
 }
 
-type message = (kam, B.term) L.message
+type message = (rtm, B.term) L.message
 
 (* Internal functions *******************************************************)
 
@@ -102,7 +102,7 @@ let rec step st m x =
    | B.GRef (_, uri)              ->
       begin match BE.get_entity uri with
          | _, _, _, E.Abbr v ->
-            if st.S.delta then begin
+            if m.n = None || !G.expand then begin
               if !G.summary then O.add ~gdelta:1 ();
                step st m v
             end else
@@ -141,7 +141,11 @@ let rec step st m x =
    | B.Appl (_, v, t)             ->
       step st {m with s = (m.e, v) :: m.s} t   
    | B.Bind (a, B.Abst (n, w), t) ->
-      begin match m.s with
+(*      if not !G.cc && st.S.si && N.to_string st.S.lenv n = "0" then begin
+         if !G.summary then O.add ~upsilon:1 ();
+         let e = B.push m.e m.e a B.Void in 
+         step st {m with e = e} t
+      end else *) begin match m.s with
          | []          ->
             let i = tsteps m in
             if i = 0 then m, x, None else
@@ -169,7 +173,7 @@ let assert_iterations m1 m2 = match m1.n, m2.n with
 let push m a b = 
    let a, l = match b with
       | B.Abst _ -> {a with E.n_apix = m.l}, succ m.l
-      | b        -> a, m.l
+      | _        -> a, m.l
    in
    let e = B.push m.e m.e a b in
    {m with e = e; l = l}
@@ -177,15 +181,15 @@ let push m a b =
 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;
    match t1, r1, t2, r2 with
-      | B.Sort (_, h1), _, B.Sort (_, h2), _                ->
+      | B.Sort (_, h1), _, B.Sort (_, h2), _         ->
          h1 = h2
       | B.LRef ({E.n_apix = e1}, _), _, 
-        B.LRef ({E.n_apix = e2}, _), _                      ->
+        B.LRef ({E.n_apix = e2}, _), _               ->
         if e1 = e2 then ac_stacks st m1 m2 else false
-      | B.GRef (_, u1), None, B.GRef (_, u2), None          ->
+      | B.GRef (_, u1), None, B.GRef (_, u2), None   ->
         if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
       | B.GRef ({E.n_apix = e1}, u1), Some v1, 
-        B.GRef ({E.n_apix = e2}, u2), Some v2               ->
+        B.GRef ({E.n_apix = e2}, u2), Some v2        ->
          if e1 < e2 then begin 
             if !G.summary then O.add ~gdelta:1 ();
            ac_nfs st (m1, t1, r1) (step st m2 v2)
@@ -197,25 +201,25 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
            if !G.summary then O.add ~gdelta:2 ();
            ac st m1 v1 m2 v2
          end 
-      | _, _, B.GRef _, Some v2                             ->
+      | _, _, B.GRef _, Some v2                      ->
          if !G.summary then O.add ~gdelta:1 ();
         ac_nfs st (m1, t1, r1) (step st m2 v2)
-      | B.GRef _, Some v1, _, _                             ->
+      | B.GRef _, Some v1, _, _                      ->
         if !G.summary then O.add ~gdelta:1 ();
         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), _         ->
+        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
            ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false
-      | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ ->
+      | 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.summary then O.add ~si:1 ();
-           ac st (push m1 a b) t1 (push m2 a b) t end
+           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
-      | _                                                   -> false
+      | _                                            -> false
 
 and ac st m1 t1 m2 t2 =
 (*   L.warn "entering R.are_convertible"; *)
@@ -232,7 +236,7 @@ and ac_stacks st m1 m2 =
 
 (* Interface functions ******************************************************)
 
-let empty_kam = { 
+let empty_rtm = { 
    e = B.empty; s = []; l = 0; d = 0; n = None
 }
 
@@ -242,12 +246,12 @@ let get m i =
 
 let xwhd st m n t =
    if !G.trace >= level then log1 st.S.lenv "Now scanning" m.e t;   
-   let m, t, _ = step {st with S.delta = true} (reset m n) t in
+   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;
-   let r = ac {st with S.delta = !G.expand} (reset m1 n1) t1 (reset m2 n2) t2 in
+   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 () *)