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