# HG changeset patch
# User wenzelm
# Date 1498158613 -7200
# Node ID fcd09fc36d7fba1dc63eca0e2a86dcc0235efae9
# Parent  1bd268ab885cd8d2dce9c90556e8a9265ee26208
consolidate proofs more simultaneously;

diff -r 1bd268ab885c -r fcd09fc36d7f src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 22 15:20:32 2017 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 22 21:10:13 2017 +0200
@@ -959,7 +959,7 @@
     | SOME {vcs, path, ...} =>
         let
           val (proved, unproved) = partition_vcs vcs;
-          val _ = List.app Thm.consolidate (maps (#2 o snd) proved);
+          val _ = Thm.consolidate (maps (#2 o snd) proved);
           val (proved', proved'') =
             List.partition (fn (_, (_, thms, _, _)) =>
               exists (#oracle o Thm.peek_status) thms) proved;
diff -r 1bd268ab885c -r fcd09fc36d7f src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Thu Jun 22 15:20:32 2017 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Jun 22 21:10:13 2017 +0200
@@ -17,6 +17,7 @@
   val is_finished: 'a lazy -> bool
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
+  val force_list: 'a lazy list -> 'a list
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
   val future: Future.params -> 'a lazy -> 'a future
 end;
@@ -42,6 +43,12 @@
     Expr _ => NONE
   | Result res => Future.peek res);
 
+fun pending (Lazy var) =
+  (case Synchronized.value var of
+    Expr _ => true
+  | Result _ => false);
+
+
 
 (* status *)
 
@@ -91,7 +98,12 @@
 
 end;
 
-fun force r = Exn.release (force_result r);
+fun force x = Exn.release (force_result x);
+
+fun force_list xs =
+  (List.app (fn x => if pending x then ignore (force_result x) else ()) xs;
+   map force xs);
+
 fun map f x = lazy_name "Lazy.map" (fn () => f (force x));
 
 
diff -r 1bd268ab885c -r fcd09fc36d7f src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Jun 22 15:20:32 2017 +0200
+++ b/src/Pure/more_thm.ML	Thu Jun 22 21:10:13 2017 +0200
@@ -645,7 +645,7 @@
   Proofs.map (fold (cons o Thm.trim_context) more_thms);
 
 fun consolidate_theory thy =
-  List.app (Thm.consolidate o Thm.transfer thy) (rev (Proofs.get thy));
+  Thm.consolidate (map (Thm.transfer thy) (rev (Proofs.get thy)));
 
 
 
diff -r 1bd268ab885c -r fcd09fc36d7f src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jun 22 15:20:32 2017 +0200
+++ b/src/Pure/proofterm.ML	Thu Jun 22 21:10:13 2017 +0200
@@ -43,7 +43,7 @@
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
     proof_body list -> 'a -> 'a
-  val consolidate: proof_body -> unit
+  val consolidate: proof_body list -> unit
   val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
@@ -197,15 +197,16 @@
 fun join_thms (thms: pthm list) =
   Future.joins (map (thm_node_body o #2) thms);
 
-fun consolidate (PBody {thms, ...}) =
-  List.app (Lazy.force o thm_node_consolidate o #2) thms;
+val consolidate =
+  maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
+  #> Lazy.force_list #> ignore;
 
 fun make_thm_node name prop body =
   Thm_Node {name = name, prop = prop, body = body,
     consolidate =
       Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
         let val PBody {thms, ...} = Future.join body
-        in List.app consolidate (join_thms thms) end)};
+        in consolidate (join_thms thms) end)};
 
 
 (***** proof atoms *****)
@@ -1530,8 +1531,7 @@
 
 fun fulfill_norm_proof thy ps body0 =
   let
-    val _ = List.app (consolidate o #2) ps;
-    val _ = consolidate body0;
+    val _ = consolidate (map #2 ps @ [body0]);
     val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
     val oracles =
       unions_oracles
diff -r 1bd268ab885c -r fcd09fc36d7f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jun 22 15:20:32 2017 +0200
+++ b/src/Pure/thm.ML	Thu Jun 22 21:10:13 2017 +0200
@@ -86,7 +86,7 @@
   val proof_bodies_of: thm list -> proof_body list
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
-  val consolidate: thm -> unit
+  val consolidate: thm list -> unit
   val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val derivation_closed: thm -> bool
@@ -598,7 +598,7 @@
 val proof_body_of = singleton proof_bodies_of;
 val proof_of = Proofterm.proof_of o proof_body_of;
 
-val consolidate = ignore o proof_bodies_of o single;
+val consolidate = ignore o proof_bodies_of;
 
 
 (* derivation status *)