blanchet@49300
|
1 |
(* Title: HOL/TPTP/MaSh_Eval.thy
|
blanchet@49249
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@49249
|
3 |
*)
|
blanchet@49249
|
4 |
|
blanchet@49300
|
5 |
header {* MaSh Evaluation Driver *}
|
blanchet@49249
|
6 |
|
blanchet@49300
|
7 |
theory MaSh_Eval
|
blanchet@49348
|
8 |
imports Complex_Main
|
blanchet@49249
|
9 |
begin
|
blanchet@49249
|
10 |
|
wenzelm@49906
|
11 |
ML_file "mash_eval.ML"
|
wenzelm@49906
|
12 |
|
blanchet@49299
|
13 |
sledgehammer_params
|
blanchet@51534
|
14 |
[provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
|
blanchet@51940
|
15 |
lam_trans = lifting, timeout = 15, dont_preplay, minimize]
|
blanchet@49299
|
16 |
|
blanchet@51940
|
17 |
declare [[sledgehammer_instantiate_inducts = false]]
|
blanchet@49251
|
18 |
|
blanchet@49250
|
19 |
ML {*
|
blanchet@51499
|
20 |
!Multithreading.max_threads
|
blanchet@51473
|
21 |
*}
|
blanchet@51473
|
22 |
|
blanchet@51473
|
23 |
ML {*
|
blanchet@49300
|
24 |
open MaSh_Eval
|
blanchet@49250
|
25 |
*}
|
blanchet@49250
|
26 |
|
blanchet@49250
|
27 |
ML {*
|
blanchet@49348
|
28 |
val do_it = false (* switch to "true" to generate the files *)
|
blanchet@49266
|
29 |
val params = Sledgehammer_Isar.default_params @{context} []
|
blanchet@51979
|
30 |
val range = (1, NONE)
|
blanchet@51528
|
31 |
val dir = "List"
|
blanchet@51528
|
32 |
val prefix = "/tmp/" ^ dir ^ "/"
|
blanchet@51528
|
33 |
val prob_dir = prefix ^ "mash_problems"
|
blanchet@49250
|
34 |
*}
|
blanchet@49250
|
35 |
|
blanchet@49250
|
36 |
ML {*
|
blanchet@49265
|
37 |
if do_it then
|
blanchet@51463
|
38 |
Isabelle_System.mkdir (Path.explode prob_dir)
|
blanchet@51463
|
39 |
else
|
blanchet@51463
|
40 |
()
|
blanchet@51463
|
41 |
*}
|
blanchet@51463
|
42 |
|
blanchet@51463
|
43 |
ML {*
|
blanchet@51463
|
44 |
if do_it then
|
blanchet@51979
|
45 |
evaluate_mash_suggestions @{context} params range
|
blanchet@51968
|
46 |
[MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
|
blanchet@51979
|
47 |
(SOME prob_dir)
|
blanchet@51979
|
48 |
(prefix ^ "mepo_suggestions")
|
blanchet@51979
|
49 |
(prefix ^ "mash_suggestions")
|
blanchet@51979
|
50 |
(prefix ^ "mash_prover_suggestions")
|
blanchet@51979
|
51 |
(prefix ^ "mesh_suggestions")
|
blanchet@51979
|
52 |
(prefix ^ "mesh_prover_suggestions")
|
blanchet@51979
|
53 |
(prefix ^ "mash_eval")
|
blanchet@49265
|
54 |
else
|
blanchet@49265
|
55 |
()
|
blanchet@49250
|
56 |
*}
|
blanchet@49250
|
57 |
|
blanchet@49249
|
58 |
end
|