X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgReduction.ml;h=87d093d82f47638ea9580a89996d7f632482e0d6;hb=448920d42f3f7886d27477281b22f0c11771d4ed;hp=8ad752bada79e9a85688362c2f8a6b26064d2e5f;hpb=dcdee4ca839dac671924a95f0ada71faf06a8be4;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 8ad752bad..87d093d82 100644
--- 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
+            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 (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