src/HOL/TPTP/mash_eval.ML
author blanchet
Sat, 15 Dec 2012 18:26:37 +0100
changeset 50555 81a1491ba936
parent 50520 f2d33310337a
child 50556 6209bc89faa3
permissions -rw-r--r--
encode lemma name in file name
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48285
902ab51dd12a renaming
blanchet
parents: 48284
diff changeset
     1
(*  Title:      HOL/TPTP/mash_eval.ML
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     3
    Copyright   2012
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     4
48285
902ab51dd12a renaming
blanchet
parents: 48284
diff changeset
     5
Evaluate proof suggestions from MaSh (Machine-learning for Sledgehammer).
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     6
*)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     7
48285
902ab51dd12a renaming
blanchet
parents: 48284
diff changeset
     8
signature MASH_EVAL =
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     9
sig
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48250
diff changeset
    10
  type params = Sledgehammer_Provers.params
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48250
diff changeset
    11
50437
9762fe72936e store evaluation output in a file
blanchet
parents: 50436
diff changeset
    12
  val evaluate_mash_suggestions :
50448
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
    13
    Proof.context -> params -> string option -> string -> string -> unit
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    14
end;
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    15
48285
902ab51dd12a renaming
blanchet
parents: 48284
diff changeset
    16
structure MaSh_Eval : MASH_EVAL =
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    17
struct
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    18
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48313
diff changeset
    19
open Sledgehammer_Fact
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48379
diff changeset
    20
open Sledgehammer_MaSh
48240
6a8d18798161 rationalized output
blanchet
parents: 48239
diff changeset
    21
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    22
val MePoN = "MePo"
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    23
val MaShN = "MaSh"
50459
52ec07a7f304 changed capitalization of MeSh filter
blanchet
parents: 50458
diff changeset
    24
val MeShN = "MeSh"
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    25
val IsarN = "Isar"
48241
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
    26
50448
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
    27
fun evaluate_mash_suggestions ctxt params prob_dir_name sugg_file_name
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
    28
                              report_file_name =
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    29
  let
50448
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
    30
    val report_path = report_file_name |> Path.explode
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
    31
    val _ = File.write report_path ""
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
    32
    fun print s = (tracing s; File.append report_path (s ^ "\n"))
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    33
    val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48236
diff changeset
    34
      Sledgehammer_Isar.default_params ctxt []
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    35
    val prover = hd provers
50412
e83ab94e3e6e use proper entry point for MaSh in test driver
blanchet
parents: 50383
diff changeset
    36
    val slack_max_facts = generous_max_facts (the max_facts)
50437
9762fe72936e store evaluation output in a file
blanchet
parents: 50436
diff changeset
    37
    val sugg_path = sugg_file_name |> Path.explode
9762fe72936e store evaluation output in a file
blanchet
parents: 50436
diff changeset
    38
    val lines = sugg_path |> File.read_lines
48530
d443166f9520 repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents: 48438
diff changeset
    39
    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
50442
4f6a4d32522c don't blacklist "case" theorems -- this causes problems in MaSh later
blanchet
parents: 50440
diff changeset
    40
    val facts = all_facts ctxt true false Symtab.empty [] [] css
50485
3c6ac2da2f45 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents: 50483
diff changeset
    41
    val all_names = build_all_names nickname_of facts
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    42
    val mepo_ok = Unsynchronized.ref 0
48241
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
    43
    val mash_ok = Unsynchronized.ref 0
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48293
diff changeset
    44
    val mesh_ok = Unsynchronized.ref 0
48300
9910021c80a7 tweak output
blanchet
parents: 48299
diff changeset
    45
    val isar_ok = Unsynchronized.ref 0
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    46
    fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    47
    fun index_string (j, s) = s ^ "@" ^ string_of_int j
