src/HOL/TPTP/atp_theory_export.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47055 16e2633f3b4b
child 47606 06dde48a1503
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: 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
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
     5
Export Isabelle theories as first-order TPTP inferences, exploiting
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
     6
Sledgehammer's translation.
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
     7
*)
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
     8
46321
484dc68c8c89 renamed theory exporter
blanchet
parents: 46320
diff changeset
     9
signature ATP_THEORY_EXPORT =
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    10
sig
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    11
  type atp_format = ATP_Problem.atp_format
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    12
43494
13eefebbc4cb make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
blanchet
parents: 43479
diff changeset
    13
  val theorems_mentioned_in_proof_term :
13eefebbc4cb make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
blanchet
parents: 43479
diff changeset
    14
    string list option -> thm -> string list
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    15
  val generate_tptp_graph_file_for_theory :
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    16
    Proof.context -> theory -> string -> unit
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    17
  val generate_tptp_inference_file_for_theory :
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
    18
    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
    19
end;
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    20
46321
484dc68c8c89 renamed theory exporter
blanchet
parents: 46320
diff changeset
    21
structure ATP_Theory_Export : ATP_THEORY_EXPORT =
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    22
struct
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    23
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    24
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
    25
open ATP_Proof
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    26
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
    27
open ATP_Systems
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    28
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    29
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
    30
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    31
fun facts_of thy =
46734
6256e064f8fa speed up Sledgehammer's clasimpset lookup a bit
blanchet
parents: 46667
diff changeset
    32
  let val ctxt = Proof_Context.init_global thy in
6256e064f8fa speed up Sledgehammer's clasimpset lookup a bit
blanchet
parents: 46667
diff changeset
    33
    Sledgehammer_Filter.all_facts ctxt false
6256e064f8fa speed up Sledgehammer's clasimpset lookup a bit
blanchet
parents: 46667
diff changeset
    34
        Symtab.empty true [] []
6256e064f8fa speed up Sledgehammer's clasimpset lookup a bit
blanchet
parents: 46667
diff changeset
    35
        (Sledgehammer_Filter.clasimpset_rule_table_of ctxt)
6256e064f8fa speed up Sledgehammer's clasimpset lookup a bit
blanchet
parents: 46667
diff changeset
    36
    |> filter (curry (op =) @{typ bool} o fastype_of
6256e064f8fa speed up Sledgehammer's clasimpset lookup a bit
blanchet
parents: 46667
diff changeset
    37
               o Object_Logic.atomize_term thy o prop_of o snd)
6256e064f8fa speed up Sledgehammer's clasimpset lookup a bit
blanchet
parents: 46667
diff changeset
    38
  end
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    39
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
    40
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
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
    41
   fixes that seem to be missing over there; or maybe the two code portions are
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
    42
   not doing the same? *)
43498
75caf7e4302e peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents: 43494
diff changeset
    43
fun fold_body_thms thm_name all_names f =
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    44
  let
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
    45
    fun app n (PBody {thms, ...}) =
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    46
      thms |> fold (fn (_, (name, prop, body)) => fn x =>
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    47
        let
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    48
          val body' = Future.join body
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    49
          val n' =
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    50
            n + (if name = "" orelse
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    51
                    (is_some all_names andalso
43498
75caf7e4302e peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents: 43494
diff changeset
    52
                     not (member (op =) (the all_names) name)) orelse
75caf7e4302e peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents: 43494
diff changeset
    53
                    (* uncommon case where the proved theorem occurs twice
75caf7e4302e peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents: 43494
diff changeset
    54
                       (e.g., "Transitive_Closure.trancl_into_trancl") *)
75caf7e4302e peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents: 43494
diff changeset
    55
                    n = 1 andalso name = thm_name then
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    56
                   0
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    57
                 else
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    58
                   1)
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    59
          val x' = x |> n' <= 1 ? app n' body'
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    60
        in (x' |> n = 1 ? f (name, prop, body')) end)
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    61
  in fold (app 0) end
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    62
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    63
fun theorems_mentioned_in_proof_term all_names thm =
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    64
  let
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    65
    fun collect (s, _, _) = if s <> "" then insert (op =) s else I
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    66
    val names =
