39 |
39 |
40 fun in_range (from, to) j = |
40 fun in_range (from, to) j = |
41 j >= from andalso (to = NONE orelse j <= the to) |
41 j >= from andalso (to = NONE orelse j <= the to) |
42 |
42 |
43 fun evaluate_mash_suggestions ctxt params range methods prob_dir_name |
43 fun evaluate_mash_suggestions ctxt params range methods prob_dir_name |
44 isar_sugg_file_name prover_sugg_file_name report_file_name = |
44 mepo_file_name mash_isar_file_name mash_prover_file_name |
|
45 mesh_isar_file_name mesh_prover_file_name report_file_name = |
45 let |
46 let |
46 val report_path = report_file_name |> Path.explode |
47 val report_path = report_file_name |> Path.explode |
47 val _ = File.write report_path "" |
48 val _ = File.write report_path "" |
48 fun print s = File.append report_path (s ^ "\n") |
49 fun print s = File.append report_path (s ^ "\n") |
49 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
50 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
50 default_params ctxt [] |
51 default_params ctxt [] |
51 val prover = hd provers |
52 val prover = hd provers |
52 val slack_max_facts = generous_max_facts (the max_facts) |
53 val slack_max_facts = generous_max_facts (the max_facts) |
53 val mash_isar_lines = Path.explode isar_sugg_file_name |> File.read_lines |
54 val lines_of = Path.explode #> try File.read_lines #> these |
54 val mash_prover_lines = |
55 val file_names = |
55 case Path.explode prover_sugg_file_name |> try File.read_lines of |
56 [mepo_file_name, mash_isar_file_name, mash_prover_file_name, |
56 NONE => replicate (length mash_isar_lines) "" |
57 mesh_isar_file_name, mesh_prover_file_name] |
57 | SOME lines => lines |
58 val lines as [mepo_lines, mash_isar_lines, mash_prover_lines, |
58 val mash_lines = mash_isar_lines ~~ mash_prover_lines |
59 mesh_isar_lines, mesh_prover_lines] = |
|
60 map lines_of file_names |
|
61 val num_lines = fold (Integer.max o length) lines 0 |
|
62 fun pad lines = lines @ replicate (num_lines - length lines) "" |
|
63 val lines = |
|
64 pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~ |
|
65 pad mesh_isar_lines ~~ pad mesh_prover_lines |
59 val css = clasimpset_rule_table_of ctxt |
66 val css = clasimpset_rule_table_of ctxt |
60 val facts = all_facts ctxt true false Symtab.empty [] [] css |
67 val facts = all_facts ctxt true false Symtab.empty [] [] css |
61 val name_tabs = build_name_tables nickname_of_thm facts |
68 val name_tabs = build_name_tables nickname_of_thm facts |
62 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
69 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
63 fun index_str (j, s) = s ^ "@" ^ string_of_int j |
70 fun index_str (j, s) = s ^ "@" ^ string_of_int j |
80 "Failure: " ^ |
87 "Failure: " ^ |
81 (facts |> take (the max_facts) |> tag_list 1 |
88 (facts |> take (the max_facts) |> tag_list 1 |
82 |> map index_str |
89 |> map index_str |
83 |> space_implode " ")) |
90 |> space_implode " ")) |
84 end |
91 end |
85 fun solve_goal (j, (mash_isar_line, mash_prover_line)) = |
92 fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line), |
|
93 mesh_isar_line), mesh_prover_line)) = |
86 if in_range range j then |
94 if in_range range j then |
87 let |
95 let |
88 val (name, mash_isar_suggs) = extract_suggestions mash_isar_line |
96 val (name1, mepo_suggs) = extract_suggestions mepo_line |
89 val (_, mash_prover_suggs) = extract_suggestions mash_prover_line |
97 val (name2, mash_isar_suggs) = extract_suggestions mash_isar_line |
|
98 val (name3, mash_prover_suggs) = extract_suggestions mash_prover_line |
|
99 val (name4, mesh_isar_suggs) = extract_suggestions mesh_isar_line |
|
100 val (name5, mesh_prover_suggs) = extract_suggestions mesh_prover_line |
|
101 val [name] = |
|
102 [name1, name2, name3, name4, name5] |
|
103 |> filter (curry (op <>) "") |> distinct (op =) |
|
104 handle General.Match => error "Input files out of sync." |
90 val th = |
105 val th = |
91 case find_first (fn (_, th) => nickname_of_thm th = name) facts of |
106 case find_first (fn (_, th) => nickname_of_thm th = name) facts of |
92 SOME (_, th) => th |
107 SOME (_, th) => th |
93 | NONE => error ("No fact called \"" ^ name ^ "\".") |
108 | NONE => error ("No fact called \"" ^ name ^ "\".") |
94 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
109 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
95 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
110 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
96 val isar_deps = isar_dependencies_of name_tabs th |
111 val isar_deps = isar_dependencies_of name_tabs th |
97 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
112 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
|
113 fun get_facts [] compute = compute facts |
|
114 | get_facts suggs _ = find_suggested_facts suggs facts |
98 val mepo_facts = |
115 val mepo_facts = |
99 mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts |
116 get_facts mepo_suggs (fn _ => |
100 concl_t facts |
117 mepo_suggested_facts ctxt params prover slack_max_facts NONE |
101 |> weight_mepo_facts |
118 hyp_ts concl_t facts |
|
119 |> weight_mepo_facts) |
102 fun mash_of suggs = |
120 fun mash_of suggs = |
103 find_mash_suggestions slack_max_facts suggs facts [] [] |
121 get_facts suggs (fn _ => |
104 |>> weight_mash_facts |
122 find_mash_suggestions slack_max_facts suggs facts [] [] |
105 val (mash_isar_facts, mash_isar_unks) = mash_of mash_isar_suggs |
123 |> fst |> weight_mash_facts) |
106 val (mash_prover_facts, mash_prover_unks) = mash_of mash_prover_suggs |
124 val mash_isar_facts = mash_of mash_isar_suggs |
107 fun mess_of mash_facts mash_unks = |
125 val mash_prover_facts = mash_of mash_prover_suggs |
|
126 fun mess_of mash_facts = |
108 [(mepo_weight, (mepo_facts, [])), |
127 [(mepo_weight, (mepo_facts, [])), |
109 (mash_weight, (mash_facts, mash_unks))] |
128 (mash_weight, (mash_facts, []))] |
110 fun mesh_of [] _ = [] |
129 fun mesh_of suggs mash_facts = |
111 | mesh_of mash_facts mash_unks = |
130 get_facts suggs (fn _ => |
112 mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts |
131 mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts |
113 (mess_of mash_facts mash_unks) |
132 (mess_of mash_facts) |
114 val mesh_isar_facts = mesh_of mash_isar_facts mash_isar_unks |
133 |> map (rpair 1.0)) |
115 val mesh_prover_facts = mesh_of mash_prover_facts mash_prover_unks |
134 val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts |
|
135 val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts |
116 val isar_facts = |
136 val isar_facts = |
117 find_suggested_facts (map (rpair 1.0) isar_deps) facts |
137 find_suggested_facts (map (rpair 1.0) isar_deps) facts |
118 (* adapted from "mirabelle_sledgehammer.ML" *) |
138 (* adapted from "mirabelle_sledgehammer.ML" *) |
119 fun set_file_name method (SOME dir) = |
139 fun set_file_name method (SOME dir) = |
120 let |
140 let |
125 Config.put dest_dir dir |
145 Config.put dest_dir dir |
126 #> Config.put problem_prefix (prob_prefix ^ "__") |
146 #> Config.put problem_prefix (prob_prefix ^ "__") |
127 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) |
147 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) |
128 end |
148 end |
129 | set_file_name _ NONE = I |
149 | set_file_name _ NONE = I |
130 fun prove method get facts = |
150 fun prove method facts = |
131 if not (member (op =) methods method) orelse |
151 if not (member (op =) methods method) orelse |
132 (null facts andalso method <> IsarN) then |
152 (null facts andalso method <> IsarN) then |
133 (str_of_method method ^ "Skipped", 0) |
153 (str_of_method method ^ "Skipped", 0) |
134 else |
154 else |
135 let |
155 let |
136 fun nickify ((_, stature), th) = |
156 fun nickify ((_, stature), th) = |
137 ((K (encode_str (nickname_of_thm th)), stature), th) |
157 ((K (encode_str (nickname_of_thm th)), stature), th) |
138 val facts = |
158 val facts = |
139 facts |
159 facts |
140 |> map (get #> nickify) |
160 |> map (fst #> nickify) |
141 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
161 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
142 |> take (the max_facts) |
162 |> take (the max_facts) |
143 val ctxt = ctxt |> set_file_name method prob_dir_name |
163 val ctxt = ctxt |> set_file_name method prob_dir_name |
144 val res as {outcome, ...} = |
164 val res as {outcome, ...} = |
145 run_prover_for_mash ctxt params prover facts goal |
165 run_prover_for_mash ctxt params prover facts goal |
146 val ok = if is_none outcome then 1 else 0 |
166 val ok = if is_none outcome then 1 else 0 |
147 in (str_of_result method facts res, ok) end |
167 in (str_of_result method facts res, ok) end |
148 val ress = |
168 val ress = |
149 [fn () => prove MePoN fst mepo_facts, |
169 [fn () => prove MePoN mepo_facts, |
150 fn () => prove MaSh_IsarN fst mash_isar_facts, |
170 fn () => prove MaSh_IsarN mash_isar_facts, |
151 fn () => prove MaSh_ProverN fst mash_prover_facts, |
171 fn () => prove MaSh_ProverN mash_prover_facts, |
152 fn () => prove MeSh_IsarN I mesh_isar_facts, |
172 fn () => prove MeSh_IsarN mesh_isar_facts, |
153 fn () => prove MeSh_ProverN I mesh_prover_facts, |
173 fn () => prove MeSh_ProverN mesh_prover_facts, |
154 fn () => prove IsarN fst isar_facts] |
174 fn () => prove IsarN isar_facts] |
155 |> (* Par_List. *) map (fn f => f ()) |
175 |> (* Par_List. *) map (fn f => f ()) |
156 in |
176 in |
157 "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress |
177 "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress |
158 |> cat_lines |> print; |
178 |> cat_lines |> print; |
159 map snd ress |
179 map snd ress |
173 "lam_trans = " ^ the_default "smart" lam_trans, |
193 "lam_trans = " ^ the_default "smart" lam_trans, |
174 "timeout = " ^ ATP_Util.string_from_time (the_default one_year timeout), |
194 "timeout = " ^ ATP_Util.string_from_time (the_default one_year timeout), |
175 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] |
195 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] |
176 val _ = print " * * *"; |
196 val _ = print " * * *"; |
177 val _ = print ("Options: " ^ commas options); |
197 val _ = print ("Options: " ^ commas options); |
178 val oks = Par_List.map solve_goal (tag_list 1 mash_lines) |
198 val oks = Par_List.map solve_goal (tag_list 1 lines) |
179 val n = length oks |
199 val n = length oks |
180 val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok, |
200 val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok, |
181 isar_ok] = |
201 isar_ok] = |
182 map Integer.sum (map_transpose I oks) |
202 map Integer.sum (map_transpose I oks) |
183 in |
203 in |