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_iter_suggestions :
21 Proof.context -> params -> theory -> int -> string -> unit
24 structure MaSh_Export : MASH_EXPORT =
27 open Sledgehammer_Fact
28 open Sledgehammer_Filter_Iter
29 open Sledgehammer_Filter_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 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 thy css_table
83 |> not include_thy ? filter_out (has_thy thy o snd)
84 fun do_fact ((_, (_, status)), th) =
86 val name = nickname_of th
88 features_of ctxt prover (theory_of_thm th) status [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 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 = isabelle_dependencies_of all_names th
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, max_facts, ...}) thy
111 include_thy file_name =
113 val path = file_name |> Path.explode
114 val _ = File.write path ""
115 val prover = hd provers
117 all_facts_of 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
121 fun is_dep dep (_, th) = nickname_of th = dep
122 fun add_isar_dep facts dep accum =
123 if exists (is_dep dep) accum then
125 else case find_first (is_dep dep) facts of
126 SOME ((name, status), th) => accum @ [((name, status), th)]
127 | NONE => accum (* shouldn't happen *)
128 fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
131 val name = nickname_of th
132 val goal = goal_of_thm thy th
133 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
135 case isabelle_dependencies_of all_names th of
137 | isar_dep as [_] => isar_dep (* can hardly beat that *)
141 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
143 facts |> iterative_relevant_facts ctxt params prover
144 (the max_facts) NONE hyp_ts concl_t
145 |> fold (add_isar_dep facts) isar_deps
148 case run_prover_for_mash ctxt params prover facts goal of
149 {outcome = NONE, used_facts, ...} =>
150 used_facts |> map fst |> sort string_ord
153 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
154 in File.append path s end
155 in List.app do_thm ths end
157 fun generate_commands ctxt prover thy file_name =
159 val path = file_name |> Path.explode
160 val _ = File.write path ""
161 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
162 val facts = all_facts_of thy css_table
163 val (new_facts, old_facts) =
164 facts |> List.partition (has_thy thy o snd)
165 |>> sort (thm_ord o pairself snd)
166 val ths = facts |> map snd
167 val all_names = all_names ths
168 fun do_fact ((_, (_, status)), th) prevs =
170 val name = nickname_of th
171 val feats = features_of ctxt prover thy status [prop_of th]
172 val deps = isabelle_dependencies_of all_names th
173 val kind = Thm.legacy_get_kind th
174 val core = escape_metas prevs ^ "; " ^ escape_metas feats
175 val query = if kind <> "" then "? " ^ core ^ "\n" else ""
177 "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^
178 escape_metas deps ^ "\n"
179 val _ = File.append path (query ^ update)
181 val thy_map = old_facts |> thy_map_from_facts
182 val parents = parent_facts thy thy_map
183 in fold do_fact new_facts parents; () end
185 fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
188 val path = file_name |> Path.explode
189 val _ = File.write path ""
190 val prover = hd provers
191 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
192 val facts = all_facts_of thy css_table
193 val (new_facts, old_facts) =
194 facts |> List.partition (has_thy thy o snd)
195 |>> sort (thm_ord o pairself snd)
196 fun do_fact (fact as (_, th)) old_facts =
198 val name = nickname_of th
199 val goal = goal_of_thm thy th
200 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
201 val kind = Thm.legacy_get_kind th
207 |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
208 prover max_relevant NONE hyp_ts concl_t
209 |> map (fn ((name, _), _) => name ())
211 val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
212 in File.append path s end
215 in fact :: old_facts end
216 in fold do_fact new_facts old_facts; () end