author | blanchet |
Wed, 18 Jul 2012 08:44:03 +0200 | |
changeset 48286 | 788c66a40b32 |
parent 48251 | 6cdcfbddc077 |
child 48296 | e7f01b7e244e |
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 |
|
48286 | 8 |
imports Complex_Main |
48234 | 9 |
uses "mash_export.ML" |
10 |
begin |
|
11 |
||
48245 | 12 |
sledgehammer_params |
13 |
[provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
|
14 |
lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
15 |
|
48234 | 16 |
ML {* |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
17 |
open Sledgehammer_Filter_MaSh |
48234 | 18 |
open MaSh_Export |
19 |
*} |
|
20 |
||
21 |
ML {* |
|
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48246
diff
changeset
|
22 |
val do_it = false (* switch to "true" to generate the files *); |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
23 |
val thy = @{theory Nat}; |
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
24 |
val params = Sledgehammer_Isar.default_params @{context} [] |
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
25 |
*} |
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
26 |
|
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
27 |
ML {* |
48245 | 28 |
if do_it then |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
29 |
generate_accessibility thy false "/tmp/mash_accessibility" |
48245 | 30 |
else |
31 |
() |
|
32 |
*} |
|
33 |
||
34 |
ML {* |
|
35 |
if do_it then |
|
36 |
generate_features thy false "/tmp/mash_features" |
|
37 |
else |
|
38 |
() |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
39 |
*} |
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 |
ML {* |
48245 | 42 |
if do_it then |
43 |
generate_isa_dependencies thy false "/tmp/mash_isa_dependencies" |
|
44 |
else |
|
45 |
() |
|
46 |
*} |
|
47 |
||
48 |
ML {* |
|
49 |
if do_it then |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
50 |
generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies" |
48245 | 51 |
else |
52 |
() |
|
48234 | 53 |
*} |
54 |
||
55 |
ML {* |
|
48245 | 56 |
if do_it then |
57 |
generate_commands thy "/tmp/mash_commands" |
|
58 |
else |
|
59 |
() |
|
48234 | 60 |
*} |
61 |
||
62 |
ML {* |
|
48245 | 63 |
if do_it then |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
64 |
generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions" |
48245 | 65 |
else |
66 |
() |
|
48234 | 67 |
*} |
68 |
||
69 |
end |