author  blanchet 
Fri, 18 Jan 2013 00:18:11 +0100  
changeset 50967  00d87ade2294 
parent 50965  7a7d1418301e 
child 51004  5f2788c38127 
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 

50953  12 
val MePoN : string 
13 
val MaSh_IsarN : string 

14 
val MaSh_ProverN : string 

15 
val MeSh_IsarN : string 

16 
val MeSh_ProverN : string 

17 
val IsarN : string 

50437  18 
val evaluate_mash_suggestions : 
50953  19 
Proof.context > params > int * int option > string list > string option 
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

20 
> string > string > string > string > string > string > unit 
48234  21 
end; 
22 

48285  23 
structure MaSh_Eval : MASH_EVAL = 
48234  24 
struct 
48235  25 

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

27 
open Sledgehammer_Fact 
50557  28 
open Sledgehammer_MePo 
48381  29 
open Sledgehammer_MaSh 
50557  30 
open Sledgehammer_Provers 
31 
open Sledgehammer_Isar 

48240  32 

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

33 
val MePoN = "MePo" 
50952  34 
val MaSh_IsarN = "MaShIsar" 
35 
val MaSh_ProverN = "MaShProver" 

36 
val MeSh_IsarN = "MeShIsar" 

37 
val MeSh_ProverN = "MeShProver" 

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

38 
val IsarN = "Isar" 
48241  39 

50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

40 
fun in_range (from, to) j = 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

41 
j >= from andalso (to = NONE orelse j <= the to) 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

42 

50953  43 
fun evaluate_mash_suggestions ctxt params range methods prob_dir_name 
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

44 
mepo_file_name mash_isar_file_name mash_prover_file_name 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

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

47 
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

48 
val _ = File.write report_path "" 
50589  49 
fun print s = File.append report_path (s ^ "\n") 
48293  50 
val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = 
50557  51 
default_params ctxt [] 
48318  52 
val prover = hd provers 
50412  53 
val slack_max_facts = generous_max_facts (the max_facts) 
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

54 
val lines_of = Path.explode #> try File.read_lines #> these 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

55 
val file_names = 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

56 
[mepo_file_name, mash_isar_file_name, mash_prover_file_name, 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

57 
mesh_isar_file_name, mesh_prover_file_name] 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

58 
val lines as [mepo_lines, mash_isar_lines, mash_prover_lines, 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

59 
mesh_isar_lines, mesh_prover_lines] = 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

60 
map lines_of file_names 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

61 
val num_lines = fold (Integer.max o length) lines 0 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

62 
fun pad lines = lines @ replicate (num_lines  length lines) "" 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

63 
val lines = 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

64 
pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~ 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

65 
pad mesh_isar_lines ~~ pad mesh_prover_lines 
50557  66 
val css = clasimpset_rule_table_of ctxt 
50442
4f6a4d32522c
don't blacklist "case" theorems  this causes problems in MaSh later
blanchet
parents:
50440
diff
changeset

67 
val facts = all_facts ctxt true false Symtab.empty [] [] css 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50633
diff
changeset

68 
val name_tabs = build_name_tables nickname_of_thm facts 
48289  69 
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) 
50952  70 
fun index_str (j, s) = s ^ "@" ^ string_of_int j 
50953  71 
val str_of_method = enclose " " ": " 
72 
fun str_of_result method facts ({outcome, run_time, used_facts, ...} 

50952  73 
: prover_result) = 
48289  74 
let val facts = facts > map (fn ((name, _), _) => name ()) in 
50953  75 
str_of_method method ^ 
48289  76 
(if is_none outcome then 
77 
"Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ 

78 
(used_facts > map (with_index facts o fst) 

79 
> sort (int_ord o pairself fst) 

50952  80 
> map index_str 
48289  81 
> space_implode " ") ^ 
48293  82 
(if length facts < the max_facts then 
48289  83 
" (of " ^ string_of_int (length facts) ^ ")" 
84 
else 

85 
"") 

86 
else 

87 
"Failure: " ^ 

48293  88 
(facts > take (the max_facts) > tag_list 1 
50952  89 
> map index_str 
48289  90 
> space_implode " ")) 
91 
end 

50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

92 
fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line), 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

93 
mesh_isar_line), mesh_prover_line)) = 
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

94 
if in_range range j then 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

95 
let 
50965  96 
val get_suggs = extract_suggestions ##> take slack_max_facts 
97 
val (name1, mepo_suggs) = get_suggs mepo_line 

98 
val (name2, mash_isar_suggs) = get_suggs mash_isar_line 

99 
val (name3, mash_prover_suggs) = get_suggs mash_prover_line 

100 
val (name4, mesh_isar_suggs) = get_suggs mesh_isar_line 

101 
val (name5, mesh_prover_suggs) = get_suggs mesh_prover_line 

50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

102 
val [name] = 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

103 
[name1, name2, name3, name4, name5] 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

104 
> filter (curry (op <>) "") > distinct (op =) 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

105 
handle General.Match => error "Input files out of sync." 
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

106 
val th = 
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50620
diff
changeset

107 
case find_first (fn (_, th) => nickname_of_thm th = name) facts of 
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

108 
SOME (_, th) => th 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

109 
 NONE => error ("No fact called \"" ^ name ^ "\".") 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

110 
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

111 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset

112 
val isar_deps = isar_dependencies_of name_tabs th 
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

113 
val facts = facts > filter (fn (_, th') => thm_ord (th', th) = LESS) 
50967
00d87ade2294
optimization  evaluate conversion to table only once
blanchet
parents:
50965
diff
changeset

114 
val find_suggs = find_suggested_facts facts 
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

