equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* MaSh Exporter *} |
5 header {* MaSh Exporter *} |
6 |
6 |
7 theory MaSh_Export |
7 theory MaSh_Export |
8 imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d" |
8 imports Complex_Main |
9 uses "mash_export.ML" |
9 uses "mash_export.ML" |
10 begin |
10 begin |
11 |
11 |
12 sledgehammer_params |
12 sledgehammer_params |
13 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
13 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
16 ML {* |
16 ML {* |
17 open MaSh_Export |
17 open MaSh_Export |
18 *} |
18 *} |
19 |
19 |
20 ML {* |
20 ML {* |
21 val do_it = false (* switch to "true" to generate the files *); |
21 val do_it = false (* switch to "true" to generate the files *) |
22 val thy = @{theory List}; |
22 val thy = @{theory List} |
23 val params = Sledgehammer_Isar.default_params @{context} [] |
23 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
|
24 val prover = hd provers |
24 *} |
25 *} |
25 |
26 |
26 ML {* |
27 ML {* |
27 if do_it then |
28 if do_it then |
28 generate_accessibility thy false "/tmp/mash_accessibility" |
29 generate_accessibility thy false "/tmp/mash_accessibility" |
30 () |
31 () |
31 *} |
32 *} |
32 |
33 |
33 ML {* |
34 ML {* |
34 if do_it then |
35 if do_it then |
35 generate_features @{context} thy false "/tmp/mash_features" |
36 generate_features @{context} prover thy false "/tmp/mash_features" |
36 else |
37 else |
37 () |
38 () |
38 *} |
39 *} |
39 |
40 |
40 ML {* |
41 ML {* |
41 if do_it then |
42 if do_it then |
42 generate_isa_dependencies thy false "/tmp/mash_isa_dependencies" |
43 generate_isar_dependencies thy false "/tmp/mash_dependencies" |
|
44 else |
|
45 () |
|
46 *} |
|
47 |
|
48 ML {* |
|
49 if do_it then |
|
50 generate_commands @{context} prover thy "/tmp/mash_commands" |
|
51 else |
|
52 () |
|
53 *} |
|
54 |
|
55 ML {* |
|
56 if do_it then |
|
57 generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions" |
43 else |
58 else |
44 () |
59 () |
45 *} |
60 *} |
46 |
61 |
47 ML {* |
62 ML {* |
49 generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies" |
64 generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies" |
50 else |
65 else |
51 () |
66 () |
52 *} |
67 *} |
53 |
68 |
54 ML {* |
|
55 if do_it then |
|
56 generate_commands @{context} thy "/tmp/mash_commands" |
|
57 else |
|
58 () |
|
59 *} |
|
60 |
|
61 ML {* |
|
62 if do_it then |
|
63 generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions" |
|
64 else |
|
65 () |
|
66 *} |
|
67 |
69 |
68 end |
70 end |