author | blanchet |
Wed, 18 Jul 2012 08:44:04 +0200 | |
changeset 48322 | 8a8d71e34297 |
parent 48301 | e5c5037a3104 |
child 48333 | 2250197977dc |
permissions | -rw-r--r-- |
48285 | 1 |
(* Title: HOL/TPTP/MaSh_Eval.thy |
48234 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
*) |
|
4 |
||
48285 | 5 |
header {* MaSh Evaluation Driver *} |
48234 | 6 |
|
48285 | 7 |
theory MaSh_Eval |
48301 | 8 |
imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d" |
48285 | 9 |
uses "mash_eval.ML" |
48234 | 10 |
begin |
11 |
||
48284 | 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] |
|
15 |
||
48236 | 16 |
declare [[sledgehammer_instantiate_inducts]] |
17 |
||
48235 | 18 |
ML {* |
48285 | 19 |
open MaSh_Eval |
48235 | 20 |
*} |
21 |
||
22 |
ML {* |
|
48322
8a8d71e34297
fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents:
48301
diff
changeset
|
23 |
val do_it = false (* switch to "true" to generate the files *); |
48301 | 24 |
val thy = @{theory Nat}; |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
25 |
val params = Sledgehammer_Isar.default_params @{context} [] |
48235 | 26 |
*} |
27 |
||
28 |
ML {* |
|
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
29 |
if do_it then |
48301 | 30 |
evaluate_mash_suggestions @{context} params thy "/Users/blanchet/tum/mash/mash/results/natNB200ATP-15.pred" |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
31 |
else |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
32 |
() |
48235 | 33 |
*} |
34 |
||
48234 | 35 |
end |