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 *)
| 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 *)
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)
| 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