src/HOL/Tools/ATP/atp_translate.ML

don't stumble on Skolem names

(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
    Author:     Fabian Immler, TU Muenchen
    Author:     Makarius
    Author:     Jasmin Blanchette, TU Muenchen

Translation of HOL to FOL for Sledgehammer.
*)

signature ATP_TRANSLATE =
sig
  type 'a fo_term = 'a ATP_Problem.fo_term
  type connective = ATP_Problem.connective
  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
  type format = ATP_Problem.format
  type formula_kind = ATP_Problem.formula_kind
  type 'a problem = 'a ATP_Problem.problem

  type name = string * string

  datatype type_literal =
    TyLitVar of name * name |
    TyLitFree of name * name

  datatype arity_literal =
    TConsLit of name * name * name list |
    TVarLit of name * name

  type arity_clause =
    {name: string,
     prem_lits: arity_literal list,
     concl_lits: arity_literal}

  type class_rel_clause =
    {name: string,
     subclass: name,
     superclass: name}

  datatype combterm =
    CombConst of name * typ * typ list |
    CombVar of name * typ |
    CombApp of combterm * combterm

  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained

  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
  datatype type_level =
    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
  datatype type_heaviness = Heavyweight | Lightweight

  datatype type_sys =
    Simple_Types of type_level |
    Preds of polymorphism * type_level * type_heaviness |
    Tags of polymorphism * type_level * type_heaviness

  type translated_formula

  val bound_var_prefix : string
  val schematic_var_prefix: string
  val fixed_var_prefix: string
  val tvar_prefix: string
  val tfree_prefix: string
  val const_prefix: string
  val type_const_prefix: string
  val class_prefix: string
  val skolem_const_prefix : string
  val old_skolem_const_prefix : string
  val new_skolem_const_prefix : string
  val type_decl_prefix : string
  val sym_decl_prefix : string
  val preds_sym_formula_prefix : string
  val lightweight_tags_sym_formula_prefix : string
  val fact_prefix : string
  val conjecture_prefix : string
  val helper_prefix : string
  val class_rel_clause_prefix : string
  val arity_clause_prefix : string
  val tfree_clause_prefix : string
  val typed_helper_suffix : string
  val untyped_helper_suffix : string
  val type_tag_idempotence_helper_name : string
  val predicator_name : string
  val app_op_name : string
  val type_tag_name : string
  val type_pred_name : string
  val simple_type_prefix : string
  val prefixed_predicator_name : string
  val prefixed_app_op_name : string
  val prefixed_type_tag_name : string
  val ascii_of: string -> string
  val unascii_of: string -> string
  val strip_prefix_and_unascii : string -> string -> string option
  val proxy_table : (string * (string * (thm * (string * string)))) list
  val proxify_const : string -> (string * string) option
  val invert_const: string -> string
  val unproxify_const: string -> string
  val make_bound_var : string -> string
  val make_schematic_var : string * int -> string
  val make_fixed_var : string -> string
  val make_schematic_type_var : string * int -> string
  val make_fixed_type_var : string -> string
  val make_fixed_const : string -> string
  val make_fixed_type_const : string -> string
  val make_type_class : string -> string
  val new_skolem_var_name_from_const : string -> string
  val num_type_args : theory -> string -> int
  val make_arity_clauses :
    theory -> string list -> class list -> class list * arity_clause list
  val make_class_rel_clauses :
    theory -> class list -> class list -> class_rel_clause list
  val combtyp_of : combterm -> typ
  val strip_combterm_comb : combterm -> combterm * combterm list
  val atyps_of : typ -> typ list
  val combterm_from_term :
    theory -> (string * typ) list -> term -> combterm * typ list
  val is_locality_global : locality -> bool
  val type_sys_from_string : string -> type_sys
  val polymorphism_of_type_sys : type_sys -> polymorphism
  val level_of_type_sys : type_sys -> type_level
  val is_type_sys_virtually_sound : type_sys -> bool
  val is_type_sys_fairly_sound : type_sys -> bool
  val choose_format : format list -> type_sys -> format * type_sys
  val raw_type_literals_for_types : typ list -> type_literal list
  val mk_aconns :
    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
  val unmangled_const_name : string -> string
  val unmangled_const : string -> string * string fo_term list
  val translate_atp_fact :
    Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
    -> translated_formula option * ((string * locality) * thm)
  val helper_table : (string * (bool * thm list)) list
  val should_specialize_helper : type_sys -> term -> bool
  val tfree_classes_of_terms : term list -> string list
  val tvar_classes_of_terms : term list -> string list
  val type_consts_of_terms : theory -> term list -> string list
  val prepare_atp_problem :
    Proof.context -> format -> formula_kind -> formula_kind -> type_sys
    -> bool option -> bool -> bool -> term list -> term
    -> (translated_formula option * ((string * 'a) * thm)) list
    -> string problem * string Symtab.table * int * int
       * (string * 'a) list vector * int list * int Symtab.table
  val atp_problem_weights : string problem -> (string * real) list
end;

structure ATP_Translate : ATP_TRANSLATE =
struct

open ATP_Util
open ATP_Problem

type name = string * string

(* FIXME: avoid *)
fun union_all xss = fold (union (op =)) xss []

(* experimental *)
val generate_useful_info = false

fun useful_isabelle_info s =
  if generate_useful_info then
    SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
  else
    NONE

val intro_info = useful_isabelle_info "intro"
val elim_info = useful_isabelle_info "elim"
val simp_info = useful_isabelle_info "simp"

val bound_var_prefix = "B_"
val schematic_var_prefix = "V_"
val fixed_var_prefix = "v_"

val tvar_prefix = "T_"
val tfree_prefix = "t_"

val const_prefix = "c_"
val type_const_prefix = "tc_"
val class_prefix = "cl_"

val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
val new_skolem_const_prefix = skolem_const_prefix ^ "n"

val type_decl_prefix = "ty_"
val sym_decl_prefix = "sy_"
val preds_sym_formula_prefix = "psy_"
val lightweight_tags_sym_formula_prefix = "tsy_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
val class_rel_clause_prefix = "clar_"
val arity_clause_prefix = "arity_"
val tfree_clause_prefix = "tfree_"

val typed_helper_suffix = "_T"
val untyped_helper_suffix = "_U"
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"

val predicator_name = "hBOOL"
val app_op_name = "hAPP"
val type_tag_name = "ti"
val type_pred_name = "is"
val simple_type_prefix = "ty_"

val prefixed_predicator_name = const_prefix ^ predicator_name
val prefixed_app_op_name = const_prefix ^ app_op_name
val prefixed_type_tag_name = const_prefix ^ type_tag_name

(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"

(*Escaping of special characters.
  Alphanumeric characters are left unchanged.
  The character _ goes to __
  Characters in the range ASCII space to / go to _A to _P, respectively.
  Other characters go to _nnn where nnn is the decimal ASCII code.*)
val upper_a_minus_space = Char.ord #"A" - Char.ord #" "

fun stringN_of_int 0 _ = ""
  | stringN_of_int k n =
    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)

fun ascii_of_char c =
  if Char.isAlphaNum c then
    String.str c
  else if c = #"_" then
    "__"
  else if #" " <= c andalso c <= #"/" then
    "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
  else
    (* fixed width, in case more digits follow *)
    "_" ^ stringN_of_int 3 (Char.ord c)

val ascii_of = String.translate ascii_of_char

(** Remove ASCII armoring from names in proof files **)

(* We don't raise error exceptions because this code can run inside a worker
   thread. Also, the errors are impossible. *)
val unascii_of =
  let
    fun un rcs [] = String.implode(rev rcs)
      | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
        (* Three types of _ escapes: __, _A to _P, _nnn *)
      | un rcs (#"_" :: #"_" :: cs) = un (#"_"::rcs) cs
      | un rcs (#"_" :: c :: cs) =
        if #"A" <= c andalso c<= #"P" then
          (* translation of #" " to #"/" *)
          un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
        else
          let val digits = List.take (c::cs, 3) handle Subscript => [] in
            case Int.fromString (String.implode digits) of
              SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
            | NONE => un (c:: #"_"::rcs) cs (* ERROR *)
          end
      | un rcs (c :: cs) = un (c :: rcs) cs
  in un [] o String.explode end

(* If string s has the prefix s1, return the result of deleting it,
   un-ASCII'd. *)
fun strip_prefix_and_unascii s1 s =
  if String.isPrefix s1 s then
    SOME (unascii_of (String.extract (s, size s1, NONE)))
  else
    NONE

val proxy_table =
  [("c_False", (@{const_name False}, (@{thm fFalse_def},
       ("fFalse", @{const_name ATP.fFalse})))),
   ("c_True", (@{const_name True}, (@{thm fTrue_def},
       ("fTrue", @{const_name ATP.fTrue})))),
   ("c_Not", (@{const_name Not}, (@{thm fNot_def},
       ("fNot", @{const_name ATP.fNot})))),
   ("c_conj", (@{const_name conj}, (@{thm fconj_def},
       ("fconj", @{const_name ATP.fconj})))),
   ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
       ("fdisj", @{const_name ATP.fdisj})))),
   ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
       ("fimplies", @{const_name ATP.fimplies})))),
   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
       ("fequal", @{const_name ATP.fequal}))))]

