- commit completed :)

[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 d4b5e68fdc111b8fd1a2c3d4380e332875590e2a..2aba23fe36d9dab97e12e3eef654a1dd02d0c2ed 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -87,7 +87,9 @@ let get m i =
 
 (* to share *)
 let rec step st m x = 
+(*
    log1 (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
@@ -95,53 +97,60 @@ let rec step st m x =
       else m, x, None
    | B.GRef (_, uri)              ->
       begin match BE.get_entity uri with
-         | _, _, E.Abbr v when st.S.delta               ->
-           O.add ~gdelta:1 (); step st m v
-         | _, _, E.Abst (_, w) when assert_tstep m true ->
-            O.add ~grt:1 (); step st (tstep m) w
-        | _, _, E.Abbr v                               ->
-           m, x, Some v
-        | _, _, E.Abst _                               ->
-           m, x, None   
-        | _, _, E.Void                                 ->
+         | _, _, E.Abbr v      ->
+            if st.S.delta then begin
+              if st.S.tc then O.add ~gdelta:1 ();
+               step st m v
+            end else
+              m, x, Some v
+         | _, _, E.Abst (_, w) ->
+            if assert_tstep m true then begin
+               if st.S.tc then O.add ~grt:1 (); 
+               step st (tstep m) w
+            end else
+            m, x, None   
+        | _, _, E.Void        ->
             assert false
       end
    | B.LRef (_, i)                ->
       begin match get m i with
-        | c, _, B.Abbr v                          ->
-           O.add ~ldelta:1 ();
+        | c, _, B.Abbr v      ->
+           if st.S.tc then O.add ~ldelta:1 ();
            step st {m with e = c} v
-        | c, _, B.Abst (_, w) when assert_tstep m true ->
-            O.add ~lrt:1 ();
-            step st {(tstep m) with e = c} w
-        | _, a, B.Abst _                               ->
-          m, B.LRef (a, i), None
-        | _, _, B.Void                                 ->
+        | c, a, B.Abst (_, w) ->
+            if assert_tstep m true then begin
+               if st.S.tc then O.add ~lrt:1 ();
+               step st {(tstep m) with e = c} w
+            end else
+              m, B.LRef (a, i), None
+        | _, _, B.Void        ->
            assert false
       end
    | B.Cast (_, u, t)             ->
       if assert_tstep m false then begin
-         O.add ~e:1 ();
+         if st.S.tc then O.add ~e:1 ();
          step st (tstep m) u
       end else begin
-         O.add ~epsilon:1 ();
+         if st.S.tc then O.add ~epsilon:1 ();
          step st m t
       end
    | B.Appl (_, v, t)             ->
       step st {m with s = (m.e, v) :: m.s} t   
    | B.Bind (a, B.Abst (n, w), t) ->
-      let n = N.minus n m.d in
-      let x = B.Bind (a, B.Abst (n, w), t) in
       begin match m.s with
-         | []          -> m, x, None
+         | []          ->
+            if n = N.infinite || m.d = 0 then m, x, None else
+            let n = N.minus n m.d in
+            m, B.Bind (a, B.Abst (n, w), t), None
         | (c, v) :: s ->
             if N.is_zero n then Q.add_nonzero st.S.cc a;
-           O.add ~beta:1 ~theta:(List.length s) ();
-           let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in 
+           if st.S.tc then O.add ~beta:1 ~theta:(List.length s) ();
+           let v = if assert_tstep m false then B.Cast ([], w, v) else v in
+            let e = B.push m.e c a (B.abbr v) in
            step st {m with e = e; s = s} t
       end
    | B.Bind (a, b, t)        ->
-      O.add ~theta:(List.length m.s) ();
+      if st.S.tc then O.add ~theta:(List.length m.s) ();
       let e = B.push m.e m.e a b in 
       step st {m with e = e} t
 
@@ -176,21 +185,21 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
          let e1 = E.apix C.err C.start a1 in
          let e2 = E.apix C.err C.start a2 in
          if e1 < e2 then begin 
-            O.add ~gdelta:1 ();
+            if st.S.tc then O.add ~gdelta:1 ();
            ac_nfs st (m1, t1, r1) (step st m2 v2)
         end else if e2 < e1 then begin
-           O.add ~gdelta:1 ();
+           if st.S.tc then O.add ~gdelta:1 ();
            ac_nfs st (step st m1 v1) (m2, t2, r2) 
          end else if U.eq u1 u2 & assert_iterations m1 m2 && ac_stacks st m1 m2 then true
          else begin
-           O.add ~gdelta:2 ();
+           if st.S.tc then O.add ~gdelta:2 ();
            ac st m1 v1 m2 v2
          end 
       | _, _, B.GRef _, Some v2                             ->
-         O.add ~gdelta:1 ();
+         if st.S.tc then O.add ~gdelta:1 ();
         ac_nfs st (m1, t1, r1) (step st m2 v2)
       | B.GRef _, Some v1, _, _                             ->
-        O.add ~gdelta:1 ();
+        if st.S.tc 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), _         ->
@@ -200,7 +209,7 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
         else false
       | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ ->
          if N.is_zero n then () else Q.add_zero st.S.cc a;
-        O.add ~si:1 ();
+        if st.S.tc then O.add ~si:1 ();
         ac st (push m1 a b) t1 (push m2 a b) t
       | _                                                   -> false