src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
author blanchet
Mon Jul 26 11:21:25 2010 +0200 (2010-07-26)
changeset 37992 7911e78a7122
parent 37962 d7dbe01f48d7
child 37993 bb39190370fe
permissions -rw-r--r--
renamed internal function
blanchet@37509
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
blanchet@37509
     2
    Author:     Jia Meng, NICTA
blanchet@37509
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@37509
     4
blanchet@37509
     5
TPTP syntax.
blanchet@37509
     6
*)
blanchet@37509
     7
blanchet@37509
     8
signature SLEDGEHAMMER_TPTP_FORMAT =
blanchet@37509
     9
sig
blanchet@37925
    10
  type class_rel_clause = Metis_Clauses.class_rel_clause
blanchet@37578
    11
  type arity_clause = Metis_Clauses.arity_clause
blanchet@37922
    12
  type fol_clause = Metis_Clauses.fol_clause
blanchet@37509
    13
blanchet@37992
    14
  datatype 'a fo_term = ATerm of 'a * 'a fo_term list
blanchet@37992
    15
  datatype quantifier = AForall | AExists
blanchet@37992
    16
  datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
blanchet@37992
    17
  datatype 'a formula =
blanchet@37992
    18
    AQuant of quantifier * 'a list * 'a formula |
blanchet@37992
    19
    AConn of connective * 'a formula list |
blanchet@37992
    20
    APred of 'a fo_term
blanchet@37992
    21
blanchet@37962
    22
  val axiom_prefix : string
blanchet@37992
    23
  val conjecture_prefix : string
blanchet@37509
    24
  val write_tptp_file :
blanchet@37643
    25
    theory -> bool -> bool -> bool -> Path.T
blanchet@37922
    26
    -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
blanchet@37925
    27
       * class_rel_clause list * arity_clause list
blanchet@37926
    28
    -> string Symtab.table * int
blanchet@37509
    29
end;
blanchet@37509
    30
blanchet@37509
    31
structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
blanchet@37509
    32
struct
blanchet@37509
    33
blanchet@37578
    34
open Metis_Clauses
blanchet@37509
    35
open Sledgehammer_Util
blanchet@37509
    36
blanchet@37643
    37
blanchet@37643
    38
(** ATP problem **)
blanchet@37643
    39
blanchet@37961
    40
datatype 'a fo_term = ATerm of 'a * 'a fo_term list
blanchet@37961
    41
datatype quantifier = AForall | AExists
blanchet@37992
    42
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
blanchet@37961
    43
datatype 'a formula =
blanchet@37961
    44
  AQuant of quantifier * 'a list * 'a formula |
blanchet@37961
    45
  AConn of connective * 'a formula list |
blanchet@37961
    46
  APred of 'a fo_term
blanchet@37961
    47
blanchet@37961
    48
fun mk_anot phi = AConn (ANot, [phi])
blanchet@37961
    49
blanchet@37961
    50
datatype 'a problem_line = Fof of string * kind * 'a formula
blanchet@37643
    51
type 'a problem = (string * 'a problem_line list) list
blanchet@37643
    52
blanchet@37961
    53
fun string_for_term (ATerm (s, [])) = s
blanchet@37961
    54
  | string_for_term (ATerm (s, ts)) =
blanchet@37961
    55
    if s = "equal" then space_implode " = " (map string_for_term ts)
blanchet@37961
    56
    else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
blanchet@37961
    57
fun string_for_quantifier AForall = "!"
blanchet@37961
    58
  | string_for_quantifier AExists = "?"
blanchet@37961
    59
fun string_for_connective ANot = "~"
blanchet@37961
    60
  | string_for_connective AAnd = "&"
blanchet@37961
    61
  | string_for_connective AOr = "|"
blanchet@37961
    62
  | string_for_connective AImplies = "=>"
blanchet@37992
    63
  | string_for_connective AIf = "<="
blanchet@37961
    64
  | string_for_connective AIff = "<=>"
blanchet@37992
    65
  | string_for_connective ANotIff = "<~>"
blanchet@37961
    66
fun string_for_formula (AQuant (q, xs, phi)) =
blanchet@37961
    67
    string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^
blanchet@37961
    68
    string_for_formula phi
