author | blanchet |
Wed, 12 Dec 2012 21:59:03 +0100 | |
changeset 50513 | cacf3cdb3276 |
parent 50484 | 8ec31bdb9d36 |
child 50519 | 2951841ec011 |
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 |
50411 | 14 |
[provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native, |
15 |
lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize] |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
16 |
|
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
|
17 |
declare [[sledgehammer_instantiate_inducts]] |
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
|
18 |
|
48234 | 19 |
ML {* |
20 |
open MaSh_Export |
|
21 |
*} |
|
22 |
||
23 |
ML {* |
|
48333 | 24 |
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
|
25 |
val thys = [@{theory List}] |
48333 | 26 |
val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
27 |
val prover = hd provers |
|
50513 | 28 |
val dir = "List" |
50349 | 29 |
val prefix = "/tmp/" ^ dir ^ "/" |
50337 | 30 |
*} |
31 |
||
32 |
ML {* |
|
50350
136d5318b1fe
tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents:
50349
diff
changeset
|
33 |
if do_it then |
136d5318b1fe
tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents:
50349
diff
changeset
|
34 |
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
|
35 |
else |
136d5318b1fe
tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents:
50349
diff
changeset
|
36 |
() |
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
37 |
*} |
48531 | 38 |
|
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
39 |
ML {* |
48245 | 40 |
if do_it then |
50349 | 41 |
generate_accessibility @{context} thys false (prefix ^ "mash_accessibility") |
48245 | 42 |
else |
43 |
() |
|
44 |
*} |
|
45 |
||
46 |
ML {* |
|
47 |
if do_it then |
|
50349 | 48 |
generate_features @{context} prover thys false (prefix ^ "mash_features") |
48245 | 49 |
else |
50 |
() |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
51 |
*} |
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
52 |
|
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
53 |
ML {* |
48245 | 54 |
if do_it then |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50434
diff
changeset
|
55 |
generate_isar_dependencies @{context} thys false |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50434
diff
changeset
|
56 |
(prefix ^ "mash_dependencies") |
48333 | 57 |
else |
58 |
() |
|
59 |
*} |
|
60 |
||
61 |
ML {* |
|
62 |
if do_it then |
|
50411 | 63 |
generate_isar_commands @{context} prover thys (prefix ^ "mash_commands") |
48333 | 64 |
else |
65 |
() |
|
66 |
*} |
|
67 |
||
68 |
ML {* |
|
69 |
if do_it then |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50434
diff
changeset
|
70 |
generate_mepo_suggestions @{context} params thys 1024 |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50434
diff
changeset
|
71 |
(prefix ^ "mash_mepo_suggestions") |
48245 | 72 |
else |
73 |
() |
|
74 |
*} |
|
75 |
||
76 |
ML {* |
|
77 |
if do_it then |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50434
diff
changeset
|
78 |
generate_prover_dependencies @{context} params thys false |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50434
diff
changeset
|
79 |
(prefix ^ "mash_prover_dependencies") |
48245 | 80 |
else |
81 |
() |
|
48234 | 82 |
*} |
83 |
||
50411 | 84 |
ML {* |
85 |
if do_it then |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50434
diff
changeset
|
86 |
generate_prover_commands @{context} params thys |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50434
diff
changeset
|
87 |
(prefix ^ "mash_prover_commands") |
50411 | 88 |
else |
89 |
() |
|
90 |
*} |
|
91 |
||
48234 | 92 |
end |