src/HOL/TPTP/atp_theory_export.ML
author blanchet
Tue Jun 24 15:08:19 2014 +0200 (2014-06-24)
changeset 57306 ff10067b2248
parent 57268 027feff882c4
child 57307 7938a6881b26
permissions -rw-r--r--
optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet@46321
     1
(*  Title:      HOL/TPTP/atp_theory_export.ML
blanchet@42602
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@42602
     3
    Copyright   2011
blanchet@42602
     4
blanchet@48234
     5
Export Isabelle theories as first-order TPTP inferences.
blanchet@42602
     6
*)
blanchet@42602
     7
blanchet@46321
     8
signature ATP_THEORY_EXPORT =
blanchet@42602
     9
sig
blanchet@45305
    10
  type atp_format = ATP_Problem.atp_format
blanchet@45305
    11
blanchet@51646
    12
  datatype inference_policy =
blanchet@51646
    13
    No_Inferences | Unchecked_Inferences | Checked_Inferences
blanchet@51646
    14
blanchet@48234
    15
  val generate_atp_inference_file_for_theory :
blanchet@51646
    16
    Proof.context -> theory -> atp_format -> inference_policy -> string
blanchet@51646
    17
    -> string -> unit
blanchet@51646
    18
  val generate_casc_lbt_isa_files_for_theory :
blanchet@51646
    19
    Proof.context -> theory -> atp_format -> inference_policy -> string
blanchet@51646
    20
    -> string -> unit
blanchet@42602
    21
end;
blanchet@42602
    22
blanchet@48234
    23
structure ATP_Theory_Export : ATP_THEORY_EXPORT =
blanchet@42602
    24
struct
blanchet@42602
    25
blanchet@43479
    26
open ATP_Problem
blanchet@43566
    27
open ATP_Proof
blanchet@46320
    28
open ATP_Problem_Generate
blanchet@43566
    29
open ATP_Systems
blanchet@42602
    30
blanchet@51646
    31
datatype inference_policy =
blanchet@51646
    32
  No_Inferences | Unchecked_Inferences | Checked_Inferences
blanchet@42602
    33
wenzelm@53980
    34
val prefix = Library.prefix
blanchet@51646
    35
val fact_name_of = prefix fact_prefix o ascii_of
blanchet@43479
    36
blanchet@54197
    37
fun atp_of_format (THF (Polymorphic, _)) = dummy_thfN
blanchet@54197
    38
  | atp_of_format (THF (Monomorphic, _)) = satallaxN
blanchet@54788
    39
  | atp_of_format (DFG Polymorphic) = spass_pirateN
blanchet@51998
    40
  | atp_of_format (DFG Monomorphic) = spassN
blanchet@52995
    41
  | atp_of_format (TFF Polymorphic) = alt_ergoN
blanchet@52995
    42
  | atp_of_format (TFF Monomorphic) = vampireN
blanchet@51998
    43
  | atp_of_format FOF = eN
blanchet@51998
    44
  | atp_of_format CNF_UEQ = waldmeisterN
blanchet@51998
    45
  | atp_of_format CNF = eN
blanchet@48318
    46
blanchet@51646
    47
val atp_timeout = seconds 0.5
blanchet@51646
    48
blanchet@51646
    49
fun run_atp ctxt format problem =
blanchet@43566
    50
  let
blanchet@43566
    51
    val thy = Proof_Context.theory_of ctxt
blanchet@47055
    52
    val prob_file = File.tmp_path (Path.explode "prob")
blanchet@51998
    53
    val atp = atp_of_format format
blanchet@47606
    54
    val {exec, arguments, proof_delims, known_failures, ...} =
blanchet@47606
    55
      get_atp thy atp ()
blanchet@47038
    56
    val ord = effective_term_order ctxt atp
blanchet@51998
    57
    val _ = problem |> lines_of_atp_problem format ord (K [])
blanchet@46442
    58
                    |> File.write_list prob_file
blanchet@52754
    59
    val exec = exec ()
blanchet@48376
    60
    val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
blanchet@43566
    61
    val command =
blanchet@50927
    62
      File.shell_path (Path.explode path) ^ " " ^
blanchet@51646
    63
      arguments ctxt false "" atp_timeout (File.shell_path prob_file)
blanchet@50927
    64
                (ord, K [], K [])
blanchet@51646
    65
    val outcome =
blanchet@51646
    66
      TimeLimit.timeLimit atp_timeout Isabelle_System.bash_output command
