src/HOL/TPTP/mash_eval.ML
author blanchet
Sun Dec 16 14:19:08 2012 +0100 (2012-12-16)
changeset 50563 3a4785d64ecb
parent 50562 0a7c7e121bd8
child 50587 bd6582be1562
permissions -rw-r--r--
escape nicknames
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@48251
    10
  type params = Sledgehammer_Provers.params
blanchet@48251
    11
blanchet@50437
    12
  val evaluate_mash_suggestions :
blanchet@50559
    13
    Proof.context -> params -> int * int option -> string option -> string
blanchet@50559
    14
    -> string -> unit
blanchet@48234
    15
end;
blanchet@48234
    16
blanchet@48285
    17
structure MaSh_Eval : MASH_EVAL =
blanchet@48234
    18
struct
blanchet@48235
    19
blanchet@50557
    20
open Sledgehammer_Util
blanchet@48315
    21
open Sledgehammer_Fact
blanchet@50557
    22
open Sledgehammer_MePo
blanchet@48381
    23
open Sledgehammer_MaSh
blanchet@50557
    24
open Sledgehammer_Provers
blanchet@50557
    25
open Sledgehammer_Isar
blanchet@48240
    26
blanchet@48379
    27
val MePoN = "MePo"
blanchet@48379
    28
val MaShN = "MaSh"
blanchet@50459
    29
val MeShN = "MeSh"
blanchet@48379
    30
val IsarN = "Isar"
blanchet@48241
    31
blanchet@50559
    32
fun in_range (from, to) j =
blanchet@50559
    33
  j >= from andalso (to = NONE orelse j <= the to)
blanchet@50559
    34
blanchet@50559
    35
fun evaluate_mash_suggestions ctxt params range prob_dir_name sugg_file_name
blanchet@50448
    36
                              report_file_name =
blanchet@48235
    37
  let
blanchet@50448
    38
    val report_path = report_file_name |> Path.explode
blanchet@50448
    39
    val _ = File.write report_path ""
blanchet@50448
    40
    fun print s = (tracing s; File.append report_path (s ^ "\n"))
blanchet@48293
    41
    val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
blanchet@50557
    42
      default_params ctxt []
blanchet@48318
    43
    val prover = hd provers
blanchet@50412
    44
    val slack_max_facts = generous_max_facts (the max_facts)
blanchet@50437
    45
    val sugg_path = sugg_file_name |> Path.explode
blanchet@50437
    46
    val lines = sugg_path |> File.read_lines
blanchet@50557
    47
    val css = clasimpset_rule_table_of ctxt
blanchet@50442
    48
    val facts = all_facts ctxt true false Symtab.empty [] [] css
blanchet@50485
    49
    val all_names = build_all_names nickname_of facts
blanchet@48379
    50
    val mepo_ok = Unsynchronized.ref 0
blanchet@48241
    51
    val mash_ok = Unsynchronized.ref 0
blanchet@48298
    52
    val mesh_ok = Unsynchronized.ref 0
blanchet@48300
    53
    val isar_ok = Unsynchronized.ref 0
blanchet@48289
    54
    fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
blanchet@48235
    55
    fun index_string (j, s) = s ^ "@" ^ string_of_int j
blanchet@50436
    56
    fun str_of_res label facts ({outcome, run_time, used_facts, ...}
blanchet@50557
    57
                                : prover_result) =
blanchet@48289
    58
      let val facts = facts |> map (fn ((name, _), _) => name ()) in
blanchet@48289
    59
        "  " ^ label ^ ": " ^
blanchet@48289
    60
        (if is_none outcome then
blanchet@48289
    61
           "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
blanchet@48289
    62
           (used_facts |> map (with_index facts o fst)
blanchet@48289
    63
                       |> sort (int_ord o pairself fst)
blanchet@48289
    64
                       |> map index_string
blanchet@48289
    65
                       |> space_implode " ") ^
blanchet@48293
    66
           (if length facts < the max_facts then
blanchet@48289
    67
              " (of " ^ string_of_int (length facts) ^ ")"
blanchet@48289
    68
            else
blanchet@48289
    69
              "")
blanchet@48289
    70
         else
blanchet@48289
    71
           "Failure: " ^
blanchet@48293
    72
           (facts |> take (the max_facts) |> tag_list 1
blanchet@48289
    73
                  |> map index_string
blanchet@48289
    74
                  |> space_implode " "))
blanchet@48289
    75
      end
blanchet@48311
    76
    fun solve_goal (j, line) =
blanchet@50559
    77
      if in_range range j then
blanchet@50559
    78
        let
blanchet@50559
    79
          val (name, suggs) = extract_query line
blanchet@50559
    80
          val th =
blanchet@50559
    81
            case find_first (fn (_, th) => nickname_of th = name) facts of
blanchet@50559
    82
              SOME (_, th) => th
blanchet@50559
    83
            | NONE => error ("No fact called \"" ^ name ^ "\".")