blanchet@37961
    69
  | string_for_formula (AConn (c, [phi])) =
blanchet@37961
    70
    string_for_connective c ^ " " ^ string_for_formula phi
blanchet@37961
    71
  | string_for_formula (AConn (c, phis)) =
blanchet@37961
    72
    "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
blanchet@37961
    73
                        (map string_for_formula phis) ^ ")"
blanchet@37961
    74
  | string_for_formula (APred tm) = string_for_term tm
blanchet@37961
    75
blanchet@37961
    76
fun string_for_problem_line (Fof (ident, kind, phi)) =
blanchet@37961
    77
  "fof(" ^ ident ^ ", " ^
blanchet@37961
    78
  (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
blanchet@37961
    79
  "    (" ^ string_for_formula phi ^ ")).\n"
blanchet@37643
    80
fun strings_for_problem problem =
blanchet@37643
    81
  "% This file was generated by Isabelle (most likely Sledgehammer)\n\
blanchet@37643
    82
  \% " ^ timestamp () ^ "\n" ::
blanchet@37643
    83
  maps (fn (_, []) => []
blanchet@37643
    84
         | (heading, lines) =>
blanchet@37643
    85
           "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
blanchet@37643
    86
           map string_for_problem_line lines) problem
blanchet@37643
    87
blanchet@37643
    88
blanchet@37643
    89
(** Nice names **)
blanchet@37643
    90
blanchet@37624
    91
fun empty_name_pool readable_names =
blanchet@37643
    92
  if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
blanchet@37624
    93
blanchet@37624
    94
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
blanchet@37624
    95
fun pool_map f xs =
blanchet@37624
    96
  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
blanchet@37624
    97
blanchet@37643
    98
(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
blanchet@37643
    99
   unreadable "op_1", "op_2", etc., in the problem files. *)
blanchet@37643
   100
val reserved_nice_names = ["equal", "op"]
blanchet@37624
   101
fun readable_name full_name s =
blanchet@37643
   102
  if s = full_name then
blanchet@37643
   103
    s
blanchet@37643
   104
  else
blanchet@37643
   105
    let
blanchet@37643
   106
      val s = s |> Long_Name.base_name
blanchet@37643
   107
                |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
blanchet@37643
   108
    in if member (op =) reserved_nice_names s then full_name else s end
blanchet@37624
   109
blanchet@37624
   110
fun nice_name (full_name, _) NONE = (full_name, NONE)
blanchet@37624
   111
  | nice_name (full_name, desired_name) (SOME the_pool) =
blanchet@37624
   112
    case Symtab.lookup (fst the_pool) full_name of
blanchet@37624
   113
      SOME nice_name => (nice_name, SOME the_pool)
blanchet@37624
   114
    | NONE =>
blanchet@37624
   115
      let
blanchet@37624
   116
        val nice_prefix = readable_name full_name desired_name
blanchet@37624
   117
        fun add j =
blanchet@37624
   118
          let
blanchet@37624
   119
            val nice_name = nice_prefix ^
blanchet@37624
   120
                            (if j = 0 then "" else "_" ^ Int.toString j)
blanchet@37624
   121
          in
blanchet@37624
   122
            case Symtab.lookup (snd the_pool) nice_name of
blanchet@37624
   123
              SOME full_name' =>
blanchet@37624
   124
              if full_name = full_name' then (nice_name, the_pool)
blanchet@37624
   125
              else add (j + 1)
blanchet@37624
   126
            | NONE =>
blanchet@37624
   127
              (nice_name,
blanchet@37624
   128
               (Symtab.update_new (full_name, nice_name) (fst the_pool),
blanchet@37624
   129
                Symtab.update_new (nice_name, full_name) (snd the_pool)))
blanchet@37624
   130
          end
blanchet@37624
   131
      in add 0 |> apsnd SOME end
blanchet@37624
   132
blanchet@37961
   133
blanchet@37961
   134
fun nice_term (ATerm (name, ts)) =
blanchet@37961
   135
  nice_name name ##>> pool_map nice_term ts #>> ATerm
blanchet@37961
   136
fun nice_formula (AQuant (q, xs, phi)) =
blanchet@37961
   137
    pool_map nice_name xs ##>> nice_formula phi
blanchet@37961
   138
    #>> (fn (xs, phi) => AQuant (q, xs, phi))
blanchet@37961
   139
  | nice_formula (AConn (c, phis)) =
blanchet@37961
   140
    pool_map nice_formula phis #>> curry AConn c
blanchet@37961
   141
  | nice_formula (APred tm) = nice_term tm #>> APred
blanchet@37961
   142
fun nice_problem_line (Fof (ident, kind, phi)) =
blanchet@37961
   143
  nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
blanchet@37931
   144
fun nice_problem problem =
blanchet@37643
   145
  pool_map (fn (heading, lines) =>
blanchet@37931
   146
               pool_map nice_problem_line lines #>> pair heading) problem
blanchet@37643
   147
blanchet@37643
   148
blanchet@37643
   149
(** Sledgehammer stuff **)
blanchet@37520
   150
blanchet@37962
   151
val axiom_prefix = "ax_"
blanchet@37962
   152
val conjecture_prefix = "conj_"
blanchet@37509
   153
val arity_clause_prefix = "clsarity_"
blanchet@37509
   154
blanchet@37643
   155
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
blanchet@37643
   156
blanchet@37961
   157
fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
blanchet@37961
   158
  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
blanchet@37961
   159
  | fo_term_for_combtyp (CombType (name, tys)) =
blanchet@37961
   160
    ATerm (name, map fo_term_for_combtyp tys)
blanchet@37643
   161
blanchet@37961
   162
fun fo_term_for_combterm full_types top_level u =
blanchet@37643
   163
  let
blanchet@37643
   164
    val (head, args) = strip_combterm_comb u
blanchet@37643
   165
    val (x, ty_args) =
blanchet@37643
   166
      case head of
blanchet@37643
   167
        CombConst (name, _, ty_args) =>
blanchet@37643
   168
        if fst name = "equal" then
blanchet@37643
   169
          (if top_level andalso length args = 2 then name
blanchet@37643
   170
           else ("c_fequal", @{const_name fequal}), [])
blanchet@37643
   171
        else
blanchet@37643
   172
          (name, if full_types then [] else ty_args)
blanchet@37643
   173
      | CombVar (name, _) => (name, [])
blanchet@37643
   174
      | CombApp _ => raise Fail "impossible \"CombApp\""
blanchet@37961
   175
    val t = ATerm (x, map fo_term_for_combtyp ty_args @
blanchet@37961
   176
                      map (fo_term_for_combterm full_types false) args)
blanchet@37643
   177
  in
blanchet@37961
   178
    if full_types then wrap_type (fo_term_for_combtyp (type_of_combterm u)) t
blanchet@37643
   179
    else t
blanchet@37643
   180
  end
blanchet@37643
   181
blanchet@37961
   182
fun fo_literal_for_literal full_types (FOLLiteral (pos, t)) =
blanchet@37961
   183
  (pos, fo_term_for_combterm full_types true t)
blanchet@37643
   184
blanchet@37961
   185
fun fo_literal_for_type_literal pos (TyLitVar (class, name)) =
blanchet@37643
   186
    (pos, ATerm (class, [ATerm (name, [])]))
blanchet@37961
   187
  | fo_literal_for_type_literal pos (TyLitFree (class, name)) =
blanchet@37643
   188
    (pos, ATerm (class, [ATerm (name, [])]))
blanchet@37643
   189
blanchet@37961
   190
fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
blanchet@37961
   191
fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), []))
blanchet@37992
   192
  | formula_for_fo_literals [lit] = formula_for_fo_literal lit
