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