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