src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML

no polymorphic "var"

(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
    Author:     Jia Meng, NICTA
    Author:     Jasmin Blanchette, TU Muenchen

TPTP syntax.
*)

signature SLEDGEHAMMER_TPTP_FORMAT =
sig
  type name = Metis_Clauses.name
  type kind = Metis_Clauses.kind
  type combterm = Metis_Clauses.combterm
  type class_rel_clause = Metis_Clauses.class_rel_clause
  type arity_clause = Metis_Clauses.arity_clause

  datatype 'a fo_term = ATerm of 'a * 'a fo_term list
  datatype quantifier = AForall | AExists
  datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
  datatype ('a, 'b) formula =
    AQuant of quantifier * 'a list * ('a, 'b) formula |
    AConn of connective * ('a, 'b) formula list |
    APred of 'b

  datatype fol_formula =
    FOLFormula of {formula_name: string,
                   kind: kind,
                   combformula: (name, combterm) formula,
                   ctypes_sorts: typ list}

  val axiom_prefix : string
  val conjecture_prefix : string
  val write_tptp_file :
    theory -> bool -> bool -> bool -> bool -> Path.T
    -> fol_formula list * fol_formula list * fol_formula list * fol_formula list
       * class_rel_clause list * arity_clause list
    -> string Symtab.table * int
end;

structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
struct

open Metis_Clauses
open Sledgehammer_Util


(** ATP problem **)

datatype 'a fo_term = ATerm of 'a * 'a fo_term list
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
datatype ('a, 'b) formula =
  AQuant of quantifier * 'a list * ('a, 'b) formula |
  AConn of connective * ('a, 'b) formula list |
  APred of 'b

fun mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
fun mk_ahorn [] phi = phi
  | mk_ahorn (phi :: phis) psi =
    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])

datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list

fun string_for_term (ATerm (s, [])) = s
  | string_for_term (ATerm (s, ts)) =
    if s = "equal" then space_implode " = " (map string_for_term ts)
    else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
fun string_for_quantifier AForall = "!"
  | string_for_quantifier AExists = "?"
fun string_for_connective ANot = "~"
  | string_for_connective AAnd = "&"
  | string_for_connective AOr = "|"
  | string_for_connective AImplies = "=>"
  | string_for_connective AIf = "<="
  | string_for_connective AIff = "<=>"
  | string_for_connective ANotIff = "<~>"
fun string_for_formula (AQuant (q, xs, phi)) =
    string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
    string_for_formula phi
  | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
    space_implode " != " (map string_for_term ts)
  | string_for_formula (AConn (c, [phi])) =
    string_for_connective c ^ " " ^ string_for_formula phi
  | string_for_formula (AConn (c, phis)) =
    "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
                        (map string_for_formula phis) ^ ")"
  | string_for_formula (APred tm) = string_for_term tm

fun string_for_problem_line (Fof (ident, kind, phi)) =
  "fof(" ^ ident ^ ", " ^
  (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
  "    (" ^ string_for_formula phi ^ ")).\n"
fun strings_for_problem problem =
  "% This file was generated by Isabelle (most likely Sledgehammer)\n\
  \% " ^ timestamp () ^ "\n" ::
  maps (fn (_, []) => []
         | (heading, lines) =>
           "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
           map string_for_problem_line lines) problem


(** Nice names **)

fun empty_name_pool readable_names =
  if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE

fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
fun pool_map f xs =
  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []

(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
   unreadable "op_1", "op_2", etc., in the problem files. *)
val reserved_nice_names = ["equal", "op"]
fun readable_name full_name s =
  if s = full_name then
    s
  else
    let
      val s = s |> Long_Name.base_name
                |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
    in if member (op =) reserved_nice_names s then full_name else s end

fun nice_name (full_name, _) NONE = (full_name, NONE)
  | nice_name (full_name, desired_name) (SOME the_pool) =
    case Symtab.lookup (fst the_pool) full_name of
      SOME nice_name => (nice_name, SOME the_pool)
    | NONE =>
      let
        val nice_prefix = readable_name full_name desired_name
        fun add j =
          let
            val nice_name = nice_prefix ^
                            (if j = 0 then "" else "_" ^ Int.toString j)
          in
            case Symtab.lookup (snd the_pool) nice_name of
              SOME full_name' =>
              if full_name = full_name' then (nice_name, the_pool)
              else add (j + 1)
            | NONE =>
              (nice_name,
               (Symtab.update_new (full_name, nice_name) (fst the_pool),
                Symtab.update_new (nice_name, full_name) (snd the_pool)))
          end
      in add 0 |> apsnd SOME end


fun nice_term (ATerm (name, ts)) =
  nice_name name ##>> pool_map nice_term ts #>> ATerm
fun nice_formula (AQuant (q, xs, phi)) =
    pool_map nice_name xs ##>> nice_formula phi
    #>> (fn (xs, phi) => AQuant (q, xs, phi))
  | nice_formula (AConn (c, phis)) =
    pool_map nice_formula phis #>> curry AConn c
  | nice_formula (APred tm) = nice_term tm #>> APred
fun nice_problem_line (Fof (ident, kind, phi)) =
  nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
fun nice_problem problem =
  pool_map (fn (heading, lines) =>
               pool_map nice_problem_line lines #>> pair heading) problem


(** Sledgehammer stuff **)

datatype fol_formula =
  FOLFormula of {formula_name: string,
                 kind: kind,
                 combformula: (name, combterm) formula,
                 ctypes_sorts: typ list}

val axiom_prefix = "ax_"
val conjecture_prefix = "conj_"
val arity_clause_prefix = "clsarity_"
val tfrees_name = "tfrees"

fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])

fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
  | fo_term_for_combtyp (CombType (name, tys)) =
    ATerm (name, map fo_term_for_combtyp tys)

fun fo_literal_for_type_literal (TyLitVar (class, name)) =
    (true, ATerm (class, [ATerm (name, [])]))
  | fo_literal_for_type_literal (TyLitFree (class, name)) =
    (true, ATerm (class, [ATerm (name, [])]))

fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot

fun fo_term_for_combterm full_types =
  let
    fun aux top_level u =
      let
        val (head, args) = strip_combterm_comb u
        val (x, ty_args) =
          case head of
            CombConst (name, _, ty_args) =>
            if fst name = "equal" then
              (if top_level andalso length args = 2 then name
               else ("c_fequal", @{const_name fequal}), [])
            else
              (name, if full_types then [] else ty_args)
          | CombVar (name, _) => (name, [])
          | CombApp _ => raise Fail "impossible \"CombApp\""
        val t = ATerm (x, map fo_term_for_combtyp ty_args @
                          map (aux false) args)
    in
      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
    end
  in aux true end

fun formula_for_combformula full_types =
  let
    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
      | aux (AConn (c, phis)) = AConn (c, map aux phis)
      | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
  in aux end

fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
                (type_literals_for_types ctypes_sorts))
           (formula_for_combformula full_types combformula)

fun problem_line_for_axiom full_types
        (formula as FOLFormula {formula_name, kind, ...}) =
  Fof (axiom_prefix ^ ascii_of formula_name, kind,
       formula_for_axiom full_types formula)

fun problem_line_for_class_rel_clause
        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
  let val ty_arg = ATerm (("T", "T"), []) in
    Fof (ascii_of axiom_name, Axiom,
         AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
                           APred (ATerm (superclass, [ty_arg]))]))
  end

fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
    (false, ATerm (c, [ATerm (sort, [])]))

fun problem_line_for_arity_clause
        (ArityClause {axiom_name, conclLit, premLits, ...}) =
  Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
       mk_ahorn (map (formula_for_fo_literal o apfst not
                      o fo_literal_for_arity_literal) premLits)
                (formula_for_fo_literal
                     (fo_literal_for_arity_literal conclLit)))

fun problem_line_for_conjecture full_types
        (FOLFormula {formula_name, kind, combformula, ...}) =
  Fof (conjecture_prefix ^ formula_name, kind,
       formula_for_combformula full_types combformula)

fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)

fun problem_line_for_free_type lit =
  Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
fun problem_lines_for_free_types conjectures =
  let
    val litss = map free_type_literals_for_conjecture conjectures
    val lits = fold (union (op =)) litss []
  in map problem_line_for_free_type lits end

(** "hBOOL" and "hAPP" **)

type const_info = {min_arity: int, max_arity: int, sub_level: bool}

fun is_variable s = Char.isUpper (String.sub (s, 0))

fun consider_term top_level (ATerm ((s, _), ts)) =
  (if is_variable s then
     I
   else
     let val n = length ts in
       Symtab.map_default
           (s, {min_arity = n, max_arity = 0, sub_level = false})
           (fn {min_arity, max_arity, sub_level} =>
               {min_arity = Int.min (n, min_arity),
                max_arity = Int.max (n, max_arity),
                sub_level = sub_level orelse not top_level})
     end)
  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
  | consider_formula (AConn (_, phis)) = fold consider_formula phis
  | consider_formula (APred tm) = consider_term true tm

fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
fun consider_problem problem = fold (fold consider_problem_line o snd) problem

fun const_table_for_problem explicit_apply problem =
  if explicit_apply then NONE
  else SOME (Symtab.empty |> consider_problem problem)

