author | blanchet |
Thu, 13 Dec 2012 23:47:01 +0100 | |
changeset 50523 | 0799339fea0f |
parent 50519 | 2951841ec011 |
child 50559 | 89c0d2f13cca |
permissions | -rw-r--r-- |
48234 | 1 |
(* Title: HOL/TPTP/mash_export.ML |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Copyright 2012 |
|
4 |
||
5 |
Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer). |
|
6 |
*) |
|
7 |
||
8 |
signature MASH_EXPORT = |
|
9 |
sig |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
10 |
type params = Sledgehammer_Provers.params |
48235 | 11 |
|
50349 | 12 |
val generate_accessibility : |
13 |
Proof.context -> theory list -> bool -> string -> unit |
|
48318 | 14 |
val generate_features : |
50349 | 15 |
Proof.context -> string -> theory list -> bool -> string -> unit |
48333 | 16 |
val generate_isar_dependencies : |
50349 | 17 |
Proof.context -> theory list -> bool -> string -> unit |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
18 |
val generate_prover_dependencies : |
50349 | 19 |
Proof.context -> params -> theory list -> bool -> string -> unit |
50411 | 20 |
val generate_isar_commands : |
21 |
Proof.context -> string -> theory list -> string -> unit |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
22 |
val generate_prover_commands : |
50349 | 23 |
Proof.context -> params -> theory list -> string -> unit |
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
24 |
val generate_mepo_suggestions : |
50349 | 25 |
Proof.context -> params -> theory list -> int -> string -> unit |
48234 | 26 |
end; |
27 |
||
28 |
structure MaSh_Export : MASH_EXPORT = |
|
29 |
struct |
|
30 |
||
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
31 |
open Sledgehammer_Fact |
48381 | 32 |
open Sledgehammer_MePo |
33 |
open Sledgehammer_MaSh |
|
48245 | 34 |
|
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
35 |
fun thy_map_from_facts ths = |
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
36 |
ths |> rev |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
37 |
|> map (snd #> `(theory_of_thm #> Context.theory_name)) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
38 |
|> AList.coalesce (op =) |
48378 | 39 |
|> map (apsnd (map nickname_of)) |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
40 |
|
50349 | 41 |
fun has_thm_thy th thy = |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
42 |
Context.theory_name thy = Context.theory_name (theory_of_thm th) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
43 |
|
50349 | 44 |
fun has_thys thys th = exists (has_thm_thy th) thys |
45 |
||
46 |
fun all_facts ctxt = |
|
48531 | 47 |
let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in |
50442
4f6a4d32522c
don't blacklist "case" theorems -- this causes problems in MaSh later
blanchet
parents:
50434
diff
changeset
|
48 |
Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css |
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
49 |
|> sort (thm_ord o pairself snd) |
48531 | 50 |
end |
51 |
||
50349 | 52 |
fun add_thy_parent_facts thy_map thy = |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
53 |
let |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
54 |
fun add_last thy = |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
55 |
case AList.lookup (op =) thy_map (Context.theory_name thy) of |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
56 |
SOME (last_fact :: _) => insert (op =) last_fact |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
57 |
| _ => add_parent thy |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
58 |
and add_parent thy = fold add_last (Theory.parents_of thy) |
50349 | 59 |
in add_parent thy end |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
60 |
|
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
61 |
val thy_name_of_fact = hd o Long_Name.explode |
50349 | 62 |
fun thy_of_fact thy = Context.get_theory thy o thy_name_of_fact |
48304 | 63 |
|
50349 | 64 |
fun generate_accessibility ctxt thys include_thys file_name = |
48304 | 65 |
let |
66 |
val path = file_name |> Path.explode |
|
67 |
val _ = File.write path "" |
|
68 |
fun do_fact fact prevs = |
|
69 |
let |
|
70 |
val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" |
|
71 |
val _ = File.append path s |
|
72 |
in [fact] end |
|
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48304
diff
changeset
|
73 |
val thy_map = |
50349 | 74 |
all_facts ctxt |
75 |
|> not include_thys ? filter_out (has_thys thys o snd) |
|
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48304
diff
changeset
|
76 |
|> thy_map_from_facts |
48304 | 77 |
fun do_thy facts = |
78 |
let |
|
50349 | 79 |
val thy = thy_of_fact (Proof_Context.theory_of ctxt) (hd facts) |
80 |
val parents = add_thy_parent_facts thy_map thy [] |
|
48530
d443166f9520
repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents:
48529
diff
changeset
|
81 |
in fold_rev do_fact facts parents; () end |
48333 | 82 |
in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end |
48304 | 83 |
|
50349 | 84 |
fun generate_features ctxt prover thys include_thys file_name = |
48304 | 85 |
let |
86 |
val path = file_name |> Path.explode |
|
87 |
val _ = File.write path "" |
|
88 |
val facts = |
|
50349 | 89 |
all_facts ctxt |
90 |
|> not include_thys ? filter_out (has_thys thys o snd) |
|
48385 | 91 |
fun do_fact ((_, stature), th) = |
48304 | 92 |
let |
48378 | 93 |
val name = nickname_of th |
48318 | 94 |
val feats = |
48385 | 95 |
features_of ctxt prover (theory_of_thm th) stature [prop_of th] |
50356 | 96 |
val s = escape_meta name ^ ": " ^ encode_features feats ^ "\n" |
48304 | 97 |
in File.append path s end |
98 |
in List.app do_fact facts end |
|
99 |
||
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
100 |
fun isar_or_prover_dependencies_of ctxt params_opt facts all_names th |
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
101 |
isar_deps_opt = |
50411 | 102 |
(case params_opt of |
103 |
SOME (params as {provers = prover :: _, ...}) => |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
104 |
prover_dependencies_of ctxt params prover 0 facts all_names th |> snd |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
105 |
| NONE => |
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
106 |
case isar_deps_opt of |
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
107 |
SOME deps => deps |
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
108 |
| NONE => isar_dependencies_of all_names th) |
50411 | 109 |
|> these |
110 |
||
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
111 |
fun generate_isar_or_prover_dependencies ctxt params_opt thys include_thys |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
112 |
file_name = |
48304 | 113 |
let |
114 |
val path = file_name |> Path.explode |
|
115 |
val facts = |
|
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
116 |
all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd) |
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
117 |
val all_names = build_all_names nickname_of facts |
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
118 |
fun do_fact (_, th) = |
48304 | 119 |
let |
48378 | 120 |
val name = nickname_of th |
48665 | 121 |
val deps = |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
122 |
isar_or_prover_dependencies_of ctxt params_opt facts all_names th NONE |
50519 | 123 |
in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end |
124 |
val lines = Par_List.map do_fact facts |
|
125 |
in File.write_list path lines end |
|
48304 | 126 |
|
50411 | 127 |
fun generate_isar_dependencies ctxt = |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
128 |
generate_isar_or_prover_dependencies ctxt NONE |
50411 | 129 |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
130 |
fun generate_prover_dependencies ctxt params = |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
131 |
generate_isar_or_prover_dependencies ctxt (SOME params) |
50411 | 132 |
|
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
133 |
fun is_bad_query ctxt ho_atp th isar_deps = |
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
134 |
Thm.legacy_get_kind th = "" orelse null isar_deps orelse |
50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50519
diff
changeset
|
135 |
is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
136 |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
137 |
fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name = |
48234 | 138 |
let |
50511
8825c36cb1ce
don't query blacklisted theorems in evaluation driver
blanchet
parents:
50485
diff
changeset
|
139 |
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover |
48234 | 140 |
val path = file_name |> Path.explode |
50349 | 141 |
val facts = all_facts ctxt |
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
142 |
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) |
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
143 |
val all_names = build_all_names nickname_of facts |
50519 | 144 |
fun do_fact ((name, ((_, stature), th)), prevs) = |
48234 | 145 |
let |
50349 | 146 |
val feats = |
147 |
features_of ctxt prover (theory_of_thm th) stature [prop_of th] |
|
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
148 |
val isar_deps = isar_dependencies_of all_names th |
48665 | 149 |
val deps = |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
150 |
isar_or_prover_dependencies_of ctxt params_opt facts all_names th |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
151 |
(SOME isar_deps) |
48529
716ec3458b1d
generate fact name in queries again + use ATP dependencies when possible
blanchet
parents:
48438
diff
changeset
|
152 |
val core = |
716ec3458b1d
generate fact name in queries again + use ATP dependencies when possible
blanchet
parents:
48438
diff
changeset
|
153 |
escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ |
50356 | 154 |
encode_features feats |
48666 | 155 |
val query = |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
156 |
if is_bad_query ctxt ho_atp th (these isar_deps) then "" |
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
157 |
else "? " ^ core ^ "\n" |
48529
716ec3458b1d
generate fact name in queries again + use ATP dependencies when possible
blanchet
parents:
48438
diff
changeset
|
158 |
val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n" |
50519 | 159 |
in query ^ update end |
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48304
diff
changeset
|
160 |
val thy_map = old_facts |> thy_map_from_facts |
50349 | 161 |
val parents = fold (add_thy_parent_facts thy_map) thys [] |
50519 | 162 |
val new_facts = new_facts |> map (`(nickname_of o snd)) |
163 |
val prevss = fst (split_last (parents :: map (single o fst) new_facts)) |
|
164 |
val lines = Par_List.map do_fact (new_facts ~~ prevss) |
|
165 |
in File.write_list path lines end |
|
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
166 |
|
50411 | 167 |
fun generate_isar_commands ctxt prover = |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
168 |
generate_isar_or_prover_commands ctxt prover NONE |
50411 | 169 |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
170 |
fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) = |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
171 |
generate_isar_or_prover_commands ctxt prover (SOME params) |
50411 | 172 |
|
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
173 |
fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) thys |
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
174 |
max_facts file_name = |
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
175 |
let |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
176 |
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover |
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
177 |
val path = file_name |> Path.explode |
50349 | 178 |
val facts = all_facts ctxt |
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
179 |
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
180 |
val all_names = build_all_names nickname_of facts |
50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50519
diff
changeset
|
181 |
fun do_fact ((_, th), old_facts) = |
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
182 |
let |
48378 | 183 |
val name = nickname_of th |
50349 | 184 |
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
48292 | 185 |
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
186 |
val isar_deps = isar_dependencies_of all_names th |
50519 | 187 |
in |
188 |
if is_bad_query ctxt ho_atp th (these isar_deps) then |
|
189 |
"" |
|
190 |
else |
|
191 |
let |
|
192 |
val suggs = |
|
193 |
old_facts |
|
194 |
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover |
|
195 |
max_facts NONE hyp_ts concl_t |
|
196 |
|> map (nickname_of o snd) |
|
197 |
in escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" end |
|
198 |
end |
|
199 |
fun accum x (yss as ys :: _) = (x :: ys) :: yss |
|
200 |
val old_factss = tl (fold accum new_facts [old_facts]) |
|
201 |
val lines = Par_List.map do_fact (new_facts ~~ rev old_factss) |
|
202 |
in File.write_list path lines end |
|
48234 | 203 |
|
204 |
end; |