blanchet@37961
   193
  | formula_for_fo_literals (lit :: lits) =
blanchet@37961
   194
    AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits])
blanchet@37961
   195
blanchet@37961
   196
fun formula_for_axiom full_types (FOLClause {literals, ctypes_sorts, ...}) =
blanchet@37961
   197
  map (fo_literal_for_literal full_types) literals @
blanchet@37961
   198
  map (fo_literal_for_type_literal false)
blanchet@37643
   199
      (type_literals_for_types ctypes_sorts)
blanchet@37961
   200
  |> formula_for_fo_literals
blanchet@37643
   201
blanchet@37643
   202
fun problem_line_for_axiom full_types
blanchet@37962
   203
        (clause as FOLClause {axiom_name, kind, ...}) =
blanchet@37992
   204
  Fof (axiom_prefix ^ ascii_of axiom_name, kind,
blanchet@37961
   205
       formula_for_axiom full_types clause)
blanchet@37643
   206
blanchet@37926
   207
fun problem_line_for_class_rel_clause
blanchet@37925
   208
        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
blanchet@37643
   209
  let val ty_arg = ATerm (("T", "T"), []) in
blanchet@37961
   210
    Fof (ascii_of axiom_name, Axiom,
blanchet@37961
   211
         AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
blanchet@37961
   212
                           APred (ATerm (superclass, [ty_arg]))]))
