author | blanchet |
Tue, 04 Dec 2012 18:12:29 +0100 | |
changeset 50349 | b79803ee14f3 |
parent 50337 | 68555697f37e |
child 50350 | 136d5318b1fe |
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 |
|
50337 | 8 |
imports |
9 |
Main |
|
10 |
(* |
|
11 |
"~/afp/thys/Jinja/J/TypeSafe" |
|
12 |
"~/afp/thys/ArrowImpossibilityGS/Thys/Arrow_Order" |
|
13 |
"~/afp/thys/FFT/FFT" |
|
14 |
"~~/src/HOL/Auth/NS_Shared" |
|
15 |
"~~/src/HOL/IMPP/Hoare" |
|
16 |
"~~/src/HOL/Library/Fundamental_Theorem_Algebra" |
|
17 |
"~~/src/HOL/Proofs/Lambda/StrongNorm" |
|
18 |
*) |
|
48234 | 19 |
begin |
20 |
||
48891 | 21 |
ML_file "mash_export.ML" |
22 |
||
48245 | 23 |
sledgehammer_params |
50337 | 24 |
[provers = spass, max_relevant = 40, strict, dont_slice, type_enc = mono_native, |
48432
60759d07df24
took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
blanchet
parents:
48379
diff
changeset
|
25 |
lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize] |
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
26 |
|
48234 | 27 |
ML {* |
28 |
open MaSh_Export |
|
29 |
*} |
|
30 |
||
31 |
ML {* |
|
48333 | 32 |
val do_it = false (* switch to "true" to generate the files *) |
50349 | 33 |
val thys = [@{theory Main}] (* [@{theory Fundamental_Theorem_Algebra}] *) |
48333 | 34 |
val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
35 |
val prover = hd provers |
|
50349 | 36 |
val dir = space_implode "__" (map Context.theory_name thys) |
37 |
val prefix = "/tmp/" ^ dir ^ "/" |
|
50337 | 38 |
*} |
39 |
||
40 |
ML {* |
|
41 |
Isabelle_System.mkdir (Path.explode prefix) |
|
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
42 |
*} |
48531 | 43 |
|
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
44 |
ML {* |
48245 | 45 |
if do_it then |
50349 | 46 |
generate_accessibility @{context} thys false (prefix ^ "mash_accessibility") |
48245 | 47 |
else |
48 |
() |
|
49 |
*} |
|
50 |
||
51 |
ML {* |
|
52 |
if do_it then |
|
50349 | 53 |
generate_features @{context} prover thys false (prefix ^ "mash_features") |
48245 | 54 |
else |
55 |
() |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
56 |
*} |
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
57 |
|
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
58 |
ML {* |
48245 | 59 |
if do_it then |
50349 | 60 |
generate_isar_dependencies @{context} thys false (prefix ^ "mash_dependencies") |
48333 | 61 |
else |
62 |
() |
|
63 |
*} |
|
64 |
||
65 |
ML {* |
|
66 |
if do_it then |
|
50349 | 67 |
generate_commands @{context} params thys (prefix ^ "mash_commands") |
48333 | 68 |
else |
69 |
() |
|
70 |
*} |
|
71 |
||
72 |
ML {* |
|
73 |
if do_it then |
|
50349 | 74 |
generate_mepo_suggestions @{context} params thys 1024 (prefix ^ "mash_mepo_suggestions") |
48245 | 75 |
else |
76 |
() |
|
77 |
*} |
|
78 |
||
79 |
ML {* |
|
80 |
if do_it then |
|
50349 | 81 |
generate_atp_dependencies @{context} params thys false (prefix ^ "mash_atp_dependencies") |
48245 | 82 |
else |
83 |
() |
|
48234 | 84 |
*} |
85 |
||
86 |
end |