Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
Sorts.certify_class: prefer the persistent name;
--- a/src/Pure/Concurrent/task_queue.ML Wed Jul 13 10:57:09 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Wed Jul 13 16:42:14 2011 +0200
@@ -318,7 +318,7 @@
| ready (task :: tasks) rest =
(case try (Task_Graph.get_entry jobs) task of
NONE => ready tasks rest
- | SOME entry =>
+ | SOME (_, entry) =>
(case ready_job task entry of
NONE => ready tasks (task :: rest)
| some => (some, List.revAppend (rest, tasks))));
@@ -327,7 +327,7 @@
| ready_dep seen (task :: tasks) =
if Tasks.defined seen task then ready_dep seen tasks
else
- let val entry as (_, (ds, _)) = Task_Graph.get_entry jobs task in
+ let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
(case ready_job task entry of
NONE => ready_dep (Tasks.update (task, ()) seen) (ds @ tasks)
| some => some)
--- a/src/Pure/General/graph.ML Wed Jul 13 10:57:09 2011 +0200
+++ b/src/Pure/General/graph.ML Wed Jul 13 16:42:14 2011 +0200
@@ -20,7 +20,7 @@
val minimals: 'a T -> key list
val maximals: 'a T -> key list
val subgraph: (key -> bool) -> 'a T -> 'a T
- val get_entry: 'a T -> key -> 'a * (key list * key list) (*exception UNDEF*)
+ val get_entry: 'a T -> key -> key * ('a * (key list * key list)) (*exception UNDEF*)
val map: (key -> 'a -> 'b) -> 'a T -> 'b T
val get_node: 'a T -> key -> 'a (*exception UNDEF*)
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
@@ -101,14 +101,14 @@
in Graph (fold_graph subg G Table.empty) end;
fun get_entry (Graph tab) x =
- (case Table.lookup tab x of
+ (case Table.lookup_key tab x of
SOME entry => entry
| NONE => raise UNDEF x);
-fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab);
+fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab);
fun map_entry_yield x f (G as Graph tab) =
- let val (a, node') = f (get_entry G x)
+ let val (a, node') = f (#2 (get_entry G x))
in (a, Graph (Table.update (x, node') tab)) end;
@@ -116,7 +116,7 @@
fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
-fun get_node G = #1 o get_entry G;
+fun get_node G = #1 o #2 o get_entry G;
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
@@ -137,8 +137,8 @@
in fold reachs xs ([], empty_keys) end;
(*immediate*)
-fun imm_preds G = #1 o #2 o get_entry G;
-fun imm_succs G = #2 o #2 o get_entry G;
+fun imm_preds G = #1 o #2 o #2 o get_entry G;
+fun imm_succs G = #2 o #2 o #2 o get_entry G;
(*transitive*)
fun all_preds G = flat o #1 o reachable (imm_preds G);
@@ -167,7 +167,7 @@
fun del_node x (G as Graph tab) =
let
fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps)));
- val (preds, succs) = #2 (get_entry G x);
+ val (preds, succs) = #2 (#2 (get_entry G x));
in
Graph (tab
|> Table.delete x
--- a/src/Pure/General/table.ML Wed Jul 13 10:57:09 2011 +0200
+++ b/src/Pure/General/table.ML Wed Jul 13 16:42:14 2011 +0200
@@ -30,6 +30,7 @@
val get_first: (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 lookup_key: 'a table -> key -> (key * 'a) option
val lookup: 'a table -> key -> 'a option
val defined: 'a table -> key -> bool
val update: key * 'a -> 'a table -> 'a table
@@ -161,25 +162,27 @@
(* lookup *)
-fun lookup tab key =
+fun lookup_key tab key =
let
fun look Empty = NONE
| look (Branch2 (left, (k, x), right)) =
(case Key.ord (key, k) of
LESS => look left
- | EQUAL => SOME x
+ | EQUAL => SOME (k, x)
| GREATER => look right)
| look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
(case Key.ord (key, k1) of
LESS => look left
- | EQUAL => SOME x1
+ | EQUAL => SOME (k1, x1)
| GREATER =>
(case Key.ord (key, k2) of
LESS => look mid
- | EQUAL => SOME x2
+ | EQUAL => SOME (k2, x2)
| GREATER => look right));
in look tab end;
+fun lookup tab key = Option.map #2 (lookup_key tab key);
+
fun defined tab key =
let
fun def Empty = false
--- a/src/Pure/sorts.ML Wed Jul 13 10:57:09 2011 +0200
+++ b/src/Pure/sorts.ML Wed Jul 13 16:42:14 2011 +0200
@@ -185,8 +185,8 @@
(* certify *)
fun certify_class algebra c =
- if can (Graph.get_node (classes_of algebra)) c then c
- else raise TYPE ("Undeclared class: " ^ quote c, [], []);
+ #1 (Graph.get_entry (classes_of algebra) c)
+ handle Graph.UNDEF _ => raise TYPE ("Undeclared class: " ^ quote c, [], []);
fun certify_sort classes = map (certify_class classes);