- the connections between the intermediate language and the "bag"

[helm.git] / helm / software / lambda-delta / src / basic_ag / bagReduction.ml

diff --git a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml
index 52f04bf0e2406249cdd290bb01bc59138413650d..d22d2c73065024250547fc452dd5dad1af910318 100644 (file)
--- a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml
@@ -13,6 +13,7 @@ module U  = NUri
 module C  = Cps
 module L  = Log
 module E  = Entity
+module J  = Marks
 module Z  = Bag
 module ZO = BagOutput
 module ZE = BagEnvironment
@@ -28,7 +29,7 @@ type whd_result =
    | Sort_ of int
    | LRef_ of int * Z.term option
    | GRef_ of Z.entity
-   | Bind_ of int * Z.id * Z.term * Z.term
+   | Bind_ of Z.attrs * int * Z.term * Z.term
 
 type ho_whd_result =
    | Sort of int
@@ -40,7 +41,7 @@ let term_of_whdr = function
    | Sort_ h             -> Z.Sort h
    | LRef_ (i, _)        -> Z.LRef i
    | GRef_ (_, uri, _)   -> Z.GRef uri
-   | Bind_ (l, id, w, t) -> Z.bind_abst l id w t
+   | Bind_ (a, l, w, t) -> Z.bind_abst a l w t
 
 let level = 5
 
@@ -57,7 +58,7 @@ let empty_machine = {i = 0; c = Z.empty_lenv; s = []}
 let inc m = {m with i = succ m.i}
 
 let unwind_to_term f m t =
-   let map f t (l, id, b) = f (Z.Bind (l, id, b, t)) in
+   let map f t (a, l, b) = f (Z.Bind (a, l, b, t)) in
    let f mc = C.list_fold_left f map t mc in
    Z.contents f m.c
 
@@ -66,16 +67,13 @@ let unwind_stack f m =
    C.list_map f map m.s
 
 let get f c m i =
-   let f = function
-      | Some (_, b) -> f b
-      | None        -> assert false
-   in
-   let f c = Z.get f c i in
+   let f _ b = f b in
+   let f c = Z.get C.err f c i in
    Z.append f c m.c
 
-let push msg f c m l id w = 
+let push msg f c m a l w = 
    assert (m.s = []);
-   let f w = Z.push msg f c l id (Z.Abst w) in
+   let f w = Z.push msg f c a l (Z.Abst w) in
    unwind_to_term f m w
 
 (* to share *)
@@ -95,18 +93,18 @@ let rec whd f c m x =
       get f c m i
    | Z.Cast (_, t)               -> whd f c m t
    | Z.Appl (v, t)               -> whd f c {m with s = v :: m.s} t   
-   | Z.Bind (l, id, Z.Abst w, t) -> 
+   | Z.Bind (a, l, Z.Abst w, t) ->
       begin match m.s with
-         | []      -> f m (Bind_ (l, id, w, t))
+         | []      -> f m (Bind_ (a, l, w, t))
         | v :: tl -> 
-            let nl = Z.new_location () in
+            let nl = J.new_location () in
            let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
-           Z.push "!" f m.c nl id (Z.Abbr (Z.Cast (w, v)))
+           Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v)))
       end
-   | Z.Bind (l, id, b, t)         -> 
-      let nl = Z.new_location () in
+   | Z.Bind (a, l, b, t)         -> 
+      let nl = J.new_location () in
       let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
-      Z.push "!" f m.c nl id b
+      Z.push "!" f m.c a nl b
 
 (* Interface functions ******************************************************)
 
@@ -157,20 +155,20 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 =
          whd (aux m1 r1) c m2 v2
       | GRef_ (_, _, E.Abbr v1), _                         ->
         whd (aux_rev m2 r2) c m1 v1      
-      | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2)   ->
-          let l = Z.new_location () in
+      | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2)     ->
+          let l = J.new_location () in
           let h c =
              let m1, m2 = inc m1, inc m2 in
              let f t1 = ZS.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in
              ZS.subst f l l1 t1
         in
-         let f r = if r then push "!" h c m1 l id1 w1 else f false in
+         let f r = if r then push "!" h c m1 a1 l w1 else f false in
         are_convertible f ~si a c m1 w1 m2 w2
 (* we detect the AUT-QE reduction rule for type/prop inclusion *)      
-      | Sort_ _, Bind_ (l2, id2, w2, t2) when si           ->
+      | Sort_ _, Bind_ (a2, l2, w2, t2) when si           ->
         let m1, m2 = inc m1, inc m2 in
         let f c = are_convertible f ~si a c m1 (term_of_whdr r1) m2 t2 in
-        push "nsi" f c m2 l2 id2 w2
+        push "nsi" f c m2 a2 l2 w2
       | _                                                  -> f false
    and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in
    let g m1 r1 = whd (aux m1 r1) c m2 t2 in