src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
author wenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826 eb94e570c1a4
parent 62735 23de054397e5
child 63692 1bc4bc2c9fd1
permissions -rw-r--r--
prefer infix operations;
blanchet@55205
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
blanchet@55205
     2
    Author:     Fabian Immler, TU Muenchen
blanchet@55205
     3
    Author:     Makarius
blanchet@55205
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@55205
     5
blanchet@55205
     6
ATPs as Sledgehammer provers.
blanchet@55205
     7
*)
blanchet@55205
     8
blanchet@55205
     9
signature SLEDGEHAMMER_PROVER_ATP =
blanchet@55205
    10
sig
blanchet@55205
    11
  type mode = Sledgehammer_Prover.mode
blanchet@55205
    12
  type prover = Sledgehammer_Prover.prover
blanchet@55205
    13
blanchet@55212
    14
  val atp_dest_dir : string Config.T
blanchet@55212
    15
  val atp_problem_prefix : string Config.T
blanchet@62718
    16
  val atp_completish : int Config.T
blanchet@55212
    17
  val atp_full_names : bool Config.T
blanchet@55212
    18
blanchet@55212
    19
  val is_ho_atp : Proof.context -> string -> bool
blanchet@55212
    20
blanchet@55205
    21
  val run_atp : mode -> string -> prover
blanchet@55205
    22
end;
blanchet@55205
    23
blanchet@55205
    24
structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP =
blanchet@55205
    25
struct
blanchet@55205
    26
blanchet@55205
    27
open ATP_Util
blanchet@55205
    28
open ATP_Problem
blanchet@55205
    29
open ATP_Proof
blanchet@55205
    30
open ATP_Problem_Generate
blanchet@55205
    31
open ATP_Proof_Reconstruct
blanchet@57267
    32
open ATP_Waldmeister
fleury@57707
    33
open ATP_Satallax
blanchet@55205
    34
open ATP_Systems
blanchet@55205
    35
open Sledgehammer_Util
blanchet@55287
    36
open Sledgehammer_Proof_Methods
blanchet@55205
    37
open Sledgehammer_Isar
blanchet@55205
    38
open Sledgehammer_Prover
blanchet@55205
    39
blanchet@55212
    40
