fix CCWBTree.split

This commit is contained in:
Simon Cruanes 2015-09-11 09:25:55 +02:00
parent e9d93bc02b
commit d8931e3602

View file

@ -371,10 +371,10 @@ module MakeFull(K : KEY) : S with type key = K.t = struct
but do not assume anything about weights. but do not assume anything about weights.
returns a tree with l, r, and (k,v) *) returns a tree with l, r, and (k,v) *)
let rec node_ k v l r = match l, r with let rec node_ k v l r = match l, r with
| E, E -> mk_node_ k v E E | E, E -> singleton k v
| E, o | E, o
| o, E -> add k v o | o, E -> add k v o
| N (kl, vl, ll, lr, wl), N (kr, vr, rl, rr, wr) -> | N (kl, vl, ll, lr, _), N (kr, vr, rl, rr, _) ->
let left = is_balanced l r in let left = is_balanced l r in
if left && is_balanced r l if left && is_balanced r l
then mk_node_ k v l r then mk_node_ k v l r
@ -385,7 +385,7 @@ module MakeFull(K : KEY) : S with type key = K.t = struct
(* join two trees, assuming all keys of [l] are smaller than keys of [r] *) (* join two trees, assuming all keys of [l] are smaller than keys of [r] *)
let join_ l r = match l, r with let join_ l r = match l, r with
| E, E -> E | E, E -> E
| E, o -> o | E, o
| o, E -> o | o, E -> o
| N _, N _ -> | N _, N _ ->
if weight l <= weight r if weight l <= weight r
@ -409,10 +409,10 @@ module MakeFull(K : KEY) : S with type key = K.t = struct
| 0 -> l, Some v', r | 0 -> l, Some v', r
| n when n<0 -> | n when n<0 ->
let ll, o, lr = split k l in let ll, o, lr = split k l in
ll, o, join_ lr r ll, o, node_ k' v' lr r
| _ -> | _ ->
let rl, o, rr = split k r in let rl, o, rr = split k r in
join_ l rl, o, rr node_ k' v' l rl, o, rr
(*$Q & ~small:List.length (*$Q & ~small:List.length
Q.(list (pair small_int small_int)) ( fun lst -> \ Q.(list (pair small_int small_int)) ( fun lst -> \
@ -421,12 +421,12 @@ module MakeFull(K : KEY) : S with type key = K.t = struct
let m = M.of_list lst in \ let m = M.of_list lst in \
List.for_all (fun (k,v) -> \ List.for_all (fun (k,v) -> \
let l, v', r = M.split k m in \ let l, v', r = M.split k m in \
v' = Some v && \ v' = Some v \
(M.to_seq l |> Sequence.for_all (fun (k',_) -> k' < k)) &&\ && (M.to_seq l |> Sequence.for_all (fun (k',_) -> k' < k)) \
(M.to_seq r |> Sequence.for_all (fun (k',_) -> k' > k)) &&\ && (M.to_seq r |> Sequence.for_all (fun (k',_) -> k' > k)) \
M.balanced m && \ && M.balanced m \
M.cardinal l + M.cardinal r + 1 = List.length lst) \ && M.cardinal l + M.cardinal r + 1 = List.length lst \
lst) ) lst)
*) *)
let rec merge f a b = match a, b with let rec merge f a b = match a, b with
@ -439,16 +439,15 @@ module MakeFull(K : KEY) : S with type key = K.t = struct
mk_node_or_join_ k v' (merge f l E) (merge f r E) mk_node_or_join_ k v' (merge f l E) (merge f r E)
| N (k1, v1, l1, r1, w1), N (k2, v2, l2, r2, w2) -> | N (k1, v1, l1, r1, w1), N (k2, v2, l2, r2, w2) ->
if K.compare k1 k2 = 0 if K.compare k1 k2 = 0
then then (* easy case *)
(* easy case *)
mk_node_or_join_ k1 (f k1 (Some v1) (Some v2)) mk_node_or_join_ k1 (f k1 (Some v1) (Some v2))
(merge f l1 l2) (merge f r1 r2) (merge f l1 l2) (merge f r1 r2)
else if w1 <= w2 else if w1 <= w2
then then (* split left tree *)
let l1', v1', r1' = split k2 a in let l1', v1', r1' = split k2 a in
mk_node_or_join_ k2 (f k2 v1' (Some v2)) mk_node_or_join_ k2 (f k2 v1' (Some v2))
(merge f l1' l2) (merge f r1' r2) (merge f l1' l2) (merge f r1' r2)
else else (* split right tree *)
let l2', v2', r2' = split k1 b in let l2', v2', r2' = split k1 b in
mk_node_or_join_ k1 (f k1 (Some v1) v2') mk_node_or_join_ k1 (f k1 (Some v1) v2')
(merge f l1 l2') (merge f r1 r2') (merge f l1 l2') (merge f r1 r2')