- some bugfix

[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..5f73a4fc0e3901c1fc7037612cef1c30fc07efe0 100644 (file)
--- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml
@@ -11,10 +11,13 @@
 
 module U  = NUri
 module C  = Cps
-module S  = Share
+module W  = Share
 module L  = Log
 module E  = Entity
+module N  = Level
 module O  = Output
+module Q  = Ccs
+module S  = Status
 module B  = Brg
 module BO = BrgOutput
 module BE = BrgEnvironment
@@ -59,12 +62,12 @@ 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)
+   if W.eq t1 t2 then f () else aux f (t1, t2)
 
 let get m i =
    let _, c, a, b = B.get m.e i in c, a, b
@@ -73,45 +76,46 @@ 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.S.delta   ->
            O.add ~gdelta:1 (); step st m v
-         | _, _, E.Abst w when st.E.rt    ->
+         | _, _, E.Abst (_, w) when st.S.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.S.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 ->
-            O.add ~beta:1 ~upsilon:(List.length s) ();
+            if N.is_zero n then Q.add_infinite st.S.cc a;
+           O.add ~beta:1 ~upsilon:(List.length s) ();
            let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in 
            step st {m with e = e; s = s} t
       end
@@ -154,12 +158,14 @@ 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)
+        when n1 = n2 || st.S.si                               ->
+        if ac {st with S.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          ->
+      | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t)
+         when N.is_zero n || st.S.si                           ->
         O.add ~si:1 ();
         ac st (push m1 a b) u (push m2 a b) t
       | _                                                      -> false
@@ -173,7 +179,7 @@ and ac_stacks st m1 m2 =
    if List.length m1.s <> List.length m2.s then false else
    let map (c1, v1) (c2, v2) =
       let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in
-      ac {st with E.si = false} m1 v1 m2 v2
+      ac {st with S.si = false} m1 v1 m2 v2
    in
    list_and map (m1.s, m2.s)
 
@@ -189,15 +195,15 @@ let get m i =
 
 let xwhd st m t =
    L.box level; log1 "Now scanning" m.e t;   
-   let m, _, t = step {st with E.delta = true; E.rt = true} m t in
+   let m, _, t = step {st with S.delta = true; S.rt = true} m t in
    L.unbox level; m, t
 
 let are_convertible st mu u mw w = 
    L.box level; log2 "Now converting" mu.e u mw.e w;
-   let r = ac {st with E.delta = st.E.expand; E.rt = false} mu u mw w in   
+   let r = ac {st with S.delta = st.S.expand; S.rt = false} mu u mw w in   
    L.unbox level; r
 (*    let err _ = in 
-      if S.eq mu mw then are_alpha_convertible err f u w else err () *)
+      if W.eq mu mw then are_alpha_convertible err f u w else err () *)
 
 (* error reporting **********************************************************)