src/HOL/TPTP/atp_theory_export.ML
author blanchet
Wed, 18 Jul 2012 08:44:03 +0200
changeset 48299 5e5c6616f0fe
parent 48251 6cdcfbddc077
child 48301 e5c5037a3104
permissions -rw-r--r--
centrally construct expensive data structures
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46321
484dc68c8c89 renamed theory exporter
blanchet
parents: 46320
diff changeset
     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
48234
06216c789ac9 moved MaSh into own files
blanchet
parents: 48233
diff changeset
     5
Export Isabelle theories as first-order TPTP inferences.
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
     6
*)
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
     7
46321
484dc68c8c89 renamed theory exporter
blanchet
parents: 46320
diff changeset
     8
signature ATP_THEORY_EXPORT =
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
     9
sig
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    10
  type atp_format = ATP_Problem.atp_format
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    11
48234
06216c789ac9 moved MaSh into own files
blanchet
parents: 48233
diff changeset
    12
  val generate_atp_inference_file_for_theory :
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    13
    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
    14
end;
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    15
48234
06216c789ac9 moved MaSh into own files
blanchet
parents: 48233
diff changeset
    16
structure ATP_Theory_Export : ATP_THEORY_EXPORT =
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    17
struct
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    18
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    19
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
    20
open ATP_Proof
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    21
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
    22
open ATP_Systems
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    23
48234
06216c789ac9 moved MaSh into own files
blanchet
parents: 48233
diff changeset
    24
val fact_name_of = prefix fact_prefix o ascii_of
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    25
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    26
fun inference_term [] = NONE
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    27
  | inference_term ss =
48132
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
    28
    ATerm (("inference", []),
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
    29
           [ATerm (("isabelle", []), []),
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
    30
            ATerm ((tptp_empty_list, []), []),
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
    31
            ATerm ((tptp_empty_list, []),
9aa0fad4e864 added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents: 48131
diff changeset
    32
            map (fn s => ATerm ((s, []), [])) ss)])
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    33
    |> SOME
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    34
fun inference infers ident =
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    35
  these (AList.lookup (op =) infers ident) |> inference_term
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    36
fun add_inferences_to_problem_line infers
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46365
diff changeset
    37
                                   (Formula (ident, Axiom, phi, NONE, tms)) =
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46365
diff changeset
    38
    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
    39
  | add_inferences_to_problem_line _ line = line
43996
4d1270ddf042 make SML/NJ happy
blanchet
parents: 43863
diff changeset
    40
fun add_inferences_to_problem infers =
4d1270ddf042 make SML/NJ happy
blanchet
parents: 43863
diff changeset
    41
  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
    42
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48140
diff changeset
    43
fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48140
diff changeset
    44
  | ident_of_problem_line (Type_Decl (ident, _, _)) = ident
48137
6f524f2066e3 cleanly distinguish between type declarations and symbol declarations
blanchet
parents: 48132
diff changeset
    45
  | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
48142
efaff8206967 finished implementation of DFG type class output
blanchet
parents: 48140
diff changeset
    46
  | 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
    47
  | 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
    48
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    49
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
    50
  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
    51
    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
    52
    val prob_file = File.tmp_path (Path.explode "prob")
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
    53
    val atp = case format of DFG _ => spassN | _ => eN
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47055
diff changeset
    54
    val {exec, arguments, proof_delims, known_failures, ...} =
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47055
diff changeset
    55
      get_atp thy atp ()
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
    56
    val ord = effective_term_order ctxt atp
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
    57
    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
    58
                    |> File.write_list prob_file
48213
d20add034f64 first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents: 48142
diff changeset
    59
    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
    60
    val command =
48213
d20add034f64 first go at generating files for MaSh (machine-learning Sledgehammer)
blanchet
parents: 48142
diff changeset
    61
      File.shell_path (Path.explode path) ^
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
    62
      " " ^ 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
    63
      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
    64
  in
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43828
diff changeset
    65
    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
    66
    |> fst
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
    67
    |> 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
    68
    |> 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
    69
  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
    70
  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
    71
