X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgReduction.ml;h=12e63765971c269b1679b23030c4520a69e7d037;hb=c2b39b7ef14ab610cb2056fb6b75492c7068288e;hp=08630cde61865bb923944a09fd8f6d309def6fd2;hpb=0dc347a7742e40a828fa98acba70078dd2d7cbd5;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 08630cde6..12e637659 100644
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -13,30 +13,29 @@ module U = NUri
 module C = Cps
 module S = Share
 module L = Log
+module Y = Entity
 module P = Output
 module B = Brg
 module O = BrgOutput
 module E = BrgEnvironment
 
-type machine = {
-   c: B.context;
-   s: (B.context * B.term) list;
+type kam = {
+   c: B.lenv;
+   s: (B.lenv * B.term) list;
    i: int
 }
 
-type message = (machine, B.term) Log.item list
-
 (* Internal functions *******************************************************)
 
 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 are_alpha_convertible err f t1 t2 =
    let rec aux f = function
@@ -71,16 +70,18 @@ let rec step f ?(delta=false) ?(rt=false) m x =
    | B.Sort _                  -> f m None x
    | B.GRef (_, uri)           ->
       let f = function
-         | _, _, B.Abbr (_, v) when delta ->
+         | _, _, Y.Abbr v when delta ->
 	    P.add ~gdelta:1 (); step f ~delta ~rt m v
-         | _, _, B.Abst (_, w) when rt    ->
+         | _, _, Y.Abst w when rt    ->
             P.add ~grt:1 (); step f ~delta ~rt m w	 
-	 | _, _, B.Void _                 ->
-	    assert false
-	 | e, _, b                        ->
-	    f m (Some (e, b)) x
+	 | a, _, Y.Abbr v            ->
+	    let f e = f m (Some (e, B.Abbr (a, v))) x in
+	    Y.apix C.err f a	    
+	 | a, _, Y.Abst w            ->
+	    let f e = f m (Some (e, B.Abst (a, w))) x in
+	    Y.apix C.err f a	    
       in
-      E.get_obj C.err f uri
+      E.get_entity C.err f uri
    | B.LRef (_, i)             ->
       let f c = function
 	 | B.Abbr (_, v)         ->
@@ -93,7 +94,7 @@ let rec step f ?(delta=false) ?(rt=false) m x =
 	    assert false
 	 | B.Abst (a, _) as b    ->
 	    let f e = f {m with c = c} (Some (e, b)) x in 
-	    B.apix C.err f a
+	    Y.apix C.err f a
       in 
       get C.err f m i
    | B.Cast (_, _, t)          ->
@@ -117,7 +118,7 @@ let rec step f ?(delta=false) ?(rt=false) m x =
 let push f m b = 
    assert (m.s = []);
    let b, i = match b with
-      | B.Abst (a, w) -> B.abst (B.Apix m.i :: a) w, succ m.i
+      | B.Abst (a, w) -> B.abst (Y.Apix m.i :: a) w, succ m.i
       | b             -> b, m.i
    in
    let f c = f {m with c = c; i = i} in
@@ -178,8 +179,8 @@ and ac_stacks err f m1 m2 =
 
 (* Interface functions ******************************************************)
 
-let empty_machine = { 
-   c = B.empty_context; s = []; i = 0
+let empty_kam = { 
+   c = B.empty_lenv; s = []; i = 0
 }
 
 let get err f m i =
@@ -202,8 +203,8 @@ let are_convertible err f ?(si=false) mu u mw w =
 
 let pp_term m frm t = O.specs.L.pp_term m.c frm t
 
-let pp_context frm m = O.specs.L.pp_context frm m.c
+let pp_lenv frm m = O.specs.L.pp_lenv frm m.c
 
 let specs = {
-   L.pp_term = pp_term; L.pp_context = pp_context
+   L.pp_term = pp_term; L.pp_lenv = pp_lenv
 }