(*  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_kind = ATP_Problem.formula_kind

  type 'a problem = 'a ATP_Problem.problem

  datatype scope = Global | Local | Assum | Chained

  datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq

  type stature = scope * status

  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic

  datatype strictness = Strict | Non_Strict

  datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars

  datatype type_level =

    All_Types |

    Noninf_Nonmono_Types of strictness * granularity |

    Fin_Nonmono_Types of granularity |

    Const_Arg_Types |

    No_Types

  type type_enc

  val type_tag_idempotence : bool Config.T

  val type_tag_arguments : bool Config.T

  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 type_tag_idempotence_helper_name : 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 polymorphism_of_type_enc : type_enc -> polymorphism

  val level_of_type_enc : type_enc -> type_level

  val is_type_enc_quasi_sound : type_enc -> bool

  val is_type_enc_fairly_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) * 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_kind -> formula_kind -> type_enc

    -> bool -> 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_weights : string problem -> (string * int) list

end;

structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =

struct

open ATP_Util

open ATP_Problem

type name = string * string

val type_tag_idempotence =

  Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)

val type_tag_arguments =

  Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K 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 *)

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

   signatures such as "!>[A : $tType] : $o", with ghost type variables. *)

val avoid_first_order_ghost_type_vars = false

val bound_var_prefix = "B_"

val all_bound_var_prefix = "BA_"

val exist_bound_var_prefix = "BE_"

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 type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"

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_schematic_type_var (x, i) =

  tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))

fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))

(* "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 (THF (_, _, 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

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

(** Isabelle arities **)

type arity_atom = name * name * name list

val type_class = the_single @{sort type}

type arity_clause =

  {name : string,

   prem_atoms : arity_atom list,

   concl_atom : arity_atom}

fun add_prem_atom tvar =

  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))

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

fun make_axiom_arity_clause (tcons, name, (cls, args)) =

  let

    val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)

    val tvars_srts = ListPair.zip (tvars, args)

  in

    {name = name,

     prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,

     concl_atom = (`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 ^ "___" ^ 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 : 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)

(* 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 []

val tvar_a_str = "'a"

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

val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)

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

fun new_skolem_const_name s num_T_args =

  [new_skolem_const_prefix, s, string_of_int num_T_args]

  |> Long_Name.implode

fun robust_const_type thy s =

  if s = app_op_name then

    Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}

  else if String.isPrefix lam_lifted_prefix s then

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

  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 format bs (P $ Q) =

    let

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

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

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

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

    (IConst (`(make_fixed_const (SOME format)) 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 _ format _ (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 format)) 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 format 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 format ((s, (name, T)) :: bs) t

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

datatype scope = Global | Local | Assum | Chained

datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq

type stature = scope * status

datatype order = First_Order | Higher_Order

datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic

datatype strictness = Strict | Non_Strict

datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars

datatype type_level =

  All_Types |

  Noninf_Nonmono_Types of strictness * granularity |

  Fin_Nonmono_Types of granularity |

  Const_Arg_Types |

  No_Types

datatype type_enc =

  Simple_Types of order * polymorphism * type_level |

  Guards of polymorphism * type_level |

  Tags of polymorphism * type_level

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

  | is_type_enc_higher_order _ = false

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

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

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

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

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

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

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

  | granularity_of_type_level (Fin_Nonmono_Types grain) = grain

  | granularity_of_type_level _ = All_Vars

fun is_type_level_quasi_sound All_Types = true

  | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true

  | is_type_level_quasi_sound _ = false

val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc

fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true

  | is_type_level_fairly_sound level = is_type_level_quasi_sound level

val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc

fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true

  | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true

  | is_type_level_monotonicity_based _ = false

(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and

   Mirabelle. *)

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

val bangs = ["!", "_bang"]

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

fun try_unsuffixes ss s =

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

fun try_nonmono constr suffixes fallback s =

  case try_unsuffixes suffixes s of

    SOME s =>

    (case try_unsuffixes suffixes s of

       SOME s => (constr Positively_Naked_Vars, s)

     | NONE =>

       case try_unsuffixes ats s of

         SOME s => (constr Ghost_Type_Arg_Vars, s)

       | NONE => (constr All_Vars, s))

  | NONE => fallback s

fun type_enc_from_string strictness s =

  (case try (unprefix "poly_") s of

     SOME s => (SOME Polymorphic, 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))

  ||> (pair All_Types

       |> try_nonmono Fin_Nonmono_Types bangs

       |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)

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

         case (core, (poly, level)) of

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

           (case (poly, level) of

              (Polymorphic, All_Types) =>

              Simple_Types (First_Order, Polymorphic, All_Types)

            | (Mangled_Monomorphic, _) =>

              if granularity_of_type_level level = All_Vars then

                Simple_Types (First_Order, Mangled_Monomorphic, level)

              else

                raise Same.SAME

            | _ => raise Same.SAME)

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

           (case (poly, level) of

              (Polymorphic, All_Types) =>

              Simple_Types (Higher_Order, Polymorphic, All_Types)

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

            | (Mangled_Monomorphic, _) =>

              if granularity_of_type_level level = All_Vars then

                Simple_Types (Higher_Order, Mangled_Monomorphic, level)

              else

                raise Same.SAME

            | _ => raise Same.SAME)

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

           if poly = Mangled_Monomorphic andalso

              granularity_of_type_level level = Ghost_Type_Arg_Vars then

             raise Same.SAME

           else

             Guards (poly, level)

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

           if granularity_of_type_level level = Ghost_Type_Arg_Vars then

             raise Same.SAME

           else

             Tags (poly, level)

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

           Guards (poly, Const_Arg_Types)

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

           Guards (Polymorphic, No_Types)

         | _ => raise Same.SAME)

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

fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))

                    (Simple_Types (order, _, level)) =

    Simple_Types (order, Mangled_Monomorphic, level)

  | adjust_type_enc (THF _) type_enc = type_enc

  | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =

    Simple_Types (First_Order, Mangled_Monomorphic, level)

  | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =

    Simple_Types (First_Order, Mangled_Monomorphic, level)

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

    Simple_Types (First_Order, poly, level)

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

    adjust_type_enc format (Guards (poly, level))

  | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =

    (if is_type_enc_fairly_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

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

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

fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =

    (case try unprefix s of

       SOME s =>

       let

         val names = Name.make_context (map fst (Term.add_var_names t' []))

         val (s, _) = Name.variant s names

       in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end

     | NONE => t)

  | open_form _ t = t

fun lift_lams_part_1 ctxt type_enc =

  map close_form #> rpair ctxt

  #-> Lambda_Lifting.lift_lambdas

          (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic 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)

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

  {name : string,

   stature : stature,

   kind : formula_kind,

   iformula : (name, typ, iterm) formula,

   atomic_types : typ list}

fun update_iformula f ({name, stature, kind, iformula, atomic_types}

                       : translated_formula) =

  {name = name, stature = stature, kind = kind, iformula = f iformula,

   atomic_types = atomic_types} : translated_formula

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

fun insert_type ctxt get_T x xs =

  let val T = get_T x in

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

    else x :: filter_out (type_generalization ctxt 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 (* infer_from_term_args *) |

  Mangled_Type_Args |

  No_Type_Args

fun type_arg_policy monom_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 Explicit_Type_Args false

    else case type_enc of

      Simple_Types (_, Polymorphic, _) => Explicit_Type_Args false

    | 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

           (s = app_op_name andalso level = Const_Arg_Types) then

          No_Type_Args

        else if poly = Mangled_Monomorphic then

          Mangled_Type_Args

        else if member (op =) monom_constrs s andalso

                granularity_of_type_level level = Positively_Naked_Vars then

          No_Type_Args

        else

          Explicit_Type_Args

              (level = All_Types orelse

               granularity_of_type_level level = Ghost_Type_Arg_Vars)

      end

  end

(* Make atoms for sorted type variables. *)

fun generic_add_sorts_on_type (_, []) = I

  | generic_add_sorts_on_type ((x, i), s :: ss) =

    generic_add_sorts_on_type ((x, i), ss)

    #> (if s = the_single @{sort HOL.type} then

          I

        else if i = ~1 then

          insert (op =) (`make_type_class s, `make_fixed_type_var x)

        else

          insert (op =) (`make_type_class s,

                         (make_schematic_type_var (x, i), x)))

fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)

  | add_sorts_on_tfree _ = I

fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z

  | add_sorts_on_tvar _ = I

fun type_class_formula type_enc class arg =

  AAtom (ATerm (class, arg ::

      (case type_enc of

         Simple_Types (First_Order, Polymorphic, _) =>

         if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]

         else []

       | _ => [])))

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 (fn (class, name) =>

                type_class_formula type_enc class (ATerm (name, [])))

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 add_term_vars phi =

  let

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

        add_formula_vars (map fst xs @ bounds) phi

      | add_formula_vars bounds (AConn (_, phis)) =

        fold (add_formula_vars bounds) phis

      | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm

  in mk_aquant AForall (add_formula_vars [] phi []) phi end

fun add_term_vars bounds (ATerm (name as (s, _), tms)) =

    (if is_tptp_variable s andalso

        not (String.isPrefix tvar_prefix s) andalso

        not (member (op =) bounds name) then

       insert (op =) (name, NONE)

     else

       I)

    #> fold (add_term_vars bounds) tms

  | add_term_vars bounds (AAbs ((name, _), tm)) =

    add_term_vars (name :: bounds) tm

fun close_formula_universally phi = close_universally add_term_vars phi

fun add_iterm_vars bounds (IApp (tm1, tm2)) =

    fold (add_iterm_vars bounds) [tm1, tm2]

  | add_iterm_vars _ (IConst _) = I

  | add_iterm_vars bounds (IVar (name, T)) =

    not (member (op =) bounds name) ? insert (op =) (name, SOME T)

  | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm

fun close_iformula_universally phi = close_universally add_iterm_vars phi

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

val fused_infinite_type = Type (fused_infinite_type_name, [])

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

fun ho_term_from_typ format 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_format_typed format 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, _)) = ATerm (tvar_name x, [])

  in term end

fun ho_term_for_type_arg format type_enc T =

  if T = dummyT then NONE else SOME (ho_term_from_typ format 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

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 format type_enc =

  generic_mangled_type_name fst o ho_term_from_typ format 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 =