(*  Title:      HOL/Tools/ATP/atp_problem_generate.ML

    Author:     Fabian Immler, TU Muenchen

    Author:     Makarius

    Author:     Jasmin Blanchette, TU Muenchen

Translation of HOL to FOL for Metis and Sledgehammer.

*)

signature ATP_PROBLEM_GENERATE =

sig

  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term

  type connective = ATP_Problem.connective

  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula

  type atp_format = ATP_Problem.atp_format

  type formula_role = ATP_Problem.formula_role

  type 'a problem = 'a ATP_Problem.problem

  datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter

  datatype scope = Global | Local | Assum | Chained

  datatype status =

    General | Induction | Intro | Inductive | Elim | Simp | Def

  type stature = scope * status

  datatype strictness = Strict | Non_Strict

  datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars

  datatype type_level =

    All_Types |

    Nonmono_Types of strictness * granularity |

    Const_Types of bool (* "?" *) |

    No_Types

  type type_enc

  val no_lamsN : string

  val hide_lamsN : string

  val liftingN : string

  val combsN : string

  val combs_and_liftingN : string

  val combs_or_liftingN : string

  val lam_liftingN : string

  val keep_lamsN : 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 lam_lifted_prefix : string

  val lam_lifted_mono_prefix : string

  val lam_lifted_poly_prefix : string

  val skolem_const_prefix : string

  val old_skolem_const_prefix : string

  val new_skolem_const_prefix : string

  val combinator_prefix : string

  val type_decl_prefix : string

  val sym_decl_prefix : string

  val guards_sym_formula_prefix : string

  val 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 lam_fact_prefix : string

  val typed_helper_suffix : string

  val untyped_helper_suffix : string

  val predicator_name : string

  val app_op_name : string

  val type_guard_name : string

  val type_tag_name : string

  val native_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 unprefix_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 new_skolem_var_name_from_const : string -> string

  val atp_irrelevant_consts : string list

  val atp_schematic_consts_of : term -> typ list Symtab.table

  val is_type_enc_higher_order : type_enc -> bool

  val is_type_enc_polymorphic : type_enc -> bool

  val level_of_type_enc : type_enc -> type_level

  val is_type_enc_sound : type_enc -> bool

  val type_enc_from_string : strictness -> string -> type_enc

  val adjust_type_enc : atp_format -> type_enc -> type_enc

  val mk_aconns :

    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula

  val unmangled_const : string -> string * (string, 'b) ho_term list

  val unmangled_const_name : string -> string list

  val helper_table : ((string * bool) * (status * thm) list) list

  val trans_lams_from_string :

    Proof.context -> type_enc -> string -> term list -> term list * term list

  val factsN : string

  val prepare_atp_problem :

    Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string

    -> bool -> bool -> bool -> term list -> term

    -> ((string * stature) * term) list

    -> string problem * string Symtab.table * (string * stature) list vector

       * (string * term) list * int Symtab.table

  val atp_problem_selection_weights : string problem -> (string * real) list

  val atp_problem_term_order_info : string problem -> (string * int) list

end;

structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =

struct

open ATP_Util

open ATP_Problem

type name = string * string

datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter

datatype scope = Global | Local | Assum | Chained

datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def

type stature = scope * status

datatype order =

  First_Order |

  Higher_Order of thf_choice

datatype phantom_policy = Without_Phantom_Type_Vars | With_Phantom_Type_Vars

datatype polymorphism =

  Type_Class_Polymorphic |

  Raw_Polymorphic of phantom_policy |

  Raw_Monomorphic |

  Mangled_Monomorphic

datatype strictness = Strict | Non_Strict

datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars

datatype type_level =

  All_Types |

  Nonmono_Types of strictness * granularity |

  Const_Types of bool |

  No_Types

datatype type_enc =

  Native of order * polymorphism * type_level |

  Guards of polymorphism * type_level |

  Tags of polymorphism * type_level

fun is_type_enc_native (Native _) = true

  | is_type_enc_native _ = false

fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true

  | is_type_enc_higher_order _ = false

fun polymorphism_of_type_enc (Native (_, poly, _)) = poly

  | polymorphism_of_type_enc (Guards (poly, _)) = poly

  | polymorphism_of_type_enc (Tags (poly, _)) = poly

fun is_type_enc_polymorphic type_enc =

  case polymorphism_of_type_enc type_enc of

    Raw_Polymorphic _ => true

  | Type_Class_Polymorphic => true

  | _ => false

fun level_of_type_enc (Native (_, _, level)) = level

  | level_of_type_enc (Guards (_, level)) = level

  | level_of_type_enc (Tags (_, level)) = level

fun granularity_of_type_level (Nonmono_Types (_, grain)) = grain

  | granularity_of_type_level _ = All_Vars

fun is_type_level_sound All_Types = true

  | is_type_level_sound (Nonmono_Types _) = true

  | is_type_level_sound _ = false

val is_type_enc_sound = is_type_level_sound o level_of_type_enc

fun is_type_level_monotonicity_based (Nonmono_Types _) = true

  | is_type_level_monotonicity_based _ = false

val no_lamsN = "no_lams" (* used internally; undocumented *)

val hide_lamsN = "hide_lams"

val liftingN = "lifting"

val combsN = "combs"

val combs_and_liftingN = "combs_and_lifting"

val combs_or_liftingN = "combs_or_lifting"

val keep_lamsN = "keep_lams"

val lam_liftingN = "lam_lifting" (* legacy *)

val bound_var_prefix = "B_"

val all_bound_var_prefix = "A_"

val exist_bound_var_prefix = "E_"

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 native_type_prefix = "n_"

val class_prefix = "cl_"

(* Freshness almost guaranteed! *)

val atp_prefix = "ATP" ^ Long_Name.separator

val atp_weak_prefix = "ATP:"

val lam_lifted_prefix = atp_weak_prefix ^ "Lam"

val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"

val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"

val skolem_const_prefix = atp_prefix ^ "Sko"

val old_skolem_const_prefix = skolem_const_prefix ^ "o"

val new_skolem_const_prefix = skolem_const_prefix ^ "n"

val combinator_prefix = "COMB"

val type_decl_prefix = "ty_"

val sym_decl_prefix = "sy_"

val guards_sym_formula_prefix = "gsy_"

val tags_sym_formula_prefix = "tsy_"

val uncurried_alias_eq_prefix = "unc_"

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 lam_fact_prefix = "ATP.lambda_"

val typed_helper_suffix = "_T"

val untyped_helper_suffix = "_U"

val predicator_name = "pp"

val app_op_name = "aa"

val type_guard_name = "gg"

val type_tag_name = "tt"

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

(*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 General.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 unprefix_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})))),

   ("c_All", (@{const_name All}, (@{thm fAll_def},

       ("fAll", @{const_name ATP.fAll})))),

   ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},

       ("fEx", @{const_name ATP.fEx}))))]

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 All}, "All"),

   (@{const_name Ex}, "Ex"),

   (@{const_name If}, "If"),

   (@{const_name Set.member}, "member"),

   (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),

   (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),

   (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),

   (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),

   (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]

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

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_all_bound_var x = all_bound_var_prefix ^ ascii_of x