val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)

(* Readable names for the more common symbolic functions. Do not mess with the
   table unless you know what you are doing. *)
val const_trans_table =
  [(@{type_name Product_Type.prod}, "prod"),
   (@{type_name Sum_Type.sum}, "sum"),
   (@{const_name False}, "False"),
   (@{const_name True}, "True"),
   (@{const_name Not}, "Not"),
   (@{const_name conj}, "conj"),
   (@{const_name disj}, "disj"),
   (@{const_name implies}, "implies"),
   (@{const_name HOL.eq}, "equal"),
   (@{const_name If}, "If"),
   (@{const_name Set.member}, "member"),
   (@{const_name Meson.COMBI}, "COMBI"),
   (@{const_name Meson.COMBK}, "COMBK"),
   (@{const_name Meson.COMBB}, "COMBB"),
   (@{const_name Meson.COMBC}, "COMBC"),
   (@{const_name Meson.COMBS}, "COMBS")]
  |> Symtab.make
  |> fold (Symtab.update o swap o snd o snd o snd) proxy_table

(* Invert the table of translations between Isabelle and ATPs. *)
val const_trans_table_inv =
  const_trans_table |> Symtab.dest |> map swap |> Symtab.make
val const_trans_table_unprox =
  Symtab.empty
  |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table

