- new attributes system

[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 c7d89bc84736abc69b1bf345155e807b1ffedaf8..2f4b5a2c7e75af941bf2e9880625a53136a704f2 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagReduction.ml
+++ b/helm/software/helena/src/basic_ag/bagReduction.ml
@@ -29,9 +29,9 @@ type machine = {
 
 type whd_result =
    | Sort_ of int
-   | LRef_ of int * Z.term option
+   | LRef_ of J.mark * Z.term option
    | GRef_ of Z.entity
-   | Bind_ of Z.attrs * int * Z.term * Z.term
+   | Bind_ of Z.attrs * J.mark * Z.term * Z.term
 
 type ho_whd_result =
    | Sort of int
@@ -42,10 +42,10 @@ type ho_whd_result =
 let level = 4
 
 let term_of_whdr = function
-   | Sort_ h             -> Z.Sort h
-   | LRef_ (i, _)        -> Z.LRef i
-   | GRef_ (_, uri, _)   -> Z.GRef uri
-   | Bind_ (a, l, w, t) -> Z.bind_abst a l w t
+   | Sort_ h              -> Z.Sort h
+   | LRef_ (i, _)         -> Z.LRef i
+   | GRef_ (_, _, uri, _) -> Z.GRef uri
+   | Bind_ (a, l, w, t)   -> Z.bind_abst a l w t
 
 let log1 s c t =
    let sc, st = s ^ " in the environment", "the term" in
@@ -99,12 +99,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_location () in
+            let nl = J.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_location () in
+      let nl = J.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
 
@@ -113,14 +113,14 @@ let rec whd f c m x =
 let rec ho_whd f c m x =
 (*   L.warn "entering R.ho_whd"; *)
    let aux m = function
-      | Sort_ h                     -> f (Sort h)
-      | Bind_ (_, _, w, _)          -> 
+      | Sort_ h                   -> f (Sort h)
+      | Bind_ (_, _, w, _)        -> 
          let f w = f (Abst w) in unwind_to_term f m w
-      | LRef_ (_, Some w)           -> ho_whd f c m w
-      | GRef_ (_, _, E.Abst (_, w)) -> ho_whd f c m w  
-      | GRef_ (_, _, E.Abbr v)      -> ho_whd f c m v
-      | LRef_ (_, None)             -> assert false
-      | GRef_ (_, _, E.Void)        -> assert false
+      | LRef_ (_, Some w)         -> ho_whd f c m w
+      | GRef_ (_, _, _, E.Abst w) -> ho_whd f c m w  
+      | GRef_ (_, _, _, E.Abbr v) -> ho_whd f c m v
+      | LRef_ (_, None)           -> assert false
+      | GRef_ (_, _, _, E.Void)   -> assert false
    in
    whd aux c m x
    
@@ -139,11 +139,11 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
          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.Apix a1 :: _), _, E.Abst _), 
-        GRef_ ((E.Apix a2 :: _), _, E.Abst _)              ->
+      | GRef_ (_, {E.n_apix = Some a1}, _, E.Abst _), 
+        GRef_ (_, {E.n_apix = Some a2}, _, E.Abst _)       ->
          if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
-      | GRef_ ((E.Apix a1 :: _), _, E.Abbr v1), 
-        GRef_ ((E.Apix a2 :: _), _, E.Abbr v2)             ->
+      | GRef_ (_, {E.n_apix = Some a1}, _, E.Abbr v1), 
+        GRef_ (_, {E.n_apix = Some 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
@@ -152,12 +152,12 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
         else
         if a1 < a2 then whd (aux m1 r1) c m2 v2 else
         whd (aux_rev m2 r2) c m1 v1
-      | _, GRef_ (_, _, E.Abbr v2)                         ->
+      | _, GRef_ (_, _, _, E.Abbr v2)                      ->
          whd (aux m1 r1) c m2 v2
-      | GRef_ (_, _, E.Abbr v1), _                         ->
+      | 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_location () in
+          let l = J.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