src/Tools/try.ML
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 62519 a564458f94db
child 63690 48a2c88091d7
permissions -rw-r--r--
clarified mode of ROOT.ML files;
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 =
58892
20aa19ecf2cc eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents: 58848
diff changeset
    10
    string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    11
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    12
  val tryN : string
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    13
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    14
  val serial_commas : string -> string list -> string list
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    15
  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
    16
  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
    17
  val try_tools : Proof.state -> (string * string) option
52641
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
    18
  val tool_setup : tool -> unit
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 =
58892
20aa19ecf2cc eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents: 58848
diff changeset
    25
  string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    26
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    27
val tryN = "try"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    28
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    29
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    30
(* helpers *)
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    31
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    32
fun serial_commas _ [] = ["??"]
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    33
  | serial_commas _ [s] = [s]
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    34
  | serial_commas conj [s1, s2] = [s1, conj, s2]
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    35
  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    36
  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    37
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59184
diff changeset
    38
val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    39
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    40
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    41
(* configuration *)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    42
43061
8096eec997a9 make SML/NJ happy
blanchet
parents: 43028
diff changeset
    43
fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
8096eec997a9 make SML/NJ happy
blanchet
parents: 43028
diff changeset
    44
  prod_ord int_ord string_ord ((weight1, name1), (weight2, name2))
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    45
33600
16a263d2b1c9 adapted Theory_Data;
wenzelm
parents: 33561
diff changeset
    46
structure Data = Theory_Data
16a263d2b1c9 adapted Theory_Data;
wenzelm
parents: 33561
diff changeset
    47
(
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    48
  type T = tool list
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    49
  val empty = []
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    50
  val extend = I
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    51
  fun merge data : T = Ord_List.merge tool_ord data
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    52
)
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    53
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    54
val get_tools = Data.get
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    55
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    56
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
    57
52641
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
    58
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    59
(* try command *)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    60
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    61
fun try_tools state =
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    62
  if subgoal_count state = 0 then
58843
521cea5fa777 discontinued obsolete Output.urgent_message;
wenzelm
parents: 58842
diff changeset
    63
    (writeln "No subgoal!"; NONE)
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    64
  else
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    65
    get_tools (Proof.theory_of state)
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    66
    |> tap (fn tools =>
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    67
               "Trying " ^ space_implode " "
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    68
                    (serial_commas "and" (map (quote o fst) tools)) ^ "..."
58843
521cea5fa777 discontinued obsolete Output.urgent_message;
wenzelm
parents: 58842
diff changeset
    69
               |> writeln)
43028
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    70
    |> Par_List.get_some
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    71
           (fn (name, (_, _, tool)) =>
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    72
               case try (tool false) state of
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    73
                 SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
1c451bbb3ad7 repaired theory merging and defined/used helpers
blanchet
parents: 43024
diff changeset
    74
               | _ => NONE)
58843
521cea5fa777 discontinued obsolete Output.urgent_message;
wenzelm
parents: 58842
diff changeset
    75
    |> tap (fn NONE => writeln "Tried in vain." | _ => ())
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    76
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    77
val _ =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59582
diff changeset
    78
  Outer_Syntax.command @{command_keyword try}
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 43061
diff changeset
    79
    "try a combination of automatic proving and disproving tools"
60190
906de96ba68a allow diagnostic proof commands with skip_proofs;
wenzelm
parents: 60094
diff changeset
    80
    (Scan.succeed (Toplevel.keep_proof (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
    81
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    82
52641
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
    83
(* automatic try (TTY) *)
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
    84
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    85
fun auto_try state =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    86
  get_tools (Proof.theory_of state)
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents: 52017
diff changeset
    87
  |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool 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
    88
  |> 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
    89
                           case try (tool true) state of
58892
20aa19ecf2cc eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents: 58848
diff changeset
    90
                             SOME (true, (_, outcome)) => SOME outcome
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    91
                           | _ => NONE)
58892
20aa19ecf2cc eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents: 58848
diff changeset
    92
  |> the_default []
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 39330
diff changeset
    93
52641
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
    94
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
    95
(* asynchronous print function (PIDE) *)
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
    96
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
    97
fun print_function ((name, (weight, auto, tool)): tool) =
53839
274a892b1230 avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);
wenzelm
parents: 53171
diff changeset
    98
  Command.print_function ("auto_" ^ name)
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58893
diff changeset
    99
    (fn {keywords, command_name, ...} =>
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58893
diff changeset
   100
      if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   101
        SOME
56467
8d7d6f17c6a7 more uniform ML/document antiquotations;
wenzelm
parents: 53839
diff changeset
   102
         {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   103
          pri = ~ weight,
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   104
          persistent = true,
52953
2c927b7501c5 explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents: 52850
diff changeset
   105
          strict = true,
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   106
          print_fn = fn _ => fn st =>
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   107
            let
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   108
              val state = Toplevel.proof_of st
52652
ebdbd5c79a13 avoid spurious warnings, notably of 'try0' about already declared simps etc.;
wenzelm
parents: 52651
diff changeset
   109
                |> Proof.map_context (Context_Position.set_visible false)
56467
8d7d6f17c6a7 more uniform ML/document antiquotations;
wenzelm
parents: 53839
diff changeset
   110
              val auto_time_limit = Options.default_real @{system_option auto_time_limit}
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   111
            in
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   112
              if auto_time_limit > 0.0 then
62519
a564458f94db tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
   113
                (case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of
59184
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 58923
diff changeset
   114
                  (true, (_, outcome)) => List.app Output.information outcome
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   115
                | _ => ())
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52648
diff changeset
   116
              else ()
62505
9e2a65912111 clarified modules;
wenzelm
parents: 60190
diff changeset
   117
            end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()}
52648
wenzelm
parents: 52647
diff changeset
   118
      else NONE)
52641
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
   119
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
   120
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
   121
(* hybrid tool setup *)
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
   122
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 52953
diff changeset
   123
fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool)
52641
c56b6fa636e8 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents: 52639
diff changeset
   124
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff changeset
   125
end;