val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)

fun lookup_const c =
  case Symtab.lookup const_trans_table c of
    SOME c' => c'
  | NONE => ascii_of c

(*Remove the initial ' character from a type variable, if it is present*)
fun trim_type_var s =
  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
  else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)

fun ascii_of_indexname (v,0) = ascii_of v
  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i

fun make_bound_var x = bound_var_prefix ^ ascii_of x
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x

fun make_schematic_type_var (x,i) =
      tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i))
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))

(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
fun make_fixed_const @{const_name HOL.eq} = "equal"
  | make_fixed_const c = const_prefix ^ lookup_const c

fun make_fixed_type_const c = type_const_prefix ^ lookup_const c

fun make_type_class clas = class_prefix ^ ascii_of clas

fun new_skolem_var_name_from_const s =
  let val ss = s |> space_explode Long_Name.separator in
    nth ss (length ss - 2)
  end

(* The number of type arguments of a constant, zero if it's monomorphic. For
   (instances of) Skolem pseudoconstants, this information is encoded in the
   constant name. *)
fun num_type_args thy s =
  if String.isPrefix skolem_const_prefix s then
    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
  else
    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length

(** Definitions and functions for FOL clauses and formulas for TPTP **)

(* The first component is the type class; the second is a "TVar" or "TFree". *)
datatype type_literal =
  TyLitVar of name * name |
  TyLitFree of name * name


(** Isabelle arities **)

datatype arity_literal =
  TConsLit of name * name * name list |
  TVarLit of name * name

fun gen_TVars 0 = []
  | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)

fun pack_sort (_,[])  = []
  | pack_sort (tvar, "HOL.type" :: srt) =
    pack_sort (tvar, srt) (* IGNORE sort "type" *)
  | pack_sort (tvar, cls :: srt) =
    (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt)

type arity_clause =
  {name: string,
   prem_lits: arity_literal list,
   concl_lits: arity_literal}

(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
fun make_axiom_arity_clause (tcons, name, (cls, args)) =
  let
    val tvars = gen_TVars (length args)
    val tvars_srts = ListPair.zip (tvars, args)
  in
    {name = name,
     prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)),
     concl_lits = TConsLit (`make_type_class cls,
                            `make_fixed_type_const tcons,
                            tvars ~~ tvars)}
  end

fun arity_clause _ _ (_, []) = []
  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
      arity_clause seen n (tcons,ars)
  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) ::
          arity_clause seen (n+1) (tcons,ars)
      else
          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
          arity_clause (class::seen) n (tcons,ars)

fun multi_arity_clause [] = []
  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists

(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
  provided its arguments have the corresponding sorts.*)
fun type_class_pairs thy tycons classes =
  let
    val alg = Sign.classes_of thy
    fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
    fun add_class tycon class =
      cons (class, domain_sorts tycon class)
      handle Sorts.CLASS_ERROR _ => I
    fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
  in map try_classes tycons end

(*Proving one (tycon, class) membership may require proving others, so iterate.*)
fun iter_type_class_pairs _ _ [] = ([], [])
  | iter_type_class_pairs thy tycons classes =
      let val cpairs = type_class_pairs thy tycons classes
          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end

