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