src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
author blanchet
Thu Jul 22 11:29:31 2010 +0200 (2010-07-22)
changeset 37931 7b452ff6bff0
parent 37926 e6ff246c0cdb
child 37961 6a48c85a211a
permissions -rw-r--r--
no polymorphic "var"s
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@37509
    14
  val write_tptp_file :
blanchet@37643
    15
    theory -> bool -> bool -> bool -> Path.T
blanchet@37922
    16
    -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
blanchet@37925
    17
       * class_rel_clause list * arity_clause list
blanchet@37926
    18
    -> string Symtab.table * int
blanchet@37509
    19
end;
blanchet@37509
    20
blanchet@37509
    21
structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
blanchet@37509
    22
struct
blanchet@37509
    23
blanchet@37578
    24
open Metis_Clauses
blanchet@37509
    25
open Sledgehammer_Util
blanchet@37509
    26
blanchet@37643
    27
blanchet@37643
    28
(** ATP problem **)
blanchet@37643
    29
blanchet@37643
    30
datatype 'a atp_term = ATerm of 'a * 'a atp_term list
blanchet@37643
    31
type 'a atp_literal = bool * 'a atp_term
blanchet@37643
    32
datatype 'a problem_line = Cnf of string * kind * 'a atp_literal list
blanchet@37643
    33
type 'a problem = (string * 'a problem_line list) list
blanchet@37643
    34
blanchet@37643
    35
fun string_for_atp_term (ATerm (s, [])) = s
blanchet@37643
    36
  | string_for_atp_term (ATerm (s, ts)) =
blanchet@37643
    37
    s ^ "(" ^ commas (map string_for_atp_term ts) ^ ")"
blanchet@37643
    38
fun string_for_atp_literal (pos, ATerm ("equal", [t1, t2])) =
blanchet@37643
    39
    string_for_atp_term t1 ^ " " ^ (if pos then "=" else "!=") ^ " " ^
blanchet@37643
    40
    string_for_atp_term t2
blanchet@37643
    41
  | string_for_atp_literal (pos, t) =
blanchet@37643
    42
    (if pos then "" else "~ ") ^ string_for_atp_term t
blanchet@37643
    43
fun string_for_problem_line (Cnf (ident, kind, lits)) =
blanchet@37643
    44
  "cnf(" ^ ident ^ ", " ^
blanchet@37643
    45
  (case kind of Axiom => "axiom" | Conjecture => "negated_conjecture") ^ ",\n" ^
blanchet@37643
    46
  "    (" ^ space_implode " | " (map string_for_atp_literal lits) ^ ")).\n"
blanchet@37643
    47
fun strings_for_problem problem =
blanchet@37643
    48
  "% This file was generated by Isabelle (most likely Sledgehammer)\n\
blanchet@37643
    49
  \% " ^ timestamp () ^ "\n" ::
blanchet@37643
    50
  maps (fn (_, []) => []
blanchet@37643
    51
         | (heading, lines) =>
blanchet@37643
    52
           "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
blanchet@37643
    53
           map string_for_problem_line lines) problem
blanchet@37643
    54
blanchet@37643
    55
blanchet@37643
    56
(** Nice names **)
blanchet@37643
    57
blanchet@37624
    58
fun empty_name_pool readable_names =
blanchet@37643
    59
  if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
blanchet@37624
    60
blanchet@37624
    61
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
blanchet@37624
    62
fun pool_map f xs =
blanchet@37624
    63
  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
blanchet@37624
    64
blanchet@37643
    65
(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
blanchet@37643
    66
   unreadable "op_1", "op_2", etc., in the problem files. *)
blanchet@37643
    67
val reserved_nice_names = ["equal", "op"]
blanchet@37624
    68
fun readable_name full_name s =
blanchet@37643
    69
  if s = full_name then
blanchet@37643
    70
    s
blanchet@37643
    71
  else
blanchet@37643
    72
    let
blanchet@37643
    73
      val s = s |> Long_Name.base_name
blanchet@37643
    74
                |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
blanchet@37643
    75
    in if member (op =) reserved_nice_names s then full_name else s end
