author  blanchet 
Sat, 15 Dec 2012 18:26:37 +0100  
changeset 50555  81a1491ba936 
parent 50520  f2d33310337a 
child 50556  6209bc89faa3 
permissions  rwrr 
48285  1 
(* Title: HOL/TPTP/mash_eval.ML 
48234  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2012 

4 

48285  5 
Evaluate proof suggestions from MaSh (Machinelearning for Sledgehammer). 
48234  6 
*) 
7 

48285  8 
signature MASH_EVAL = 
48234  9 
sig 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

10 
type params = Sledgehammer_Provers.params 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

11 

50437  12 
val evaluate_mash_suggestions : 
50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

13 
Proof.context > params > string option > string > string > unit 
48234  14 
end; 
15 

48285  16 
structure MaSh_Eval : MASH_EVAL = 
48234  17 
struct 
48235  18 

48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48313
diff
changeset

19 
open Sledgehammer_Fact 
48381  20 
open Sledgehammer_MaSh 
48240  21 

48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

22 
val MePoN = "MePo" 
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

23 
val MaShN = "MaSh" 
50459  24 
val MeShN = "MeSh" 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

25 
val IsarN = "Isar" 
48241  26 

50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

27 
fun evaluate_mash_suggestions ctxt params prob_dir_name sugg_file_name 
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

28 
report_file_name = 
48235  29 
let 
50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

30 
val report_path = report_file_name > Path.explode 
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

31 
val _ = File.write report_path "" 
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

32 
fun print s = (tracing s; File.append report_path (s ^ "\n")) 
48293  33 
val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = 
48239
0016290f904c
generate MengPaulson facts for evaluation purposes
blanchet
parents:
48236
diff
changeset

34 
Sledgehammer_Isar.default_params ctxt [] 
48318  35 
val prover = hd provers 
50412  36 
val slack_max_facts = generous_max_facts (the max_facts) 
50437  37 
val sugg_path = sugg_file_name > Path.explode 
38 
val lines = sugg_path > File.read_lines 

48530
d443166f9520
repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents:
48438
diff
changeset

39 
val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt 
50442
4f6a4d32522c
don't blacklist "case" theorems  this causes problems in MaSh later
blanchet
parents:
50440
diff
changeset

40 
val facts = all_facts ctxt true false Symtab.empty [] [] css 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50483
diff
changeset

41 
val all_names = build_all_names nickname_of facts 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

42 
val mepo_ok = Unsynchronized.ref 0 
48241  43 
val mash_ok = Unsynchronized.ref 0 
48298  44 
val mesh_ok = Unsynchronized.ref 0 
48300  45 
val isar_ok = Unsynchronized.ref 0 
48289  46 
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) 
48235  47 
fun index_string (j, s) = s ^ "@" ^ string_of_int j 
50436  48 
fun str_of_res label facts ({outcome, run_time, used_facts, ...} 
49 
: Sledgehammer_Provers.prover_result) = 

48289  50 
let val facts = facts > map (fn ((name, _), _) => name ()) in 
51 
" " ^ label ^ ": " ^ 

52 
(if is_none outcome then 

53 
"Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ 

54 
(used_facts > map (with_index facts o fst) 

55 
> sort (int_ord o pairself fst) 

56 
> map index_string 

57 
> space_implode " ") ^ 

48293  58 
(if length facts < the max_facts then 
48289  59 
" (of " ^ string_of_int (length facts) ^ ")" 
60 
else 

61 
"") 

62 
else 

63 
"Failure: " ^ 

48293  64 
(facts > take (the max_facts) > tag_list 1 
48289  65 
> map index_string 
66 
> space_implode " ")) 

67 
end 

48311  68 
fun solve_goal (j, line) = 
48235  69 
let 
48311  70 
val (name, suggs) = extract_query line 
48235  71 
val th = 
48378  72 
case find_first (fn (_, th) => nickname_of th = name) facts of 
48235  73 
SOME (_, th) => th 
48530
d443166f9520
repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents:
48438
diff
changeset

74 
 NONE => error ("No fact called \"" ^ name ^ "\".") 
50358  75 
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th 
48245  76 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 
48404  77 
val isar_deps = isar_dependencies_of all_names th > these 
48235  78 
val facts = facts > filter (fn (_, th') => thm_ord (th', th) = LESS) 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

