src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML

first step in using "fof" rather than "cnf" in TPTP problems

(*  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 class_rel_clause = Metis_Clauses.class_rel_clause
  type arity_clause = Metis_Clauses.arity_clause
  type fol_clause = Metis_Clauses.fol_clause

  val write_tptp_file :
    theory -> bool -> bool -> bool -> Path.T
    -> fol_clause list * fol_clause list * fol_clause list * fol_clause 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 | AIff
datatype 'a formula =
  AQuant of quantifier * 'a list * 'a formula |
  AConn of connective * 'a formula list |
  APred of 'a fo_term

fun mk_anot phi = AConn (ANot, [phi])

datatype 'a problem_line = Fof of string * kind * 'a 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 AIff = "<=>"
fun string_for_formula (AQuant (q, xs, phi)) =
    string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^
    string_for_formula phi
  | 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 **)

val clause_prefix = "cls_"
val arity_clause_prefix = "clsarity_"

fun hol_ident axiom_name clause_id =
  clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id

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_term_for_combterm full_types 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 (fo_term_for_combterm full_types false) args)
  in
    if full_types then wrap_type (fo_term_for_combtyp (type_of_combterm u)) t
    else t
  end

fun fo_literal_for_literal full_types (FOLLiteral (pos, t)) =
  (pos, fo_term_for_combterm full_types true t)

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

fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), []))
  | formula_for_fo_literals (lit :: lits) =
    AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits])

fun formula_for_axiom full_types (FOLClause {literals, ctypes_sorts, ...}) =
  map (fo_literal_for_literal full_types) literals @
  map (fo_literal_for_type_literal false)
      (type_literals_for_types ctypes_sorts)
  |> formula_for_fo_literals

fun problem_line_for_axiom full_types
        (clause as FOLClause {axiom_name, clause_id, kind, ...}) =
  Fof (hol_ident axiom_name clause_id, kind,
       formula_for_axiom full_types clause)

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,
       map fo_literal_for_arity_literal (conclLit :: premLits)
       |> formula_for_fo_literals)

fun problem_line_for_conjecture full_types
        (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) =
  Fof (hol_ident axiom_name clause_id, kind,
       map (fo_literal_for_literal full_types) literals
       |> formula_for_fo_literals |> mk_anot)

fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
  map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)

fun problem_line_for_free_type lit =
  Fof ("tfree_tcs", Conjecture, formula_for_fo_literal lit)
fun problem_lines_for_free_types conjectures =
  let
    val litss = map atp_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 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)
val repair_problem_with_const_table = map o apsnd o map oooo repair_problem_line

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 full_types explicit_apply file
                    (conjectures, axiom_clauses, extra_clauses, helper_clauses,
                     class_rel_clauses, arity_clauses) =
  let
    val explicit_forall = true (* FIXME *)
    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
    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;