blanchet@37643
   213
  end
blanchet@37643
   214
blanchet@37961
   215
fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
blanchet@37643
   216
    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
blanchet@37961
   217
  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
blanchet@37643
   218
    (false, ATerm (c, [ATerm (sort, [])]))
blanchet@37643
   219
blanchet@37926
   220
fun problem_line_for_arity_clause
blanchet@37926
   221
        (ArityClause {axiom_name, conclLit, premLits, ...}) =
blanchet@37961
   222
  Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
blanchet@37961
   223
       map fo_literal_for_arity_literal (conclLit :: premLits)
blanchet@37961
   224
       |> formula_for_fo_literals)
blanchet@37643
   225
blanchet@37643
   226
fun problem_line_for_conjecture full_types
blanchet@37992
   227
        (clause as FOLClause {clause_id, kind, literals, ...}) =
blanchet@37992
   228
  Fof (conjecture_prefix ^ Int.toString clause_id,
blanchet@37992
   229
       kind, map (fo_literal_for_literal full_types) literals
blanchet@37992
   230
             |> formula_for_fo_literals |> mk_anot)
blanchet@37643
   231
blanchet@37922
   232
fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
blanchet@37961
   233
  map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
blanchet@37509
   234
blanchet@37961
   235
fun problem_line_for_free_type lit =
blanchet@37961
   236
  Fof ("tfree_tcs", Conjecture, formula_for_fo_literal lit)
blanchet@37643
   237
fun problem_lines_for_free_types conjectures =
blanchet@37643
   238
  let
blanchet@37643
   239
    val litss = map atp_free_type_literals_for_conjecture conjectures
blanchet@37643
   240
    val lits = fold (union (op =)) litss []
blanchet@37643
   241
  in map problem_line_for_free_type lits end
blanchet@37643
   242
blanchet@37643
   243
(** "hBOOL" and "hAPP" **)
blanchet@37643
   244
blanchet@37643
   245
type const_info = {min_arity: int, max_arity: int, sub_level: bool}
blanchet@37643
   246
blanchet@37961
   247
fun is_variable s = Char.isUpper (String.sub (s, 0))
blanchet@37643
   248
blanchet@37643
   249
fun consider_term top_level (ATerm ((s, _), ts)) =
blanchet@37961
   250
  (if is_variable s then
blanchet@37643
   251
     I
blanchet@37643
   252
   else
blanchet@37643
   253
     let val n = length ts in
blanchet@37643
   254
       Symtab.map_default
blanchet@37643
   255
           (s, {min_arity = n, max_arity = 0, sub_level = false})
blanchet@37643
   256
           (fn {min_arity, max_arity, sub_level} =>
blanchet@37643
   257
               {min_arity = Int.min (n, min_arity),
blanchet@37643
   258
                max_arity = Int.max (n, max_arity),
blanchet@37643
   259
                sub_level = sub_level orelse not top_level})
blanchet@37643
   260
     end)
blanchet@37643
   261
  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
blanchet@37961
   262
fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
blanchet@37961
   263
  | consider_formula (AConn (_, phis)) = fold consider_formula phis
blanchet@37961
   264
  | consider_formula (APred tm) = consider_term true tm
blanchet@37961
   265
blanchet@37961
   266
fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
blanchet@37931
   267
fun consider_problem problem = fold (fold consider_problem_line o snd) problem
blanchet@37643
   268
blanchet@37643
   269
fun const_table_for_problem explicit_apply problem =
blanchet@37643
   270
  if explicit_apply then NONE
