- | ESort -> f x
- | EBind (e, {E.n_name = Some n}, Abst _) -> fold_names f map (map x n) e
- | _ -> assert false
-
-let rec mem err f e b = match e with
- | ESort -> err ()
- | EBind (e, a, _) ->
- if a.E.n_name = b.E.n_name then f () else mem err f e b
- | EAppl (e, _, _) -> mem err f e b
- | EProj (e, _, d) ->
- let err () = mem err f e b in mem err f d b
+ | 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
+ in
+ aux f e