src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
author blanchet
Fri Jan 31 13:32:13 2014 +0100 (2014-01-31 ago)
changeset 55207 42ad887a1c7c
parent 55205 8450622db0c5
child 55208 11dd3d1da83b
permissions -rw-r--r--
guarded against exception
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
smolkas@52555
    15
  type reconstructor = Sledgehammer_Reconstructor.reconstructor
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@54824
    60
     preplay : (reconstructor * play_outcome) Lazy.lazy,
blanchet@54824
    61
     message : reconstructor * 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@43092
    68
  val dest_dir : string Config.T
blanchet@43092
    69
  val problem_prefix : string Config.T
blanchet@48143
    70
  val completish : bool Config.T
blanchet@44592
    71
  val atp_full_names : bool Config.T
blanchet@48319
    72
  val SledgehammerN : string
blanchet@45519
    73
  val plain_metis : reconstructor
blanchet@55205
    74
  val overlord_file_location_of_prover : string -> string * string
blanchet@55205
    75
  val proof_banner : mode -> string -> string
blanchet@54811
    76
  val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
blanchet@45379
    77
  val is_reconstructor : string -> bool
blanchet@43050
    78
  val is_atp : theory -> string -> bool
blanchet@47962
    79
  val is_ho_atp: Proof.context -> string -> bool
blanchet@42944
    80
  val is_unit_equational_atp : Proof.context -> string -> bool
blanchet@42944
    81
  val is_unit_equality : term -> bool
blanchet@51998
    82
  val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
blanchet@41727
    83
  val supported_provers : Proof.context -> unit
blanchet@40059
    84
  val kill_provers : unit -> unit
blanchet@40059
    85
  val running_provers : unit -> unit
blanchet@40059
    86
  val messages : int option -> unit
