blanchet@49300
|
1 |
(* Title: HOL/TPTP/mash_eval.ML
|
blanchet@49249
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@49249
|
3 |
Copyright 2012
|
blanchet@49249
|
4 |
|
blanchet@49300
|
5 |
Evaluate proof suggestions from MaSh (Machine-learning for Sledgehammer).
|
blanchet@49249
|
6 |
*)
|
blanchet@49249
|
7 |
|
blanchet@49300
|
8 |
signature MASH_EVAL =
|
blanchet@49249
|
9 |
sig
|
blanchet@49266
|
10 |
type params = Sledgehammer_Provers.params
|
blanchet@49266
|
11 |
|
blanchet@52197
|
12 |
val MePoN : string
|
blanchet@51968
|
13 |
val MaSh_IsarN : string
|
blanchet@51968
|
14 |
val MaSh_ProverN : string
|
blanchet@51968
|
15 |
val MeSh_IsarN : string
|
blanchet@51968
|
16 |
val MeSh_ProverN : string
|
blanchet@51968
|
17 |
val IsarN : string
|
blanchet@51452
|
18 |
val evaluate_mash_suggestions :
|
blanchet@52319
|
19 |
Proof.context -> params -> int * int option -> bool -> string list
|
blanchet@52319
|
20 |
-> string option -> string -> string -> string -> string -> string -> string
|
blanchet@52319
|
21 |
-> unit
|
blanchet@49249
|
22 |
end;
|
blanchet@49249
|
23 |
|
blanchet@49300
|
24 |
structure MaSh_Eval : MASH_EVAL =
|
blanchet@49249
|
25 |
struct
|
blanchet@49250
|
26 |
|
blanchet@51572
|
27 |
open Sledgehammer_Util
|
blanchet@49330
|
28 |
open Sledgehammer_Fact
|
blanchet@51572
|
29 |
open Sledgehammer_MePo
|
blanchet@49396
|
30 |
open Sledgehammer_MaSh
|
blanchet@51572
|
31 |
open Sledgehammer_Provers
|
blanchet@51572
|
32 |
open Sledgehammer_Isar
|
blanchet@49255
|
33 |
|
blanchet@52190
|
34 |
val MaSh_IsarN = MaShN ^ "-Isar"
|
blanchet@52190
|
35 |
val MaSh_ProverN = MaShN ^ "-Prover"
|
blanchet@52190
|
36 |
val MeSh_IsarN = MeShN ^ "-Isar"
|
blanchet@52190
|
37 |
val MeSh_ProverN = MeShN ^ "-Prover"
|
blanchet@49394
|
38 |
val IsarN = "Isar"
|
blanchet@49256
|
39 |
|
blanchet@51574
|
40 |
fun in_range (from, to) j =
|
blanchet@51574
|
41 |
j >= from andalso (to = NONE orelse j <= the to)
|
blanchet@51574
|
42 |
|
blanchet@52319
|
43 |
fun evaluate_mash_suggestions ctxt params range linearize methods prob_dir_name
|
blanchet@51979
|
44 |
mepo_file_name mash_isar_file_name mash_prover_file_name
|
blanchet@51979
|
45 |
mesh_isar_file_name mesh_prover_file_name report_file_name =
|
blanchet@49250
|
46 |
let
|
blanchet@52210
|
47 |
val zeros = [0, 0, 0, 0, 0, 0]
|
blanchet@51463
|
48 |
val report_path = report_file_name |> Path.explode
|
blanchet@51463
|
49 |
val _ = File.write report_path ""
|
blanchet@51604
|
50 |
fun print s = File.append report_path (s ^ "\n")
|
blanchet@49308
|
51 |
val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
|
blanchet@51572
|
52 |
default_params ctxt []
|
blanchet@49333
|
53 |
val prover = hd provers
|
blanchet@51427
|
54 |
val slack_max_facts = generous_max_facts (the max_facts)
|
blanchet@51979
|
55 |
val lines_of = Path.explode #> try File.read_lines #> these
|
blanchet@51979
|
56 |
val file_names =
|
blanchet@51979
|
57 |
[mepo_file_name, mash_isar_file_name, mash_prover_file_name,
|
blanchet@51979
|
58 |
mesh_isar_file_name, mesh_prover_file_name]
|
blanchet@51979
|
59 |
val lines as [mepo_lines, mash_isar_lines, mash_prover_lines,
|
blanchet@51979
|
60 |
mesh_isar_lines, mesh_prover_lines] =
|
blanchet@51979
|
61 |
map lines_of file_names
|
blanchet@51979
|
62 |
val num_lines = fold (Integer.max o length) lines 0
|
blanchet@51979
|
63 |
fun pad lines = lines @ replicate (num_lines - length lines) ""
|
blanchet@51979
|
64 |
val lines =
|
blanchet@51979
|
65 |
pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~
|
blanchet@51979
|
66 |
pad mesh_isar_lines ~~ pad mesh_prover_lines
|
blanchet@51572
|
67 |
val css = clasimpset_rule_table_of ctxt
|
blanchet@51457
|
68 |
val facts = all_facts ctxt true false Symtab.empty [] [] css
|
blanchet@51750
|
69 |
val name_tabs = build_name_tables nickname_of_thm facts
|
blanchet@49304
|
70 |
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
|
blanchet@51967
|
71 |
fun index_str (j, s) = s ^ "@" ^ string_of_int j
|
blanchet@51968
|
72 |
val str_of_method = enclose " " ": "
|
blanchet@51968
|
73 |
fun str_of_result method facts ({outcome, run_time, used_facts, ...}
|
blanchet@51967
|
74 |
: prover_result) =
|
blanchet@52186
|
75 |
let val facts = facts |> map (fst o fst) in
|
blanchet@51968
|
76 |
str_of_method method ^
|
blanchet@49304
|
77 |
(if is_none outcome then
|
blanchet@49304
|
78 |
"Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
|
blanchet@49304
|
79 |
(used_facts |> map (with_index facts o fst)
|
blanchet@49304
|
80 |
|> sort (int_ord o pairself fst)
|
blanchet@51967
|
81 |
|> map index_str
|
blanchet@49304
|
82 |
|> space_implode " ") ^
|
blanchet@49308
|
83 |
(if length facts < the max_facts then
|
blanchet@49304
|
84 |
" (of " ^ string_of_int (length facts) ^ ")"
|
blanchet@49304
|
85 |
else
|
blanchet@49304
|
86 |
"")
|
blanchet@49304
|
87 |
else
|
blanchet@49304
|
88 |
"Failure: " ^
|
blanchet@49308
|
89 |
(facts |> take (the max_facts) |> tag_list 1
|
blanchet@51967
|
90 |
|> map index_str
|
blanchet@49304
|
91 |
|> space_implode " "))
|
blanchet@49304
|
92 |
end
|
blanchet@51979
|
93 |
fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line),
|
blanchet@51979
|
94 |
mesh_isar_line), mesh_prover_line)) =
|
blanchet@51574
|
95 |
if in_range range j then
|
blanchet@51574
|
96 |
let
|
blanchet@51980
|
97 |
val get_suggs = extract_suggestions ##> take slack_max_facts
|
blanchet@51980
|
98 |
val (name1, mepo_suggs) = get_suggs mepo_line
|
blanchet@51980
|
99 |
val (name2, mash_isar_suggs) = get_suggs mash_isar_line
|
blanchet@51980
|
100 |
val (name3, mash_prover_suggs) = get_suggs mash_prover_line
|
blanchet@51980
|
101 |
val (name4, mesh_isar_suggs) = get_suggs mesh_isar_line
|
blanchet@51980
|
102 |
val (name5, mesh_prover_suggs) = get_suggs mesh_prover_line
|
blanchet@51979
|
103 |
val [name] =
|
blanchet@51979
|
104 |
[name1, name2, name3, name4, name5]
|
blanchet@51979
|
105 |
|> filter (curry (op <>) "") |> distinct (op =)
|
blanchet@51979
|
106 |
handle General.Match => error "Input files out of sync."
|
blanchet@51574
|
107 |
val th =
|
blanchet@51639
|
108 |
case find_first (fn (_, th) => nickname_of_thm th = name) facts of
|
blanchet@51574
|
109 |
SOME (_, th) => th
|
blanchet@51574
|
110 |
| NONE => error ("No fact called \"" ^ name ^ "\".")
|
blanchet@51574
|
111 |
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
|
blanchet@51574
|
112 |
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
|
blanchet@51769
|
113 |
val isar_deps = isar_dependencies_of name_tabs th
|
blanchet@52272
|
114 |
val facts =
|
blanchet@52336
|
115 |
facts
|
blanchet@52336
|
116 |
|> filter (fn (_, th') =>
|
blanchet@52336
|
117 |
if linearize then crude_thm_ord (th', th) = LESS
|
blanchet@52336
|
118 |
else thm_less (th', th))
|
blanchet@52271
|
119 |
val find_suggs =
|
blanchet@52271
|
120 |
find_suggested_facts ctxt facts #> map fact_of_raw_fact
|
blanchet@51979
|
121 |
fun get_facts [] compute = compute facts
|
blanchet@51982
|
122 |
| get_facts suggs _ = find_suggs suggs
|
blanchet@51574
|
123 |
val mepo_facts =
|
blanchet@51979
|
124 |
get_facts mepo_suggs (fn _ =>
|
blanchet@51979
|
125 |
mepo_suggested_facts ctxt params prover slack_max_facts NONE
|
blanchet@51980
|
126 |
hyp_ts concl_t facts)
|
blanchet@51980
|
127 |
|> weight_mepo_facts
|
blanchet@51967
|
128 |
fun mash_of suggs =
|
blanchet@51979
|
129 |
get_facts suggs (fn _ =>
|
blanchet@52271
|
130 |
find_mash_suggestions ctxt slack_max_facts suggs facts [] []
|
blanchet@52186
|
131 |
|> fst |> map fact_of_raw_fact)
|
blanchet@51980
|
132 |
|> weight_mash_facts
|
blanchet@51979
|
133 |
val mash_isar_facts = mash_of mash_isar_suggs
|
blanchet@51979
|
134 |
val mash_prover_facts = mash_of mash_prover_suggs
|
blanchet@51979
|
135 |
fun mess_of mash_facts =
|
blanchet@51829
|
136 |
[(mepo_weight, (mepo_facts, [])),
|
blanchet@51979
|
137 |
(mash_weight, (mash_facts, []))]
|
blanchet@51979
|
138 |
fun mesh_of suggs mash_facts =
|
blanchet@51979
|
139 |
get_facts suggs (fn _ =>
|
blanchet@51979
|
140 |
mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
|
blanchet@51980
|
141 |
(mess_of mash_facts))
|
blanchet@51979
|
142 |
val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts
|
blanchet@51979
|
143 |
val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts
|
blanchet@51982
|
144 |
val isar_facts = find_suggs isar_deps
|
blanchet@51574
|
145 |
(* adapted from "mirabelle_sledgehammer.ML" *)
|
blanchet@51968
|
146 |
fun set_file_name method (SOME dir) =
|
blanchet@51574
|
147 |
let
|
blanchet@51574
|
148 |
val prob_prefix =
|
blanchet@51841
|
149 |
"goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^
|
blanchet@51968
|
150 |
method
|
blanchet@51574
|
151 |
in
|
blanchet@51574
|
152 |
Config.put dest_dir dir
|
blanchet@51574
|
153 |
#> Config.put problem_prefix (prob_prefix ^ "__")
|
blanchet@51574
|
154 |
#> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
|
blanchet@51574
|
155 |
end
|
blanchet@51574
|
156 |
| set_file_name _ NONE = I
|
blanchet@51980
|
157 |
fun prove method get facts =
|
blanchet@51968
|
158 |
if not (member (op =) methods method) orelse
|
blanchet@51968
|
159 |
(null facts andalso method <> IsarN) then
|
blanchet@51968
|
160 |
(str_of_method method ^ "Skipped", 0)
|
blanchet@51967
|
161 |
else
|
blanchet@51967
|
162 |
let
|
blanchet@51967
|
163 |
fun nickify ((_, stature), th) =
|
blanchet@51967
|
164 |
((K (encode_str (nickname_of_thm th)), stature), th)
|
blanchet@51967
|
165 |
val facts =
|
blanchet@51967
|
166 |
facts
|
blanchet@51980
|
167 |
|> map (get #> nickify)
|
blanchet@51967
|
168 |
|> maybe_instantiate_inducts ctxt hyp_ts concl_t
|
blanchet@51967
|
169 |
|> take (the max_facts)
|
blanchet@52186
|
170 |
|> map fact_of_raw_fact
|
blanchet@51968
|
171 |
val ctxt = ctxt |> set_file_name method prob_dir_name
|
blanchet@51967
|
172 |
val res as {outcome, ...} =
|
blanchet@51967
|
173 |
run_prover_for_mash ctxt params prover facts goal
|
blanchet@51967
|
174 |
val ok = if is_none outcome then 1 else 0
|
blanchet@51968
|
175 |
in (str_of_result method facts res, ok) end
|
blanchet@51606
|
176 |
val ress =
|
blanchet@51980
|
177 |
[fn () => prove MePoN fst mepo_facts,
|
blanchet@51980
|
178 |
fn () => prove MaSh_IsarN fst mash_isar_facts,
|
blanchet@51980
|
179 |
fn () => prove MaSh_ProverN fst mash_prover_facts,
|
blanchet@51980
|
180 |
fn () => prove MeSh_IsarN I mesh_isar_facts,
|
blanchet@51980
|
181 |
fn () => prove MeSh_ProverN I mesh_prover_facts,
|
blanchet@51980
|
182 |
fn () => prove IsarN I isar_facts]
|
blanchet@51574
|
183 |
|> (* Par_List. *) map (fn f => f ())
|
blanchet@51574
|
184 |
in
|
blanchet@51606
|
185 |
"Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
|
blanchet@51602
|
186 |
|> cat_lines |> print;
|
blanchet@51606
|
187 |
map snd ress
|
blanchet@51574
|
188 |
end
|
blanchet@51574
|
189 |
else
|
blanchet@52210
|
190 |
zeros
|
blanchet@51968
|
191 |
fun total_of method ok n =
|
blanchet@51968
|
192 |
str_of_method method ^ string_of_int ok ^ " (" ^
|
blanchet@51606
|
193 |
Real.fmt (StringCvt.FIX (SOME 1))
|
blanchet@52210
|
194 |
(100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
|
blanchet@51572
|
195 |
val inst_inducts = Config.get ctxt instantiate_inducts
|
blanchet@49260
|
196 |
val options =
|
blanchet@51782
|
197 |
["prover = " ^ prover,
|
blanchet@51782
|
198 |
"max_facts = " ^ string_of_int (the max_facts),
|
blanchet@51782
|
199 |
"slice" |> not slice ? prefix "dont_",
|
blanchet@51782
|
200 |
"type_enc = " ^ the_default "smart" type_enc,
|
blanchet@51782
|
201 |
"lam_trans = " ^ the_default "smart" lam_trans,
|
blanchet@51782
|
202 |
"timeout = " ^ ATP_Util.string_from_time (the_default one_year timeout),
|
blanchet@49256
|
203 |
"instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
|
blanchet@51602
|
204 |
val _ = print " * * *";
|
blanchet@51602
|
205 |
val _ = print ("Options: " ^ commas options);
|
blanchet@51979
|
206 |
val oks = Par_List.map solve_goal (tag_list 1 lines)
|
blanchet@51635
|
207 |
val n = length oks
|
blanchet@51967
|
208 |
val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok,
|
blanchet@51967
|
209 |
isar_ok] =
|
blanchet@52210
|
210 |
if n = 0 then zeros else map Integer.sum (map_transpose I oks)
|
blanchet@49256
|
211 |
in
|
blanchet@49256
|
212 |
["Successes (of " ^ string_of_int n ^ " goals)",
|
blanchet@49394
|
213 |
total_of MePoN mepo_ok n,
|
blanchet@51967
|
214 |
total_of MaSh_IsarN mash_isar_ok n,
|
blanchet@51967
|
215 |
total_of MaSh_ProverN mash_prover_ok n,
|
blanchet@51967
|
216 |
total_of MeSh_IsarN mesh_isar_ok n,
|
blanchet@51967
|
217 |
total_of MeSh_ProverN mesh_prover_ok n,
|
blanchet@49394
|
218 |
total_of IsarN isar_ok n]
|
blanchet@51452
|
219 |
|> cat_lines |> print
|
blanchet@49256
|
220 |
end
|
blanchet@49250
|
221 |
|
blanchet@49249
|
222 |
end;
|