author | desharna |
Fri, 09 Jul 2021 17:58:17 +0200 | |
changeset 73942 | 57423714c29d |
parent 73575 | 23d2adc5489e |
child 74044 | 943757b788f9 |
permissions | -rw-r--r-- |
46321 | 1 |
(* Title: HOL/TPTP/atp_theory_export.ML |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
3 |
Copyright 2011 |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
4 |
|
48234 | 5 |
Export Isabelle theories as first-order TPTP inferences. |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
6 |
*) |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
7 |
|
46321 | 8 |
signature ATP_THEORY_EXPORT = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
9 |
sig |
45305 | 10 |
type atp_format = ATP_Problem.atp_format |
11 |
||
51646 | 12 |
datatype inference_policy = |
13 |
No_Inferences | Unchecked_Inferences | Checked_Inferences |
|
14 |
||
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
15 |
val generate_atp_inference_file_for_theory : Proof.context -> theory -> atp_format -> |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
16 |
inference_policy -> string -> string -> unit |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
17 |
val generate_casc_lbt_isa_files_for_theory : Proof.context -> theory -> atp_format -> |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
18 |
inference_policy -> string -> string -> unit |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
19 |
end; |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
20 |
|
48234 | 21 |
structure ATP_Theory_Export : ATP_THEORY_EXPORT = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
22 |
struct |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
23 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
24 |
open ATP_Problem |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
25 |
open ATP_Proof |
46320 | 26 |
open ATP_Problem_Generate |
72400 | 27 |
open Sledgehammer_ATP_Systems |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
28 |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
29 |
val max_dependencies = 100 |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
30 |
val max_facts = 512 |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
31 |
val atp_timeout = seconds 0.5 |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
32 |
|
51646 | 33 |
datatype inference_policy = |
34 |
No_Inferences | Unchecked_Inferences | Checked_Inferences |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
35 |
|
53980
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
53586
diff
changeset
|
36 |
val prefix = Library.prefix |
51646 | 37 |
val fact_name_of = prefix fact_prefix o ascii_of |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
38 |
|
72591 | 39 |
fun atp_of_format (THF (_, Polymorphic, _)) = leo3N |
40 |
| atp_of_format (THF (_, Monomorphic, _)) = satallaxN |
|
59577 | 41 |
| atp_of_format (DFG Polymorphic) = pirateN |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
42 |
| atp_of_format (DFG Monomorphic) = spassN |
72591 | 43 |
| atp_of_format (TFF (_, Polymorphic)) = alt_ergoN |
44 |
| atp_of_format (TFF (_, Monomorphic)) = vampireN |
|
70943 | 45 |
| atp_of_format FOF = eN (* FIXME? *) |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
46 |
| atp_of_format CNF_UEQ = waldmeisterN |
70943 | 47 |
| atp_of_format CNF = eN (* FIXME? *) |
48318 | 48 |
|
51646 | 49 |
fun run_atp ctxt format problem = |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
50 |
let |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
51 |
val thy = Proof_Context.theory_of ctxt |
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
47038
diff
changeset
|
52 |
val prob_file = File.tmp_path (Path.explode "prob") |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
53 |
val atp = atp_of_format format |
57676 | 54 |
val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
55 |
val ord = effective_term_order ctxt atp |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
56 |
val _ = problem |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
57 |
|> lines_of_atp_problem format ord (K []) |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
58 |
|> File.write_list prob_file |
48376
416e4123baf3
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents:
48324
diff
changeset
|
59 |
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
60 |
val command = |
73575 | 61 |
space_implode " " (File.bash_path (Path.explode path) :: |
62 |
arguments ctxt false "" atp_timeout prob_file (ord, K [], K [])) |
|
51646 | 63 |
val outcome = |
62519 | 64 |
Timeout.apply atp_timeout Isabelle_System.bash_output command |
51646 | 65 |
|> fst |
66 |
|> extract_tstplike_proof_and_outcome false proof_delims known_failures |
|
67 |
|> snd |
|
62519 | 68 |
handle Timeout.TIMEOUT _ => SOME TimedOut |
51647
25acf689a53e
no need to filter tautologies anymore -- they are prefiltered by "all_facts"'
blanchet
parents:
51646
diff
changeset
|
69 |
val _ = |
25acf689a53e
no need to filter tautologies anymore -- they are prefiltered by "all_facts"'
blanchet
parents:
51646
diff
changeset
|
70 |
tracing ("Ran ATP: " ^ |
51649 | 71 |
(case outcome of |
72 |
NONE => "Success" |
|
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
52995
diff
changeset
|
73 |
| SOME failure => string_of_atp_failure failure)) |
51646 | 74 |
in outcome end |
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
75 |
|
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
76 |
fun is_problem_line_reprovable ctxt format prelude axioms deps (Formula (ident', _, phi, _, _)) = |
51646 | 77 |
is_none (run_atp ctxt format |
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
78 |
((factsN, |
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
79 |
Formula (ident', Conjecture, phi, NONE, []) :: map_filter (Symtab.lookup axioms) deps) :: |
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
80 |
prelude)) |
51646 | 81 |
| is_problem_line_reprovable _ _ _ _ _ _ = false |
82 |
||
83 |
fun inference_term _ [] = NONE |
|
84 |
| inference_term check_infs ss = |
|
85 |
ATerm (("inference", []), |
|
86 |
[ATerm (("checked_isabelle" |> not check_infs ? prefix "un", []), []), |
|
87 |
ATerm ((tptp_empty_list, []), []), |
|
88 |
ATerm ((tptp_empty_list, []), |
|
89 |
map (fn s => ATerm ((s, []), [])) ss)]) |
|
90 |
|> SOME |
|
91 |
||
92 |
fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers |
|
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
93 |
(line as Formula ((ident, alt), Axiom, phi, NONE, info)) = |
51646 | 94 |
let |
95 |
val deps = |
|
96 |
case these (AList.lookup (op =) infers ident) of |
|
97 |
[] => [] |
|
98 |
| deps => |
|
99 |
if check_infs andalso |
|
100 |
not (is_problem_line_reprovable ctxt format prelude axioms deps |
|
101 |
line) then |
|
102 |
[] |
|
103 |
else |
|
104 |
deps |
|
105 |
in |
|
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
106 |
Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, info) |
51646 | 107 |
end |
108 |
| add_inferences_to_problem_line _ _ _ _ _ _ line = line |
|
109 |
||
110 |
fun add_inferences_to_problem ctxt format check_infs prelude infers problem = |
|
111 |
let |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
112 |
fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) = Symtab.default (ident, axiom) |
51646 | 113 |
| add_if_axiom _ = I |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
114 |
|
51646 | 115 |
val add_axioms_of_problem = fold (fold add_if_axiom o snd) |
116 |
val axioms = Symtab.empty |> check_infs ? add_axioms_of_problem problem |
|
117 |
in |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
118 |
map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs prelude axioms infers))) |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
119 |
problem |
51646 | 120 |
end |
121 |
||
122 |
fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident |
|
123 |
| ident_of_problem_line (Type_Decl (ident, _, _)) = ident |
|
124 |
| ident_of_problem_line (Sym_Decl (ident, _, _)) = ident |
|
125 |
| ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident |
|
126 |
| ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident |
|
127 |
||
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58922
diff
changeset
|
128 |
fun order_facts ord = sort (ord o apply2 ident_of_problem_line) |
51646 | 129 |
|
43499 | 130 |
fun order_problem_facts _ [] = [] |
131 |
| order_problem_facts ord ((heading, lines) :: problem) = |
|
132 |
if heading = factsN then (heading, order_facts ord lines) :: problem |
|
133 |
else (heading, lines) :: order_problem_facts ord problem |
|
134 |
||
45305 | 135 |
(* A fairly random selection of types used for monomorphizing. *) |
136 |
val ground_types = |
|
69597 | 137 |
[\<^typ>\<open>nat\<close>, HOLogic.intT, HOLogic.realT, \<^typ>\<open>nat => bool\<close>, \<^typ>\<open>bool\<close>, |
138 |
\<^typ>\<open>unit\<close>] |
|
45305 | 139 |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
140 |
fun ground_type_of_tvar _ [] tvar = raise TYPE ("ground_type_of_tvar", [TVar tvar], []) |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
141 |
| ground_type_of_tvar thy (T :: Ts) tvar = |
45305 | 142 |
if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
143 |
else ground_type_of_tvar thy Ts tvar |
45305 | 144 |
|
145 |
fun monomorphize_term ctxt t = |
|
146 |
let val thy = Proof_Context.theory_of ctxt in |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
147 |
t |> map_types (map_type_tvar (ground_type_of_tvar thy ground_types)) |
69597 | 148 |
handle TYPE _ => \<^prop>\<open>True\<close> |
45305 | 149 |
end |
150 |
||
51633 | 151 |
fun heading_sort_key heading = |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
152 |
if String.isPrefix factsN heading then "_" ^ heading else heading |
57306
ff10067b2248
optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents:
57268
diff
changeset
|
153 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
154 |
fun problem_of_theory ctxt thy format infer_policy type_enc = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
155 |
let |
48299 | 156 |
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48301
diff
changeset
|
157 |
val type_enc = |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
158 |
type_enc |> type_enc_of_string Non_Strict |
48315
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48301
diff
changeset
|
159 |
|> adjust_type_enc format |
48131 | 160 |
val mono = not (is_type_enc_polymorphic type_enc) |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
161 |
|
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48406
diff
changeset
|
162 |
val facts = |
73942 | 163 |
Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true Keyword.empty_keywords [] [] |
164 |
css_table |
|
60641 | 165 |
|> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd) |
51646 | 166 |
val problem = |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset
|
167 |
facts |
45305 | 168 |
|> map (fn ((_, loc), th) => |
59582 | 169 |
((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt)) |
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
170 |
|> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true [] |
69597 | 171 |
\<^prop>\<open>False\<close> |
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
60641
diff
changeset
|
172 |
|> #1 |> sort_by (heading_sort_key o fst) |
51646 | 173 |
val prelude = fst (split_last problem) |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50521
diff
changeset
|
174 |
val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
175 |
val infers = |
51646 | 176 |
if infer_policy = No_Inferences then |
177 |
[] |
|
178 |
else |
|
179 |
facts |
|
180 |
|> map (fn (_, th) => |
|
181 |
(fact_name_of (Thm.get_name_hint th), |
|
57306
ff10067b2248
optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents:
57268
diff
changeset
|
182 |
th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs) |
ff10067b2248
optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents:
57268
diff
changeset
|
183 |
|> these |> map fact_name_of)) |
51650 | 184 |
val all_problem_names = |
57307 | 185 |
problem |> maps (map ident_of_problem_line o snd) |> distinct (op =) |
51650 | 186 |
val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
187 |
val infers = |
51650 | 188 |
infers |> filter (Symtab.defined all_problem_name_set o fst) |
189 |
|> map (apsnd (filter (Symtab.defined all_problem_name_set))) |
|
190 |
val maybe_add_edge = perhaps o try o String_Graph.add_edge_acyclic |
|
43499 | 191 |
val ordered_names = |
192 |
String_Graph.empty |
|
51646 | 193 |
|> fold (String_Graph.new_node o rpair ()) all_problem_names |
57307 | 194 |
|> fold (fn (to, froms) => fold (fn from => maybe_add_edge (from, to)) froms) infers |
51650 | 195 |
|> fold (fn (to, from) => maybe_add_edge (from, to)) |
57307 | 196 |
(tl all_problem_names ~~ fst (split_last all_problem_names)) |
43499 | 197 |
|> String_Graph.topological_order |
198 |
val order_tab = |
|
199 |
Symtab.empty |
|
57307 | 200 |
|> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names)) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58922
diff
changeset
|
201 |
val name_ord = int_ord o apply2 (the o Symtab.lookup order_tab) |
51646 | 202 |
in |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
203 |
(facts, |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
204 |
problem |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
205 |
|> (case format of |
51646 | 206 |
DFG _ => I |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
207 |
| _ => add_inferences_to_problem ctxt format (infer_policy = Checked_Inferences) prelude |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
208 |
infers) |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
209 |
|> order_problem_facts name_ord) |
51646 | 210 |
end |
211 |
||
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
212 |
fun lines_of_problem ctxt format = |
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
213 |
lines_of_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K []) |
51646 | 214 |
|
215 |
fun write_lines path ss = |
|
216 |
let |
|
217 |
val _ = File.write path "" |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
218 |
val _ = app (File.append path) ss |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
219 |
in () end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
220 |
|
70943 | 221 |
fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc file_name = |
51646 | 222 |
let |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
223 |
val (_, problem) = problem_of_theory ctxt thy format infer_policy type_enc |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
224 |
val ss = lines_of_problem ctxt format problem |
51646 | 225 |
in write_lines (Path.explode file_name) ss end |
226 |
||
227 |
fun ap dir = Path.append dir o Path.explode |
|
228 |
||
229 |
fun chop_maximal_groups eq xs = |
|
230 |
let |
|
231 |
val rev_xs = rev xs |
|
232 |
fun chop_group _ [] = [] |
|
233 |
| chop_group n (xs as x :: _) = |
|
234 |
let |
|
235 |
val n' = find_index (curry eq x) rev_xs |
|
236 |
val (ws', xs') = chop (n - n') xs |
|
237 |
in ws' :: chop_group n' xs' end |
|
238 |
in chop_group (length xs) xs end |
|
239 |
||
240 |
fun theory_name_of_fact (Formula ((_, alt), _, _, _, _)) = |
|
241 |
(case first_field Long_Name.separator alt of |
|
242 |
NONE => alt |
|
243 |
| SOME (thy, _) => thy) |
|
244 |
| theory_name_of_fact _ = "" |
|
245 |
||
246 |
val problem_suffix = ".p" |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
247 |
val suggestion_suffix = ".sugg" |
51646 | 248 |
val include_suffix = ".ax" |
249 |
||
250 |
val file_order_name = "FilesInProcessingOrder" |
|
251 |
val problem_order_name = "ProblemsInProcessingOrder" |
|
252 |
val problem_name = "problems" |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
253 |
val suggestion_name = "suggestions" |
51646 | 254 |
val include_name = "incl" |
255 |
val prelude_base_name = "prelude" |
|
256 |
val prelude_name = prelude_base_name ^ include_suffix |
|
257 |
||
51652
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
258 |
val encode_meta = Sledgehammer_MaSh.encode_str |
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
259 |
|
53980
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
53586
diff
changeset
|
260 |
fun include_base_name_of_fact x = encode_meta (theory_name_of_fact x) |
51646 | 261 |
|
262 |
fun include_line base_name = |
|
263 |
"include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n" |
|
264 |
||
51652
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
265 |
val hol_base_name = encode_meta "HOL" |
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
266 |
|
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
267 |
fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) = |
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
268 |
(case try (Global_Theory.get_thm thy) alt of |
51652
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
269 |
SOME th => |
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
270 |
(* This is a crude hack to detect theorems stated and proved by the user (as opposed to those |
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
271 |
derived by various packages). In addition, we leave out everything in "HOL" as too basic to |
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
272 |
be interesting. *) |
51652
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
273 |
Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name |
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
274 |
| NONE => false) |
51646 | 275 |
|
276 |
(* Convention: theoryname__goalname *) |
|
51652
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
277 |
fun problem_name_of base_name n alt = |
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
278 |
base_name ^ "__" ^ string_of_int n ^ "_" ^ |
5ff01d585a8c
handle case clashes on Mac file system by encoding goal numbers
blanchet
parents:
51650
diff
changeset
|
279 |
perhaps (try (unprefix (base_name ^ "_"))) alt ^ problem_suffix |
51646 | 280 |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
281 |
fun suggestion_name_of base_name n alt = |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
282 |
base_name ^ "__" ^ string_of_int n ^ "_" ^ |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
283 |
perhaps (try (unprefix (base_name ^ "_"))) alt ^ suggestion_suffix |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
284 |
|
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
285 |
fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc dir_name = |
51646 | 286 |
let |
73315 | 287 |
val dir = Isabelle_System.make_directory (Path.explode dir_name) |
51646 | 288 |
val file_order_path = ap dir file_order_name |
289 |
val _ = File.write file_order_path "" |
|
290 |
val problem_order_path = ap dir problem_order_name |
|
291 |
val _ = File.write problem_order_path "" |
|
73315 | 292 |
val problem_dir = Isabelle_System.make_directory (ap dir problem_name) |
293 |
val suggestion_dir = Isabelle_System.make_directory (ap dir suggestion_name) |
|
294 |
val include_dir = Isabelle_System.make_directory (ap problem_dir include_name) |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
295 |
|
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
296 |
val (facts, (prelude, groups)) = |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
297 |
problem_of_theory ctxt thy format infer_policy type_enc |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
298 |
||> split_last |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
299 |
||> apsnd (snd |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58922
diff
changeset
|
300 |
#> chop_maximal_groups (op = o apply2 theory_name_of_fact) |
51646 | 301 |
#> map (`(include_base_name_of_fact o hd))) |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
302 |
|
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
303 |
val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts) |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
304 |
|
51646 | 305 |
fun write_prelude () = |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
306 |
let val ss = lines_of_problem ctxt format prelude in |
51646 | 307 |
File.append file_order_path (prelude_base_name ^ "\n"); |
308 |
write_lines (ap include_dir prelude_name) ss |
|
309 |
end |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
310 |
|
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
311 |
fun write_include_file (base_name, fact_lines) = |
51646 | 312 |
let |
313 |
val name = base_name ^ include_suffix |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
314 |
val ss = lines_of_problem ctxt format [(factsN, fact_lines)] |
51646 | 315 |
in |
316 |
File.append file_order_path (base_name ^ "\n"); |
|
317 |
write_lines (ap include_dir name) ss |
|
318 |
end |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
319 |
|
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
320 |
fun select_facts_for_fact facts fact = |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
321 |
let |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
322 |
val (hyp_ts, conj_t) = Logic.strip_horn (Thm.prop_of (snd fact)) |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
323 |
val mepo = Sledgehammer_MePo.mepo_suggested_facts ctxt |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
324 |
(Sledgehammer_Commands.default_params thy []) max_facts NONE hyp_ts conj_t facts |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
325 |
in |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
326 |
map (suffix "\n" o fact_name_of o Thm.get_name_hint o snd) mepo |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
327 |
end |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
328 |
|
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
329 |
fun write_problem_files _ _ _ _ [] = () |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
330 |
| write_problem_files _ seen_facts includes [] groups = |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
331 |
write_problem_files 1 seen_facts includes includes groups |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
332 |
| write_problem_files n seen_facts includes _ ((base_name, []) :: groups) = |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
333 |
write_problem_files n seen_facts (includes @ [include_line base_name]) [] groups |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
334 |
| write_problem_files n seen_facts includes seen_ss |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
335 |
((base_name, fact_line :: fact_lines) :: groups) = |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
336 |
let |
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
337 |
val (alt, pname, sname, conj) = |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
338 |
(case fact_line of |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
339 |
Formula ((ident, alt), _, phi, _, _) => |
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61323
diff
changeset
|
340 |
(alt, problem_name_of base_name n (encode_meta alt), |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
341 |
suggestion_name_of base_name n (encode_meta alt), |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
342 |
Formula ((ident, alt), Conjecture, phi, NONE, []))) |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
343 |
val fact = the (Symtab.lookup fact_tab alt) |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
344 |
val fact_s = tptp_string_of_line format fact_line |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
345 |
in |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
346 |
(if should_generate_problem thy base_name fact_line then |
51646 | 347 |
let |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51652
diff
changeset
|
348 |
val conj_s = tptp_string_of_line format conj |
51646 | 349 |
in |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
350 |
File.append problem_order_path (pname ^ "\n"); |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
351 |
write_lines (ap problem_dir pname) (seen_ss @ [conj_s]); |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
352 |
write_lines (ap suggestion_dir sname) (select_facts_for_fact facts fact) |
51646 | 353 |
end |
354 |
else |
|
355 |
(); |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
356 |
write_problem_files (n + 1) (fact :: seen_facts) includes (seen_ss @ [fact_s]) |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
357 |
((base_name, fact_lines) :: groups)) |
51646 | 358 |
end |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
359 |
|
51646 | 360 |
val _ = write_prelude () |
361 |
val _ = app write_include_file groups |
|
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
60924
diff
changeset
|
362 |
val _ = write_problem_files 1 [] [include_line prelude_base_name] [] groups |
51646 | 363 |
in () end |
364 |
||
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
365 |
end; |