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