blanchet@48798
    87
  val is_fact_chained : (('a * stature) * 'b) -> bool
blanchet@55205
    88
  val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
blanchet@48798
    89
  val filter_used_facts :
blanchet@48798
    90
    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
blanchet@48798
    91
    ((''a * stature) * 'b) list
blanchet@55205
    92
  val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
blanchet@55205
    93
    Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome
blanchet@55205
    94
  val remotify_atp_if_not_installed : theory -> string -> string option
blanchet@55205
    95
  val isar_supported_prover_of : theory -> string -> string
blanchet@55205
    96
  val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
blanchet@55205
    97
    string -> reconstructor * play_outcome -> 'a
blanchet@55205
    98
  val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
blanchet@55205
    99
    Proof.context
blanchet@55205
   100
  val run_reconstructor : mode -> string -> prover
wenzelm@28477
   101
end;
wenzelm@28477
   102
blanchet@55201
   103
structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
wenzelm@28477
   104
struct
wenzelm@28477
   105
blanchet@43085
   106
open ATP_Util
blanchet@38028
   107
open ATP_Problem
blanchet@39491
   108
open ATP_Proof
blanchet@38028
   109
open ATP_Systems
blanchet@46320
   110
open ATP_Problem_Generate
blanchet@46320
   111
open ATP_Proof_Reconstruct
blanchet@45521
   112
open Metis_Tactic
blanchet@38023
   113
open Sledgehammer_Util
blanchet@51005
   114
open Sledgehammer_Fact
smolkas@52555
   115
open Sledgehammer_Reconstructor
blanchet@55202
   116
open Sledgehammer_Isar_Print
blanchet@55202
   117
open Sledgehammer_Isar
blanchet@48288
   118
blanchet@54000
   119
(* Empty string means create files in Isabelle's temporary files directory. *)
blanchet@54094
   120
val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
blanchet@54094
   121
val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
blanchet@54094
   122
val completish = Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
blanchet@54000
   123
blanchet@54000
   124
(* In addition to being easier to read, readable names are often much shorter,
blanchet@54000
   125
   especially if types are mangled in names. This makes a difference for some
blanchet@54000
   126
   provers (e.g., E). For these reason, short names are enabled by default. *)
blanchet@54094
   127
val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
blanchet@54000
   128
wenzelm@53052
   129
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
blanchet@43021
   130
blanchet@45376
   131
(* Identifier that distinguishes Sledgehammer from other tools that could use
blanchet@38102
   132
   "Async_Manager". *)
blanchet@48319
   133
val SledgehammerN = "Sledgehammer"
blanchet@37585
   134
blanchet@45520
   135
val reconstructor_names = [metisN, smtN]
blanchet@46365
   136
val plain_metis = Metis (hd partial_type_encs, combsN)
blanchet@45561
   137
val is_reconstructor = member (op =) reconstructor_names
blanchet@43228
   138
blanchet@43050
   139
val is_atp = member (op =) o supported_atps
blanchet@43050
   140
blanchet@51998
   141
fun is_atp_of_format is_format ctxt name =
blanchet@42944
   142
  let val thy = Proof_Context.theory_of ctxt in
blanchet@55205
   143
    (case try (get_atp thy) name of
blanchet@47606
   144
      SOME config =>
blanchet@55205
   145
      exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
blanchet@55205
   146
    | NONE => false)
blanchet@42944
   147
  end
blanchet@42944
   148
blanchet@51998
   149
val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ)
blanchet@51998
   150
val is_ho_atp = is_atp_of_format is_format_higher_order
blanchet@44597
   151
blanchet@55205
   152
fun remotify_atp_if_supported_and_not_already_remote thy name =
blanchet@51200
   153
  if String.isPrefix remote_prefix name then
blanchet@51200
   154
    SOME name
blanchet@51200
   155
  else
blanchet@51200
   156
    let val remote_name = remote_prefix ^ name in
blanchet@55205
   157
      if is_atp thy remote_name then SOME remote_name else NONE
blanchet@51200
   158
    end
blanchet@51200
   159
blanchet@55205
   160
fun remotify_atp_if_not_installed thy name =
blanchet@55207
   161
  if is_atp thy name andalso is_atp_installed thy name then SOME name
blanchet@55205
   162
  else remotify_atp_if_supported_and_not_already_remote thy name
blanchet@40063
   163
blanchet@42956
   164
fun is_if (@{const_name If}, _) = true
blanchet@42956
   165
  | is_if _ = false
blanchet@42956
   166
blanchet@42956
   167
(* Beware of "if and only if" (which is translated as such) and "If" (which is
blanchet@42956
   168
   translated to conditional equations). *)
blanchet@42956
   169
fun is_good_unit_equality T t u =
blanchet@42956
   170
  T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u])
blanchet@42956
   171
blanchet@42944
   172
fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t
blanchet@42944
   173
  | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) =
blanchet@42944
   174
    is_unit_equality t
blanchet@42944
   175
  | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) =
blanchet@42944
   176
    is_unit_equality t
blanchet@42956
   177
  | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) =
blanchet@42956
   178
    is_good_unit_equality T t u
blanchet@42956
   179
  | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) =
blanchet@42956
   180
    is_good_unit_equality T t u
blanchet@42944
   181
  | is_unit_equality _ = false
blanchet@42944
   182
blanchet@51998
   183
fun is_appropriate_prop_of_prover ctxt name =
blanchet@42944
   184
  if is_unit_equational_atp ctxt name then is_unit_equality else K true
blanchet@42944
   185
blanchet@41727
   186
fun supported_provers ctxt =
blanchet@40060
   187
  let
wenzelm@42361
   188
    val thy = Proof_Context.theory_of ctxt
blanchet@40060
   189
    val (remote_provers, local_provers) =
blanchet@45520
   190
      reconstructor_names @
blanchet@41727
   191
      sort_strings (supported_atps thy) @
blanchet@41727
   192
      sort_strings (SMT_Solver.available_solvers_of ctxt)
