src/Tools/try.ML
changeset 43018 121aa59b4d17
parent 40931 061b8257ab9f
child 43020 abb5d1f907e4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -0,0 +1,71 @@
     1.4 +(*  Title:      Tools/try.ML
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +
     1.7 +Manager for tools that should be tried on conjectures.
     1.8 +*)
     1.9 +
    1.10 +signature TRY =
    1.11 +sig
    1.12 +  val auto_time_limit: real Unsynchronized.ref
    1.13 +
    1.14 +  val register_tool :
    1.15 +    bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
    1.16 +    -> theory
    1.17 +end;
    1.18 +
    1.19 +structure Try : TRY =
    1.20 +struct
    1.21 +
    1.22 +(* preferences *)
    1.23 +
    1.24 +val auto_time_limit = Unsynchronized.ref 4.0
    1.25 +
    1.26 +val auto_try_time_limitN = "auto-try-time-limit"
    1.27 +val _ =
    1.28 +  ProofGeneralPgip.add_preference Preferences.category_tracing
    1.29 +    (Preferences.real_pref auto_time_limit
    1.30 +      auto_try_time_limitN "Time limit for automatically tried tools (in seconds).")
    1.31 +
    1.32 +
    1.33 +(* configuration *)
    1.34 +
    1.35 +structure Data = Theory_Data
    1.36 +(
    1.37 +  type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
    1.38 +  val empty = []
    1.39 +  val extend = I
    1.40 +  fun merge data : T = AList.merge (op =) (K true) data
    1.41 +)
    1.42 +
    1.43 +val register_tool = Data.map o AList.update (op =)
    1.44 +
    1.45 +
    1.46 +(* automatic testing *)
    1.47 +
    1.48 +fun run_tools tools state =
    1.49 +  tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
    1.50 +        |> Par_List.get_some (fn tool =>
    1.51 +                                 case try tool state of
    1.52 +                                   SOME (true, state) => SOME state
    1.53 +                                 | _ => NONE)
    1.54 +        |> the_default state
    1.55 +
    1.56 +(* Too large values are understood as milliseconds, ensuring compatibility with
    1.57 +   old setting files. No users can possibly in their right mind want the user
    1.58 +   interface to block for more than 100 seconds. *)
    1.59 +fun smart_seconds r =
    1.60 +  seconds (if r >= 100.0 then
    1.61 +             (legacy_feature (quote auto_try_time_limitN ^
    1.62 +                " expressed in milliseconds -- use seconds instead"); 0.001 * r)
    1.63 +           else
    1.64 +             r)
    1.65 +
    1.66 +val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
    1.67 +  if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
    1.68 +    TimeLimit.timeLimit (smart_seconds (!auto_time_limit))
    1.69 +        (run_tools (Data.get (Proof.theory_of state))) state
    1.70 +    handle TimeLimit.TimeOut => state
    1.71 +  else
    1.72 +    state))
    1.73 +
    1.74 +end;