src/Tools/try.ML
author blanchet
Fri May 27 10:30:08 2011 +0200 (2011-05-27)
changeset 43018 121aa59b4d17
parent 40931 src/Tools/auto_tools.ML@061b8257ab9f
child 43020 abb5d1f907e4
permissions -rw-r--r--
renamed "Auto_Tools" "Try"
blanchet@43018
     1
(*  Title:      Tools/try.ML
blanchet@33561
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@33561
     3
blanchet@43018
     4
Manager for tools that should be tried on conjectures.
blanchet@33561
     5
*)
blanchet@33561
     6
blanchet@43018
     7
signature TRY =
blanchet@33561
     8
sig
blanchet@43018
     9
  val auto_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@43018
    16
structure Try : TRY =
blanchet@33561
    17
struct
blanchet@33561
    18
blanchet@33561
    19
(* preferences *)
blanchet@33561
    20
blanchet@43018
    21
val auto_time_limit = Unsynchronized.ref 4.0
blanchet@33561
    22
blanchet@43018
    23
val auto_try_time_limitN = "auto-try-time-limit"
blanchet@33561
    24
val _ =
blanchet@33561
    25
  ProofGeneralPgip.add_preference Preferences.category_tracing
blanchet@43018
    26
    (Preferences.real_pref auto_time_limit
blanchet@43018
    27
      auto_try_time_limitN "Time limit for automatically tried 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@43018
    58
             (legacy_feature (quote auto_try_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@43018
    64
  if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
blanchet@43018
    65
    TimeLimit.timeLimit (smart_seconds (!auto_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;