blanchet@40060
   193
      |> List.partition (String.isPrefix remote_prefix)
blanchet@40060
   194
  in
blanchet@41727
   195
    Output.urgent_message ("Supported provers: " ^
blanchet@40205
   196
                           commas (local_provers @ remote_provers) ^ ".")
blanchet@40060
   197
  end
blanchet@35969
   198
blanchet@48319
   199
fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
blanchet@48319
   200
fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
blanchet@48319
   201
val messages = Async_Manager.thread_messages SledgehammerN "prover"
blanchet@40059
   202
blanchet@35969
   203
type params =
blanchet@48321
   204
  {debug : bool,
blanchet@48321
   205
   verbose : bool,
blanchet@48321
   206
   overlord : bool,
blanchet@53800
   207
   spy : bool,
blanchet@48321
   208
   blocking : bool,
blanchet@48321
   209
   provers : string list,
blanchet@48321
   210
   type_enc : string option,
blanchet@48321
   211
   strict : bool,
blanchet@48321
   212
   lam_trans : string option,
blanchet@48321
   213
   uncurried_aliases : bool option,
blanchet@48321
   214
   learn : bool,
blanchet@48321
   215
   fact_filter : string option,
blanchet@48321
   216
   max_facts : int option,
blanchet@48321
   217
   fact_thresholds : real * real,
blanchet@48321
   218
   max_mono_iters : int option,
blanchet@48321
   219
   max_new_mono_instances : int option,
blanchet@51190
   220
   isar_proofs : bool option,
blanchet@55183
   221
   compress_isar : real,
blanchet@55183
   222
   try0_isar : bool,
blanchet@48321
   223
   slice : bool,
blanchet@48321
   224
   minimize : bool option,
blanchet@54816
   225
   timeout : Time.time,
blanchet@54816
   226
   preplay_timeout : Time.time,
blanchet@48321
   227
   expect : string}
blanchet@35867
   228
blanchet@40061
   229
type prover_problem =
blanchet@54141
   230
  {comment : string,
blanchet@54141
   231
   state : Proof.state,
blanchet@48321
   232
   goal : thm,
blanchet@48321
   233
   subgoal : int,
blanchet@48321
   234
   subgoal_count : int,
blanchet@51010
   235
   factss : (string * fact list) list}
blanchet@35867
   236
blanchet@40061
   237
type prover_result =
blanchet@53586
   238
  {outcome : atp_failure option,
blanchet@48321
   239
   used_facts : (string * stature) list,
blanchet@51009
   240
   used_from : fact list,
blanchet@48321
   241
   run_time : Time.time,
blanchet@54824
   242
   preplay : (reconstructor * play_outcome) Lazy.lazy,
blanchet@54824
   243
   message : reconstructor * play_outcome -> string,
blanchet@48321
   244
   message_tail : string}
blanchet@35867
   245
blanchet@43051
   246
type prover =
blanchet@45520
   247
  params -> ((string * string list) list -> string -> minimize_command)
blanchet@45520
   248
  -> prover_problem -> prover_result
blanchet@35867
   249
blanchet@55205
   250
fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
blanchet@41313
   251
blanchet@43052
   252
fun proof_banner mode name =
blanchet@55205
   253
  (case mode of
blanchet@43033
   254
    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
blanchet@43033
   255
  | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
blanchet@55205
   256
  | _ => "Try this")
blanchet@43033
   257
blanchet@45561
   258
fun bunch_of_reconstructors needs_full_types lam_trans =
blanchet@48800
   259
  if needs_full_types then
blanchet@48802
   260
    [Metis (full_type_enc, lam_trans false),
blanchet@48802
   261
     Metis (really_full_type_enc, lam_trans false),
blanchet@48802
   262
     Metis (full_type_enc, lam_trans true),
blanchet@48802
   263
     Metis (really_full_type_enc, lam_trans true),
blanchet@48802
   264
     SMT]
