src/HOL/TPTP/ATP_Theory_Export.thy
author wenzelm
Sun, 05 Oct 2014 22:18:40 +0200
changeset 58550 f65911a725ba
parent 51648 3e09226c3378
child 58889 5b7a9633cfa8
permissions -rw-r--r--
more explicit syntax, to avoid misunderstanding of foo-bar as 3 separate arguments;
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
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
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48375
diff changeset
    11
ML_file "atp_theory_export.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48375
diff changeset
    12
42607
c8673078f915 fix ROOT.ML and handle "readable_names" reference slightly more cleanly
blanchet
parents: 42602
diff changeset
    13
ML {*
48375
blanchet
parents: 48302
diff changeset
    14
open ATP_Problem
blanchet
parents: 48302
diff changeset
    15
open ATP_Theory_Export
45305
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    16
*}
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    17
3e09961326ce also export DFG formats
blanchet
parents: 44402
diff changeset
    18
ML {*
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}
51648
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    21
val thy = @{theory List}
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    22
val infer_policy = Unchecked_Inferences
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    23
*}
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    24
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    25
ML {*
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    26
if do_it then
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    27
  "/tmp/axs_tc_native.dfg"
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    28
  |> 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
    29
         infer_policy "tc_native"
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    30
else
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
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 {*
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/infs_poly_guards_query_query.tptp"
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 FOF infer_policy
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    38
         "poly_guards??"
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
  ()
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48239
diff changeset
    41
*}
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48239
diff changeset
    42
51648
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    43
ML {*
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_tags_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_tags??"
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
  ()
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    50
*}
51646
005b7682178b work on CASC LTB ISA exporter
blanchet
parents: 51645
diff changeset
    51
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48239
diff changeset
    52
ML {*
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/casc_ltb_isa"
3e09226c3378 reverted accidental changes to theory file + updated wrt ML file
blanchet
parents: 51646
diff changeset
    55
  |> 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
    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
  ()
43400
3d03f4472883 use more appropriate type systems for ATP exporter
blanchet
parents: 43223
diff changeset
    59
*}
3d03f4472883 use more appropriate type systems for ATP exporter
blanchet
parents: 43223
diff changeset
    60
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    61
end