50436
5291606b21e2 use parallel map
blanchet
parents: 50412
diff changeset
    48
    fun str_of_res label facts ({outcome, run_time, used_facts, ...}
5291606b21e2 use parallel map
blanchet
parents: 50412
diff changeset
    49
                                : Sledgehammer_Provers.prover_result) =
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    50
      let val facts = facts |> map (fn ((name, _), _) => name ()) in
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    51
        "  " ^ label ^ ": " ^
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    52
        (if is_none outcome then
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    53
           "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    54
           (used_facts |> map (with_index facts o fst)
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    55
                       |> sort (int_ord o pairself fst)
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    56
                       |> map index_string
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    57
                       |> space_implode " ") ^
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    58
           (if length facts < the max_facts then
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    59
              " (of " ^ string_of_int (length facts) ^ ")"
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    60
            else
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    61
              "")
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    62
         else
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    63
           "Failure: " ^
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    64
           (facts |> take (the max_facts) |> tag_list 1
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    65
                  |> map index_string
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    66
                  |> space_implode " "))
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48285
diff changeset
    67
      end
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48307
diff changeset
    68
    fun solve_goal (j, line) =
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    69
      let
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48307
diff changeset
    70
        val (name, suggs) = extract_query line
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    71
        val th =
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48333
diff changeset
    72
          case find_first (fn (_, th) => nickname_of th = name) facts of
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    73
            SOME (_, th) => th
48530
d443166f9520 repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents: 48438
diff changeset
    74
          | NONE => error ("No fact called \"" ^ name ^ "\".")
50358
b7d3319409b7 rationalized MaSh evaluation harness
blanchet
parents: 48615
diff changeset
    75
        val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
48245
854a47677335 generate ATP dependencies
blanchet
parents: 48241
diff changeset
    76
        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48394
diff changeset
    77
        val isar_deps = isar_dependencies_of all_names th |> these
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    78
        val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    79
        val mepo_facts =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
    80
          Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48379
diff changeset
    81
              slack_max_facts NONE hyp_ts concl_t facts
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
    82
          |> Sledgehammer_MePo.weight_mepo_facts
50440
ca99c269ca3a don't have MaSh pretend it knows facts it doesn't know
blanchet
parents: 50439
diff changeset
    83
        val (mash_facts, mash_unks) =
50412
e83ab94e3e6e use proper entry point for MaSh in test driver
blanchet
parents: 50383
diff changeset
    84
          find_mash_suggestions slack_max_facts suggs facts [] []
50440
ca99c269ca3a don't have MaSh pretend it knows facts it doesn't know
blanchet
parents: 50439
diff changeset
    85
          |>> weight_mash_facts
ca99c269ca3a don't have MaSh pretend it knows facts it doesn't know
blanchet
parents: 50439
diff changeset
    86
        val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
    87
        val mesh_facts = mesh_facts slack_max_facts mess
50412
e83ab94e3e6e use proper entry point for MaSh in test driver
blanchet
parents: 50383
diff changeset
    88
        val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts
50448
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
    89
        (* adapted from "mirabelle_sledgehammer.ML" *)
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
    90
        fun set_file_name heading (SOME dir) =
50555
81a1491ba936 encode lemma name in file name
blanchet
parents: 50520
diff changeset
    91
            let
81a1491ba936 encode lemma name in file name
blanchet
parents: 50520
diff changeset
    92
              val prob_prefix =
81a1491ba936 encode lemma name in file name
blanchet
parents: 50520
diff changeset
    93
                "goal_" ^ string_of_int j ^ "__" ^ name ^ "__" ^ heading
81a1491ba936 encode lemma name in file name
blanchet
parents: 50520
diff changeset
    94
            in
50483
da63f2bc66b3 better name for SMT solver files
blanchet
parents: 50459
diff changeset
    95
              Config.put Sledgehammer_Provers.dest_dir dir
da63f2bc66b3 better name for SMT solver files
blanchet
parents: 50459
diff changeset
    96
              #> Config.put Sledgehammer_Provers.problem_prefix
da63f2bc66b3 better name for SMT solver files
blanchet
parents: 50459
diff changeset
    97
                            (prob_prefix ^ "__")
da63f2bc66b3 better name for SMT solver files
blanchet
parents: 50459
diff changeset
    98
              #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