(* Empty string means create files in Isabelle's temporary files directory. *)
blanchet@55212
    41
val atp_dest_dir = Attrib.setup_config_string @{binding sledgehammer_atp_dest_dir} (K "")
blanchet@55212
    42
val atp_problem_prefix =
blanchet@55212
    43
  Attrib.setup_config_string @{binding sledgehammer_atp_problem_prefix} (K "prob")
blanchet@62718
    44
val atp_completish = Attrib.setup_config_int @{binding sledgehammer_atp_completish} (K 0)
blanchet@55212
    45
(* In addition to being easier to read, readable names are often much shorter, especially if types
blanchet@55212
    46
   are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short
blanchet@55212
    47
   names are enabled by default. *)
blanchet@55212
    48
val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
blanchet@55212
    49
blanchet@55212
    50
fun is_atp_of_format is_format ctxt name =
blanchet@55212
    51
  let val thy = Proof_Context.theory_of ctxt in
blanchet@55212
    52
    (case try (get_atp thy) name of
blanchet@55212
    53
      SOME config =>
blanchet@55212
    54
      exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
blanchet@55212
    55
    | NONE => false)
blanchet@55212
    56
  end
blanchet@55212
    57
blanchet@55212
    58
val is_ho_atp = is_atp_of_format is_format_higher_order
blanchet@55212
    59
blanchet@55205
    60
fun choose_type_enc strictness best_type_enc format =
blanchet@55205
    61
  the_default best_type_enc
blanchet@55205
    62
  #> type_enc_of_string strictness
blanchet@55205
    63
  #> adjust_type_enc format
blanchet@55205
    64
blanchet@55205
    65
fun has_bound_or_var_of_type pred =
blanchet@55205
    66
  exists_subterm (fn Var (_, T as Type _) => pred T
blanchet@55205
    67
                   | Abs (_, T as Type _, _) => pred T
blanchet@55205
    68
                   | _ => false)
blanchet@55205
    69
blanchet@55205
    70
(* Unwanted equalities are those between a (bound or schematic) variable that does not properly
blanchet@55205
    71
   occur in the second operand. *)
blanchet@55205
    72
val is_exhaustive_finite =
blanchet@55205
    73
  let
blanchet@55205
    74
    fun is_bad_equal (Var z) t =
blanchet@55205
    75
        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
blanchet@55205
    76
      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
blanchet@55205
    77
      | is_bad_equal _ _ = false
blanchet@55205
    78
    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
blanchet@55205
    79
    fun do_formula pos t =
blanchet@55208
    80
      (case (pos, t) of
blanchet@55205
    81
        (_, @{const Trueprop} $ t1) => do_formula pos t1
wenzelm@56245
    82
      | (true, Const (@{const_name Pure.all}, _) $ Abs (_, _, t')) => do_formula pos t'
blanchet@55208
    83
      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => do_formula pos t'
blanchet@55208
    84
      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => do_formula pos t'
wenzelm@56245
    85
      | (_, @{const Pure.imp} $ t1 $ t2) =>
blanchet@55208
    86
        do_formula (not pos) t1 andalso (t2 = @{prop False} orelse do_formula pos t2)
blanchet@55205
    87
      | (_, @{const HOL.implies} $ t1 $ t2) =>
blanchet@55208
    88
        do_formula (not pos) t1 andalso (t2 = @{const False} orelse do_formula pos t2)
blanchet@55205
    89
      | (_, @{const Not} $ t1) => do_formula (not pos) t1
blanchet@55205
    90
      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
blanchet@55205
    91
      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
blanchet@55205
    92
      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
wenzelm@56245
    93
      | (true, Const (@{const_name Pure.eq}, _) $ t1 $ t2) => do_equals t1 t2
blanchet@55208
    94
      | _ => false)
blanchet@55205
    95
  in do_formula true end
blanchet@55205
    96
blanchet@55205
    97
(* Facts containing variables of finite types such as "unit" or "bool" or of the form
blanchet@55205
    98
   "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type
blanchet@55205
    99
   encodings. *)
blanchet@55205
   100
fun is_dangerous_prop ctxt =
blanchet@55205
   101
  transform_elim_prop
blanchet@55205
   102
  #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite)
blanchet@55205
   103
blanchet@55205
   104
fun get_slices slice slices =
blanchet@55205
   105
  (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
blanchet@55205
   106
blanchet@55205
   107
fun get_facts_of_filter _ [(_, facts)] = facts
blanchet@55205
   108
  | get_facts_of_filter fact_filter factss =
blanchet@55205
   109
    (case AList.lookup (op =) factss fact_filter of
blanchet@55205
   110
      SOME facts => facts
blanchet@55205
   111
    | NONE => snd (hd factss))
blanchet@55205
   112
blanchet@55205
   113
(* For low values of "max_facts", this fudge value ensures that most slices are invoked with a
blanchet@55205
   114
   nontrivial amount of facts. *)
blanchet@55205
   115
val max_fact_factor_fudge = 5
blanchet@55205
   116
blanchet@55205
   117
val mono_max_privileged_facts = 10
blanchet@55205
   118
blanchet@55205
   119
fun suffix_of_mode Auto_Try = "_try"
blanchet@55205
   120
  | suffix_of_mode Try = "_try"
blanchet@55205
   121
  | suffix_of_mode Normal = ""
blanchet@55205
   122
  | suffix_of_mode MaSh = ""
blanchet@55205
   123
  | suffix_of_mode Minimize = "_min"
blanchet@55205
   124
blanchet@55205
   125
(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be
blanchet@55205
   126
   the only ATP that does not honor its time limit. *)
blanchet@55205
   127
val atp_timeout_slack = seconds 1.0
blanchet@55205
   128
blanchet@57738
   129
(* Important messages are important but not so important that users want to see them each time. *)
blanchet@55205
   130
val atp_important_message_keep_quotient = 25
blanchet@55205
   131
blanchet@55205
   132
fun run_atp mode name
blanchet@57732
   133
    ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
blanchet@57732
   134
     max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
blanchet@57732
   135
     slice, minimize, timeout, preplay_timeout, ...} : params)
blanchet@62735
   136
    ({comment, state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) =
blanchet@55205
   137
  let
blanchet@55205
   138
    val thy = Proof.theory_of state
blanchet@55205
   139
    val ctxt = Proof.context_of state
blanchet@55205
   140
blanchet@55205
   141
    val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
blanchet@55205
   142
      best_max_new_mono_instances, ...} = get_atp thy name ()
blanchet@55205
   143
blanchet@57671
   144
    val full_proofs = isar_proofs |> the_default (mode = Minimize)
blanchet@57267
   145
    val local_name = perhaps (try (unprefix remote_prefix)) name
blanchet@57267
   146
    val waldmeister_new = (local_name = waldmeister_newN)
blanchet@59577
   147
    val spassy = (local_name = pirateN orelse local_name = spassN)
blanchet@57267
   148
blanchet@62718
   149
    val completish = Config.get ctxt atp_completish
blanchet@62718
   150
    val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer
blanchet@55205
   151
    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
blanchet@55205
   152
    val (dest_dir, problem_prefix) =
blanchet@55205
   153
      if overlord then overlord_file_location_of_prover name
blanchet@55212
   154
      else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix)
blanchet@55205
   155
    val problem_file_name =
blanchet@55205
   156
      Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
blanchet@58085
   157
        suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
blanchet@55205
   158
    val prob_path =
blanchet@55205
   159
      if dest_dir = "" then
blanchet@55205
   160
        File.tmp_path problem_file_name
blanchet@55205
   161
      else if File.exists (Path.explode dest_dir) then
blanchet@55205
   162
        Path.append (Path.explode dest_dir) problem_file_name
blanchet@55205
   163
      else
blanchet@55205
   164
        error ("No such directory: " ^ quote dest_dir ^ ".")
blanchet@57671
   165
    val exec = exec full_proofs
blanchet@55205
   166
    val command0 =
blanchet@55208
   167
      (case find_first (fn var => getenv var <> "") (fst exec) of
blanchet@55205
   168
        SOME var =>
blanchet@55205
   169
        let
blanchet@55205
   170
          val pref = getenv var ^ "/"
wenzelm@60978
   171
          val paths =
wenzelm@60978
   172
            map (Path.explode o prefix pref)
wenzelm@60978
   173
              (if ML_System.platform_is_windows then
wenzelm@60978
   174
                map (suffix ".exe") (snd exec) @ snd exec
wenzelm@60978
   175
               else snd exec);
blanchet@55205
   176
        in
blanchet@55208
   177
          (case find_first File.exists paths of
blanchet@55205
   178
            SOME path => path
blanchet@55208
   179
          | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ "."))
blanchet@55205
   180
        end
blanchet@55208
   181
      | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set."))
blanchet@55205
   182
blanchet@55205
   183
    fun split_time s =
blanchet@55205
   184
      let
blanchet@55205
   185
        val split = String.tokens (fn c => str c = "\n")
blanchet@55249
   186
        val (output, t) = s |> split |> (try split_last #> the_default ([], "0")) |>> cat_lines
blanchet@55249
   187
        val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
blanchet@55205
   188
        val digit = Scan.one Symbol.is_ascii_digit
blanchet@55249
   189
        val num3 = digit ::: digit ::: (digit >> single) >> (fst o read_int)
blanchet@55205
   190
        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
blanchet@55249
   191
        val as_time = raw_explode #> Scan.read Symbol.stopper time #> the_default 0
blanchet@55205
   192
      in (output, as_time t |> Time.fromMilliseconds) end
blanchet@55205
   193
blanchet@55205
   194
    fun run () =
blanchet@55205
   195
      let
blanchet@55208
   196
        (* If slicing is disabled, we expand the last slice to fill the entire time available. *)
blanchet@55205
   197
        val all_slices = best_slices ctxt
blanchet@55205
   198
        val actual_slices = get_slices slice all_slices
blanchet@55276
   199
blanchet@55276
   200
        fun max_facts_of_slices (slices : (real * (slice_spec * string)) list) =
blanchet@55276
   201
          fold (Integer.max o fst o #1 o fst o snd) slices 0
blanchet@55276
   202
blanchet@55205
   203
        val num_actual_slices = length actual_slices
blanchet@55205
   204
        val max_fact_factor =
blanchet@55248
   205
          Real.fromInt (case max_facts of NONE => max_facts_of_slices all_slices | SOME max => max)
blanchet@55248
   206
          / Real.fromInt (max_facts_of_slices (map snd actual_slices))
blanchet@55212
   207
blanchet@55205
   208
        fun monomorphize_facts facts =
blanchet@55205
   209
          let
blanchet@55205
   210
            val ctxt =
blanchet@55205
   211
              ctxt
blanchet@55205
   212
              |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances
blanchet@55205
   213
                   best_max_new_mono_instances
blanchet@55205
   214
            (* pseudo-theorem involving the same constants as the subgoal *)
blanchet@55205
   215
            val subgoal_th =
blanchet@55205
   216
              Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
blanchet@55205
   217
            val rths =
blanchet@55205
   218
              facts |> chop mono_max_privileged_facts
blanchet@55205
   219
                    |>> map (pair 1 o snd)
blanchet@55205
   220
                    ||> map (pair 2 o snd)
blanchet@55205
   221
                    |> op @
blanchet@55205
   222
                    |> cons (0, subgoal_th)
blanchet@55205
   223
          in
blanchet@55205
   224
            Monomorph.monomorph atp_schematic_consts_of ctxt rths
blanchet@55205
   225
            |> tl |> curry ListPair.zip (map fst facts)
blanchet@55208
   226
            |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths)
blanchet@55205
   227
          end
blanchet@55205
   228
blanchet@55208
   229
        fun run_slice time_left (cache_key, cache_value) (slice, (time_frac,
blanchet@55208
   230
            (key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans,
blanchet@55249
   231
               best_uncurried_aliases),
blanchet@55208
   232
             extra))) =
blanchet@55205
   233
          let
blanchet@55208
   234
            val effective_fact_filter = fact_filter |> the_default best_fact_filter
blanchet@55205
   235
            val facts = get_facts_of_filter effective_fact_filter factss
blanchet@55205
   236
            val num_facts =
blanchet@55205
   237
              Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge
blanchet@55205
   238
              |> Integer.min (length facts)
blanchet@61862
   239
            val generate_info = (case format of DFG _ => true | _ => false)
blanchet@55205
   240
            val strictness = if strict then Strict else Non_Strict
blanchet@55205
   241
            val type_enc = type_enc |> choose_type_enc strictness best_type_enc format
blanchet@55205
   242
            val sound = is_type_enc_sound type_enc
blanchet@55205
   243
            val real_ms = Real.fromInt o Time.toMilliseconds
blanchet@55205
   244
            val slice_timeout =
blanchet@55205
   245
              (real_ms time_left
blanchet@55205
   246
               |> (if slice < num_actual_slices - 1 then
blanchet@55205
   247
                     curry Real.min (time_frac * real_ms timeout)
blanchet@55205
   248
                   else
blanchet@55205
   249
                     I))
blanchet@55205
   250
              * 0.001
blanchet@55205
   251
              |> seconds
blanchet@55205
   252
            val generous_slice_timeout =
wenzelm@62826
   253
              if mode = MaSh then one_day else slice_timeout + atp_timeout_slack
blanchet@55205
   254
            val _ =
blanchet@55205
   255
              if debug then
blanchet@55205
   256
                quote name ^ " slice #" ^ string_of_int (slice + 1) ^
blanchet@55205
   257
                " with " ^ string_of_int num_facts ^ " fact" ^
blanchet@55205
   258
                plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
wenzelm@58843
   259
                |> writeln
blanchet@55205
   260
              else
blanchet@55205
   261
                ()
blanchet@55205
   262
            val readable_names = not (Config.get ctxt atp_full_names)
blanchet@55208
   263
            val lam_trans = lam_trans |> the_default best_lam_trans
blanchet@55208
   264
            val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases
steckerm@58142
   265
            val value as (atp_problem, _, _, _, _) =
blanchet@55205
   266
              if cache_key = SOME key then
blanchet@55205
   267
                cache_value
blanchet@55205
   268
              else
blanchet@55205
   269
                facts
wenzelm@59582
   270
                |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd)