blanchet@51646
    67
      |> fst
blanchet@51646
    68
      |> extract_tstplike_proof_and_outcome false proof_delims known_failures
blanchet@51646
    69
      |> snd
blanchet@51646
    70
      handle TimeLimit.TimeOut => SOME TimedOut
blanchet@51647
    71
    val _ =
blanchet@51647
    72
      tracing ("Ran ATP: " ^
blanchet@51649
    73
               (case outcome of
blanchet@51649
    74
                  NONE => "Success"
blanchet@53586
    75
                | SOME failure => string_of_atp_failure failure))
blanchet@51646
    76
  in outcome end
blanchet@43566
    77
blanchet@51646
    78
fun is_problem_line_reprovable ctxt format prelude axioms deps
blanchet@51646
    79
                               (Formula (ident', _, phi, _, _)) =
blanchet@51646
    80
    is_none (run_atp ctxt format
blanchet@51646
    81
        ((factsN, Formula (ident', Conjecture, phi, NONE, []) ::
blanchet@51646
    82
                  map_filter (Symtab.lookup axioms) deps) ::
blanchet@51646
    83
         prelude))
blanchet@51646
    84
  | is_problem_line_reprovable _ _ _ _ _ _ = false
blanchet@51646
    85
blanchet@51646
    86
fun inference_term _ [] = NONE
blanchet@51646
    87
  | inference_term check_infs ss =
blanchet@51646
    88
    ATerm (("inference", []),
blanchet@51646
    89
        [ATerm (("checked_isabelle" |> not check_infs ? prefix "un", []), []),
blanchet@51646
    90
         ATerm ((tptp_empty_list, []), []),
blanchet@51646
    91
         ATerm ((tptp_empty_list, []),
blanchet@51646
    92
         map (fn s => ATerm ((s, []), [])) ss)])
blanchet@51646
    93
    |> SOME
blanchet@51646
    94
blanchet@51646
    95
fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers
blanchet@51646
    96
        (line as Formula ((ident, alt), Axiom, phi, NONE, tms)) =
blanchet@51646
    97
    let
blanchet@51646
    98
      val deps =
blanchet@51646
    99
        case these (AList.lookup (op =) infers ident) of
blanchet@51646
   100
          [] => []
blanchet@51646
   101
        | deps =>
blanchet@51646
   102
          if check_infs andalso
blanchet@51646
   103
             not (is_problem_line_reprovable ctxt format prelude axioms deps
blanchet@51646
   104
                                             line) then
blanchet@51646
   105
            []
blanchet@51646
   106
          else
blanchet@51646
   107
            deps
blanchet@51646
   108
    in
blanchet@51646
   109
      Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, tms)
blanchet@51646
   110
    end
blanchet@51646
   111
  | add_inferences_to_problem_line _ _ _ _ _ _ line = line
blanchet@51646
   112
blanchet@51646
   113
fun add_inferences_to_problem ctxt format check_infs prelude infers problem =
blanchet@51646
   114
  let
blanchet@51646
   115
    fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) =
blanchet@51646
   116
        Symtab.default (ident, axiom)
blanchet@51646
   117
      | add_if_axiom _ = I
blanchet@51646
   118
    val add_axioms_of_problem = fold (fold add_if_axiom o snd)
blanchet@51646
   119
    val axioms = Symtab.empty |> check_infs ? add_axioms_of_problem problem
blanchet@51646
   120
  in
blanchet@51646
   121
    map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs
blanchet@51646
   122
                         prelude axioms infers))) problem
blanchet@51646
   123
  end
blanchet@51646
   124
blanchet@51646
   125
fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident
blanchet@51646
   126
  | ident_of_problem_line (Type_Decl (ident, _, _)) = ident
blanchet@51646
   127
  | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
blanchet@51646
   128
  | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
blanchet@51646
   129
  | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
blanchet@51646
   130
blanchet@43499
   131
fun order_facts ord = sort (ord o pairself ident_of_problem_line)
blanchet@51646
   132
blanchet@43499
   133
fun order_problem_facts _ [] = []
blanchet@43499
   134
  | order_problem_facts ord ((heading, lines) :: problem) =
blanchet@43499
   135
    if heading = factsN then (heading, order_facts ord lines) :: problem
blanchet@43499
   136
    else (heading, lines) :: order_problem_facts ord problem
blanchet@43499
   137
blanchet@45305
   138
