src/HOL/TPTP/MaSh_Export.thy
author blanchet
Mon, 02 Jun 2014 11:59:50 +0200
changeset 57150 f591096a9c94
parent 57122 5f69b8c3af5a
child 57431 02c408aed5ee
permissions -rw-r--r--
add option to keep duplicates, for more precise evaluation of relevance filters
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/TPTP/MaSh_Export.thy
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
*)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     4
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     5
header {* MaSh Exporter *}
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     6
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     7
theory MaSh_Export
50350
136d5318b1fe tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents: 50349
diff changeset
     8
imports Main
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     9
begin
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    10
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48531
diff changeset
    11
ML_file "mash_export.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48531
diff changeset
    12
48245
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    13
sledgehammer_params
50519
2951841ec011 parallelized MaSh exporter
blanchet
parents: 50513
diff changeset
    14
  [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
50925
dfc0177384f9 tweaked defaults
blanchet
parents: 50906
diff changeset
    15
   lam_trans = lifting, timeout = 2, dont_preplay, minimize]
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    16
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57122
diff changeset
    17
declare [[sledgehammer_fact_duplicates = true]]
50925
dfc0177384f9 tweaked defaults
blanchet
parents: 50906
diff changeset
    18
declare [[sledgehammer_instantiate_inducts = false]]
50434
960a3429615c more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents: 50411
diff changeset
    19
51027
0f817f80bcca hide "ext" name, but keep "HOL.ext", to ensure consistency in naming when "ext" is used by LEO-II or Satallax implicitly
blanchet
parents: 50966
diff changeset
    20
hide_fact (open) HOL.ext
0f817f80bcca hide "ext" name, but keep "HOL.ext", to ensure consistency in naming when "ext" is used by LEO-II or Satallax implicitly
blanchet
parents: 50966
diff changeset
    21
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    22
ML {*
54717
42c209a6c225 support for polml-5.5.2;
wenzelm
parents: 54118
diff changeset
    23
Multithreading.max_threads_value ()
50519
2951841ec011 parallelized MaSh exporter
blanchet
parents: 50513
diff changeset
    24
*}
2951841ec011 parallelized MaSh exporter
blanchet
parents: 50513
diff changeset
    25
2951841ec011 parallelized MaSh exporter
blanchet
parents: 50513
diff changeset
    26
ML {*
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    27
open MaSh_Export
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    28
*}
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    29
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    30
ML {*
57122
5f69b8c3af5a more work on exporter
blanchet
parents: 57121
diff changeset
    31
val do_it = false (* switch to "true" to generate the files *)
50350
136d5318b1fe tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents: 50349
diff changeset
    32
val thys = [@{theory List}]
55208
11dd3d1da83b compile
blanchet
parents: 55198
diff changeset
    33
val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
48333
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
    34
val prover = hd provers
57122
5f69b8c3af5a more work on exporter
blanchet
parents: 57121
diff changeset
    35
val range = (1, NONE)
50954
7bc58677860e added step to skip some queries
blanchet
parents: 50925
diff changeset
    36
val step = 1
50964
2a990baa09af use precomputed MaSh/MePo data whenever available
blanchet
parents: 50954
diff changeset
    37
val max_suggestions = 1024
50513
blanchet
parents: 50484
diff changeset
    38
val dir = "List"
50349
b79803ee14f3 generalized MaSh exporter to sets of theories
blanchet
parents: 50337
diff changeset
    39
val prefix = "/tmp/" ^ dir ^ "/"
50337
68555697f37e tweaked MaSh exporter
blanchet
parents: 48891
diff changeset
    40
*}
68555697f37e tweaked MaSh exporter
blanchet
parents: 48891
diff changeset
    41
68555697f37e tweaked MaSh exporter
blanchet
parents: 48891
diff changeset
    42
ML {*
50350
136d5318b1fe tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents: 50349
diff changeset
    43
if do_it then
136d5318b1fe tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents: 50349
diff changeset
    44
  Isabelle_System.mkdir (Path.explode prefix)
136d5318b1fe tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents: 50349
diff changeset
    45
else
136d5318b1fe tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents: 50349
diff changeset
    46
  ()
48246
fb11c09d7729 add Isabelle dependencies to tweak relevance filter
blanchet
parents: 48245
diff changeset
    47
*}
48531
7da5d3b8aef4 don't export technical theorems for MaSh
blanchet
parents: 48529
diff changeset
    48
57121
426ab5fabcae got rid of 'linearize' option
blanchet
parents: 57120
diff changeset
    49
ML {* Options.put_default @{system_option MaSh} "sml_nb" *}
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    50
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    51
ML {*
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    52
if do_it then
57121
426ab5fabcae got rid of 'linearize' option
blanchet
parents: 57120
diff changeset
    53
  generate_mash_suggestions @{context} params (range, step) thys max_suggestions
57122
5f69b8c3af5a more work on exporter
blanchet
parents: 57121
diff changeset
    54
    (prefix ^ "mash_sml_nb_suggestions")
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    55
else
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    56
  ()
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    57
*}
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    58
57121
426ab5fabcae got rid of 'linearize' option
blanchet
parents: 57120
diff changeset
    59
ML {* Options.put_default @{system_option MaSh} "sml_knn" *}
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    60
48246
fb11c09d7729 add Isabelle dependencies to tweak relevance filter
blanchet
parents: 48245
diff changeset
    61