blanchet@55205
   271
                |> take num_facts
blanchet@55205
   272
                |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
wenzelm@59582
   273
                |> map (apsnd Thm.prop_of)
blanchet@57267
   274
                |> (if waldmeister_new then
blanchet@57267
   275
                      generate_waldmeister_problem ctxt hyp_ts concl_t
blanchet@61329
   276
                      #> (fn (a, b, c, d, e) => (a, b, c, d, SOME e))
blanchet@57267
   277
                    else
blanchet@61862
   278
                      generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode
blanchet@61862
   279
                        lam_trans uncurried_aliases readable_names true hyp_ts concl_t
blanchet@61329
   280
                      #> (fn (a, b, c, d) => (a, b, c, d, NONE)))
blanchet@55205
   281
blanchet@55205
   282
            fun sel_weights () = atp_problem_selection_weights atp_problem
blanchet@55205
   283
            fun ord_info () = atp_problem_term_order_info atp_problem
blanchet@55205
   284
blanchet@55205
   285
            val ord = effective_term_order ctxt name
blanchet@55205
   286
            val args =
wenzelm@62549
   287
              arguments ctxt full_proofs extra slice_timeout (File.bash_path prob_path)
blanchet@55205
   288
                (ord, ord_info, sel_weights)
blanchet@55205
   289
            val command =
wenzelm@62549
   290
              "(exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args ^ " " ^ ")"
