28 | un accum (c :: cs) = un (c :: accum) cs |
31 | un accum (c :: cs) = un (c :: accum) cs |
29 in un [] o String.explode end |
32 in un [] o String.explode end |
30 |
33 |
31 val of_fact_name = unescape_meta |
34 val of_fact_name = unescape_meta |
32 |
35 |
33 val depN = "Dependencies" |
36 val isaN = "Isabelle" |
34 val mengN = "Meng & Paulson" |
37 val iterN = "Iterative" |
35 val mashN = "MaSh" |
38 val mashN = "MaSh" |
36 val meng_mashN = "M&P+MaSh" |
39 val iter_mashN = "Iter+MaSh" |
37 |
40 |
38 val max_relevant_slack = 2 |
41 val max_relevant_slack = 2 |
39 |
42 |
40 fun import_and_evaluate_mash_suggestions ctxt thy file_name = |
43 fun import_and_evaluate_mash_suggestions ctxt params thy file_name = |
41 let |
44 let |
42 val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} = |
45 val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} = |
43 Sledgehammer_Isar.default_params ctxt [] |
46 Sledgehammer_Isar.default_params ctxt [] |
44 val prover_name = hd provers |
47 val prover_name = hd provers |
45 val path = file_name |> Path.explode |
48 val path = file_name |> Path.explode |
46 val lines = path |> File.read_lines |
49 val lines = path |> File.read_lines |
47 val facts = non_tautological_facts_of thy |
50 val facts = all_non_tautological_facts_of thy |
48 val all_names = facts |> map (Thm.get_name_hint o snd) |
51 val all_names = facts |> map (Thm.get_name_hint o snd) |
49 val meng_ok = Unsynchronized.ref 0 |
52 val iter_ok = Unsynchronized.ref 0 |
50 val mash_ok = Unsynchronized.ref 0 |
53 val mash_ok = Unsynchronized.ref 0 |
51 val meng_mash_ok = Unsynchronized.ref 0 |
54 val iter_mash_ok = Unsynchronized.ref 0 |
52 val dep_ok = Unsynchronized.ref 0 |
55 val isa_ok = Unsynchronized.ref 0 |
53 fun find_sugg facts sugg = |
56 fun find_sugg facts sugg = |
54 find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts |
57 find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts |
55 fun sugg_facts hyp_ts concl_t facts = |
58 fun sugg_facts hyp_ts concl_t facts = |
56 map_filter (find_sugg facts o of_fact_name) |
59 map_filter (find_sugg facts o of_fact_name) |
57 #> take (max_relevant_slack * the max_relevant) |
60 #> take (max_relevant_slack * the max_relevant) |
58 #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t |
61 #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t |
59 #> map (apfst (apfst (fn name => name ()))) |
62 #> map (apfst (apfst (fn name => name ()))) |
60 fun meng_mash_facts fs1 fs2 = |
63 fun iter_mash_facts fs1 fs2 = |
61 let |
64 let |
62 val fact_eq = (op =) o pairself fst |
65 val fact_eq = (op =) o pairself fst |
63 fun score_in f fs = |
66 fun score_in f fs = |
64 case find_index (curry fact_eq f) fs of |
67 case find_index (curry fact_eq f) fs of |
65 ~1 => length fs |
68 ~1 => length fs |
90 (facts |> map (fst o fst) |
93 (facts |> map (fst o fst) |
91 |> take (the max_relevant) |
94 |> take (the max_relevant) |
92 |> tag_list 1 |
95 |> tag_list 1 |
93 |> map index_string |
96 |> map index_string |
94 |> space_implode " ")) |
97 |> space_implode " ")) |
95 fun run_sh ok heading facts goal = |
98 fun prove ok heading facts goal = |
96 let |
99 let |
97 val facts = facts |> take (the max_relevant) |
100 val facts = facts |> take (the max_relevant) |
98 val res as {outcome, ...} = run_sledgehammer ctxt facts goal |
101 val res as {outcome, ...} = run_prover ctxt params facts goal |
99 val _ = if is_none outcome then ok := !ok + 1 else () |
102 val _ = if is_none outcome then ok := !ok + 1 else () |
100 in str_of_res heading facts res end |
103 in str_of_res heading facts res end |
101 fun solve_goal j name suggs = |
104 fun solve_goal j name suggs = |
102 let |
105 let |
103 val name = of_fact_name name |
106 val name = of_fact_name name |
104 val th = |
107 val th = |
105 case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of |
108 case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of |
106 SOME (_, th) => th |
109 SOME (_, th) => th |
107 | NONE => error ("No fact called \"" ^ name ^ "\"") |
110 | NONE => error ("No fact called \"" ^ name ^ "\"") |
108 val deps = dependencies_of all_names th |
111 val isa_deps = isabelle_dependencies_of all_names th |
109 val goal = goal_of_thm thy th |
112 val goal = goal_of_thm thy th |
110 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
113 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
111 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
114 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
112 val deps_facts = sugg_facts hyp_ts concl_t facts deps |
115 val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps |
113 val meng_facts = |
116 val iter_facts = |
114 meng_paulson_facts ctxt (max_relevant_slack * the max_relevant) goal |
117 iter_facts ctxt params (max_relevant_slack * the max_relevant) goal |
115 facts |
118 facts |
116 val mash_facts = sugg_facts hyp_ts concl_t facts suggs |
119 val mash_facts = sugg_facts hyp_ts concl_t facts suggs |
117 val meng_mash_facts = meng_mash_facts meng_facts mash_facts |
120 val iter_mash_facts = iter_mash_facts iter_facts mash_facts |
118 val meng_s = run_sh meng_ok mengN meng_facts goal |
121 val iter_s = prove iter_ok iterN iter_facts goal |
119 val mash_s = run_sh mash_ok mashN mash_facts goal |
122 val mash_s = prove mash_ok mashN mash_facts goal |
120 val meng_mash_s = run_sh meng_mash_ok meng_mashN meng_mash_facts goal |
123 val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal |
121 val dep_s = run_sh dep_ok depN deps_facts goal |
124 val isa_s = prove isa_ok isaN isa_facts goal |
122 in |
125 in |
123 ["Goal " ^ string_of_int j ^ ": " ^ name, meng_s, mash_s, meng_mash_s, |
126 ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, iter_mash_s, |
124 dep_s] |
127 isa_s] |
125 |> cat_lines |> tracing |
128 |> cat_lines |> tracing |
126 end |
129 end |
127 val explode_suggs = space_explode " " #> filter_out (curry (op =) "") |
130 val explode_suggs = space_explode " " #> filter_out (curry (op =) "") |
128 fun do_line (j, line) = |
131 fun do_line (j, line) = |
129 case space_explode ":" line of |
132 case space_explode ":" line of |
143 in |
146 in |
144 tracing " * * *"; |
147 tracing " * * *"; |
145 tracing ("Options: " ^ commas options); |
148 tracing ("Options: " ^ commas options); |
146 List.app do_line (tag_list 1 lines); |
149 List.app do_line (tag_list 1 lines); |
147 ["Successes (of " ^ string_of_int n ^ " goals)", |
150 ["Successes (of " ^ string_of_int n ^ " goals)", |
148 total_of mengN meng_ok n, |
151 total_of iterN iter_ok n, |
149 total_of mashN mash_ok n, |
152 total_of mashN mash_ok n, |
150 total_of meng_mashN meng_mash_ok n, |
153 total_of iter_mashN iter_mash_ok n, |
151 total_of depN dep_ok n] |
154 total_of isaN isa_ok n] |
152 |> cat_lines |> tracing |
155 |> cat_lines |> tracing |
153 end |
156 end |
154 |
157 |
155 end; |
158 end; |