src/Tools/auto_tools.ML
author blanchet
Fri Dec 03 09:55:45 2010 +0100 (2010-12-03)
changeset 40931 061b8257ab9f
parent 39330 46c06182b1e3
permissions -rw-r--r--
run synchronous Auto Tools in parallel
blanchet@39324
     1
(*  Title:      Tools/auto_tools.ML
blanchet@33561
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@33561
     3
blanchet@39324
     4
Manager for tools that should be run automatically on newly entered conjectures.
blanchet@33561
     5
*)
blanchet@33561
     6
blanchet@39324
     7
signature AUTO_TOOLS =
blanchet@33561
     8
sig
blanchet@40931
     9
  val time_limit: real Unsynchronized.ref
blanchet@33561
    10
blanchet@33561
    11
  val register_tool :
blanchet@40931
    12
    bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
blanchet@40931
    13
    -> theory
blanchet@33561
    14
end;
blanchet@33561
    15
blanchet@39324
    16
structure Auto_Tools : AUTO_TOOLS =
blanchet@33561
    17
struct
blanchet@33561
    18
blanchet@33561
    19
(* preferences *)
blanchet@33561
    20
blanchet@40931
    21
val time_limit = Unsynchronized.ref 4.0
blanchet@33561
    22
blanchet@40931
    23
val auto_tools_time_limitN = "auto-tools-time-limit"
blanchet@33561
    24
val _ =
blanchet@33561
    25
  ProofGeneralPgip.add_preference Preferences.category_tracing
blanchet@40931
    26
    (Preferences.real_pref time_limit
blanchet@40931
    27
      auto_tools_time_limitN "Time limit for automatic tools (in seconds).")
blanchet@33561
    28
blanchet@33561
    29
blanchet@33561
    30
(* configuration *)
blanchet@33561
    31
wenzelm@33600
    32
structure Data = Theory_Data
wenzelm@33600
    33
(
blanchet@40931
    34
  type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
blanchet@33561
    35
  val empty = []
blanchet@33561
    36
  val extend = I
wenzelm@33600
    37
  fun merge data : T = AList.merge (op =) (K true) data
blanchet@33561
    38
)
blanchet@33561
    39
blanchet@33561
    40
val register_tool = Data.map o AList.update (op =)
blanchet@33561
    41
blanchet@33561
    42
blanchet@33561
    43
(* automatic testing *)
blanchet@33561
    44
blanchet@40931
    45
fun run_tools tools state =
blanchet@40931
    46
  tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
blanchet@40931
    47
        |> Par_List.get_some (fn tool =>
blanchet@40931
    48
                                 case try tool state of
blanchet@40931
    49
                                   SOME (true, state) => SOME state
blanchet@40931
    50
                                 | _ => NONE)
blanchet@40931
    51
        |> the_default state
blanchet@40931
    52
blanchet@40931
    53
(* Too large values are understood as milliseconds, ensuring compatibility with
blanchet@40931
    54
   old setting files. No users can possibly in their right mind want the user
blanchet@40931
    55
   interface to block for more than 100 seconds. *)
blanchet@40931
    56
fun smart_seconds r =
blanchet@40931
    57
  seconds (if r >= 100.0 then
blanchet@40931
    58
             (legacy_feature (quote auto_tools_time_limitN ^
blanchet@40931
    59
                " expressed in milliseconds -- use seconds instead"); 0.001 * r)
blanchet@40931
    60
           else
blanchet@40931
    61
             r)
blanchet@40931
    62
blanchet@33561
    63
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
blanchet@40931
    64
  if interact andalso not (!Toplevel.quiet) andalso !time_limit > 0.0 then
blanchet@40931
    65
    TimeLimit.timeLimit (smart_seconds (!time_limit))
blanchet@40931
    66
        (run_tools (Data.get (Proof.theory_of state))) state
blanchet@40931
    67
    handle TimeLimit.TimeOut => state
blanchet@40931
    68
  else
blanchet@40931
    69
    state))
blanchet@33561
    70
blanchet@33561
    71
end;