- brgOutput: the nodes count is now implemented

[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 8ad752bada79e9a85688362c2f8a6b26064d2e5f..16dc395bbfe39c7eb6e4c94a1936ae2ff2874705 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -12,6 +12,7 @@
 module U = NUri
 module C = Cps
 module L = Log
+module P = Output
 module B = Brg
 module O = BrgOutput
 module E = BrgEnvironment
@@ -26,8 +27,6 @@ type machine = {
 
 (* Internal functions *******************************************************)
 
-let reductions = ref O.initial_reductions
-
 let level = 5
 
 let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
@@ -67,17 +66,18 @@ let push f m a b =
    f {m with c = (a, b) :: m.c}
 
 (* to share *)
-let rec step f ?(delta=false) ?(sty=false) c m x = 
+let rec step f ?(delta=false) ?(rt=false) c m x = 
 (*   L.warn "entering R.step"; *)
    match x with
    | B.Sort _                -> f m x
    | B.GRef (a, uri)         ->
       let f = function
          | _, _, B.Abbr v when delta ->
-            reductions := O.add ~gdelta:1 !reductions;
-           step f ~delta ~sty c m v
-         | _, _, B.Abst w when sty   ->
-           step f ~delta ~sty c m w     
+            P.add ~gdelta:1 ();
+           step f ~delta ~rt c m v
+         | _, _, B.Abst w when rt   ->
+            P.add ~grt:1 ();
+           step f ~delta ~rt c m w      
         | e, _, b                   ->
            f m (B.GRef (B.Entry (e, b) :: a, uri))
       in
@@ -85,32 +85,34 @@ let rec step f ?(delta=false) ?(sty=false) c m x =
    | B.LRef (a, i)           ->
       let f e = function
         | B.Abbr v          ->
-           reductions := O.add ~ldelta:1 !reductions;
-           step f ~delta ~sty c m v
-        | B.Abst w when sty ->
-            step f ~delta ~sty c m w
+           P.add ~ldelta:1 ();
+           step f ~delta ~rt c m v
+        | B.Abst w when rt ->
+            P.add ~lrt:1 ();
+            step f ~delta ~rt c m w
         | b                 ->
            f m (B.LRef (B.Entry (e, b) :: a, i))
       in
       let f e = S.lift_bind (f e) (succ i) (0) in 
       get f c m i
    | B.Cast (_, _, t)        ->
-      reductions := O.add ~tau:1 !reductions;
-      step f ~delta ~sty c m t
+      P.add ~tau:1 ();
+      step f ~delta ~rt c m t
    | B.Appl (_, v, t)        ->
-      step f ~delta ~sty c {m with s = (v, 0) :: m.s} t   
+      step f ~delta ~rt c {m with s = (v, 0) :: m.s} t   
    | B.Bind (a, B.Abst w, t) -> 
       begin match m.s with
          | []           -> f m x
         | (v, h) :: tl -> 
-            reductions := O.add ~beta:1 !reductions;
-           let f mc = step f ~delta ~sty c {c = mc; s = tl} t in
-           let f v = B.push f m.c a (B.Abbr (B.Cast ([], w, v))) in
+            P.add ~beta:1 ~upsilon:(List.length tl) ();
+           let f mc sc = step f ~delta ~rt c {c = mc; s = sc} t in
+           let f mc = lift_stack (f mc) tl in 
+           let f v = B.push f m.c a (B.Abbr v (* (B.Cast ([], w, v)) *) ) in
            S.lift f h (0) v
       end
    | B.Bind (a, b, t)        -> 
-      reductions := O.add ~upsilon:(List.length m.s) !reductions;
-      let f sc mc = step f ~delta ~sty c {c = mc; s = sc} t in
+      P.add ~upsilon:(List.length m.s) ();
+      let f sc mc = step f ~delta ~rt c {c = mc; s = sc} t in
       let f sc = B.push (f sc) m.c a b in
       lift_stack f m.s
 
@@ -124,7 +126,7 @@ let domain f c t =
       | x                       -> f None
    in
    L.box level; log1 "Now scanning" c t;
-   step f ~delta:true ~sty:true c empty_machine t
+   step f ~delta:true ~rt:true c empty_machine t
 
 let rec ac_nfs f ~si r c m1 u m2 t =
 (*   L.warn "entering R.are_convertible_aux"; *)
@@ -132,8 +134,9 @@ let rec ac_nfs f ~si r c m1 u m2 t =
    match u, t with
       | B.Sort (_, h1), B.Sort (_, h2)             ->
          if h1 = h2 then f r else f false 
-      | B.LRef (B.Entry (e1, B.Abst _) :: _, _), 
-        B.LRef (B.Entry (e2, B.Abst _) :: _, _)    ->
+      | B.LRef (B.Entry (e1, B.Abst _) :: _, i1), 
+        B.LRef (B.Entry (e2, B.Abst _) :: _, i2)   ->
+        P.add ~zeta:(i1+i2-e1-e2) ();
         if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false
       | B.GRef (B.Entry (e1, B.Abst _) :: _, _), 
         B.GRef (B.Entry (e2, B.Abst _) :: _, _)    ->
@@ -144,23 +147,23 @@ let rec ac_nfs f ~si r c m1 u m2 t =
            let f r = 
               if r then f r 
               else begin  
-                  reductions := O.add ~gdelta:2 !reductions;
+                  P.add ~gdelta:2 ();
                  ac f ~si true c m1 v1 m2 v2
               end
            in
            ac_stacks f ~si r c m1 m2
         else if e1 < e2 then begin 
-            reductions := O.add ~gdelta:1 !reductions;
+            P.add ~gdelta:1 ();
            step (ac_nfs f ~si r c m1 u) c m2 v2
         end else begin
-           reductions := O.add ~gdelta:1 !reductions;
+           P.add ~gdelta:1 ();
            step (ac_nfs_rev f ~si r c m2 t) c m1 v1
          end
       | _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) ->
-         reductions := O.add ~gdelta:1 !reductions;
+         P.add ~gdelta:1 ();
          step (ac_nfs f ~si r c m1 u) c m2 v2      
       | B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ ->
-         reductions := O.add ~gdelta:1 !reductions;
+         P.add ~gdelta:1 ();
         step (ac_nfs_rev f ~si r c m2 t) c m1 v1            
       | B.Bind (a1, (B.Abst w1 as b1), t1), 
         B.Bind (a2, (B.Abst w2 as b2), t2)         ->
@@ -169,6 +172,7 @@ let rec ac_nfs f ~si r c m1 u m2 t =
         let f r = if r then push g m1 a1 b1 else f false in
         ac f ~si r c m1 w1 m2 w2      
       | B.Sort _, B.Bind (a, b, t) when si         ->
+        P.add ~si:1 ();
         let f m1 m2 = ac f ~si r c m1 u m2 t in
         let f m1 = push (f m1) m2 a b in
         push f m1 a b