src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
author blanchet
Mon Feb 03 15:33:18 2014 +0100 (2014-02-03 ago)
changeset 55286 7bbbd9393ce0
parent 55285 e88ad20035f4
child 55287 ffa306239316
permissions -rw-r--r--
tuning
blanchet@55201
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover.ML
wenzelm@28477
     2
    Author:     Fabian Immler, TU Muenchen
wenzelm@32996
     3
    Author:     Makarius
blanchet@35969
     4
    Author:     Jasmin Blanchette, TU Muenchen
wenzelm@28477
     5
blanchet@41087
     6
Generic prover abstraction for Sledgehammer.
wenzelm@28477
     7
*)
wenzelm@28477
     8
blanchet@55201
     9
signature SLEDGEHAMMER_PROVER =
wenzelm@28477
    10
sig
blanchet@53586
    11
  type atp_failure = ATP_Proof.atp_failure
blanchet@46340
    12
  type stature = ATP_Problem_Generate.stature
blanchet@46320
    13
  type type_enc = ATP_Problem_Generate.type_enc
blanchet@51005
    14
  type fact = Sledgehammer_Fact.fact
blanchet@55285
    15
  type proof_method = Sledgehammer_Reconstructor.proof_method
blanchet@54824
    16
  type play_outcome = Sledgehammer_Reconstructor.play_outcome
smolkas@52555
    17
  type minimize_command = Sledgehammer_Reconstructor.minimize_command
blanchet@39493
    18
wenzelm@53052
    19
  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
blanchet@43021
    20
blanchet@35969
    21
  type params =
blanchet@48321
    22
    {debug : bool,
blanchet@48321
    23
     verbose : bool,
blanchet@48321
    24
     overlord : bool,
blanchet@53800
    25
     spy : bool,
blanchet@48321
    26
     blocking : bool,
blanchet@48321
    27
     provers : string list,
blanchet@48321
    28
     type_enc : string option,
blanchet@48321
    29
     strict : bool,
blanchet@48321
    30
     lam_trans : string option,
blanchet@48321
    31
     uncurried_aliases : bool option,
blanchet@48321
    32
     learn : bool,
blanchet@48321
    33
     fact_filter : string option,
blanchet@48321
    34
     max_facts : int option,
blanchet@48321
    35
     fact_thresholds : real * real,
blanchet@48321
    36
     max_mono_iters : int option,
blanchet@48321
    37
     max_new_mono_instances : int option,
blanchet@51190
    38
     isar_proofs : bool option,
blanchet@55183
    39
     compress_isar : real,
blanchet@55183
    40
     try0_isar : bool,
blanchet@48321
    41
     slice : bool,
blanchet@48321
    42
     minimize : bool option,
blanchet@54816
    43
     timeout : Time.time,
blanchet@54816
    44
     preplay_timeout : Time.time,
blanchet@48321
    45
     expect : string}
blanchet@39493
    46
blanchet@40061
    47
  type prover_problem =
blanchet@54141
    48
    {comment : string,
blanchet@54141
    49
     state : Proof.state,
blanchet@48321
    50
     goal : thm,
blanchet@48321
    51
     subgoal : int,
blanchet@48321
    52
     subgoal_count : int,
blanchet@51010
    53
     factss : (string * fact list) list}
blanchet@39493
    54
blanchet@40061
    55
  type prover_result =
blanchet@53586
    56
    {outcome : atp_failure option,
blanchet@51009
    57
     used_facts : (string * stature) list,
blanchet@51009
    58
     used_from : fact list,
blanchet@48321
    59
     run_time : Time.time,
blanchet@55285
    60
     preplay : (proof_method * play_outcome) Lazy.lazy,
blanchet@55285
    61
     message : proof_method * play_outcome -> string,
blanchet@48321
    62
     message_tail : string}
blanchet@39493
    63
blanchet@43051
    64
  type prover =
blanchet@45520
    65
    params -> ((string * string list) list -> string -> minimize_command)
blanchet@45520
    66
    -> prover_problem -> prover_result
blanchet@35867
    67
blanchet@48319
    68
  val SledgehammerN : string
blanchet@55205
    69
  val overlord_file_location_of_prover : string -> string * string
blanchet@55205
    70
  val proof_banner : mode -> string -> string
