author | blanchet |
Wed, 11 Jul 2012 21:43:19 +0200 | |
changeset 48251 | 6cdcfbddc077 |
parent 48250 | 1065c307fafe |
child 48299 | 5e5c6616f0fe |
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 |
46406 | 37 |
(Formula (ident, Axiom, phi, NONE, tms)) = |
38 |
Formula (ident, 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 |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
47 |
| ident_of_problem_line (Formula (ident, _, _, _, _)) = ident |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
48 |
|
45305 | 49 |
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
|
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") |
48131 | 53 |
val atp = case format of DFG _ => spassN | _ => eN |
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47055
diff
changeset
|
54 |
val {exec, arguments, proof_delims, known_failures, ...} = |
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47055
diff
changeset
|
55 |
get_atp thy atp () |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
56 |
val ord = effective_term_order ctxt atp |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
57 |
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
|
58 |
|> File.write_list prob_file |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
59 |
val path = getenv (List.last (fst exec)) ^ "/" ^ 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 = |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
61 |
File.shell_path (Path.explode path) ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
62 |
" " ^ 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
|
63 |
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
|
64 |
in |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43828
diff
changeset
|
65 |
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
|
66 |
|> fst |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
67 |
|> extract_tstplike_proof_and_outcome false true 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
|
68 |
|> 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
|
69 |
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
|
70 |
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
|
71 |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
72 |
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
|
73 |
[@{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
|
74 |
|> 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
|
75 |
|
45305 | 76 |
fun is_problem_line_tautology ctxt format (Formula (ident, _, 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
|
77 |
exists (fn prefix => String.isPrefix prefix ident) |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
78 |
tautology_prefixes andalso |
45305 | 79 |
is_none (run_some_atp ctxt format |
46406 | 80 |
[(factsN, [Formula (ident, Conjecture, phi, NONE, [])])]) |
45305 | 81 |
| 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
|
82 |
|
43499 | 83 |
fun order_facts ord = sort (ord o pairself ident_of_problem_line) |
84 |
fun order_problem_facts _ [] = [] |
|
85 |
| order_problem_facts ord ((heading, lines) :: problem) = |
|
86 |
if heading = factsN then (heading, order_facts ord lines) :: problem |
|
87 |
else (heading, lines) :: order_problem_facts ord problem |
|
88 |
||
45305 | 89 |
(* A fairly random selection of types used for monomorphizing. *) |
90 |
val ground_types = |
|
91 |
[@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool}, |
|
92 |
@{typ unit}] |
|
93 |
||
94 |
fun ground_type_for_tvar _ [] tvar = |
|
95 |
raise TYPE ("ground_type_for_sorts", [TVar tvar], []) |
|
96 |
| ground_type_for_tvar thy (T :: Ts) tvar = |
|
97 |
if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T |
|
98 |
else ground_type_for_tvar thy Ts tvar |
|
99 |
||
100 |
fun monomorphize_term ctxt t = |
|
101 |
let val thy = Proof_Context.theory_of ctxt in |
|
102 |
t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types)) |
|
103 |
handle TYPE _ => @{prop True} |
|
104 |
end |
|
105 |
||
48234 | 106 |
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
|
107 |
let |
46301 | 108 |
val type_enc = type_enc |> type_enc_from_string Strict |
45305 | 109 |
|> adjust_type_enc format |
48131 | 110 |
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
|
111 |
val path = file_name |> Path.explode |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
112 |
val _ = File.write path "" |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
113 |
val facts = Sledgehammer_Fact.all_facts_of thy |
45551 | 114 |
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
|
115 |
facts |
45305 | 116 |
|> map (fn ((_, loc), th) => |
117 |
((Thm.get_name_hint th, loc), |
|
118 |
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
|
119 |
|> 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
|
120 |
false true [] @{prop False} |
45551 | 121 |
|> #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
|
122 |
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
|
123 |
atp_problem |
45305 | 124 |
|> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
125 |
val ths = facts |> map snd |
48229 | 126 |
val all_names = ths |> map Thm.get_name_hint |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
127 |
val infers = |
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
|
128 |
facts |> map (fn (_, th) => |
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
|
129 |
(fact_name_of (Thm.get_name_hint th), |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
130 |
th |> Sledgehammer_Util.thms_in_proof (SOME all_names) |
48234 | 131 |
|> 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
|
132 |
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
|
133 |
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
|
134 |
val infers = |
43499 | 135 |
infers |> filter (member (op =) all_atp_problem_names o fst) |
136 |
|> map (apsnd (filter (member (op =) all_atp_problem_names))) |
|
137 |
val ordered_names = |
|
138 |
String_Graph.empty |
|
139 |
|> fold (String_Graph.new_node o rpair ()) all_atp_problem_names |
|
140 |
|> 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
|
141 |
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
|
142 |
infers |
43499 | 143 |
|> String_Graph.topological_order |
144 |
val order_tab = |
|
145 |
Symtab.empty |
|
146 |
|> fold (Symtab.insert (op =)) |
|
147 |
(ordered_names ~~ (1 upto length ordered_names)) |
|
148 |
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab) |
|
149 |
val atp_problem = |
|
45305 | 150 |
atp_problem |
48131 | 151 |
|> (case format of DFG _ => I | _ => add_inferences_to_problem infers) |
45305 | 152 |
|> order_problem_facts name_ord |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
153 |
val ord = effective_term_order ctxt eN (* dummy *) |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
154 |
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
|
155 |
val _ = app (File.append path) ss |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
156 |
in () end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
157 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
158 |
end; |