author | blanchet |
Mon, 09 Jul 2012 23:23:12 +0200 | |
changeset 48217 | 8994afe09c18 |
parent 48216 | 9075d4636dd8 |
child 48218 | 6a797139f0b2 |
permissions | -rw-r--r-- |
46321 | 1 |
(* Title: HOL/TPTP/ATP_Theory_Export.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* ATP Theory Exporter *} |
|
6 |
||
7 |
theory ATP_Theory_Export |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
8 |
imports "~~/src/HOL/Sledgehammer2d" Complex_Main (* ### *) |
46321 | 9 |
uses "atp_theory_export.ML" |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
10 |
begin |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
11 |
|
42607
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset
|
12 |
ML {* |
45305 | 13 |
open ATP_Problem; |
46321 | 14 |
open ATP_Theory_Export; |
45305 | 15 |
*} |
16 |
||
17 |
ML {* |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
18 |
val do_it = true (* false ### *); (* switch to "true" to generate the files *) |
48216 | 19 |
val thy = @{theory Nat}; (* @{theory Complex_Main}; ### *) |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
20 |
val ctxt = @{context} |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
21 |
*} |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
22 |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
23 |
|
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
24 |
(* MaSh *) |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
25 |
|
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
26 |
ML {* |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
27 |
if do_it then |
48216 | 28 |
"/tmp/mash_sample_problem.out" |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
29 |
|> generate_mash_problem_file_for_theory thy |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
30 |
else |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
31 |
() |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
32 |
*} |
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
33 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
34 |
ML {* |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
35 |
if do_it then |
48216 | 36 |
"/tmp/mash_accessibility.out" |
37 |
|> generate_mash_accessibility_file_for_theory thy false |
|
38 |
else |
|
39 |
() |
|
40 |
*} |
|
41 |
||
42 |
ML {* |
|
43 |
if do_it then |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
44 |
"/tmp/mash_features.out" |
48216 | 45 |
|> generate_mash_feature_file_for_theory thy false |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
46 |
else |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
47 |
() |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
48 |
*} |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
49 |
|
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
50 |
ML {* |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
51 |
if do_it then |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
52 |
"/tmp/mash_dependencies.out" |
48216 | 53 |
|> generate_mash_dependency_file_for_theory thy false |
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
54 |
else |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
55 |
() |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
56 |
*} |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
57 |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
58 |
|
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
59 |
(* TPTP/DFG *) |
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
60 |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
61 |
ML {* |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
62 |
if do_it then |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
63 |
"/tmp/infs_poly_guards_query_query.tptp" |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
64 |
|> generate_tptp_inference_file_for_theory ctxt thy FOF |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
65 |
"poly_guards_query_query" |
43400
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
66 |
else |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
67 |
() |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
68 |
*} |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
69 |
|
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
70 |
ML {* |
3d03f4472883
use more appropriate type systems for ATP exporter
blanchet
parents:
43223
diff
changeset
|
71 |
if do_it then |
48145 | 72 |
"/tmp/infs_poly_tags_query_query.tptp" |
73 |
|> generate_tptp_inference_file_for_theory ctxt thy FOF |
|
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
74 |
"poly_tags_query_query" |
45305 | 75 |
else |
76 |
() |
|
77 |
*} |
|
78 |
||
79 |
ML {* |
|
80 |
if do_it then |
|
48213
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
81 |
"/tmp/axs_tc_native.dfg" |
d20add034f64
first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents:
48145
diff
changeset
|
82 |
|> generate_tptp_inference_file_for_theory ctxt thy (DFG Polymorphic) |
48217
8994afe09c18
more precise dependencies -- eliminate tautologies
blanchet
parents:
48216
diff
changeset
|
83 |
"tc_native" |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
84 |
else |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42607
diff
changeset
|
85 |
() |
42607
c8673078f915
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents:
42602
diff
changeset
|
86 |
*} |
42602
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
87 |
|
a2db47fa015e
added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff
changeset
|
88 |
end |