blanchet@37624
    76
blanchet@37624
    77
fun nice_name (full_name, _) NONE = (full_name, NONE)
blanchet@37624
    78
  | nice_name (full_name, desired_name) (SOME the_pool) =
blanchet@37624
    79
    case Symtab.lookup (fst the_pool) full_name of
blanchet@37624
    80
      SOME nice_name => (nice_name, SOME the_pool)
blanchet@37624
    81
    | NONE =>
blanchet@37624
    82
      let
blanchet@37624
    83
        val nice_prefix = readable_name full_name desired_name
blanchet@37624
    84
        fun add j =
blanchet@37624
    85
          let
blanchet@37624
    86
            val nice_name = nice_prefix ^
blanchet@37624
    87
                            (if j = 0 then "" else "_" ^ Int.toString j)
blanchet@37624
    88
          in
blanchet@37624
    89
            case Symtab.lookup (snd the_pool) nice_name of
blanchet@37624
    90
              SOME full_name' =>
blanchet@37624
    91
              if full_name = full_name' then (nice_name, the_pool)
blanchet@37624
    92
              else add (j + 1)
blanchet@37624
    93
            | NONE =>
blanchet@37624
    94
              (nice_name,
blanchet@37624
    95
               (Symtab.update_new (full_name, nice_name) (fst the_pool),
blanchet@37624
    96
                Symtab.update_new (nice_name, full_name) (snd the_pool)))
blanchet@37624
    97
          end
blanchet@37624
    98
      in add 0 |> apsnd SOME end
blanchet@37624
    99
blanchet@37643
   100
fun nice_atp_term (ATerm (name, ts)) =
blanchet@37643
   101
  nice_name name ##>> pool_map nice_atp_term ts #>> ATerm
blanchet@37643
   102
fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos
blanchet@37643
   103
fun nice_problem_line (Cnf (ident, kind, lits)) =
blanchet@37643
   104
  pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits))
blanchet@37931
   105
