(* Leftist heap (priority queue) by Norman Ramsey *)
(* Copyright 2011, licensed Creative Commons Attribution (BY),
   i.e., attribution required, but all uses permitted 
*)

module type PQUEUE = sig
  type t
  type elem
  val empty  : t
  val insert : elem * t -> t
  val is_empty : t -> bool
  exception Empty
  val deletemin : t -> elem * t  (* raises Empty *)
  val ok : t -> bool (* satisfies invariant *)

  val merges : int ref
end


module MkTreePQ (Elem : sig
                           type t
                           val compare : t * t -> int
                         end) :
  PQUEUE with type elem = Elem.t
=
struct
  type elem = Elem.t
  type height = int
  type t = EMPTY
         | NODE of elem * height * t * t
    (* invariant:
         elem in a node is not greater than the elems in its nonempty children
         left child is at least as high as right child
         height represents true height
     *)

  let le (x1, x2) = Elem.compare (x1, x2) <= 0

  let rec height = function
    | EMPTY -> 0
    | (NODE (_, h, _, _)) -> h

  let merges = ref 0

  let rec merge = function
    | (EMPTY, q) -> q
    | (q, EMPTY) -> q
    | ((NODE (x1, _, l1, r1) as q1), (NODE (x2, _, _, _) as q2)) ->
        if le (x1, x2) then
                let (to_merge, to_stand) =
                  if height l1 > height q2 then (q2, l1) else (l1, q2) in
                let newq1 = merge (r1, to_merge) in
                let newq2 = to_stand in
                let h1 = height newq1 in
                let h2 = height newq2 in
                let h = max h1 h2 + 1 in
                let (l, r) = if h1 > h2 then (newq1, newq2) else (newq2, newq1) in
                let _ = merges := !merges + 1 in
                NODE (x1, h, l, r)
        else
            merge (q2, q1)
            
  let empty = EMPTY
  let rec insert = function
    | (x, EMPTY) -> NODE (x, 1, EMPTY, EMPTY)
    | (x, q) -> merge (insert(x, empty), q)

  let is_empty = function
    | EMPTY -> true
    | (NODE _) -> false

  exception Empty
  let deletemin = function
    | EMPTY -> raise Empty
    | (NODE (x, _, q, q')) -> (x, merge (q, q'))


  let rec ok_h_le h x q =
       (* q satisfies invariant, has height h, each elem at least x *)
    match q with
    | EMPTY -> h = 0
    | NODE (x', h', l, r) ->
                 h = h' && le(x, x') &&
                 (h = height l + 1 || h = height r + 1) &&
                 h > height l && h > height r &&
                 ok_h_le (height l) x' l && ok_h_le (height r) x' r

  let ok = function
    | EMPTY -> true
    | (NODE (x, h, _, _) as q) -> ok_h_le h x q

end