fun make_exist_bound_var x = exist_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_tvar (s, i) = tvar_prefix ^ (ascii_of_indexname (unprefix "'" s, i))

fun make_tfree s = tfree_prefix ^ (ascii_of (unprefix "'" s))

fun tvar_name (x as (s, _)) = (make_tvar x, s)

(* "HOL.eq" and choice are mapped to the ATP's equivalents *)

local

  val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT

  fun default c = const_prefix ^ lookup_const c

in

  fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal

    | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _))) c =

      if c = choice_const then tptp_choice else default c

    | make_fixed_const _ c = default c

end

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

(* These are either simplified away by "Meson.presimplify" (most of the time) or

   handled specially via "fFalse", "fTrue", ..., "fequal". *)

val atp_irrelevant_consts =

  [@{const_name False}, @{const_name True}, @{const_name Not},

   @{const_name conj}, @{const_name disj}, @{const_name implies},

   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]

val atp_monomorph_bad_consts =

  atp_irrelevant_consts @

  (* These are ignored anyway by the relevance filter (unless they appear in

     higher-order places) but not by the monomorphizer. *)

  [@{const_name all}, @{const_name "==>"}, @{const_name "=="},

   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},

   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]

fun add_schematic_const (x as (_, T)) =

  Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x

val add_schematic_consts_of =

  Term.fold_aterms (fn Const (x as (s, _)) =>

                       not (member (op =) atp_monomorph_bad_consts s)

                       ? add_schematic_const x

                      | _ => I)

fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty

val tvar_a_str = "'a"

val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)

val tvar_a_name = tvar_name (tvar_a_str, 0)

val itself_name = `make_fixed_type_const @{type_name itself}

val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}

val tvar_a_atype = AType (tvar_a_name, [])

val a_itself_atype = AType (itself_name, [tvar_a_atype])

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

(** Isabelle arities **)

val type_class = the_single @{sort type}

type arity_clause =

  {name : string,

   prems : (string * typ) list,

   concl : string * typ}

fun add_prem_atom T = fold (fn s => s <> type_class ? cons (s, T))

(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)

fun make_axiom_arity_clause (tc, name, (class, args)) =

  let

    val tvars =

      map (fn j => TVar ((tvar_a_str, j), @{sort HOL.type}))

          (1 upto length args)

  in

    {name = name, prems = fold (uncurry add_prem_atom) (tvars ~~ args) [],

     concl = (class, Type (tc, 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 ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,

          ar) ::

      arity_clause seen (n + 1) (tcons, ars)

    else

      make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^

                               ascii_of 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

        fun maybe_insert_class s =

          (s <> type_class andalso not (member (op =) classes s))

          ? insert (op =) s

        val cpairs = type_class_pairs thy tycons classes

        val newclasses =

          [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs

        val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses

      in (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 : string,

   superclass : string}

(* 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 = sub, superclass = super}

fun make_class_rel_clauses thy subs supers =

  map make_class_rel_clause (class_pairs thy subs supers)

(* intermediate terms *)

datatype iterm =

  IConst of name * typ * typ list |

  IVar of name * typ |

  IApp of iterm * iterm |

  IAbs of (name * typ) * iterm

fun ityp_of (IConst (_, T, _)) = T

  | ityp_of (IVar (_, T)) = T

  | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))

  | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm

(*gets the head of a combinator application, along with the list of arguments*)

fun strip_iterm_comb u =

  let

    fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)

      | stripc x = x

  in stripc (u, []) end

fun atomic_types_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]

  |> Long_Name.implode

val alpha_to_beta = Logic.varifyT_global @{typ "'a => 'b"}

val alpha_to_beta_to_alpha_to_beta = alpha_to_beta --> alpha_to_beta

fun robust_const_type thy s =

  if s = app_op_name then

    alpha_to_beta_to_alpha_to_beta

  else if String.isPrefix lam_lifted_prefix s then

    alpha_to_beta

  else

    (* Old Skolems throw a "TYPE" exception here, which will be caught. *)

    s |> Sign.the_const_type thy

val robust_const_ary =

  let

    fun ary (Type (@{type_name fun}, [_, T])) = 1 + ary T

      | ary _ = 0

  in ary oo robust_const_type end

(* This function only makes sense if "T" is as general as possible. *)

fun robust_const_typargs thy (s, T) =

  if s = app_op_name then

    let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end

  else if String.isPrefix old_skolem_const_prefix s then

    [] |> Term.add_tvarsT T |> rev |> map TVar

  else if String.isPrefix lam_lifted_prefix s then

    if String.isPrefix lam_lifted_poly_prefix s then

      let val (T1, T2) = T |> dest_funT in [T1, T2] end

    else

      []

  else

    (s, T) |> Sign.const_typargs thy

(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.

   Also accumulates sort infomation. *)

fun iterm_from_term thy type_enc bs (P $ Q) =

    let

      val (P', P_atomics_Ts) = iterm_from_term thy type_enc bs P

      val (Q', Q_atomics_Ts) = iterm_from_term thy type_enc bs Q

    in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end

  | iterm_from_term thy type_enc _ (Const (c, T)) =

    (IConst (`(make_fixed_const (SOME type_enc)) c, T,

             robust_const_typargs thy (c, T)),

     atomic_types_of T)

  | iterm_from_term _ _ _ (Free (s, T)) =

    (IConst (`make_fixed_var s, T, []), atomic_types_of T)

  | iterm_from_term _ type_enc _ (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 IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end

     else

       IVar ((make_schematic_var v, s), T), atomic_types_of T)

  | iterm_from_term _ _ bs (Bound j) =

    nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))

  | iterm_from_term thy type_enc bs (Abs (s, T, t)) =

    let

      fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string

      val s = vary s

      val name = `make_bound_var s

      val (tm, atomic_Ts) =

        iterm_from_term thy type_enc ((s, (name, T)) :: bs) t

    in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end

(* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *)

val queries = ["?", "_query"]

val ats = ["@", "_at"]

fun try_unsuffixes ss s =

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

fun type_enc_from_string strictness s =

  (case try (unprefix "tc_") s of

     SOME s => (SOME Type_Class_Polymorphic, s)

   | NONE =>

       case try (unprefix "poly_") s of

         (* It's still unclear whether all TFF1 implementations will support

            type signatures such as "!>[A : $tType] : $o", with phantom type

            variables. *)

         SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)

       | NONE =>

         case try (unprefix "raw_mono_") s of

           SOME s => (SOME Raw_Monomorphic, s)

         | NONE =>

           case try (unprefix "mono_") s of

             SOME s => (SOME Mangled_Monomorphic, s)

           | NONE => (NONE, s))

  ||> (fn s =>

          case try_unsuffixes queries s of

          SOME s =>

          (case try_unsuffixes queries s of

             SOME s => (Nonmono_Types (strictness, Positively_Naked_Vars), s)

           | NONE =>

             case try_unsuffixes ats s of

               SOME s => (Nonmono_Types (strictness, Undercover_Vars), s)

             | NONE => (Nonmono_Types (strictness, All_Vars), s))

         | NONE => (All_Types, s))

  |> (fn (poly, (level, core)) =>

         case (core, (poly, level)) of

           ("native", (SOME poly, _)) =>

           (case (poly, level) of

              (Mangled_Monomorphic, _) =>

              if granularity_of_type_level level = All_Vars then

                Native (First_Order, Mangled_Monomorphic, level)

              else

                raise Same.SAME

            | (Raw_Monomorphic, _) => raise Same.SAME

            | (poly, All_Types) => Native (First_Order, poly, All_Types))

         | ("native_higher", (SOME poly, _)) =>

           (case (poly, level) of

              (_, Nonmono_Types _) => raise Same.SAME

            | (Mangled_Monomorphic, _) =>

              if granularity_of_type_level level = All_Vars then

                Native (Higher_Order THF_With_Choice, Mangled_Monomorphic,

                        level)

              else

                raise Same.SAME

            | (Raw_Monomorphic, _) => raise Same.SAME

            | (poly, All_Types) =>

              Native (Higher_Order THF_With_Choice, poly, All_Types))

         | ("guards", (SOME poly, _)) =>

           if poly = Mangled_Monomorphic andalso

              granularity_of_type_level level = Undercover_Vars then

             raise Same.SAME

           else

             Guards (poly, level)

         | ("tags", (SOME poly, _)) =>

           if granularity_of_type_level level = Undercover_Vars then

             raise Same.SAME

           else

             Tags (poly, level)

         | ("args", (SOME poly, All_Types (* naja *))) =>

           Guards (poly, Const_Types false)

         | ("args", (SOME poly, Nonmono_Types (_, All_Vars) (* naja *))) =>

           if poly = Mangled_Monomorphic then raise Same.SAME

           else Guards (poly, Const_Types true)

         | ("erased", (NONE, All_Types (* naja *))) =>

           Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)

         | _ => raise Same.SAME)

  handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")

