X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2FbagReduction.ml;h=b7eb88f6395ee4f3fd0a5dbb24f4d6d9450b8907;hb=ea41b1f6e212334924a8de4b2ff53b2586de9c4b;hp=c2de019cd57628f8e250a239509d541340910ae8;hpb=c52a5748465e24374aec569bf74fc85e5bbb075a;p=helm.git

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
index c2de019cd..b7eb88f63 100644
--- 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
@@ -19,14 +20,14 @@ module S = BagSubstitution
 
 type machine = {
    i: int;
-   c: B.context;
+   c: B.lenv;
    s: B.term list
 }
 
 type whd_result =
    | Sort_ of int
    | LRef_ of int * B.term option
-   | GRef_ of B.obj
+   | GRef_ of B.entity
    | Bind_ of int * B.id * B.term * B.term
 
 type ho_whd_result =
@@ -44,14 +45,14 @@ let term_of_whdr = function
 let level = 5
 
 let log1 s c t =
-   let sc, st = s ^ " in the context", "the term" in
-   L.log O.specs level (L.ct_items1 sc c st t)
+   let sc, st = s ^ " in the environment", "the term" in
+   L.log O.specs level (L.et_items1 sc c st t)
 
 let log2 s cu u ct t =
-   let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in
-   L.log O.specs level (L.ct_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+   let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
+   L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
 
-let empty_machine = {i = 0; c = B.empty_context; s = []}
+let empty_machine = {i = 0; c = B.empty_lenv; s = []}
 
 let inc m = {m with i = succ m.i}
 
@@ -83,8 +84,8 @@ let rec whd f c m x =
    match x with
    | B.Sort h                    -> f m (Sort_ h)
    | B.GRef uri                  ->
-      let f obj = f m (GRef_ obj) in
-      E.get_obj f uri
+      let f entry = f m (GRef_ entry) in
+      E.get_entity f uri
    | B.LRef i                    ->
       let f = function
          | B.Void   -> f m (LRef_ (i, None))
@@ -116,10 +117,10 @@ 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
+      | GRef_ (_, _, Y.Void)   -> assert false
    in
    whd aux c m x
    
@@ -139,9 +140,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 +153,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