more direct balanced version Ord_List.unions;
authorwenzelm
Sat Aug 20 20:00:55 2011 +0200 (2011-08-20 ago)
changeset 44334605381e7c7c5
parent 44333 cc53ce50f738
child 44335 156be0e43336
more direct balanced version Ord_List.unions;
Admin/polyml/future/ROOT.ML
src/Pure/Concurrent/par_exn.ML
src/Pure/General/ord_list.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/Admin/polyml/future/ROOT.ML	Sat Aug 20 19:21:03 2011 +0200
     1.2 +++ b/Admin/polyml/future/ROOT.ML	Sat Aug 20 20:00:55 2011 +0200
     1.3 @@ -78,7 +78,6 @@
     1.4  use "General/table.ML";
     1.5  use "General/graph.ML";
     1.6  use "General/ord_list.ML";
     1.7 -use "General/balanced_tree.ML";
     1.8  
     1.9  structure Position =
    1.10  struct
     2.1 --- a/src/Pure/Concurrent/par_exn.ML	Sat Aug 20 19:21:03 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/par_exn.ML	Sat Aug 20 20:00:55 2011 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4    | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
     2.5  
     2.6  fun make exns =
     2.7 -  (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
     2.8 +  (case Ord_List.unions exn_ord (map par_exns exns) of
     2.9      [] => Exn.Interrupt
    2.10    | es => Par_Exn es);
    2.11  
     3.1 --- a/src/Pure/General/ord_list.ML	Sat Aug 20 19:21:03 2011 +0200
     3.2 +++ b/src/Pure/General/ord_list.ML	Sat Aug 20 20:00:55 2011 +0200
     3.3 @@ -14,6 +14,7 @@
     3.4    val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
     3.5    val subset: ('b * 'a -> order) -> 'b T * 'a T -> bool
     3.6    val union: ('a * 'a -> order) -> 'a T -> 'a T -> 'a T
     3.7 +  val unions: ('a * 'a -> order) -> 'a T list -> 'a T
     3.8    val merge: ('a * 'a -> order) -> 'a T * 'a T -> 'a T
     3.9    val inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
    3.10    val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
    3.11 @@ -86,6 +87,15 @@
    3.12            | GREATER => y :: unio lst1 ys);
    3.13    in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
    3.14  
    3.15 +fun unions ord lists =
    3.16 +  let
    3.17 +    fun unios (xs :: ys :: rest) acc = unios rest (union ord xs ys :: acc)
    3.18 +      | unios [xs] (ys :: acc) = unios (union ord xs ys :: acc) []
    3.19 +      | unios [xs] [] = xs
    3.20 +      | unios [] [] = []
    3.21 +      | unios [] acc = unios acc [];
    3.22 +  in unios lists [] end;
    3.23 +
    3.24  fun merge ord (list1, list2) = union ord list2 list1;
    3.25  
    3.26  (*intersection: filter second list for elements present in first list*)
     4.1 --- a/src/Pure/proofterm.ML	Sat Aug 20 19:21:03 2011 +0200
     4.2 +++ b/src/Pure/proofterm.ML	Sat Aug 20 20:00:55 2011 +0200
     4.3 @@ -46,8 +46,8 @@
     4.4  
     4.5    val oracle_ord: oracle * oracle -> order
     4.6    val thm_ord: pthm * pthm -> order
     4.7 -  val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
     4.8 -  val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
     4.9 +  val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
    4.10 +  val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
    4.11    val all_oracles_of: proof_body -> oracle Ord_List.T
    4.12    val approximate_proof_body: proof -> proof_body
    4.13  
    4.14 @@ -237,8 +237,8 @@
    4.15  val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
    4.16  fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
    4.17  
    4.18 -val merge_oracles = Ord_List.union oracle_ord;
    4.19 -val merge_thms = Ord_List.union thm_ord;
    4.20 +val unions_oracles = Ord_List.unions oracle_ord;
    4.21 +val unions_thms = Ord_List.unions thm_ord;
    4.22  
    4.23  val all_oracles_of =
    4.24    let
    4.25 @@ -249,8 +249,8 @@
    4.26            let
    4.27              val body' = Future.join body;
    4.28              val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
    4.29 -          in (merge_oracles oracles x', seen') end);
    4.30 -  in fn body => #1 (collect body ([], Inttab.empty)) end;
    4.31 +          in (if null oracles then x' else oracles :: x', seen') end);
    4.32 +  in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
    4.33  
    4.34  fun approximate_proof_body prf =
    4.35    let
    4.36 @@ -1385,8 +1385,11 @@
    4.37  fun fulfill_norm_proof thy ps body0 =
    4.38    let
    4.39      val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
    4.40 -    val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
    4.41 -    val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
    4.42 +    val oracles =
    4.43 +      unions_oracles
    4.44 +        (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
    4.45 +    val thms =
    4.46 +      unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
    4.47      val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
    4.48  
    4.49      fun fill (Promise (i, prop, Ts)) =
     5.1 --- a/src/Pure/thm.ML	Sat Aug 20 19:21:03 2011 +0200
     5.2 +++ b/src/Pure/thm.ML	Sat Aug 20 20:00:55 2011 +0200
     5.3 @@ -492,8 +492,8 @@
     5.4      (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
     5.5    let
     5.6      val ps = Ord_List.union promise_ord ps1 ps2;
     5.7 -    val oras = Proofterm.merge_oracles oras1 oras2;
     5.8 -    val thms = Proofterm.merge_thms thms1 thms2;
     5.9 +    val oras = Proofterm.unions_oracles [oras1, oras2];
    5.10 +    val thms = Proofterm.unions_thms [thms1, thms2];
    5.11      val prf =
    5.12        (case ! Proofterm.proofs of
    5.13          2 => f prf1 prf2