blanchet@55205
   291
              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
blanchet@57263
   292
blanchet@55205
   293
            val _ =
blanchet@55205
   294
              atp_problem
blanchet@55205
   295
              |> lines_of_atp_problem format ord ord_info
blanchet@55205
   296
              |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
blanchet@55205
   297
              |> File.write_list prob_path
blanchet@57263
   298
blanchet@55205
   299
            val ((output, run_time), (atp_proof, outcome)) =
wenzelm@62519
   300
              Timeout.apply generous_slice_timeout Isabelle_System.bash_output command
blanchet@55205
   301
              |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
blanchet@55205
   302
              |> fst |> split_time
blanchet@55205
   303
              |> (fn accum as (output, _) =>
blanchet@57776
   304
                (accum,
blanchet@57776
   305
                 extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
blanchet@57776
   306
                 |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name)
blanchet@57776
   307
                   atp_problem
blanchet@57776
   308
                 handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
wenzelm@62519
   309
              handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut))
blanchet@57263
   310
blanchet@55205
   311
            val outcome =
blanchet@55205
   312
              (case outcome of
blanchet@55205
   313
                NONE =>
blanchet@57776
   314
                (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of
blanchet@55208
   315
                  SOME facts =>
blanchet@57776
   316
                  let
blanchet@57776
   317
                    val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts)
blanchet@57776
   318
                  in
blanchet@55208
   319
                    if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
blanchet@55208
   320
                  end
blanchet@62735
   321
                | NONE => (found_proof (); NONE))