115 
fun get_facts [] compute = compute facts 
50967
00d87ade2294
optimization  evaluate conversion to table only once
blanchet
parents:
50965
diff
changeset

116 
 get_facts suggs _ = find_suggs suggs 
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

117 
val mepo_facts = 
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

118 
get_facts mepo_suggs (fn _ => 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

119 
mepo_suggested_facts ctxt params prover slack_max_facts NONE 
50965  120 
hyp_ts concl_t facts) 
121 
> weight_mepo_facts 

50952  122 
fun mash_of suggs = 
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

123 
get_facts suggs (fn _ => 
50965  124 
find_mash_suggestions slack_max_facts suggs facts [] [] > fst) 
125 
> weight_mash_facts 

50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

126 
val mash_isar_facts = mash_of mash_isar_suggs 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

127 
val mash_prover_facts = mash_of mash_prover_suggs 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

128 
fun mess_of mash_facts = 
50814  129 
[(mepo_weight, (mepo_facts, [])), 
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

130 
(mash_weight, (mash_facts, []))] 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

131 
fun mesh_of suggs mash_facts = 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

132 
get_facts suggs (fn _ => 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

133 
mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts 
50965  134 
(mess_of mash_facts)) 
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

135 
val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts 
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

136 
val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts 
50967
00d87ade2294
optimization  evaluate conversion to table only once
blanchet
parents:
50965
diff
changeset

137 
val isar_facts = find_suggs isar_deps 
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

138 
(* adapted from "mirabelle_sledgehammer.ML" *) 
50953  139 
fun set_file_name method (SOME dir) = 
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

140 
let 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

141 
val prob_prefix = 
50826  142 
"goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ 
50953  143 
method 
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

144 
in 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

145 
Config.put dest_dir dir 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

146 
#> Config.put problem_prefix (prob_prefix ^ "__") 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

147 
#> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

148 
end 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

149 
 set_file_name _ NONE = I 
50965  150 
fun prove method get facts = 
50953  151 
if not (member (op =) methods method) orelse 
152 
(null facts andalso method <> IsarN) then 

153 
(str_of_method method ^ "Skipped", 0) 

50952  154 
else 
155 
let 

156 
fun nickify ((_, stature), th) = 

157 
((K (encode_str (nickname_of_thm th)), stature), th) 

158 
val facts = 

159 
facts 

50965  160 
> map (get #> nickify) 
50952  161 
> maybe_instantiate_inducts ctxt hyp_ts concl_t 
162 
> take (the max_facts) 

50953  163 
val ctxt = ctxt > set_file_name method prob_dir_name 
50952  164 
val res as {outcome, ...} = 
165 
run_prover_for_mash ctxt params prover facts goal 

166 
val ok = if is_none outcome then 1 else 0 

50953  167 
in (str_of_result method facts res, ok) end 
50591  168 
val ress = 
50965  169 
[fn () => prove MePoN fst mepo_facts, 
170 
fn () => prove MaSh_IsarN fst mash_isar_facts, 

171 
fn () => prove MaSh_ProverN fst mash_prover_facts, 

172 
fn () => prove MeSh_IsarN I mesh_isar_facts, 

173 
fn () => prove MeSh_ProverN I mesh_prover_facts, 

174 
fn () => prove IsarN I isar_facts] 

50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

175 
> (* Par_List. *) map (fn f => f ()) 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

176 
in 
50591  177 
"Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress 
50587
bd6582be1562
synchronize access to shared reference and print proper total
blanchet
parents:
50563
diff
changeset

178 
> cat_lines > print; 
50591  179 
map snd ress 
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

180 
end 
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50557
diff
changeset

181 
else 
50952  182 
[0, 0, 0, 0, 0, 0] 
50953  183 
fun total_of method ok n = 
184 
str_of_method method ^ string_of_int ok ^ " (" ^ 

50591  185 
Real.fmt (StringCvt.FIX (SOME 1)) 
186 
(100.0 * Real.fromInt ok / Real.fromInt n) ^ "%)" 

50557  187 
val inst_inducts = Config.get ctxt instantiate_inducts 
48245  188 
val options = 
50767  189 
["prover = " ^ prover, 
190 
"max_facts = " ^ string_of_int (the max_facts), 

191 
"slice" > not slice ? prefix "dont_", 

192 
"type_enc = " ^ the_default "smart" type_enc, 

193 
"lam_trans = " ^ the_default "smart" lam_trans, 

194 
"timeout = " ^ ATP_Util.string_from_time (the_default one_year timeout), 

48241  195 
"instantiate_inducts" > not inst_inducts ? prefix "dont_"] 
50587
bd6582be1562
synchronize access to shared reference and print proper total
blanchet
parents:
50563
diff
changeset

196 
val _ = print " * * *"; 
bd6582be1562
synchronize access to shared reference and print proper total
blanchet
parents:
50563
diff
changeset

197 
val _ = print ("Options: " ^ commas options); 
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset

198 
val oks = Par_List.map solve_goal (tag_list 1 lines) 
50620  199 
val n = length oks 
50952  200 
val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok, 
201 
isar_ok] = 

50591  202 
map Integer.sum (map_transpose I oks) 
48241  203 
in 
204 
["Successes (of " ^ string_of_int n ^ " goals)", 

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

205 
total_of MePoN mepo_ok n, 
50952  206 
total_of MaSh_IsarN mash_isar_ok n, 
207 
total_of MaSh_ProverN mash_prover_ok n, 

208 
total_of MeSh_IsarN mesh_isar_ok n, 

209 
total_of MeSh_ProverN mesh_prover_ok n, 

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

210 
total_of IsarN isar_ok n] 
50437  211 
> cat_lines > print 
48241  212 
end 
48235  213 

48234  214 
end; 