src/Tools/try.ML
author wenzelm
Tue Sep 24 13:23:25 2013 +0200 (2013-09-24)
changeset 53839 274a892b1230
parent 53171 a5e54d4d9081
child 56467 8d7d6f17c6a7
permissions -rw-r--r--
avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);
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 =
wenzelm@52639
    10
    string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
blanchet@43020
    11
blanchet@43020
    12
  val tryN : string
blanchet@33561
    13
blanchet@43028
    14
  val serial_commas : string -> string list -> string list
blanchet@43028
    15
  val subgoal_count : Proof.state -> int
blanchet@43020
    16
  val get_tools : theory -> tool list
blanchet@43020
    17
  val try_tools : Proof.state -> (string * string) option
wenzelm@52641
    18
  val tool_setup : tool -> unit
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 =
wenzelm@52639
    25
  string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
blanchet@43020
    26
blanchet@43020
    27
val tryN = "try"
blanchet@43020
    28
blanchet@43020
    29
blanchet@33561
    30
(* preferences *)
blanchet@33561
    31
blanchet@33561
    32
val _ =
wenzelm@52639
    33
  ProofGeneral.preference_option ProofGeneral.category_tracing
wenzelm@52645
    34
    (SOME "4.0")
wenzelm@52639
    35
    @{option auto_time_limit}
wenzelm@52007
    36
    "auto-try-time-limit"
wenzelm@52007
    37
    "Time limit for automatically tried tools (in seconds)"
blanchet@33561
    38
blanchet@33561
    39
blanchet@43028
    40
(* helpers *)
blanchet@43028
    41
blanchet@43028
    42
fun serial_commas _ [] = ["??"]
blanchet@43028
    43
  | serial_commas _ [s] = [s]
blanchet@43028
    44
  | serial_commas conj [s1, s2] = [s1, conj, s2]
blanchet@43028
    45
  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
blanchet@43028
    46
  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
blanchet@43028
    47
blanchet@43028
    48
val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
blanchet@43028
    49
blanchet@43028
    50
blanchet@33561
    51
(* configuration *)
blanchet@33561
    52
blanchet@43061
    53
fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
blanchet@43061
    54
  prod_ord int_ord string_ord ((weight1, name1), (weight2, name2))
blanchet@43028
    55
wenzelm@33600
    56
structure Data = Theory_Data
wenzelm@33600
    57
(
blanchet@43020
    58
  type T = tool list
blanchet@33561
    59
  val empty = []
blanchet@33561
    60
  val extend = I
blanchet@43028
    61
  fun merge data : T = Ord_List.merge tool_ord data
blanchet@33561
    62
)
blanchet@33561
    63
blanchet@43020
    64
val get_tools = Data.get
blanchet@43020
    65
blanchet@43028
    66
val register_tool = Data.map o Ord_List.insert tool_ord
blanchet@33561
    67
wenzelm@52641
    68
blanchet@43020
    69
(* try command *)
blanchet@43020
    70
blanchet@43020
    71
fun try_tools state =
blanchet@43028
    72
  if subgoal_count state = 0 then
blanchet@43028
    73
    (Output.urgent_message "No subgoal!"; NONE)
blanchet@43028
    74
  else
blanchet@43028
    75
    get_tools (Proof.theory_of state)
blanchet@43028
    76
    |> tap (fn tools =>
blanchet@43028
    77
               "Trying " ^ space_implode " "
blanchet@43028
    78
                    (serial_commas "and" (map (quote o fst) tools)) ^ "..."
blanchet@43028
    79
               |> Output.urgent_message)
blanchet@43028
    80
    |> Par_List.get_some
blanchet@43028
    81
           (fn (name, (_, _, tool)) =>
blanchet@43028
    82
               case try (tool false) state of
blanchet@43028
    83
                 SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
blanchet@43028
    84
               | _ => NONE)
blanchet@43028
    85
    |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
blanchet@43020
    86
blanchet@43020
    87
val _ =
wenzelm@46961
    88
  Outer_Syntax.improper_command @{command_spec "try"}
wenzelm@46961
    89
    "try a combination of automatic proving and disproving tools"
wenzelm@51557
    90
    (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
blanchet@43020
    91
blanchet@33561
    92
wenzelm@52641
    93
(* automatic try (TTY) *)
blanchet@33561
    94
blanchet@43020
    95
fun auto_try state =
blanchet@43020
    96
  get_tools (Proof.theory_of state)
wenzelm@52639
    97
  |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
blanchet@43020
    98
  |> Par_List.get_some (fn tool =>
blanchet@43020
    99
                           case try (tool true) state of
blanchet@43020
   100
                             SOME (true, (_, state)) => SOME state
blanchet@43020
   101
                           | _ => NONE)
blanchet@43020
   102
  |> the_default state
blanchet@40931
   103
blanchet@33561
   104
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
wenzelm@52639
   105
  let
wenzelm@52639
   106
    val auto_time_limit = Options.default_real @{option auto_time_limit}
wenzelm@52639
   107
  in
wenzelm@52639
   108
    if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
wenzelm@52639
   109
      TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
wenzelm@52639
   110
      handle TimeLimit.TimeOut => state
wenzelm@52639
   111
    else
wenzelm@52639
   112
      state
wenzelm@52639
   113
  end))
blanchet@33561
   114
wenzelm@52641
   115
wenzelm@52641
   116
(* asynchronous print function (PIDE) *)
wenzelm@52641
   117
wenzelm@52641
   118
fun print_function ((name, (weight, auto, tool)): tool) =
wenzelm@53839
   119
  Command.print_function ("auto_" ^ name)
wenzelm@52850
   120
    (fn {command_name, ...} =>
wenzelm@52641
   121
      if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
wenzelm@52651
   122
        SOME
wenzelm@52762
   123
         {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
wenzelm@52651
   124
          pri = ~ weight,
wenzelm@52651
   125
          persistent = true,
wenzelm@52953
   126
          strict = true,
wenzelm@52651
   127
          print_fn = fn _ => fn st =>
wenzelm@52651
   128
            let
wenzelm@52651
   129
              val state = Toplevel.proof_of st
wenzelm@52652
   130
                |> Proof.map_context (Context_Position.set_visible false)
wenzelm@52651
   131
              val auto_time_limit = Options.default_real @{option auto_time_limit}
wenzelm@52651
   132
            in
wenzelm@52651
   133
              if auto_time_limit > 0.0 then
wenzelm@52651
   134
                (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
wenzelm@52651
   135
                  (true, (_, state')) =>
wenzelm@52651
   136
                    List.app Pretty.writeln (Proof.pretty_goal_messages state')
wenzelm@52651
   137
                | _ => ())
wenzelm@52651
   138
              else ()
wenzelm@52651
   139
            end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
wenzelm@52648
   140
      else NONE)
wenzelm@52641
   141
wenzelm@52641
   142
wenzelm@52641
   143
(* hybrid tool setup *)
wenzelm@52641
   144
wenzelm@53171
   145
fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool)
wenzelm@52641
   146
blanchet@33561
   147
end;