src/Pure/General/heap.ML
changeset 23179 8db2b22257bd
parent 18134 6450591da9f0
child 28581 6cd2e5d5c6d0
equal deleted inserted replaced
23178:07ba6b58b3d2 23179:8db2b22257bd
    12   type elem
    12   type elem
    13   type T
    13   type T
    14   val empty: T
    14   val empty: T
    15   val is_empty: T -> bool
    15   val is_empty: T -> bool
    16   val merge: T * T -> T
    16   val merge: T * T -> T
    17   val insert: elem * T -> T
    17   val insert: elem -> T -> T
    18   val min: T -> elem        (*exception Empty*)
    18   val min: T -> elem        (*exception Empty*)
    19   val delete_min: T -> T    (*exception Empty*)
    19   val delete_min: T -> T    (*exception Empty*)
    20 end;
    20 end;
    21 
    21 
    22 functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
    22 functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
    55   | merge (h1 as Heap (_, x1, a1, b1), h2 as Heap (_, x2, a2, b2)) =
    55   | merge (h1 as Heap (_, x1, a1, b1), h2 as Heap (_, x2, a2, b2)) =
    56       (case ord (x1, x2) of
    56       (case ord (x1, x2) of
    57         GREATER => heap x2 a2 (merge (h1, b2))
    57         GREATER => heap x2 a2 (merge (h1, b2))
    58       | _ => heap x1 a1 (merge (b1, h2)));
    58       | _ => heap x1 a1 (merge (b1, h2)));
    59 
    59 
    60 fun insert (x, h) = merge (Heap (1, x, Empty, Empty), h);
    60 fun insert x h = merge (Heap (1, x, Empty, Empty), h);
    61 
    61 
    62 end;
    62 end;
    63 
    63 
    64 
    64 
    65 (* minimum element *)
    65 (* minimum element *)