- sort inclusion must be restricted to term backbone in order to avoid

[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 b57cb552b909452740884682804811a5d14ecd27..26663cf5f1ec5350d20138c919837f311fa3ec6a 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -64,7 +64,6 @@ let are_alpha_convertible f t1 t2 =
       | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
          let f r = if r then aux f (t1, t2) else f r in
         aux_bind f (b1, b2)
-      | B.Sort _ as t1, B.Bind (_, _, t2)      -> aux f (t1, t2)
       | _                                      -> f false
    and aux_bind f = function
       | B.Abbr v1, B.Abbr v2
@@ -148,11 +147,10 @@ let push f m a b =
 let rec ac_nfs f ~si r m1 a1 u m2 a2 t =
    log2 "Now converting nfs" m1.c u m2.c t;
    match a1, u, a2, t with
-      | _, B.Sort (_, h1), 
-        _, B.Sort (_, h2)                                ->
+      | _, B.Sort (_, h1), _, B.Sort (_, h2)             ->
          if h1 = h2 then f r else f false 
       | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _   ->
-        if e1 = e2 then ac_stacks f ~si r m1 m2 else f false
+        if e1 = e2 then ac_stacks f r m1 m2 else f false
       | Some (e1, B.Abbr v1), _, Some (e2, B.Abbr v2), _ ->
          if e1 = e2 then
            let f r = 
@@ -162,7 +160,7 @@ let rec ac_nfs f ~si r m1 a1 u m2 a2 t =
                  ac f ~si true m1 v1 m2 v2
               end
            in
-           ac_stacks f ~si r m1 m2
+           ac_stacks f r m1 m2
         else if e1 < e2 then begin 
             P.add ~gdelta:1 ();
            step (ac_nfs f ~si r m1 a1 u) m2 v2
@@ -181,7 +179,7 @@ let rec ac_nfs f ~si r m1 a1 u m2 a2 t =
         let g m1 m2 = ac f ~si r m1 t1 m2 t2 in
          let g m1 = push (g m1) m2 a2 b2 in 
         let f r = if r then push g m1 a1 b1 else f false in
-        ac f ~si r m1 w1 m2 w2      
+        ac f ~si:false r 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 m1 u m2 t in
@@ -196,12 +194,12 @@ and ac f ~si r m1 t1 m2 t2 =
    let g m1 a1 t1 = step (ac_nfs f ~si r m1 a1 t1) m2 t2 in 
    if r = false then f false else step g m1 t1
 
-and ac_stacks f ~si r m1 m2 =
+and ac_stacks f r m1 m2 =
 (*   L.warn "entering R.are_convertible_stacks"; *)
    if List.length m1.s <> List.length m2.s then f false else
    let map f r (c1, v1) (c2, v2) =
       let m1, m2 = {m1 with c = c1; s = []}, {m2 with c = c2; s = []} in
-      ac f ~si r m1 v1 m2 v2
+      ac f ~si:false r m1 v1 m2 v2
    in
    C.list_fold_left2 f map r m1.s m2.s