21 val generate_isar_commands : |
21 val generate_isar_commands : |
22 Proof.context -> string -> theory list -> string -> unit |
22 Proof.context -> string -> theory list -> string -> unit |
23 val generate_prover_commands : |
23 val generate_prover_commands : |
24 Proof.context -> params -> int * int option -> theory list -> string -> unit |
24 Proof.context -> params -> int * int option -> theory list -> string -> unit |
25 val generate_mepo_suggestions : |
25 val generate_mepo_suggestions : |
26 Proof.context -> params -> theory list -> int -> string -> unit |
26 Proof.context -> params -> int * int option -> theory list -> int -> string |
|
27 -> unit |
27 val generate_mesh_suggestions : int -> string -> string -> string -> unit |
28 val generate_mesh_suggestions : int -> string -> string -> string -> unit |
28 end; |
29 end; |
29 |
30 |
30 structure MaSh_Export : MASH_EXPORT = |
31 structure MaSh_Export : MASH_EXPORT = |
31 struct |
32 struct |
163 generate_isar_or_prover_commands ctxt prover NONE (1, NONE) |
164 generate_isar_or_prover_commands ctxt prover NONE (1, NONE) |
164 |
165 |
165 fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) = |
166 fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) = |
166 generate_isar_or_prover_commands ctxt prover (SOME params) |
167 generate_isar_or_prover_commands ctxt prover (SOME params) |
167 |
168 |
168 fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) thys |
169 fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) |
169 max_suggs file_name = |
170 range thys max_suggs file_name = |
170 let |
171 let |
171 val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover |
172 val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover |
172 val path = file_name |> Path.explode |
173 val path = file_name |> Path.explode |
173 val facts = all_facts ctxt |
174 val facts = all_facts ctxt |
174 val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) |
175 val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) |
175 val name_tabs = build_name_tables nickname_of_thm facts |
176 val name_tabs = build_name_tables nickname_of_thm facts |
176 fun do_fact (j, ((_, th), old_facts)) = |
177 fun do_fact (j, ((_, th), old_facts)) = |
177 let |
178 if in_range range j then |
178 val name = nickname_of_thm th |
179 let |
179 val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) |
180 val name = nickname_of_thm th |
180 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
181 val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) |
181 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
182 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
182 val isar_deps = isar_dependencies_of name_tabs th |
183 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
183 in |
184 val isar_deps = isar_dependencies_of name_tabs th |
184 if is_bad_query ctxt ho_atp th isar_deps then |
185 in |
185 "" |
186 if is_bad_query ctxt ho_atp th isar_deps then |
186 else |
187 "" |
187 let |
188 else |
188 val suggs = |
189 let |
189 old_facts |
190 val suggs = |
190 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover |
191 old_facts |
191 max_suggs NONE hyp_ts concl_t |
192 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover |
192 |> map (nickname_of_thm o snd) |
193 max_suggs NONE hyp_ts concl_t |
193 in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end |
194 |> map (nickname_of_thm o snd) |
194 end |
195 in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end |
|
196 end |
|
197 else |
|
198 "" |
195 fun accum x (yss as ys :: _) = (x :: ys) :: yss |
199 fun accum x (yss as ys :: _) = (x :: ys) :: yss |
196 val old_factss = tl (fold accum new_facts [old_facts]) |
200 val old_factss = tl (fold accum new_facts [old_facts]) |
197 val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ rev old_factss)) |
201 val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ rev old_factss)) |
198 in File.write_list path lines end |
202 in File.write_list path lines end |
199 |
203 |