fun make_arity_clauses thy tycons =
  iter_type_class_pairs thy tycons ##> multi_arity_clause


(** Isabelle class relations **)

type class_rel_clause =
  {name: string,
   subclass: name,
   superclass: name}

(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
fun class_pairs _ [] _ = []
  | class_pairs thy subs supers =
      let
        val class_less = Sorts.class_less (Sign.classes_of thy)
        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
        fun add_supers sub = fold (add_super sub) supers
      in fold add_supers subs [] end

fun make_class_rel_clause (sub,super) =
  {name = sub ^ "_" ^ super,
   subclass = `make_type_class sub,
   superclass = `make_type_class super}

fun make_class_rel_clauses thy subs supers =
  map make_class_rel_clause (class_pairs thy subs supers)

datatype combterm =
  CombConst of name * typ * typ list |
  CombVar of name * typ |
  CombApp of combterm * combterm

fun combtyp_of (CombConst (_, T, _)) = T
  | combtyp_of (CombVar (_, T)) = T
  | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))

(*gets the head of a combinator application, along with the list of arguments*)
fun strip_combterm_comb u =
    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
        |   stripc  x =  x
    in stripc(u,[]) end

fun atyps_of T = fold_atyps (insert (op =)) T []

fun new_skolem_const_name s num_T_args =
  [new_skolem_const_prefix, s, string_of_int num_T_args]
  |> space_implode Long_Name.separator

(* Converts a term (with combinators) into a combterm. Also accumulates sort
   infomation. *)
