--- a/Admin/polyml/future/ROOT.ML Sat Aug 20 19:21:03 2011 +0200
+++ b/Admin/polyml/future/ROOT.ML Sat Aug 20 20:00:55 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/Pure/Concurrent/par_exn.ML Sat Aug 20 19:21:03 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML Sat Aug 20 20:00:55 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/General/ord_list.ML Sat Aug 20 19:21:03 2011 +0200
+++ b/src/Pure/General/ord_list.ML Sat Aug 20 20:00:55 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/proofterm.ML Sat Aug 20 19:21:03 2011 +0200
+++ b/src/Pure/proofterm.ML Sat Aug 20 20:00:55 2011 +0200
@@ -46,8 +46,8 @@
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
@@ -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)) =
--- a/src/Pure/thm.ML Sat Aug 20 19:21:03 2011 +0200
+++ b/src/Pure/thm.ML Sat Aug 20 20:00:55 2011 +0200
@@ -492,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