79 
val mepo_facts = 
48406  80 
Sledgehammer_MePo.mepo_suggested_facts ctxt params prover 
48381  81 
slack_max_facts NONE hyp_ts concl_t facts 
48406  82 
> Sledgehammer_MePo.weight_mepo_facts 
50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50439
diff
changeset

83 
val (mash_facts, mash_unks) = 
50412  84 
find_mash_suggestions slack_max_facts suggs facts [] [] 
50440
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50439
diff
changeset

85 
>> weight_mash_facts 
ca99c269ca3a
don't have MaSh pretend it knows facts it doesn't know
blanchet
parents:
50439
diff
changeset

86 
val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] 
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

87 
val mesh_facts = mesh_facts slack_max_facts mess 
50412  88 
val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts 
50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

89 
(* adapted from "mirabelle_sledgehammer.ML" *) 
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

90 
fun set_file_name heading (SOME dir) = 
50555  91 
let 
92 
val prob_prefix = 

93 
"goal_" ^ string_of_int j ^ "__" ^ name ^ "__" ^ heading 

94 
in 

50483  95 
Config.put Sledgehammer_Provers.dest_dir dir 
96 
#> Config.put Sledgehammer_Provers.problem_prefix 

97 
(prob_prefix ^ "__") 

98 
#> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) 

99 
end 

50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

100 
 set_file_name _ NONE = I 
48406  101 
fun prove ok heading get facts = 
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

102 
let 
50520
f2d33310337a
use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents:
50485
diff
changeset

103 
fun nickify ((_, stature), th) = ((K (nickname_of th), stature), th) 
48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

104 
val facts = 
50520
f2d33310337a
use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents:
50485
diff
changeset

105 
facts 
f2d33310337a
use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents:
50485
diff
changeset

106 
> map get 
f2d33310337a
use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents:
50485
diff
changeset

107 
> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t 
f2d33310337a
use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents:
50485
diff
changeset

108 
> take (the max_facts) 
f2d33310337a
use MaSh nicknames in ATP problem files to facilitate gathering of statistics
blanchet
parents:
50485
diff
changeset

109 
> map nickify 
50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50442
diff
changeset

110 
val ctxt = ctxt > set_file_name heading prob_dir_name 
48321  111 
val res as {outcome, ...} = 
112 
run_prover_for_mash ctxt params prover facts goal 

48313
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

113 
val _ = if is_none outcome then ok := !ok + 1 else () 
0faafdffa662
mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents:
48312
diff
changeset

114 
in str_of_res heading facts res end 
50436  115 
val [mepo_s, mash_s, mesh_s, isar_s] = 
116 
[fn () => prove mepo_ok MePoN fst mepo_facts, 

117 
fn () => prove mash_ok MaShN fst mash_facts, 

50459  118 
fn () => prove mesh_ok MeShN I mesh_facts, 
50436  119 
fn () => prove isar_ok IsarN fst isar_facts] 
50458
85739c08d126
(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
blanchet
parents:
50448
diff
changeset

120 
> (* Par_List. *) map (fn f => f ()) 
48235  121 
in 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

122 
["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, 
48300  123 
isar_s] 
50437  124 
> cat_lines > print 
48235  125 
end 
48241  126 
fun total_of heading ok n = 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

127 
" " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ 
48241  128 
Real.fmt (StringCvt.FIX (SOME 1)) 
129 
(100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset

130 
val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts 
48245  131 
val options = 
48318  132 
[prover, string_of_int (the max_facts) ^ " facts", 
48241  133 
"slice" > not slice ? prefix "dont_", the_default "smart" type_enc, 
134 
the_default "smart" lam_trans, ATP_Util.string_from_time timeout, 

135 
"instantiate_inducts" > not inst_inducts ? prefix "dont_"] 

136 
val n = length lines 

137 
in 

50437  138 
print " * * *"; 
139 
print ("Options: " ^ commas options); 

50458
85739c08d126
(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
blanchet
parents:
50448
diff
changeset

140 
Par_List.map solve_goal (tag_list 1 lines); 
48241  141 
["Successes (of " ^ string_of_int n ^ " goals)", 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

142 
total_of MePoN mepo_ok n, 
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

143 
total_of MaShN mash_ok n, 
50459  144 
total_of MeShN mesh_ok n, 
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (MengPaulson)
blanchet
parents:
48378
diff
changeset

145 
total_of IsarN isar_ok n] 
50437  146 
> cat_lines > print 
48241  147 
end 
48235  148 

48234  149 
end; 