From fdfc806afbab4cc7690cb2b73a37060f502fca9e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Glen=20M=C3=A9vel?= <glen.mevel@crans.org>
Date: Sat, 27 Jul 2024 14:50:28 +0200
Subject: [PATCH] CCHeap: avoid boxing in delete_one

---
 src/core/CCHeap.ml | 35 ++++++++++++++---------------------
 1 file changed, 14 insertions(+), 21 deletions(-)

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