when sort inclusion is enabled, we can produce conversion constraints in xml

[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 5a5559f7ce1e7f5dafa71049473b010b17f6d7c4..79ffcb32f6b60160dfc24cdce1799a035986a861 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
@@ -64,7 +67,7 @@ let are_alpha_convertible err f t1 t2 =
       | 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
@@ -76,9 +79,9 @@ let rec step st m x =
    | 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                   ->
            let e = E.apix C.err C.start a in
@@ -93,7 +96,7 @@ let rec step st m x =
         | 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                     ->
@@ -111,7 +114,8 @@ let rec step st m x =
       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
@@ -156,10 +160,11 @@ let rec ac_nfs st (m1, r1, u) (m2, r2, t) =
         ac_nfs st (step st m1 v1) (m2, r2, t)             
       | _, 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
+        if n1 = n2 && 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 +178,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 +194,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 **********************************************************)