- E.get_name err f j a
- | EBind (tl, _, _) ->
- get_name err f (pred i) j tl
- | EProj (tl, _, e) ->
- let err i = get_name err f i j tl in
- get_name err f i j e
-
-let get_index err f i j lenv =
- let rec aux f i k = function
- | ESort -> err i
- | EBind (tl, _, Abst (_, []))
- | EBind (tl, _, Abbr [])
- | EBind (tl, _, Void 0) -> aux f i k tl
- | EBind (_, a, _) when i = 0 ->
- if E.count_names a > j then f (k + j) else err i
- | EBind (tl, a, _) ->
- aux f (pred i) (k + E.count_names a) tl
- | EProj (tl, _, d) -> aux f i k (eshift C.start tl d)
+ E.name err f a
+ | EBind (tl, _, _, _) -> get_name err f (pred i) tl
+ | EProj (tl, e) ->
+ let err i = get_name err f i tl in
+ get_name err f i e
+
+let rec get e i = match e with
+ | ESort -> ESort, E.empty_node, E.empty_bind, Void
+ | EBind (e, y, a, b) when i = 0 -> e, y, a, b
+ | EBind (e, _, _, _) -> get e (pred i)
+ | EAppl (e, _, _) -> get e i
+ | EProj (e, d) -> get (append C.start e d) i
+
+let rec sub_list_strict f e l = match e, l with
+ | _, [] -> f e
+ | EBind (e, _, _, Abst _), _ :: tl -> sub_list_strict f e tl
+ | _ -> assert false
+
+let rec fold_names f map x = function
+ | ESort -> f x
+ | EBind (e, _, {E.b_name = Some n}, Abst _) -> fold_names f map (map x n) e
+ | _ -> assert false
+
+let rec mem err f e a0 = match e with
+ | ESort -> err ()
+ | EBind (e, _, a, _) ->
+ if a.E.b_name = a0.E.b_name then f () else mem err f e a0
+ | EAppl (e, _, _) -> mem err f e a0
+ | EProj (e, d) ->
+ let err () = mem err f e a0 in mem err f d a0
+
+let set_layer f n0 e =
+ let rec aux f = function
+ | ESort -> f ESort
+ | EBind (e, y, a, Abst (r, n, w)) -> aux (push_bind f y a (Abst (r, n0, w))) e
+ | EBind (e, y, a, b) -> aux (push_bind f y a b) e
+ | EAppl (e, a, v) -> aux (push_appl f a v) e
+ | EProj (e, d) -> let f d = aux (push_proj f d) e in aux f d
+ in
+ aux f e
+
+let set_attrs f a0 e =
+ let rec aux f = function
+ | ESort -> f ESort
+ | EBind (e, y, a, b) ->
+ let a = E.compose a a0 in
+ aux (push_bind f y a b) e
+ | EAppl (e, a, v) ->
+ aux (push_appl f a v) e
+ | EProj (e, d) ->
+ let f d = aux (push_proj f d) e in
+ aux f d