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