author | wenzelm |
Wed, 22 Aug 2012 22:55:41 +0200 | |
changeset 48891 | c0eafbd55de3 |
parent 48531 | 7da5d3b8aef4 |
child 50337 | 68555697f37e |
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 |
|
48333 | 8 |
imports Complex_Main |
48234 | 9 |
begin |
10 |
||
48891 | 11 |
ML_file "mash_export.ML" |
12 |
||
48245 | 13 |
sledgehammer_params |
14 |
[provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
|
48432
60759d07df24
took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
blanchet
parents:
48379
diff
changeset
|
15 |
lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize] |
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
16 |
|
48234 | 17 |
ML {* |
18 |
open MaSh_Export |
|
19 |
*} |
|
20 |
||
21 |
ML {* |
|
48333 | 22 |
val do_it = false (* switch to "true" to generate the files *) |
23 |
val thy = @{theory List} |
|
24 |
val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
|
25 |
val prover = hd provers |
|
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
26 |
*} |
48531 | 27 |
|
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
28 |
ML {* |
48245 | 29 |
if do_it then |
48531 | 30 |
generate_accessibility @{context} thy false "/tmp/mash_accessibility" |
48245 | 31 |
else |
32 |
() |
|
33 |
*} |
|
34 |
||
35 |
ML {* |
|
36 |
if do_it then |
|
48333 | 37 |
generate_features @{context} prover thy false "/tmp/mash_features" |
48245 | 38 |
else |
39 |
() |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
40 |
*} |
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
41 |
|
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
42 |
ML {* |
48245 | 43 |
if do_it then |
48531 | 44 |
generate_isar_dependencies @{context} thy false "/tmp/mash_dependencies" |
48333 | 45 |
else |
46 |
() |
|
47 |
*} |
|
48 |
||
49 |
ML {* |
|
50 |
if do_it then |
|
48529
716ec3458b1d
generate fact name in queries again + use ATP dependencies when possible
blanchet
parents:
48432
diff
changeset
|
51 |
generate_commands @{context} params thy "/tmp/mash_commands" |
48333 | 52 |
else |
53 |
() |
|
54 |
*} |
|
55 |
||
56 |
ML {* |
|
57 |
if do_it then |
|
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48333
diff
changeset
|
58 |
generate_mepo_suggestions @{context} params thy 500 "/tmp/mash_mepo_suggestions" |
48245 | 59 |
else |
60 |
() |
|
61 |
*} |
|
62 |
||
63 |
ML {* |
|
64 |
if do_it then |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
65 |
generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies" |
48245 | 66 |
else |
67 |
() |
|
48234 | 68 |
*} |
69 |
||
70 |
end |