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