blanchet@55205
   322
              | _ => outcome)
blanchet@55205
   323
          in
fleury@57255
   324
            ((SOME key, value), (output, run_time, facts, atp_proof, outcome),
fleury@57255
   325
              SOME (format, type_enc))
blanchet@55205
   326
          end
blanchet@55205
   327
blanchet@55205
   328
        val timer = Timer.startRealTimer ()
blanchet@55205
   329
fleury@57255
   330
        fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) =
wenzelm@62826
   331
            let val time_left = timeout - Timer.checkRealTimer timer in
wenzelm@62826
   332
              if time_left <= Time.zeroTime then
blanchet@55205
   333
                result
blanchet@55205
   334
              else
blanchet@55205
   335
                run_slice time_left cache slice
fleury@57255
   336
                |> (fn (cache, (output, run_time, used_from, atp_proof, outcome),
fleury@57255
   337
                        format_type_enc) =>
wenzelm@62826
   338
                  (cache, (output, run_time0 + run_time, used_from, atp_proof, outcome),
fleury@57255
   339
                   format_type_enc))
blanchet@55205
   340
            end
blanchet@55205
   341
          | maybe_run_slice _ result = result
blanchet@55205
   342
      in
steckerm@58142
   343
        ((NONE, ([], Symtab.empty, [], Symtab.empty,NONE)),
fleury@57255
   344
         ("", Time.zeroTime, [], [], SOME InternalError), NONE)
