author | blanchet |
Tue, 10 Jul 2012 23:36:03 +0200 | |
changeset 48233 | 50e00ee405f8 |
parent 48229 | 141ab3c13ac8 |
child 48234 | 06216c789ac9 |
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 |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
5 |
Export Isabelle theories as MaSh (Machine-learning for Sledgehammer) or as |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
6 |
first-order TPTP inferences. |
42602
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 |
48216 | 15 |
val generate_mash_accessibility_file_for_theory : |
16 |
theory -> bool -> string -> unit |
|
17 |
val generate_mash_feature_file_for_theory : theory -> bool -> string -> unit |
|
18 |
val generate_mash_dependency_file_for_theory : |
|
19 |
theory -> bool -> string -> unit |
|
20 |
val generate_mash_problem_file_for_theory : theory -> string -> unit |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
21 |
val generate_tptp_inference_file_for_theory : |
45305 | 22 |
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
|
23 |
end; |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
24 |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
25 |
structure ATP_Theory_Export (* ### : ATP_THEORY_EXPORT *) = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
26 |
struct |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
27 |
|
43479
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
28 |
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
|
29 |
open ATP_Proof |
46320 | 30 |
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
|
31 |
open ATP_Systems |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
32 |
open ATP_Util |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
33 |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
34 |
fun stringN_of_int 0 _ = "" |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
35 |
| stringN_of_int k n = |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
36 |
stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
37 |
|
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
38 |
fun escape_meta_char c = |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
39 |
if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse |
48233 | 40 |
c = #")" orelse c = #"," then |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
41 |
String.str c |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
42 |
else if c = #"'" then |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
43 |
"~" |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
44 |
else |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
45 |
(* fixed width, in case more digits follow *) |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
46 |
"\\" ^ stringN_of_int 3 (Char.ord c) |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
47 |
val escape_meta = String.translate escape_meta_char |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
48 |
|
48225 | 49 |
val thy_prefix = "y_" |
50 |
||
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
51 |
val fact_name_of = escape_meta |
48225 | 52 |
val thy_name_of = prefix thy_prefix o escape_meta |
48216 | 53 |
val const_name_of = prefix const_prefix o escape_meta |
54 |
val type_name_of = prefix type_const_prefix o escape_meta |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
55 |
val class_name_of = prefix class_prefix o escape_meta |
48216 | 56 |
|
57 |
val thy_name_of_thm = theory_of_thm #> Context.theory_name |
|
58 |
||
59 |
fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th) |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
60 |
|
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
|
61 |
(* 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
|
62 |
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
|
63 |
not doing the same? *) |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
64 |
fun fold_body_thms thm_name f = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
65 |
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
|
66 |
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
|
67 |
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
|
68 |
let |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
69 |
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
|
70 |
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
|
71 |
n + (if name = "" orelse |
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
|
72 |
(* 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
|
73 |
(e.g., "Transitive_Closure.trancl_into_trancl") *) |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
74 |
(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
|
75 |
0 |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
76 |
else |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
77 |
1) |
5af1abc13c1f
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
in fold (app 0) end |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
81 |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
82 |
fun theorems_mentioned_in_proof_term all_names th = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
83 |
let |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
84 |
val is_name_ok = |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
85 |
case all_names of |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
86 |
SOME names => member (op =) names |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
87 |
| NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s)) |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
88 |
fun collect (s, _, _) = is_name_ok s ? insert (op =) s |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
89 |
val names = |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
90 |
[] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of 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
|
91 |
|> map fact_name_of |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
92 |
in names end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
93 |
|
48228 | 94 |
fun interesting_terms_types_and_classes term_max_depth type_max_depth t = |
48216 | 95 |
let |
48226 | 96 |
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
97 |
val bad_consts = atp_widely_irrelevant_consts |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
98 |
val add_classes = |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
99 |
subtract (op =) @{sort type} #> map class_name_of #> union (op =) |
48228 | 100 |
fun do_add_type (Type (s, Ts)) = |
48226 | 101 |
(not (member (op =) bad_types s) ? insert (op =) (type_name_of s)) |
48228 | 102 |
#> fold do_add_type Ts |
103 |
| do_add_type (TFree (_, S)) = add_classes S |
|
104 |
| do_add_type (TVar (_, S)) = add_classes S |
|
105 |
fun add_type T = type_max_depth >= 0 ? do_add_type T |
|
48226 | 106 |
fun mk_app s args = |
48233 | 107 |
if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" |
48226 | 108 |
else s |
48233 | 109 |
fun patternify ~1 _ = "" |
48226 | 110 |
| patternify depth t = |
111 |
case strip_comb t of |
|
112 |
(Const (s, _), args) => |
|
113 |
mk_app (const_name_of s) (map (patternify (depth - 1)) args) |
|
48233 | 114 |
| _ => "" |
48228 | 115 |
fun add_term_patterns ~1 _ = I |
116 |
| add_term_patterns depth t = |
|
48226 | 117 |
insert (op =) (patternify depth t) |
118 |
#> add_term_patterns (depth - 1) t |
|
119 |
val add_term = add_term_patterns term_max_depth |
|
120 |
fun add_patterns t = |
|
121 |
let val (head, args) = strip_comb t in |
|
122 |
(case head of |
|
123 |
Const (s, T) => |
|
124 |
not (member (op =) bad_consts s) ? (add_term t #> add_type T) |
|
125 |
| Free (_, T) => add_type T |
|
126 |
| Var (_, T) => add_type T |
|
127 |
| Abs (_, T, body) => add_type T #> add_patterns body |
|
128 |
| _ => I) |
|
129 |
#> fold add_patterns args |
|
130 |
end |
|
131 |
in [] |> add_patterns t |> sort string_ord end |
|
48216 | 132 |
|
48229 | 133 |
fun is_likely_tautology th = |
48233 | 134 |
null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso |
48229 | 135 |
not (Thm.eq_thm_prop (@{thm ext}, th)) |
136 |
||
137 |
fun is_too_meta thy th = |
|
138 |
fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool} |
|
139 |
||
140 |
fun facts_of thy = |
|
141 |
let val ctxt = Proof_Context.init_global thy in |
|
142 |
Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] |
|
143 |
(Sledgehammer_Filter.clasimpset_rule_table_of ctxt) |
|
144 |
|> filter_out ((is_likely_tautology orf is_too_meta thy) o snd) |
|
145 |
|> rev |
|
146 |
end |
|
147 |
||
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
148 |
fun theory_ord p = |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
149 |
if Theory.eq_thy p then EQUAL |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
150 |
else if Theory.subthy p then LESS |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
151 |
else if Theory.subthy (swap p) then GREATER |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
152 |
else EQUAL |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
153 |
|
48216 | 154 |
val thm_ord = theory_ord o pairself theory_of_thm |
155 |
||
156 |
fun parent_thms thy_ths thy = |
|
157 |
Theory.parents_of thy |
|
48225 | 158 |
|> map Context.theory_name |
48216 | 159 |
|> map_filter (AList.lookup (op =) thy_ths) |
160 |
|> map List.last |
|
161 |
|> map (fact_name_of o Thm.get_name_hint) |
|
162 |
||
163 |
val thms_by_thy = |
|
164 |
map (snd #> `thy_name_of_thm) |
|
165 |
#> AList.group (op =) |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
166 |
#> sort (int_ord |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
167 |
o pairself (length o Theory.ancestors_of o theory_of_thm o hd o snd)) |
48216 | 168 |
#> map (apsnd (sort thm_ord)) |
169 |
||
170 |
fun generate_mash_accessibility_file_for_theory thy include_thy file_name = |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
171 |
let |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
172 |
val path = file_name |> Path.explode |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
173 |
val _ = File.write path "" |
48214 | 174 |
fun do_thm th prevs = |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
175 |
let |
48214 | 176 |
val s = th ^ ": " ^ space_implode " " prevs ^ "\n" |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
177 |
val _ = File.append path s |
48214 | 178 |
in [th] end |
179 |
val thy_ths = |
|
180 |
facts_of thy |
|
48216 | 181 |
|> not include_thy ? filter_out (has_thy thy o snd) |
182 |
|> thms_by_thy |
|
48214 | 183 |
fun do_thy ths = |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
184 |
let |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
185 |
val thy = theory_of_thm (hd ths) |
48216 | 186 |
val parents = parent_thms thy_ths thy |
48214 | 187 |
val ths = ths |> map (fact_name_of o Thm.get_name_hint) |
188 |
val _ = fold do_thm ths parents |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
189 |
in () end |
48214 | 190 |
val _ = List.app (do_thy o snd) thy_ths |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
191 |
in () end |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
192 |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
193 |
fun has_bool @{typ bool} = true |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
194 |
| has_bool (Type (_, Ts)) = exists has_bool Ts |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
195 |
| has_bool _ = false |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
196 |
|
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
197 |
fun has_fun (Type (@{type_name fun}, _)) = true |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
198 |
| has_fun (Type (_, Ts)) = exists has_fun Ts |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
199 |
| has_fun _ = false |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
200 |
|
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
201 |
val is_conn = member (op =) |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
202 |
[@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
203 |
@{const_name HOL.implies}, @{const_name Not}, |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
204 |
@{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}, |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
205 |
@{const_name HOL.eq}] |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
206 |
|
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
207 |
val has_bool_arg_const = |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
208 |
exists_Const (fn (c, T) => |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
209 |
not (is_conn c) andalso exists has_bool (binder_types T)) |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
210 |
|
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
211 |
fun higher_inst_const thy (c, T) = |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
212 |
case binder_types T of |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
213 |
[] => false |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
214 |
| Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
215 |
|
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
216 |
val binders = [@{const_name All}, @{const_name Ex}] |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
217 |
|
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
218 |
fun is_fo_term thy t = |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
219 |
let |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
220 |
val t = |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
221 |
t |> Envir.beta_eta_contract |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
222 |
|> transform_elim_prop |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
223 |
|> Object_Logic.atomize_term thy |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
224 |
in |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
225 |
Term.is_first_order binders t andalso |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
226 |
not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
227 |
| _ => false) t orelse |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
228 |
has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t) |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
229 |
end |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
230 |
|
48228 | 231 |
fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
232 |
|
48226 | 233 |
val max_depth = 1 |
234 |
||
48216 | 235 |
fun features_of thy (status, th) = |
48228 | 236 |
let val t = Thm.prop_of th in |
48225 | 237 |
thy_name_of (thy_name_of_thm th) :: |
48228 | 238 |
interesting_terms_types_and_classes max_depth max_depth t |
239 |
|> not (has_no_lambdas t) ? cons "lambdas" |
|
240 |
|> exists_Const is_exists t ? cons "skolems" |
|
241 |
|> not (is_fo_term thy t) ? cons "ho" |
|
48216 | 242 |
|> (case status of |
243 |
General => I |
|
244 |
| Induction => cons "induction" |
|
245 |
| Intro => cons "intro" |
|
246 |
| Inductive => cons "inductive" |
|
247 |
| Elim => cons "elim" |
|
248 |
| Simp => cons "simp" |
|
249 |
| Def => cons "def") |
|
250 |
end |
|
251 |
||
252 |
fun generate_mash_feature_file_for_theory thy include_thy file_name = |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
253 |
let |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
254 |
val path = file_name |> Path.explode |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
255 |
val _ = File.write path "" |
48216 | 256 |
val facts = facts_of thy |> not include_thy ? filter_out (has_thy thy o snd) |
48215 | 257 |
fun do_fact ((_, (_, status)), th) = |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
258 |
let |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
259 |
val name = Thm.get_name_hint th |
48216 | 260 |
val feats = features_of thy (status, th) |
261 |
val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n" |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
262 |
in File.append path s end |
48215 | 263 |
val _ = List.app do_fact facts |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
264 |
in () end |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
265 |
|
48216 | 266 |
val dependencies_of = theorems_mentioned_in_proof_term o SOME |
267 |
||
268 |
fun generate_mash_dependency_file_for_theory thy include_thy file_name = |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
269 |
let |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
270 |
val path = file_name |> Path.explode |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
271 |
val _ = File.write path "" |
48216 | 272 |
val ths = |
273 |
facts_of thy |> not include_thy ? filter_out (has_thy thy o snd) |
|
274 |
|> map snd |
|
48229 | 275 |
val all_names = ths |> map Thm.get_name_hint |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
276 |
fun do_thm th = |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
277 |
let |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
278 |
val name = Thm.get_name_hint th |
48216 | 279 |
val deps = dependencies_of all_names th |
280 |
val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
281 |
in File.append path s end |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
282 |
val _ = List.app do_thm ths |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
283 |
in () end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
284 |
|
48216 | 285 |
fun generate_mash_problem_file_for_theory thy file_name = |
286 |
let |
|
287 |
val path = file_name |> Path.explode |
|
288 |
val _ = File.write path "" |
|
289 |
val facts = facts_of thy |
|
290 |
val (new_facts, old_facts) = |
|
291 |
facts |> List.partition (has_thy thy o snd) |
|
292 |
|>> sort (thm_ord o pairself snd) |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
293 |
val ths = facts |> map snd |
48229 | 294 |
val all_names = ths |> map Thm.get_name_hint |
48216 | 295 |
fun do_fact ((_, (_, status)), th) prevs = |
296 |
let |
|
297 |
val name = Thm.get_name_hint th |
|
298 |
val feats = features_of thy (status, th) |
|
299 |
val deps = dependencies_of all_names th |
|
48233 | 300 |
val kind = Thm.legacy_get_kind th |
301 |
val name = fact_name_of name |
|
302 |
val core = |
|
303 |
name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats |
|
304 |
val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
|
305 |
val update = "! " ^ core ^ "; " ^ space_implode " " deps ^ "\n" |
|
306 |
val _ = File.append path (query ^ update) |
|
307 |
in [name] end |
|
48216 | 308 |
val thy_ths = old_facts |> thms_by_thy |
309 |
val parents = parent_thms thy_ths thy |
|
310 |
val _ = fold do_fact new_facts parents |
|
311 |
in () end |
|
312 |
||
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
313 |
fun inference_term [] = NONE |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
314 |
| inference_term ss = |
48132
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
315 |
ATerm (("inference", []), |
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
316 |
[ATerm (("isabelle", []), []), |
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
317 |
ATerm ((tptp_empty_list, []), []), |
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
318 |
ATerm ((tptp_empty_list, []), |
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
48131
diff
changeset
|
319 |
map (fn s => ATerm ((s, []), [])) ss)]) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
320 |
|> SOME |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
321 |
fun inference infers ident = |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
322 |
these (AList.lookup (op =) infers ident) |> inference_term |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
323 |
fun add_inferences_to_problem_line infers |
46406 | 324 |
(Formula (ident, Axiom, phi, NONE, tms)) = |
325 |
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
|
326 |
| add_inferences_to_problem_line _ line = line |
43996 | 327 |
fun add_inferences_to_problem infers = |
328 |
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
|
329 |
|
48142
efaff8206967
finished implementation of DFG type class output
blanchet
parents:
48140
diff
changeset
|
330 |
fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident |
efaff8206967
finished implementation of DFG type class output
blanchet
parents:
48140
diff
changeset
|
331 |
| ident_of_problem_line (Type_Decl (ident, _, _)) = ident |
48137
6f524f2066e3
cleanly distinguish between type declarations and symbol declarations
blanchet
parents:
48132
diff
changeset
|
332 |
| ident_of_problem_line (Sym_Decl (ident, _, _)) = ident |
48142
efaff8206967
finished implementation of DFG type class output
blanchet
parents:
48140
diff
changeset
|
333 |
| 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
|
334 |
| 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
|
335 |
|
45305 | 336 |
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
|
337 |
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
|
338 |
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
|
339 |
val prob_file = File.tmp_path (Path.explode "prob") |
48131 | 340 |
val atp = case format of DFG _ => spassN | _ => eN |
47606
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47055
diff
changeset
|
341 |
val {exec, arguments, proof_delims, known_failures, ...} = |
06dde48a1503
true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents:
47055
diff
changeset
|
342 |
get_atp thy atp () |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
343 |
val ord = effective_term_order ctxt atp |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
344 |
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
|
345 |
|> File.write_list prob_file |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
346 |
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
|
347 |
val command = |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48142
diff
changeset
|
348 |
File.shell_path (Path.explode path) ^ |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
349 |
" " ^ 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
|
350 |
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
|
351 |
in |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43828
diff
changeset
|
352 |
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
|
353 |
|> fst |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
354 |
|> 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
|
355 |
|> 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
|
356 |
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
|
357 |
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
|
358 |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
359 |
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
|
360 |
[@{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
|
361 |
|> 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
|
362 |
|
45305 | 363 |
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
|
364 |
exists (fn prefix => String.isPrefix prefix ident) |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
365 |
tautology_prefixes andalso |
45305 | 366 |
is_none (run_some_atp ctxt format |
46406 | 367 |
[(factsN, [Formula (ident, Conjecture, phi, NONE, [])])]) |
45305 | 368 |
| 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
|
369 |
|
43499 | 370 |
fun order_facts ord = sort (ord o pairself ident_of_problem_line) |
371 |
fun order_problem_facts _ [] = [] |
|
372 |
| order_problem_facts ord ((heading, lines) :: problem) = |
|
373 |
if heading = factsN then (heading, order_facts ord lines) :: problem |
|
374 |
else (heading, lines) :: order_problem_facts ord problem |
|
375 |
||
45305 | 376 |
(* A fairly random selection of types used for monomorphizing. *) |
377 |
val ground_types = |
|
378 |
[@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool}, |
|
379 |
@{typ unit}] |
|
380 |
||
381 |
fun ground_type_for_tvar _ [] tvar = |
|
382 |
raise TYPE ("ground_type_for_sorts", [TVar tvar], []) |
|
383 |
| ground_type_for_tvar thy (T :: Ts) tvar = |
|
384 |
if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T |
|
385 |
else ground_type_for_tvar thy Ts tvar |
|
386 |
||
387 |
fun monomorphize_term ctxt t = |
|
388 |
let val thy = Proof_Context.theory_of ctxt in |
|
389 |
t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types)) |
|
390 |
handle TYPE _ => @{prop True} |
|
391 |
end |
|
392 |
||
393 |
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
|
394 |
let |
46301 | 395 |
val type_enc = type_enc |> type_enc_from_string Strict |
45305 | 396 |
|> adjust_type_enc format |
48131 | 397 |
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
|
398 |
val path = file_name |> Path.explode |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
399 |
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
|
400 |
val facts = facts_of thy |
45551 | 401 |
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
|
402 |
facts |
45305 | 403 |
|> map (fn ((_, loc), th) => |
404 |
((Thm.get_name_hint th, loc), |
|
405 |
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
|
406 |
|> 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
|
407 |
false true [] @{prop False} |
45551 | 408 |
|> #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
|
409 |
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
|
410 |
atp_problem |
45305 | 411 |
|> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
412 |
val ths = facts |> map snd |
48229 | 413 |
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
|
414 |
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
|
415 |
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
|
416 |
(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
|
417 |
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
|
418 |
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
|
419 |
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
|
420 |
val infers = |
43499 | 421 |
infers |> filter (member (op =) all_atp_problem_names o fst) |
422 |
|> map (apsnd (filter (member (op =) all_atp_problem_names))) |
|
423 |
val ordered_names = |
|
424 |
String_Graph.empty |
|
425 |
|> fold (String_Graph.new_node o rpair ()) all_atp_problem_names |
|
426 |
|> 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
|
427 |
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
|
428 |
infers |
43499 | 429 |
|> String_Graph.topological_order |
430 |
val order_tab = |
|
431 |
Symtab.empty |
|
432 |
|> fold (Symtab.insert (op =)) |
|
433 |
(ordered_names ~~ (1 upto length ordered_names)) |
|
434 |
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab) |
|
435 |
val atp_problem = |
|
45305 | 436 |
atp_problem |
48131 | 437 |
|> (case format of DFG _ => I | _ => add_inferences_to_problem infers) |
45305 | 438 |
|> order_problem_facts name_ord |
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
439 |
val ord = effective_term_order ctxt eN (* dummy *) |
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset
|
440 |
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
|
441 |
val _ = app (File.append path) ss |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
442 |
in () end |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
443 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
444 |
end; |