43498
75caf7e4302e peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents: 43494
diff changeset
    67
      [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect
75caf7e4302e peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents: 43494
diff changeset
    68
                           [Thm.proof_body_of thm]
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    69
         |> map fact_name_of
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    70
  in names end
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    71
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    72
fun interesting_const_names ctxt =
43276
91bf67e0e755 modernized Proof_Context;
wenzelm
parents: 43259
diff changeset
    73
  let val thy = Proof_Context.theory_of ctxt in
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    74
    Sledgehammer_Filter.const_names_in_fact thy
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
    75
        (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN)
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    76
  end
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    77
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    78
fun generate_tptp_graph_file_for_theory ctxt thy file_name =
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    79
  let
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    80
    val path = file_name |> Path.explode
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    81
    val _ = File.write path ""
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    82
    val axioms = Theory.all_axioms_of thy |> map fst
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    83
    fun do_thm thm =
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    84
      let
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    85
        val name = Thm.get_name_hint thm
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    86
        val s =
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    87
          "[" ^ Thm.legacy_get_kind thm ^ "] " ^
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    88
          (if member (op =) axioms name then "A" else "T") ^ " " ^
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    89
          prefix fact_prefix (ascii_of name) ^ ": " ^
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    90
          commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
    91
          commas (map (prefix const_prefix o ascii_of)
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    92
                      (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    93
      in File.append path s end
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43224
diff changeset
    94
    val thms = facts_of thy |> map snd
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    95
    val _ = map do_thm thms
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    96
  in () end
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    97
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    98
fun inference_term [] = NONE
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
    99
  | inference_term ss =
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
   100
    ATerm ("inference",
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
   101
           [ATerm ("isabelle", []),
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
   102
            ATerm (tptp_empty_list, []),
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
   103
            ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)])
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   104
    |> SOME
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   105
fun inference infers ident =
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   106
  these (AList.lookup (op =) infers ident) |> inference_term
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   107
fun add_inferences_to_problem_line infers
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46365
diff changeset
   108
                                   (Formula (ident, Axiom, phi, NONE, tms)) =
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46365
diff changeset
   109
    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
   110
  | add_inferences_to_problem_line _ line = line
43996
4d1270ddf042 make SML/NJ happy
blanchet
parents: 43863
diff changeset
   111
fun add_inferences_to_problem infers =
4d1270ddf042 make SML/NJ happy
blanchet
parents: 43863
diff changeset
   112
  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
   113
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
   114
fun ident_of_problem_line (Decl (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
   115
  | 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
   116
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   117
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
   118
  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
   119
    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
   120
    val prob_file = File.tmp_path (Path.explode "prob")
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   121
    val atp = case format of DFG _ => spass_newN | _ => eN
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   122
    val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   123
    val ord = effective_term_order ctxt atp
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   124
    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
   125
                    |> File.write_list prob_file
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
   126
    val command =
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
   127
      File.shell_path (Path.explode (getenv (hd (fst exec)) ^ "/" ^ snd exec)) ^
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   128
      " " ^ 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
   129
      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
   130
  in
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43828
diff changeset
   131
    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
   132
    |> fst
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   133
    |> 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
   134
    |> 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
   135
  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
   136
  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
   137
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43499
diff changeset
   138
val likely_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
   139
  [@{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
   140
  |> 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
   141
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   142
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
   143
    exists (fn prefix => String.isPrefix prefix ident)
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43499
diff changeset
   144
           likely_tautology_prefixes andalso
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   145
    is_none (run_some_atp ctxt format
46406
0e490b9e8422 extended SPASS/DFG output with ranks
blanchet
parents: 46365
diff changeset
   146
                 [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])])
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   147
  | 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
   148
43499
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   149
fun order_facts ord = sort (ord o pairself ident_of_problem_line)
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   150
fun order_problem_facts _ [] = []
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   151
  | order_problem_facts ord ((heading, lines) :: problem) =
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   152
    if heading = factsN then (heading, order_facts ord lines) :: problem
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   153
    else (heading, lines) :: order_problem_facts ord problem
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   154
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   155
(* A fairly random selection of types used for monomorphizing. *)
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   156
val ground_types =
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   157
  [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool},
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   158
   @{typ unit}]
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   159
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   160
fun ground_type_for_tvar _ [] tvar =
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   161
    raise TYPE ("ground_type_for_sorts", [TVar tvar], [])
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   162
  | ground_type_for_tvar thy (T :: Ts) tvar =
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   163
    if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   164
    else ground_type_for_tvar thy Ts tvar
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   165
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   166
fun monomorphize_term ctxt t =
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   167
  let val thy = Proof_Context.theory_of ctxt in
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   168
    t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types))
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   169
    handle TYPE _ => @{prop True}
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   170
  end
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   171
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   172
fun generate_tptp_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
   173
  let
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 45551
diff changeset
   174
    val type_enc = type_enc |> type_enc_from_string Strict
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   175
                            |> adjust_type_enc format
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   176
    val mono = polymorphism_of_type_enc type_enc <> Polymorphic
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   177
    val path = file_name |> Path.explode
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   178
    val _ = File.write path ""
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
   179
    val facts = facts_of thy
45551
a62c7a21f4ab removed needless baggage
blanchet
parents: 45508
diff changeset
   180
    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
   181
      facts
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   182
      |> map (fn ((_, loc), th) =>
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   183
                 ((Thm.get_name_hint th, loc),
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   184
                   th |> prop_of |> mono ? monomorphize_term ctxt))
46365
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46321
diff changeset
   185
      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46406
diff changeset
   186
                             false true [] @{prop False}
45551
a62c7a21f4ab removed needless baggage
blanchet
parents: 45508
diff changeset
   187
      |> #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
   188
    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
   189
      atp_problem
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   190
      |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
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
   191
    val all_names = facts |> map (Thm.get_name_hint o snd)
42602
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   192
    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
   193
      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
   194
                       (fact_name_of (Thm.get_name_hint 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
   195
                        theorems_mentioned_in_proof_term (SOME all_names) th))
43479
5af1abc13c1f only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
blanchet
parents: 43468
diff changeset
   196
    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
   197
      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
   198
    val infers =
43499
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   199
      infers |> filter (member (op =) all_atp_problem_names o fst)
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   200
             |> map (apsnd (filter (member (op =) all_atp_problem_names)))
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   201
    val ordered_names =
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   202
      String_Graph.empty
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   203
      |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   204
      |> 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
   205
                  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
   206
              infers
43499
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   207
      |> String_Graph.topological_order
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   208
    val order_tab =
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   209
      Symtab.empty
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   210
      |> fold (Symtab.insert (op =))
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   211
              (ordered_names ~~ (1 upto length ordered_names))
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   212
    val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
9ca694caa61b order generated facts topologically
blanchet
parents: 43498
diff changeset
   213
    val atp_problem =
45305
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   214
      atp_problem
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   215
      |> (case format of DFG _ => I | _ => add_inferences_to_problem infers)
3e09961326ce also export DFG formats
blanchet
parents: 45301
diff changeset
   216
      |> order_problem_facts name_ord
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   217
    val ord = effective_term_order ctxt eN (* dummy *)
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 46734
diff changeset
   218
    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
   219
    val _ = app (File.append path) ss
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   220
  in () end
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   221
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning
blanchet
parents:
diff changeset
   222
end;