src/Pure/par_tactical.ML
author wenzelm
Mon Feb 19 11:29:08 2018 +0100 (17 months ago)
changeset 67660 0cae317eda7b
parent 60372 b62eaac5c1af
child 68130 6fb85346cb79
permissions -rw-r--r--
misc tuning and clarification;
     1 (*  Title:      Pure/par_tactical.ML
     2     Author:     Makarius
     3 
     4 Parallel tacticals.
     5 *)
     6 
     7 signature BASIC_PAR_TACTICAL =
     8 sig
     9   val PARALLEL_CHOICE: tactic list -> tactic
    10   val PARALLEL_GOALS: tactic -> tactic
    11   val PARALLEL_ALLGOALS: (int -> tactic) -> tactic
    12 end;
    13 
    14 signature PAR_TACTICAL =
    15 sig
    16   include BASIC_PAR_TACTICAL
    17 end;
    18 
    19 structure Par_Tactical: PAR_TACTICAL =
    20 struct
    21 
    22 (* parallel choice of single results *)
    23 
    24 fun PARALLEL_CHOICE tacs st =
    25   (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
    26     NONE => Seq.empty
    27   | SOME st' => Seq.single st');
    28 
    29 
    30 (* parallel refinement of non-schematic goal by single results *)
    31 
    32 local
    33 
    34 exception FAILED of unit;
    35 
    36 fun retrofit st' =
    37   rotate_prems ~1 #>
    38   Thm.bicompose NONE {flatten = false, match = false, incremented = false}
    39       (false, Goal.conclude st', Thm.nprems_of st') 1;
    40 
    41 in
    42 
    43 fun PARALLEL_GOALS tac st =
    44   let
    45     val goals =
    46       Drule.strip_imp_prems (Thm.cprop_of st)
    47       |> map (Thm.adjust_maxidx_cterm ~1);
    48   in
    49     if Multithreading.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then
    50       let
    51         fun try_goal g =
    52           (case SINGLE tac (Goal.init g) of
    53             NONE => raise FAILED ()
    54           | SOME st' => st');
    55         val results = Par_List.map try_goal goals;
    56       in EVERY (map retrofit (rev results)) st
    57       end handle FAILED () => Seq.empty
    58     else DETERM tac st
    59   end;
    60 
    61 end;
    62 
    63 val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
    64 
    65 end;
    66 
    67 structure Basic_Par_Tactical: BASIC_PAR_TACTICAL = Par_Tactical;
    68 open Basic_Par_Tactical;