src/HOL/TPTP/mash_eval.ML
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63692 1bc4bc2c9fd1
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
blanchet@48285
     1
(*  Title:      HOL/TPTP/mash_eval.ML
blanchet@48234
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48234
     3
    Copyright   2012
blanchet@48234
     4
blanchet@48285
     5
Evaluate proof suggestions from MaSh (Machine-learning for Sledgehammer).
blanchet@48234
     6
*)
blanchet@48234
     7
blanchet@48285
     8
signature MASH_EVAL =
blanchet@48234
     9
sig
blanchet@55201
    10
  type params = Sledgehammer_Prover.params
blanchet@48251
    11
blanchet@57456
    12
  val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string option ->
blanchet@57456
    13
    string list -> string -> unit
blanchet@48234
    14
end;
blanchet@48234
    15
blanchet@48285
    16
structure MaSh_Eval : MASH_EVAL =
blanchet@48234
    17
struct
blanchet@48235
    18
blanchet@50557
    19
open Sledgehammer_Util
blanchet@48315
    20
open Sledgehammer_Fact
blanchet@50557
    21
open Sledgehammer_MePo
blanchet@48381
    22
open Sledgehammer_MaSh
blanchet@55201
    23
open Sledgehammer_Prover
blanchet@55212
    24
open Sledgehammer_Prover_ATP
blanchet@55198
    25
open Sledgehammer_Commands
blanchet@57431
    26
open MaSh_Export
blanchet@48240
    27
wenzelm@53980
    28
val prefix = Library.prefix
wenzelm@53980
    29
blanchet@57456
    30
fun evaluate_mash_suggestions ctxt params range prob_dir_name file_names report_file_name =
blanchet@48235
    31
  let
blanchet@55205
    32
    val thy = Proof_Context.theory_of ctxt
blanchet@51028
    33
    val zeros = [0, 0, 0, 0, 0, 0]
blanchet@50448
    34
    val report_path = report_file_name |> Path.explode
blanchet@50448
    35
    val _ = File.write report_path ""
blanchet@57432
    36
blanchet@50589
    37
    fun print s = File.append report_path (s ^ "\n")
blanchet@57432
    38
blanchet@55205
    39
    val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
blanchet@48318
    40
    val prover = hd provers
blanchet@57108
    41
    val max_suggs = generous_max_suggestions (the max_facts)
blanchet@57456
    42
blanchet@57456
    43
    val method_of_file_name =
blanchet@57456
    44
      perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/"
blanchet@57456
    45
blanchet@57456
    46
    val methods = "isar" :: map method_of_file_name file_names
blanchet@50964
    47
    val lines_of = Path.explode #> try File.read_lines #> these
blanchet@57456
    48
    val liness0 = map lines_of file_names
blanchet@57456
    49
    val num_lines = fold (Integer.max o length) liness0 0
blanchet@57432
    50
blanchet@50964
    51
    fun pad lines = lines @ replicate (num_lines - length lines) ""
blanchet@57432
    52
blanchet@58205
    53
    val liness' = Ctr_Sugar_Util.transpose (map pad liness0)
blanchet@57456
    54
blanchet@50557
    55
    val css = clasimpset_rule_table_of ctxt
wenzelm@58922
    56
    val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css
blanchet@61321
    57
    val name_tabs = build_name_tables nickname_of_thm facts
blanchet@57432
    58
blanchet@48289
    59
    fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
blanchet@50952
    60
    fun index_str (j, s) = s ^ "@" ^ string_of_int j
blanchet@50953
    61
    val str_of_method = enclose "  " ": "
blanchet@57432
    62
blanchet@57432
    63
    fun str_of_result method facts ({outcome, run_time, used_facts, ...} : prover_result) =
blanchet@51004
    64
      let val facts = facts |> map (fst o fst) in
blanchet@50953
    65
        str_of_method method ^
blanchet@48289
    66
        (if is_none outcome then
blanchet@52031
    67
           "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^
blanchet@48289
    68
           (used_facts |> map (with_index facts o fst)
wenzelm@59058
    69
                       |> sort (int_ord o apply2 fst)
blanchet@50952
    70
                       |> map index_str
blanchet@48289
    71
                       |> space_implode " ") ^
blanchet@48293
    72
           (if length facts < the max_facts then
blanchet@48289
    73
              " (of " ^ string_of_int (length facts) ^ ")"
blanchet@48289
    74
            else
blanchet@48289
    75
              "")
blanchet@48289
    76
         else
blanchet@48289
    77
           "Failure: " ^
blanchet@48293
    78
           (facts |> take (the max_facts) |> tag_list 1
blanchet@50952
    79
                  |> map index_str
blanchet@48289
    80
                  |> space_implode " "))
blanchet@48289
    81
      end
blanchet@57432
    82
blanchet@57456
    83
    fun solve_goal (j, lines) =
blanchet@58205
    84
      if in_range range j andalso exists (curry (op <>) "") lines then
blanchet@50559
    85
        let
blanchet@57125
    86
          val get_suggs = extract_suggestions ##> (take max_suggs #> map fst)
