# HG changeset patch # User wenzelm # Date 1313863255 -7200 # Node ID 605381e7c7c5e7afba651c5e3ea68c4830f4b2c9 # Parent cc53ce50f738f59865cdf49769140b8fa05322a3 more direct balanced version Ord_List.unions; diff -r cc53ce50f738 -r 605381e7c7c5 Admin/polyml/future/ROOT.ML --- 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 diff -r cc53ce50f738 -r 605381e7c7c5 src/Pure/Concurrent/par_exn.ML --- 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); diff -r cc53ce50f738 -r 605381e7c7c5 src/Pure/General/ord_list.ML --- 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*) diff -r cc53ce50f738 -r 605381e7c7c5 src/Pure/proofterm.ML --- 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)) = diff -r cc53ce50f738 -r 605381e7c7c5 src/Pure/thm.ML --- 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