fun nice_problem problem =
blanchet@37643
   106
  pool_map (fn (heading, lines) =>
blanchet@37931
   107
               pool_map nice_problem_line lines #>> pair heading) problem
blanchet@37643
   108
blanchet@37643
   109
blanchet@37643
   110
(** Sledgehammer stuff **)
blanchet@37520
   111
blanchet@37509
   112
val clause_prefix = "cls_"
blanchet@37509
   113
val arity_clause_prefix = "clsarity_"
blanchet@37509
   114
blanchet@37643
   115
fun hol_ident axiom_name clause_id =
blanchet@37643
   116
  clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id
blanchet@37643
   117
blanchet@37643
   118
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
blanchet@37643
   119
blanchet@37924
   120
fun atp_term_for_combtyp (CombTVar name) = ATerm (name, [])
blanchet@37924
   121
  | atp_term_for_combtyp (CombTFree name) = ATerm (name, [])
blanchet@37924
   122
  | atp_term_for_combtyp (CombType (name, tys)) =
blanchet@37643
   123
    ATerm (name, map atp_term_for_combtyp tys)
blanchet@37643
   124
blanchet@37643
   125
fun atp_term_for_combterm full_types top_level u =
blanchet@37643
   126
  let
blanchet@37643
   127
    val (head, args) = strip_combterm_comb u
blanchet@37643
   128
    val (x, ty_args) =
blanchet@37643
   129
      case head of
blanchet@37643
   130
        CombConst (name, _, ty_args) =>
blanchet@37643
   131
        if fst name = "equal" then
blanchet@37643
   132
          (if top_level andalso length args = 2 then name
blanchet@37643
   133
           else ("c_fequal", @{const_name fequal}), [])
blanchet@37643
   134
        else
blanchet@37643
   135
          (name, if full_types then [] else ty_args)
blanchet@37643
   136
      | CombVar (name, _) => (name, [])
blanchet@37643
   137
      | CombApp _ => raise Fail "impossible \"CombApp\""
blanchet@37643
   138
    val t = ATerm (x, map atp_term_for_combtyp ty_args @
blanchet@37643
   139
                      map (atp_term_for_combterm full_types false) args)
blanchet@37643
   140
  in
blanchet@37643
   141
    if full_types then wrap_type (atp_term_for_combtyp (type_of_combterm u)) t
blanchet@37643
   142
    else t
blanchet@37643
   143
  end
blanchet@37643
   144
blanchet@37923
   145
fun atp_literal_for_literal full_types (FOLLiteral (pos, t)) =
blanchet@37643
   146
  (pos, atp_term_for_combterm full_types true t)
blanchet@37643
   147
blanchet@37643
   148
fun atp_literal_for_type_literal pos (TyLitVar (class, name)) =
blanchet@37643
   149
    (pos, ATerm (class, [ATerm (name, [])]))
blanchet@37643
   150
  | atp_literal_for_type_literal pos (TyLitFree (class, name)) =
blanchet@37643
   151
    (pos, ATerm (class, [ATerm (name, [])]))
blanchet@37643
   152
blanchet@37643
   153
fun atp_literals_for_axiom full_types
blanchet@37922
   154
                           (FOLClause {literals, ctypes_sorts, ...}) =
blanchet@37643
   155
  map (atp_literal_for_literal full_types) literals @
blanchet@37643
   156
  map (atp_literal_for_type_literal false)
blanchet@37643
   157
      (type_literals_for_types ctypes_sorts)
blanchet@37643
   158
blanchet@37643
   159
fun problem_line_for_axiom full_types
blanchet@37922
   160
        (clause as FOLClause {axiom_name, clause_id, kind, ...}) =
blanchet@37643
   161
  Cnf (hol_ident axiom_name clause_id, kind,
blanchet@37643
   162
       atp_literals_for_axiom full_types clause)
blanchet@37643
   163
blanchet@37926
   164
fun problem_line_for_class_rel_clause
blanchet@37925
   165
        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
blanchet@37643
   166
  let val ty_arg = ATerm (("T", "T"), []) in
blanchet@37643
   167
    Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
blanchet@37643
   168
                                      (true, ATerm (superclass, [ty_arg]))])
blanchet@37643
   169
  end
blanchet@37643
   170
blanchet@37643
   171
fun atp_literal_for_arity_literal (TConsLit (c, t, args)) =
blanchet@37643
   172
    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
blanchet@37643
   173
  | atp_literal_for_arity_literal (TVarLit (c, sort)) =
blanchet@37643
   174
    (false, ATerm (c, [ATerm (sort, [])]))
blanchet@37643
   175
blanchet@37926
   176
fun problem_line_for_arity_clause
blanchet@37926
   177
        (ArityClause {axiom_name, conclLit, premLits, ...}) =
blanchet@37643
   178
  Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
blanchet@37643
   179
       map atp_literal_for_arity_literal (conclLit :: premLits))
blanchet@37643
   180
blanchet@37643
   181
fun problem_line_for_conjecture full_types
blanchet@37922
   182
        (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) =
blanchet@37643
   183
  Cnf (hol_ident axiom_name clause_id, kind,
blanchet@37643
   184
       map (atp_literal_for_literal full_types) literals)
blanchet@37643
   185
blanchet@37922
   186
fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
blanchet@37643
   187
  map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
blanchet@37509
   188
blanchet@37643
   189
fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit])
blanchet@37643
   190
fun problem_lines_for_free_types conjectures =
blanchet@37643
   191
  let
blanchet@37643
   192
    val litss = map atp_free_type_literals_for_conjecture conjectures
blanchet@37643
   193
    val lits = fold (union (op =)) litss []
blanchet@37643
   194
  in map problem_line_for_free_type lits end
blanchet@37643
   195
blanchet@37643
   196
(** "hBOOL" and "hAPP" **)
blanchet@37643
   197
blanchet@37643
   198
type const_info = {min_arity: int, max_arity: int, sub_level: bool}
blanchet@37643
   199
blanchet@37643
   200
fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
blanchet@37643
   201
blanchet@37643
   202