blanchet@50559
    84
          val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
blanchet@50559
    85
          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
blanchet@50559
    86
          val isar_deps = isar_dependencies_of all_names th |> these
blanchet@50559
    87
          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
blanchet@50559
    88
          val mepo_facts =
blanchet@50559
    89
            mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
blanchet@50559
    90
                concl_t facts
blanchet@50559
    91
            |> weight_mepo_facts
blanchet@50559
    92
          val (mash_facts, mash_unks) =
blanchet@50559
    93
            find_mash_suggestions slack_max_facts suggs facts [] []
blanchet@50559
    94
            |>> weight_mash_facts
blanchet@50559
    95
          val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
blanchet@50559
    96
          val mesh_facts = mesh_facts slack_max_facts mess
blanchet@50559
    97
          val isar_facts =
blanchet@50559
    98
            find_suggested_facts (map (rpair 1.0) isar_deps) facts
blanchet@50559
    99
          (* adapted from "mirabelle_sledgehammer.ML" *)
blanchet@50559
   100
          fun set_file_name heading (SOME dir) =
blanchet@50559
   101
              let
blanchet@50559
   102
                val prob_prefix =
blanchet@50559
   103
                  "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^
blanchet@50559
   104
                  heading
blanchet@50559
   105
              in
blanchet@50559
   106
                Config.put dest_dir dir
blanchet@50559
   107
                #> Config.put problem_prefix (prob_prefix ^ "__")
blanchet@50559
   108
                #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
blanchet@50559
   109
              end
blanchet@50559
   110
            | set_file_name _ NONE = I
blanchet@50559
   111
          fun prove ok heading get facts =
blanchet@50555
   112
            let
blanchet@50559
   113
              fun nickify ((_, stature), th) =
blanchet@50563
   114
                ((K (escape_meta (nickname_of th)), stature), th)
blanchet@50559
   115
              val facts =
blanchet@50559
   116
                facts
blanchet@50562
   117
                |> map (get #> nickify)
blanchet@50559
   118
                |> maybe_instantiate_inducts ctxt hyp_ts concl_t
blanchet@50559
   119
                |> take (the max_facts)
blanchet@50559
   120
              val ctxt = ctxt |> set_file_name heading prob_dir_name
blanchet@50559
   121
              val res as {outcome, ...} =
blanchet@50559
   122
                run_prover_for_mash ctxt params prover facts goal
blanchet@50559
   123
              val _ = if is_none outcome then ok := !ok + 1 else ()
blanchet@50559
   124
            in str_of_res heading facts res end
blanchet@50559
   125
          val [mepo_s, mash_s, mesh_s, isar_s] =
blanchet@50559
   126
            [fn () => prove mepo_ok MePoN fst mepo_facts,
blanchet@50559
   127
             fn () => prove mash_ok MaShN fst mash_facts,
blanchet@50559
   128
             fn () => prove mesh_ok MeShN I mesh_facts,
blanchet@50559
   129
             fn () => prove isar_ok IsarN fst isar_facts]
blanchet@50559
   130
            |> (* Par_List. *) map (fn f => f ())
blanchet@50559
   131
        in
blanchet@50559
   132
          ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
blanchet@50559
   133
           isar_s]
blanchet@50559
   134
          |> cat_lines |> print
blanchet@50559
   135
        end
blanchet@50559
   136
      else
blanchet@50559
   137
        ()
blanchet@48241
   138
    fun total_of heading ok n =
blanchet@48379
   139
      "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
blanchet@48241
   140
      Real.fmt (StringCvt.FIX (SOME 1))
blanchet@48241
   141
               (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
blanchet@50557
   142
    val inst_inducts = Config.get ctxt instantiate_inducts
blanchet@48245
   143
    val options =
blanchet@48318
   144
      [prover, string_of_int (the max_facts) ^ " facts",
blanchet@48241
   145
       "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
blanchet@50557
   146
       the_default "smart" lam_trans,
blanchet@50557
   147
       ATP_Util.string_from_time (timeout |> the_default one_year),
blanchet@48241
   148
       "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
blanchet@48241
   149
    val n = length lines
blanchet@48241
   150
  in
blanchet@50437
   151
    print " * * *";
blanchet@50437
   152
    print ("Options: " ^ commas options);
blanchet@50458
   153
    Par_List.map solve_goal (tag_list 1 lines);
blanchet@48241
   154
    ["Successes (of " ^ string_of_int n ^ " goals)",
blanchet@48379
   155
     total_of MePoN mepo_ok n,
blanchet@48379
   156
     total_of MaShN mash_ok n,
blanchet@50459
   157
     total_of MeShN mesh_ok n,
blanchet@48379
   158
     total_of IsarN isar_ok n]
blanchet@50437
   159
    |> cat_lines |> print
blanchet@48241
   160
  end
blanchet@48235
   161
blanchet@48234
   162
end;