author | haftmann |
Fri, 20 Oct 2017 20:57:55 +0200 | |
changeset 66888 | 930abfdf8727 |
parent 63167 | 0909deb8059b |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
46321 | 1 |
(* Title: HOL/TPTP/ATP_Theory_Export.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
*) |
|
4 |
||
63167 | 5 |
section \<open>ATP Theory Exporter\<close> |
46321 | 6 |
|
7 |
theory ATP_Theory_Export |
|
51648
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
8 |
imports Complex_Main |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
9 |
begin |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
10 |
|
48891 | 11 |
ML_file "atp_theory_export.ML" |
12 |
||
63167 | 13 |
ML \<open> |
48375 | 14 |
open ATP_Problem |
15 |
open ATP_Theory_Export |
|
63167 | 16 |
\<close> |
45305 | 17 |
|
63167 | 18 |
ML \<open> |
51648
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
19 |
val do_it = false (* switch to "true" to generate the files *) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
20 |
val ctxt = @{context} |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
58889
diff
changeset
|
21 |
val thy = @{theory Complex_Main} |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
58889
diff
changeset
|
22 |
val infer_policy = (* Unchecked_Inferences *) No_Inferences |
63167 | 23 |
\<close> |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
58889
diff
changeset
|
24 |
|
63167 | 25 |
ML \<open> |
61323
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
58889
diff
changeset
|
26 |
if do_it then |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
58889
diff
changeset
|
27 |
"/tmp/isa_filter" |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
58889
diff
changeset
|
28 |
|> generate_casc_lbt_isa_files_for_theory ctxt thy (THF (Polymorphic, THF_Without_Choice)) |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
58889
diff
changeset
|
29 |
infer_policy "poly_native_higher" |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
58889
diff
changeset
|
30 |
else |
99b3a17a7eab
extended theory exporter to also export MePo-selected facts
blanchet
parents:
58889
diff
changeset
|
31 |
() |
63167 | 32 |
\<close> |
51648
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
33 |
|
63167 | 34 |
ML \<open> |
51648
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
35 |
if do_it then |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
36 |
"/tmp/axs_tc_native.dfg" |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
37 |
|> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic) |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
38 |
infer_policy "tc_native" |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
39 |
else |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
40 |
() |
63167 | 41 |
\<close> |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
42 |
|
63167 | 43 |
ML \<open> |
51648
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
44 |
if do_it then |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
45 |
"/tmp/infs_poly_guards_query_query.tptp" |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
46 |
|> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
47 |
"poly_guards??" |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
48 |
else |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
49 |
() |
63167 | 50 |
\<close> |
48301 | 51 |
|
63167 | 52 |
ML \<open> |
51648
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
53 |
if do_it then |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
54 |
"/tmp/infs_poly_tags_query_query.tptp" |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
55 |
|> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
56 |
"poly_tags??" |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
57 |
else |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
58 |
() |
63167 | 59 |
\<close> |
51646 | 60 |
|
63167 | 61 |
ML \<open> |
51648
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
62 |
if do_it then |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
63 |
"/tmp/casc_ltb_isa" |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
64 |
|> generate_casc_lbt_isa_files_for_theory ctxt thy FOF infer_policy |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
65 |
"poly_tags??" |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
66 |
else |
3e09226c3378
reverted accidental changes to theory file + updated wrt ML file
blanchet
parents:
51646
diff
changeset
|
67 |
() |
63167 | 68 |
\<close> |
43400
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
69 |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
70 |
end |