fun consider_term top_level (ATerm ((s, _), ts)) =
blanchet@37643
   203
  (if is_atp_variable s then
blanchet@37643
   204
     I
blanchet@37643
   205
   else
blanchet@37643
   206
     let val n = length ts in
blanchet@37643
   207
       Symtab.map_default
blanchet@37643
   208
           (s, {min_arity = n, max_arity = 0, sub_level = false})
blanchet@37643
   209
           (fn {min_arity, max_arity, sub_level} =>
blanchet@37643
   210
               {min_arity = Int.min (n, min_arity),
blanchet@37643
   211
                max_arity = Int.max (n, max_arity),
blanchet@37643
   212
                sub_level = sub_level orelse not top_level})
blanchet@37643
   213
     end)
blanchet@37643
   214
  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
blanchet@37643
   215
fun consider_literal (_, t) = consider_term true t
blanchet@37643
   216
fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits
blanchet@37931
   217
fun consider_problem problem = fold (fold consider_problem_line o snd) problem
blanchet@37643
   218
blanchet@37643
   219
fun const_table_for_problem explicit_apply problem =
blanchet@37643
   220
  if explicit_apply then NONE
blanchet@37643
   221
  else SOME (Symtab.empty |> consider_problem problem)
blanchet@37643
   222
blanchet@37643
   223
val tc_fun = make_fixed_type_const @{type_name fun}
blanchet@37643
   224
blanchet@37643
   225
fun min_arity_of thy full_types NONE s =
blanchet@37643
   226
    (if s = "equal" orelse s = type_wrapper_name orelse
blanchet@37643
   227
        String.isPrefix type_const_prefix s orelse
blanchet@37643
   228
        String.isPrefix class_prefix s then
blanchet@37643
   229
       16383 (* large number *)
blanchet@37643
   230
     else if full_types then
blanchet@37643
   231
       0
blanchet@37643
   232
     else case strip_prefix const_prefix s of
blanchet@37643
   233
       SOME s' => num_type_args thy (invert_const s')
blanchet@37643
   234
     | NONE => 0)
blanchet@37643
   235
  | min_arity_of _ _ (SOME the_const_tab) s =
blanchet@37643
   236
    case Symtab.lookup the_const_tab s of
blanchet@37643
   237
      SOME ({min_arity, ...} : const_info) => min_arity
blanchet@37643
   238
    | NONE => 0
blanchet@37643
   239
blanchet@37643
   240
fun full_type_of (ATerm ((s, _), [ty, _])) =
blanchet@37643
   241
    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
blanchet@37643
   242
  | full_type_of _ = raise Fail "expected type wrapper"
blanchet@37643
   243
blanchet@37643
   244
fun list_hAPP_rev _ t1 [] = t1
blanchet@37643
   245
  | list_hAPP_rev NONE t1 (t2 :: ts2) =
blanchet@37643
   246
    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
blanchet@37643
   247
  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
blanchet@37643
   248
    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
blanchet@37643
   249
                         [full_type_of t2, ty]) in
blanchet@37643
   250
      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
blanchet@37643
   251
    end
blanchet@37643
   252
blanchet@37643
   253
fun repair_applications_in_term thy full_types const_tab =
blanchet@37643
   254
  let
blanchet@37643
   255
    fun aux opt_ty (ATerm (name as (s, _), ts)) =
blanchet@37643
   256
      if s = type_wrapper_name then
blanchet@37643
   257
        case ts of
blanchet@37643
   258
          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
blanchet@37643
   259
        | _ => raise Fail "malformed type wrapper"
blanchet@37643
   260
      else
blanchet@37643
   261
        let
blanchet@37643
   262
          val ts = map (aux NONE) ts
blanchet@37643
   263
          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
blanchet@37643
   264
        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
blanchet@37643
   265
  in aux NONE end
blanchet@37643
   266
blanchet@37643
   267