ML {*
48245
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    62
if do_it then
57122
5f69b8c3af5a more work on exporter
blanchet
parents: 57121
diff changeset
    63
  generate_mash_suggestions @{context} params (range, step) thys max_suggestions
5f69b8c3af5a more work on exporter
blanchet
parents: 57121
diff changeset
    64
    (prefix ^ "mash_sml_knn_suggestions")
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    65
else
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    66
  ()
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    67
*}
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    68
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    69
ML {* Options.put_default @{system_option MaSh} "py" *}
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    70
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    71
ML {*
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    72
if do_it then
57122
5f69b8c3af5a more work on exporter
blanchet
parents: 57121
diff changeset
    73
  generate_mash_suggestions @{context} params (range, step) thys max_suggestions
5f69b8c3af5a more work on exporter
blanchet
parents: 57121
diff changeset
    74
    (prefix ^ "mash_py_suggestions")
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    75
else
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    76
  ()
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    77
*}
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    78
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    79
ML {*
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
    80
if do_it then
57121
426ab5fabcae got rid of 'linearize' option
blanchet
parents: 57120
diff changeset
    81
  generate_accessibility @{context} thys (prefix ^ "mash_accessibility")
48245
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    82
else
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    83
  ()
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    84
*}
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    85
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    86
ML {*
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    87
if do_it then
55212
blanchet
parents: 55208
diff changeset
    88
  generate_features @{context} thys (prefix ^ "mash_features")
48245
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    89
else
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    90
  ()
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    91
*}
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    92
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    93
ML {*
48245
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
    94
if do_it then
57121
426ab5fabcae got rid of 'linearize' option
blanchet
parents: 57120
diff changeset
    95
  generate_isar_dependencies @{context} range thys (prefix ^ "mash_dependencies")
48333
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
    96
else
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
    97
  ()
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
    98
*}
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
    99
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
   100
ML {*
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
   101
if do_it then
57121
426ab5fabcae got rid of 'linearize' option
blanchet
parents: 57120
diff changeset
   102
  generate_isar_commands @{context} prover (range, step) thys max_suggestions
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
   103
    (prefix ^ "mash_commands")
48333
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
   104
else
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
   105
  ()
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
   106
*}
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
   107
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
   108
ML {*
50816
2c366a03c888 removed debugging code
blanchet
parents: 50814
diff changeset
   109
if do_it then
57121
426ab5fabcae got rid of 'linearize' option
blanchet
parents: 57120
diff changeset
   110
  generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
   111
    (prefix ^ "mepo_suggestions")
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50559
diff changeset
   112
else
4247cbd78aaf export MeSh data as well
blanchet
parents: 50559
diff changeset
   113
  ()
4247cbd78aaf export MeSh data as well
blanchet
parents: 50559
diff changeset
   114
*}
4247cbd78aaf export MeSh data as well
blanchet
parents: 50559
diff changeset
   115
4247cbd78aaf export MeSh data as well
blanchet
parents: 50559
diff changeset
   116
ML {*
48333
2250197977dc repair MaSh exporter
blanchet
parents: 48304
diff changeset
   117
if do_it then
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50559
diff changeset
   118
  generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
   119
    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
48245
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
   120
else
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
   121
  ()
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
   122
*}
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
   123
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
   124
ML {*
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
   125
if do_it then
57121
426ab5fabcae got rid of 'linearize' option
blanchet
parents: 57120
diff changeset
   126
  generate_prover_dependencies @{context} params range thys (prefix ^ "mash_prover_dependencies")
48245
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
   127
else
854a47677335 generate ATP dependencies
blanchet
parents: 48239
diff changeset
   128
  ()
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   129
*}
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   130
50411
c9023d78d1a6 export ATP and Isar commands separately
blanchet
parents: 50350
diff changeset
   131
ML {*
c9023d78d1a6 export ATP and Isar commands separately
blanchet
parents: 50350
diff changeset
   132
if do_it then
57121
426ab5fabcae got rid of 'linearize' option
blanchet
parents: 57120
diff changeset
   133
  generate_prover_commands @{context} params (range, step) thys max_suggestions
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
   134
    (prefix ^ "mash_prover_commands")
50411
c9023d78d1a6 export ATP and Isar commands separately
blanchet
parents: 50350
diff changeset
   135
else
c9023d78d1a6 export ATP and Isar commands separately
blanchet
parents: 50350
diff changeset
   136
  ()
c9023d78d1a6 export ATP and Isar commands separately
blanchet
parents: 50350
diff changeset
   137
*}
c9023d78d1a6 export ATP and Isar commands separately
blanchet
parents: 50350
diff changeset
   138
50966
b85cb3049df9 MeSh prover generation
blanchet
parents: 50964
diff changeset
   139
ML {*
b85cb3049df9 MeSh prover generation
blanchet
parents: 50964
diff changeset
   140
if do_it then
b85cb3049df9 MeSh prover generation
blanchet
parents: 50964
diff changeset
   141
  generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 55212
diff changeset
   142
    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
50966
b85cb3049df9 MeSh prover generation
blanchet
parents: 50964
diff changeset
   143
else
b85cb3049df9 MeSh prover generation
blanchet
parents: 50964
diff changeset
   144
  ()
b85cb3049df9 MeSh prover generation
blanchet
parents: 50964
diff changeset
   145
*}
b85cb3049df9 MeSh prover generation
blanchet
parents: 50964
diff changeset
   146
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   147
end