blanchet@55205
   345
        |> fold maybe_run_slice actual_slices
blanchet@55205
   346
      end
blanchet@55205
   347
blanchet@55205
   348
    (* If the problem file has not been exported, remove it; otherwise, export
blanchet@55205
   349
       the proof file too. *)
blanchet@55208
   350
    fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else ()
fleury@57255
   351
    fun export (_, (output, _, _, _, _), _) =
blanchet@55205
   352
      if dest_dir = "" then ()
blanchet@55205
   353
      else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
blanchet@55208
   354
steckerm@58142
   355
    val ((_, (_, pool, lifted, sym_tab,wm_info)), (output, run_time, used_from, atp_proof, outcome),
blanchet@57263
   356
         SOME (format, type_enc)) =
blanchet@55205
   357
      with_cleanup clean_up run () |> tap export
blanchet@55208
   358
blanchet@55205
   359
    val important_message =
wenzelm@59172
   360
      if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0
wenzelm@59172
   361
      then extract_important_message output
wenzelm@59172
   362
      else ""
blanchet@55205
   363
blanchet@57738
   364
    val (used_facts, preferred_methss, message) =
blanchet@55205
   365
      (case outcome of
blanchet@55205
   366
        NONE =>
blanchet@55205
   367
        let
wenzelm@60924
   368
          val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
blanchet@55205
   369
          val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
blanchet@57734
   370
          val preferred_methss =
blanchet@57778
   371
            (Metis_Method (NONE, NONE),
blanchet@57778
   372
             bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types
blanchet@57778
   373
               (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN))
blanchet@55205
   374
        in
blanchet@57734
   375
          (used_facts, preferred_methss,
blanchet@55205
   376
           fn preplay =>
blanchet@55205
   377
              let
wenzelm@58843
   378
                val _ = if verbose then writeln "Generating proof text..." else ()
blanchet@57263
   379
blanchet@55205
   380
                fun isar_params () =
blanchet@55205
   381
                  let
blanchet@55205
   382
                    val metis_type_enc =
blanchet@55257
   383
                      if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE
blanchet@55257
   384
                    val metis_lam_trans =
blanchet@55257
   385
                      if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE
blanchet@55205
   386
                    val atp_proof =
blanchet@55205
   387
                      atp_proof
steckerm@58142
   388
                      |> (if waldmeister_new then termify_waldmeister_proof ctxt pool
steckerm@58142
   389
                          else termify_atp_proof ctxt name format type_enc pool lifted sym_tab)
blanchet@59577
   390
                      |> spassy ? introduce_spassy_skolems
steckerm@58246
   391
                      |> (if waldmeister_new then introduce_waldmeister_skolems (the wm_info) else I)
blanchet@57263
   392
                      |> factify_atp_proof (map fst used_from) hyp_ts concl_t
blanchet@55205
   393
                  in
blanchet@57245
   394
                    (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
blanchet@57721
   395
                     minimize, atp_proof, goal)
blanchet@55205
   396
                  end
blanchet@57263
   397
blanchet@57750
   398
                val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
blanchet@55205
   399
                val num_chained = length (#facts (Proof.goal state))
blanchet@55205
   400
              in
blanchet@57738
   401
                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
blanchet@57738
   402
                  one_line_params ^
blanchet@57738
   403
                (if important_message <> "" then
blanchet@57738
   404
                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
blanchet@57738
   405
                 else
blanchet@57738
   406
                   "")
blanchet@57738
   407
              end)
blanchet@55205
   408
        end
blanchet@55205
   409
      | SOME failure =>
blanchet@57738
   410
        ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
blanchet@55205
   411
  in
blanchet@57734
   412
    {outcome = outcome, used_facts = used_facts, used_from = used_from,
blanchet@57738
   413
     preferred_methss = preferred_methss, run_time = run_time, message = message}
blanchet@55205
   414
  end
blanchet@55205
   415
nipkow@62382
   416
end;