author | blanchet |
Mon, 21 May 2012 10:39:32 +0200 | |
changeset 47946 | 33afcfad3f8d |
parent 47912 | 12de57c5eee5 |
child 47949 | fafbb2607366 |
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 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
5 |
Export Isabelle theories as first-order TPTP inferences, exploiting |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
6 |
Sledgehammer's translation. |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
7 |
*) |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
8 |
|
46321 | 9 |
signature ATP_THEORY_EXPORT = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
10 |
sig |
45305 | 11 |
type atp_format = ATP_Problem.atp_format |
12 |
||
43494
13eefebbc4cb
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
blanchet
parents:
43479
diff
changeset
|
13 |
val theorems_mentioned_in_proof_term : |
13eefebbc4cb
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
blanchet
parents:
43479
diff
changeset
|
14 |
string list option -> thm -> string list |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
15 |
val generate_tptp_graph_file_for_theory : |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
16 |
Proof.context -> theory -> string -> unit |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
17 |
val generate_tptp_inference_file_for_theory : |
45305 | 18 |
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
|
19 |
end; |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
20 |
|
46321 | 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 |
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
|
27 |
open ATP_Systems |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
28 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
29 |
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
|
30 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
31 |
fun facts_of thy = |
46734 | 32 |
let val ctxt = Proof_Context.init_global thy in |
33 |
Sledgehammer_Filter.all_facts ctxt false |
|
34 |
Symtab.empty true [] [] |
|
35 |
(Sledgehammer_Filter.clasimpset_rule_table_of ctxt) |
|
36 |
|> filter (curry (op =) @{typ bool} o fastype_of |
|
37 |
o Object_Logic.atomize_term thy o prop_of o snd) |
|
38 |
end |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
39 |
|
43468
c768f7adb711
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
blanchet
parents:
43400
diff
changeset
|
40 |
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
c768f7adb711
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
blanchet
parents:
43400
diff
changeset
|
41 |
fixes that seem to be missing over there; or maybe the two code portions are |
c768f7adb711
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
blanchet
parents:
43400
diff
changeset
|
42 |
not doing the same? *) |
43498
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
43 |
fun fold_body_thms thm_name all_names f = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
44 |
let |
43468
c768f7adb711
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
blanchet
parents:
43400
diff
changeset
|
45 |
fun app n (PBody {thms, ...}) = |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
46 |
thms |> fold (fn (_, (name, prop, body)) => fn x => |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
47 |
let |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
48 |
val body' = Future.join body |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
49 |
val n' = |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
50 |
n + (if name = "" orelse |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
51 |
(is_some all_names andalso |
43498
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
52 |
not (member (op =) (the all_names) name)) orelse |
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
53 |
(* uncommon case where the proved theorem occurs twice |
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
54 |
(e.g., "Transitive_Closure.trancl_into_trancl") *) |
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
55 |
n = 1 andalso name = thm_name then |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
56 |
0 |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
57 |
else |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
58 |
1) |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
59 |
val x' = x |> n' <= 1 ? app n' body' |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
60 |
in (x' |> n = 1 ? f (name, prop, body')) end) |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
61 |
in fold (app 0) end |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
62 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
63 |
fun theorems_mentioned_in_proof_term all_names thm = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
64 |
let |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
65 |
fun collect (s, _, _) = if s <> "" then insert (op =) s else I |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
66 |
val names = |
43498
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
67 |
[] |> fold_body_thms (Thm.get_name_hint thm) all_names collect |
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset
|
68 |
[Thm.proof_body_of thm] |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
69 |
|> map fact_name_of |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
70 |
in names end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
71 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
72 |
fun interesting_const_names ctxt = |
43276 | 73 |
let val thy = Proof_Context.theory_of ctxt in |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
74 |
Sledgehammer_Filter.const_names_in_fact thy |
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 |
(Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
76 |
end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
77 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
78 |
fun generate_tptp_graph_file_for_theory ctxt thy file_name = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
79 |
let |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
80 |
val path = file_name |> Path.explode |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
81 |
val _ = File.write path "" |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
82 |
val axioms = Theory.all_axioms_of thy |> map fst |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
83 |
fun do_thm thm = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
84 |
let |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
85 |
val name = Thm.get_name_hint thm |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
86 |
val s = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
87 |
"[" ^ Thm.legacy_get_kind thm ^ "] " ^ |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
88 |
(if member (op =) axioms name then "A" else "T") ^ " " ^ |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
89 |
prefix fact_prefix (ascii_of name) ^ ": " ^ |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
90 |
commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^ |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
91 |
commas (map (prefix const_prefix o ascii_of) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
92 |
(interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
93 |
in File.append path s end |
43245 | 94 |
val thms = facts_of thy |> map snd |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
95 |
val _ = map do_thm thms |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
96 |
in () end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
97 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
98 |
fun inference_term [] = NONE |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
99 |
| inference_term ss = |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
100 |
ATerm ("inference", |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
101 |
[ATerm ("isabelle", []), |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
102 |
ATerm (tptp_empty_list, []), |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
103 |
ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)]) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
104 |
|> SOME |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
105 |
fun inference infers ident = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
106 |
these (AList.lookup (op =) infers ident) |> inference_term |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
107 |
fun add_inferences_to_problem_line infers |
46406 | 108 |
(Formula (ident, Axiom, phi, NONE, tms)) = |
109 |
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
|
110 |
| add_inferences_to_problem_line _ line = line |
43996 | 111 |
fun add_inferences_to_problem infers = |
112 |
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
|
113 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
114 |
fun ident_of_problem_line (Decl (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
|
115 |
| 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
|
116 |
|
45305 | 117 |
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
|
118 |
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
|
119 |
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
|
120 |
val prob_file = File.tmp_path (Path.explode "prob") |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
121 |
val atp = case format of DFG _ => spass_newN | _ => eN |
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47055
diff
changeset
|
122 |
val {exec, arguments, proof_delims, known_failures, ...} = |
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47055
diff
changeset
|
123 |
get_atp thy atp () |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
124 |
val ord = effective_term_order ctxt atp |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
125 |
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
|
126 |
|> File.write_list prob_file |
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
|
127 |
val command = |
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
|
128 |
File.shell_path (Path.explode (getenv (hd (fst exec)) ^ "/" ^ snd exec)) ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
129 |
" " ^ 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
|
130 |
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
|
131 |
in |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43828
diff
changeset
|
132 |
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
|
133 |
|> fst |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
134 |
|> 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
|
135 |
|> 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
|
136 |
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
|
137 |
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
|
138 |
|
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
139 |
val likely_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
|
140 |
[@{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
|
141 |
|> 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
|
142 |
|
45305 | 143 |
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
|
144 |
exists (fn prefix => String.isPrefix prefix ident) |
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset
|
145 |
likely_tautology_prefixes andalso |
45305 | 146 |
is_none (run_some_atp ctxt format |
46406 | 147 |
[(factsN, [Formula (ident, Conjecture, phi, NONE, [])])]) |
45305 | 148 |
| 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
|
149 |
|
43499 | 150 |
fun order_facts ord = sort (ord o pairself ident_of_problem_line) |
151 |
fun order_problem_facts _ [] = [] |
|
152 |
| order_problem_facts ord ((heading, lines) :: problem) = |
|
153 |
if heading = factsN then (heading, order_facts ord lines) :: problem |
|
154 |
else (heading, lines) :: order_problem_facts ord problem |
|
155 |
||
45305 | 156 |
(* A fairly random selection of types used for monomorphizing. *) |
157 |
val ground_types = |
|
158 |
[@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool}, |
|
159 |
@{typ unit}] |
|
160 |
||
161 |
fun ground_type_for_tvar _ [] tvar = |
|
162 |
raise TYPE ("ground_type_for_sorts", [TVar tvar], []) |
|
163 |
| ground_type_for_tvar thy (T :: Ts) tvar = |
|
164 |
if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T |
|
165 |
else ground_type_for_tvar thy Ts tvar |
|
166 |
||
167 |
fun monomorphize_term ctxt t = |
|
168 |
let val thy = Proof_Context.theory_of ctxt in |
|
169 |
t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types)) |
|
170 |
handle TYPE _ => @{prop True} |
|
171 |
end |
|
172 |
||
173 |
fun generate_tptp_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
|
174 |
let |
46301 | 175 |
val type_enc = type_enc |> type_enc_from_string Strict |
45305 | 176 |
|> adjust_type_enc format |
177 |
val mono = polymorphism_of_type_enc type_enc <> Polymorphic |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
178 |
val path = file_name |> Path.explode |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
179 |
val _ = File.write path "" |
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
|
180 |
val facts = facts_of thy |
45551 | 181 |
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
|
182 |
facts |
45305 | 183 |
|> map (fn ((_, loc), th) => |
184 |
((Thm.get_name_hint th, loc), |
|
185 |
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
|
186 |
|> 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
|
187 |
false true [] @{prop False} |
45551 | 188 |
|> #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
|
189 |
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
|
190 |
atp_problem |
45305 | 191 |
|> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) |
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
|
192 |
val all_names = facts |> map (Thm.get_name_hint o snd) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
193 |
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
|
194 |
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
|
195 |
(fact_name_of (Thm.get_name_hint 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
|
196 |
theorems_mentioned_in_proof_term (SOME all_names) th)) |
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
197 |
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
|
198 |
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
|
199 |
val infers = |
43499 | 200 |
infers |> filter (member (op =) all_atp_problem_names o fst) |
201 |
|> map (apsnd (filter (member (op =) all_atp_problem_names))) |
|
202 |
val ordered_names = |
|
203 |
String_Graph.empty |
|
204 |
|> fold (String_Graph.new_node o rpair ()) all_atp_problem_names |
|
205 |
|> 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
|
206 |
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
|
207 |
infers |
43499 | 208 |
|> String_Graph.topological_order |
209 |
val order_tab = |
|
210 |
Symtab.empty |
|
211 |
|> fold (Symtab.insert (op =)) |
|
212 |
(ordered_names ~~ (1 upto length ordered_names)) |
|
213 |
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab) |
|
214 |
val atp_problem = |
|
45305 | 215 |
atp_problem |
216 |
|> (case format of DFG _ => I | _ => add_inferences_to_problem infers) |
|
217 |
|> order_problem_facts name_ord |
|
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
218 |
val ord = effective_term_order ctxt eN (* dummy *) |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
219 |
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
|
220 |
val _ = app (File.append path) ss |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
221 |
in () end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
222 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
223 |
end; |