src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML

no polymorphic "var"s

(*  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 atp_term = ATerm of 'a * 'a atp_term list
type 'a atp_literal = bool * 'a atp_term
datatype 'a problem_line = Cnf of string * kind * 'a atp_literal list
type 'a problem = (string * 'a problem_line list) list

fun string_for_atp_term (ATerm (s, [])) = s
  | string_for_atp_term (ATerm (s, ts)) =
    s ^ "(" ^ commas (map string_for_atp_term ts) ^ ")"
fun string_for_atp_literal (pos, ATerm ("equal", [t1, t2])) =
    string_for_atp_term t1 ^ " " ^ (if pos then "=" else "!=") ^ " " ^
    string_for_atp_term t2
  | string_for_atp_literal (pos, t) =
    (if pos then "" else "~ ") ^ string_for_atp_term t
fun string_for_problem_line (Cnf (ident, kind, lits)) =
  "cnf(" ^ ident ^ ", " ^
  (case kind of Axiom => "axiom" | Conjecture => "negated_conjecture") ^ ",\n" ^
  "    (" ^ space_implode " | " (map string_for_atp_literal lits) ^ ")).\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_atp_term (ATerm (name, ts)) =
  nice_name name ##>> pool_map nice_atp_term ts #>> ATerm
fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos
fun nice_problem_line (Cnf (ident, kind, lits)) =
  pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits))
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 atp_term_for_combtyp (CombTVar name) = ATerm (name, [])
  | atp_term_for_combtyp (CombTFree name) = ATerm (name, [])
  | atp_term_for_combtyp (CombType (name, tys)) =
    ATerm (name, map atp_term_for_combtyp tys)

fun atp_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 atp_term_for_combtyp ty_args @
                      map (atp_term_for_combterm full_types false) args)
  in
    if full_types then wrap_type (atp_term_for_combtyp (type_of_combterm u)) t
    else t
  end

fun atp_literal_for_literal full_types (FOLLiteral (pos, t)) =
  (pos, atp_term_for_combterm full_types true t)

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

fun atp_literals_for_axiom full_types
                           (FOLClause {literals, ctypes_sorts, ...}) =
  map (atp_literal_for_literal full_types) literals @
  map (atp_literal_for_type_literal false)
      (type_literals_for_types ctypes_sorts)

fun problem_line_for_axiom full_types
        (clause as FOLClause {axiom_name, clause_id, kind, ...}) =
  Cnf (hol_ident axiom_name clause_id, kind,
       atp_literals_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
    Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
                                      (true, ATerm (superclass, [ty_arg]))])
  end

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

fun problem_line_for_arity_clause
        (ArityClause {axiom_name, conclLit, premLits, ...}) =
  Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
       map atp_literal_for_arity_literal (conclLit :: premLits))

fun problem_line_for_conjecture full_types
        (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) =
  Cnf (hol_ident axiom_name clause_id, kind,
       map (atp_literal_for_literal full_types) literals)

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

fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [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_atp_variable s = Char.isUpper (String.sub (s, 0))

fun consider_term top_level (ATerm ((s, _), ts)) =
  (if is_atp_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_literal (_, t) = consider_term true t
fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits
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 repair_literal thy full_types const_tab (pos, t) =
  (pos, t |> repair_applications_in_term thy full_types const_tab
          |> repair_predicates_in_term const_tab)
fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) =
  Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits)
fun repair_problem_with_const_table thy full_types const_tab problem =
  map (apsnd (map (repair_problem_line thy full_types const_tab))) problem
fun repair_problem thy full_types explicit_apply problem =
  repair_problem_with_const_table thy 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 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 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;