1 (* Title: HOL/TPTP/mash_export.ML
2 Author: Jasmin Blanchette, TU Muenchen
5 Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer).
8 signature MASH_EXPORT =
10 type params = Sledgehammer_Provers.params
12 val generate_accessibility : theory -> bool -> string -> unit
13 val generate_features :
14 Proof.context -> string -> theory -> bool -> string -> unit
15 val generate_isar_dependencies :
16 theory -> bool -> string -> unit
17 val generate_atp_dependencies :
18 Proof.context -> params -> theory -> bool -> string -> unit
19 val generate_commands : Proof.context -> string -> theory -> string -> unit
20 val generate_mepo_suggestions :
21 Proof.context -> params -> theory -> int -> string -> unit
24 structure MaSh_Export : MASH_EXPORT =
27 open Sledgehammer_Fact
28 open Sledgehammer_MePo
29 open Sledgehammer_MaSh
31 fun thy_map_from_facts ths =
32 ths |> sort (thm_ord o swap o pairself snd)
33 |> map (snd #> `(theory_of_thm #> Context.theory_name))
34 |> AList.coalesce (op =)
35 |> map (apsnd (map nickname_of))
38 Context.theory_name thy = Context.theory_name (theory_of_thm th)
40 fun parent_facts thy thy_map =
43 case AList.lookup (op =) thy_map (Context.theory_name thy) of
44 SOME (last_fact :: _) => insert (op =) last_fact
46 and add_parent thy = fold add_last (Theory.parents_of thy)
47 in add_parent thy [] end
49 val thy_name_of_fact = hd o Long_Name.explode
50 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
53 filter_out is_likely_tautology_or_too_meta
54 #> map (rpair () o nickname_of) #> Symtab.make
56 fun generate_accessibility thy include_thy file_name =
58 val path = file_name |> Path.explode
59 val _ = File.write path ""
60 fun do_fact fact prevs =
62 val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
63 val _ = File.append path s
66 all_facts_of (Proof_Context.init_global thy) Termtab.empty
67 |> not include_thy ? filter_out (has_thy thy o snd)
71 val thy = thy_of_fact thy (hd facts)
72 val parents = parent_facts thy thy_map
73 in fold do_fact facts parents; () end
74 in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
76 fun generate_features ctxt prover thy include_thy file_name =
78 val path = file_name |> Path.explode
79 val _ = File.write path ""
80 val css_table = clasimpset_rule_table_of ctxt
82 all_facts_of (Proof_Context.init_global thy) css_table
83 |> not include_thy ? filter_out (has_thy thy o snd)
84 fun do_fact ((_, stature), th) =
86 val name = nickname_of th
88 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
89 val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
90 in File.append path s end
91 in List.app do_fact facts end
93 fun generate_isar_dependencies thy include_thy file_name =
95 val path = file_name |> Path.explode
96 val _ = File.write path ""
98 all_facts_of (Proof_Context.init_global thy) Termtab.empty
99 |> not include_thy ? filter_out (has_thy thy o snd)
101 val all_names = all_names ths
104 val name = nickname_of th
105 val deps = isar_dependencies_of all_names th |> these
106 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
107 in File.append path s end
108 in List.app do_thm ths end
110 fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy
113 val path = file_name |> Path.explode
114 val _ = File.write path ""
115 val prover = hd provers
117 all_facts_of (Proof_Context.init_global thy) Termtab.empty
118 |> not include_thy ? filter_out (has_thy thy o snd)
119 val ths = facts |> map snd
120 val all_names = all_names ths
123 val name = nickname_of th
125 case atp_dependencies_of ctxt params prover 0 facts all_names th of
127 | NONE => isar_dependencies_of all_names th |> these
128 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
129 in File.append path s end
130 in List.app do_thm ths end
132 fun generate_commands ctxt prover thy file_name =
134 val path = file_name |> Path.explode
135 val _ = File.write path ""
136 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
137 val facts = all_facts_of (Proof_Context.init_global thy) css_table
138 val (new_facts, old_facts) =
139 facts |> List.partition (has_thy thy o snd)
140 |>> sort (thm_ord o pairself snd)
141 val ths = facts |> map snd
142 val all_names = all_names ths
143 fun do_fact ((_, stature), th) prevs =
145 val name = nickname_of th
146 val feats = features_of ctxt prover thy stature [prop_of th]
147 val deps = isar_dependencies_of all_names th |> these
148 val kind = Thm.legacy_get_kind th
149 val core = escape_metas prevs ^ "; " ^ escape_metas feats
150 val query = if kind <> "" then "? " ^ core ^ "\n" else ""
152 "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^
153 escape_metas deps ^ "\n"
154 val _ = File.append path (query ^ update)
156 val thy_map = old_facts |> thy_map_from_facts
157 val parents = parent_facts thy thy_map
158 in fold do_fact new_facts parents; () end
160 fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant
163 val path = file_name |> Path.explode
164 val _ = File.write path ""
165 val prover = hd provers
166 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
167 val facts = all_facts_of (Proof_Context.init_global thy) css_table
168 val (new_facts, old_facts) =
169 facts |> List.partition (has_thy thy o snd)
170 |>> sort (thm_ord o pairself snd)
171 fun do_fact (fact as (_, th)) old_facts =
173 val name = nickname_of th
174 val goal = goal_of_thm thy th
175 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
176 val kind = Thm.legacy_get_kind th
182 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
183 max_relevant NONE hyp_ts concl_t
184 |> map (fn ((name, _), _) => name ())
185 val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
186 in File.append path s end
189 in fact :: old_facts end
190 in fold do_fact new_facts old_facts; () end