fun adjust_order THF_Without_Choice (Higher_Order _) =

    Higher_Order THF_Without_Choice

  | adjust_order _ type_enc = type_enc

fun adjust_type_enc (THF (Polymorphic, _, choice, _))

                    (Native (order, poly, level)) =

    Native (adjust_order choice order, poly, level)

  | adjust_type_enc (THF (Monomorphic, _, choice, _))

                         (Native (order, _, level)) =

    Native (adjust_order choice order, Mangled_Monomorphic, level)

  | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) =

    Native (First_Order, Mangled_Monomorphic, level)

  | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =

    Native (First_Order, poly, level)

  | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) =

    Native (First_Order, Mangled_Monomorphic, level)

  | adjust_type_enc (TFF _) (Native (_, poly, level)) =

    Native (First_Order, poly, level)

  | adjust_type_enc format (Native (_, poly, level)) =

    adjust_type_enc format (Guards (poly, level))

  | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =

    (if is_type_enc_sound type_enc then Tags else Guards) stuff

  | adjust_type_enc _ type_enc = type_enc

fun is_fol_term t =

  case t of

    @{const Not} $ t1 => is_fol_term t1

  | Const (@{const_name All}, _) $ Abs (_, _, t') => is_fol_term t'

  | Const (@{const_name All}, _) $ t1 => is_fol_term t1

  | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_fol_term t'

  | Const (@{const_name Ex}, _) $ t1 => is_fol_term t1

  | @{const HOL.conj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2

  | @{const HOL.disj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2

  | @{const HOL.implies} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2

  | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>

    is_fol_term t1 andalso is_fol_term t2

  | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)

fun simple_translate_lambdas do_lambdas ctxt t =

  if is_fol_term t then

    t

  else

    let

      fun trans Ts t =

        case t of

          @{const Not} $ t1 => @{const Not} $ trans Ts t1

        | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>

          t0 $ Abs (s, T, trans (T :: Ts) t')

        | (t0 as Const (@{const_name All}, _)) $ t1 =>

          trans Ts (t0 $ eta_expand Ts t1 1)

        | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>

          t0 $ Abs (s, T, trans (T :: Ts) t')

        | (t0 as Const (@{const_name Ex}, _)) $ t1 =>

          trans Ts (t0 $ eta_expand Ts t1 1)

        | (t0 as @{const HOL.conj}) $ t1 $ t2 =>

          t0 $ trans Ts t1 $ trans Ts t2

        | (t0 as @{const HOL.disj}) $ t1 $ t2 =>

          t0 $ trans Ts t1 $ trans Ts t2

        | (t0 as @{const HOL.implies}) $ t1 $ t2 =>

          t0 $ trans Ts t1 $ trans Ts t2

        | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))

            $ t1 $ t2 =>

          t0 $ trans Ts t1 $ trans Ts t2

        | _ =>

          if not (exists_subterm (fn Abs _ => true | _ => false) t) then t

          else t |> Envir.eta_contract |> do_lambdas ctxt Ts

      val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single

    in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end

fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =

    do_cheaply_conceal_lambdas Ts t1

    $ do_cheaply_conceal_lambdas Ts t2

  | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =

    Const (lam_lifted_poly_prefix ^ serial_string (),

           T --> fastype_of1 (T :: Ts, t))

  | do_cheaply_conceal_lambdas _ t = t

fun concealed_bound_name j = atp_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 do_introduce_combinators ctxt Ts t =

  let val thy = Proof_Context.theory_of ctxt in

    t |> conceal_bounds Ts

      |> cterm_of thy

      |> Meson_Clausify.introduce_combinators_in_cterm

      |> prop_of |> Logic.dest_equals |> snd

      |> reveal_bounds Ts

  end

  (* A type variable of sort "{}" will make abstraction fail. *)

  handle THM _ => t |> do_cheaply_conceal_lambdas Ts

val introduce_combinators = simple_translate_lambdas do_introduce_combinators

fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u

  | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)

  | constify_lifted (Free (x as (s, _))) =

    (if String.isPrefix lam_lifted_prefix s then Const else Free) x

  | constify_lifted t = t

fun lift_lams_part_1 ctxt type_enc =

  map close_form #> rpair ctxt

  #-> Lambda_Lifting.lift_lambdas

          (SOME ((if is_type_enc_polymorphic type_enc then

                    lam_lifted_poly_prefix

                  else

                    lam_lifted_mono_prefix) ^ "_a"))

          Lambda_Lifting.is_quantifier

  #> fst

fun lift_lams_part_2 ctxt (facts, lifted) =

  (facts, lifted)

  (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid

     of them *)

  |> pairself (map (introduce_combinators ctxt))

  |> pairself (map constify_lifted)

  (* Requires bound variables not to clash with any schematic variables (as

     should be the case right after lambda-lifting). *)

  |>> map (open_form (unprefix close_form_prefix))

  ||> map (open_form I)

fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt

fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =

    intentionalize_def t

  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =

    let

      fun lam T t = Abs (Name.uu, T, t)

      val (head, args) = strip_comb t ||> rev

      val head_T = fastype_of head

      val n = length args

      val arg_Ts = head_T |> binder_types |> take n |> rev

      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))

    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end

  | intentionalize_def t = t

