From 8b9f8bbd91f1661e6ce23560f888862908e0a66c Mon Sep 17 00:00:00 2001
From: Sebastien Ferre
Date: Thu, 20 Apr 2006 16:37:34 +0000
Subject: [PATCH] Abstraction over paths.

setrie.ml  652 ++++++++++++++++++++++++++++++++++++
1 file changed, 381 insertions(+), 271 deletions()
diff git a/setrie.ml b/setrie.ml
index 8a3389a..bf34414 100644
 a/setrie.ml
+++ b/setrie.ml
@@ 1,299 +1,409 @@
module type PATH =
sig
+ type elt
type t
+ val from_lset : elt LSet.t > t
+
val is_empty : t > bool
 val compare_first : t > t > int
+ val compare_head : t > t > int
+ val empty : t
val append : t > t > t
+ val iter : (elt > unit) > t > unit
+ val tail : t > t > t
val prefix_zip : t > t > t * t * t
val prefix_inter : t > t > t * t
end
+module PathLSet : PATH with type elt = int =
+ struct
+ type elt = int
+ type t = elt LSet.t
+
+ let from_lset l = l
+
+ let is_empty l = l = []
+
+ let compare_head xs ys =
+ LSet.compare (List.hd xs) (List.hd ys)
+
+ let empty = []
let compare x y = Pervasives.compare y x (* for compatibility with LSet (Oops!) *)
+ let append = (@)
type ('a,'b) tree = Node of 'a LSet.t * 'b option * ('a,'b) tree * ('a,'b) tree  Nil
 (* Node (label, value at label, elder child, next brother), to be specialized (?) when child and/or brother are Nil *)
+ let iter = List.iter
+
+ let rec tail xs ys =
+ let y = List.hd ys in
+ tail2 xs y
+ and tail2 xs y =
+ match xs with
+  [] > []
+  x::xs1 >
+ let c = LSet.compare x y in
+ if c < 0
+ then tail2 xs1 y
+ else xs
+
+ let rec prefix_zip xs ys =
+ prefix_zip_aux [] (xs,ys)
+ and prefix_zip_aux p = function
+  x::xs1, y::ys1 when x=y >
+ prefix_zip_aux (x::p) (xs1,ys1)
+  xs, ys >
+ (List.rev p), xs, ys
+
+ let rec prefix_inter xs ys =
+ prefix_inter_aux [] (xs,ys)
+ and prefix_inter_aux s (xs0,ys0) =
+ match xs0, ys0 with
+  x::xs, y::ys >
+ let c = LSet.compare x y in
+ if c = 0 then prefix_inter_aux (y::s) (xs,ys)
+ else if c < 0 then prefix_inter_aux s (xs,ys0)
+ else (* c > 0 *) prefix_inter_aux s (xs0,ys)
+  [], _ > [], (List.rev s)
+  _, [] > xs0, (List.rev s)
+ end
type ('a,'b) t = 'b option * ('a,'b) tree (* (vopt, tree) ~ Node ([], vopt, tree, Nil) *)
 (* tree, and value associated to the empty set *)
+module PathLSetLast : PATH with type elt = int =
+ struct
+ type elt = int
+ type t = elt LSet.t * elt
let make_branch ys vopt child =
 if ys = []
 then vopt, child
 else None, Node (ys, vopt, child, Nil)
+ let rec last = function
+  [] > 0
+  [e] > e
+  e::l > last l
let rec first_vopt = function
  [] > None
  None::l > first_vopt l
  Some v::l > Some v
