CCHeap: avoid boxing in delete_one

This commit is contained in:
Glen Mével 2024-07-27 14:50:28 +02:00
parent 6c810eb83d
commit fdfc806afb

View file

@ -429,29 +429,22 @@ module Make (E : PARTIAL_ORD) : S with type elt = E.t = struct
(** {2 Filtering} *) (** {2 Filtering} *)
let delete_one eq x h = let rec delete_one eq x0 = function
let rec aux = function | N (_, x, l, r) as h when E.leq x x0 ->
| E -> false, E if eq x0 x then
| N (_, y, l, r) as h -> merge l r
if eq x y then else begin
true, merge l r let l' = delete_one eq x0 l in
else if E.leq y x then ( if CCEqual.physical l' l then
let found_left, l1 = aux l in let r' = delete_one eq x0 r in
let found, r1 = if CCEqual.physical r' r then
if found_left then h
true, r
else else
aux r _make_node x l r'
in
if found then
true, _make_node y l1 r1
else else
false, h _make_node x l' r
) else end
false, h | h -> h
in
snd (aux h)
let delete_all eq x0 h = let delete_all eq x0 h =
(* Iterates [k] on sub-heaps of [h] whose merger is equal to [h] minus (* Iterates [k] on sub-heaps of [h] whose merger is equal to [h] minus