blanchet@57456
    87
          val (names, suggss0) = split_list (map get_suggs lines)
blanchet@58205
    88
          val name =
blanchet@58205
    89
            (case names |> filter (curry (op <>) "") |> distinct (op =) of
blanchet@58205
    90
              [name] => name
blanchet@63692
    91
            | names => error ("Input files out of sync: facts " ^ commas (map quote names)))
blanchet@50559
    92
          val th =
blanchet@61321
    93
            case find_first (fn (_, th) => nickname_of_thm th = name) facts of
blanchet@50559
    94
              SOME (_, th) => th
blanchet@63692
    95
            | NONE => error ("No fact called \"" ^ name)
blanchet@50559
    96
          val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
blanchet@52196
    97
          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
blanchet@61321
    98
          val isar_deps = these (isar_dependencies_of name_tabs th)
blanchet@57456
    99
          val suggss = isar_deps :: suggss0
blanchet@57406
   100
          val facts = facts |> filter (fn (_, th') => thm_less (th', th))
blanchet@57432
   101
blanchet@50559
   102
          (* adapted from "mirabelle_sledgehammer.ML" *)
blanchet@50953
   103
          fun set_file_name method (SOME dir) =
blanchet@50559
   104
              let
blanchet@57432
   105
                val prob_prefix = "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ method
blanchet@50559
   106
              in
blanchet@55212
   107
                Config.put atp_dest_dir dir
blanchet@55212
   108
                #> Config.put atp_problem_prefix (prob_prefix ^ "__")
blanchet@58061
   109
                #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
blanchet@50559
   110
              end
blanchet@50559
   111
            | set_file_name _ NONE = I
blanchet@57432
   112
blanchet@53139
   113
          fun prove method suggs =
blanchet@57456
   114
            if null facts then
blanchet@50953
   115
              (str_of_method method ^ "Skipped", 0)
blanchet@50952
   116
            else
blanchet@50952
   117
              let
blanchet@50952
   118
                fun nickify ((_, stature), th) =
blanchet@61321
   119
                  ((K (encode_str (nickname_of_thm th)), stature), th)
blanchet@57432
   120
blanchet@50952
   121
                val facts =
blanchet@53139
   122
                  suggs
blanchet@53139
   123
                  |> find_suggested_facts ctxt facts
blanchet@53139
   124
                  |> map (fact_of_raw_fact #> nickify)
blanchet@50952
   125
                  |> maybe_instantiate_inducts ctxt hyp_ts concl_t
blanchet@50952
   126
                  |> take (the max_facts)
blanchet@51004
   127
                  |> map fact_of_raw_fact
blanchet@50953
   128
                val ctxt = ctxt |> set_file_name method prob_dir_name
blanchet@57434
   129
                val res as {outcome, ...} = run_prover_for_mash ctxt params prover name facts goal
blanchet@50952
   130
                val ok = if is_none outcome then 1 else 0
blanchet@57432
   131
              in
blanchet@57432
   132
                (str_of_result method facts res, ok)
blanchet@57432
   133
              end
blanchet@57432
   134
blanchet@57456
   135
          val ress = map2 prove methods suggss
blanchet@50559
   136
        in
blanchet@50591
   137
          "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
blanchet@50587
   138
          |> cat_lines |> print;
blanchet@50591
   139
          map snd ress
blanchet@50559
   140
        end
blanchet@50559
   141
      else
blanchet@51028
   142
        zeros
blanchet@57432
   143
blanchet@50557
   144
    val inst_inducts = Config.get ctxt instantiate_inducts
blanchet@48245
   145
    val options =
blanchet@50767
   146
      ["prover = " ^ prover,
blanchet@50767
   147
       "max_facts = " ^ string_of_int (the max_facts),
blanchet@50767
   148
       "slice" |> not slice ? prefix "dont_",
blanchet@50767
   149
       "type_enc = " ^ the_default "smart" type_enc,
blanchet@50767
   150
       "lam_trans = " ^ the_default "smart" lam_trans,
blanchet@54816
   151
       "timeout = " ^ ATP_Util.string_of_time timeout,
blanchet@48241
   152
       "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
blanchet@50587
   153
    val _ = print " * * *";
blanchet@50587
   154
    val _ = print ("Options: " ^ commas options);
blanchet@58205
   155
    val oks = Par_List.map solve_goal (tag_list 1 liness')
blanchet@50620
   156
    val n = length oks
blanchet@57456
   157
blanchet@57456
   158
    fun total_of method ok =
blanchet@57456
   159
      str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1))
blanchet@57456
   160
        (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
blanchet@57456
   161
blanchet@57456
   162
    val oks' = if n = 0 then zeros else map Integer.sum (map_transpose I oks)
blanchet@48241
   163
  in
blanchet@57456
   164
    "Successes (of " ^ string_of_int n ^ " goals)" ::
blanchet@57456
   165
    map2 total_of methods oks'
blanchet@50437
   166
    |> cat_lines |> print
blanchet@48241
   167
  end
blanchet@48235
   168
blanchet@48234
   169
end;