blanchet@48802
   265
  else
blanchet@48800
   266
    [Metis (partial_type_enc, lam_trans false),
blanchet@48800
   267
     Metis (full_type_enc, lam_trans false),
blanchet@48800
   268
     Metis (no_typesN, lam_trans true),
blanchet@48800
   269
     Metis (really_full_type_enc, lam_trans true),
blanchet@48800
   270
     SMT]
blanchet@45561
   271
blanchet@54824
   272
fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
blanchet@45561
   273
    let
blanchet@45561
   274
      val override_params =
blanchet@54824
   275
        (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
blanchet@54824
   276
         else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
blanchet@54824
   277
        (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
blanchet@54824
   278
         else [("lam_trans", [lam_trans'])])
blanchet@45561
   279
    in (metisN, override_params) end
blanchet@45561
   280
  | extract_reconstructor _ SMT = (smtN, [])
blanchet@45561
   281
blanchet@43033
   282
(* based on "Mirabelle.can_apply" and generalized *)
blanchet@43034
   283
fun timed_apply timeout tac state i =
blanchet@43033
   284
  let
blanchet@43033
   285
    val {context = ctxt, facts, goal} = Proof.goal state
blanchet@43033
   286
    val full_tac = Method.insert_tac facts i THEN tac ctxt i
blanchet@54816
   287
  in
blanchet@54816
   288
    TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
blanchet@54816
   289
  end
blanchet@43033
   290
blanchet@54824
   291
fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
blanchet@51998
   292
  | tac_of_reconstructor SMT = SMT_Solver.smt_tac
blanchet@43034
   293
blanchet@45520
   294
fun timed_reconstructor reconstr debug timeout ths =
blanchet@55170
   295
  timed_apply timeout (silence_reconstructors debug
blanchet@55170
   296
    #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
blanchet@43033
   297
blanchet@48798
   298
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
blanchet@48798
   299
blanchet@48798
   300
fun filter_used_facts keep_chained used =
blanchet@54773
   301
  filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
blanchet@43033
   302
blanchet@54815
   303
fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
blanchet@43034
   304
  let
blanchet@45520
   305
    fun get_preferred reconstrs =
blanchet@45520
   306
      if member (op =) reconstrs preferred then preferred
blanchet@45520
   307
      else List.last reconstrs
blanchet@43034
   308
  in
blanchet@54816
   309
    if timeout = Time.zeroTime then
blanchet@54824
   310
      (get_preferred reconstrs, Not_Played)
blanchet@45379
   311
    else
blanchet@50557
   312
      let
blanchet@54815
   313
        val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
blanchet@50557
   314
        val ths = pairs |> sort_wrt (fst o fst) |> map snd
blanchet@54824
   315
        fun play [] [] = (get_preferred reconstrs, Play_Failed)
blanchet@54824
   316
          | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
blanchet@50557
   317
          | play timed_out (reconstr :: reconstrs) =
blanchet@50557
   318
            let
blanchet@50557
   319
              val _ =
blanchet@50557
   320
                if verbose then
blanchet@54816
   321
                  Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
blanchet@54816
   322
                    "\" for " ^ string_of_time timeout ^ "...")
blanchet@50557
   323
                else
blanchet@50557
   324
                  ()
blanchet@50557
   325
              val timer = Timer.startRealTimer ()
blanchet@50557
   326
            in
blanchet@50557
   327
              case timed_reconstructor reconstr debug timeout ths state i of
blanchet@54824
   328
                SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
blanchet@50557
   329
              | _ => play timed_out reconstrs
blanchet@50557
   330
            end
blanchet@50557
   331
            handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
blanchet@54824
   332
      in
blanchet@54824
   333
        play [] reconstrs
blanchet@54824
   334
      end
blanchet@43033
   335
  end
blanchet@43033
   336
blanchet@55205
   337
val canonical_isar_supported_prover = eN
blanchet@51013
   338
blanchet@55205
   339
fun isar_supported_prover_of thy name =
blanchet@55205
   340
  if is_atp thy name then name
blanchet@55205
   341
  else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover)
blanchet@43051
   342
blanchet@55202
   343
(* FIXME: See the analogous logic in the function "maybe_minimize" in
blanchet@55202
   344
   "sledgehammer_prover_minimize.ML". *)
blanchet@55205
   345
fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay =
blanchet@45520
   346
  let
blanchet@55205
   347
    val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
blanchet@51200
   348
    val (min_name, override_params) =
blanchet@54824
   349
      (case preplay of
blanchet@54824
   350
        (reconstr, Played _) =>
blanchet@51200
   351
        if isar_proofs = SOME true then (maybe_isar_name, [])
blanchet@51200
   352
        else extract_reconstructor params reconstr
blanchet@54824
   353
      | _ => (maybe_isar_name, []))
blanchet@51200
   354
  in minimize_command override_params min_name end
blanchet@43051
   355
blanchet@53480
   356
val max_fact_instances = 10 (* FUDGE *)
blanchet@53480
   357
blanchet@55205
   358
fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
blanchet@52034
   359
  Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
blanchet@52034
   360
  #> Config.put Monomorph.max_new_instances
blanchet@55205
   361
       (max_new_instances |> the_default best_max_new_instances)
blanchet@53480
   362
  #> Config.put Monomorph.max_thm_instances max_fact_instances
blanchet@52034
   363
blanchet@55205
   364
fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
blanchet@54824
   365
    minimize_command
blanchet@55205
   366
    ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
blanchet@43050
   367
  let
blanchet@45520
   368
    val reconstr =
blanchet@45520
   369
      if name = metisN then
blanchet@45520
   370
        Metis (type_enc |> the_default (hd partial_type_encs),
blanchet@54500
   371
               lam_trans |> the_default default_metis_lam_trans)
blanchet@45520
   372
      else if name = smtN then
blanchet@45520
   373
        SMT
blanchet@45520
   374
      else
blanchet@45520
   375
        raise Fail ("unknown reconstructor: " ^ quote name)
blanchet@51005
   376
    val used_facts = facts |> map fst
blanchet@43050
   377
  in
blanchet@54828
   378
    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
blanchet@54828
   379
       state subgoal reconstr [reconstr] of
blanchet@54824
   380
      play as (_, Played time) =>
blanchet@54824
   381
      {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
blanchet@54824
   382
       preplay = Lazy.value play,
blanchet@45561
   383
       message =
blanchet@45561
   384
         fn play =>
blanchet@45561
   385
            let
blanchet@45561
   386
              val (_, override_params) = extract_reconstructor params reconstr
blanchet@45561
   387
              val one_line_params =
blanchet@54824
   388
                (play, proof_banner mode name, used_facts, minimize_command override_params name,
blanchet@54824
   389
                 subgoal, subgoal_count)
blanchet@48799
   390
              val num_chained = length (#facts (Proof.goal state))
blanchet@52754
   391
            in
wenzelm@53052
   392
              one_line_proof_text num_chained one_line_params
blanchet@52754
   393
            end,
blanchet@43261
   394
       message_tail = ""}
blanchet@43052
   395
    | play =>
blanchet@43166
   396
      let
blanchet@54824
   397
        val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
blanchet@43166
   398
      in
blanchet@51009
   399
        {outcome = SOME failure, used_facts = [], used_from = [],
blanchet@51009
   400
         run_time = Time.zeroTime, preplay = Lazy.value play,
blanchet@53586
   401
         message = fn _ => string_of_atp_failure failure, message_tail = ""}
blanchet@54824
   402
      end)
blanchet@43050
   403
  end
blanchet@43050
   404
wenzelm@28582
   405
end;