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