src/Tools/try.ML
author blanchet
Fri May 27 10:30:08 2011 +0200 (2011-05-27)
changeset 43020 abb5d1f907e4
parent 43018 121aa59b4d17
child 43021 5910dd009d0e
permissions -rw-r--r--
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
     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   type tool =
    10     string * (bool Unsynchronized.ref
    11               * (bool -> Proof.state -> bool * (string * Proof.state)))
    12 
    13   val tryN : string
    14   val auto_time_limit: real Unsynchronized.ref
    15 
    16   val register_tool : tool -> theory -> theory
    17   val get_tools : theory -> tool list
    18   val try_tools : Proof.state -> (string * string) option
    19 end;
    20 
    21 structure Try : TRY =
    22 struct
    23 
    24 type tool =
    25   string * (bool Unsynchronized.ref
    26             * (bool -> Proof.state -> bool * (string * Proof.state)))
    27 
    28 val tryN = "try"
    29 
    30 
    31 (* preferences *)
    32 
    33 val auto_time_limit = Unsynchronized.ref 4.0
    34 
    35 val auto_try_time_limitN = "auto-try-time-limit"
    36 val _ =
    37   ProofGeneralPgip.add_preference Preferences.category_tracing
    38     (Preferences.real_pref auto_time_limit
    39       auto_try_time_limitN "Time limit for automatically tried tools (in seconds).")
    40 
    41 
    42 (* configuration *)
    43 
    44 structure Data = Theory_Data
    45 (
    46   type T = tool list
    47   val empty = []
    48   val extend = I
    49   fun merge data : T = AList.merge (op =) (K true) data
    50 )
    51 
    52 val get_tools = Data.get
    53 
    54 val register_tool = Data.map o AList.update (op =)
    55 
    56 (* try command *)
    57 
    58 fun try_tools state =
    59   get_tools (Proof.theory_of state)
    60   |> Par_List.get_some
    61          (fn (name, (_, tool)) =>
    62              case try (tool false) state of
    63                SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
    64              | _ => NONE)
    65 
    66 val _ =
    67   Outer_Syntax.improper_command tryN
    68       "try a combination of automatic proving and disproving tools" Keyword.diag
    69       (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
    70 
    71 
    72 (* automatic try *)
    73 
    74 fun auto_try state =
    75   get_tools (Proof.theory_of state)
    76   |> map_filter (fn (_, (auto, tool)) => if !auto then SOME tool else NONE)
    77   |> Par_List.get_some (fn tool =>
    78                            case try (tool true) state of
    79                              SOME (true, (_, state)) => SOME state
    80                            | _ => NONE)
    81   |> the_default state
    82 
    83 (* Too large values are understood as milliseconds, ensuring compatibility with
    84    old setting files. No users can possibly in their right mind want the user
    85    interface to block for more than 100 seconds. *)
    86 fun smart_seconds r =
    87   seconds (if r >= 100.0 then
    88              (legacy_feature (quote auto_try_time_limitN ^
    89                 " expressed in milliseconds -- use seconds instead"); 0.001 * r)
    90            else
    91              r)
    92 
    93 val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
    94   if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
    95     TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) auto_try state
    96     handle TimeLimit.TimeOut => state
    97   else
    98     state))
    99 
   100 end;