src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
author blanchet
Tue Jun 29 09:19:16 2010 +0200 (2010-06-29)
changeset 37624 3ee568334813
parent 37617 f73cd4069f69
child 37642 06992bc8bdda
permissions -rw-r--r--
move "nice names" from Metis to TPTP format
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@37509
    15
  val write_tptp_file :
blanchet@37509
    16
    bool -> bool -> bool -> Path.T
blanchet@37509
    17
    -> hol_clause list * hol_clause list * hol_clause list * hol_clause list
blanchet@37509
    18
       * classrel_clause list * arity_clause list
blanchet@37509
    19
    -> name_pool option * int
blanchet@37509
    20
end;
blanchet@37509
    21
blanchet@37509
    22
structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
blanchet@37509
    23
struct
blanchet@37509
    24
blanchet@37578
    25
open Metis_Clauses
blanchet@37509
    26
open Sledgehammer_Util
blanchet@37509
    27
blanchet@37624
    28
type name_pool = string Symtab.table * string Symtab.table
blanchet@37624
    29
blanchet@37624
    30
fun empty_name_pool readable_names =
blanchet@37624
    31
  if readable_names then SOME (`I Symtab.empty) else NONE
blanchet@37624
    32
blanchet@37624
    33
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
blanchet@37624
    34
fun pool_map f xs =
blanchet@37624
    35
  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
blanchet@37624
    36
blanchet@37624
    37
fun translate_first_char f s =
blanchet@37624
    38
  String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
blanchet@37624
    39
fun readable_name full_name s =
blanchet@37624
    40
  let
blanchet@37624
    41
    val s = s |> Long_Name.base_name |> Name.desymbolize false
blanchet@37624
    42
    val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
blanchet@37624
    43
    val s' =
blanchet@37624
    44
      (s' |> rev
blanchet@37624
    45
          |> implode
blanchet@37624
    46
          |> String.translate
blanchet@37624
    47
                 (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
blanchet@37624
    48
                          else ""))
blanchet@37624
    49
      ^ replicate_string (String.size s - length s') "_"
blanchet@37624
    50
    val s' =
blanchet@37624
    51
      if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
blanchet@37624
    52
      else s'
blanchet@37624
    53
    (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
blanchet@37624
    54
       ("op &", "op |", etc.). *)
blanchet@37624
    55
    val s' = if s' = "equal" orelse s' = "op" then full_name else s'
blanchet@37624
    56
  in
blanchet@37624
    57
    case (Char.isLower (String.sub (full_name, 0)),
blanchet@37624
    58
          Char.isLower (String.sub (s', 0))) of
blanchet@37624
    59
      (true, false) => translate_first_char Char.toLower s'
blanchet@37624
    60
    | (false, true) => translate_first_char Char.toUpper s'
blanchet@37624
    61
    | _ => s'
blanchet@37624
    62
  end
blanchet@37624
    63
blanchet@37624
    64
fun nice_name (full_name, _) NONE = (full_name, NONE)
blanchet@37624
    65
  | nice_name (full_name, desired_name) (SOME the_pool) =
blanchet@37624
    66
    case Symtab.lookup (fst the_pool) full_name of
blanchet@37624
    67
      SOME nice_name => (nice_name, SOME the_pool)
blanchet@37624
    68
    | NONE =>
blanchet@37624
    69
      let
blanchet@37624
    70
        val nice_prefix = readable_name full_name desired_name
blanchet@37624
    71
        fun add j =
blanchet@37624
    72
          let
blanchet@37624
    73
            val nice_name = nice_prefix ^
blanchet@37624
    74
                            (if j = 0 then "" else "_" ^ Int.toString j)
blanchet@37624
    75
          in
blanchet@37624
    76
            case Symtab.lookup (snd the_pool) nice_name of
blanchet@37624
    77
              SOME full_name' =>
blanchet@37624
    78
              if full_name = full_name' then (nice_name, the_pool)
blanchet@37624
    79
              else add (j + 1)
blanchet@37624
    80
            | NONE =>
blanchet@37624
    81
              (nice_name,
blanchet@37624
    82
               (Symtab.update_new (full_name, nice_name) (fst the_pool),
blanchet@37624
    83
                Symtab.update_new (nice_name, full_name) (snd the_pool)))
blanchet@37624
    84
          end
blanchet@37624
    85
      in add 0 |> apsnd SOME end
blanchet@37624
    86
blanchet@37520
    87
type const_info = {min_arity: int, max_arity: int, sub_level: bool}
blanchet@37520
    88
blanchet@37509
    89
val clause_prefix = "cls_"
blanchet@37509
    90
val arity_clause_prefix = "clsarity_"
blanchet@37509
    91
blanchet@37509
    92
fun paren_pack [] = ""
blanchet@37509
    93
  | paren_pack strings = "(" ^ commas strings ^ ")"
blanchet@37509
    94
blanchet@37509
    95
fun string_of_fol_type (TyVar sp) pool = nice_name sp pool
blanchet@37509
    96
  | string_of_fol_type (TyFree sp) pool = nice_name sp pool
blanchet@37509
    97
  | string_of_fol_type (TyConstr (sp, tys)) pool =
blanchet@37509
    98
    let
blanchet@37509
    99
      val (s, pool) = nice_name sp pool
blanchet@37509
   100
      val (ss, pool) = pool_map string_of_fol_type tys pool
blanchet@37509
   101
    in (s ^ paren_pack ss, pool) end
blanchet@37509
   102
blanchet@37509
   103
(* True if the constant ever appears outside of the top-level position in
blanchet@37520
   104
   literals, or if it appears with different arities (e.g., because of different
blanchet@37520
   105
   type instantiations). If false, the constant always receives all of its
blanchet@37520
   106
   arguments and is used as a predicate. *)
blanchet@37520
   107
fun needs_hBOOL NONE _ = true
blanchet@37520
   108
  | needs_hBOOL (SOME the_const_tab) c =
blanchet@37520
   109
    case Symtab.lookup the_const_tab c of
blanchet@37520
   110
      SOME ({min_arity, max_arity, sub_level} : const_info) =>
blanchet@37520
   111
      sub_level orelse min_arity < max_arity
blanchet@37520
   112
    | NONE => false
blanchet@37509
   113
blanchet@37520
   114
fun head_needs_hBOOL const_tab (CombConst ((c, _), _, _)) =
blanchet@37520
   115
    needs_hBOOL const_tab c
blanchet@37520
   116
  | head_needs_hBOOL _ _ = true
blanchet@37509
   117
blanchet@37509
   118
fun wrap_type full_types (s, ty) pool =
blanchet@37509
   119
  if full_types then
blanchet@37509
   120
    let val (s', pool) = string_of_fol_type ty pool in
blanchet@37509
   121
      (type_wrapper_name ^ paren_pack [s, s'], pool)
blanchet@37509
   122
    end
blanchet@37509
   123
  else
blanchet@37509
   124
    (s, pool)
blanchet@37509
   125
blanchet@37520
   126
fun wrap_type_if (full_types, const_tab) (head, s, tp) =
blanchet@37520
   127
  if head_needs_hBOOL const_tab head then wrap_type full_types (s, tp)
blanchet@37520
   128
  else pair s
blanchet@37509
   129
blanchet@37509
   130
fun apply ss = "hAPP" ^ paren_pack ss;
blanchet@37509
   131
blanchet@37509
   132
fun rev_apply (v, []) = v
blanchet@37509
   133
  | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
blanchet@37509
   134
blanchet@37509
   135
fun string_apply (v, args) = rev_apply (v, rev args)
blanchet@37509
   136
blanchet@37520
   137
fun min_arity_of NONE _ = 0
blanchet@37520
   138
  | min_arity_of (SOME the_const_tab) c =
blanchet@37520
   139
    case Symtab.lookup the_const_tab c of
blanchet@37520
   140
      SOME ({min_arity, ...} : const_info) => min_arity
blanchet@37520
   141
    | NONE => 0
blanchet@37509
   142
blanchet@37509
   143
(* Apply an operator to the argument strings, using either the "apply" operator
blanchet@37509
   144
   or direct function application. *)
blanchet@37520
   145
fun string_of_application (full_types, const_tab)
blanchet@37519
   146
                          (CombConst ((s, s'), _, tvars), args) pool =
blanchet@37509
   147
    let
blanchet@37509
   148
      val s = if s = "equal" then "c_fequal" else s
blanchet@37520
   149
      val nargs = min_arity_of const_tab s
blanchet@37509
   150
      val args1 = List.take (args, nargs)
blanchet@37509
   151
        handle Subscript =>
blanchet@37509
   152
               raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
blanchet@37509
   153
                           " but is applied to " ^ commas (map quote args))
blanchet@37509
   154
      val args2 = List.drop (args, nargs)
blanchet@37509
   155
      val (targs, pool) = if full_types then ([], pool)
blanchet@37509
   156
                          else pool_map string_of_fol_type tvars pool
blanchet@37509
   157
      val (s, pool) = nice_name (s, s') pool
blanchet@37509
   158
    in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
blanchet@37520
   159
  | string_of_application _ (CombVar (name, _), args) pool =
blanchet@37509
   160
    nice_name name pool |>> (fn s => string_apply (s, args))
blanchet@37509
   161
blanchet@37520
   162
fun string_of_combterm params t pool =
blanchet@37509
   163
  let
blanchet@37509
   164
    val (head, args) = strip_combterm_comb t
blanchet@37509
   165
    val (ss, pool) = pool_map (string_of_combterm params) args pool
blanchet@37520
   166
    val (s, pool) = string_of_application params (head, ss) pool
blanchet@37520
   167
  in wrap_type_if params (head, s, type_of_combterm t) pool end
blanchet@37509
   168
blanchet@37509
   169
(*Boolean-valued terms are here converted to literals.*)
blanchet@37509
   170
fun boolify params c =
blanchet@37509
   171
  string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
blanchet@37509
   172
blanchet@37520
   173
fun string_of_predicate (params as (_, const_tab)) t =
blanchet@37509
   174
  case #1 (strip_combterm_comb t) of
blanchet@37509
   175
    CombConst ((s, _), _, _) =>
blanchet@37520
   176
    (if needs_hBOOL const_tab s then boolify else string_of_combterm) params t
blanchet@37509
   177
  | _ => boolify params t
blanchet@37509
   178
blanchet@37509
   179
fun tptp_of_equality params pos (t1, t2) =
blanchet@37509
   180
  pool_map (string_of_combterm params) [t1, t2]
blanchet@37509
   181
  #>> space_implode (if pos then " = " else " != ")
blanchet@37509
   182
blanchet@37509
   183
fun tptp_sign true s = s
blanchet@37509
   184
  | tptp_sign false s = "~ " ^ s
blanchet@37509
   185
blanchet@37509
   186
fun tptp_literal params
blanchet@37509
   187
        (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
blanchet@37509
   188
                                         t2))) =
blanchet@37509
   189
    tptp_of_equality params pos (t1, t2)
blanchet@37509
   190
  | tptp_literal params (Literal (pos, pred)) =
blanchet@37509
   191
    string_of_predicate params pred #>> tptp_sign pos
blanchet@37509
   192
 
blanchet@37509
   193
fun tptp_of_type_literal pos (TyLitVar (s, name)) =
blanchet@37509
   194
    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
blanchet@37509
   195
  | tptp_of_type_literal pos (TyLitFree (s, name)) =
blanchet@37509
   196
    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
blanchet@37509
   197
blanchet@37509
   198
(* Given a clause, returns its literals paired with a list of literals
blanchet@37509
   199
   concerning TFrees; the latter should only occur in conjecture clauses. *)
blanchet@37509
   200
fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
blanchet@37509
   201
                       pool =
blanchet@37509
   202
  let
blanchet@37509
   203
    val (lits, pool) = pool_map (tptp_literal params) literals pool
blanchet@37509
   204
    val (tylits, pool) = pool_map (tptp_of_type_literal pos)
blanchet@37509
   205
                                  (type_literals_for_types ctypes_sorts) pool
blanchet@37509
   206
  in ((lits, tylits), pool) end
blanchet@37509
   207
blanchet@37509
   208
fun tptp_cnf name kind formula =
blanchet@37509
   209
  "cnf(" ^ name ^ ", " ^ kind ^ ",\n    " ^ formula ^ ").\n"
blanchet@37509
   210
blanchet@37509
   211
fun tptp_raw_clause strings = "(" ^ space_implode " | " strings ^ ")"
blanchet@37509
   212
blanchet@37509
   213
val tptp_tfree_clause =
blanchet@37509
   214
  tptp_cnf "tfree_tcs" "negated_conjecture" o tptp_raw_clause o single
blanchet@37509
   215
blanchet@37509
   216
fun tptp_classrel_literals sub sup =
blanchet@37509
   217
  let val tvar = "(T)" in
blanchet@37509
   218
    tptp_raw_clause [tptp_sign false (sub ^ tvar), tptp_sign true (sup ^ tvar)]
blanchet@37509
   219
  end
blanchet@37509
   220
blanchet@37509
   221
fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
blanchet@37509
   222
                pool =
blanchet@37509
   223
  let
blanchet@37509
   224
    val ((lits, tylits), pool) =
blanchet@37509
   225
      tptp_type_literals params (kind = Conjecture) cls pool
blanchet@37509
   226
    val name = clause_prefix ^ ascii_of axiom_name ^ "_" ^
blanchet@37509
   227
               Int.toString clause_id
blanchet@37509
   228
    val cnf =
blanchet@37509
   229
      case kind of
blanchet@37509
   230
        Axiom => tptp_cnf name "axiom" (tptp_raw_clause (tylits @ lits))
blanchet@37509
   231
      | Conjecture => tptp_cnf name "negated_conjecture" (tptp_raw_clause lits)
blanchet@37509
   232
  in ((cnf, tylits), pool) end
blanchet@37509
   233
blanchet@37509
   234
fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass,
blanchet@37509
   235
                                          ...}) =
blanchet@37509
   236
  tptp_cnf axiom_name "axiom" (tptp_classrel_literals subclass superclass)
blanchet@37509
   237
blanchet@37509
   238
fun tptp_of_arity_literal (TConsLit (c, t, args)) =
blanchet@37509
   239
    tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
blanchet@37509
   240
  | tptp_of_arity_literal (TVarLit (c, str)) =
blanchet@37509
   241
    tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
blanchet@37509
   242
blanchet@37509
   243
fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) =
blanchet@37509
   244
  tptp_cnf (arity_clause_prefix ^ ascii_of axiom_name) "axiom"
blanchet@37509
   245
           (tptp_raw_clause (map tptp_of_arity_literal (conclLit :: premLits)))
blanchet@37509
   246
blanchet@37520
   247
(* Find the minimal arity of each function mentioned in the term. Also, note
blanchet@37520
   248
   which uses are not at top level, to see if "hBOOL" is needed. *)
blanchet@37617
   249
fun count_constants_term top_level t =
blanchet@37617
   250
  let val (head, args) = strip_combterm_comb t in
blanchet@37617
   251
    (case head of
blanchet@37617
   252
       CombConst ((a, _), _, _) =>
blanchet@37617
   253
       let
blanchet@37617
   254
         (* Predicate or function version of "equal"? *)
blanchet@37617
   255
         val a = if a = "equal" andalso not top_level then "c_fequal" else a
blanchet@37617
   256
         val n = length args
blanchet@37617
   257
       in
blanchet@37617
   258
         Symtab.map_default
blanchet@37617
   259
             (a, {min_arity = n, max_arity = 0, sub_level = false})
blanchet@37617
   260
             (fn {min_arity, max_arity, sub_level} =>
blanchet@37617
   261
                 {min_arity = Int.min (n, min_arity),
blanchet@37617
   262
                  max_arity = Int.max (n, max_arity),
blanchet@37617
   263
                  sub_level = sub_level orelse not top_level})
blanchet@37617
   264
       end
blanchet@37617
   265
     | _ => I)
blanchet@37617
   266
    #> fold (count_constants_term false) args
blanchet@37509
   267
  end
blanchet@37520
   268
fun count_constants_literal (Literal (_, t)) = count_constants_term true t
blanchet@37509
   269
fun count_constants_clause (HOLClause {literals, ...}) =
blanchet@37520
   270
  fold count_constants_literal literals
blanchet@37520
   271
fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
blanchet@37520
   272
  fold (fold count_constants_clause)
blanchet@37520
   273
       [conjectures, extra_clauses, helper_clauses]
blanchet@37509
   274
blanchet@37509
   275
fun write_tptp_file readable_names full_types explicit_apply file clauses =
blanchet@37509
   276
  let
blanchet@37509
   277
    fun section _ [] = []
blanchet@37509
   278
      | section name ss =
blanchet@37509
   279
        "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^
blanchet@37509
   280
        ")\n" :: ss
blanchet@37509
   281
    val pool = empty_name_pool readable_names
blanchet@37509
   282
    val (conjectures, axclauses, _, helper_clauses,
blanchet@37509
   283
      classrel_clauses, arity_clauses) = clauses
blanchet@37520
   284
    val const_tab = if explicit_apply then NONE
blanchet@37520
   285
                    else SOME (Symtab.empty |> count_constants clauses)
blanchet@37520
   286
    val params = (full_types, const_tab)
blanchet@37509
   287
    val ((conjecture_clss, tfree_litss), pool) =
blanchet@37509
   288
      pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
blanchet@37509
   289
    val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
blanchet@37509
   290
    val (ax_clss, pool) =
blanchet@37509
   291
      pool_map (apfst fst oo tptp_clause params) axclauses pool
blanchet@37509
   292
    val classrel_clss = map tptp_classrel_clause classrel_clauses
blanchet@37509
   293
    val arity_clss = map tptp_arity_clause arity_clauses
blanchet@37509
   294
    val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
blanchet@37509
   295
                                       helper_clauses pool
blanchet@37509
   296
    val conjecture_offset =
blanchet@37509
   297
      length ax_clss + length classrel_clss + length arity_clss
blanchet@37509
   298
      + length helper_clss
blanchet@37509
   299
    val _ =
blanchet@37509
   300
      File.write_list file
blanchet@37509
   301
          ("% This file was generated by Isabelle (most likely Sledgehammer)\n\
blanchet@37509
   302
           \% " ^ timestamp () ^ "\n" ::
blanchet@37509
   303
           section "Relevant fact" ax_clss @
blanchet@37509
   304
           section "Class relationship" classrel_clss @
blanchet@37509
   305
           section "Arity declaration" arity_clss @
blanchet@37509
   306
           section "Helper fact" helper_clss @
blanchet@37509
   307
           section "Conjecture" conjecture_clss @
blanchet@37509
   308
           section "Type variable" tfree_clss)
blanchet@37509
   309
  in (pool, conjecture_offset) end
blanchet@37509
   310
blanchet@37509
   311
end;