val tc_fun = make_fixed_type_const @{type_name fun}

fun min_arity_of thy full_types NONE s =
    (if s = "equal" orelse s = type_wrapper_name orelse
        String.isPrefix type_const_prefix s orelse
        String.isPrefix class_prefix s then
       16383 (* large number *)
     else if full_types then
       0
     else case strip_prefix_and_undo_ascii const_prefix s of
       SOME s' => num_type_args thy (invert_const s')
     | NONE => 0)
  | min_arity_of _ _ (SOME the_const_tab) s =
    case Symtab.lookup the_const_tab s of
      SOME ({min_arity, ...} : const_info) => min_arity
    | NONE => 0

fun full_type_of (ATerm ((s, _), [ty, _])) =
    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
  | full_type_of _ = raise Fail "expected type wrapper"

fun list_hAPP_rev _ t1 [] = t1
  | list_hAPP_rev NONE t1 (t2 :: ts2) =
    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
                         [full_type_of t2, ty]) in
      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
    end

fun repair_applications_in_term thy full_types const_tab =
  let
    fun aux opt_ty (ATerm (name as (s, _), ts)) =
      if s = type_wrapper_name then
        case ts of
          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
        | _ => raise Fail "malformed type wrapper"
      else
        let
          val ts = map (aux NONE) ts
          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
  in aux NONE end

fun boolify t = ATerm (`I "hBOOL", [t])

(* True if the constant ever appears outside of the top-level position in
   literals, or if it appears with different arities (e.g., because of different
   type instantiations). If false, the constant always receives all of its
   arguments and is used as a predicate. *)
fun is_predicate NONE s =
    s = "equal" orelse String.isPrefix type_const_prefix s orelse
    String.isPrefix class_prefix s
  | is_predicate (SOME the_const_tab) s =
    case Symtab.lookup the_const_tab s of
      SOME {min_arity, max_arity, sub_level} =>
      not sub_level andalso min_arity = max_arity
    | NONE => false

fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
  if s = type_wrapper_name then
    case ts of
      [_, t' as ATerm ((s', _), _)] =>
      if is_predicate const_tab s' then t' else boolify t
    | _ => raise Fail "malformed type wrapper"
  else
    t |> not (is_predicate const_tab s) ? boolify

fun close_universally phi =
  let
    fun term_vars bounds (ATerm (name as (s, _), tms)) =
        (is_variable s andalso not (member (op =) bounds name))
          ? insert (op =) name
        #> fold (term_vars bounds) tms
    fun formula_vars bounds (AQuant (q, xs, phi)) =
        formula_vars (xs @ bounds) phi
      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
      | formula_vars bounds (APred tm) = term_vars bounds tm
  in
    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
  end

fun repair_formula thy explicit_forall full_types const_tab =
  let
    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
      | aux (AConn (c, phis)) = AConn (c, map aux phis)
      | aux (APred tm) =
        APred (tm |> repair_applications_in_term thy full_types const_tab
                  |> repair_predicates_in_term const_tab)
  in aux #> explicit_forall ? close_universally end

fun repair_problem_line thy explicit_forall full_types const_tab
                        (Fof (ident, kind, phi)) =
  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
fun repair_problem_with_const_table thy =
  map o apsnd o map ooo repair_problem_line thy

fun repair_problem thy explicit_forall full_types explicit_apply problem =
  repair_problem_with_const_table thy explicit_forall full_types
      (const_table_for_problem explicit_apply problem) problem

fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
                    file (conjectures, axiom_clauses, extra_clauses,
                          helper_clauses, class_rel_clauses, arity_clauses) =
  let
    val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
    val class_rel_lines =
      map problem_line_for_class_rel_clause class_rel_clauses
    val arity_lines = map problem_line_for_arity_clause arity_clauses
    val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
    val conjecture_lines =
      map (problem_line_for_conjecture full_types) conjectures
    val tfree_lines = problem_lines_for_free_types conjectures
    (* Reordering these might or might not confuse the proof reconstruction
       code or the SPASS Flotter hack. *)
    val problem =
      [("Relevant facts", axiom_lines),
       ("Class relationships", class_rel_lines),
       ("Arity declarations", arity_lines),
       ("Helper facts", helper_lines),
       ("Conjectures", conjecture_lines),
       ("Type variables", tfree_lines)]
      |> repair_problem thy explicit_forall full_types explicit_apply
    val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
    val conjecture_offset =
      length axiom_lines + length class_rel_lines + length arity_lines
      + length helper_lines
    val _ = File.write_list file (strings_for_problem problem)
  in
    (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
     conjecture_offset)
  end

end;