- initial support for abstractions with explicit levels

[helm.git] / helm / software / lambda-delta / src / basic_rg / brgReduction.ml

diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
index bd78edc26b60c5e829accbc30910e8d87d41d96a..5a5559f7ce1e7f5dafa71049473b010b17f6d7c4 100644 (file)
--- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
@@ -59,10 +59,10 @@ let are_alpha_convertible err f t1 t2 =
         aux_bind f (b1, b2)
       | _                                      -> err ()
    and aux_bind f = function
-      | B.Abbr v1, B.Abbr v2
-      | B.Abst v1, B.Abst v2                   -> aux f (v1, v2)
-      | B.Void, B.Void                         -> f ()
-      | _                                      -> err ()
+      | B.Abbr v1, B.Abbr v2                          -> aux f (v1, v2)
+      | B.Abst (n1, v1), B.Abst (n2, v2) when n1 = n2 -> aux f (v1, v2)
+      | B.Void, B.Void                                -> f ()
+      | _                                             -> err ()
    in
    if S.eq t1 t2 then f () else aux f (t1, t2)
 
@@ -73,41 +73,41 @@ let get m i =
 let rec step st m x = 
 (*   L.warn "entering R.step"; *)
    match x with
-   | B.Sort _                -> m, None, x
-   | B.GRef (_, uri)         ->
+   | B.Sort _                     -> m, None, x
+   | B.GRef (_, uri)              ->
       begin match BE.get_entity uri with
-         | _, _, E.Abbr v when st.E.delta ->
+         | _, _, E.Abbr v when st.E.delta   ->
            O.add ~gdelta:1 (); step st m v
-         | _, _, E.Abst w when st.E.rt    ->
+         | _, _, E.Abst (_, w) when st.E.rt ->
             O.add ~grt:1 (); step st m w        
-        | a, _, E.Abbr v                 ->
+        | a, _, E.Abbr v                   ->
            let e = E.apix C.err C.start a in
            m, Some (e, a, B.Abbr v), x   
-        | a, _, E.Abst w                 ->
+        | a, _, E.Abst (n, w)              ->
            let e = E.apix C.err C.start a in
-           m, Some (e, a, B.Abst w), x
-        | _, _, E.Void                   -> assert false
+           m, Some (e, a, B.Abst (n, w)), x
+        | _, _, E.Void                     -> assert false
       end
-   | B.LRef (_, i)           ->
+   | B.LRef (_, i)                ->
       begin match get m i with
-        | c, _, B.Abbr v              ->
+        | c, _, B.Abbr v                   ->
            O.add ~ldelta:1 ();
            step st {m with e = c} v
-        | c, _, B.Abst w when st.E.rt ->
+        | c, _, B.Abst (_, w) when st.E.rt ->
             O.add ~lrt:1 ();
             step st {m with e = c} w
-        | c, _, B.Void                ->
+        | c, _, B.Void                     ->
            assert false
-        | c, a, (B.Abst _ as b)       ->
+        | c, a, (B.Abst _ as b)            ->
            let e = E.apix C.err C.start a in
            {m with e = c}, Some (e, a, b), x
       end
-   | B.Cast (_, _, t)        ->
+   | B.Cast (_, _, t)             ->
       O.add ~tau:1 ();
       step st m t
-   | B.Appl (_, v, t)        ->
+   | B.Appl (_, v, t)             ->
       step st {m with s = (m.e, v) :: m.s} t   
-   | B.Bind (a, B.Abst w, t) ->
+   | B.Bind (a, B.Abst (n, w), t) ->
       begin match m.s with
          | []          -> m, None, x
         | (c, v) :: s ->
@@ -154,9 +154,9 @@ let rec ac_nfs st (m1, r1, u) (m2, r2, t) =
       | Some (_, _, B.Abbr v1), _, _, _                        ->
          O.add ~gdelta:1 ();
         ac_nfs st (step st m1 v1) (m2, r2, t)             
-      | _, B.Bind (a1, (B.Abst w1 as b1), t1), 
-        _, B.Bind (a2, (B.Abst w2 as b2), t2)                  ->
-        if ac {st with E.si = false} m1 w1 m2 w2 then
+      | _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1), 
+        _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2)            ->
+        if (* n1 = n2 && *) ac {st with E.si = false} m1 w1 m2 w2 then
            ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false
       | _, B.Sort _, _, B.Bind (a, b, t) when st.E.si          ->