- common/entity: new format for kernel entities

[helm.git] / helm / software / lambda-delta / basic_rg / brgReduction.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index e6ea501423b65792c82c084c3c3bc696cc01f521..12e63765971c269b1679b23030c4520a69e7d037 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -13,6 +13,7 @@ module U = NUri
 module C = Cps
 module S = Share
 module L = Log
+module Y = Entity
 module P = Output
 module B = Brg
 module O = BrgOutput
@@ -69,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_entry C.err f uri
+      E.get_entity C.err f uri
    | B.LRef (_, i)             ->
       let f c = function
         | B.Abbr (_, v)         ->
@@ -91,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)          ->
@@ -115,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