type ifact =

  {name : string,

   stature : stature,

   role : formula_role,

   iformula : (name, typ, iterm) formula,

   atomic_types : typ list}

fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) =

  {name = name, stature = stature, role = role, iformula = f iformula,

   atomic_types = atomic_types} : ifact

fun ifact_lift f ({iformula, ...} : ifact) = f iformula

fun insert_type thy get_T x xs =

  let val T = get_T x in

    if exists (type_instance thy T o get_T) xs then xs

    else x :: filter_out (type_generalization thy T o get_T) xs

  end

(* The Booleans indicate whether all type arguments should be kept. *)

datatype type_arg_policy =

  Mangled_Type_Args |

  All_Type_Args |

  Noninferable_Type_Args |

  Constr_Type_Args |

  No_Type_Args

fun type_arg_policy constrs type_enc s =

  let val poly = polymorphism_of_type_enc type_enc in

    if s = type_tag_name then

      if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args

    else case type_enc of

      Native (_, Raw_Polymorphic _, _) => All_Type_Args

    | Native (_, Type_Class_Polymorphic, _) => All_Type_Args

    | Tags (_, All_Types) => No_Type_Args

    | _ =>

      let val level = level_of_type_enc type_enc in

        if level = No_Types orelse s = @{const_name HOL.eq} orelse

           (case level of Const_Types _ => s = app_op_name | _ => false) then

          No_Type_Args

        else if poly = Mangled_Monomorphic then

          Mangled_Type_Args

        else if level = All_Types orelse

                granularity_of_type_level level = Undercover_Vars then

          Noninferable_Type_Args

        else if member (op =) constrs s andalso level <> Const_Types false then

          Constr_Type_Args

        else

          All_Type_Args

      end

  end

