# HG changeset patch
# User wenzelm
# Date 1244913554 -7200
# Node ID 63893e3a50a696306343ca943d33157a9ec3ba8c
# Parent  0b807e04f1f87b510e4fd70bac173873e1077488
native get_first, with optional boundary;
tuned signature;

diff -r 0b807e04f1f8 -r 63893e3a50a6 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sat Jun 13 19:13:27 2009 +0200
+++ b/src/Pure/General/graph.ML	Sat Jun 13 19:19:14 2009 +0200
@@ -15,7 +15,8 @@
   val is_empty: 'a T -> bool
   val keys: 'a T -> key list
   val dest: 'a T -> (key * key list) list
-  val get_first: (key * ('a * (key list * key list)) -> 'b option) -> 'a T -> 'b option
+  val get_first: key option -> (key * ('a * (key list * key list)) -> 'b option) ->
+    'a T -> 'b option
   val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
   val minimals: 'a T -> key list
   val maximals: 'a T -> key list
@@ -88,7 +89,7 @@
 fun keys (Graph tab) = Table.keys tab;
 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
 
-fun get_first f (Graph tab) = Table.get_first f tab;
+fun get_first b f (Graph tab) = Table.get_first b f tab;
 fun fold_graph f (Graph tab) = Table.fold f tab;
 
 fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
diff -r 0b807e04f1f8 -r 63893e3a50a6 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Jun 13 19:13:27 2009 +0200
+++ b/src/Pure/General/table.ML	Sat Jun 13 19:19:14 2009 +0200
@@ -26,13 +26,13 @@
   val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
+  val min_key: 'a table -> key option
+  val max_key: 'a table -> key option
+  val get_first: key option -> (key * 'a -> 'b option) -> 'a table -> 'b option
   val exists: (key * 'a -> bool) -> 'a table -> bool
   val forall: (key * 'a -> bool) -> 'a table -> bool
-  val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
-  val min_key: 'a table -> key option
-  val max_key: 'a table -> key option
+  val lookup: 'a table -> key -> 'a option
   val defined: 'a table -> key -> bool
-  val lookup: 'a table -> key -> 'a option
   val update: key * 'a -> 'a table -> 'a table
   val update_new: key * 'a -> 'a table -> 'a table                     (*exception DUP*)
   val default: key * 'a -> 'a table -> 'a table
@@ -114,17 +114,6 @@
 fun dest tab = fold_rev_table cons tab [];
 fun keys tab = fold_rev_table (cons o #1) tab [];
 
-fun get_first f tab =
-  let
-    exception FOUND of 'b option;
-    fun get entry () = (case f entry of NONE => () | some => raise FOUND some);
-  in (fold_table get tab (); NONE) handle FOUND res => res end;
-
-fun exists pred =
-  is_some o get_first (fn entry => if pred entry then SOME () else NONE);
-
-fun forall pred = not o exists (not o pred);
-
 
 (* min/max keys *)
 
@@ -141,6 +130,45 @@
   | max_key (Branch3 (_, _, _, _, right)) = max_key right;
 
 
+(* get_first *)
+
+fun get_first boundary f tab =
+  let
+    val check =
+      (case boundary of
+        NONE => (fn p => f p)
+      | SOME b => (fn p as (k, _) =>
+          (case Key.ord (b, k) of GREATER => f p | _ => NONE)));
+
+    fun get Empty = NONE
+      | get (Branch2 (left, p, right)) =
+          (case get left of
+            NONE =>
+              (case check p of
+                NONE => get right
+              | some => some)
+          | some => some)
+      | get (Branch3 (left, p, mid, q, right)) =
+          (case get left of
+            NONE =>
+              (case check p of
+                NONE =>
+                  (case get mid of
+                    NONE =>
+                      (case check q of
+                        NONE => get right
+                      | some => some)
+                  | some => some)
+              | some => some)
+          | some => some);
+  in get tab end;
+
+fun exists pred =
+  is_some o get_first NONE (fn entry => if pred entry then SOME () else NONE);
+
+fun forall pred = not o exists (not o pred);
+
+
 (* lookup *)
 
 fun lookup tab key =