src/Pure/General/heap.ML
changeset 28581 6cd2e5d5c6d0
parent 23179 8db2b22257bd
child 29606 fedb8be05f24
equal deleted inserted replaced
28580:3f37ae257506 28581:6cd2e5d5c6d0
    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   val min_elem: T -> elem * T   (*exception Empty*)
       
    21   val upto: elem -> T -> elem list * T
    20 end;
    22 end;
    21 
    23 
    22 functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
    24 functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
    23 struct
    25 struct
    24 
    26 
    68   | min (Heap (_, x, _, _)) = x;
    70   | min (Heap (_, x, _, _)) = x;
    69 
    71 
    70 fun delete_min Empty = raise List.Empty
    72 fun delete_min Empty = raise List.Empty
    71   | delete_min (Heap (_, _, a, b)) = merge (a, b);
    73   | delete_min (Heap (_, _, a, b)) = merge (a, b);
    72 
    74 
       
    75 fun min_elem h = (min h, delete_min h);
       
    76 
       
    77 
       
    78 (* initial interval *)
       
    79 
       
    80 nonfix upto;
       
    81 
       
    82 fun upto _ (h as Empty) = ([], h)
       
    83   | upto limit (h as Heap (_, x, a, b)) =
       
    84       (case ord (x, limit) of
       
    85         GREATER => ([], h)
       
    86       | _ => upto limit (delete_min h) |>> cons x);
       
    87 
    73 end;
    88 end;