# HG changeset patch
# User wenzelm
# Date 1223982117 -7200
# Node ID 6cd2e5d5c6d0108ac433a10836e0bac874b5e524
# Parent  3f37ae257506a997fed449a7f2da6092586d6691
added min_elem, upto;

diff -r 3f37ae257506 -r 6cd2e5d5c6d0 src/Pure/General/heap.ML
--- a/src/Pure/General/heap.ML	Tue Oct 14 13:01:56 2008 +0200
+++ b/src/Pure/General/heap.ML	Tue Oct 14 13:01:57 2008 +0200
@@ -15,8 +15,10 @@
   val is_empty: T -> bool
   val merge: T * T -> T
   val insert: elem -> T -> T
-  val min: T -> elem        (*exception Empty*)
-  val delete_min: T -> T    (*exception Empty*)
+  val min: T -> elem            (*exception Empty*)
+  val delete_min: T -> T        (*exception Empty*)
+  val min_elem: T -> elem * T   (*exception Empty*)
+  val upto: elem -> T -> elem list * T
 end;
 
 functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
@@ -70,4 +72,17 @@
 fun delete_min Empty = raise List.Empty
   | delete_min (Heap (_, _, a, b)) = merge (a, b);
 
+fun min_elem h = (min h, delete_min h);
+
+
+(* initial interval *)
+
+nonfix upto;
+
+fun upto _ (h as Empty) = ([], h)
+  | upto limit (h as Heap (_, x, a, b)) =
+      (case ord (x, limit) of
+        GREATER => ([], h)
+      | _ => upto limit (delete_min h) |>> cons x);
+
 end;