X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2Fbrg.ml;h=fcf503c6fb78bf7dea41ffc709cacaeea79298fa;hp=e6ac94e5bd8f4265ea05a0afe7718bab1d9f211e;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hpb=fdb80b08af83b86759833142456ce3c4f84cd80e

diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml
index e6ac94e5b..fcf503c6f 100644
--- a/helm/software/helena/src/basic_rg/brg.ml
+++ b/helm/software/helena/src/basic_rg/brg.ml
@@ -17,6 +17,7 @@ module E = Entity
 
 type uri = E.uri
 type n_attrs = E.node_attrs
+type a_attrs = E.appl_attrs
 type b_attrs = E.bind_attrs
 
 (* x-reduced abstractions are output by RTM only *)
@@ -28,7 +29,7 @@ and term = Sort of int                    (* hierarchy index *)
          | LRef of n_attrs * int          (* attrs, position index *)
          | GRef of n_attrs * uri          (* attrs, reference *)
          | Cast of term * term            (* type, term *)
-         | Appl of bool * term * term     (* extended?, argument, function *)
+         | Appl of a_attrs * term * term  (* attrs, argument, function *)
          | Bind of b_attrs * bind * term  (* attrs, binder, scope *)
 
 type entity = term E.entity (* attrs, uri, binder *)
@@ -51,7 +52,7 @@ let gref a u = GRef (a, u)
 
 let cast u t = Cast (u, t)
 
-let appl x u t = Appl (x, u, t)
+let appl a u t = Appl (a, u, t)
 
 let bind y b t = Bind (y, b, t)
 
@@ -72,12 +73,17 @@ let rec get e i = match e with
    | Cons (e, c, a, y, b) when i = 0 -> e, c, a, y, b
    | Cons (e, _, _, _, _)            -> get e (pred i)
 
+let rec mem err f e y0 = match e with
+   | Null                 -> err ()
+   | Cons (e, _, _, y, _) ->
+      if y.E.b_name = y0.E.b_name then f () else mem err f e y0
+
 (* used in BrgOutput.pp_lenv *)
 let rec fold_right f map e x = match e with   
    | Null                 -> f x
    | Cons (e, c, a, y, b) -> fold_right (map f c a y b) map e x
 
-let rec mem err f e y0 = match e with
-   | Null                 -> err ()
-   | Cons (e, _, _, y, _) ->
-      if y.E.b_name = y0.E.b_name then f () else mem err f e y0
+(* used in BrgCC.output_entity_cc0 *)
+let rec fold_left map x e = match e with   
+   | Null                 -> x
+   | Cons (e, c, a, y, b) -> fold_left map (map x c a y b) e