48217
8994afe09c18 more precise dependencies -- eliminate tautologies
blanchet
parents: 48216
diff changeset
    72
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
    73
  [@{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
    74
  |> 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
    75
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    76
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
    77
    exists (fn prefix => String.isPrefix prefix ident)
48217
8994afe09c18 more precise dependencies -- eliminate tautologies
blanchet
parents: 48216
diff changeset
    78
           tautology_prefixes andalso
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    79
    is_none (run_some_atp ctxt format
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46365
diff changeset
    80
                 [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])])
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    81
  | 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
    82
43499
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
    83
fun order_facts ord = sort (ord o pairself ident_of_problem_line)
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
    84
fun order_problem_facts _ [] = []
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
    85
  | order_problem_facts ord ((heading, lines) :: problem) =
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
    86
    if heading = factsN then (heading, order_facts ord lines) :: problem
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
    87
    else (heading, lines) :: order_problem_facts ord problem
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
    88
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    89
(* A fairly random selection of types used for monomorphizing. *)
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    90
val ground_types =
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    91
  [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool},
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    92
   @{typ unit}]
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    93
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    94
fun ground_type_for_tvar _ [] tvar =
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    95
    raise TYPE ("ground_type_for_sorts", [TVar tvar], [])
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    96
  | ground_type_for_tvar thy (T :: Ts) tvar =
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    97
    if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    98
    else ground_type_for_tvar thy Ts tvar
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    99
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   100
fun monomorphize_term ctxt t =
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   101
  let val thy = Proof_Context.theory_of ctxt in
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   102
    t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types))
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   103
    handle TYPE _ => @{prop True}
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   104
  end
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   105
48234
06216c789ac9 moved MaSh into own files
blanchet
parents: 48233
diff changeset
   106
fun generate_atp_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
   107
  let
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48251
diff changeset
   108
    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 45551
diff changeset
   109
    val type_enc = type_enc |> type_enc_from_string Strict
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   110
                            |> adjust_type_enc format
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   111
    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
   112
    val path = file_name |> Path.explode
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   113
    val _ = File.write path ""
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48251
diff changeset
   114
    val facts = Sledgehammer_Fact.all_facts_of thy css_table
45551
a62c7a21f4ab removed needless baggage
blanchet
parents: 45508
diff changeset
   115
    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
   116
      facts
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   117
      |> map (fn ((_, loc), th) =>
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   118
                 ((Thm.get_name_hint th, loc),
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   119
                   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
   120
      |> 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
   121
                             false true [] @{prop False}
45551
a62c7a21f4ab removed needless baggage
blanchet
parents: 45508
diff changeset
   122
      |> #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
   123
    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
   124
      atp_problem
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   125
      |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
48217
8994afe09c18 more precise dependencies -- eliminate tautologies
blanchet
parents: 48216
diff changeset
   126
    val ths = facts |> map snd
48229
141ab3c13ac8 better tautology elimination
blanchet
parents: 48228
diff changeset
   127
    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
   128
    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
   129
      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
   130
                       (fact_name_of (Thm.get_name_hint th),
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48250
diff changeset
   131
                        th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
48234
06216c789ac9 moved MaSh into own files
blanchet
parents: 48233
diff changeset
   132
                           |> map fact_name_of))
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
   133
    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
   134
      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
   135
    val infers =
43499
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   136
      infers |> filter (member (op =) all_atp_problem_names o fst)
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   137
             |> map (apsnd (filter (member (op =) all_atp_problem_names)))
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   138
    val ordered_names =
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   139
      String_Graph.empty
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   140
      |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   141
      |> 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
   142
                  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
   143
              infers
43499
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   144
      |> String_Graph.topological_order
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   145
    val order_tab =
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   146
      Symtab.empty
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   147
      |> fold (Symtab.insert (op =))
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   148
              (ordered_names ~~ (1 upto length ordered_names))
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   149
    val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   150
    val atp_problem =
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   151
      atp_problem
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   152
      |> (case format of DFG _ => I | _ => add_inferences_to_problem infers)
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   153
      |> order_problem_facts name_ord
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   154
    val ord = effective_term_order ctxt eN (* dummy *)
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   155
    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
   156
    val _ = app (File.append path) ss
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   157
  in () end
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   158
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   159
end;