(* A fairly random selection of types used for monomorphizing. *)
blanchet@45305
   139
val ground_types =
blanchet@45305
   140
  [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool},
blanchet@45305
   141
   @{typ unit}]
blanchet@45305
   142
blanchet@51998
   143
fun ground_type_of_tvar _ [] tvar =
blanchet@51998
   144
    raise TYPE ("ground_type_of_tvar", [TVar tvar], [])
blanchet@51998
   145
  | ground_type_of_tvar thy (T :: Ts) tvar =
blanchet@45305
   146
    if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T
blanchet@51998
   147
    else ground_type_of_tvar thy Ts tvar
blanchet@45305
   148
blanchet@45305
   149
fun monomorphize_term ctxt t =
blanchet@45305
   150
  let val thy = Proof_Context.theory_of ctxt in
blanchet@51998
   151
    t |> map_types (map_type_tvar (ground_type_of_tvar thy ground_types))
blanchet@45305
   152
    handle TYPE _ => @{prop True}
blanchet@45305
   153
  end
blanchet@45305
   154
blanchet@51633
   155
fun heading_sort_key heading =
blanchet@51633
   156
  if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading
blanchet@51633
   157
blanchet@57306
   158
val max_dependencies = 100
blanchet@57306
   159
blanchet@51998
   160
fun problem_of_theory ctxt thy format infer_policy type_enc =
blanchet@42602
   161
  let
blanchet@48299
   162
    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
blanchet@48315
   163
    val type_enc =
blanchet@52031
   164
      type_enc |> type_enc_of_string Non_Strict
blanchet@48315
   165
               |> adjust_type_enc format
blanchet@48131
   166
    val mono = not (is_type_enc_polymorphic type_enc)
blanchet@48438
   167
    val facts =
blanchet@50442
   168
      Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
blanchet@48530
   169
                                  Symtab.empty [] [] css_table
blanchet@51633
   170
      |> sort (Sledgehammer_MaSh.crude_thm_ord o pairself snd)
blanchet@51646
   171
    val problem =
blanchet@43576
   172
      facts
blanchet@45305
   173
      |> map (fn ((_, loc), th) =>
blanchet@57268
   174
        ((Thm.get_name_hint th, loc), th |> prop_of |> mono ? monomorphize_term ctxt))
blanchet@57268
   175
      |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
blanchet@57268
   176
        @{prop False}
blanchet@51647
   177
      |> #1 |> sort_wrt (heading_sort_key o fst)
blanchet@51646
   178
    val prelude = fst (split_last problem)
blanchet@50735
   179
    val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
blanchet@42602
   180
    val infers =
blanchet@51646
   181
      if infer_policy = No_Inferences then
blanchet@51646
   182
        []
blanchet@51646
   183
      else
blanchet@51646
   184
        facts
blanchet@51646
   185
        |> map (fn (_, th) =>
blanchet@51646
   186
                   (fact_name_of (Thm.get_name_hint th),
blanchet@57306
   187
                    th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs)
blanchet@57306
   188
                       |> these |> map fact_name_of))
blanchet@51650
   189
    val all_problem_names =
blanchet@51650
   190
      problem |> maps (map ident_of_problem_line o snd)
blanchet@51650
   191
              |> distinct (op =)
blanchet@51650
   192
    val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names)
blanchet@42602
   193
    val infers =
blanchet@51650
   194
      infers |> filter (Symtab.defined all_problem_name_set o fst)
blanchet@51650
   195
             |> map (apsnd (filter (Symtab.defined all_problem_name_set)))
blanchet@51650
   196
    val maybe_add_edge = perhaps o try o String_Graph.add_edge_acyclic
blanchet@43499
   197
    val ordered_names =
blanchet@43499
   198
      String_Graph.empty
blanchet@51646
   199
      |> fold (String_Graph.new_node o rpair ()) all_problem_names
blanchet@43499
   200
      |> fold (fn (to, froms) =>
blanchet@51650
   201
                  fold (fn from => maybe_add_edge (from, to)) froms)
blanchet@43566
   202
              infers
blanchet@51650
   203
      |> fold (fn (to, from) => maybe_add_edge (from, to))
blanchet@51646
   204
              (tl all_problem_names ~~ fst (split_last all_problem_names))
blanchet@43499
   205
      |> String_Graph.topological_order
blanchet@43499
   206
    val order_tab =
blanchet@43499
   207
      Symtab.empty
blanchet@43499
   208
      |> fold (Symtab.insert (op =))
