- bugfix is refreshed state of AutCrg: now we return a fresh state

[helm.git] / helm / software / helena / src / basic_ag / bagReduction.ml

diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml
index 8df9274ed648a8611bd5d99f257ad76396a94ffe..287978f5064dcf1a71856d4ab0d52c6798fa546d 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagReduction.ml
+++ b/helm/software/helena/src/basic_ag/bagReduction.ml
@@ -12,10 +12,9 @@
 module U  = NUri
 module C  = Cps
 module L  = Log
-module E  = Entity
+module P  = Marks
 module G  = Options
-module J  = Marks
-module S  = Status
+module E  = Entity
 module Z  = Bag
 module ZO = BagOutput
 module ZE = BagEnvironment
@@ -29,9 +28,9 @@ type machine = {
 
 type whd_result =
    | Sort_ of int
-   | LRef_ of J.mark * Z.term option
+   | LRef_ of P.mark * Z.term option
    | GRef_ of Z.entity
-   | Bind_ of Z.attrs * J.mark * Z.term * Z.term
+   | Bind_ of Z.attrs * P.mark * Z.term * Z.term
 
 type ho_whd_result =
    | Sort of int
@@ -39,7 +38,7 @@ type ho_whd_result =
 
 (* Internal functions *******************************************************)
 
-let level = 4
+let level = 5
 
 let term_of_whdr = function
    | Sort_ h              -> Z.Sort h
@@ -49,11 +48,11 @@ let term_of_whdr = function
 
 let log1 st s c t =
    let s1, s2 = s ^ " in the environment", "the term" in
-   L.log st ZO.specs level (L.et_items1 s1 c s2 t)
+   L.log st ZO.specs (pred level) (L.et_items1 s1 c s2 t)
 
 let log2 st s cu u ct t =
    let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
-   L.log st ZO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+   L.log st ZO.specs (pred level) (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
 
 let empty_machine = {i = 0; c = Z.empty_lenv; s = []}
 
@@ -99,12 +98,12 @@ let rec whd f c m x =
       begin match m.s with
          | []      -> f m (Bind_ (a, l, w, t))
         | v :: tl -> 
-            let nl = J.new_mark () in
+            let nl = P.new_mark () in
            let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
            Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v)))
       end
    | Z.Bind (a, l, b, t)         -> 
-      let nl = J.new_mark () in
+      let nl = P.new_mark () in
       let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
       Z.push "!" f m.c a nl b
 
@@ -125,7 +124,7 @@ let rec ho_whd f c m x =
    whd aux c m x
    
 let ho_whd f st c t =
-   if !G.trace >= level then log1 st.S.lenv "Now scanning" c t;
+   if !G.trace >= level then log1 st "Now scanning" c t;
    ho_whd f c empty_machine t
 
 let rec are_convertible f st a c m1 t1 m2 t2 =
@@ -133,17 +132,17 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
    let rec aux m1 r1 m2 r2 =
 (*   L.warn "entering R.are_convertible_aux"; *)
    let u, t = term_of_whdr r1, term_of_whdr r2 in
-   if !G.trace >= level then log2 st.S.lenv "Now really converting" c u c t;   
+   if !G.trace >= level then log2 st "Now really converting" c u c t;   
    match r1, r2 with
       | Sort_ h1, Sort_ h2                                 ->
          if h1 = h2 then f a else f false 
       | LRef_ (i1, _), LRef_ (i2, _)                       ->
          if i1 = i2 then are_convertible_stacks f st a c m1 m2 else f false
-      | GRef_ (_, {E.n_apix = Some a1}, _, E.Abst _), 
-        GRef_ (_, {E.n_apix = Some a2}, _, E.Abst _)       ->
+      | GRef_ (_, {E.n_apix = a1}, _, E.Abst _), 
+        GRef_ (_, {E.n_apix = a2}, _, E.Abst _)            ->
          if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
-      | GRef_ (_, {E.n_apix = Some a1}, _, E.Abbr v1), 
-        GRef_ (_, {E.n_apix = Some a2}, _, E.Abbr v2)      ->
+      | GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1), 
+        GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2)           ->
          if a1 = a2 then
            let f a = 
               if a then f a else are_convertible f st true c m1 v1 m2 v2
@@ -157,7 +156,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
       | GRef_ (_, _, _, E.Abbr v1), _                      ->
         whd (aux_rev m2 r2) c m1 v1      
       | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2)     ->
-          let l = J.new_mark () in
+          let l = P.new_mark () in
           let h c =
              let m1, m2 = inc m1, inc m2 in
              let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in
@@ -166,7 +165,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
          let f r = if r then push "!" h c m1 a1 l w1 else f false in
         are_convertible f st a c m1 w1 m2 w2
 (* we detect the AUT-QE reduction rule for type/prop inclusion *)      
-      | Sort_ _, Bind_ (a2, l2, w2, t2) when st.S.si       ->
+      | Sort_ _, Bind_ (a2, l2, w2, t2) when !G.si         ->
         let m1, m2 = inc m1, inc m2 in
         let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in
         push "nsi" f c m2 a2 l2 w2
@@ -190,5 +189,5 @@ and are_convertible_stacks f st a c m1 m2 =
       C.list_fold_left2 f map a m1.s m2.s
 
 let are_convertible f st c u t = 
-   if !G.trace >= level then log2 st.S.lenv "Now converting" c u c t;
+   if !G.trace >= level then log2 st "Now converting" c u c t;
    are_convertible f st true c empty_machine u empty_machine t