--- a/src/Pure/ROOT Tue Aug 19 17:00:44 2014 +0200
+++ b/src/Pure/ROOT Tue Aug 19 18:11:04 2014 +0200
@@ -233,6 +233,7 @@
"morphism.ML"
"name.ML"
"net.ML"
+ "par_tactical.ML"
"pattern.ML"
"primitive_defs.ML"
"proofterm.ML"
--- a/src/Pure/ROOT.ML Tue Aug 19 17:00:44 2014 +0200
+++ b/src/Pure/ROOT.ML Tue Aug 19 18:11:04 2014 +0200
@@ -255,6 +255,7 @@
(** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
(*basic proof engine*)
+use "par_tactical.ML";
use "Isar/proof_display.ML";
use "Isar/attrib.ML";
use "Isar/context_rules.ML";
--- a/src/Pure/goal.ML Tue Aug 19 17:00:44 2014 +0200
+++ b/src/Pure/goal.ML Tue Aug 19 18:11:04 2014 +0200
@@ -11,9 +11,6 @@
val PREFER_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
- val PARALLEL_CHOICE: tactic list -> tactic
- val PARALLEL_GOALS: tactic -> tactic
- val PARALLEL_ALLGOALS: (int -> tactic) -> tactic
end;
signature GOAL =
@@ -341,52 +338,6 @@
etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
in fold_rev (curry op APPEND') tacs (K no_tac) i end);
-
-
-(** parallel tacticals **)
-
-(* 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, 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 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_Goal: BASIC_GOAL = Goal;
--- /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;
+