fun combterm_from_term thy bs (P $ Q) =
    let
      val (P', P_atomics_Ts) = combterm_from_term thy bs P
      val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
    in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
  | combterm_from_term thy _ (Const (c, T)) =
    let
      val tvar_list =
        (if String.isPrefix old_skolem_const_prefix c then
           [] |> Term.add_tvarsT T |> map TVar
         else
           (c, T) |> Sign.const_typargs thy)
      val c' = CombConst (`make_fixed_const c, T, tvar_list)
    in (c', atyps_of T) end
  | combterm_from_term _ _ (Free (v, T)) =
    (CombConst (`make_fixed_var v, T, []), atyps_of T)
  | combterm_from_term _ _ (Var (v as (s, _), T)) =
    (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
       let
         val Ts = T |> strip_type |> swap |> op ::
         val s' = new_skolem_const_name s (length Ts)
       in CombConst (`make_fixed_const s', T, Ts) end
     else
       CombVar ((make_schematic_var v, s), T), atyps_of T)
  | combterm_from_term _ bs (Bound j) =
    nth bs j
    |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"

datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained

(* (quasi-)underapproximation of the truth *)
fun is_locality_global Local = false
  | is_locality_global Assum = false
  | is_locality_global Chained = false
  | is_locality_global _ = true

datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
datatype type_level =
  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
datatype type_heaviness = Heavyweight | Lightweight

datatype type_sys =
  Simple_Types of type_level |
  Preds of polymorphism * type_level * type_heaviness |
  Tags of polymorphism * type_level * type_heaviness

fun try_unsuffixes ss s =
  fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE

fun type_sys_from_string s =
  (case try (unprefix "poly_") s of
     SOME s => (SOME Polymorphic, s)
   | NONE =>
     case try (unprefix "mono_") s of
       SOME s => (SOME Monomorphic, s)
     | NONE =>
       case try (unprefix "mangled_") s of
         SOME s => (SOME Mangled_Monomorphic, s)
       | NONE => (NONE, s))
  ||> (fn s =>
          (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
          case try_unsuffixes ["?", "_query"] s of
            SOME s => (Nonmonotonic_Types, s)
          | NONE =>
            case try_unsuffixes ["!", "_bang"] s of
              SOME s => (Finite_Types, s)
            | NONE => (All_Types, s))
  ||> apsnd (fn s =>
                case try (unsuffix "_heavy") s of
                  SOME s => (Heavyweight, s)
                | NONE => (Lightweight, s))
  |> (fn (poly, (level, (heaviness, core))) =>
         case (core, (poly, level, heaviness)) of
           ("simple", (NONE, _, Lightweight)) => Simple_Types level
         | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
         | ("tags", (SOME Polymorphic, All_Types, _)) =>
           Tags (Polymorphic, All_Types, heaviness)
         | ("tags", (SOME Polymorphic, _, _)) =>
           (* The actual light encoding is very unsound. *)
           Tags (Polymorphic, level, Heavyweight)
         | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
         | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
           Preds (poly, Const_Arg_Types, Lightweight)
         | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
           Preds (Polymorphic, No_Types, Lightweight)
         | _ => raise Same.SAME)
  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")

fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
  | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
  | polymorphism_of_type_sys (Tags (poly, _, _)) = poly

fun level_of_type_sys (Simple_Types level) = level
  | level_of_type_sys (Preds (_, level, _)) = level
  | level_of_type_sys (Tags (_, level, _)) = level

fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
  | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
  | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness

fun is_type_level_virtually_sound level =
  level = All_Types orelse level = Nonmonotonic_Types
val is_type_sys_virtually_sound =
  is_type_level_virtually_sound o level_of_type_sys

fun is_type_level_fairly_sound level =
  is_type_level_virtually_sound level orelse level = Finite_Types
val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys

fun is_setting_higher_order THF (Simple_Types _) = true
  | is_setting_higher_order _ _ = false

fun choose_format formats (Simple_Types level) =
    if member (op =) formats THF then (THF, Simple_Types level)
    else if member (op =) formats TFF then (TFF, Simple_Types level)
    else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
  | choose_format formats type_sys =
    (case hd formats of
       CNF_UEQ =>
       (CNF_UEQ, case type_sys of
                   Preds stuff =>
                   (if is_type_sys_fairly_sound type_sys then Preds else Tags)
                       stuff
                 | _ => type_sys)
     | format => (format, type_sys))

type translated_formula =
  {name: string,
   locality: locality,
   kind: formula_kind,
   combformula: (name, typ, combterm) formula,
   atomic_types: typ list}

fun update_combformula f ({name, locality, kind, combformula, atomic_types}
                          : translated_formula) =
  {name = name, locality = locality, kind = kind, combformula = f combformula,
   atomic_types = atomic_types} : translated_formula

fun fact_lift f ({combformula, ...} : translated_formula) = f combformula

val type_instance = Sign.typ_instance o Proof_Context.theory_of

fun insert_type ctxt get_T x xs =
  let val T = get_T x in
    if exists (curry (type_instance ctxt) T o get_T) xs then xs
    else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
  end

(* The Booleans indicate whether all type arguments should be kept. *)
datatype type_arg_policy =
  Explicit_Type_Args of bool |
  Mangled_Type_Args of bool |
  No_Type_Args

fun should_drop_arg_type_args (Simple_Types _) =
    false (* since TFF doesn't support overloading *)
  | should_drop_arg_type_args type_sys =
    level_of_type_sys type_sys = All_Types andalso
    heaviness_of_type_sys type_sys = Heavyweight

fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
  | general_type_arg_policy type_sys =
    if level_of_type_sys type_sys = No_Types then
      No_Type_Args
    else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
      Mangled_Type_Args (should_drop_arg_type_args type_sys)
    else
      Explicit_Type_Args (should_drop_arg_type_args type_sys)

fun type_arg_policy type_sys s =
  if s = @{const_name HOL.eq} orelse
     (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
    No_Type_Args
  else if s = type_tag_name then
    Explicit_Type_Args false
  else
    general_type_arg_policy type_sys

(*Make literals for sorted type variables*)
fun generic_sorts_on_type (_, []) = []
  | generic_sorts_on_type ((x, i), s :: ss) =
    generic_sorts_on_type ((x, i), ss)
    |> (if s = the_single @{sort HOL.type} then
          I
        else if i = ~1 then
          cons (TyLitFree (`make_type_class s, `make_fixed_type_var x))
        else
          cons (TyLitVar (`make_type_class s,
                          (make_schematic_type_var (x, i), x))))
fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S)
  | sorts_on_tfree _ = []
fun sorts_on_tvar (TVar z) = generic_sorts_on_type z
  | sorts_on_tvar _ = []

(* Given a list of sorted type variables, return a list of type literals. *)
fun raw_type_literals_for_types Ts =
  union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)

fun type_literals_for_types type_sys sorts_on_typ Ts =
  if level_of_type_sys type_sys = No_Types then []
  else union_all (map sorts_on_typ Ts)

fun mk_aconns c phis =
  let val (phis', phi') = split_last phis in
    fold_rev (mk_aconn c) phis' phi'
  end
fun mk_ahorn [] phi = phi
  | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
fun mk_aquant _ [] phi = phi
  | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
    if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
  | mk_aquant q xs phi = AQuant (q, xs, phi)

fun close_universally atom_vars phi =
  let
    fun formula_vars bounds (AQuant (_, xs, phi)) =
        formula_vars (map fst xs @ bounds) phi
      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
      | formula_vars bounds (AAtom tm) =
        union (op =) (atom_vars tm []
                      |> filter_out (member (op =) bounds o fst))
  in mk_aquant AForall (formula_vars [] phi []) phi end

fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
  | combterm_vars (CombConst _) = I
  | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
fun close_combformula_universally phi = close_universally combterm_vars phi

fun term_vars (ATerm (name as (s, _), tms)) =
  is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
fun close_formula_universally phi = close_universally term_vars phi

val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
val homo_infinite_type = Type (homo_infinite_type_name, [])

fun fo_term_from_typ format type_sys =
  let
    fun term (Type (s, Ts)) =
      ATerm (case (is_setting_higher_order format type_sys, s) of
               (true, @{type_name bool}) => `I tptp_bool_type
             | (true, @{type_name fun}) => `I tptp_fun_type
             | _ => if s = homo_infinite_type_name andalso
                       (format = TFF orelse format = THF) then
                      `I tptp_individual_type
                    else
                      `make_fixed_type_const s,
             map term Ts)
    | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
    | term (TVar ((x as (s, _)), _)) =
      ATerm ((make_schematic_type_var x, s), [])
  in term end

(* This shouldn't clash with anything else. *)
val mangled_type_sep = "\000"

fun generic_mangled_type_name f (ATerm (name, [])) = f name
  | generic_mangled_type_name f (ATerm (name, tys)) =
    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
    ^ ")"

val bool_atype = AType (`I tptp_bool_type)

fun make_simple_type s =
  if s = tptp_bool_type orelse s = tptp_fun_type orelse
     s = tptp_individual_type then
    s
  else
    simple_type_prefix ^ ascii_of s

fun ho_type_from_fo_term format type_sys pred_sym ary =
  let
    fun to_atype ty =
      AType ((make_simple_type (generic_mangled_type_name fst ty),
              generic_mangled_type_name snd ty))
    fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
    fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
      | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
    fun to_ho (ty as ATerm ((s, _), tys)) =
      if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
  in if is_setting_higher_order format type_sys then to_ho else to_fo ary end

fun mangled_type format type_sys pred_sym ary =
  ho_type_from_fo_term format type_sys pred_sym ary
  o fo_term_from_typ format type_sys

fun mangled_const_name format type_sys T_args (s, s') =
  let
    val ty_args = map (fo_term_from_typ format type_sys) T_args
    fun type_suffix f g =
      fold_rev (curry (op ^) o g o prefix mangled_type_sep
                o generic_mangled_type_name f) ty_args ""
  in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end

val parse_mangled_ident =
  Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode

fun parse_mangled_type x =
  (parse_mangled_ident
   -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
                    [] >> ATerm) x
and parse_mangled_types x =
  (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x

fun unmangled_type s =
  s |> suffix ")" |> raw_explode
    |> Scan.finite Symbol.stopper
           (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
                                                quote s)) parse_mangled_type))
    |> fst

val unmangled_const_name = space_explode mangled_type_sep #> hd
fun unmangled_const s =
  let val ss = space_explode mangled_type_sep s in
    (hd ss, map unmangled_type (tl ss))
  end

fun introduce_proxies format type_sys =
  let
    fun intro top_level (CombApp (tm1, tm2)) =
        CombApp (intro top_level tm1, intro false tm2)
      | intro top_level (CombConst (name as (s, _), T, T_args)) =
        (case proxify_const s of
           SOME proxy_base =>
           if top_level orelse is_setting_higher_order format type_sys then
             case (top_level, s) of
               (_, "c_False") => (`I tptp_false, [])
             | (_, "c_True") => (`I tptp_true, [])
             | (false, "c_Not") => (`I tptp_not, [])
             | (false, "c_conj") => (`I tptp_and, [])
             | (false, "c_disj") => (`I tptp_or, [])
             | (false, "c_implies") => (`I tptp_implies, [])
             | (false, s) =>
               if is_tptp_equal s then (`I tptp_equal, [])
               else (proxy_base |>> prefix const_prefix, T_args)
             | _ => (name, [])
           else
             (proxy_base |>> prefix const_prefix, T_args)
          | NONE => (name, T_args))
        |> (fn (name, T_args) => CombConst (name, T, T_args))
      | intro _ tm = tm
  in intro true end

fun combformula_from_prop thy format type_sys eq_as_iff =
  let
    fun do_term bs t atomic_types =
      combterm_from_term thy bs (Envir.eta_contract t)
      |>> (introduce_proxies format type_sys #> AAtom)
      ||> union (op =) atomic_types
    fun do_quant bs q s T t' =
      let val s = Name.variant (map fst bs) s in
        do_formula ((s, T) :: bs) t'
        #>> mk_aquant q [(`make_bound_var s, SOME T)]
      end
    and do_conn bs c t1 t2 =
      do_formula bs t1 ##>> do_formula bs t2
      #>> uncurry (mk_aconn c)
    and do_formula bs t =
      case t of
        @{const Trueprop} $ t1 => do_formula bs t1
      | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
        do_quant bs AForall s T t'
      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
        do_quant bs AExists s T t'
      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
        if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
      | _ => do_term bs t
  in do_formula [] end

fun presimplify_term ctxt =
  Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
  #> Meson.presimplify ctxt
  #> prop_of

fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
fun conceal_bounds Ts t =
  subst_bounds (map (Free o apfst concealed_bound_name)
                    (0 upto length Ts - 1 ~~ Ts), t)
fun reveal_bounds Ts =
  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
                    (0 upto length Ts - 1 ~~ Ts))

fun extensionalize_term ctxt t =
  let val thy = Proof_Context.theory_of ctxt in
    t |> cterm_of thy |> Meson.extensionalize_conv ctxt
      |> prop_of |> Logic.dest_equals |> snd
  end

fun introduce_combinators_in_term ctxt kind t =
  let val thy = Proof_Context.theory_of ctxt in
    if Meson.is_fol_term thy t then
      t
    else
      let
        fun aux Ts t =
          case t of
            @{const Not} $ t1 => @{const Not} $ aux Ts t1
          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
            t0 $ Abs (s, T, aux (T :: Ts) t')
          | (t0 as Const (@{const_name All}, _)) $ t1 =>
            aux Ts (t0 $ eta_expand Ts t1 1)
          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
            t0 $ Abs (s, T, aux (T :: Ts) t')
          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
            aux Ts (t0 $ eta_expand Ts t1 1)
          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
              $ t1 $ t2 =>
            t0 $ aux Ts t1 $ aux Ts t2
          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
                   t
                 else
                   t |> conceal_bounds Ts
                     |> Envir.eta_contract
                     |> cterm_of thy
                     |> Meson_Clausify.introduce_combinators_in_cterm
                     |> prop_of |> Logic.dest_equals |> snd
                     |> reveal_bounds Ts
        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
      handle THM _ =>
             (* A type variable of sort "{}" will make abstraction fail. *)
             if kind = Conjecture then HOLogic.false_const
             else HOLogic.true_const
  end

(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
fun freeze_term t =
  let
    fun aux (t $ u) = aux t $ aux u
      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
      | aux (Var ((s, i), T)) =
        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
      | aux t = t
  in t |> exists_subterm is_Var t ? aux end

fun preprocess_prop ctxt presimp kind t =
  let
    val thy = Proof_Context.theory_of ctxt
    val t = t |> Envir.beta_eta_contract
              |> transform_elim_prop
              |> Object_Logic.atomize_term thy
    val need_trueprop = (fastype_of t = @{typ bool})
  in
    t |> need_trueprop ? HOLogic.mk_Trueprop
      |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
      |> extensionalize_term ctxt
      |> presimp ? presimplify_term ctxt
      |> perhaps (try (HOLogic.dest_Trueprop))
      |> introduce_combinators_in_term ctxt kind
  end

(* making fact and conjecture formulas *)
fun make_formula thy format type_sys eq_as_iff name loc kind t =
  let
    val (combformula, atomic_types) =
      combformula_from_prop thy format type_sys eq_as_iff t []
  in
    {name = name, locality = loc, kind = kind, combformula = combformula,
     atomic_types = atomic_types}
  end

fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp
              ((name, loc), t) =
  let val thy = Proof_Context.theory_of ctxt in
    case (keep_trivial,
          t |> preproc ? preprocess_prop ctxt presimp Axiom
            |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
      (false,
       formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
      if s = tptp_true then NONE else SOME formula
    | (_, formula) => SOME formula
  end

fun make_conjecture ctxt format prem_kind type_sys preproc ts =
  let
    val thy = Proof_Context.theory_of ctxt
    val last = length ts - 1
  in
    map2 (fn j => fn t =>
             let
               val (kind, maybe_negate) =
                 if j = last then
                   (Conjecture, I)
                 else
                   (prem_kind,
                    if prem_kind = Conjecture then update_combformula mk_anot
                    else I)
              in
                t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
                  |> make_formula thy format type_sys true (string_of_int j)
                                  General kind
                  |> maybe_negate
              end)
         (0 upto last) ts
  end

(** Finite and infinite type inference **)

fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
  | deep_freeze_atyp T = T
val deep_freeze_type = map_atyps deep_freeze_atyp

(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
   dangerous because their "exhaust" properties can easily lead to unsound ATP
   proofs. On the other hand, all HOL infinite types can be given the same
   models in first-order logic (via Löwenheim-Skolem). *)

fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
    exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
  | should_encode_type _ _ All_Types _ = true
  | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
  | should_encode_type _ _ _ _ = false

fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
                             should_predicate_on_var T =
    (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
    should_encode_type ctxt nonmono_Ts level T
  | should_predicate_on_type _ _ _ _ _ = false

fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
    String.isPrefix bound_var_prefix s
  | is_var_or_bound_var (CombVar _) = true
  | is_var_or_bound_var _ = false

datatype tag_site = Top_Level | Eq_Arg | Elsewhere

fun should_tag_with_type _ _ _ Top_Level _ _ = false
  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
    (case heaviness of
       Heavyweight => should_encode_type ctxt nonmono_Ts level T
     | Lightweight =>
       case (site, is_var_or_bound_var u) of
         (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
       | _ => false)
  | should_tag_with_type _ _ _ _ _ _ = false

fun homogenized_type ctxt nonmono_Ts level =
  let
    val should_encode = should_encode_type ctxt nonmono_Ts level
    fun homo 0 T = if should_encode T then T else homo_infinite_type
      | homo ary (Type (@{type_name fun}, [T1, T2])) =
        homo 0 T1 --> homo (ary - 1) T2
      | homo _ _ = raise Fail "expected function type"
  in homo end

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

type sym_info =
  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}

fun add_combterm_syms_to_table ctxt explicit_apply =
  let
    fun consider_var_arity const_T var_T max_ary =
      let
        fun iter ary T =
          if ary = max_ary orelse type_instance ctxt (var_T, T) then ary
          else iter (ary + 1) (range_type T)
      in iter 0 const_T end
    fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =
      let
        fun do_var_or_bound_var T =
          if explicit_apply = NONE andalso can dest_funT T then
            let
              fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
                {pred_sym = pred_sym,
                 min_ary =
                   fold (fn T' => consider_var_arity T' T) types min_ary,
                 max_ary = max_ary, types = types}
              val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T
            in
              if pointer_eq (ho_var_Ts', ho_var_Ts) then accum
              else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
            end
          else
            accum
        val (head, args) = strip_combterm_comb tm
      in
        (case head of
           CombConst ((s, _), T, _) =>
           if String.isPrefix bound_var_prefix s then
             do_var_or_bound_var T
           else
             let val ary = length args in
               (ho_var_Ts,
                case Symtab.lookup sym_tab s of
                  SOME {pred_sym, min_ary, max_ary, types} =>
                  let
                    val types' = types |> insert_type ctxt I T
                    val min_ary =
                      if is_some explicit_apply orelse
                         pointer_eq (types', types) then
                        min_ary
                      else
                        fold (consider_var_arity T) ho_var_Ts min_ary
                  in
                    Symtab.update (s, {pred_sym = pred_sym andalso top_level,
                                       min_ary = Int.min (ary, min_ary),
                                       max_ary = Int.max (ary, max_ary),
                                       types = types'})
                                  sym_tab
                  end
                | NONE =>
                  let
                    val min_ary =
                      case explicit_apply of
                        SOME true => 0
                      | SOME false => ary
                      | NONE => fold (consider_var_arity T) ho_var_Ts ary
                  in
                    Symtab.update_new (s, {pred_sym = top_level,
                                           min_ary = min_ary, max_ary = ary,
                                           types = [T]})
                                      sym_tab
                  end)
             end
         | CombVar (_, T) => do_var_or_bound_var T
         | _ => accum)
        |> fold (add false) args
      end
  in add true end
fun add_fact_syms_to_table ctxt explicit_apply =
  fact_lift (formula_fold NONE
                          (K (add_combterm_syms_to_table ctxt explicit_apply)))

val default_sym_tab_entries : (string * sym_info) list =
  (prefixed_predicator_name,
   {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
  ([tptp_false, tptp_true]
   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
  ([tptp_equal, tptp_old_equal]
   |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))

fun sym_table_for_facts ctxt explicit_apply facts =
  Symtab.empty
  |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
  |> fold Symtab.update default_sym_tab_entries

fun min_arity_of sym_tab s =
  case Symtab.lookup sym_tab s of
    SOME ({min_ary, ...} : sym_info) => min_ary
  | NONE =>
    case strip_prefix_and_unascii const_prefix s of
      SOME s =>
      let val s = s |> unmangled_const_name |> invert_const in
        if s = predicator_name then 1
        else if s = app_op_name then 2
        else if s = type_pred_name then 1
        else 0
      end