+ let from_lset l = l, last l
(* utilitary functions on LSets *)
(*  *)
+ let is_empty (l,e) = l = []
+
+ let compare_head (xs,ex) (ys,ey) =
+ LSet.compare (List.hd xs) (List.hd ys)
+
+ let empty = [], 0
+
+ let append (l1,e1) (l2,e2) =
+ if l2 = [] then (l1,e1) else (l1@l2,e2)
+
+ let iter f (l,e) = List.iter f l
+
+ let rec tail (xs,ex) (ys,ey) =
+ if xs = []
+ then [], 0
+ else
+ let y = List.hd ys in
+ let c = LSet.compare ex y in
+ if c < 0 then [], 0
+ else if c = 0 then [ex], ex
+ else tail2 xs (List.hd ys), ex
+ and tail2 xs y =
+ match xs with
+  [] > []
+  x::xs1 >
+ let c = LSet.compare x y in
+ if c < 0
+ then tail2 xs1 y
+ else xs
+
+ let rec prefix_zip (xs,ex) (ys,ey) =
+ let prefix, xs', ys' = prefix_zip_aux ([],0) (xs,ys) in
+ prefix, (xs',ex), (ys',ey)
+ and prefix_zip_aux (p,e) = function
+  x::xs1, y::ys1 when x=y >
+ prefix_zip_aux (x::p,x) (xs1,ys1)
+  xs, ys >
+ (List.rev p,e), xs, ys
+
+ let rec prefix_inter (xs,ex) (ys,ey) =
+ let c = LSet.compare (List.hd xs) ey in
+ if c > 0 then (xs,ex), ([],0)
+ else if c = 0 then (List.tl xs,ex), ([ey],ey)
+ else (* c < 0 *)
+ let xs', yse' = prefix_inter_aux ([],0) (xs,ys) in
+ (xs',ex), yse'
+ and prefix_inter_aux (s,e) (xs0,ys0) =
+ match xs0, ys0 with
+  x::xs, y::ys >
+ let c = LSet.compare x y in
+ if c = 0 then prefix_inter_aux (y::s,y) (xs,ys)
+ else if c < 0 then prefix_inter_aux (s,e) (xs,ys0)
+ else (* c > 0 *) prefix_inter_aux (s,e) (xs0,ys)
+  [], _ > [], (List.rev s,e)
+  _, [] > xs0, (List.rev s,e)
+ end
let rec prefix_zip xs ys =
 prefix_zip_aux [] (xs,ys)
and prefix_zip_aux p = function
  x::xs1, y::ys1 when x=y >
 prefix_zip_aux (x::p) (xs1,ys1)
  xs, ys >
 List.rev p, xs, ys
+module Make (Path : PATH) =
+ struct
+ type 'b tree = Node of Path.t * 'b option * 'b tree * 'b tree  Nil
+ (* Node (path, value at path, elder child, next brother), to be specialized (?) when child and/or brother are Nil *)
+
+ type 'b t = 'b option * 'b tree (* (vopt, tree) ~ Node ([], vopt, tree, Nil) *)
+ (* tree, and value associated to the empty set *)
+
+ let make_branch ys vopt child =
+ if Path.is_empty ys
+ then vopt, child
+ else None, Node (ys, vopt, child, Nil)
+
+ let rec first_vopt = function
+  [] > None
+  None::l > first_vopt l
+  Some v::l > Some v
let rec prefix_inter xs ys =
 prefix_inter_aux [] (xs,ys)
and prefix_inter_aux s (xs0,ys0) =
 match xs0, ys0 with
  x::xs, y::ys >
 let c = compare x y in
 if c = 0 then prefix_inter_aux (y::s) (xs,ys)
 else if c < 0 then prefix_inter_aux s (xs,ys0)
 else (* c > 0 *) prefix_inter_aux s (xs0,ys)
  [], _ > [], List.rev s
  _, [] > xs0, List.rev s
(* main interface *)
(*  *)
let rec fold : ('a LSet.t > 'b > 'c > 'c) > ('a,'b) t > 'c > 'c =
 fun f (vopt,t) e >
 let e1 = match vopt with None > e  Some v > f [] v e in
 fold2 f t e1 []
and fold2 f t e ys0 =
 match t with
  Nil > e
  Node (ys, vopt, child, brother) >
 let ys' = ys0 @ ys in
 let e1 = match vopt with None > e  Some v > f ys' v e in
 let e2 = fold2 f child e1 ys' in
 let e3 = fold2 f brother e2 ys0 in
 e3


let empty : ('a,'b) t = None, Nil

let rec cardinal : ('a,'b) t > int =
 fun (vopt,tree) >
 cardinal_vopt vopt + cardinal2 tree
and cardinal2 = function
  Nil > 0
  Node (_,vopt,child,brother) >
 cardinal_vopt vopt + cardinal2 child + cardinal2 brother
and cardinal_vopt = function
  None > 0
  Some _ > 1

let singleton : 'a LSet.t > 'b > ('a,'b) t =
 fun xs v >
 if LSet.is_empty xs
 then Some v, Nil
 else None, Node (xs, Some v, Nil, Nil)

let rec add : ('b > 'b > 'b) > 'a LSet.t > 'b > ('a,'b) t > ('a,'b) t =
 fun u xs v t >
 match xs, t with
  [], (vopt,tree) > (add_vopt u vopt v, tree)
  x::xs1, (vopt,Nil) > (vopt, Node (xs, Some v, Nil, Nil))
  x::xs1, (vopt, (Node (y::ys2 as ys, vopt2, c2, b2) as tree)) >
 let c = compare x y in
 if c = 0 then
 let prefix, xs1', ys2' = prefix_zip xs1 ys2 in
 let t2' = make_branch ys2' vopt2 c2 in
 let vopt', child' = add u xs1' v t2' in
 vopt, Node (y::prefix, vopt', child', b2)
 else if c < 0 then
 vopt, Node (xs, Some v, Nil, tree)
 else (* c > 0 *)
 let _, brother' = add u xs v (None, b2) in
 vopt, Node (ys, vopt2, c2, brother')
  _ > assert false
and add_vopt u vopt v =
 match vopt with
  None > Some v
  Some v0 > Some (u v0 v)

let rec remove : 'a LSet.t > ('a,'b) t > ('a,'b) t =
 fun xs (vopt,tree) >
 if xs = []
 then None, tree
 else vopt, remove2 xs tree
and remove2 xs t =
 match xs, t with
  [], _ > t
  x::xs1, Nil > Nil
  x::xs1, Node (y::ys1 as ys, vopt, child, brother) >
 let c = compare x y in
 if c = 0 then
 let prefix, xs1', ys1' = prefix_zip xs1 ys1 in
 if ys1' <> [] then (* xs is not present *)
 t
 else if xs1' = [] then (* vopt must be set to None *)
 if child = Nil then brother else Node (ys, None, child, brother)
 else (* element to be removed is in b *)
 let child' = remove2 xs1' child in
 if vopt = None && child' = Nil then brother else Node (ys, vopt, child', brother)
 else if c < 0 then (* xs is not present *)
 t
 else (* c > 0 *) (* xs is in b *)
 let brother' = remove2 xs brother in
 Node (ys, vopt, child, brother')
  _ > assert false

let rec union : ('b > 'b > 'b) > ('a,'b) t > ('a,'b) t > ('a,'b) t =
 fun u (vopt1,tree1) (vopt2,tree2) >
 union_vopt u vopt1 vopt2, union2 u tree1 tree2
and union2 u t1 t2 =
 match t1, t2 with
  Nil, _ > t2
  _, Nil > t1
  Node (y1::ys1, vopt1, c1, b1), Node (y2::ys2, vopt2, c2, b2) >
 let c = compare y1 y2 in
 if c = 0 then
 let prefix, ys1', ys2' = prefix_zip ys1 ys2 in
 let t1' = make_branch ys1' vopt1 c1 in
 let t2' = make_branch ys2' vopt2 c2 in
 let vopt', child' = union u t1' t2' in
 let brother' = union2 u b1 b2 in
 Node (y1::prefix, vopt', child', brother')
 else if c < 0 then
 Node (y1::ys1, vopt1, c1, union2 u b1 t2)
 else (* c > 0 *)
 Node (y2::ys2, vopt2, c2, union2 u t1 b2)
  _ > assert false
and union_vopt u vopt1 vopt2 =
 match vopt1, vopt2 with
  None, _ > vopt2
  _, None > vopt1
  Some v1, Some v2 > Some (u v1 v2)


let rec exists_contains : ('a,'b) t > 'a LSet.t > ('a LSet.t > 'b > bool) > bool =
 fun (vopt,t) xs p >
 exists_contains_vopt vopt p [] 
 exists_contains2 t xs p []
and exists_contains2 t xs p path =
 match xs, t with
  _, Nil > false
  [], Node (ys, vopt, child, brother) >
 let path1 = path @ ys in
 exists_contains_vopt vopt p path1 
 exists_contains2 child [] p path1 
 exists_contains2 brother [] p path
  x::xs1, Node (y::ys1 as ys, vopt, child, brother) >
 let c = compare x y in
 if c = 0 then
 let xs1', ys1' = prefix_inter xs1 ys1 in
 if ys1' = ys1
 then
 let path1 = path @ ys in
 exists_contains_vopt vopt p path1 
 exists_contains2 child xs1' p path1
 else false
 else if c < 0 then false (* x is missing *)
 else (* c > 0 *)
 let xs1', ys1' = prefix_inter xs ys1 in
 if ys1' = ys1
 then
 let path1 = path @ ys in
 exists_contains_vopt vopt p path1 
 exists_contains2 child xs1' p path1 
 exists_contains2 brother xs p path
 else
 exists_contains2 brother xs p path
  _ > assert false
and exists_contains_vopt vopt p path =
 match vopt with
  None > false
  Some v > p path v

let rec map_inter : ('a LSet.t > 'b > 'a LSet.t > 'b option) > ('b > 'b > 'b) > ('a,'b) t > 'a LSet.t > ('a,'b) t =
 fun f u (vopt,t) xs >
 let vopt' = map_inter_vopt f vopt [] [] in
 let vopt'', t' = map_inter2 f u t xs [] [] in
 union_vopt u vopt' vopt'', t'
and map_inter2 f u t xs path path' =
 match xs, t with
  _, Nil > None, Nil
  [], Node (ys, vopt, child, brother) >
 let vopt' = map_inter_vopt f vopt (path@ys) path' in
 let child_vopt', _ (* Nil *) = map_inter2 f u child [] (path@ys) path' in
 let brother_vopt', _ (* Nil *) = map_inter2 f u brother [] path path' in
 union_vopt u vopt' (union_vopt u child_vopt' brother_vopt'), Nil
  x::xs1, Node (y::ys1, vopt, child, brother) >
 let c = compare x y in
 if c = 0 then
 let xs1', ys1' = prefix_inter xs1 ys1 in
 let path1, path1' = path @ y::ys1, path' @ y::ys1' in
 let vopt' = map_inter_vopt f vopt path1 path1' in
 let child_vopt', child' = map_inter2 f u child xs1' path1 path1' in
 let brother_vopt', brother' = map_inter2 f u brother xs1 path path' in
 brother_vopt', Node (y::ys1', union_vopt u child_vopt' vopt', child', brother')
 else if c < 0 then
 map_inter2 f u t xs1 path path'
 else (* c > 0 *)
 let xs1', ys1' = prefix_inter xs ys1 in
 let path1, path1' = path @ y::ys1, path' @ ys1' in
 let vopt' = map_inter_vopt f vopt path1 path1' in
 let child_vopt', child' = map_inter2 f u child xs1' path1 path1' in
 let brother_vopt', brother' = map_inter2 f u brother xs path path' in
 let t1 = make_branch ys1' (union_vopt u vopt' child_vopt') child' in
 let t2 = brother_vopt', brother' in
 union u t1 t2
  _ > assert false
and map_inter_vopt f vopt ys ys' =
 match vopt with
  None > None
  Some v > f ys v ys'


let rec mapmin_inter : ('a LSet.t > 'b > 'b option) > ('a,'b) t > 'a LSet.t > ('a,'b) t =
 fun f (vopt,t) xs >
 let child_vopt, t' = mapmin_inter2 f t xs [] in
 let vopt' = mapmin_inter_vopt f (first_vopt [vopt; child_vopt]) [] in
 vopt', t'
and mapmin_inter2 f t xs path' =
 match xs, t with
  _, Nil > None, Nil
  [], Node (ys, vopt, child, brother) >
 let return_vopt =
 let brother_vopt, _ (* Nil *) = mapmin_inter2 f brother [] path' in
 if brother_vopt <> None then brother_vopt
 else if vopt <> None then vopt
+ let rec fold : (Path.t > 'b > 'c > 'c) > 'b t > 'c > 'c =
+ fun f (vopt,t) e >
+ let e1 = match vopt with None > e  Some v > f Path.empty v e in
+ fold2 f t e1 Path.empty
+ and fold2 f t e ys0 =
+ match t with
+  Nil > e
+  Node (ys, vopt, child, brother) >
+ let ys' = Path.append ys0 ys in
+ let e1 = match vopt with None > e  Some v > f ys' v e in
+ let e2 = fold2 f child e1 ys' in
+ let e3 = fold2 f brother e2 ys0 in
+ e3
+
+
+ let empty : 'b t = None, Nil
+
+ let rec cardinal : 'b t > int =
+ fun (vopt,tree) >
+ cardinal_vopt vopt + cardinal2 tree
+ and cardinal2 = function
+  Nil > 0
+  Node (_,vopt,child,brother) >
+ cardinal_vopt vopt + cardinal2 child + cardinal2 brother
+ and cardinal_vopt = function
+  None > 0
+  Some _ > 1
+
+ let singleton : Path.t > 'b > 'b t =
+ fun xs v >
+ if Path.is_empty xs
+ then Some v, Nil
+ else None, Node (xs, Some v, Nil, Nil)
+
+ let rec add : ('b > 'b > 'b) > Path.t > 'b > 'b t > 'b t =
+ fun u xs v (vopt,t) >
+ if Path.is_empty xs
+ then add_vopt u vopt v, t
else
 let child_vopt, _ (* Nil *) = mapmin_inter2 f child [] path' in
 child_vopt in
 return_vopt, Nil
  x::xs1, Node (y::ys1, vopt, child, brother) >
 let c = compare x y in
 if c = 0 then
 let xs1', ys1' = prefix_inter xs1 ys1 in
 let path1' = path' @ y::ys1' in
 let child_vopt, child' = mapmin_inter2 f child xs1' path1' in
 let brother_vopt, brother' = mapmin_inter2 f brother xs1 path' in
 let vopt' = mapmin_inter_vopt f (first_vopt [vopt; child_vopt]) path1' in
 brother_vopt, Node (y::ys1', vopt', child', brother')
 else if c < 0 then
 mapmin_inter2 f t xs1 path'
 else (* c > 0 *)
 let xs1', ys1' = prefix_inter xs ys1 in
 let path1' = path' @ ys1' in
 let child_vopt, child' = mapmin_inter2 f child xs1' path1' in
 let brother_vopt, brother' = mapmin_inter2 f brother xs path' in
 let t1 =
 let vopt1 = first_vopt [vopt; child_vopt] in
 if ys1' = []
+ match t with
+  Nil > vopt, Node (xs, Some v, Nil, Nil)
+  Node (ys, vopt2, c2, b2) as tree >
+ let c = Path.compare_head xs ys in
+ if c = 0 then
+ let prefix, xs1', ys2' = Path.prefix_zip xs ys in
+ let t2' = make_branch ys2' vopt2 c2 in
+ let vopt', child' = add u xs1' v t2' in
+ vopt, Node (prefix, vopt', child', b2)
+ else if c < 0 then
+ vopt, Node (xs, Some v, Nil, tree)
+ else (* c > 0 *)
+ let _, brother' = add u xs v (None, b2) in
+ vopt, Node (ys, vopt2, c2, brother')
+ and add_vopt u vopt v =
+ match vopt with
+  None > Some v
+  Some v0 > Some (u v0 v)
+
+ let rec remove : Path.t > 'b t > 'b t =
+ fun xs (vopt,tree) >
+ if Path.is_empty xs
+ then None, tree
+ else vopt, remove2 xs tree
+ and remove2 xs t =
+ if Path.is_empty xs
+ then t
+ else
+ match t with (* xs = x::xs1, ys = y::ys1 *)
+  Nil > Nil
+  Node (ys, vopt, child, brother) >
+ let c = Path.compare_head xs ys in
+ if c = 0 then
+ let prefix, xs1', ys1' = Path.prefix_zip xs ys in
+ if not (Path.is_empty ys1') then (* xs is not present *)
+ t
+ else if Path.is_empty xs1' then (* vopt must be set to None *)
+ if child = Nil then brother else Node (ys, None, child, brother)
+ else (* element to be removed is in b *)
+ let child' = remove2 xs1' child in
+ if vopt = None && child' = Nil then brother else Node (ys, vopt, child', brother)
+ else if c < 0 then (* xs is not present *)
+ t
+ else (* c > 0 *) (* xs is in b *)
+ let brother' = remove2 xs brother in
+ Node (ys, vopt, child, brother')
+
+ let rec union : ('b > 'b > 'b) > 'b t > 'b t > 'b t =
+ fun u (vopt1,tree1) (vopt2,tree2) >
+ union_vopt u vopt1 vopt2, union2 u tree1 tree2
+ and union2 u t1 t2 =
+ match t1, t2 with
+  Nil, _ > t2
+  _, Nil > t1
+  Node (ys1, vopt1, c1, b1), Node (ys2, vopt2, c2, b2) >
+ let c = Path.compare_head ys1 ys2 in
+ if c = 0 then
+ let prefix, ys1', ys2' = Path.prefix_zip ys1 ys2 in
+ let t1' = make_branch ys1' vopt1 c1 in
+ let t2' = make_branch ys2' vopt2 c2 in
+ let vopt', child' = union u t1' t2' in
+ let brother' = union2 u b1 b2 in
+ Node (prefix, vopt', child', brother')
+ else if c < 0 then
+ Node (ys1, vopt1, c1, union2 u b1 t2)
+ else (* c > 0 *)
+ Node (ys2, vopt2, c2, union2 u t1 b2)
+ and union_vopt u vopt1 vopt2 =
+ match vopt1, vopt2 with
+  None, _ > vopt2
+  _, None > vopt1
+  Some v1, Some v2 > Some (u v1 v2)
+
+(* to be corrected
+ let rec exists_contains : 'b t > Path.t > (Path.t > 'b > bool) > bool =
+ fun (vopt,t) xs p >
+ exists_contains_vopt vopt p Path.empty 
+ exists_contains2 t xs p Path.empty
+ and exists_contains2 t xs p path =
+ match t with
+  Nil > false
+  Node (ys, vopt, child, brother) >
+ if Path.is_empty xs
then
 let return_vopt = if brother_vopt = None then vopt1 else None in
 return_vopt, child'
+ let path1 = Path.append path ys in
+ exists_contains_vopt vopt p path1 
+ exists_contains2 child xs p path1 
+ exists_contains2 brother xs p path
else
 let vopt' = mapmin_inter_vopt f vopt1 path1' in
 None, Node (ys1', vopt', child', Nil) in
 let t2 = brother_vopt, brother' in
 union (fun _ v2 > v2) t1 t2
  _ > assert false
and mapmin_inter_vopt f vopt ys' =
 match vopt with
  None > None
  Some v > f ys' v
+ let c = Path.compare_head xs ys in
+ if c = 0 then
+ let xs', ys' = Path.prefix_inter xs ys in
+ if ys' = ys
+ then
+ let path1 = Path.append path ys in
+ exists_contains_vopt vopt p path1 
+ exists_contains2 child xs' p path1
+ else false
+ else if c < 0 then false (* head xs is missing *)
+ else (* c > 0 *)
+ let xs', ys' = Path.prefix_inter xs ys in
+ if ys' = ys (* NO!! *)
+ then
+ let path1 = Path.append path ys in
+ exists_contains_vopt vopt p path1 
+ exists_contains2 child xs' p path1 
+ exists_contains2 brother xs p path
+ else
+ exists_contains2 brother xs p path
+ and exists_contains_vopt vopt p path =
+ match vopt with
+  None > false
+  Some v > p path v
+*)
+ let rec map_inter : (Path.t > 'b > Path.t > 'b option) > ('b > 'b > 'b) > 'b t > Path.t > 'b t =
+ fun f u (vopt,t) xs >
+ let vopt' = map_inter_vopt f vopt Path.empty Path.empty in
+ let vopt'', t' = map_inter2 f u t xs Path.empty Path.empty in
+ union_vopt u vopt' vopt'', t'
+ and map_inter2 f u t xs path path' =
+ match t with
+  Nil > None, Nil
+  Node (ys, vopt, child, brother) >
+ if Path.is_empty xs
+ then
+ let path1 = Path.append path ys in
+ let vopt' = map_inter_vopt f vopt path1 path' in
+ let child_vopt', _ (* Nil *) = map_inter2 f u child xs path1 path' in
+ let brother_vopt', _ (* Nil *) = map_inter2 f u brother xs path path' in
+ union_vopt u vopt' (union_vopt u child_vopt' brother_vopt'), Nil
+ else (* xs = x::xs1, ys = y::ys1 *)
+ let c = Path.compare_head xs ys in
+ if c = 0 then
+ let xs', ys' = Path.prefix_inter xs ys in
+ let path1, path1' = Path.append path ys, Path.append path' ys' in
+ let vopt' = map_inter_vopt f vopt path1 path1' in
+ let child_vopt', child' = map_inter2 f u child xs' path1 path1' in
+ let brother_vopt', brother' = map_inter2 f u brother xs path path' in
+ brother_vopt', Node (ys', union_vopt u child_vopt' vopt', child', brother')
+ else if c < 0 then
+ map_inter2 f u t (Path.tail xs ys) path path'
+ else (* c > 0 *)
+ let xs', ys' = Path.prefix_inter xs ys in
+ let path1, path1' = Path.append path ys, Path.append path' ys' in
+ let vopt' = map_inter_vopt f vopt path1 path1' in
+ let child_vopt', child' = map_inter2 f u child xs' path1 path1' in
+ let brother_vopt', brother' = map_inter2 f u brother xs path path' in
+ let t1 = make_branch ys' (union_vopt u vopt' child_vopt') child' in
+ let t2 = brother_vopt', brother' in
+ union u t1 t2
+ and map_inter_vopt f vopt ys ys' =
+ match vopt with
+  None > None
+  Some v > f ys v ys'
+
+
+ let rec mapmin_inter : (Path.t > 'b > 'b option) > 'b t > Path.t > 'b t =
+ fun f (vopt,t) xs >
+ let child_vopt, t' = mapmin_inter2 f t xs Path.empty in
+ let vopt' = mapmin_inter_vopt f (first_vopt [vopt; child_vopt]) Path.empty in
+ vopt', t'
+ and mapmin_inter2 f t xs path' =
+ match t with
+  Nil > None, Nil
+  Node (ys, vopt, child, brother) >
+ if Path.is_empty xs
+ then
+ let return_vopt =
+ let brother_vopt, _ (* Nil *) = mapmin_inter2 f brother xs path' in
+ if brother_vopt <> None then brother_vopt
+ else if vopt <> None then vopt
+ else
+ let child_vopt, _ (* Nil *) = mapmin_inter2 f child xs path' in
+ child_vopt in
+ return_vopt, Nil
+ else
+ let c = Path.compare_head xs ys in
+ if c = 0 then
+ let xs', ys' = Path.prefix_inter xs ys in (* we know that ys' is not empty *)
+ let path1' = Path.append path' ys' in
+ let child_vopt, child' = mapmin_inter2 f child xs' path1' in
+ let brother_vopt, brother' = mapmin_inter2 f brother xs path' in
+ let vopt' = mapmin_inter_vopt f (first_vopt [vopt; child_vopt]) path1' in
+ brother_vopt, Node (ys', vopt', child', brother')
+ else if c < 0 then
+ mapmin_inter2 f t (Path.tail xs ys) path'
+ else (* c > 0 *)
+ let xs', ys' = Path.prefix_inter xs ys in (* ys' may be empty *)
+ let path1' = Path.append path' ys' in
+ let child_vopt, child' = mapmin_inter2 f child xs' path1' in
+ let brother_vopt, brother' = mapmin_inter2 f brother xs path' in
+ let t1 =
+ let vopt1 = first_vopt [vopt; child_vopt] in
+ if Path.is_empty ys'
+ then
+ let return_vopt = if brother_vopt = None then vopt1 else None in
+ return_vopt, child'
+ else
+ let vopt' = mapmin_inter_vopt f vopt1 path1' in
+ None, Node (ys', vopt', child', Nil) in
+ let t2 = brother_vopt, brother' in
+ union (fun _ v2 > v2) t1 t2
+ and mapmin_inter_vopt f vopt ys' =
+ match vopt with
+  None > None
+  Some v > f ys' v
+
+ end

2.1.1