24 val MeshN = "Mesh" |
24 val MeshN = "Mesh" |
25 val IsarN = "Isar" |
25 val IsarN = "Isar" |
26 |
26 |
27 val all_names = map (rpair () o nickname_of) #> Symtab.make |
27 val all_names = map (rpair () o nickname_of) #> Symtab.make |
28 |
28 |
29 fun evaluate_mash_suggestions ctxt params sugg_file_name out_file_name = |
29 fun evaluate_mash_suggestions ctxt params prob_dir_name sugg_file_name |
|
30 report_file_name = |
30 let |
31 let |
31 val out_path = out_file_name |> Path.explode |
32 val report_path = report_file_name |> Path.explode |
32 val _ = File.write out_path "" |
33 val _ = File.write report_path "" |
33 fun print s = (tracing s; File.append out_path (s ^ "\n")) |
34 fun print s = (tracing s; File.append report_path (s ^ "\n")) |
34 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
35 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
35 Sledgehammer_Isar.default_params ctxt [] |
36 Sledgehammer_Isar.default_params ctxt [] |
36 val prover = hd provers |
37 val prover = hd provers |
37 val slack_max_facts = generous_max_facts (the max_facts) |
38 val slack_max_facts = generous_max_facts (the max_facts) |
38 val sugg_path = sugg_file_name |> Path.explode |
39 val sugg_path = sugg_file_name |> Path.explode |
85 find_mash_suggestions slack_max_facts suggs facts [] [] |
86 find_mash_suggestions slack_max_facts suggs facts [] [] |
86 |>> weight_mash_facts |
87 |>> weight_mash_facts |
87 val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] |
88 val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] |
88 val mesh_facts = mesh_facts slack_max_facts mess |
89 val mesh_facts = mesh_facts slack_max_facts mess |
89 val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts |
90 val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts |
|
91 (* adapted from "mirabelle_sledgehammer.ML" *) |
|
92 fun set_file_name heading (SOME dir) = |
|
93 Config.put Sledgehammer_Provers.dest_dir dir |
|
94 #> Config.put Sledgehammer_Provers.problem_prefix |
|
95 ("goal_" ^ string_of_int j ^ "_" ^ heading ^ "__") |
|
96 #> Config.put SMT_Config.debug_files |
|
97 (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_" |
|
98 ^ serial_string ()) |
|
99 | set_file_name _ NONE = I |
90 fun prove ok heading get facts = |
100 fun prove ok heading get facts = |
91 let |
101 let |
92 val facts = |
102 val facts = |
93 facts |> map get |
103 facts |> map get |
94 |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts |
104 |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts |
95 concl_t |
105 concl_t |
96 |> take (the max_facts) |
106 |> take (the max_facts) |
|
107 val ctxt = ctxt |> set_file_name heading prob_dir_name |
97 val res as {outcome, ...} = |
108 val res as {outcome, ...} = |
98 run_prover_for_mash ctxt params prover facts goal |
109 run_prover_for_mash ctxt params prover facts goal |
99 val _ = if is_none outcome then ok := !ok + 1 else () |
110 val _ = if is_none outcome then ok := !ok + 1 else () |
100 in str_of_res heading facts res end |
111 in str_of_res heading facts res end |
101 val [mepo_s, mash_s, mesh_s, isar_s] = |
112 val [mepo_s, mash_s, mesh_s, isar_s] = |