author | blanchet |
Wed, 11 Jul 2012 21:43:19 +0200 | |
changeset 49260 | 854a47677335 |
parent 49254 | 0016290f904c |
child 49261 | fb11c09d7729 |
permissions | -rw-r--r-- |
blanchet@49249 | 1 |
(* Title: HOL/TPTP/MaSh_Export.thy |
blanchet@49249 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
blanchet@49249 | 3 |
*) |
blanchet@49249 | 4 |
|
blanchet@49249 | 5 |
header {* MaSh Exporter *} |
blanchet@49249 | 6 |
|
blanchet@49249 | 7 |
theory MaSh_Export |
blanchet@49249 | 8 |
imports ATP_Theory_Export |
blanchet@49249 | 9 |
uses "mash_export.ML" |
blanchet@49249 | 10 |
begin |
blanchet@49249 | 11 |
|
blanchet@49260 | 12 |
sledgehammer_params |
blanchet@49260 | 13 |
[provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
blanchet@49260 | 14 |
lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
blanchet@49254 | 15 |
|
blanchet@49249 | 16 |
ML {* |
blanchet@49249 | 17 |
open MaSh_Export |
blanchet@49249 | 18 |
*} |
blanchet@49249 | 19 |
|
blanchet@49249 | 20 |
ML {* |
blanchet@49260 | 21 |
if do_it then |
blanchet@49260 | 22 |
generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies" |
blanchet@49260 | 23 |
else |
blanchet@49260 | 24 |
() |
blanchet@49249 | 25 |
*} |
blanchet@49249 | 26 |
|
blanchet@49249 | 27 |
ML {* |
blanchet@49260 | 28 |
val do_it = true (* switch to "true" to generate the files *); |
blanchet@49260 | 29 |
val thy = @{theory Nat} |
blanchet@49254 | 30 |
*} |
blanchet@49254 | 31 |
|
blanchet@49254 | 32 |
ML {* |
blanchet@49260 | 33 |
if do_it then |
blanchet@49260 | 34 |
generate_features thy false "/tmp/mash_features" |
blanchet@49260 | 35 |
else |
blanchet@49260 | 36 |
() |
blanchet@49249 | 37 |
*} |
blanchet@49249 | 38 |
|
blanchet@49249 | 39 |
ML {* |
blanchet@49260 | 40 |
if do_it then |
blanchet@49260 | 41 |
generate_accessibility thy false "/tmp/mash_accessibility" |
blanchet@49260 | 42 |
else |
blanchet@49260 | 43 |
() |
blanchet@49249 | 44 |
*} |
blanchet@49249 | 45 |
|
blanchet@49249 | 46 |
ML {* |
blanchet@49260 | 47 |
if do_it then |
blanchet@49260 | 48 |
generate_isa_dependencies thy false "/tmp/mash_isa_dependencies" |
blanchet@49260 | 49 |
else |
blanchet@49260 | 50 |
() |
blanchet@49249 | 51 |
*} |
blanchet@49249 | 52 |
|
blanchet@49249 | 53 |
ML {* |
blanchet@49260 | 54 |
if do_it then |
blanchet@49260 | 55 |
generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies" |
blanchet@49260 | 56 |
else |
blanchet@49260 | 57 |
() |
blanchet@49260 | 58 |
*} |
blanchet@49260 | 59 |
|
blanchet@49260 | 60 |
ML {* |
blanchet@49260 | 61 |
if do_it then |
blanchet@49260 | 62 |
generate_commands thy "/tmp/mash_commands" |
blanchet@49260 | 63 |
else |
blanchet@49260 | 64 |
() |
blanchet@49260 | 65 |
*} |
blanchet@49260 | 66 |
|
blanchet@49260 | 67 |
ML {* |
blanchet@49260 | 68 |
if do_it then |
blanchet@49260 | 69 |
generate_meng_paulson_suggestions @{context} thy 500 "/tmp/mash_meng_paulson_suggestions" |
blanchet@49260 | 70 |
else |
blanchet@49260 | 71 |
() |
blanchet@49250 | 72 |
*} |
blanchet@49250 | 73 |
|
blanchet@49249 | 74 |
end |