| author | wenzelm |
| Fri, 19 Jan 2018 14:55:46 +0100 | |
| changeset 67471 | bddfa23a4ea9 |
| parent 63167 | 0909deb8059b |
| child 73315 | d01ca5e9e0da |
| permissions | -rw-r--r-- |
| 48234 | 1 |
(* Title: HOL/TPTP/MaSh_Export.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
*) |
|
4 |
||
| 63167 | 5 |
section \<open>MaSh Exporter\<close> |
| 48234 | 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 |
||
| 63167 | 11 |
ML \<open> |
|
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 |
() |
| 63167 | 16 |
\<close> |
| 48531 | 17 |
|
| 63167 | 18 |
ML \<open> |
| 57120 | 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 |
() |
|
| 63167 | 24 |
\<close> |
| 57120 | 25 |
|
| 63167 | 26 |
ML \<open> |
| 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 |
() |
|
| 63167 | 32 |
\<close> |
| 57120 | 33 |
|
| 63167 | 34 |
ML \<open> |
| 57457 | 35 |
if do_it then |
36 |
generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
|
|
37 |
(prefix ^ "mepo_suggestions") |
|
38 |
else |
|
39 |
() |
|
| 63167 | 40 |
\<close> |
| 57457 | 41 |
|
| 63167 | 42 |
ML \<open> |
| 57457 | 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 |
() |
|
| 63167 | 48 |
\<close> |
| 57457 | 49 |
|
| 63167 | 50 |
ML \<open> |
| 57457 | 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 |
() |
|
| 63167 | 56 |
\<close> |
| 57120 | 57 |
|
| 63167 | 58 |
ML \<open> |
| 57120 | 59 |
if do_it then |
| 57457 | 60 |
generate_prover_dependencies @{context} params range thys
|
61 |
(prefix ^ "mash_nb_prover_dependencies") |
|
62 |
else |
|
63 |
() |
|
| 63167 | 64 |
\<close> |
| 57457 | 65 |
|
| 63167 | 66 |
ML \<open> |
| 57457 | 67 |
if do_it then |
68 |
generate_prover_dependencies @{context} params range thys
|
|
69 |
(prefix ^ "mash_knn_prover_dependencies") |
|
70 |
else |
|
71 |
() |
|
| 63167 | 72 |
\<close> |
| 57457 | 73 |
|
| 63167 | 74 |
ML \<open> |
| 57457 | 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 |
() |
|
| 63167 | 80 |
\<close> |
| 57457 | 81 |
|
| 63167 | 82 |
ML \<open> |
| 57457 | 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 |
() |
|
| 63167 | 88 |
\<close> |
| 57120 | 89 |
|
| 63167 | 90 |
ML \<open> |
| 57120 | 91 |
if do_it then |
| 57121 | 92 |
generate_accessibility @{context} thys (prefix ^ "mash_accessibility")
|
| 48245 | 93 |
else |
94 |
() |
|
| 63167 | 95 |
\<close> |
| 48245 | 96 |
|
| 63167 | 97 |
ML \<open> |
| 48245 | 98 |
if do_it then |
| 55212 | 99 |
generate_features @{context} thys (prefix ^ "mash_features")
|
| 48245 | 100 |
else |
101 |
() |
|
| 63167 | 102 |
\<close> |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
103 |
|
| 63167 | 104 |
ML \<open> |
| 48245 | 105 |
if do_it then |
| 57121 | 106 |
generate_isar_dependencies @{context} range thys (prefix ^ "mash_dependencies")
|
| 48333 | 107 |
else |
108 |
() |
|
| 63167 | 109 |
\<close> |
| 48333 | 110 |
|
| 63167 | 111 |
ML \<open> |
| 48333 | 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 |
() |
|
| 63167 | 117 |
\<close> |
| 48333 | 118 |
|
| 63167 | 119 |
ML \<open> |
| 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 |
() |
|
| 63167 | 125 |
\<close> |
| 50411 | 126 |
|
| 48234 | 127 |
end |