src/Pure/par_tactical.ML
author wenzelm
Sat Jun 06 13:38:24 2015 +0200 (2015-06-06)
changeset 60372 b62eaac5c1af
parent 58950 d07464875dd4
child 67660 0cae317eda7b
permissions -rw-r--r--
more tight treatment of subgoals: main goal may refer to extra variables;
     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   if not (Multithreading.enabled ()) orelse Thm.nprems_of st <= 1 then DETERM tac st
    45   else
    46     let val subgoals = map (Thm.adjust_maxidx_cterm ~1) (Drule.strip_imp_prems (Thm.cprop_of st)) in
    47       if exists (fn sg => Thm.maxidx_of_cterm sg >= 0) subgoals then DETERM tac st
    48       else
    49         let
    50           fun try_tac g =
    51             (case SINGLE tac g of
    52               NONE => raise FAILED ()
    53             | SOME g' => g');
    54           val results = Par_List.map (try_tac o Goal.init) subgoals;
    55         in EVERY (map retrofit (rev results)) st end
    56         handle FAILED () => Seq.empty
    57     end;
    58 
    59 end;
    60 
    61 val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
    62 
    63 end;
    64 
    65 structure Basic_Par_Tactical: BASIC_PAR_TACTICAL = Par_Tactical;
    66 open Basic_Par_Tactical;