author | blanchet |
Mon, 08 Sep 2014 13:56:28 +0200 | |
changeset 58206 | 3e22d3ed829f |
parent 57457 | b2bafc09b7e7 |
child 58889 | 5b7a9633cfa8 |
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 |
|
58206
3e22d3ed829f
refactored MaSh files to avoid regenerating exports on each eval
blanchet
parents:
57457
diff
changeset
|
8 |
imports MaSh_Export_Base |
48234 | 9 |
begin |
10 |
||
50337 | 11 |
ML {* |
50350
136d5318b1fe
tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents:
50349
diff
changeset
|
12 |
if do_it then |
136d5318b1fe
tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents:
50349
diff
changeset
|
13 |
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
|
14 |
else |
136d5318b1fe
tuned MaSh exporter -- and don't make temp directories unless explicitly told so
blanchet
parents:
50349
diff
changeset
|
15 |
() |
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
16 |
*} |
48531 | 17 |
|
57120 | 18 |
ML {* |
19 |
if do_it then |
|
57457 | 20 |
generate_mash_suggestions "nb" @{context} params (range, step) thys max_suggestions |
57431
02c408aed5ee
killed Python version of MaSh, now that the SML version works adequately
blanchet
parents:
57150
diff
changeset
|
21 |
(prefix ^ "mash_nb_suggestions") |
57120 | 22 |
else |
23 |
() |
|
24 |
*} |
|
25 |
||
48246
fb11c09d7729
add Isabelle dependencies to tweak relevance filter
blanchet
parents:
48245
diff
changeset
|
26 |
ML {* |
48245 | 27 |
if do_it then |
57457 | 28 |
generate_mash_suggestions "knn" @{context} params (range, step) thys max_suggestions |
57431
02c408aed5ee
killed Python version of MaSh, now that the SML version works adequately
blanchet
parents:
57150
diff
changeset
|
29 |
(prefix ^ "mash_knn_suggestions") |
57120 | 30 |
else |
31 |
() |
|
32 |
*} |
|
33 |
||
57457 | 34 |
ML {* |
35 |
if do_it then |
|
36 |
generate_mepo_suggestions @{context} params (range, step) thys max_suggestions |
|
37 |
(prefix ^ "mepo_suggestions") |
|
38 |
else |
|
39 |
() |
|
40 |
*} |
|
41 |
||
42 |
ML {* |
|
43 |
if do_it then |
|
44 |
generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_suggestions") |
|
45 |
(prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_suggestions") |
|
46 |
else |
|
47 |
() |
|
48 |
*} |
|
49 |
||
50 |
ML {* |
|
51 |
if do_it then |
|
52 |
generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_suggestions") |
|
53 |
(prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_suggestions") |
|
54 |
else |
|
55 |
() |
|
56 |
*} |
|
57120 | 57 |
|
58 |
ML {* |
|
59 |
if do_it then |
|
57457 | 60 |
generate_prover_dependencies @{context} params range thys |
61 |
(prefix ^ "mash_nb_prover_dependencies") |
|
62 |
else |
|
63 |
() |
|
64 |
*} |
|
65 |
||
66 |
ML {* |
|
67 |
if do_it then |
|
68 |
generate_prover_dependencies @{context} params range thys |
|
69 |
(prefix ^ "mash_knn_prover_dependencies") |
|
70 |
else |
|
71 |
() |
|
72 |
*} |
|
73 |
||
74 |
ML {* |
|
75 |
if do_it then |
|
76 |
generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_prover_suggestions") |
|
77 |
(prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_prover_suggestions") |
|
78 |
else |
|
79 |
() |
|
80 |
*} |
|
81 |
||
82 |
ML {* |
|
83 |
if do_it then |
|
84 |
generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_prover_suggestions") |
|
85 |
(prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_prover_suggestions") |
|
57120 | 86 |
else |
87 |
() |
|
88 |
*} |
|
89 |
||
90 |
ML {* |
|
91 |
if do_it then |
|
57121 | 92 |
generate_accessibility @{context} thys (prefix ^ "mash_accessibility") |
48245 | 93 |
else |
94 |
() |
|
95 |
*} |
|
96 |
||
97 |
ML {* |
|
98 |
if do_it then |
|
55212 | 99 |
generate_features @{context} thys (prefix ^ "mash_features") |
48245 | 100 |
else |
101 |
() |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
102 |
*} |
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
103 |
|
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
104 |
ML {* |
48245 | 105 |
if do_it then |
57121 | 106 |
generate_isar_dependencies @{context} range thys (prefix ^ "mash_dependencies") |
48333 | 107 |
else |
108 |
() |
|
109 |
*} |
|
110 |
||
111 |
ML {* |
|
112 |
if do_it then |
|
57121 | 113 |
generate_isar_commands @{context} prover (range, step) thys max_suggestions |
57120 | 114 |
(prefix ^ "mash_commands") |
48333 | 115 |
else |
116 |
() |
|
117 |
*} |
|
118 |
||
119 |
ML {* |
|
50816 | 120 |
if do_it then |
57121 | 121 |
generate_prover_commands @{context} params (range, step) thys max_suggestions |
57120 | 122 |
(prefix ^ "mash_prover_commands") |
50411 | 123 |
else |
124 |
() |
|
125 |
*} |
|
126 |
||
48234 | 127 |
end |