val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)

val fused_infinite_type = Type (fused_infinite_type_name, [])

fun ho_term_from_typ type_enc =

  let

    fun term (Type (s, Ts)) =

      ATerm ((case (is_type_enc_higher_order type_enc, s) of

                (true, @{type_name bool}) => `I tptp_bool_type

              | (true, @{type_name fun}) => `I tptp_fun_type

              | _ => if s = fused_infinite_type_name andalso

                        is_type_enc_native type_enc then

                       `I tptp_individual_type

                     else

                       `make_fixed_type_const s,

              []), map term Ts)

    | term (TFree (s, _)) = ATerm ((`make_tfree s, []), [])

    | term (TVar (x, _)) = ATerm ((tvar_name x, []), [])

  in term end

fun ho_term_for_type_arg type_enc T =

  if T = dummyT then NONE else SOME (ho_term_from_typ type_enc T)

(* This shouldn't clash with anything else. *)

val uncurried_alias_sep = "\000"

val mangled_type_sep = "\001"

val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep

(* ### FIXME: insane *)

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)

    ^ ")"

  | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"

fun mangled_type type_enc =

  generic_mangled_type_name fst o ho_term_from_typ type_enc

fun make_native_type s =

  if s = tptp_bool_type orelse s = tptp_fun_type orelse

     s = tptp_individual_type then

    s

  else

    native_type_prefix ^ ascii_of s

fun ho_type_from_ho_term type_enc pred_sym ary =

  let

    fun to_mangled_atype ty =

      AType ((make_native_type (generic_mangled_type_name fst ty),

              generic_mangled_type_name snd ty), [])

    fun to_poly_atype (ATerm ((name, []), tys)) =

        AType (name, map to_poly_atype tys)

      | to_poly_atype _ = raise Fail "unexpected type abstraction"

    val to_atype =

      if is_type_enc_polymorphic type_enc then to_poly_atype

      else to_mangled_atype

    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

      | to_fo _ _ = raise Fail "unexpected type abstraction"

    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

      | to_ho _ = raise Fail "unexpected type abstraction"

  in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end

fun ho_type_from_typ type_enc pred_sym ary =

  ho_type_from_ho_term type_enc pred_sym ary

  o ho_term_from_typ type_enc

(* Make atoms for sorted type variables. *)

fun generic_add_sorts_on_type _ [] = I

  | generic_add_sorts_on_type T (s :: ss) =

    generic_add_sorts_on_type T ss

    #> (if s = the_single @{sort HOL.type} then I else insert (op =) (s, T))

fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S

  | add_sorts_on_tfree _ = I

fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S

  | add_sorts_on_tvar _ = I

fun process_type_args type_enc T_args =

  if is_type_enc_native type_enc then

    (map (ho_type_from_typ type_enc false 0) T_args, [])

  else

    ([], map_filter (ho_term_for_type_arg type_enc) T_args)

fun type_class_atom type_enc (class, T) =

  let

    val class = `make_type_class class

    val (ty_args, tm_args) = process_type_args type_enc [T]

    val tm_args =

      tm_args @

      (case type_enc of

         Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>

         [ATerm ((TYPE_name, ty_args), [])]

       | _ => [])

  in AAtom (ATerm ((class, ty_args), tm_args)) end

fun formulas_for_types type_enc add_sorts_on_typ Ts =

  [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts

     |> map (type_class_atom type_enc)

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 mk_atyquant _ [] phi = phi

  | mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) =

    if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi)

  | mk_atyquant q xs phi = ATyQuant (q, xs, phi)

fun close_universally add_term_vars phi =

  let

    fun add_formula_vars bounds (ATyQuant (_, _, phi)) =

        add_formula_vars bounds phi

      | add_formula_vars bounds (AQuant (_, xs, phi)) =

        add_formula_vars (map fst xs @ bounds) phi