(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) Jean-Christophe Filliatre                               *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(* Braun trees *)

module type Ordered = sig
  type t
  val le: t -> t -> bool
end

exception Empty

module Make(X: Ordered) = struct

  type t =
    | Leaf
    | Node of t * X.t * t

  let empty = Leaf

  let is_empty t = t = Leaf

  let rec insert x = function
    | Leaf ->
        Node (Leaf, x, Leaf)
    | Node (l, y, r) ->
        if X.le x y then
          Node (insert y r, x, l)
        else
          Node (insert x r, y, l)

  let rec extract = function
    | Leaf ->
        assert false
    | Node (Leaf, y, r) ->
        assert (r = Leaf);
        y, Leaf
    | Node (l, y, r) ->
        let x, l = extract l in
        x, Node (r, y, l)

  let is_above x = function
    | Leaf -> true
    | Node (_, y, _) -> X.le x y

  let rec replace_min x = function
    | Node (l, _, r) when is_above x l && is_above x r ->
        Node (l, x, r)
    | Node ((Node (_, lx, _) as l), _, r) when is_above lx r ->
        (* lx <= x, rx necessarily *)
        Node (replace_min x l, lx, r)
    | Node (l, _, (Node (_, rx, _) as r)) ->
        (* rx <= x, lx necessarily *)
        Node (l, rx, replace_min x r)
    | Leaf | Node (Leaf, _, _) | Node (_, _, Leaf) ->
        assert false

  (* merges two Braun trees [l] and [r],
     with the assumption that [size r <= size l <= size r + 1] *)
  let rec merge l r = match l, r with
    | _, Leaf ->
        l
    | Node (ll, lx, lr), Node (_, ly, _) ->
        if X.le lx ly then
          Node (r, lx, merge ll lr)
        else
          let x, l = extract l in
          Node (replace_min x r, ly, l)
    | Leaf, _ ->
        assert false (* contradicts the assumption *)

  let min = function
    | Leaf -> raise Empty
    | Node (_, x, _) -> x

  let extract_min = function
    | Leaf ->
        raise Empty
    | Node (l, x, r) ->
        x, merge l r

  (* from
       Three Algorithms on Braun Trees (Functional Pearl)
       Chris Okasaki
       J. Functional Programming 7 (6) 661-666, November 1997 *)

  let rec naive_size = function
    | Leaf -> 0
    | Node (l, _, r) -> 1 + naive_size l + naive_size r

  let rec size = function
    | Leaf -> 0
    | Node (l, _, r) -> let m = size r in 1 + 2*m + diff m l

  and diff m = function
    | Leaf ->
        assert (m = 0);
        0
    | Node (l, _, r) when m = 0 ->
        assert (l = Leaf && r = Leaf);
        1
    | Node (l, _, _) when m land 1 = 1 ->
        (* m = 2k + 1  *)
        diff (m lsr 1) l
    | Node (_, _, r) ->
        (* m = 2k + 2 *)
        diff ((m - 1) lsr 1) r

  let rec copy2 m x =
    if m = 0 then
      Node (Leaf, x, Leaf), Leaf
    else if m land 1 = 1 then
      let l, r = copy2 (m lsr 1) x in
      Node (l, x, r), Node (r, x, r)
    else
      let l, r = copy2 ((m - 1) lsr 1) x in
      Node (l, x, l), Node (l, x, r)

  let copy n x = snd (copy2 n x)

end

This document was generated using caml2html