src/Pure/par_tactical.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 70521 9ddd66d53130
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
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@70521
    17
  val strip_goals: thm -> cterm list option
wenzelm@70521
    18
  val retrofit_tac: {close: bool} -> thm list -> tactic
wenzelm@58009
    19
end;
wenzelm@58009
    20
wenzelm@58009
    21
structure Par_Tactical: PAR_TACTICAL =
wenzelm@58009
    22
struct
wenzelm@58009
    23
wenzelm@58009
    24
(* parallel choice of single results *)
wenzelm@58009
    25
wenzelm@58009
    26
fun PARALLEL_CHOICE tacs st =
wenzelm@58009
    27
  (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
wenzelm@58009
    28
    NONE => Seq.empty
wenzelm@58009
    29
  | SOME st' => Seq.single st');
wenzelm@58009
    30
wenzelm@58009
    31
wenzelm@58009
    32
(* parallel refinement of non-schematic goal by single results *)
wenzelm@58009
    33
wenzelm@70521
    34
fun strip_goals st =
wenzelm@67660
    35
  let
wenzelm@67660
    36
    val goals =
wenzelm@67660
    37
      Drule.strip_imp_prems (Thm.cprop_of st)
wenzelm@67660
    38
      |> map (Thm.adjust_maxidx_cterm ~1);
wenzelm@67660
    39
  in
wenzelm@70521
    40
    if not (null goals) andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals
wenzelm@70521
    41
    then SOME goals else NONE
wenzelm@67660
    42
  end;
wenzelm@58009
    43
wenzelm@70521
    44
local
wenzelm@70521
    45
wenzelm@70521
    46
exception FAILED of unit;
wenzelm@70521
    47
wenzelm@70521
    48
fun retrofit {close} st' =
wenzelm@70521
    49
  rotate_prems ~1 #>
wenzelm@70521
    50
  Thm.bicompose NONE {flatten = false, match = false, incremented = false}
wenzelm@70521
    51
      (false, Goal.conclude st' |> close ? Thm.close_derivation \<^here>, Thm.nprems_of st') 1;
wenzelm@70521
    52
wenzelm@70521
    53
in
wenzelm@70521
    54
wenzelm@70521
    55
fun retrofit_tac close = EVERY o map (retrofit close);
wenzelm@70521
    56
wenzelm@70521
    57
fun PARALLEL_GOALS tac st =
wenzelm@70521
    58
  (case strip_goals st of
wenzelm@70521
    59
    SOME goals =>
wenzelm@70521
    60
      if Future.relevant goals then
wenzelm@70521
    61
        let
wenzelm@70521
    62
          fun try_goal g =
wenzelm@70521
    63
            (case SINGLE tac (Goal.init g) of
wenzelm@70521
    64
              NONE => raise FAILED ()
wenzelm@70521
    65
            | SOME st' => st');
wenzelm@70521
    66
          val results = Par_List.map try_goal goals;
wenzelm@70521
    67
        in retrofit_tac {close = false} (rev results) st end handle FAILED () => Seq.empty
wenzelm@70521
    68
      else DETERM tac st
wenzelm@70521
    69
  | NONE => DETERM tac st);
wenzelm@70521
    70
wenzelm@58009
    71
end;
wenzelm@58009
    72
wenzelm@58009
    73
val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
wenzelm@58009
    74
wenzelm@58009
    75
end;
wenzelm@58009
    76
wenzelm@58009
    77
structure Basic_Par_Tactical: BASIC_PAR_TACTICAL = Par_Tactical;
wenzelm@58009
    78
open Basic_Par_Tactical;