author | blanchet |
Fri, 04 Jan 2013 21:56:20 +0100 | |
changeset 50735 | 6b232d76cbc9 |
parent 50521 | bec828f3364e |
child 50927 | 31d864d5057a |
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 |
||
48234 | 12 |
val generate_atp_inference_file_for_theory : |
45305 | 13 |
Proof.context -> theory -> atp_format -> string -> string -> unit |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
14 |
end; |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
15 |
|
48234 | 16 |
structure ATP_Theory_Export : ATP_THEORY_EXPORT = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
17 |
struct |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
18 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
19 |
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
|
20 |
open ATP_Proof |
46320 | 21 |
open ATP_Problem_Generate |
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
|
22 |
open ATP_Systems |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
23 |
|
48234 | 24 |
val fact_name_of = prefix fact_prefix o ascii_of |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
25 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
26 |
fun inference_term [] = NONE |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
27 |
| inference_term ss = |
48132
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
28 |
ATerm (("inference", []), |
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
29 |
[ATerm (("isabelle", []), []), |
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
30 |
ATerm ((tptp_empty_list, []), []), |
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
31 |
ATerm ((tptp_empty_list, []), |
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
32 |
map (fn s => ATerm ((s, []), [])) ss)]) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
33 |
|> SOME |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
34 |
fun inference infers ident = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
35 |
these (AList.lookup (op =) infers ident) |> inference_term |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
36 |
fun add_inferences_to_problem_line infers |
50521
bec828f3364e
generate comments with original names for debugging
blanchet
parents:
50485
diff
changeset
|
37 |
(Formula ((ident, alt), Axiom, phi, NONE, tms)) = |
bec828f3364e
generate comments with original names for debugging
blanchet
parents:
50485
diff
changeset
|
38 |
Formula ((ident, alt), Lemma, phi, inference infers ident, tms) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
39 |
| add_inferences_to_problem_line _ line = line |
43996 | 40 |
fun add_inferences_to_problem infers = |
41 |
map (apsnd (map (add_inferences_to_problem_line infers))) |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
42 |
|
48142
efaff8206967
finished implementation of DFG type class output
blanchet
parents:
48140
diff
changeset
|
43 |
fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident |
efaff8206967
finished implementation of DFG type class output
blanchet
parents:
48140
diff
changeset
|
44 |
| ident_of_problem_line (Type_Decl (ident, _, _)) = ident |
48137
6f524f2066e3
cleanly distinguish between type declarations and symbol declarations
blanchet
parents:
48132
diff
changeset
|
45 |
| ident_of_problem_line (Sym_Decl (ident, _, _)) = ident |
48142
efaff8206967
finished implementation of DFG type class output
blanchet
parents:
48140
diff
changeset
|
46 |
| ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident |
50521
bec828f3364e
generate comments with original names for debugging
blanchet
parents:
50485
diff
changeset
|
47 |
| ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
48 |
|
48318 | 49 |
fun atp_for_format (THF (Polymorphic, _, _, _)) = dummy_thfN |
50 |
| atp_for_format (THF (Monomorphic, _, _, _)) = satallaxN |
|
51 |
| atp_for_format (DFG Polymorphic) = spass_polyN |
|
52 |
| atp_for_format (DFG Monomorphic) = spassN |
|
53 |
| atp_for_format (TFF (Polymorphic, _)) = alt_ergoN |
|
54 |
| atp_for_format (TFF (Monomorphic, _)) = vampireN |
|
55 |
| atp_for_format FOF = eN |
|
56 |
| atp_for_format CNF_UEQ = waldmeisterN |
|
57 |
| atp_for_format CNF = eN |
|
58 |
||
45305 | 59 |
fun run_some_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
|
60 |
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
|
61 |
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
|
62 |
val prob_file = File.tmp_path (Path.explode "prob") |
48318 | 63 |
val atp = atp_for_format format |
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47055
diff
changeset
|
64 |
val {exec, arguments, proof_delims, known_failures, ...} = |
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47055
diff
changeset
|
65 |
get_atp thy atp () |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
66 |
val ord = effective_term_order ctxt atp |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
67 |
val _ = problem |> lines_for_atp_problem format ord (K []) |
46442
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46409
diff
changeset
|
68 |
|> 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
|
69 |
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
|
70 |
val command = |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
71 |
File.shell_path (Path.explode path) ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
72 |
" " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^ |
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
|
73 |
File.shell_path prob_file |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
74 |
in |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43828
diff
changeset
|
75 |
TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command |
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
|
76 |
|> fst |
48716
1d2a12bb0640
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents:
48530
diff
changeset
|
77 |
|> extract_tstplike_proof_and_outcome false proof_delims known_failures |
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
|
78 |
|> snd |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
79 |
end |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
80 |
handle TimeLimit.TimeOut => SOME TimedOut |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
81 |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
82 |
val tautology_prefixes = |
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43566
diff
changeset
|
83 |
[@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] |
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
|
84 |
|> map (fact_name_of o Context.theory_name) |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
85 |
|
50521
bec828f3364e
generate comments with original names for debugging
blanchet
parents:
50485
diff
changeset
|
86 |
fun is_problem_line_tautology ctxt format |
bec828f3364e
generate comments with original names for debugging
blanchet
parents:
50485
diff
changeset
|
87 |
(Formula ((ident, alt), _, phi, _, _)) = |
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
|
88 |
exists (fn prefix => String.isPrefix prefix ident) |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
89 |
tautology_prefixes andalso |
45305 | 90 |
is_none (run_some_atp ctxt format |
50521
bec828f3364e
generate comments with original names for debugging
blanchet
parents:
50485
diff
changeset
|
91 |
[(factsN, [Formula ((ident, alt), Conjecture, phi, NONE, [])])]) |
45305 | 92 |
| is_problem_line_tautology _ _ _ = false |
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
|
93 |
|
43499 | 94 |
fun order_facts ord = sort (ord o pairself ident_of_problem_line) |
95 |
fun order_problem_facts _ [] = [] |
|
96 |
| order_problem_facts ord ((heading, lines) :: problem) = |
|
97 |
if heading = factsN then (heading, order_facts ord lines) :: problem |
|
98 |
else (heading, lines) :: order_problem_facts ord problem |
|
99 |
||
45305 | 100 |
(* A fairly random selection of types used for monomorphizing. *) |
101 |
val ground_types = |
|
102 |
[@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool}, |
|
103 |
@{typ unit}] |
|
104 |
||
105 |
fun ground_type_for_tvar _ [] tvar = |
|
106 |
raise TYPE ("ground_type_for_sorts", [TVar tvar], []) |
|
107 |
| ground_type_for_tvar thy (T :: Ts) tvar = |
|
108 |
if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T |
|
109 |
else ground_type_for_tvar thy Ts tvar |
|
110 |
||
111 |
fun monomorphize_term ctxt t = |
|
112 |
let val thy = Proof_Context.theory_of ctxt in |
|
113 |
t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types)) |
|
114 |
handle TYPE _ => @{prop True} |
|
115 |
end |
|
116 |
||
48234 | 117 |
fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
118 |
let |
48299 | 119 |
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
|
120 |
val type_enc = |
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48301
diff
changeset
|
121 |
type_enc |> type_enc_from_string Strict |
82d6e46c673f
fixed order of accessibles + other tweaks to MaSh
blanchet
parents:
48301
diff
changeset
|
122 |
|> adjust_type_enc format |
48131 | 123 |
val mono = not (is_type_enc_polymorphic type_enc) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
124 |
val path = file_name |> Path.explode |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
125 |
val _ = File.write path "" |
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48406
diff
changeset
|
126 |
val facts = |
50442
4f6a4d32522c
don't blacklist "case" theorems -- this causes problems in MaSh later
blanchet
parents:
48716
diff
changeset
|
127 |
Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false |
48530
d443166f9520
repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents:
48438
diff
changeset
|
128 |
Symtab.empty [] [] css_table |
45551 | 129 |
val atp_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
|
130 |
facts |
45305 | 131 |
|> map (fn ((_, loc), th) => |
132 |
((Thm.get_name_hint th, loc), |
|
133 |
th |> prop_of |> mono ? monomorphize_term ctxt)) |
|
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47912
diff
changeset
|
134 |
|> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
47912
diff
changeset
|
135 |
false true [] @{prop False} |
45551 | 136 |
|> #1 |
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
|
137 |
val atp_problem = |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
138 |
atp_problem |
45305 | 139 |
|> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50521
diff
changeset
|
140 |
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
|
141 |
val infers = |
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50442
diff
changeset
|
142 |
facts |
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50442
diff
changeset
|
143 |
|> map (fn (_, th) => |
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50442
diff
changeset
|
144 |
(fact_name_of (Thm.get_name_hint th), |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50521
diff
changeset
|
145 |
th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs) |
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50442
diff
changeset
|
146 |
|> map fact_name_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
|
147 |
val all_atp_problem_names = |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
148 |
atp_problem |> maps (map ident_of_problem_line o snd) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
149 |
val infers = |
43499 | 150 |
infers |> filter (member (op =) all_atp_problem_names o fst) |
151 |
|> map (apsnd (filter (member (op =) all_atp_problem_names))) |
|
152 |
val ordered_names = |
|
153 |
String_Graph.empty |
|
154 |
|> fold (String_Graph.new_node o rpair ()) all_atp_problem_names |
|
155 |
|> fold (fn (to, froms) => |
|
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
|
156 |
fold (fn from => String_Graph.add_edge (from, to)) froms) |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
157 |
infers |
43499 | 158 |
|> String_Graph.topological_order |
159 |
val order_tab = |
|
160 |
Symtab.empty |
|
161 |
|> fold (Symtab.insert (op =)) |
|
162 |
(ordered_names ~~ (1 upto length ordered_names)) |
|
163 |
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab) |
|
164 |
val atp_problem = |
|
45305 | 165 |
atp_problem |
48131 | 166 |
|> (case format of DFG _ => I | _ => add_inferences_to_problem infers) |
45305 | 167 |
|> order_problem_facts name_ord |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
168 |
val ord = effective_term_order ctxt eN (* dummy *) |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
169 |
val ss = lines_for_atp_problem format ord (K []) atp_problem |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
170 |
val _ = app (File.append path) ss |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
171 |
in () end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
172 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
173 |
end; |