fun boolify t = ATerm (`I "hBOOL", [t])
blanchet@37509
   268
blanchet@37509
   269
(* True if the constant ever appears outside of the top-level position in
blanchet@37520
   270
   literals, or if it appears with different arities (e.g., because of different
blanchet@37520
   271
   type instantiations). If false, the constant always receives all of its
blanchet@37520
   272
   arguments and is used as a predicate. *)
blanchet@37643
   273
fun is_predicate NONE s =
blanchet@37643
   274
    s = "equal" orelse String.isPrefix type_const_prefix s orelse
blanchet@37643
   275
    String.isPrefix class_prefix s
blanchet@37643
   276
  | is_predicate (SOME the_const_tab) s =
blanchet@37643
   277
    case Symtab.lookup the_const_tab s of
blanchet@37643
   278
      SOME {min_arity, max_arity, sub_level} =>
blanchet@37643
   279
      not sub_level andalso min_arity = max_arity
blanchet@37520
   280
    | NONE => false
blanchet@37509
   281
blanchet@37643
   282
fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
blanchet@37643
   283
  if s = type_wrapper_name then
blanchet@37643
   284
    case ts of
blanchet@37643
   285
      [_, t' as ATerm ((s', _), _)] =>
blanchet@37643
   286
      if is_predicate const_tab s' then t' else boolify t
blanchet@37643
   287
    | _ => raise Fail "malformed type wrapper"
blanchet@37509
   288
  else
blanchet@37643
   289
    t |> not (is_predicate const_tab s) ? boolify
blanchet@37509
   290
blanchet@37643
   291
fun repair_literal thy full_types const_tab (pos, t) =
blanchet@37643
   292
  (pos, t |> repair_applications_in_term thy full_types const_tab
blanchet@37643
   293
          |> repair_predicates_in_term const_tab)
blanchet@37643
   294
fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) =
blanchet@37643
   295
  Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits)
blanchet@37931
   296
fun repair_problem_with_const_table thy full_types const_tab problem =
blanchet@37931
   297
  map (apsnd (map (repair_problem_line thy full_types const_tab))) problem
blanchet@37643
   298
fun repair_problem thy full_types explicit_apply problem =
blanchet@37643
   299
  repair_problem_with_const_table thy full_types
blanchet@37643
   300
      (const_table_for_problem explicit_apply problem) problem
blanchet@37509
   301
blanchet@37643
   302
fun write_tptp_file thy readable_names full_types explicit_apply file
blanchet@37643
   303
                    (conjectures, axiom_clauses, extra_clauses, helper_clauses,
blanchet@37925
   304
                     class_rel_clauses, arity_clauses) =
blanchet@37509
   305
  let
blanchet@37643
   306
    val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
blanchet@37926
   307
    val class_rel_lines =
blanchet@37926
   308
      map problem_line_for_class_rel_clause class_rel_clauses
blanchet@37926
   309
    val arity_lines = map problem_line_for_arity_clause arity_clauses
blanchet@37643
   310
    val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
blanchet@37643
   311
    val conjecture_lines =
blanchet@37643
   312
      map (problem_line_for_conjecture full_types) conjectures
blanchet@37643
   313
    val tfree_lines = problem_lines_for_free_types conjectures
blanchet@37643
   314
    val problem = [("Relevant facts", axiom_lines),
blanchet@37925
   315
                   ("Class relationships", class_rel_lines),
blanchet@37643
   316
                   ("Arity declarations", arity_lines),
blanchet@37643
   317
                   ("Helper facts", helper_lines),
blanchet@37643
   318
                   ("Conjectures", conjecture_lines),
blanchet@37643
   319
                   ("Type variables", tfree_lines)]
blanchet@37643
   320
                  |> repair_problem thy full_types explicit_apply
blanchet@37643
   321
    val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
blanchet@37509
   322
    val conjecture_offset =
blanchet@37925
   323
      length axiom_lines + length class_rel_lines + length arity_lines
blanchet@37643
   324
      + length helper_lines
blanchet@37643
   325
    val _ = File.write_list file (strings_for_problem problem)
blanchet@37926
   326
  in
blanchet@37926
   327
    (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
blanchet@37926
   328
     conjecture_offset)
blanchet@37926
   329
  end
blanchet@37509
   330
blanchet@37509
   331
end;