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 : Proof.context -> theory -> bool -> string -> unit
13 val generate_features :
14 Proof.context -> string -> theory -> bool -> string -> unit
15 val generate_isar_dependencies :
16 Proof.context -> theory -> bool -> string -> unit
17 val generate_atp_dependencies :
18 Proof.context -> params -> theory -> bool -> string -> unit
19 val generate_commands : Proof.context -> params -> 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 all_non_technical_facts ctxt thy =
41 let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
42 all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
43 |> filter_out (is_thm_technical o snd)
46 fun parent_facts thy thy_map =
49 case AList.lookup (op =) thy_map (Context.theory_name thy) of
50 SOME (last_fact :: _) => insert (op =) last_fact
52 and add_parent thy = fold add_last (Theory.parents_of thy)
53 in add_parent thy [] end
55 val thy_name_of_fact = hd o Long_Name.explode
56 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
58 val all_names = map (rpair () o nickname_of) #> Symtab.make
60 fun smart_dependencies_of ctxt params prover facts all_names th =
61 case atp_dependencies_of ctxt params prover 0 facts all_names th of
63 | NONE => isar_dependencies_of all_names th |> these
65 fun generate_accessibility ctxt thy include_thy file_name =
67 val path = file_name |> Path.explode
68 val _ = File.write path ""
69 fun do_fact fact prevs =
71 val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
72 val _ = File.append path s
75 all_non_technical_facts ctxt thy
76 |> not include_thy ? filter_out (has_thy thy o snd)
80 val thy = thy_of_fact thy (hd facts)
81 val parents = parent_facts thy thy_map
82 in fold_rev do_fact facts parents; () end
83 in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
85 fun generate_features ctxt prover thy include_thy file_name =
87 val path = file_name |> Path.explode
88 val _ = File.write path ""
90 all_non_technical_facts ctxt thy
91 |> not include_thy ? filter_out (has_thy thy o snd)
92 fun do_fact ((_, stature), th) =
94 val name = nickname_of th
96 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
97 val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
98 in File.append path s end
99 in List.app do_fact facts end
101 fun generate_isar_dependencies ctxt thy include_thy file_name =
103 val path = file_name |> Path.explode
104 val _ = File.write path ""
106 all_non_technical_facts ctxt thy
107 |> not include_thy ? filter_out (has_thy thy o snd)
109 val all_names = all_names ths
112 val name = nickname_of th
113 val deps = isar_dependencies_of all_names th |> these
114 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
115 in File.append path s end
116 in List.app do_thm ths end
118 fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy
121 val path = file_name |> Path.explode
122 val _ = File.write path ""
123 val prover = hd provers
125 all_non_technical_facts ctxt thy
126 |> not include_thy ? filter_out (has_thy thy o snd)
127 val ths = facts |> map snd
128 val all_names = all_names ths
131 val name = nickname_of th
132 val deps = smart_dependencies_of ctxt params prover facts all_names th
133 val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
134 in File.append path s end
135 in List.app do_thm ths end
137 fun generate_commands ctxt (params as {provers, ...}) thy file_name =
139 val path = file_name |> Path.explode
140 val _ = File.write path ""
141 val prover = hd provers
142 val facts = all_non_technical_facts ctxt thy
143 val (new_facts, old_facts) =
144 facts |> List.partition (has_thy thy o snd)
145 |>> sort (thm_ord o pairself snd)
146 val ths = facts |> map snd
147 val all_names = all_names ths
148 fun do_fact ((_, stature), th) prevs =
150 val name = nickname_of th
151 val feats = features_of ctxt prover thy stature [prop_of th]
152 val deps = smart_dependencies_of ctxt params prover facts all_names th
153 val kind = Thm.legacy_get_kind th
155 escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
157 val query = if kind <> "" then "? " ^ core ^ "\n" else ""
158 val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
159 val _ = File.append path (query ^ update)
161 val thy_map = old_facts |> thy_map_from_facts
162 val parents = parent_facts thy thy_map
163 in fold do_fact new_facts parents; () end
165 fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant
168 val path = file_name |> Path.explode
169 val _ = File.write path ""
170 val prover = hd provers
171 val facts = all_non_technical_facts ctxt thy
172 val (new_facts, old_facts) =
173 facts |> List.partition (has_thy thy o snd)
174 |>> sort (thm_ord o pairself snd)
175 fun do_fact (fact as (_, th)) old_facts =
177 val name = nickname_of th
178 val goal = goal_of_thm thy th
179 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
180 val kind = Thm.legacy_get_kind th
186 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
187 max_relevant NONE hyp_ts concl_t
188 |> map (fn ((name, _), _) => name ())
189 val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
190 in File.append path s end
193 in fact :: old_facts end
194 in fold do_fact new_facts old_facts; () end