--- a/Admin/polyml/future/ROOT.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/Admin/polyml/future/ROOT.ML Sun Aug 21 13:36:23 2011 +0200
@@ -78,7 +78,6 @@
use "General/table.ML";
use "General/graph.ML";
use "General/ord_list.ML";
-use "General/balanced_tree.ML";
structure Position =
struct
--- a/src/HOL/Library/Multiset.thy Sat Aug 20 15:19:35 2011 -0700
+++ b/src/HOL/Library/Multiset.thy Sun Aug 21 13:36:23 2011 +0200
@@ -1598,7 +1598,7 @@
definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
"image_mset f = fold_mset (op + o single o f) {#}"
-interpretation image_fun_commute: comp_fun_commute "op + o single o f"
+interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
proof qed (simp add: add_ac fun_eq_iff)
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
--- a/src/HOL/Tools/Function/context_tree.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/HOL/Tools/Function/context_tree.ML Sun Aug 21 13:36:23 2011 +0200
@@ -205,7 +205,7 @@
SOME _ => (T, x)
| NONE =>
let
- val (T', x') = fold fill_table (Int_Graph.imm_succs G i) (T, x)
+ val (T', x') = Int_Graph.Keys.fold fill_table (Int_Graph.imm_succs G i) (T, x)
val (v, x'') = f (the o Inttab.lookup T') i x'
in
(Inttab.update (i, v) T', x'')
@@ -226,7 +226,7 @@
fun sub_step lu i x =
let
val (ctxt', subtree) = nth branches i
- val used = fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
+ val used = Int_Graph.Keys.fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x
val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *)
in
@@ -264,7 +264,7 @@
fun sub_step lu i x =
let
val ((fixes, assumes), st) = nth branches i
- val used = map lu (Int_Graph.imm_succs deps i)
+ val used = map lu (Int_Graph.immediate_succs deps i)
|> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
|> filter_out Thm.is_reflexive
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Aug 21 13:36:23 2011 +0200
@@ -303,7 +303,7 @@
val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
Termtab.update (const, consts)) consts) constss;
fun succs consts = consts
- |> maps (Term_Graph.imm_succs gr)
+ |> maps (Term_Graph.immediate_succs gr)
|> subtract eq_cname consts
|> map (the o Termtab.lookup mapping)
|> distinct (eq_list eq_cname);
--- a/src/Pure/Concurrent/future.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Concurrent/future.ML Sun Aug 21 13:36:23 2011 +0200
@@ -62,12 +62,13 @@
val fork: (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
+ val joins: 'a future list -> 'a list
val join: 'a future -> 'a
val join_tasks: task list -> unit
val value_result: 'a Exn.result -> 'a future
val value: 'a -> 'a future
+ val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
val map: ('a -> 'b) -> 'a future -> 'b future
- val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
val promise_group: group -> (unit -> unit) -> 'a future
val promise: (unit -> unit) -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
@@ -185,13 +186,21 @@
(* cancellation primitives *)
fun cancel_now group = (*requires SYNCHRONIZED*)
- Task_Queue.cancel (! queue) group;
+ let
+ val (tasks, threads) = Task_Queue.cancel (! queue) group;
+ val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+ in tasks end;
+
+fun cancel_all () = (*requires SYNCHRONIZED*)
+ let
+ val (groups, threads) = Task_Queue.cancel_all (! queue);
+ val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+ in groups end;
fun cancel_later group = (*requires SYNCHRONIZED*)
(Unsynchronized.change canceled (insert Task_Queue.eq_group group);
broadcast scheduler_event);
-
fun interruptible_task f x =
(if Multithreading.available then
Multithreading.with_attributes
@@ -379,7 +388,7 @@
handle exn =>
if Exn.is_interrupt exn then
(Multithreading.tracing 1 (fn () => "Interrupt");
- List.app cancel_later (Task_Queue.cancel_all (! queue));
+ List.app cancel_later (cancel_all ());
broadcast_work (); true)
else reraise exn;
@@ -534,6 +543,7 @@
end;
fun join_result x = singleton join_results x;
+fun joins xs = Par_Exn.release_all (join_results xs);
fun join x = Exn.release (join_result x);
fun join_tasks [] = ()
@@ -556,6 +566,10 @@
fun value x = value_result (Exn.Res x);
+fun cond_forks args es =
+ if Multithreading.enabled () then forks args es
+ else map (fn e => value_result (Exn.interruptible_capture e ())) es;
+
fun map_future f x =
let
val task = task_of x;
@@ -569,16 +583,12 @@
in
if extended then Future {promised = false, task = task, result = result}
else
- (singleton o forks)
+ (singleton o cond_forks)
{name = "map_future", group = SOME group, deps = [task],
pri = Task_Queue.pri_of_task task, interrupts = true}
(fn () => f (join x))
end;
-fun cond_forks args es =
- if Multithreading.enabled () then forks args es
- else map (fn e => value_result (Exn.interruptible_capture e ())) es;
-
(* promised futures -- fulfilled by external means *)
--- a/src/Pure/Concurrent/par_exn.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Concurrent/par_exn.ML Sun Aug 21 13:36:23 2011 +0200
@@ -43,7 +43,7 @@
| par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
fun make exns =
- (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
+ (case Ord_List.unions exn_ord (map par_exns exns) of
[] => Exn.Interrupt
| es => Par_Exn es);
--- a/src/Pure/Concurrent/task_queue.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Concurrent/task_queue.ML Sun Aug 21 13:36:23 2011 +0200
@@ -31,8 +31,8 @@
val known_task: queue -> task -> bool
val all_passive: queue -> bool
val status: queue -> {ready: int, pending: int, running: int, passive: int}
- val cancel: queue -> group -> task list
- val cancel_all: queue -> group list
+ val cancel: queue -> group -> task list * Thread.thread list
+ val cancel_all: queue -> group list * Thread.thread list
val finish: task -> queue -> bool * queue
val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
@@ -211,9 +211,11 @@
(* job status *)
-fun ready_job task (Job list, ([], _)) = SOME (task, rev list)
- | ready_job task (Passive abort, ([], _)) =
- if is_canceled (group_of_task task) then SOME (task, [fn _ => abort ()])
+fun ready_job task (Job list, (deps, _)) =
+ if Task_Graph.Keys.is_empty deps then SOME (task, rev list) else NONE
+ | ready_job task (Passive abort, (deps, _)) =
+ if Task_Graph.Keys.is_empty deps andalso is_canceled (group_of_task task)
+ then SOME (task, [fn _ => abort ()])
else NONE
| ready_job _ _ = NONE;
@@ -232,7 +234,7 @@
val (x, y, z, w) =
Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
(case job of
- Job _ => if null deps then (x + 1, y, z, w) else (x, y + 1, z, w)
+ Job _ => if Task_Graph.Keys.is_empty deps then (x + 1, y, z, w) else (x, y + 1, z, w)
| Running _ => (x, y, z + 1, w)
| Passive _ => (x, y, z, w + 1)))
jobs (0, 0, 0, 0);
@@ -248,12 +250,13 @@
let
val _ = cancel_group group Exn.Interrupt;
val running =
- Tasks.fold (fn (task, _) =>
- (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
- (get_tasks groups (group_id group)) [];
- val threads = fold (insert Thread.equal o #2) running [];
- val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
- in map #1 running end;
+ Tasks.fold (fn (task, _) => fn (tasks, threads) =>
+ (case get_job jobs task of
+ Running thread => (task :: tasks, insert Thread.equal thread threads)
+ | Passive _ => (task :: tasks, threads)
+ | _ => (tasks, threads)))
+ (get_tasks groups (group_id group)) ([], []);
+ in running end;
fun cancel_all (Queue {jobs, ...}) =
let
@@ -266,9 +269,8 @@
Running t => (insert eq_group group groups, insert Thread.equal t running)
| _ => (groups, running))
end;
- val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []);
- val _ = List.app Simple_Thread.interrupt_unsynchronized running;
- in running_groups end;
+ val running = Task_Graph.fold cancel_job jobs ([], []);
+ in running end;
(* finish *)
@@ -278,7 +280,7 @@
val group = group_of_task task;
val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
val jobs' = Task_Graph.del_node task jobs;
- val maximal = null (Task_Graph.imm_succs jobs task);
+ val maximal = Task_Graph.is_maximal jobs task;
in (maximal, make_queue groups' jobs') end;
@@ -342,7 +344,7 @@
else
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)
+ NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks)
| some => some)
end;
--- a/src/Pure/General/graph.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/General/graph.ML Sun Aug 21 13:36:23 2011 +0200
@@ -7,6 +7,14 @@
signature GRAPH =
sig
type key
+ structure Keys:
+ sig
+ type T
+ val is_empty: T -> bool
+ val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a
+ val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a
+ val dest: T -> key list
+ end
type 'a T
exception DUP of key
exception SAME
@@ -15,20 +23,24 @@
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 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
+ val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
+ val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
val subgraph: (key -> bool) -> 'a T -> 'a T
- val get_entry: 'a T -> key -> key * ('a * (key list * key list)) (*exception UNDEF*)
+ val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*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
val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
- val imm_preds: 'a T -> key -> key list
- val imm_succs: 'a T -> key -> key list
+ val imm_preds: 'a T -> key -> Keys.T
+ val imm_succs: 'a T -> key -> Keys.T
+ val immediate_preds: 'a T -> key -> key list
+ val immediate_succs: 'a T -> key -> key list
val all_preds: 'a T -> key list -> key list
val all_succs: 'a T -> key list -> key list
+ val minimals: 'a T -> key list
+ val maximals: 'a T -> key list
+ val is_minimal: 'a T -> key -> bool
+ val is_maximal: 'a T -> key -> bool
val strong_conn: 'a T -> key list list
val new_node: key * 'a -> 'a T -> 'a T (*exception DUP*)
val default_node: key * 'a -> 'a T -> 'a T
@@ -59,27 +71,38 @@
(* keys *)
type key = Key.key;
-
val eq_key = is_equal o Key.ord;
-val member_key = member eq_key;
-val remove_key = remove eq_key;
+structure Table = Table(Key);
+
+structure Keys =
+struct
+abstype T = Keys of unit Table.table
+with
-(* tables and sets of keys *)
+val empty = Keys Table.empty;
+fun is_empty (Keys tab) = Table.is_empty tab;
-structure Table = Table(Key);
-type keys = unit Table.table;
+fun member (Keys tab) = Table.defined tab;
+fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab);
+fun remove x (Keys tab) = Keys (Table.delete_safe x tab);
+
+fun fold f (Keys tab) = Table.fold (f o #1) tab;
+fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
-val empty_keys = Table.empty: keys;
+fun make xs = Basics.fold insert xs empty;
+fun dest keys = fold_rev cons keys [];
-fun member_keys tab = Table.defined (tab: keys);
-fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
+fun filter P keys = fold (fn x => P x ? insert x) keys empty;
+
+end;
+end;
(* graphs *)
-datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
+datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table;
exception DUP = Table.DUP;
exception UNDEF = Table.UNDEF;
@@ -88,18 +111,16 @@
val empty = Graph Table.empty;
fun is_empty (Graph tab) = Table.is_empty tab;
fun keys (Graph tab) = Table.keys tab;
-fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
+fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
fun get_first f (Graph tab) = Table.get_first f tab;
fun fold_graph f (Graph tab) = Table.fold f tab;
-fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
-fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G [];
-
fun subgraph P G =
let
fun subg (k, (i, (preds, succs))) =
- if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I;
+ if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs)))
+ else I;
in Graph (fold_graph subg G Table.empty) end;
fun get_entry (Graph tab) x =
@@ -132,20 +153,29 @@
fun reachable next xs =
let
fun reach x (rs, R) =
- if member_keys R x then (rs, R)
- else fold reach (next x) (rs, insert_keys x R) |>> cons x;
+ if Keys.member R x then (rs, R)
+ else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
fun reachs x (rss, R) =
reach x ([], R) |>> (fn rs => rs :: rss);
- in fold reachs xs ([], empty_keys) end;
+ in fold reachs xs ([], Keys.empty) end;
(*immediate*)
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;
+fun immediate_preds G = Keys.dest o imm_preds G;
+fun immediate_succs G = Keys.dest o imm_succs G;
+
(*transitive*)
fun all_preds G = flat o #1 o reachable (imm_preds G);
fun all_succs G = flat o #1 o reachable (imm_succs G);
+(*minimal and maximal elements*)
+fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
+fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
+fun is_minimal G x = Keys.is_empty (imm_preds G x);
+fun is_maximal G x = Keys.is_empty (imm_succs G x);
+
(*strongly connected components; see: David King and John Launchbury,
"Structuring Depth First Search Algorithms in Haskell"*)
fun strong_conn G =
@@ -155,43 +185,44 @@
(* nodes *)
fun new_node (x, info) (Graph tab) =
- Graph (Table.update_new (x, (info, ([], []))) tab);
+ Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
fun default_node (x, info) (Graph tab) =
- Graph (Table.default (x, (info, ([], []))) tab);
+ Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
fun del_nodes xs (Graph tab) =
Graph (tab
|> fold Table.delete xs
|> Table.map (fn _ => fn (i, (preds, succs)) =>
- (i, (fold remove_key xs preds, fold remove_key xs succs))));
+ (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
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)));
+ fun del_adjacent which y =
+ Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps)));
val (preds, succs) = #2 (#2 (get_entry G x));
in
Graph (tab
|> Table.delete x
- |> fold (del_adjacent apsnd) preds
- |> fold (del_adjacent apfst) succs)
+ |> Keys.fold (del_adjacent apsnd) preds
+ |> Keys.fold (del_adjacent apfst) succs)
end;
(* edges *)
-fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
+fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
fun add_edge (x, y) G =
if is_edge G (x, y) then G
else
- G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
- |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
+ G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs)))
+ |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs)));
fun del_edge (x, y) G =
if is_edge G (x, y) then
- G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
- |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
+ G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
+ |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
else G;
fun diff_edges G1 G2 =
@@ -203,7 +234,7 @@
(* join and merge *)
-fun no_edges (i, _) = (i, ([], []));
+fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
fun join f (G1 as Graph tab1, G2 as Graph tab2) =
let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
@@ -227,11 +258,11 @@
fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
fun irreds [] xs' = xs'
| irreds (x :: xs) xs' =
- if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse
+ if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse
exists (red x) xs orelse exists (red x) xs'
then irreds xs xs'
else irreds xs (x :: xs');
- in irreds (imm_preds G z) [] end;
+ in irreds (immediate_preds G z) [] end;
fun irreducible_paths G (x, y) =
let
@@ -249,8 +280,8 @@
val (_, X) = reachable (imm_succs G) [x];
fun paths path z =
if not (null path) andalso eq_key (x, z) then [z :: path]
- else if member_keys X z andalso not (member_key path z)
- then maps (paths (z :: path)) (imm_preds G z)
+ else if Keys.member X z andalso not (member eq_key path z)
+ then maps (paths (z :: path)) (immediate_preds G z)
else [];
in paths [] y end;
@@ -297,7 +328,7 @@
val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
let
val a = get_node G x;
- val deps = imm_preds G x |> map (fn y =>
+ val deps = immediate_preds G x |> map (fn y =>
(case Table.lookup tab y of
SOME b => (y, b)
| NONE => raise DEP (x, y)));
--- a/src/Pure/General/ord_list.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/General/ord_list.ML Sun Aug 21 13:36:23 2011 +0200
@@ -14,6 +14,7 @@
val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
val subset: ('b * 'a -> order) -> 'b T * 'a T -> bool
val union: ('a * 'a -> order) -> 'a T -> 'a T -> 'a T
+ val unions: ('a * 'a -> order) -> 'a T list -> 'a T
val merge: ('a * 'a -> order) -> 'a T * 'a T -> 'a T
val inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
@@ -86,6 +87,15 @@
| GREATER => y :: unio lst1 ys);
in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
+fun unions ord lists =
+ let
+ fun unios (xs :: ys :: rest) acc = unios rest (union ord xs ys :: acc)
+ | unios [xs] (ys :: acc) = unios (union ord xs ys :: acc) []
+ | unios [xs] [] = xs
+ | unios [] [] = []
+ | unios [] acc = unios acc [];
+ in unios lists [] end;
+
fun merge ord (list1, list2) = union ord list2 list1;
(*intersection: filter second list for elements present in first list*)
--- a/src/Pure/General/table.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/General/table.ML Sun Aug 21 13:36:23 2011 +0200
@@ -340,7 +340,7 @@
in
fun delete key tab = snd (snd (del (SOME key) tab));
-fun delete_safe key tab = delete key tab handle UNDEF _ => tab;
+fun delete_safe key tab = if defined tab key then delete key tab else tab;
end;
--- a/src/Pure/Isar/isar_cmd.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Isar/isar_cmd.ML Sun Aug 21 13:36:23 2011 +0200
@@ -407,7 +407,7 @@
val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
val classes = Sorts.classes_of algebra;
fun entry (c, (i, (_, cs))) =
- (i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs,
+ (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
dir = "", unfold = true, path = ""});
val gr =
Graph.fold (cons o entry) classes []
--- a/src/Pure/PIDE/document.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/PIDE/document.ML Sun Aug 21 13:36:23 2011 +0200
@@ -145,7 +145,8 @@
|> default_node name
|> fold default_node parents;
val nodes2 = nodes1
- |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
+ |> Graph.Keys.fold
+ (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
val (header', nodes3) =
(header, Graph.add_deps_acyclic (name, parents) nodes2)
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
@@ -371,7 +372,7 @@
|> set_result result;
in ((assigns, execs, [(name, node')]), node') end)
end))
- |> Future.join_results |> Par_Exn.release_all |> map #1;
+ |> Future.joins |> map #1;
val state' = state
|> fold (fold define_exec o #2) updates
--- a/src/Pure/Thy/thm_deps.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Thy/thm_deps.ML Sun Aug 21 13:36:23 2011 +0200
@@ -40,7 +40,7 @@
path = "",
parents = parents};
in cons entry end;
- val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
+ val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
in Present.display_graph (sort_wrt #ID deps) end;
@@ -66,7 +66,8 @@
val used =
Proofterm.fold_body_thms
(fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
- (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) new_thms) Symtab.empty;
+ (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
+ Symtab.empty;
fun is_unused a = not (Symtab.defined used a);
--- a/src/Pure/Thy/thy_info.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Thy/thy_info.ML Sun Aug 21 13:36:23 2011 +0200
@@ -113,10 +113,6 @@
val is_finished = is_none o get_deps;
val master_directory = master_dir o get_deps;
-fun get_parents name =
- thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
- error (loader_msg "nothing known about theory" [name]);
-
(* access theory *)
@@ -130,6 +126,8 @@
SOME theory => theory
| _ => error (loader_msg "undefined theory entry for" [name]));
+val get_imports = Thy_Load.imports_of o get_theory;
+
fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
(case get_deps name of
NONE => []
@@ -242,7 +240,7 @@
fun check_deps dir name =
(case lookup_deps name of
- SOME NONE => (true, NONE, get_parents name)
+ SOME NONE => (true, NONE, get_imports name)
| NONE =>
let val {master, text, imports, ...} = Thy_Load.check_thy dir name
in (false, SOME (make_deps master imports, text), imports) end
--- a/src/Pure/axclass.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/axclass.ML Sun Aug 21 13:36:23 2011 +0200
@@ -220,7 +220,9 @@
in ((c1_pred, c2_succ), th') end;
val new_classrels =
- Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
+ Library.map_product pair
+ (c1 :: Graph.immediate_preds classes c1)
+ (c2 :: Graph.immediate_succs classes c2)
|> filter_out ((op =) orf Symreltab.defined classrels)
|> map gen_classrel;
val needed = not (null new_classrels);
--- a/src/Pure/proofterm.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/proofterm.ML Sun Aug 21 13:36:23 2011 +0200
@@ -37,17 +37,17 @@
type oracle = string * term
type pthm = serial * (string * term * proof_body future)
- val join_body: proof_body -> unit
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
+ val join_bodies: proof_body list -> unit
val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
val oracle_ord: oracle * oracle -> order
val thm_ord: pthm * pthm -> order
- val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
- val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
+ val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
+ val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
val all_oracles_of: proof_body -> oracle Ord_List.T
val approximate_proof_body: proof -> proof_body
@@ -171,13 +171,11 @@
type oracle = string * term;
type pthm = serial * (string * term * proof_body future);
-fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
-fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
-fun join_body (PBody {thms, ...}) = join_thms thms;
-
fun proof_of (PBody {proof, ...}) = proof;
val join_proof = Future.join #> proof_of;
+fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
+
(***** proof atoms *****)
@@ -208,6 +206,8 @@
in (f (name, prop, body') x', seen') end);
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
+fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
+
fun status_of bodies =
let
fun status (PBody {oracles, thms, ...}) x =
@@ -237,8 +237,8 @@
val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
-val merge_oracles = Ord_List.union oracle_ord;
-val merge_thms = Ord_List.union thm_ord;
+val unions_oracles = Ord_List.unions oracle_ord;
+val unions_thms = Ord_List.unions thm_ord;
val all_oracles_of =
let
@@ -249,8 +249,8 @@
let
val body' = Future.join body;
val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
- in (merge_oracles oracles x', seen') end);
- in fn body => #1 (collect body ([], Inttab.empty)) end;
+ in (if null oracles then x' else oracles :: x', seen') end);
+ in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
fun approximate_proof_body prf =
let
@@ -1385,8 +1385,11 @@
fun fulfill_norm_proof thy ps body0 =
let
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
- val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
- val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+ val oracles =
+ unions_oracles
+ (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
+ val thms =
+ unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
fun fill (Promise (i, prop, Ts)) =
@@ -1396,12 +1399,9 @@
| fill _ = NONE;
val (rules, procs) = get_data thy;
val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
- val _ = join_thms thms;
in PBody {oracles = oracles, thms = thms, proof = proof} end;
-fun fulfill_proof_future _ [] postproc body =
- if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
- else Future.map postproc body
+fun fulfill_proof_future _ [] postproc body = Future.map postproc body
| fulfill_proof_future thy promises postproc body =
(singleton o Future.forks)
{name = "Proofterm.fulfill_proof_future", group = NONE,
@@ -1460,11 +1460,10 @@
fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
val body0 =
if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
- else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
else
- (singleton o Future.forks)
+ (singleton o Future.cond_forks)
{name = "Proofterm.prepare_thm_proof", group = NONE,
- deps = [], pri = ~1, interrupts = true}
+ deps = [], pri = 0, interrupts = true}
(make_body0 o full_proof0);
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
--- a/src/Pure/sorts.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/sorts.ML Sun Aug 21 13:36:23 2011 +0200
@@ -128,7 +128,7 @@
fun all_classes (Algebra {classes, ...}) = Graph.all_preds classes (Graph.maximals classes);
-val super_classes = Graph.imm_succs o classes_of;
+val super_classes = Graph.immediate_succs o classes_of;
(* class relations *)
@@ -413,7 +413,7 @@
end;
fun derive (_, []) = []
- | derive (T as Type (a, Us), S) =
+ | derive (Type (a, Us), S) =
let
val Ss = mg_domain algebra a S;
val dom = map2 (fn U => fn S => derive (U, S) ~~ S) Us Ss;
--- a/src/Pure/thm.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/thm.ML Sun Aug 21 13:36:23 2011 +0200
@@ -95,9 +95,10 @@
val weaken: cterm -> thm -> thm
val weaken_sorts: sort list -> cterm -> cterm
val extra_shyps: thm -> sort list
- val join_proofs: thm list -> unit
+ val proof_bodies_of: thm list -> proof_body list
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
+ val join_proofs: thm list -> unit
val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
val future: thm future -> cterm -> thm
val derivation_name: thm -> string
@@ -491,8 +492,8 @@
(Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
let
val ps = Ord_List.union promise_ord ps1 ps2;
- val oras = Proofterm.merge_oracles oras1 oras2;
- val thms = Proofterm.merge_thms thms1 thms2;
+ val oras = Proofterm.unions_oracles [oras1, oras2];
+ val thms = Proofterm.unions_thms [thms1, thms2];
val prf =
(case ! Proofterm.proofs of
2 => f prf1 prf2
@@ -510,18 +511,30 @@
(* fulfilled proofs *)
-fun raw_body (Thm (Deriv {body, ...}, _)) = body;
+fun raw_body_of (Thm (Deriv {body, ...}, _)) = body;
+fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;
+
+fun join_promises [] = ()
+ | join_promises promises = join_promises_of (Future.joins (map snd promises))
+and join_promises_of thms = join_promises (maps raw_promises_of thms);
fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
- Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
- (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
-and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
+ Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body
+and fulfill_promises promises =
+ map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
-fun join_proofs thms = ignore (map fulfill_body thms);
+fun proof_bodies_of thms =
+ let
+ val _ = join_promises_of thms;
+ val bodies = map fulfill_body thms;
+ val _ = Proofterm.join_bodies bodies;
+ in bodies end;
-fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
+val proof_body_of = singleton proof_bodies_of;
val proof_of = Proofterm.proof_of o proof_body_of;
+val join_proofs = ignore o proof_bodies_of;
+
(* derivation status *)
@@ -529,7 +542,7 @@
let
val ps = map (Future.peek o snd) promises;
val bodies = body ::
- map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
+ map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
val {oracle, unfinished, failed} = Proofterm.status_of bodies;
in
{oracle = oracle,
@@ -552,7 +565,7 @@
val _ = null hyps orelse err "bad hyps";
val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
- val _ = fulfill_bodies (map #2 promises);
+ val _ = join_promises promises;
in thm end;
fun future future_thm ct =
--- a/src/Tools/Code/code_namespace.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/Code/code_namespace.ML Sun Aug 21 13:36:23 2011 +0200
@@ -86,7 +86,8 @@
end;
val proto_program = Graph.empty
|> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
- |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+ |> Graph.fold (fn (name, (_, (_, names))) =>
+ Graph.Keys.fold (add_dependency name) names) program;
(* name declarations and statement modifications *)
fun declare name (base, stmt) (gr, nsp) =
@@ -191,7 +192,8 @@
in (map_module name_fragments_common o apsnd) add_edge end;
val proto_program = empty_program
|> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
- |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+ |> Graph.fold (fn (name, (_, (_, names))) =>
+ Graph.Keys.fold (add_dependency name) names) program;
(* name declarations, data and statement modifications *)
fun make_declarations nsps (data, nodes) =
--- a/src/Tools/Code/code_preproc.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/Code/code_preproc.ML Sun Aug 21 13:36:23 2011 +0200
@@ -309,7 +309,7 @@
val diff_classes = new_classes |> subtract (op =) old_classes;
in if null diff_classes then vardeps_data
else let
- val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
+ val c_ks = Vargraph.immediate_succs (fst vardeps_data) c_k |> insert (op =) c_k;
in
vardeps_data
|> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
--- a/src/Tools/Code/code_scala.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/Code/code_scala.ML Sun Aug 21 13:36:23 2011 +0200
@@ -321,7 +321,7 @@
of Code_Thingol.Classinst _ => true
| _ => false;
val implicits = filter (is_classinst o Graph.get_node program)
- (Graph.imm_succs program name);
+ (Graph.immediate_succs program name);
in union (op =) implicits end;
fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
| modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
--- a/src/Tools/Code/code_thingol.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/Code/code_thingol.ML Sun Aug 21 13:36:23 2011 +0200
@@ -921,7 +921,7 @@
let
val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
Graph.get_node program1 Term.dummy_patternN;
- val deps = Graph.imm_succs program1 Term.dummy_patternN;
+ val deps = Graph.immediate_succs program1 Term.dummy_patternN;
val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
val deps_all = Graph.all_succs program2 deps;
val program3 = Graph.subgraph (member (op =) deps_all) program2;
@@ -1010,7 +1010,7 @@
val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
Symtab.update (const, consts)) consts) constss;
fun succs consts = consts
- |> maps (Graph.imm_succs eqngr)
+ |> maps (Graph.immediate_succs eqngr)
|> subtract (op =) consts
|> map (the o Symtab.lookup mapping)
|> distinct (op =);
--- a/src/Tools/codegen.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/codegen.ML Sun Aug 21 13:36:23 2011 +0200
@@ -756,7 +756,7 @@
let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
if a = a' then Option.map (pair x)
(find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
- (Graph.imm_succs gr x))
+ (Graph.immediate_succs gr x))
else NONE) code
in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
| string_of_cycle _ = ""
@@ -767,7 +767,7 @@
val mod_gr = fold_rev Graph.add_edge_acyclic
(maps (fn (s, (_, module, _)) => map (pair module)
(filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
- (Graph.imm_succs gr s)))) code)
+ (Graph.immediate_succs gr s)))) code)
(fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
val modules' =
rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
--- a/src/Tools/jEdit/src/session_dockable.scala Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/jEdit/src/session_dockable.scala Sun Aug 21 13:36:23 2011 +0200
@@ -54,19 +54,13 @@
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Prover status"
- private val interrupt = new Button("Interrupt") {
- reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
- }
- interrupt.tooltip = "Broadcast interrupt to all prover tasks"
-
private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
logic.listenTo(logic.selection)
logic.reactions += {
case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
}
- private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic)
+ private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/nbe.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/nbe.ML Sun Aug 21 13:36:23 2011 +0200
@@ -471,7 +471,7 @@
then (nbe_program, (maxidx, idx_tab))
else (nbe_program, (maxidx, idx_tab))
|> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
- Graph.imm_succs program name)) names);
+ Graph.immediate_succs program name)) names);
in
fold_rev add_stmts (Graph.strong_conn program)
end;
--- a/src/Tools/subtyping.ML Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/subtyping.ML Sun Aug 21 13:36:23 2011 +0200
@@ -171,10 +171,10 @@
fun get_succs G T = Typ_Graph.all_succs G [T];
fun maybe_new_typnode T G = perhaps (try (Typ_Graph.new_node (T, ()))) G;
fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G;
-fun new_imm_preds G Ts =
- subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.imm_preds G) Ts));
-fun new_imm_succs G Ts =
- subtract op= Ts (distinct (op =) (maps (Typ_Graph.imm_succs G) Ts));
+fun new_imm_preds G Ts = (* FIXME inefficient *)
+ subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_preds G) Ts));
+fun new_imm_succs G Ts = (* FIXME inefficient *)
+ subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_succs G) Ts));
(* Graph shortcuts *)
@@ -406,7 +406,7 @@
(*styps stands either for supertypes or for subtypes of a type T
in terms of the subtype-relation (excluding T itself)*)
fun styps super T =
- (if super then Graph.imm_succs else Graph.imm_preds) coes_graph T
+ (if super then Graph.immediate_succs else Graph.immediate_preds) coes_graph T
handle Graph.UNDEF _ => [];
fun minmax sup (T :: Ts) =