blanchet@43499
   209
              (ordered_names ~~ (1 upto length ordered_names))
blanchet@43499
   210
    val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
blanchet@51646
   211
  in
blanchet@51646
   212
    problem
blanchet@51646
   213
    |> (case format of
blanchet@51646
   214
          DFG _ => I
blanchet@51646
   215
        | _ => add_inferences_to_problem ctxt format
blanchet@51646
   216
                   (infer_policy = Checked_Inferences) prelude infers)
blanchet@51646
   217
    |> order_problem_facts name_ord
blanchet@51646
   218
  end
blanchet@51646
   219
blanchet@51998
   220
fun lines_of_problem ctxt format =
blanchet@51998
   221
  lines_of_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K [])
blanchet@51646
   222
blanchet@51646
   223
fun write_lines path ss =
blanchet@51646
   224
  let
blanchet@51646
   225
    val _ = File.write path ""
blanchet@42602
   226
    val _ = app (File.append path) ss
blanchet@42602
   227
  in () end
blanchet@42602
   228
blanchet@51646
   229
fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc
blanchet@51646
   230
                                           file_name =
blanchet@51646
   231
  let
blanchet@51998
   232
    val problem = problem_of_theory ctxt thy format infer_policy type_enc
blanchet@51998
   233
    val ss = lines_of_problem ctxt format problem
blanchet@51646
   234
  in write_lines (Path.explode file_name) ss end
blanchet@51646
   235
blanchet@51646
   236
fun ap dir = Path.append dir o Path.explode
blanchet@51646
   237
blanchet@51646
   238
fun chop_maximal_groups eq xs =
blanchet@51646
   239
  let
blanchet@51646
   240
    val rev_xs = rev xs
blanchet@51646
   241
    fun chop_group _ [] = []
blanchet@51646
   242
      | chop_group n (xs as x :: _) =
blanchet@51646
   243
        let
blanchet@51646
   244
          val n' = find_index (curry eq x) rev_xs
blanchet@51646
   245
          val (ws', xs') = chop (n - n') xs
blanchet@51646
   246
        in ws' :: chop_group n' xs' end
blanchet@51646
   247
   in chop_group (length xs) xs end
blanchet@51646
   248
blanchet@51646
   249
fun theory_name_of_fact (Formula ((_, alt), _, _, _, _)) =
blanchet@51646
   250
    (case first_field Long_Name.separator alt of
blanchet@51646
   251
       NONE => alt
blanchet@51646
   252
     | SOME (thy, _) => thy)
blanchet@51646
   253
  | theory_name_of_fact _ = ""
blanchet@51646
   254
blanchet@51646
   255
val problem_suffix = ".p"
blanchet@51646
   256
val include_suffix = ".ax"
blanchet@51646
   257
blanchet@51646
   258
val file_order_name = "FilesInProcessingOrder"
blanchet@51646
   259
val problem_order_name = "ProblemsInProcessingOrder"
blanchet@51646
   260
val problem_name = "problems"
blanchet@51646
   261
val include_name = "incl"
blanchet@51646
   262
val prelude_base_name = "prelude"
blanchet@51646
   263
val prelude_name = prelude_base_name ^ include_suffix
blanchet@51646
   264
blanchet@51652
   265
val encode_meta = Sledgehammer_MaSh.encode_str
blanchet@51652
   266
wenzelm@53980
   267
fun include_base_name_of_fact x = encode_meta (theory_name_of_fact x)
blanchet@51646
   268
blanchet@51646
   269
fun include_line base_name =
blanchet@51646
   270
  "include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n"
blanchet@51646
   271
blanchet@51652
   272
val hol_base_name = encode_meta "HOL"
blanchet@51652
   273
blanchet@51652
   274
fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) =
blanchet@51646
   275
  case try (Global_Theory.get_thm thy) alt of
blanchet@51652
   276
    SOME th =>
blanchet@51652
   277
    (* This is a crude hack to detect theorems stated and proved by the user (as
blanchet@51652
   278
       opposed to those derived by various packages). In addition, we leave out
blanchet@51652
   279
       everything in "HOL" as too basic to be interesting. *)
blanchet@51652
   280
    Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name
blanchet@51646
   281
  | NONE => false
blanchet@51646
   282
blanchet@51646
   283
(* Convention: theoryname__goalname *)
blanchet@51652
   284
