X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2FbagReduction.ml;h=e26a7ec1ed29eec594186fbae3013d1f988f5a72;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=a0e4fa739fcb97165e91a554c6fbfbbe22ef6274;hpb=fec20705af4705f8eb9542aece87769b82a6a6b4;p=helm.git

diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml
index a0e4fa739..e26a7ec1e 100644
--- a/helm/software/helena/src/basic_ag/bagReduction.ml
+++ b/helm/software/helena/src/basic_ag/bagReduction.ml
@@ -20,6 +20,8 @@ module ZO = BagOutput
 module ZE = BagEnvironment
 module ZS = BagSubstitution
 
+IFDEF TYPE THEN
+
 type machine = {
    i: int;
    c: Z.lenv;
@@ -112,27 +114,31 @@ let rec whd f c m x =
 let rec ho_whd f c m x =
 (*   L.warn "entering R.ho_whd"; *)
    let aux m = function
-      | Sort_ h                   -> f (Sort h)
-      | Bind_ (_, _, w, _)        -> 
+      | Sort_ h                        -> f (Sort h)
+      | Bind_ (_, _, w, _)             -> 
          let f w = f (Abst w) in unwind_to_term f m w
-      | LRef_ (_, Some w)         -> ho_whd f c m w
-      | GRef_ (_, _, _, E.Abst w) -> ho_whd f c m w  
-      | GRef_ (_, _, _, E.Abbr v) -> ho_whd f c m v
-      | LRef_ (_, None)           -> assert false
-      | GRef_ (_, _, _, E.Void)   -> assert false
+      | LRef_ (_, Some w)              -> ho_whd f c m w
+      | GRef_ (_, _, _, E.Abst (_, w)) -> ho_whd f c m w  
+      | GRef_ (_, _, _, E.Abbr (_, v)) -> ho_whd f c m v
+      | LRef_ (_, None)                -> assert false
+      | GRef_ (_, _, _, E.Void)        -> assert false
    in
    whd aux c m x
    
 let ho_whd f st c t =
-   if !G.ct >= level then log1 st "Now scanning" c t;
+IFDEF TRACE THEN
+   if !G.ct >= level then log1 st "Now scanning" c t
+ELSE () END;
    ho_whd f c empty_machine t
 
 let rec are_convertible f st a c m1 t1 m2 t2 =
 (*   L.warn "entering R.are_convertible"; *)
    let rec aux m1 r1 m2 r2 =
 (*   L.warn "entering R.are_convertible_aux"; *)
+IFDEF TRACE THEN
    let u, t = term_of_whdr r1, term_of_whdr r2 in
-   if !G.ct >= level then log2 st "Now really converting" c u c t;   
+   if !G.ct >= level then log2 st "Now really converting" c u c t
+ELSE () END;   
    match r1, r2 with
       | Sort_ k1, Sort_ k2                            ->
          if k1 = k2 then f a else f false 
@@ -141,8 +147,8 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
       | GRef_ (_, {E.n_apix = a1}, _, E.Abst _), 
         GRef_ (_, {E.n_apix = a2}, _, E.Abst _)       ->
          if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
-      | GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1), 
-        GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2)      ->
+      | GRef_ (_, {E.n_apix = a1}, _, E.Abbr (_, v1)), 
+        GRef_ (_, {E.n_apix = a2}, _, E.Abbr (_, v2)) ->
          if a1 = a2 then
 	    let f a = 
 	       if a then f a else are_convertible f st true c m1 v1 m2 v2
@@ -151,9 +157,9 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
 	 else
 	 if a1 < a2 then whd (aux m1 r1) c m2 v2 else
 	 whd (aux_rev m2 r2) c m1 v1
-      | _, GRef_ (_, _, _, E.Abbr v2)                 ->
+      | _, GRef_ (_, _, _, E.Abbr (_, v2))            ->
          whd (aux m1 r1) c m2 v2
-      | GRef_ (_, _, _, E.Abbr v1), _                 ->
+      | GRef_ (_, _, _, E.Abbr (_, v1)), _            ->
 	 whd (aux_rev m2 r2) c m1 v1      
       | Bind_ (y1, l1, w1, t1), Bind_ (_, l2, w2, t2) ->
 	   let l = P.new_mark () in
@@ -188,6 +194,10 @@ and are_convertible_stacks f st a c m1 m2 =
    else
       C.list_fold_left2 f map a m1.s m2.s
 
-let are_convertible f st c u t = 
-   if !G.ct >= level then log2 st "Now converting" c u c t;
+let are_convertible f st c u t =
+IFDEF TRACE THEN 
+   if !G.ct >= level then log2 st "Now converting" c u c t
+ELSE () END;
    are_convertible f st true c empty_machine u empty_machine t
+
+END