src/HOL/TPTP/ATP_Theory_Export.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46435 e9c90516bc0d
child 48129 933d43c31689
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46321
484dc68c8c89 renamed theory exporter
blanchet
parents: 45305
diff changeset
     1
(*  Title:      HOL/TPTP/ATP_Theory_Export.thy
484dc68c8c89 renamed theory exporter
blanchet
parents: 45305
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
484dc68c8c89 renamed theory exporter
blanchet
parents: 45305
diff changeset
     3
*)
484dc68c8c89 renamed theory exporter
blanchet
parents: 45305
diff changeset
     4
484dc68c8c89 renamed theory exporter
blanchet
parents: 45305
diff changeset
     5
header {* ATP Theory Exporter *}
484dc68c8c89 renamed theory exporter
blanchet
parents: 45305
diff changeset
     6
484dc68c8c89 renamed theory exporter
blanchet
parents: 45305
diff changeset
     7
theory ATP_Theory_Export
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
     8
imports Complex_Main
46321
484dc68c8c89 renamed theory exporter
blanchet
parents: 45305
diff changeset
     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
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    13
open ATP_Problem;
46321
484dc68c8c89 renamed theory exporter
blanchet
parents: 45305
diff changeset
    14
open ATP_Theory_Export;
45305
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    15
*}
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    16
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    17
ML {*
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
    18
val do_it = false; (* switch to "true" to generate the files *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    19
val thy = @{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
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    23
ML {*
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    24
if do_it then
46435
e9c90516bc0d renamed type encoding
blanchet
parents: 46321
diff changeset
    25
  "/tmp/axs_mono_native.dfg"
45305
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    26
  |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted)
46435
e9c90516bc0d renamed type encoding
blanchet
parents: 46321
diff changeset
    27
         "mono_native"
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    28
else
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    29
  ()
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
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    32
ML {*
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    33
if do_it then
45305
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    34
  "/tmp/infs_poly_guards.tptp"
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    35
  |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_guards"
43400
3d03f4472883 use more appropriate type systems for ATP exporter
blanchet
parents: 43223
diff changeset
    36
else
3d03f4472883 use more appropriate type systems for ATP exporter
blanchet
parents: 43223
diff changeset
    37
  ()
3d03f4472883 use more appropriate type systems for ATP exporter
blanchet
parents: 43223
diff changeset
    38
*}
3d03f4472883 use more appropriate type systems for ATP exporter
blanchet
parents: 43223
diff changeset
    39
3d03f4472883 use more appropriate type systems for ATP exporter
blanchet
parents: 43223
diff changeset
    40
ML {*
3d03f4472883 use more appropriate type systems for ATP exporter
blanchet
parents: 43223
diff changeset
    41
if do_it then
45305
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    42
  "/tmp/infs_poly_tags.tptp"
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    43
  |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags"
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    44
else
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    45
  ()
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    46
*}
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    47
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    48
ML {*
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    49
if do_it then
45305
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    50
  "/tmp/infs_poly_tags_uniform.tptp"
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    51
  |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags_uniform"
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    52
else
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    53
  ()
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    54
*}
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    55
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    56
ML {*
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    57
if do_it then
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    58
  "/tmp/graph.out" |> generate_tptp_graph_file_for_theory ctxt thy
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    59
else
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42607
diff changeset
    60
  ()
42607
c8673078f915 fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents: 42602
diff changeset
    61
*}
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    62
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    63
end