fun problem_name_of base_name n alt =
blanchet@51652
   285
  base_name ^ "__" ^ string_of_int n ^ "_" ^
blanchet@51652
   286
  perhaps (try (unprefix (base_name ^ "_"))) alt ^ problem_suffix
blanchet@51646
   287
blanchet@51646
   288
fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc
blanchet@51646
   289
                                           dir_name =
blanchet@51646
   290
  let
blanchet@51646
   291
    val dir = Path.explode dir_name
blanchet@51646
   292
    val _ = Isabelle_System.mkdir dir
blanchet@51646
   293
    val file_order_path = ap dir file_order_name
blanchet@51646
   294
    val _ = File.write file_order_path ""
blanchet@51646
   295
    val problem_order_path = ap dir problem_order_name
blanchet@51646
   296
    val _ = File.write problem_order_path ""
blanchet@51646
   297
    val problem_dir = ap dir problem_name
blanchet@51646
   298
    val _ = Isabelle_System.mkdir problem_dir
blanchet@51646
   299
    val include_dir = ap problem_dir include_name
blanchet@51646
   300
    val _ = Isabelle_System.mkdir include_dir
blanchet@51646
   301
    val (prelude, groups) =
blanchet@51998
   302
      problem_of_theory ctxt thy format infer_policy type_enc
blanchet@51646
   303
      |> split_last
blanchet@51646
   304
      ||> (snd
blanchet@51646
   305
           #> chop_maximal_groups (op = o pairself theory_name_of_fact)
blanchet@51646
   306
           #> map (`(include_base_name_of_fact o hd)))
blanchet@51646
   307
    fun write_prelude () =
blanchet@51998
   308
      let val ss = lines_of_problem ctxt format prelude in
blanchet@51646
   309
        File.append file_order_path (prelude_base_name ^ "\n");
blanchet@51646
   310
        write_lines (ap include_dir prelude_name) ss
blanchet@51646
   311
      end
blanchet@51646
   312
    fun write_include_file (base_name, facts) =
blanchet@51646
   313
      let
blanchet@51646
   314
        val name = base_name ^ include_suffix
blanchet@51998
   315
        val ss = lines_of_problem ctxt format [(factsN, facts)]
blanchet@51646
   316
      in
blanchet@51646
   317
        File.append file_order_path (base_name ^ "\n");
blanchet@51646
   318
        write_lines (ap include_dir name) ss
blanchet@51646
   319
      end
blanchet@51652
   320
    fun write_problem_files _ _ _ [] = ()
blanchet@51652
   321
      | write_problem_files _ includes [] groups =
blanchet@51652
   322
        write_problem_files 1 includes includes groups
blanchet@51652
   323
      | write_problem_files n includes _ ((base_name, []) :: groups) =
blanchet@51652
   324
        write_problem_files n (includes @ [include_line base_name]) [] groups
blanchet@51652
   325
      | write_problem_files n includes seen
blanchet@51646
   326
                            ((base_name, fact :: facts) :: groups) =
blanchet@51998
   327
        let val fact_s = tptp_string_of_line format fact in
blanchet@51652
   328
          (if should_generate_problem thy base_name fact then
blanchet@51646
   329
             let
blanchet@51646
   330
               val (name, conj) =
blanchet@51646
   331
                 (case fact of
blanchet@51646
   332
                    Formula ((ident, alt), _, phi, _, _) =>
blanchet@51652
   333
                    (problem_name_of base_name n (encode_meta alt),
blanchet@51646
   334
                     Formula ((ident, alt), Conjecture, phi, NONE, [])))
blanchet@51998
   335
               val conj_s = tptp_string_of_line format conj
blanchet@51646
   336
             in
blanchet@51646
   337
               File.append problem_order_path (name ^ "\n");
blanchet@51646
   338
               write_lines (ap problem_dir name) (seen @ [conj_s])
blanchet@51646
   339
             end
blanchet@51646
   340
           else
blanchet@51646
   341
             ();
blanchet@51652
   342
           write_problem_files (n + 1) includes (seen @ [fact_s])
blanchet@51646
   343
                               ((base_name, facts) :: groups))
blanchet@51646
   344
        end
blanchet@51646
   345
    val _ = write_prelude ()
blanchet@51646
   346
    val _ = app write_include_file groups
blanchet@51652
   347
    val _ = write_problem_files 1 [include_line prelude_base_name] [] groups
blanchet@51646
   348
  in () end
blanchet@51646
   349
blanchet@42602
   350
end;