blanchet@37643
   271
  else SOME (Symtab.empty |> consider_problem problem)
blanchet@37643
   272
blanchet@37643
   273
val tc_fun = make_fixed_type_const @{type_name fun}
blanchet@37643
   274
blanchet@37643
   275
fun min_arity_of thy full_types NONE s =
blanchet@37643
   276
    (if s = "equal" orelse s = type_wrapper_name orelse
blanchet@37643
   277
        String.isPrefix type_const_prefix s orelse
blanchet@37643
   278
        String.isPrefix class_prefix s then
blanchet@37643
   279
       16383 (* large number *)
blanchet@37643
   280
     else if full_types then
blanchet@37643
   281
       0
blanchet@37992
   282
     else case strip_prefix_and_undo_ascii const_prefix s of
blanchet@37643
   283
       SOME s' => num_type_args thy (invert_const s')
blanchet@37643
   284
     | NONE => 0)
blanchet@37643
   285
  | min_arity_of _ _ (SOME the_const_tab) s =
blanchet@37643
   286
    case Symtab.lookup the_const_tab s of
blanchet@37643
   287
      SOME ({min_arity, ...} : const_info) => min_arity
blanchet@37643
   288
    | NONE => 0
blanchet@37643
   289
blanchet@37643
   290
fun full_type_of (ATerm ((s, _), [ty, _])) =
blanchet@37643
   291
    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
blanchet@37643
   292
  | full_type_of _ = raise Fail "expected type wrapper"
blanchet@37643
   293
blanchet@37643
   294
fun list_hAPP_rev _ t1 [] = t1
blanchet@37643
   295
  | list_hAPP_rev NONE t1 (t2 :: ts2) =
blanchet@37643
   296
    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
blanchet@37643
   297
  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
blanchet@37643
   298
    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
blanchet@37643
   299
                         [full_type_of t2, ty]) in
blanchet@37643
   300
      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
blanchet@37643
   301
    end
blanchet@37643
   302
blanchet@37643
   303
fun repair_applications_in_term thy full_types const_tab =
blanchet@37643
   304
  let
blanchet@37643
   305
    fun aux opt_ty (ATerm (name as (s, _), ts)) =
blanchet@37643
   306
      if s = type_wrapper_name then
blanchet@37643
   307
        case ts of
blanchet@37643
   308
          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
blanchet@37643
   309
        | _ => raise Fail "malformed type wrapper"
blanchet@37643
   310
      else
blanchet@37643
   311
        let
blanchet@37643
   312
          val ts = map (aux NONE) ts
blanchet@37643
   313
          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
blanchet@37643
   314
        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
blanchet@37643
   315
  in aux NONE end
blanchet@37643
   316
blanchet@37643
   317
