blanchet@49249
|
1 |
(* Title: HOL/TPTP/mash_export.ML
|
blanchet@49249
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@49249
|
3 |
Copyright 2012
|
blanchet@49249
|
4 |
|
blanchet@49249
|
5 |
Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer).
|
blanchet@49249
|
6 |
*)
|
blanchet@49249
|
7 |
|
blanchet@49249
|
8 |
signature MASH_EXPORT =
|
blanchet@49249
|
9 |
sig
|
blanchet@49266
|
10 |
type params = Sledgehammer_Provers.params
|
blanchet@49250
|
11 |
|
blanchet@49319
|
12 |
val generate_accessibility : theory -> bool -> string -> unit
|
blanchet@49333
|
13 |
val generate_features :
|
blanchet@49333
|
14 |
Proof.context -> string -> theory -> bool -> string -> unit
|
blanchet@49348
|
15 |
val generate_isar_dependencies :
|
blanchet@49339
|
16 |
theory -> bool -> string -> unit
|
blanchet@49348
|
17 |
val generate_atp_dependencies :
|
blanchet@49319
|
18 |
Proof.context -> params -> theory -> bool -> string -> unit
|
blanchet@49333
|
19 |
val generate_commands : Proof.context -> string -> theory -> string -> unit
|
blanchet@49394
|
20 |
val generate_mepo_suggestions :
|
blanchet@49266
|
21 |
Proof.context -> params -> theory -> int -> string -> unit
|
blanchet@49249
|
22 |
end;
|
blanchet@49249
|
23 |
|
blanchet@49249
|
24 |
structure MaSh_Export : MASH_EXPORT =
|
blanchet@49249
|
25 |
struct
|
blanchet@49249
|
26 |
|
blanchet@49319
|
27 |
open Sledgehammer_Fact
|
blanchet@49396
|
28 |
open Sledgehammer_MePo
|
blanchet@49396
|
29 |
open Sledgehammer_MaSh
|
blanchet@49260
|
30 |
|
blanchet@49331
|
31 |
fun thy_map_from_facts ths =
|
blanchet@49331
|
32 |
ths |> sort (thm_ord o swap o pairself snd)
|
blanchet@49331
|
33 |
|> map (snd #> `(theory_of_thm #> Context.theory_name))
|
blanchet@49331
|
34 |
|> AList.coalesce (op =)
|
blanchet@49393
|
35 |
|> map (apsnd (map nickname_of))
|
blanchet@49331
|
36 |
|
blanchet@49331
|
37 |
fun has_thy thy th =
|
blanchet@49331
|
38 |
Context.theory_name thy = Context.theory_name (theory_of_thm th)
|
blanchet@49331
|
39 |
|
blanchet@49331
|
40 |
fun parent_facts thy thy_map =
|
blanchet@49331
|
41 |
let
|
blanchet@49331
|
42 |
fun add_last thy =
|
blanchet@49331
|
43 |
case AList.lookup (op =) thy_map (Context.theory_name thy) of
|
blanchet@49331
|
44 |
SOME (last_fact :: _) => insert (op =) last_fact
|
blanchet@49331
|
45 |
| _ => add_parent thy
|
blanchet@49331
|
46 |
and add_parent thy = fold add_last (Theory.parents_of thy)
|
blanchet@49331
|
47 |
in add_parent thy [] end
|
blanchet@49331
|
48 |
|
blanchet@49331
|
49 |
val thy_name_of_fact = hd o Long_Name.explode
|
blanchet@49319
|
50 |
fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
|
blanchet@49319
|
51 |
|
blanchet@49339
|
52 |
val all_names =
|
blanchet@49348
|
53 |
filter_out is_likely_tautology_or_too_meta
|
blanchet@49393
|
54 |
#> map (rpair () o nickname_of) #> Symtab.make
|
blanchet@49331
|
55 |
|
blanchet@49319
|
56 |
fun generate_accessibility thy include_thy file_name =
|
blanchet@49319
|
57 |
let
|
blanchet@49319
|
58 |
val path = file_name |> Path.explode
|
blanchet@49319
|
59 |
val _ = File.write path ""
|
blanchet@49319
|
60 |
fun do_fact fact prevs =
|
blanchet@49319
|
61 |
let
|
blanchet@49319
|
62 |
val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
|
blanchet@49319
|
63 |
val _ = File.append path s
|
blanchet@49319
|
64 |
in [fact] end
|
blanchet@49330
|
65 |
val thy_map =
|
blanchet@49330
|
66 |
all_facts_of thy Termtab.empty
|
blanchet@49319
|
67 |
|> not include_thy ? filter_out (has_thy thy o snd)
|
blanchet@49330
|
68 |
|> thy_map_from_facts
|
blanchet@49319
|
69 |
fun do_thy facts =
|
blanchet@49319
|
70 |
let
|
blanchet@49319
|
71 |
val thy = thy_of_fact thy (hd facts)
|
blanchet@49330
|
72 |
val parents = parent_facts thy thy_map
|
blanchet@49319
|
73 |
in fold do_fact facts parents; () end
|
blanchet@49348
|
74 |
in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
|
blanchet@49319
|
75 |
|
blanchet@49333
|
76 |
fun generate_features ctxt prover thy include_thy file_name =
|
blanchet@49319
|
77 |
let
|
blanchet@49319
|
78 |
val path = file_name |> Path.explode
|
blanchet@49319
|
79 |
val _ = File.write path ""
|
blanchet@49319
|
80 |
val css_table = clasimpset_rule_table_of ctxt
|
blanchet@49319
|
81 |
val facts =
|
blanchet@49330
|
82 |
all_facts_of thy css_table
|
blanchet@49319
|
83 |
|> not include_thy ? filter_out (has_thy thy o snd)
|
blanchet@49400
|
84 |
fun do_fact ((_, stature), th) =
|
blanchet@49319
|
85 |
let
|
blanchet@49393
|
86 |
val name = nickname_of th
|
blanchet@49333
|
87 |
val feats =
|
blanchet@49400
|
88 |
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
|
blanchet@49319
|
89 |
val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
|
blanchet@49319
|
90 |
in File.append path s end
|
blanchet@49319
|
91 |
in List.app do_fact facts end
|
blanchet@49319
|
92 |
|
blanchet@49348
|
93 |
fun generate_isar_dependencies thy include_thy file_name =
|
blanchet@49319
|
94 |
let
|
blanchet@49319
|
95 |
val path = file_name |> Path.explode
|
blanchet@49319
|
96 |
val _ = File.write path ""
|
blanchet@49319
|
97 |
val ths =
|
blanchet@49330
|
98 |
all_facts_of thy Termtab.empty
|
blanchet@49319
|
99 |
|> not include_thy ? filter_out (has_thy thy o snd)
|
blanchet@49319
|
100 |
|> map snd
|
blanchet@49339
|
101 |
val all_names = all_names ths
|
blanchet@49319
|
102 |
fun do_thm th =
|
blanchet@49319
|
103 |
let
|
blanchet@49393
|
104 |
val name = nickname_of th
|
blanchet@49407
|
105 |
val deps = isar_dependencies_of all_names th
|
blanchet@49319
|
106 |
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
|
blanchet@49319
|
107 |
in File.append path s end
|
blanchet@49319
|
108 |
in List.app do_thm ths end
|
blanchet@49319
|
109 |
|
blanchet@49407
|
110 |
fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy
|
blanchet@49407
|
111 |
file_name =
|
blanchet@49319
|
112 |
let
|
blanchet@49319
|
113 |
val path = file_name |> Path.explode
|
blanchet@49319
|
114 |
val _ = File.write path ""
|
blanchet@49333
|
115 |
val prover = hd provers
|
blanchet@49319
|
116 |
val facts =
|
blanchet@49330
|
117 |
all_facts_of thy Termtab.empty
|
blanchet@49319
|
118 |
|> not include_thy ? filter_out (has_thy thy o snd)
|
blanchet@49319
|
119 |
val ths = facts |> map snd
|
blanchet@49339
|
120 |
val all_names = all_names ths
|
blanchet@49319
|
121 |
fun do_thm th =
|
blanchet@49319
|
122 |
let
|
blanchet@49393
|
123 |
val name = nickname_of th
|
blanchet@49319
|
124 |
val deps =
|
blanchet@49407
|
125 |
atp_dependencies_of ctxt params prover false facts all_names th
|
blanchet@49319
|
126 |
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
|
blanchet@49319
|
127 |
in File.append path s end
|
blanchet@49319
|
128 |
in List.app do_thm ths end
|
blanchet@49319
|
129 |
|
blanchet@49333
|
130 |
fun generate_commands ctxt prover thy file_name =
|
blanchet@49249
|
131 |
let
|
blanchet@49249
|
132 |
val path = file_name |> Path.explode
|
blanchet@49249
|
133 |
val _ = File.write path ""
|
blanchet@49314
|
134 |
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
|
blanchet@49330
|
135 |
val facts = all_facts_of thy css_table
|
blanchet@49249
|
136 |
val (new_facts, old_facts) =
|
blanchet@49249
|
137 |
facts |> List.partition (has_thy thy o snd)
|
blanchet@49249
|
138 |
|>> sort (thm_ord o pairself snd)
|
blanchet@49249
|
139 |
val ths = facts |> map snd
|
blanchet@49339
|
140 |
val all_names = all_names ths
|
blanchet@49400
|
141 |
fun do_fact ((_, stature), th) prevs =
|
blanchet@49249
|
142 |
let
|
blanchet@49393
|
143 |
val name = nickname_of th
|
blanchet@49400
|
144 |
val feats = features_of ctxt prover thy stature [prop_of th]
|
blanchet@49407
|
145 |
val deps = isar_dependencies_of all_names th
|
blanchet@49249
|
146 |
val kind = Thm.legacy_get_kind th
|
blanchet@49319
|
147 |
val core = escape_metas prevs ^ "; " ^ escape_metas feats
|
blanchet@49249
|
148 |
val query = if kind <> "" then "? " ^ core ^ "\n" else ""
|
blanchet@49315
|
149 |
val update =
|
blanchet@49318
|
150 |
"! " ^ escape_meta name ^ ": " ^ core ^ "; " ^
|
blanchet@49319
|
151 |
escape_metas deps ^ "\n"
|
blanchet@49249
|
152 |
val _ = File.append path (query ^ update)
|
blanchet@49249
|
153 |
in [name] end
|
blanchet@49330
|
154 |
val thy_map = old_facts |> thy_map_from_facts
|
blanchet@49330
|
155 |
val parents = parent_facts thy thy_map
|
blanchet@49254
|
156 |
in fold do_fact new_facts parents; () end
|
blanchet@49254
|
157 |
|
blanchet@49394
|
158 |
fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant
|
blanchet@49307
|
159 |
file_name =
|
blanchet@49254
|
160 |
let
|
blanchet@49254
|
161 |
val path = file_name |> Path.explode
|
blanchet@49254
|
162 |
val _ = File.write path ""
|
blanchet@49333
|
163 |
val prover = hd provers
|
blanchet@49314
|
164 |
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
|
blanchet@49330
|
165 |
val facts = all_facts_of thy css_table
|
blanchet@49254
|
166 |
val (new_facts, old_facts) =
|
blanchet@49254
|
167 |
facts |> List.partition (has_thy thy o snd)
|
blanchet@49254
|
168 |
|>> sort (thm_ord o pairself snd)
|
blanchet@49254
|
169 |
fun do_fact (fact as (_, th)) old_facts =
|
blanchet@49254
|
170 |
let
|
blanchet@49393
|
171 |
val name = nickname_of th
|
blanchet@49265
|
172 |
val goal = goal_of_thm thy th
|
blanchet@49307
|
173 |
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
|
blanchet@49254
|
174 |
val kind = Thm.legacy_get_kind th
|
blanchet@49254
|
175 |
val _ =
|
blanchet@49254
|
176 |
if kind <> "" then
|
blanchet@49254
|
177 |
let
|
blanchet@49254
|
178 |
val suggs =
|
blanchet@49307
|
179 |
old_facts
|
blanchet@49396
|
180 |
|> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
|
blanchet@49396
|
181 |
max_relevant NONE hyp_ts concl_t
|
blanchet@49318
|
182 |
|> map (fn ((name, _), _) => name ())
|
blanchet@49318
|
183 |
val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
|
blanchet@49254
|
184 |
in File.append path s end
|
blanchet@49254
|
185 |
else
|
blanchet@49254
|
186 |
()
|
blanchet@49254
|
187 |
in fact :: old_facts end
|
blanchet@49254
|
188 |
in fold do_fact new_facts old_facts; () end
|
blanchet@49249
|
189 |
|
blanchet@49249
|
190 |
end;
|