author | blanchet |
Tue, 01 Jul 2014 16:47:10 +0200 | |
changeset 57457 | b2bafc09b7e7 |
parent 57431 | 02c408aed5ee |
child 58206 | 3e22d3ed829f |
permissions | -rw-r--r-- |
48234 | 1 |
(* Title: HOL/TPTP/MaSh_Export.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* MaSh Exporter *} |
|
6 |
||
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 | 9 |
begin |
10 |
||
48891 | 11 |
ML_file "mash_export.ML" |
12 |
||
48245 | 13 |
sledgehammer_params |
50519 | 14 |
[provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native, |
50925 | 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 | 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 | 22 |
ML {* |
54717 | 23 |
Multithreading.max_threads_value () |
50519 | 24 |
*} |
25 |
||
26 |
ML {* |
|
48234 | 27 |
open MaSh_Export |
28 |
*} |
|
29 |
||
30 |
ML {* |
|
57122 | 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 | 33 |
val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} [] |
48333 | 34 |
val prover = hd provers |
57122 | 35 |
val range = (1, NONE) |
50954 | 36 |
val step = 1 |
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50954
diff
changeset
|
37 |
val max_suggestions = 1024 |
50513 | 38 |
val dir = "List" |
50349 | 39 |
val prefix = "/tmp/" ^ dir ^ "/" |
50337 | 40 |
*} |
41 |
||
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 | 48 |
|
57120 | 49 |
ML {* |
50 |
if do_it then |
|
57457 | 51 |
generate_mash_suggestions "nb" @{context} params (range, step) thys max_suggestions |
57431
02c408aed5ee
killed Python version of MaSh, now that the SML version works adequately
blanchet
parents:
57150
diff
changeset
|
52 |
(prefix ^ "mash_nb_suggestions") |
57120 | 53 |
else |
54 |
() |
|
55 |
*} |
|
56 |
||
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
57 |
ML {* |
48245 | 58 |
if do_it then |
57457 | 59 |
generate_mash_suggestions "knn" @{context} params (range, step) thys max_suggestions |
57431
02c408aed5ee
killed Python version of MaSh, now that the SML version works adequately
blanchet
parents:
57150
diff
changeset
|
60 |
(prefix ^ "mash_knn_suggestions") |
57120 | 61 |
else |
62 |
() |
|
63 |
*} |
|
64 |
||
57457 | 65 |
ML {* |
66 |
if do_it then |
|
67 |
generate_mepo_suggestions @{context} params (range, step) thys max_suggestions |
|
68 |
(prefix ^ "mepo_suggestions") |
|
69 |
else |
|
70 |
() |
|
71 |
*} |
|
72 |
||
73 |
ML {* |
|
74 |
if do_it then |
|
75 |
generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_suggestions") |
|
76 |
(prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_suggestions") |
|
77 |
else |
|
78 |
() |
|
79 |
*} |
|
80 |
||
81 |
ML {* |
|
82 |
if do_it then |
|
83 |
generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_suggestions") |
|
84 |
(prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_suggestions") |
|
85 |
else |
|
86 |
() |
|
87 |
*} |
|
57120 | 88 |
|
89 |
ML {* |
|
90 |
if do_it then |
|
57457 | 91 |
generate_prover_dependencies @{context} params range thys |
92 |
(prefix ^ "mash_nb_prover_dependencies") |
|
93 |
else |
|
94 |
() |
|
95 |
*} |
|
96 |
||
97 |
ML {* |
|
98 |
if do_it then |
|
99 |
generate_prover_dependencies @{context} params range thys |
|
100 |
(prefix ^ "mash_knn_prover_dependencies") |
|
101 |
else |
|
102 |
() |
|
103 |
*} |
|
104 |
||
105 |
ML {* |
|
106 |
if do_it then |
|
107 |
generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_prover_suggestions") |
|
108 |
(prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_prover_suggestions") |
|
109 |
else |
|
110 |
() |
|
111 |
*} |
|
112 |
||
113 |
ML {* |
|
114 |
if do_it then |
|
115 |
generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_prover_suggestions") |
|
116 |
(prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_prover_suggestions") |
|
57120 | 117 |
else |
118 |
() |
|
119 |
*} |
|
120 |
||
121 |
ML {* |
|
122 |
if do_it then |
|
57121 | 123 |
generate_accessibility @{context} thys (prefix ^ "mash_accessibility") |
48245 | 124 |
else |
125 |
() |
|
126 |
*} |
|
127 |
||
128 |
ML {* |
|
129 |
if do_it then |
|
55212 | 130 |
generate_features @{context} thys (prefix ^ "mash_features") |
48245 | 131 |
else |
132 |
() |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
133 |
*} |
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
134 |
|
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
135 |
ML {* |
48245 | 136 |
if do_it then |
57121 | 137 |
generate_isar_dependencies @{context} range thys (prefix ^ "mash_dependencies") |
48333 | 138 |
else |
139 |
() |
|
140 |
*} |
|
141 |
||
142 |
ML {* |
|
143 |
if do_it then |
|
57121 | 144 |
generate_isar_commands @{context} prover (range, step) thys max_suggestions |
57120 | 145 |
(prefix ^ "mash_commands") |
48333 | 146 |
else |
147 |
() |
|
148 |
*} |
|
149 |
||
150 |
ML {* |
|
50816 | 151 |
if do_it then |
57121 | 152 |
generate_prover_commands @{context} params (range, step) thys max_suggestions |
57120 | 153 |
(prefix ^ "mash_prover_commands") |
50411 | 154 |
else |
155 |
() |
|
156 |
*} |
|
157 |
||
48234 | 158 |
end |