24 val mashN = "MaSh" |
24 val mashN = "MaSh" |
25 val meshN = "Mesh" |
25 val meshN = "Mesh" |
26 |
26 |
27 val max_facts_slack = 2 |
27 val max_facts_slack = 2 |
28 |
28 |
29 val all_names = |
29 fun all_names ctxt prover = |
30 filter_out (is_likely_tautology orf is_too_meta) |
30 filter_out (is_likely_tautology ctxt prover orf is_too_meta) |
31 #> map (rpair () o Thm.get_name_hint) #> Symtab.make |
31 #> map (rpair () o Thm.get_name_hint) #> Symtab.make |
32 |
32 |
33 fun evaluate_mash_suggestions ctxt params thy file_name = |
33 fun evaluate_mash_suggestions ctxt params thy file_name = |
34 let |
34 let |
35 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
35 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = |
36 Sledgehammer_Isar.default_params ctxt [] |
36 Sledgehammer_Isar.default_params ctxt [] |
37 val prover_name = hd provers |
37 val prover = hd provers |
38 val slack_max_facts = max_facts_slack * the max_facts |
38 val slack_max_facts = max_facts_slack * the max_facts |
39 val path = file_name |> Path.explode |
39 val path = file_name |> Path.explode |
40 val lines = path |> File.read_lines |
40 val lines = path |> File.read_lines |
41 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
41 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
42 val facts = all_facts_of thy css_table |
42 val facts = all_facts_of thy css_table |
43 val all_names = all_names (facts |> map snd) |
43 val all_names = all_names ctxt prover (facts |> map snd) |
44 val iter_ok = Unsynchronized.ref 0 |
44 val iter_ok = Unsynchronized.ref 0 |
45 val mash_ok = Unsynchronized.ref 0 |
45 val mash_ok = Unsynchronized.ref 0 |
46 val mesh_ok = Unsynchronized.ref 0 |
46 val mesh_ok = Unsynchronized.ref 0 |
47 val isar_ok = Unsynchronized.ref 0 |
47 val isar_ok = Unsynchronized.ref 0 |
48 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
48 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
78 val isar_deps = isabelle_dependencies_of all_names th |
78 val isar_deps = isabelle_dependencies_of all_names th |
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
80 val isar_facts = suggested_facts isar_deps facts |
80 val isar_facts = suggested_facts isar_deps facts |
81 val iter_facts = |
81 val iter_facts = |
82 Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params |
82 Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params |
83 prover_name slack_max_facts NONE hyp_ts concl_t facts |
83 prover slack_max_facts NONE hyp_ts concl_t facts |
84 val mash_facts = suggested_facts suggs facts |
84 val mash_facts = suggested_facts suggs facts |
85 val mess = [(iter_facts, SOME (length iter_facts)), (mash_facts, NONE)] |
85 val mess = [(iter_facts, SOME (length iter_facts)), (mash_facts, NONE)] |
86 val mesh_facts = mesh_facts slack_max_facts mess |
86 val mesh_facts = mesh_facts slack_max_facts mess |
87 fun prove ok heading facts = |
87 fun prove ok heading facts = |
88 let |
88 let |
89 val facts = |
89 val facts = |
90 facts |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t |
90 facts |
91 |> take (the max_facts) |
91 |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t |
92 val res as {outcome, ...} = run_prover ctxt params facts goal |
92 |> take (the max_facts) |
|
93 val res as {outcome, ...} = run_prover ctxt params prover facts goal |
93 val _ = if is_none outcome then ok := !ok + 1 else () |
94 val _ = if is_none outcome then ok := !ok + 1 else () |
94 in str_of_res heading facts res end |
95 in str_of_res heading facts res end |
95 val iter_s = prove iter_ok iterN iter_facts |
96 val iter_s = prove iter_ok iterN iter_facts |
96 val mash_s = prove mash_ok mashN mash_facts |
97 val mash_s = prove mash_ok mashN mash_facts |
97 val mesh_s = prove mesh_ok meshN mesh_facts |
98 val mesh_s = prove mesh_ok meshN mesh_facts |
105 " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ |
106 " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ |
106 Real.fmt (StringCvt.FIX (SOME 1)) |
107 Real.fmt (StringCvt.FIX (SOME 1)) |
107 (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" |
108 (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" |
108 val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts |
109 val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts |
109 val options = |
110 val options = |
110 [prover_name, string_of_int (the max_facts) ^ " facts", |
111 [prover, string_of_int (the max_facts) ^ " facts", |
111 "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, |
112 "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, |
112 the_default "smart" lam_trans, ATP_Util.string_from_time timeout, |
113 the_default "smart" lam_trans, ATP_Util.string_from_time timeout, |
113 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] |
114 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] |
114 val n = length lines |
115 val n = length lines |
115 in |
116 in |