1(*  Title:      Pure/par_tactical.ML
2    Author:     Makarius
3
4Parallel tacticals.
5*)
6
7signature BASIC_PAR_TACTICAL =
8sig
9  val PARALLEL_CHOICE: tactic list -> tactic
10  val PARALLEL_GOALS: tactic -> tactic
11  val PARALLEL_ALLGOALS: (int -> tactic) -> tactic
12end;
13
14signature PAR_TACTICAL =
15sig
16  include BASIC_PAR_TACTICAL
17  val strip_goals: thm -> cterm list option
18  val retrofit_tac: {close: bool} -> thm list -> tactic
19end;
20
21structure Par_Tactical: PAR_TACTICAL =
22struct
23
24(* parallel choice of single results *)
25
26fun PARALLEL_CHOICE tacs st =
27  (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
28    NONE => Seq.empty
29  | SOME st' => Seq.single st');
30
31
32(* parallel refinement of non-schematic goal by single results *)
33
34fun strip_goals st =
35  let
36    val goals =
37      Drule.strip_imp_prems (Thm.cprop_of st)
38      |> map (Thm.adjust_maxidx_cterm ~1);
39  in
40    if not (null goals) andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals
41    then SOME goals else NONE
42  end;
43
44local
45
46exception FAILED of unit;
47
48fun retrofit {close} st' =
49  rotate_prems ~1 #>
50  Thm.bicompose NONE {flatten = false, match = false, incremented = false}
51      (false, Goal.conclude st' |> close ? Thm.close_derivation \<^here>, Thm.nprems_of st') 1;
52
53in
54
55fun retrofit_tac close = EVERY o map (retrofit close);
56
57fun PARALLEL_GOALS tac st =
58  (case strip_goals st of
59    SOME goals =>
60      if Future.relevant goals then
61        let
62          fun try_goal g =
63            (case SINGLE tac (Goal.init g) of
64              NONE => raise FAILED ()
65            | SOME st' => st');
66          val results = Par_List.map try_goal goals;
67        in retrofit_tac {close = false} (rev results) st end handle FAILED () => Seq.empty
68      else DETERM tac st
69  | NONE => DETERM tac st);
70
71end;
72
73val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
74
75end;
76
77structure Basic_Par_Tactical: BASIC_PAR_TACTICAL = Par_Tactical;
78open Basic_Par_Tactical;
79