(*  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 classrel_clause = Metis_Clauses.classrel_clause

  type arity_clause = Metis_Clauses.arity_clause

  type hol_clause = Metis_Clauses.hol_clause

  type name_pool = string Symtab.table * string Symtab.table

  val type_wrapper_name : string

  val write_tptp_file :

    theory -> bool -> bool -> bool -> Path.T

    -> hol_clause list * hol_clause list * hol_clause list * hol_clause list

       * classrel_clause list * arity_clause list

    -> name_pool option * 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 **)

type name_pool = string Symtab.table * string Symtab.table

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))

val nice_problem =

  pool_map (fn (heading, lines) =>

               pool_map nice_problem_line lines #>> pair heading)

(** 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 (TyVar name) = ATerm (name, [])

  | atp_term_for_combtyp (TyFree name) = ATerm (name, [])

  | atp_term_for_combtyp (TyConstr (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 (Literal (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

        (HOLClause {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 HOLClause {axiom_name, clause_id, kind, ...}) =

  Cnf (hol_ident axiom_name clause_id, kind,

       atp_literals_for_axiom full_types clause)

fun problem_line_for_classrel

        (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 (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 HOLClause {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 (HOLClause {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

val consider_problem = fold (fold consider_problem_line o snd)

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)

val repair_problem_with_const_table = map o apsnd o map ooo repair_problem_line

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,

                     classrel_clauses, arity_clauses) =

  let

    val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses

    val classrel_lines = map problem_line_for_classrel classrel_clauses

    val arity_lines = map problem_line_for_arity 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", classrel_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 classrel_lines + length arity_lines

      + length helper_lines

    val _ = File.write_list file (strings_for_problem problem)

  in (pool, conjecture_offset) end

end;