src/Pure/par_tactical.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/par_tactical.ML	Tue Aug 19 18:11:04 2014 +0200
@@ -0,0 +1,68 @@
+(*  Title:      Pure/par_tactical.ML
+    Author:     Makarius
+
+Parallel tacticals.
+*)
+
+signature BASIC_PAR_TACTICAL =
+sig
+  val PARALLEL_CHOICE: tactic list -> tactic
+  val PARALLEL_GOALS: tactic -> tactic
+  val PARALLEL_ALLGOALS: (int -> tactic) -> tactic
+end;
+
+signature PAR_TACTICAL =
+sig
+  include BASIC_PAR_TACTICAL
+end;
+
+structure Par_Tactical: PAR_TACTICAL =
+struct
+
+(* parallel choice of single results *)
+
+fun PARALLEL_CHOICE tacs st =
+  (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
+    NONE => Seq.empty
+  | SOME st' => Seq.single st');
+
+
+(* parallel refinement of non-schematic goal by single results *)
+
+local
+
+exception FAILED of unit;
+
+fun retrofit st' =
+  rotate_prems ~1 #>
+  Thm.bicompose {flatten = false, match = false, incremented = false}
+      (false, Goal.conclude st', Thm.nprems_of st') 1;
+
+in
+
+fun PARALLEL_GOALS tac =
+  Thm.adjust_maxidx_thm ~1 #>
+  (fn st =>
+    if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
+    then DETERM tac st
+    else
+      let
+        fun try_tac g =
+          (case SINGLE tac g of
+            NONE => raise FAILED ()
+          | SOME g' => g');
+
+        val goals = Drule.strip_imp_prems (Thm.cprop_of st);
+        val results = Par_List.map (try_tac o Goal.init) goals;
+      in EVERY (map retrofit (rev results)) st end
+      handle FAILED () => Seq.empty);
+
+end;
+
+val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
+
+end;
+
+structure Basic_Par_Tactical: BASIC_PAR_TACTICAL = Par_Tactical;
+open Basic_Par_Tactical;
+