- common/entity: new format for kernel entities

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

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
index 628968befdd51b7beda755cf3e322e9beae926bd..a05d4b5d682b7333c26b182fd76c4ba139ccda99 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -12,6 +12,7 @@
 module U = NUri
 module C = Cps
 module L = Log
+module Y = Entity
 module B = Bag
 module O = BagOutput
 module E = BagEnvironment
@@ -26,7 +27,7 @@ type machine = {
 type whd_result =
    | Sort_ of int
    | LRef_ of int * B.term option
-   | GRef_ of B.entry
+   | GRef_ of B.entity
    | Bind_ of int * B.id * B.term * B.term
 
 type ho_whd_result =
@@ -84,7 +85,7 @@ let rec whd f c m x =
    | B.Sort h                    -> f m (Sort_ h)
    | B.GRef uri                  ->
       let f entry = f m (GRef_ entry) in
-      E.get_entry f uri
+      E.get_entity f uri
    | B.LRef i                    ->
       let f = function
          | B.Void   -> f m (LRef_ (i, None))
@@ -116,10 +117,9 @@ let rec ho_whd f c m x =
       | 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_ (_, _, B.Abst w) -> ho_whd f c m w  
-      | GRef_ (_, _, B.Abbr v) -> ho_whd f c m v
+      | GRef_ (_, _, Y.Abst w) -> ho_whd f c m w  
+      | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v
       | LRef_ (_, None)        -> assert false
-      | GRef_ (_, _, B.Void)   -> assert false
    in
    whd aux c m x
    
@@ -139,9 +139,11 @@ let rec are_convertible f ~si 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 ~si a c m1 m2 else f false
-      | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _)   ->
+      | GRef_ ((Y.Apix a1 :: _), _, Y.Abst _), 
+        GRef_ ((Y.Apix a2 :: _), _, Y.Abst _)              ->
          if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
-      | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) ->
+      | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1), 
+        GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2)             ->
          if a1 = a2 then
            let f a = 
               if a then f a else are_convertible f ~si true c m1 v1 m2 v2
@@ -150,9 +152,9 @@ let rec are_convertible f ~si 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_ (_, _, B.Abbr v2)                         ->
+      | _, GRef_ (_, _, Y.Abbr v2)                         ->
          whd (aux m1 r1) c m2 v2
-      | GRef_ (_, _, B.Abbr v1), _                         ->
+      | GRef_ (_, _, Y.Abbr v1), _                         ->
         whd (aux_rev m2 r2) c m1 v1      
       | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2)   ->
           let l = B.new_location () in