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