new options activated

[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 bb31fc9768a77d98c7e8150b4003206d58c1774b..6c5ac1e9809e0fe6e83026da1703f1b2770fbc64 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -55,21 +55,21 @@ let zero = Some 0
 let are_alpha_convertible err f t1 t2 =
    let rec aux f = function
       | B.Sort (_, p1), B.Sort (_, p2)
-      | B.LRef (_, p1), B.LRef (_, p2)         ->
+      | B.LRef (_, p1), B.LRef (_, p2)               ->
          if p1 = p2 then f () else err ()
-      | B.GRef (_, u1), B.GRef (_, u2)         ->
+      | B.GRef (_, u1), B.GRef (_, u2)               ->
          if U.eq u1 u2 then f () else err ()
       | B.Cast (_, v1, t1), B.Cast (_, v2, t2)         
-      | B.Appl (_, v1, t1), B.Appl (_, v2, t2) ->
+      | B.Appl (_, _, v1, t1), B.Appl (_, _, v2, t2) ->
          let f _ = aux f (t1, t2) in
         aux f (v1, v2)
-      | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
+      | B.Bind (_, b1, t1), B.Bind (_, b2, t2)       ->
          let f _ = aux f (t1, t2) in
         aux_bind f (b1, b2)
-      | _                                      -> err ()
+      | _                                            -> err ()
    and aux_bind f = function
       | B.Abbr v1, B.Abbr v2                                             -> aux f (v1, v2)
-      | B.Abst (x1, n1, v1), B.Abst (x2, n2, v2) when x1 = x2 && n1 = n2 -> aux f (v1, v2)
+      | B.Abst (r1, n1, v1), B.Abst (r2, n2, v2) when r1 = r2 && n1 = n2 -> aux f (v1, v2)
       | B.Void, B.Void                                                   -> f ()
       | _                                                                -> err ()
    in
@@ -92,7 +92,7 @@ let get m i =
 
 (* to share *)
 let rec step st m r = 
-   if !G.trace >= sublevel then 
+   if !G.ct >= sublevel then 
    log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r;
    match r with
    | B.Sort (a, h)                       ->
@@ -102,7 +102,7 @@ let rec step st m r =
    | B.GRef (_, uri)                     ->
       begin match BE.get_entity uri with
          | _, _, _, E.Abbr v ->
-            if m.n = None || !G.expand then begin
+            if !G.expand then begin
               if !G.summary then O.add ~gdelta:1 ();
                step st m v
             end else
@@ -138,7 +138,7 @@ let rec step st m r =
          if !G.summary then O.add ~epsilon:1 ();
          step st m t
       end
-   | B.Appl (_, v, t)                    ->
+   | B.Appl (_, _, v, t)                 ->
       step st {m with s = (m.e, v) :: m.s} t   
    | B.Bind (a, B.Abst (false, n, w), t) ->
       let i = tsteps m in
@@ -183,7 +183,7 @@ let push m a b =
    {m with e = e; l = l}
 
 let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
-   if !G.trace >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
+   if !G.ct >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
    match t1, r1, t2, r2 with
       | B.Sort (_, h1), _, B.Sort (_, h2), _               ->
          h1 = h2
@@ -238,6 +238,15 @@ and ac_stacks st m1 m2 =
    in
    list_and map (m1.s, m2.s)
 
+let rec ih_nfs st (m, t, r) =
+   match t, r with
+      | B.GRef _, Some v ->
+        if !G.summary then O.add ~gdelta:1 ();
+        ih st m v
+      | _                -> m, t
+
+and ih st m t = ih_nfs st (step st m t)
+
 (* Interface functions ******************************************************)
 
 let empty_rtm = { 
@@ -249,12 +258,11 @@ let get m i =
    let _, _, _, b = B.get m.e i in b
 
 let xwhd st m n t =
-   if !G.trace >= level then log1 st "Now scanning" m.e t;   
-   let m, t, _ = step st (reset m n) t in
-   m, t
+   if !G.ct >= level then log1 st "Now scanning" m.e t;   
+   ih st (reset m n) t
 
 let are_convertible st m1 n1 t1 m2 n2 t2 = 
-   if !G.trace >= level then log2 st "Now converting" m1.e t1 m2.e t2;
+   if !G.ct >= level then log2 st "Now converting" m1.e t1 m2.e t2;
    let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in
    r
 (*    let err _ = in