fun boolify t = ATerm (`I "hBOOL", [t])
blanchet@37509
   318
blanchet@37509
   319
(* True if the constant ever appears outside of the top-level position in
blanchet@37520
   320
   literals, or if it appears with different arities (e.g., because of different
blanchet@37520
   321
   type instantiations). If false, the constant always receives all of its
blanchet@37520
   322
   arguments and is used as a predicate. *)
blanchet@37643
   323
fun is_predicate NONE s =
blanchet@37643
   324
    s = "equal" orelse String.isPrefix type_const_prefix s orelse
blanchet@37643
   325
    String.isPrefix class_prefix s
blanchet@37643
   326
  | is_predicate (SOME the_const_tab) s =
blanchet@37643
   327
    case Symtab.lookup the_const_tab s of
blanchet@37643
   328
      SOME {min_arity, max_arity, sub_level} =>
blanchet@37643
   329
      not sub_level andalso min_arity = max_arity
blanchet@37520
   330
    | NONE => false
blanchet@37509
   331
blanchet@37643
   332
fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
blanchet@37643
   333
  if s = type_wrapper_name then
blanchet@37643
   334
    case ts of
blanchet@37643
   335
      [_, t' as ATerm ((s', _), _)] =>
blanchet@37643
   336
      if is_predicate const_tab s' then t' else boolify t
blanchet@37643
   337
    | _ => raise Fail "malformed type wrapper"
blanchet@37509
   338
  else
blanchet@37643
   339
    t |> not (is_predicate const_tab s) ? boolify
blanchet@37509
   340
blanchet@37961
   341
fun close_universally phi =
blanchet@37961
   342
  let
blanchet@37961
   343
    fun term_vars bounds (ATerm (name as (s, _), tms)) =
blanchet@37961
   344
        (is_variable s andalso not (member (op =) bounds name))
blanchet@37961
   345
          ? insert (op =) name
blanchet@37961
   346
        #> fold (term_vars bounds) tms
blanchet@37961
   347
    fun formula_vars bounds (AQuant (q, xs, phi)) =
blanchet@37961
   348
        formula_vars (xs @ bounds) phi
blanchet@37961
   349
      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
blanchet@37961
   350
      | formula_vars bounds (APred tm) = term_vars bounds tm
blanchet@37961
   351
  in
blanchet@37961
   352
    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
blanchet@37961
   353
  end
blanchet@37961
   354
blanchet@37961
   355
fun repair_formula thy explicit_forall full_types const_tab =
blanchet@37961
   356
  let
blanchet@37961
   357
    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
blanchet@37961
   358
      | aux (AConn (c, phis)) = AConn (c, map aux phis)
blanchet@37961
   359
      | aux (APred tm) =
blanchet@37961
   360
        APred (tm |> repair_applications_in_term thy full_types const_tab
blanchet@37961
   361
                  |> repair_predicates_in_term const_tab)
blanchet@37961
   362
  in aux #> explicit_forall ? close_universally end
blanchet@37961
   363
blanchet@37961
   364
fun repair_problem_line thy explicit_forall full_types const_tab
blanchet@37961
   365
                        (Fof (ident, kind, phi)) =
blanchet@37961
   366
  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
blanchet@37961
   367
val repair_problem_with_const_table = map o apsnd o map oooo repair_problem_line
blanchet@37961
   368
blanchet@37961
   369
fun repair_problem thy explicit_forall full_types explicit_apply problem =
blanchet@37961
   370
  repair_problem_with_const_table thy explicit_forall full_types
blanchet@37643
   371
      (const_table_for_problem explicit_apply problem) problem
blanchet@37509
   372
blanchet@37643
   373
fun write_tptp_file thy readable_names full_types explicit_apply file
blanchet@37643
   374
                    (conjectures, axiom_clauses, extra_clauses, helper_clauses,
blanchet@37925
   375
                     class_rel_clauses, arity_clauses) =
blanchet@37509
   376
  let
blanchet@37992
   377
    val explicit_forall = true (* ### FIXME *)
blanchet@37643
   378
    val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
blanchet@37926
   379
    val class_rel_lines =
blanchet@37926
   380
      map problem_line_for_class_rel_clause class_rel_clauses
blanchet@37926
   381
    val arity_lines = map problem_line_for_arity_clause arity_clauses
blanchet@37643
   382
    val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
blanchet@37643
   383
    val conjecture_lines =
blanchet@37643
   384
      map (problem_line_for_conjecture full_types) conjectures
blanchet@37643
   385
    val tfree_lines = problem_lines_for_free_types conjectures
blanchet@37961
   386
    val problem =
blanchet@37961
   387
      [("Relevant facts", axiom_lines),
blanchet@37961
   388
       ("Class relationships", class_rel_lines),
blanchet@37961
   389
       ("Arity declarations", arity_lines),
blanchet@37961
   390
       ("Helper facts", helper_lines),
blanchet@37961
   391
       ("Conjectures", conjecture_lines),
blanchet@37961
   392
       ("Type variables", tfree_lines)]
blanchet@37961
   393
      |> repair_problem thy explicit_forall full_types explicit_apply
blanchet@37643
   394
    val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
blanchet@37509
   395
    val conjecture_offset =
blanchet@37925
   396
      length axiom_lines + length class_rel_lines + length arity_lines
blanchet@37643
   397
      + length helper_lines
blanchet@37643
   398
    val _ = File.write_list file (strings_for_problem problem)
blanchet@37926
   399
  in
blanchet@37926
   400
    (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
blanchet@37926
   401
     conjecture_offset)
blanchet@37926
   402
  end
blanchet@37509
   403
blanchet@37509
   404
end;