src/Pure/General/heap.ML
changeset 9095 3b26cc949016
child 9413 ba209591a8d4
equal deleted inserted replaced
9094:530e7a33b3dd 9095:3b26cc949016
       
     1 (* Source code from
       
     2  *   Purely Functional Data Structures (Chapter 3)
       
     3  *   Chris Okasaki
       
     4  *   Cambridge University Press, 1998
       
     5  *
       
     6  * Copyright (c) 1998 Cambridge University Press
       
     7     ID:         $Id$
       
     8  *)
       
     9 
       
    10 signature ORDERED =
       
    11   (* a totally ordered type and its comparison functions *)
       
    12 sig
       
    13   type T
       
    14 
       
    15   val eq  : T * T -> bool
       
    16   val lt  : T * T -> bool
       
    17   val leq : T * T -> bool
       
    18 end;
       
    19 
       
    20 signature HEAP =
       
    21 sig
       
    22   structure Elem : ORDERED
       
    23 
       
    24   type Heap
       
    25 
       
    26   val empty     : Heap
       
    27   val isEmpty   : Heap -> bool
       
    28 
       
    29   val insert    : Elem.T * Heap -> Heap
       
    30   val merge     : Heap * Heap -> Heap
       
    31 
       
    32   val findMin   : Heap -> Elem.T   (* raises Empty if heap is empty *)
       
    33   val deleteMin : Heap -> Heap     (* raises Empty if heap is empty *)
       
    34 end;
       
    35 
       
    36 functor LeftistHeap (Element : ORDERED) : HEAP =
       
    37 struct
       
    38   structure Elem = Element
       
    39 
       
    40   datatype Heap = E | T of int * Elem.T * Heap * Heap
       
    41 
       
    42   fun rank E = 0
       
    43     | rank (T (r,_,_,_)) = r
       
    44   fun makeT (x, a, b) = if rank a >= rank b then T (rank b + 1, x, a, b)
       
    45                         else T (rank a + 1, x, b, a)
       
    46 
       
    47   val empty = E
       
    48   fun isEmpty E = true | isEmpty _ = false
       
    49 
       
    50   fun merge (h, E) = h
       
    51     | merge (E, h) = h
       
    52     | merge (h1 as T (_, x, a1, b1), h2 as T (_, y, a2, b2)) =
       
    53         if Elem.leq (x, y) then makeT (x, a1, merge (b1, h2))
       
    54         else makeT (y, a2, merge (h1, b2))
       
    55 
       
    56   fun insert (x, h) = merge (T (1, x, E, E), h)
       
    57 
       
    58   fun findMin E = raise List.Empty
       
    59     | findMin (T (_, x, a, b)) = x
       
    60   fun deleteMin E = raise List.Empty
       
    61     | deleteMin (T (_, x, a, b)) = merge (a, b)
       
    62 end;