src/Tools/try.ML
author blanchet
Tue, 02 Apr 2013 10:58:51 +0200
changeset 51594 89bfe7a33615
parent 51557 4e4b56b7a3a5
child 52006 9402221f77dd
permissions -rw-r--r--
got rid of legacy smartness
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 =
43024
58150aa44941 prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
blanchet
parents: 43021
diff changeset
    10
    string * (int * bool Unsynchronized.ref
43020
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
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    16
  val serial_commas : string -> string list -> string list
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    17
  val subgoal_count : Proof.state -> int
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    18
  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
    19
  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
    20
  val try_tools : Proof.state -> (string * string) option
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    21
end;
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    22
43018
121aa59b4d17 renamed "Auto_Tools" "Try"
blanchet
parents: 40931
diff changeset
    23
structure Try : TRY =
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    24
struct
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    25
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    26
type tool =
43024
58150aa44941 prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
blanchet
parents: 43021
diff changeset
    27
  string * (int * bool Unsynchronized.ref
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    28
            * (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
    29
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    30
val tryN = "try"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    31
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    32
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    33
(* preferences *)
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_time_limit = Unsynchronized.ref 4.0
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    36
43018
121aa59b4d17 renamed "Auto_Tools" "Try"
blanchet
parents: 40931
diff changeset
    37
val auto_try_time_limitN = "auto-try-time-limit"
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    38
val _ =
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    39
  ProofGeneralPgip.add_preference Preferences.category_tracing
43018
121aa59b4d17 renamed "Auto_Tools" "Try"
blanchet
parents: 40931
diff changeset
    40
    (Preferences.real_pref auto_time_limit
121aa59b4d17 renamed "Auto_Tools" "Try"
blanchet
parents: 40931
diff changeset
    41
      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
    42
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    43
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    44
(* helpers *)
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    45
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    46
fun serial_commas _ [] = ["??"]
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    47
  | serial_commas _ [s] = [s]
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    48
  | serial_commas conj [s1, s2] = [s1, conj, s2]
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    49
  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    50
  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    51
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    52
val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    53
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    54
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    55
(* configuration *)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    56
43061
8096eec997a9 make SML/NJ happy
blanchet
parents: 43028
diff changeset
    57
fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
8096eec997a9 make SML/NJ happy
blanchet
parents: 43028
diff changeset
    58
  prod_ord int_ord string_ord ((weight1, name1), (weight2, name2))
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    59
33600
16a263d2b1c9 adapted Theory_Data;
wenzelm
parents: 33561
diff changeset
    60
structure Data = Theory_Data
16a263d2b1c9 adapted Theory_Data;
wenzelm
parents: 33561
diff changeset
    61
(
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    62
  type T = tool list
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    63
  val empty = []
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    64
  val extend = I
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    65
  fun merge data : T = Ord_List.merge tool_ord data
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    66
)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    67
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    68
val get_tools = Data.get
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    69
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    70
val register_tool = Data.map o Ord_List.insert tool_ord
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    71
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    72
(* try command *)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    73
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    74
fun try_tools state =
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    75
  if subgoal_count state = 0 then
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    76
    (Output.urgent_message "No subgoal!"; NONE)
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    77
  else
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    78
    get_tools (Proof.theory_of state)
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    79
    |> tap (fn tools =>
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    80
               "Trying " ^ space_implode " "
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    81
                    (serial_commas "and" (map (quote o fst) tools)) ^ "..."
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    82
               |> Output.urgent_message)
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    83
    |> Par_List.get_some
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    84
           (fn (name, (_, _, tool)) =>
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    85
               case try (tool false) state of
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    86
                 SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    87
               | _ => NONE)
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    88
    |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    89
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    90
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 43061
diff changeset
    91
  Outer_Syntax.improper_command @{command_spec "try"}
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 43061
diff changeset
    92
    "try a combination of automatic proving and disproving tools"
51557
4e4b56b7a3a5 more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents: 46961
diff changeset
    93
    (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    94
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    95
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    96
(* automatic try *)
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    97
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    98
fun auto_try state =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    99
  get_tools (Proof.theory_of state)
43024
58150aa44941 prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
blanchet
parents: 43021
diff changeset
   100
  |> map_filter (fn (_, (_, auto, tool)) => if !auto then SOME tool else NONE)
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   101
  |> 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
   102
                           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
   103
                             SOME (true, (_, state)) => SOME state
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   104
                           | _ => NONE)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   105
  |> the_default state
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 39330
diff changeset
   106
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
   107
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
43018
121aa59b4d17 renamed "Auto_Tools" "Try"
blanchet
parents: 40931
diff changeset
   108
  if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
51594
89bfe7a33615 got rid of legacy smartness
blanchet
parents: 51557
diff changeset
   109
    TimeLimit.timeLimit (seconds (!auto_time_limit)) auto_try state
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 39330
diff changeset
   110
    handle TimeLimit.TimeOut => state
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 39330
diff changeset
   111
  else
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 39330
diff changeset
   112
    state))
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
   113
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
   114
end;