da63f2bc66b3 better name for SMT solver files
blanchet
parents: 50459
diff changeset
    99
            end
50448
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
   100
          | set_file_name _ NONE = I
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   101
        fun prove ok heading get facts =
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   102
          let
50520
f2d33310337a use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents: 50485
diff changeset
   103
            fun nickify ((_, stature), th) = ((K (nickname_of th), stature), th)
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   104
            val facts =
50520
f2d33310337a use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents: 50485
diff changeset
   105
              facts
f2d33310337a use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents: 50485
diff changeset
   106
              |> map get
f2d33310337a use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents: 50485
diff changeset
   107
              |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
f2d33310337a use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents: 50485
diff changeset
   108
              |> take (the max_facts)
f2d33310337a use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents: 50485
diff changeset
   109
              |> map nickify
50448
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents: 50442
diff changeset
   110
            val ctxt = ctxt |> set_file_name heading prob_dir_name
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   111
            val res as {outcome, ...} =
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   112
              run_prover_for_mash ctxt params prover facts goal
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   113
            val _ = if is_none outcome then ok := !ok + 1 else ()
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   114
          in str_of_res heading facts res end
50436
5291606b21e2 use parallel map
blanchet
parents: 50412
diff changeset
   115
        val [mepo_s, mash_s, mesh_s, isar_s] =
5291606b21e2 use parallel map
blanchet
parents: 50412
diff changeset
   116
          [fn () => prove mepo_ok MePoN fst mepo_facts,
5291606b21e2 use parallel map
blanchet
parents: 50412
diff changeset
   117
           fn () => prove mash_ok MaShN fst mash_facts,
50459
52ec07a7f304 changed capitalization of MeSh filter
blanchet
parents: 50458
diff changeset
   118
           fn () => prove mesh_ok MeShN I mesh_facts,
50436
5291606b21e2 use parallel map
blanchet
parents: 50412
diff changeset
   119
           fn () => prove isar_ok IsarN fst isar_facts]
50458
85739c08d126 (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
blanchet
parents: 50448
diff changeset
   120
          |> (* Par_List. *) map (fn f => f ())
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
   121
      in
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   122
        ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
48300
9910021c80a7 tweak output
blanchet
parents: 48299
diff changeset
   123
         isar_s]
50437
9762fe72936e store evaluation output in a file
blanchet
parents: 50436
diff changeset
   124
        |> cat_lines |> print
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
   125
      end
48241
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   126
    fun total_of heading ok n =
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   127
      "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
48241
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   128
      Real.fmt (StringCvt.FIX (SOME 1))
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   129
               (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48245
diff changeset
   130
    val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
48245
854a47677335 generate ATP dependencies
blanchet
parents: 48241
diff changeset
   131
    val options =
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   132
      [prover, string_of_int (the max_facts) ^ " facts",
48241
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   133
       "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   134
       the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   135
       "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   136
    val n = length lines
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   137
  in
50437
9762fe72936e store evaluation output in a file
blanchet
parents: 50436
diff changeset
   138
    print " * * *";
9762fe72936e store evaluation output in a file
blanchet
parents: 50436
diff changeset
   139
    print ("Options: " ^ commas options);
50458
85739c08d126 (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
blanchet
parents: 50448
diff changeset
   140
    Par_List.map solve_goal (tag_list 1 lines);
48241
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   141
    ["Successes (of " ^ string_of_int n ^ " goals)",
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   142
     total_of MePoN mepo_ok n,
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   143
     total_of MaShN mash_ok n,
50459
52ec07a7f304 changed capitalization of MeSh filter
blanchet
parents: 50458
diff changeset
   144
     total_of MeShN mesh_ok n,
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   145
     total_of IsarN isar_ok n]
50437
9762fe72936e store evaluation output in a file
blanchet
parents: 50436
diff changeset
   146
    |> cat_lines |> print
48241
688f1172d523 nicer output
blanchet
parents: 48240
diff changeset
   147
  end
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
   148
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   149
end;