src/Pure/par_tactical.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 60372 b62eaac5c1af
child 67660 0cae317eda7b
permissions -rw-r--r--
tuned;
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@60372
    43
fun PARALLEL_GOALS tac st =
wenzelm@60372
    44
  if not (Multithreading.enabled ()) orelse Thm.nprems_of st <= 1 then DETERM tac st
wenzelm@60372
    45
  else
wenzelm@60372
    46
    let val subgoals = map (Thm.adjust_maxidx_cterm ~1) (Drule.strip_imp_prems (Thm.cprop_of st)) in
wenzelm@60372
    47
      if exists (fn sg => Thm.maxidx_of_cterm sg >= 0) subgoals then DETERM tac st
wenzelm@60372
    48
      else
wenzelm@60372
    49
        let
wenzelm@60372
    50
          fun try_tac g =
wenzelm@60372
    51
            (case SINGLE tac g of
wenzelm@60372
    52
              NONE => raise FAILED ()
wenzelm@60372
    53
            | SOME g' => g');
wenzelm@60372
    54
          val results = Par_List.map (try_tac o Goal.init) subgoals;
wenzelm@60372
    55
        in EVERY (map retrofit (rev results)) st end
wenzelm@60372
    56
        handle FAILED () => Seq.empty
wenzelm@60372
    57
    end;
wenzelm@58009
    58
wenzelm@58009
    59
end;
wenzelm@58009
    60
wenzelm@58009
    61
val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
wenzelm@58009
    62
wenzelm@58009
    63
end;
wenzelm@58009
    64
wenzelm@58009
    65
structure Basic_Par_Tactical: BASIC_PAR_TACTICAL = Par_Tactical;
wenzelm@58009
    66
open Basic_Par_Tactical;