+ let parallel_positions bag pos ctx id t f =
+ let rec aux bag pos ctx id = function
+ | Terms.Leaf _ as t -> f bag t pos ctx id
+ | Terms.Var _ as t -> bag,t,id
+ | Terms.Node (hd::l) as t->
+ let bag,t,id1 = f bag t pos ctx id in
+ if id = id1 then
+ let bag, l, _, id =
+ List.fold_left
+ (fun (bag,pre,post,id) t ->
+ let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
+ let newpos = (List.length pre)::pos in
+ let bag,newt,id = aux bag newpos newctx id t in
+ if post = [] then bag, pre@[newt], [], id
+ else bag, pre @ [newt], List.tl post, id)
+ (bag, [hd], List.tl l, id) l
+ in
+ bag, Terms.Node l, id
+ else bag,t,id1
+ (* else aux bag pos ctx id1 t *)
+ | _ -> assert false
+ in
+ aux bag pos ctx id t
+ ;;
+
+ let visit bag pos ctx id t f =
+ let rec aux bag pos ctx id subst = function
+ | Terms.Leaf _ as t ->
+ let bag,subst,t,id = f bag t pos ctx id
+ in assert (subst=[]); bag,t,id
+ | Terms.Var i as t ->
+ let t= Subst.apply_subst subst t in
+ bag,t,id
+ | Terms.Node (hd::l) ->
+ let bag, l, _, id =
+ List.fold_left
+ (fun (bag,pre,post,id) t ->
+ let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
+ let newpos = (List.length pre)::pos in
+ let bag,newt,id = aux bag newpos newctx id subst t in
+ if post = [] then bag, pre@[newt], [], id
+ else bag, pre @ [newt], List.tl post, id)
+ (bag, [hd], List.map (Subst.apply_subst subst) (List.tl l), id) l
+ in
+ let bag,subst,t,id1 = f bag (Terms.Node l) pos ctx id
+ in
+ if id1 = id then (assert (subst=[]); bag,t,id)
+ else aux bag pos ctx id1 subst t
+ | _ -> assert false
+ in
+ aux bag pos ctx id [] t