blanchet@55285
    71
  val extract_proof_method : params -> proof_method -> string * (string * string list) list
blanchet@55285
    72
  val is_proof_method : string -> bool
blanchet@43050
    73
  val is_atp : theory -> string -> bool
blanchet@55285
    74
  val bunch_of_proof_methods : bool -> string -> proof_method list
blanchet@48798
    75
  val is_fact_chained : (('a * stature) * 'b) -> bool
blanchet@48798
    76
  val filter_used_facts :
blanchet@48798
    77
    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
blanchet@48798
    78
    ((''a * stature) * 'b) list
blanchet@55205
    79
  val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
blanchet@55285
    80
    Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
blanchet@55205
    81
  val remotify_atp_if_not_installed : theory -> string -> string option
blanchet@55205
    82
  val isar_supported_prover_of : theory -> string -> string
blanchet@55205
    83
  val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
blanchet@55285
    84
    string -> proof_method * play_outcome -> 'a
blanchet@55205
    85
  val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
blanchet@55205
    86
    Proof.context
blanchet@55212
    87
blanchet@55212
    88
  val supported_provers : Proof.context -> unit
blanchet@55212
    89
  val kill_provers : unit -> unit
blanchet@55212
    90
  val running_provers : unit -> unit
blanchet@55212
    91
  val messages : int option -> unit
wenzelm@28477
    92
end;
wenzelm@28477
    93
blanchet@55201
    94
structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
wenzelm@28477
    95
struct
wenzelm@28477
    96
blanchet@43085
    97
open ATP_Util
blanchet@38028
    98
open ATP_Problem
blanchet@38028
    99
open ATP_Systems
blanchet@46320
   100
open ATP_Problem_Generate
blanchet@46320
   101
open ATP_Proof_Reconstruct
blanchet@45521
   102
open Metis_Tactic
blanchet@51005
   103
open Sledgehammer_Fact
smolkas@52555
   104
open Sledgehammer_Reconstructor
blanchet@54000
   105
wenzelm@53052
   106
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
blanchet@43021
   107
blanchet@45376
   108
(* Identifier that distinguishes Sledgehammer from other tools that could use
blanchet@38102
   109
   "Async_Manager". *)
blanchet@48319
   110
val SledgehammerN = "Sledgehammer"
blanchet@37585
   111
blanchet@55285
   112
val proof_method_names = [metisN, smtN]
blanchet@55285
   113
val is_proof_method = member (op =) proof_method_names
blanchet@43228
   114
blanchet@43050
   115
val is_atp = member (op =) o supported_atps
blanchet@43050
   116
blanchet@55205
   117
fun remotify_atp_if_supported_and_not_already_remote thy name =
blanchet@51200
   118
  if String.isPrefix remote_prefix name then
blanchet@51200
   119
    SOME name
blanchet@51200
   120
  else
blanchet@51200
   121
    let val remote_name = remote_prefix ^ name in
blanchet@55205
   122
      if is_atp thy remote_name then SOME remote_name else NONE
blanchet@51200
   123
    end
blanchet@51200
   124
blanchet@55205
   125
fun remotify_atp_if_not_installed thy name =
blanchet@55207
   126
  if is_atp thy name andalso is_atp_installed thy name then SOME name
blanchet@55205
   127
  else remotify_atp_if_supported_and_not_already_remote thy name
blanchet@40063
   128
blanchet@35969
   129
type params =
blanchet@48321
   130
  {debug : bool,
blanchet@48321
   131
   verbose : bool,
blanchet@48321
   132
   overlord : bool,
blanchet@53800
   133
   spy : bool,
blanchet@48321
   134
   blocking : bool,
blanchet@48321
   135
   provers : string list,
blanchet@48321
   136
   type_enc : string option,
blanchet@48321
   137
   strict : bool,
blanchet@48321
   138
   lam_trans : string option,
blanchet@48321
   139
   uncurried_aliases : bool option,
blanchet@48321
   140
   learn : bool,
blanchet@48321
   141
   fact_filter : string option,
blanchet@48321
   142
   max_facts : int option,
blanchet@48321
   143
   fact_thresholds : real * real,
blanchet@48321
   144
   max_mono_iters : int option,
blanchet@48321
   145
   max_new_mono_instances : int option,
blanchet@51190
   146
   isar_proofs : bool option,
blanchet@55183
   147
   compress_isar : real,
blanchet@55183
   148
   try0_isar : bool,
blanchet@48321
   149
   slice : bool,
blanchet@48321
   150
   minimize : bool option,
blanchet@54816
   151
   timeout : Time.time,
blanchet@54816
   152
   preplay_timeout : Time.time,
blanchet@48321
   153
   expect : string}
blanchet@35867
   154
blanchet@40061
   155
type prover_problem =
blanchet@54141
   156
  {comment : string,
blanchet@54141
   157
   state : Proof.state,
blanchet@48321
   158
   goal : thm,
blanchet@48321
   159
   subgoal : int,
blanchet@48321
   160
   subgoal_count : int,
blanchet@51010
   161
   factss : (string * fact list) list}
blanchet@35867
   162
blanchet@40061
   163
type prover_result =
blanchet@53586
   164
  {outcome : atp_failure option,
blanchet@48321
   165
   used_facts : (string * stature) list,
blanchet@51009
   166
   used_from : fact list,
blanchet@48321
   167
   run_time : Time.time,
blanchet@55285
   168
   preplay : (proof_method * play_outcome) Lazy.lazy,
blanchet@55285
   169
   message : proof_method * play_outcome -> string,
blanchet@48321
   170
   message_tail : string}
blanchet@35867
   171
blanchet@43051
   172
type prover =
blanchet@45520
   173
  params -> ((string * string list) list -> string -> minimize_command)
blanchet@45520
   174
  -> prover_problem -> prover_result
blanchet@35867
   175
blanchet@55205
   176
fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
blanchet@41313
   177
blanchet@43052
   178
fun proof_banner mode name =
blanchet@55205
   179
  (case mode of
blanchet@43033
   180
    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
blanchet@43033
   181
  | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
blanchet@55205
   182
  | _ => "Try this")
blanchet@43033
   183
blanchet@55285
   184
fun bunch_of_proof_methods needs_full_types desperate_lam_trans =
blanchet@48800
   185
  if needs_full_types then
blanchet@55285
   186
    [Metis_Method (SOME full_type_enc, NONE),
blanchet@55285
   187
     Metis_Method (SOME really_full_type_enc, NONE),
blanchet@55285
   188
     Metis_Method (SOME full_type_enc, SOME desperate_lam_trans),
blanchet@55285
   189
     Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
blanchet@55285
   190
     SMT_Method]
blanchet@48802
   191
  else
blanchet@55285
   192
    [Metis_Method (NONE, NONE),
blanchet@55285
   193
     Metis_Method (SOME full_type_enc, NONE),
blanchet@55285
   194
     Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
blanchet@55285
   195
     Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
blanchet@55285
   196
     SMT_Method]
blanchet@45561
   197
blanchet@55285
   198
fun extract_proof_method ({type_enc, lam_trans, ...} : params)
blanchet@55285
   199
      (Metis_Method (type_enc', lam_trans')) =
blanchet@45561
   200
    let
blanchet@45561
   201
      val override_params =
blanchet@55285
   202
        (if is_none type_enc' andalso is_none type_enc then []
blanchet@55285
   203
         else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
blanchet@55285
   204
        (if is_none lam_trans' andalso is_none lam_trans then []
blanchet@55285
   205
         else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
blanchet@45561
   206
    in (metisN, override_params) end
blanchet@55285
   207
  | extract_proof_method _ SMT_Method = (smtN, [])
blanchet@45561
   208
blanchet@43033
   209
(* based on "Mirabelle.can_apply" and generalized *)
blanchet@43034
   210
fun timed_apply timeout tac state i =
blanchet@43033
   211
  let
blanchet@43033
   212
    val {context = ctxt, facts, goal} = Proof.goal state
blanchet@43033
   213
    val full_tac = Method.insert_tac facts i THEN tac ctxt i
blanchet@54816
   214
  in
blanchet@54816
   215
    TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
blanchet@54816
   216
  end
blanchet@43033
   217
blanchet@55286
   218
fun timed_proof_method meth timeout ths =
blanchet@55286
   219
  timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
blanchet@43033
   220
blanchet@48798
   221
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
blanchet@48798
   222
blanchet@48798
   223
fun filter_used_facts keep_chained used =
blanchet@54773
   224
  filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
blanchet@43033
   225
blanchet@55285
   226
fun play_one_line_proof mode debug verbose timeout pairs state i preferred meths =
blanchet@43034
   227
  let
blanchet@55285
   228
    fun get_preferred meths =
blanchet@55285
   229
      if member (op =) meths preferred then preferred else List.last meths
blanchet@43034
   230
  in
blanchet@54816
   231
    if timeout = Time.zeroTime then
blanchet@55285
   232
      (get_preferred meths, Not_Played)
blanchet@45379
   233
    else
blanchet@50557
   234
      let
blanchet@54815
   235
        val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
blanchet@50557
   236
        val ths = pairs |> sort_wrt (fst o fst) |> map snd
blanchet@55285
   237
        fun play [] [] = (get_preferred meths, Play_Failed)
blanchet@54824
   238
          | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
blanchet@55285
   239
          | play timed_out (meth :: meths) =
blanchet@50557
   240
            let
blanchet@50557
   241
              val _ =
blanchet@50557
   242
                if verbose then
blanchet@55285
   243
                  Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
blanchet@54816
   244
                    "\" for " ^ string_of_time timeout ^ "...")
blanchet@50557
   245
                else
blanchet@50557
   246
                  ()
blanchet@50557
   247
              val timer = Timer.startRealTimer ()
blanchet@50557
   248
            in
blanchet@55286
   249
              (case timed_proof_method meth timeout ths state i of
blanchet@55285
   250
                SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
blanchet@55286
   251
              | _ => play timed_out meths)
blanchet@50557
   252
            end
blanchet@55285
   253
            handle TimeLimit.TimeOut => play (meth :: timed_out) meths
blanchet@54824
   254
      in
blanchet@55285
   255
        play [] meths
blanchet@54824
   256
      end
blanchet@43033
   257
  end
blanchet@43033
   258
blanchet@55205
   259
val canonical_isar_supported_prover = eN
blanchet@51013
   260
blanchet@55205
   261
fun isar_supported_prover_of thy name =
blanchet@55205
   262
  if is_atp thy name then name
blanchet@55205
   263
  else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover)
blanchet@43051
   264
blanchet@55202
   265
(* FIXME: See the analogous logic in the function "maybe_minimize" in
blanchet@55202
   266
   "sledgehammer_prover_minimize.ML". *)
blanchet@55205
   267
fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay =
blanchet@45520
   268
  let
blanchet@55205
   269
    val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
blanchet@51200
   270
    val (min_name, override_params) =
blanchet@54824
   271
      (case preplay of
blanchet@55285
   272
        (meth, Played _) =>
blanchet@55285
   273
        if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
blanchet@54824
   274
      | _ => (maybe_isar_name, []))
blanchet@51200
   275
  in minimize_command override_params min_name end
blanchet@43051
   276
blanchet@53480
   277
val max_fact_instances = 10 (* FUDGE *)
blanchet@53480
   278
blanchet@55205
   279
fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
blanchet@52034
   280
  Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
blanchet@52034
   281
  #> Config.put Monomorph.max_new_instances
blanchet@55205
   282
       (max_new_instances |> the_default best_max_new_instances)
blanchet@53480
   283
  #> Config.put Monomorph.max_thm_instances max_fact_instances
blanchet@52034
   284
blanchet@55212
   285
fun supported_provers ctxt =
blanchet@43050
   286
  let
blanchet@55212
   287
    val thy = Proof_Context.theory_of ctxt
blanchet@55212
   288
    val (remote_provers, local_provers) =
blanchet@55285
   289
      proof_method_names @
blanchet@55212
   290
      sort_strings (supported_atps thy) @
blanchet@55212
   291
      sort_strings (SMT_Solver.available_solvers_of ctxt)
blanchet@55212
   292
      |> List.partition (String.isPrefix remote_prefix)
blanchet@43050
   293
  in
blanchet@55212
   294
    Output.urgent_message ("Supported provers: " ^
blanchet@55212
   295
                           commas (local_provers @ remote_provers) ^ ".")
blanchet@43050
   296
  end
blanchet@43050
   297
blanchet@55212
   298
fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
blanchet@55212
   299
fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
blanchet@55212
   300
val messages = Async_Manager.thread_messages SledgehammerN "prover"
blanchet@55212
   301
wenzelm@28582
   302
end;