src/HOL/Tools/ATP/atp_problem_generate.ML
author blanchet
Sun Mar 04 23:20:43 2012 +0100 (2012-03-04)
changeset 46818 2a28e66e2e4c
parent 46711 f745bcc4a1e5
child 47030 7e80e14247fc
permissions -rw-r--r--
ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
     1 (*  Title:      HOL/Tools/ATP/atp_problem_generate.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Translation of HOL to FOL for Metis and Sledgehammer.
     7 *)
     8 
     9 signature ATP_PROBLEM_GENERATE =
    10 sig
    11   type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
    12   type connective = ATP_Problem.connective
    13   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
    14   type atp_format = ATP_Problem.atp_format
    15   type formula_kind = ATP_Problem.formula_kind
    16   type 'a problem = 'a ATP_Problem.problem
    17 
    18   datatype scope = Global | Local | Assum | Chained
    19   datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
    20   type stature = scope * status
    21 
    22   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    23   datatype strictness = Strict | Non_Strict
    24   datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
    25   datatype type_level =
    26     All_Types |
    27     Noninf_Nonmono_Types of strictness * granularity |
    28     Fin_Nonmono_Types of granularity |
    29     Const_Arg_Types |
    30     No_Types
    31   type type_enc
    32 
    33   val type_tag_idempotence : bool Config.T
    34   val type_tag_arguments : bool Config.T
    35   val no_lamsN : string
    36   val hide_lamsN : string
    37   val liftingN : string
    38   val combsN : string
    39   val combs_and_liftingN : string
    40   val combs_or_liftingN : string
    41   val lam_liftingN : string
    42   val keep_lamsN : string
    43   val schematic_var_prefix : string
    44   val fixed_var_prefix : string
    45   val tvar_prefix : string
    46   val tfree_prefix : string
    47   val const_prefix : string
    48   val type_const_prefix : string
    49   val class_prefix : string
    50   val lam_lifted_prefix : string
    51   val lam_lifted_mono_prefix : string
    52   val lam_lifted_poly_prefix : string
    53   val skolem_const_prefix : string
    54   val old_skolem_const_prefix : string
    55   val new_skolem_const_prefix : string
    56   val combinator_prefix : string
    57   val type_decl_prefix : string
    58   val sym_decl_prefix : string
    59   val guards_sym_formula_prefix : string
    60   val tags_sym_formula_prefix : string
    61   val fact_prefix : string
    62   val conjecture_prefix : string
    63   val helper_prefix : string
    64   val class_rel_clause_prefix : string
    65   val arity_clause_prefix : string
    66   val tfree_clause_prefix : string
    67   val lam_fact_prefix : string
    68   val typed_helper_suffix : string
    69   val untyped_helper_suffix : string
    70   val type_tag_idempotence_helper_name : string
    71   val predicator_name : string
    72   val app_op_name : string
    73   val type_guard_name : string
    74   val type_tag_name : string
    75   val native_type_prefix : string
    76   val prefixed_predicator_name : string
    77   val prefixed_app_op_name : string
    78   val prefixed_type_tag_name : string
    79   val ascii_of : string -> string
    80   val unascii_of : string -> string
    81   val unprefix_and_unascii : string -> string -> string option
    82   val proxy_table : (string * (string * (thm * (string * string)))) list
    83   val proxify_const : string -> (string * string) option
    84   val invert_const : string -> string
    85   val unproxify_const : string -> string
    86   val new_skolem_var_name_from_const : string -> string
    87   val atp_irrelevant_consts : string list
    88   val atp_schematic_consts_of : term -> typ list Symtab.table
    89   val is_type_enc_higher_order : type_enc -> bool
    90   val polymorphism_of_type_enc : type_enc -> polymorphism
    91   val level_of_type_enc : type_enc -> type_level
    92   val is_type_enc_quasi_sound : type_enc -> bool
    93   val is_type_enc_fairly_sound : type_enc -> bool
    94   val type_enc_from_string : strictness -> string -> type_enc
    95   val adjust_type_enc : atp_format -> type_enc -> type_enc
    96   val mk_aconns :
    97     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    98   val unmangled_const : string -> string * (string, 'b) ho_term list
    99   val unmangled_const_name : string -> string list
   100   val helper_table : ((string * bool) * thm list) list
   101   val trans_lams_from_string :
   102     Proof.context -> type_enc -> string -> term list -> term list * term list
   103   val factsN : string
   104   val prepare_atp_problem :
   105     Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
   106     -> bool -> string -> bool -> bool -> bool -> term list -> term
   107     -> ((string * stature) * term) list
   108     -> string problem * string Symtab.table * (string * stature) list vector
   109        * (string * term) list * int Symtab.table
   110   val atp_problem_relevance_weights : string problem -> (string * real) list
   111   val atp_problem_kbo_weights : string problem -> (string * int) list
   112 end;
   113 
   114 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
   115 struct
   116 
   117 open ATP_Util
   118 open ATP_Problem
   119 
   120 type name = string * string
   121 
   122 val type_tag_idempotence =
   123   Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
   124 val type_tag_arguments =
   125   Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
   126 
   127 val no_lamsN = "no_lams" (* used internally; undocumented *)
   128 val hide_lamsN = "hide_lams"
   129 val liftingN = "lifting"
   130 val combsN = "combs"
   131 val combs_and_liftingN = "combs_and_lifting"
   132 val combs_or_liftingN = "combs_or_lifting"
   133 val keep_lamsN = "keep_lams"
   134 val lam_liftingN = "lam_lifting" (* legacy *)
   135 
   136 (* It's still unclear whether all TFF1 implementations will support type
   137    signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
   138 val avoid_first_order_ghost_type_vars = false
   139 
   140 val bound_var_prefix = "B_"
   141 val all_bound_var_prefix = "BA_"
   142 val exist_bound_var_prefix = "BE_"
   143 val schematic_var_prefix = "V_"
   144 val fixed_var_prefix = "v_"
   145 val tvar_prefix = "T_"
   146 val tfree_prefix = "t_"
   147 val const_prefix = "c_"
   148 val type_const_prefix = "tc_"
   149 val native_type_prefix = "n_"
   150 val class_prefix = "cl_"
   151 
   152 (* Freshness almost guaranteed! *)
   153 val atp_prefix = "ATP" ^ Long_Name.separator
   154 val atp_weak_prefix = "ATP:"
   155 
   156 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
   157 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
   158 val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
   159 
   160 val skolem_const_prefix = atp_prefix ^ "Sko"
   161 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
   162 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
   163 
   164 val combinator_prefix = "COMB"
   165 
   166 val type_decl_prefix = "ty_"
   167 val sym_decl_prefix = "sy_"
   168 val guards_sym_formula_prefix = "gsy_"
   169 val tags_sym_formula_prefix = "tsy_"
   170 val uncurried_alias_eq_prefix = "unc_"
   171 val fact_prefix = "fact_"
   172 val conjecture_prefix = "conj_"
   173 val helper_prefix = "help_"
   174 val class_rel_clause_prefix = "clar_"
   175 val arity_clause_prefix = "arity_"
   176 val tfree_clause_prefix = "tfree_"
   177 
   178 val lam_fact_prefix = "ATP.lambda_"
   179 val typed_helper_suffix = "_T"
   180 val untyped_helper_suffix = "_U"
   181 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
   182 
   183 val predicator_name = "pp"
   184 val app_op_name = "aa"
   185 val type_guard_name = "gg"
   186 val type_tag_name = "tt"
   187 
   188 val prefixed_predicator_name = const_prefix ^ predicator_name
   189 val prefixed_app_op_name = const_prefix ^ app_op_name
   190 val prefixed_type_tag_name = const_prefix ^ type_tag_name
   191 
   192 (*Escaping of special characters.
   193   Alphanumeric characters are left unchanged.
   194   The character _ goes to __
   195   Characters in the range ASCII space to / go to _A to _P, respectively.
   196   Other characters go to _nnn where nnn is the decimal ASCII code.*)
   197 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
   198 
   199 fun stringN_of_int 0 _ = ""
   200   | stringN_of_int k n =
   201     stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
   202 
   203 fun ascii_of_char c =
   204   if Char.isAlphaNum c then
   205     String.str c
   206   else if c = #"_" then
   207     "__"
   208   else if #" " <= c andalso c <= #"/" then
   209     "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
   210   else
   211     (* fixed width, in case more digits follow *)
   212     "_" ^ stringN_of_int 3 (Char.ord c)
   213 
   214 val ascii_of = String.translate ascii_of_char
   215 
   216 (** Remove ASCII armoring from names in proof files **)
   217 
   218 (* We don't raise error exceptions because this code can run inside a worker
   219    thread. Also, the errors are impossible. *)
   220 val unascii_of =
   221   let
   222     fun un rcs [] = String.implode(rev rcs)
   223       | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
   224         (* Three types of _ escapes: __, _A to _P, _nnn *)
   225       | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
   226       | un rcs (#"_" :: c :: cs) =
   227         if #"A" <= c andalso c<= #"P" then
   228           (* translation of #" " to #"/" *)
   229           un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
   230         else
   231           let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
   232             case Int.fromString (String.implode digits) of
   233               SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
   234             | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
   235           end
   236       | un rcs (c :: cs) = un (c :: rcs) cs
   237   in un [] o String.explode end
   238 
   239 (* If string s has the prefix s1, return the result of deleting it,
   240    un-ASCII'd. *)
   241 fun unprefix_and_unascii s1 s =
   242   if String.isPrefix s1 s then
   243     SOME (unascii_of (String.extract (s, size s1, NONE)))
   244   else
   245     NONE
   246 
   247 val proxy_table =
   248   [("c_False", (@{const_name False}, (@{thm fFalse_def},
   249        ("fFalse", @{const_name ATP.fFalse})))),
   250    ("c_True", (@{const_name True}, (@{thm fTrue_def},
   251        ("fTrue", @{const_name ATP.fTrue})))),
   252    ("c_Not", (@{const_name Not}, (@{thm fNot_def},
   253        ("fNot", @{const_name ATP.fNot})))),
   254    ("c_conj", (@{const_name conj}, (@{thm fconj_def},
   255        ("fconj", @{const_name ATP.fconj})))),
   256    ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
   257        ("fdisj", @{const_name ATP.fdisj})))),
   258    ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
   259        ("fimplies", @{const_name ATP.fimplies})))),
   260    ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
   261        ("fequal", @{const_name ATP.fequal})))),
   262    ("c_All", (@{const_name All}, (@{thm fAll_def},
   263        ("fAll", @{const_name ATP.fAll})))),
   264    ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
   265        ("fEx", @{const_name ATP.fEx}))))]
   266 
   267 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
   268 
   269 (* Readable names for the more common symbolic functions. Do not mess with the
   270    table unless you know what you are doing. *)
   271 val const_trans_table =
   272   [(@{type_name Product_Type.prod}, "prod"),
   273    (@{type_name Sum_Type.sum}, "sum"),
   274    (@{const_name False}, "False"),
   275    (@{const_name True}, "True"),
   276    (@{const_name Not}, "Not"),
   277    (@{const_name conj}, "conj"),
   278    (@{const_name disj}, "disj"),
   279    (@{const_name implies}, "implies"),
   280    (@{const_name HOL.eq}, "equal"),
   281    (@{const_name All}, "All"),
   282    (@{const_name Ex}, "Ex"),
   283    (@{const_name If}, "If"),
   284    (@{const_name Set.member}, "member"),
   285    (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
   286    (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
   287    (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
   288    (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
   289    (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
   290   |> Symtab.make
   291   |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
   292 
   293 (* Invert the table of translations between Isabelle and ATPs. *)
   294 val const_trans_table_inv =
   295   const_trans_table |> Symtab.dest |> map swap |> Symtab.make
   296 val const_trans_table_unprox =
   297   Symtab.empty
   298   |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
   299 
   300 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
   301 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
   302 
   303 fun lookup_const c =
   304   case Symtab.lookup const_trans_table c of
   305     SOME c' => c'
   306   | NONE => ascii_of c
   307 
   308 fun ascii_of_indexname (v, 0) = ascii_of v
   309   | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
   310 
   311 fun make_bound_var x = bound_var_prefix ^ ascii_of x
   312 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
   313 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
   314 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
   315 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
   316 
   317 fun make_schematic_type_var (x, i) =
   318   tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
   319 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
   320 
   321 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
   322 local
   323   val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
   324   fun default c = const_prefix ^ lookup_const c
   325 in
   326   fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
   327     | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
   328       if c = choice_const then tptp_choice else default c
   329     | make_fixed_const _ c = default c
   330 end
   331 
   332 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
   333 
   334 fun make_type_class clas = class_prefix ^ ascii_of clas
   335 
   336 fun new_skolem_var_name_from_const s =
   337   let val ss = s |> space_explode Long_Name.separator in
   338     nth ss (length ss - 2)
   339   end
   340 
   341 (* These are either simplified away by "Meson.presimplify" (most of the time) or
   342    handled specially via "fFalse", "fTrue", ..., "fequal". *)
   343 val atp_irrelevant_consts =
   344   [@{const_name False}, @{const_name True}, @{const_name Not},
   345    @{const_name conj}, @{const_name disj}, @{const_name implies},
   346    @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
   347 
   348 val atp_monomorph_bad_consts =
   349   atp_irrelevant_consts @
   350   (* These are ignored anyway by the relevance filter (unless they appear in
   351      higher-order places) but not by the monomorphizer. *)
   352   [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
   353    @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
   354    @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
   355 
   356 fun add_schematic_const (x as (_, T)) =
   357   Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
   358 val add_schematic_consts_of =
   359   Term.fold_aterms (fn Const (x as (s, _)) =>
   360                        not (member (op =) atp_monomorph_bad_consts s)
   361                        ? add_schematic_const x
   362                       | _ => I)
   363 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
   364 
   365 (** Definitions and functions for FOL clauses and formulas for TPTP **)
   366 
   367 (** Isabelle arities **)
   368 
   369 type arity_atom = name * name * name list
   370 
   371 val type_class = the_single @{sort type}
   372 
   373 type arity_clause =
   374   {name : string,
   375    prem_atoms : arity_atom list,
   376    concl_atom : arity_atom}
   377 
   378 fun add_prem_atom tvar =
   379   fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
   380 
   381 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
   382 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
   383   let
   384     val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
   385     val tvars_srts = ListPair.zip (tvars, args)
   386   in
   387     {name = name,
   388      prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
   389      concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
   390                    tvars ~~ tvars)}
   391   end
   392 
   393 fun arity_clause _ _ (_, []) = []
   394   | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)
   395     arity_clause seen n (tcons, ars)
   396   | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
   397     if member (op =) seen class then
   398       (* multiple arities for the same (tycon, class) pair *)
   399       make_axiom_arity_clause (tcons,
   400           lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
   401           ar) ::
   402       arity_clause seen (n + 1) (tcons, ars)
   403     else
   404       make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
   405                                ascii_of class, ar) ::
   406       arity_clause (class :: seen) n (tcons, ars)
   407 
   408 fun multi_arity_clause [] = []
   409   | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   410     arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   411 
   412 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
   413    theory thy provided its arguments have the corresponding sorts. *)
   414 fun type_class_pairs thy tycons classes =
   415   let
   416     val alg = Sign.classes_of thy
   417     fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
   418     fun add_class tycon class =
   419       cons (class, domain_sorts tycon class)
   420       handle Sorts.CLASS_ERROR _ => I
   421     fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
   422   in map try_classes tycons end
   423 
   424 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
   425 fun iter_type_class_pairs _ _ [] = ([], [])
   426   | iter_type_class_pairs thy tycons classes =
   427       let
   428         fun maybe_insert_class s =
   429           (s <> type_class andalso not (member (op =) classes s))
   430           ? insert (op =) s
   431         val cpairs = type_class_pairs thy tycons classes
   432         val newclasses =
   433           [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
   434         val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   435       in (classes' @ classes, union (op =) cpairs' cpairs) end
   436 
   437 fun make_arity_clauses thy tycons =
   438   iter_type_class_pairs thy tycons ##> multi_arity_clause
   439 
   440 
   441 (** Isabelle class relations **)
   442 
   443 type class_rel_clause =
   444   {name : string,
   445    subclass : name,
   446    superclass : name}
   447 
   448 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
   449    in theory "thy". *)
   450 fun class_pairs _ [] _ = []
   451   | class_pairs thy subs supers =
   452       let
   453         val class_less = Sorts.class_less (Sign.classes_of thy)
   454         fun add_super sub super = class_less (sub, super) ? cons (sub, super)
   455         fun add_supers sub = fold (add_super sub) supers
   456       in fold add_supers subs [] end
   457 
   458 fun make_class_rel_clause (sub, super) =
   459   {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
   460    superclass = `make_type_class super}
   461 
   462 fun make_class_rel_clauses thy subs supers =
   463   map make_class_rel_clause (class_pairs thy subs supers)
   464 
   465 (* intermediate terms *)
   466 datatype iterm =
   467   IConst of name * typ * typ list |
   468   IVar of name * typ |
   469   IApp of iterm * iterm |
   470   IAbs of (name * typ) * iterm
   471 
   472 fun ityp_of (IConst (_, T, _)) = T
   473   | ityp_of (IVar (_, T)) = T
   474   | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
   475   | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
   476 
   477 (*gets the head of a combinator application, along with the list of arguments*)
   478 fun strip_iterm_comb u =
   479   let
   480     fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
   481       | stripc x = x
   482   in stripc (u, []) end
   483 
   484 fun atomic_types_of T = fold_atyps (insert (op =)) T []
   485 
   486 val tvar_a_str = "'a"
   487 val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
   488 val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
   489 val itself_name = `make_fixed_type_const @{type_name itself}
   490 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
   491 val tvar_a_atype = AType (tvar_a_name, [])
   492 val a_itself_atype = AType (itself_name, [tvar_a_atype])
   493 
   494 fun new_skolem_const_name s num_T_args =
   495   [new_skolem_const_prefix, s, string_of_int num_T_args]
   496   |> Long_Name.implode
   497 
   498 fun robust_const_type thy s =
   499   if s = app_op_name then
   500     Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
   501   else if String.isPrefix lam_lifted_prefix s then
   502     Logic.varifyT_global @{typ "'a => 'b"}
   503   else
   504     (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
   505     s |> Sign.the_const_type thy
   506 
   507 val robust_const_ary =
   508   let
   509     fun ary (Type (@{type_name fun}, [_, T])) = 1 + ary T
   510       | ary _ = 0
   511   in ary oo robust_const_type end
   512 
   513 (* This function only makes sense if "T" is as general as possible. *)
   514 fun robust_const_typargs thy (s, T) =
   515   if s = app_op_name then
   516     let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
   517   else if String.isPrefix old_skolem_const_prefix s then
   518     [] |> Term.add_tvarsT T |> rev |> map TVar
   519   else if String.isPrefix lam_lifted_prefix s then
   520     if String.isPrefix lam_lifted_poly_prefix s then
   521       let val (T1, T2) = T |> dest_funT in [T1, T2] end
   522     else
   523       []
   524   else
   525     (s, T) |> Sign.const_typargs thy
   526 
   527 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
   528    Also accumulates sort infomation. *)
   529 fun iterm_from_term thy format bs (P $ Q) =
   530     let
   531       val (P', P_atomics_Ts) = iterm_from_term thy format bs P
   532       val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
   533     in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
   534   | iterm_from_term thy format _ (Const (c, T)) =
   535     (IConst (`(make_fixed_const (SOME format)) c, T,
   536              robust_const_typargs thy (c, T)),
   537      atomic_types_of T)
   538   | iterm_from_term _ _ _ (Free (s, T)) =
   539     (IConst (`make_fixed_var s, T, []), atomic_types_of T)
   540   | iterm_from_term _ format _ (Var (v as (s, _), T)) =
   541     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
   542        let
   543          val Ts = T |> strip_type |> swap |> op ::
   544          val s' = new_skolem_const_name s (length Ts)
   545        in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
   546      else
   547        IVar ((make_schematic_var v, s), T), atomic_types_of T)
   548   | iterm_from_term _ _ bs (Bound j) =
   549     nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
   550   | iterm_from_term thy format bs (Abs (s, T, t)) =
   551     let
   552       fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
   553       val s = vary s
   554       val name = `make_bound_var s
   555       val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
   556     in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
   557 
   558 datatype scope = Global | Local | Assum | Chained
   559 datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
   560 type stature = scope * status
   561 
   562 datatype order = First_Order | Higher_Order
   563 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
   564 datatype strictness = Strict | Non_Strict
   565 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
   566 datatype type_level =
   567   All_Types |
   568   Noninf_Nonmono_Types of strictness * granularity |
   569   Fin_Nonmono_Types of granularity |
   570   Const_Arg_Types |
   571   No_Types
   572 
   573 datatype type_enc =
   574   Simple_Types of order * polymorphism * type_level |
   575   Guards of polymorphism * type_level |
   576   Tags of polymorphism * type_level
   577 
   578 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
   579   | is_type_enc_higher_order _ = false
   580 
   581 fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
   582   | polymorphism_of_type_enc (Guards (poly, _)) = poly
   583   | polymorphism_of_type_enc (Tags (poly, _)) = poly
   584 
   585 fun level_of_type_enc (Simple_Types (_, _, level)) = level
   586   | level_of_type_enc (Guards (_, level)) = level
   587   | level_of_type_enc (Tags (_, level)) = level
   588 
   589 fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
   590   | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
   591   | granularity_of_type_level _ = All_Vars
   592 
   593 fun is_type_level_quasi_sound All_Types = true
   594   | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
   595   | is_type_level_quasi_sound _ = false
   596 val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
   597 
   598 fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
   599   | is_type_level_fairly_sound level = is_type_level_quasi_sound level
   600 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
   601 
   602 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
   603   | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
   604   | is_type_level_monotonicity_based _ = false
   605 
   606 (* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
   607    Mirabelle. *)
   608 val queries = ["?", "_query"]
   609 val bangs = ["!", "_bang"]
   610 val ats = ["@", "_at"]
   611 
   612 fun try_unsuffixes ss s =
   613   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
   614 
   615 fun try_nonmono constr suffixes fallback s =
   616   case try_unsuffixes suffixes s of
   617     SOME s =>
   618     (case try_unsuffixes suffixes s of
   619        SOME s => (constr Positively_Naked_Vars, s)
   620      | NONE =>
   621        case try_unsuffixes ats s of
   622          SOME s => (constr Ghost_Type_Arg_Vars, s)
   623        | NONE => (constr All_Vars, s))
   624   | NONE => fallback s
   625 
   626 fun type_enc_from_string strictness s =
   627   (case try (unprefix "poly_") s of
   628      SOME s => (SOME Polymorphic, s)
   629    | NONE =>
   630      case try (unprefix "raw_mono_") s of
   631        SOME s => (SOME Raw_Monomorphic, s)
   632      | NONE =>
   633        case try (unprefix "mono_") s of
   634          SOME s => (SOME Mangled_Monomorphic, s)
   635        | NONE => (NONE, s))
   636   ||> (pair All_Types
   637        |> try_nonmono Fin_Nonmono_Types bangs
   638        |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
   639   |> (fn (poly, (level, core)) =>
   640          case (core, (poly, level)) of
   641            ("native", (SOME poly, _)) =>
   642            (case (poly, level) of
   643               (Polymorphic, All_Types) =>
   644               Simple_Types (First_Order, Polymorphic, All_Types)
   645             | (Mangled_Monomorphic, _) =>
   646               if granularity_of_type_level level = All_Vars then
   647                 Simple_Types (First_Order, Mangled_Monomorphic, level)
   648               else
   649                 raise Same.SAME
   650             | _ => raise Same.SAME)
   651          | ("native_higher", (SOME poly, _)) =>
   652            (case (poly, level) of
   653               (Polymorphic, All_Types) =>
   654               Simple_Types (Higher_Order, Polymorphic, All_Types)
   655             | (_, Noninf_Nonmono_Types _) => raise Same.SAME
   656             | (Mangled_Monomorphic, _) =>
   657               if granularity_of_type_level level = All_Vars then
   658                 Simple_Types (Higher_Order, Mangled_Monomorphic, level)
   659               else
   660                 raise Same.SAME
   661             | _ => raise Same.SAME)
   662          | ("guards", (SOME poly, _)) =>
   663            if poly = Mangled_Monomorphic andalso
   664               granularity_of_type_level level = Ghost_Type_Arg_Vars then
   665              raise Same.SAME
   666            else
   667              Guards (poly, level)
   668          | ("tags", (SOME poly, _)) =>
   669            if granularity_of_type_level level = Ghost_Type_Arg_Vars then
   670              raise Same.SAME
   671            else
   672              Tags (poly, level)
   673          | ("args", (SOME poly, All_Types (* naja *))) =>
   674            Guards (poly, Const_Arg_Types)
   675          | ("erased", (NONE, All_Types (* naja *))) =>
   676            Guards (Polymorphic, No_Types)
   677          | _ => raise Same.SAME)
   678   handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
   679 
   680 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
   681                     (Simple_Types (order, _, level)) =
   682     Simple_Types (order, Mangled_Monomorphic, level)
   683   | adjust_type_enc (THF _) type_enc = type_enc
   684   | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
   685     Simple_Types (First_Order, Mangled_Monomorphic, level)
   686   | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
   687     Simple_Types (First_Order, Mangled_Monomorphic, level)
   688   | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
   689     Simple_Types (First_Order, poly, level)
   690   | adjust_type_enc format (Simple_Types (_, poly, level)) =
   691     adjust_type_enc format (Guards (poly, level))
   692   | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
   693     (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
   694   | adjust_type_enc _ type_enc = type_enc
   695 
   696 fun is_fol_term t =
   697   case t of
   698     @{const Not} $ t1 => is_fol_term t1
   699   | Const (@{const_name All}, _) $ Abs (_, _, t') => is_fol_term t'
   700   | Const (@{const_name All}, _) $ t1 => is_fol_term t1
   701   | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_fol_term t'
   702   | Const (@{const_name Ex}, _) $ t1 => is_fol_term t1
   703   | @{const HOL.conj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
   704   | @{const HOL.disj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
   705   | @{const HOL.implies} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
   706   | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   707     is_fol_term t1 andalso is_fol_term t2
   708   | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)
   709 
   710 fun simple_translate_lambdas do_lambdas ctxt t =
   711   if is_fol_term t then
   712     t
   713   else
   714     let
   715       fun trans Ts t =
   716         case t of
   717           @{const Not} $ t1 => @{const Not} $ trans Ts t1
   718         | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   719           t0 $ Abs (s, T, trans (T :: Ts) t')
   720         | (t0 as Const (@{const_name All}, _)) $ t1 =>
   721           trans Ts (t0 $ eta_expand Ts t1 1)
   722         | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   723           t0 $ Abs (s, T, trans (T :: Ts) t')
   724         | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   725           trans Ts (t0 $ eta_expand Ts t1 1)
   726         | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
   727           t0 $ trans Ts t1 $ trans Ts t2
   728         | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
   729           t0 $ trans Ts t1 $ trans Ts t2
   730         | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
   731           t0 $ trans Ts t1 $ trans Ts t2
   732         | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   733             $ t1 $ t2 =>
   734           t0 $ trans Ts t1 $ trans Ts t2
   735         | _ =>
   736           if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
   737           else t |> Envir.eta_contract |> do_lambdas ctxt Ts
   738       val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   739     in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
   740 
   741 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
   742     do_cheaply_conceal_lambdas Ts t1
   743     $ do_cheaply_conceal_lambdas Ts t2
   744   | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
   745     Const (lam_lifted_poly_prefix ^ serial_string (),
   746            T --> fastype_of1 (T :: Ts, t))
   747   | do_cheaply_conceal_lambdas _ t = t
   748 
   749 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
   750 fun conceal_bounds Ts t =
   751   subst_bounds (map (Free o apfst concealed_bound_name)
   752                     (0 upto length Ts - 1 ~~ Ts), t)
   753 fun reveal_bounds Ts =
   754   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   755                     (0 upto length Ts - 1 ~~ Ts))
   756 
   757 fun do_introduce_combinators ctxt Ts t =
   758   let val thy = Proof_Context.theory_of ctxt in
   759     t |> conceal_bounds Ts
   760       |> cterm_of thy
   761       |> Meson_Clausify.introduce_combinators_in_cterm
   762       |> prop_of |> Logic.dest_equals |> snd
   763       |> reveal_bounds Ts
   764   end
   765   (* A type variable of sort "{}" will make abstraction fail. *)
   766   handle THM _ => t |> do_cheaply_conceal_lambdas Ts
   767 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
   768 
   769 fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
   770   | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
   771   | constify_lifted (Free (x as (s, _))) =
   772     (if String.isPrefix lam_lifted_prefix s then Const else Free) x
   773   | constify_lifted t = t
   774 
   775 (* Requires bound variables not to clash with any schematic variables (as should
   776    be the case right after lambda-lifting). *)
   777 fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
   778     (case try unprefix s of
   779        SOME s =>
   780        let
   781          val names = Name.make_context (map fst (Term.add_var_names t' []))
   782          val (s, _) = Name.variant s names
   783        in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end
   784      | NONE => t)
   785   | open_form _ t = t
   786 
   787 fun lift_lams_part_1 ctxt type_enc =
   788   map close_form #> rpair ctxt
   789   #-> Lambda_Lifting.lift_lambdas
   790           (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
   791                     lam_lifted_poly_prefix
   792                   else
   793                     lam_lifted_mono_prefix) ^ "_a"))
   794           Lambda_Lifting.is_quantifier
   795   #> fst
   796 
   797 fun lift_lams_part_2 ctxt (facts, lifted) =
   798   (facts, lifted)
   799   (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid
   800      of them *)
   801   |> pairself (map (introduce_combinators ctxt))
   802   |> pairself (map constify_lifted)
   803   |>> map (open_form (unprefix close_form_prefix))
   804   ||> map (open_form I)
   805 
   806 fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
   807 
   808 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
   809     intentionalize_def t
   810   | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
   811     let
   812       fun lam T t = Abs (Name.uu, T, t)
   813       val (head, args) = strip_comb t ||> rev
   814       val head_T = fastype_of head
   815       val n = length args
   816       val arg_Ts = head_T |> binder_types |> take n |> rev
   817       val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
   818     in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
   819   | intentionalize_def t = t
   820 
   821 type translated_formula =
   822   {name : string,
   823    stature : stature,
   824    kind : formula_kind,
   825    iformula : (name, typ, iterm) formula,
   826    atomic_types : typ list}
   827 
   828 fun update_iformula f ({name, stature, kind, iformula, atomic_types}
   829                        : translated_formula) =
   830   {name = name, stature = stature, kind = kind, iformula = f iformula,
   831    atomic_types = atomic_types} : translated_formula
   832 
   833 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
   834 
   835 fun insert_type ctxt get_T x xs =
   836   let val T = get_T x in
   837     if exists (type_instance ctxt T o get_T) xs then xs
   838     else x :: filter_out (type_generalization ctxt T o get_T) xs
   839   end
   840 
   841 (* The Booleans indicate whether all type arguments should be kept. *)
   842 datatype type_arg_policy =
   843   Explicit_Type_Args of bool (* infer_from_term_args *) |
   844   Mangled_Type_Args |
   845   No_Type_Args
   846 
   847 fun type_arg_policy monom_constrs type_enc s =
   848   let val poly = polymorphism_of_type_enc type_enc in
   849     if s = type_tag_name then
   850       if poly = Mangled_Monomorphic then Mangled_Type_Args
   851       else Explicit_Type_Args false
   852     else case type_enc of
   853       Simple_Types (_, Polymorphic, _) => Explicit_Type_Args false
   854     | Tags (_, All_Types) => No_Type_Args
   855     | _ =>
   856       let val level = level_of_type_enc type_enc in
   857         if level = No_Types orelse s = @{const_name HOL.eq} orelse
   858            (s = app_op_name andalso level = Const_Arg_Types) then
   859           No_Type_Args
   860         else if poly = Mangled_Monomorphic then
   861           Mangled_Type_Args
   862         else if member (op =) monom_constrs s andalso
   863                 granularity_of_type_level level = Positively_Naked_Vars then
   864           No_Type_Args
   865         else
   866           Explicit_Type_Args
   867               (level = All_Types orelse
   868                granularity_of_type_level level = Ghost_Type_Arg_Vars)
   869       end
   870   end
   871 
   872 (* Make atoms for sorted type variables. *)
   873 fun generic_add_sorts_on_type (_, []) = I
   874   | generic_add_sorts_on_type ((x, i), s :: ss) =
   875     generic_add_sorts_on_type ((x, i), ss)
   876     #> (if s = the_single @{sort HOL.type} then
   877           I
   878         else if i = ~1 then
   879           insert (op =) (`make_type_class s, `make_fixed_type_var x)
   880         else
   881           insert (op =) (`make_type_class s,
   882                          (make_schematic_type_var (x, i), x)))
   883 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
   884   | add_sorts_on_tfree _ = I
   885 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
   886   | add_sorts_on_tvar _ = I
   887 
   888 fun type_class_formula type_enc class arg =
   889   AAtom (ATerm (class, arg ::
   890       (case type_enc of
   891          Simple_Types (First_Order, Polymorphic, _) =>
   892          if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
   893          else []
   894        | _ => [])))
   895 fun formulas_for_types type_enc add_sorts_on_typ Ts =
   896   [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
   897      |> map (fn (class, name) =>
   898                 type_class_formula type_enc class (ATerm (name, [])))
   899 
   900 fun mk_aconns c phis =
   901   let val (phis', phi') = split_last phis in
   902     fold_rev (mk_aconn c) phis' phi'
   903   end
   904 fun mk_ahorn [] phi = phi
   905   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
   906 fun mk_aquant _ [] phi = phi
   907   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
   908     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
   909   | mk_aquant q xs phi = AQuant (q, xs, phi)
   910 
   911 fun close_universally add_term_vars phi =
   912   let
   913     fun add_formula_vars bounds (AQuant (_, xs, phi)) =
   914         add_formula_vars (map fst xs @ bounds) phi
   915       | add_formula_vars bounds (AConn (_, phis)) =
   916         fold (add_formula_vars bounds) phis
   917       | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
   918   in mk_aquant AForall (add_formula_vars [] phi []) phi end
   919 
   920 fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
   921     (if is_tptp_variable s andalso
   922         not (String.isPrefix tvar_prefix s) andalso
   923         not (member (op =) bounds name) then
   924        insert (op =) (name, NONE)
   925      else
   926        I)
   927     #> fold (add_term_vars bounds) tms
   928   | add_term_vars bounds (AAbs ((name, _), tm)) =
   929     add_term_vars (name :: bounds) tm
   930 fun close_formula_universally phi = close_universally add_term_vars phi
   931 
   932 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
   933     fold (add_iterm_vars bounds) [tm1, tm2]
   934   | add_iterm_vars _ (IConst _) = I
   935   | add_iterm_vars bounds (IVar (name, T)) =
   936     not (member (op =) bounds name) ? insert (op =) (name, SOME T)
   937   | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
   938 fun close_iformula_universally phi = close_universally add_iterm_vars phi
   939 
   940 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
   941 val fused_infinite_type = Type (fused_infinite_type_name, [])
   942 
   943 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
   944 
   945 fun ho_term_from_typ format type_enc =
   946   let
   947     fun term (Type (s, Ts)) =
   948       ATerm (case (is_type_enc_higher_order type_enc, s) of
   949                (true, @{type_name bool}) => `I tptp_bool_type
   950              | (true, @{type_name fun}) => `I tptp_fun_type
   951              | _ => if s = fused_infinite_type_name andalso
   952                        is_format_typed format then
   953                       `I tptp_individual_type
   954                     else
   955                       `make_fixed_type_const s,
   956              map term Ts)
   957     | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
   958     | term (TVar (x, _)) = ATerm (tvar_name x, [])
   959   in term end
   960 
   961 fun ho_term_for_type_arg format type_enc T =
   962   if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
   963 
   964 (* This shouldn't clash with anything else. *)
   965 val uncurried_alias_sep = "\000"
   966 val mangled_type_sep = "\001"
   967 
   968 val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
   969 
   970 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   971   | generic_mangled_type_name f (ATerm (name, tys)) =
   972     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
   973     ^ ")"
   974   | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
   975 
   976 fun mangled_type format type_enc =
   977   generic_mangled_type_name fst o ho_term_from_typ format type_enc
   978 
   979 fun make_native_type s =
   980   if s = tptp_bool_type orelse s = tptp_fun_type orelse
   981      s = tptp_individual_type then
   982     s
   983   else
   984     native_type_prefix ^ ascii_of s
   985 
   986 fun ho_type_from_ho_term type_enc pred_sym ary =
   987   let
   988     fun to_mangled_atype ty =
   989       AType ((make_native_type (generic_mangled_type_name fst ty),
   990               generic_mangled_type_name snd ty), [])
   991     fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
   992       | to_poly_atype _ = raise Fail "unexpected type abstraction"
   993     val to_atype =
   994       if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
   995       else to_mangled_atype
   996     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
   997     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
   998       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
   999       | to_fo _ _ = raise Fail "unexpected type abstraction"
  1000     fun to_ho (ty as ATerm ((s, _), tys)) =
  1001         if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
  1002       | to_ho _ = raise Fail "unexpected type abstraction"
  1003   in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
  1004 
  1005 fun ho_type_from_typ format type_enc pred_sym ary =
  1006   ho_type_from_ho_term type_enc pred_sym ary
  1007   o ho_term_from_typ format type_enc
  1008 
  1009 fun aliased_uncurried ary (s, s') =
  1010   (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
  1011 fun unaliased_uncurried (s, s') =
  1012   case space_explode uncurried_alias_sep s of
  1013     [_] => (s, s')
  1014   | [s1, s2] => (s1, unsuffix s2 s')
  1015   | _ => raise Fail "ill-formed explicit application alias"
  1016 
  1017 fun raw_mangled_const_name type_name ty_args (s, s') =
  1018   let
  1019     fun type_suffix f g =
  1020       fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
  1021                ty_args ""
  1022   in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
  1023 fun mangled_const_name format type_enc =
  1024   map_filter (ho_term_for_type_arg format type_enc)
  1025   #> raw_mangled_const_name generic_mangled_type_name
  1026 
  1027 val parse_mangled_ident =
  1028   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
  1029 
  1030 fun parse_mangled_type x =
  1031   (parse_mangled_ident
  1032    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
  1033                     [] >> ATerm) x
  1034 and parse_mangled_types x =
  1035   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
  1036 
  1037 fun unmangled_type s =
  1038   s |> suffix ")" |> raw_explode
  1039     |> Scan.finite Symbol.stopper
  1040            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
  1041                                                 quote s)) parse_mangled_type))
  1042     |> fst
  1043 
  1044 fun unmangled_const_name s =
  1045   (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
  1046 fun unmangled_const s =
  1047   let val ss = unmangled_const_name s in
  1048     (hd ss, map unmangled_type (tl ss))
  1049   end
  1050 
  1051 fun introduce_proxies_in_iterm type_enc =
  1052   let
  1053     fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
  1054       | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
  1055                        _ =
  1056         (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
  1057            limitation. This works in conjuction with special code in
  1058            "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
  1059            possible. *)
  1060         IAbs ((`I "P", p_T),
  1061               IApp (IConst (`I ho_quant, T, []),
  1062                     IAbs ((`I "X", x_T),
  1063                           IApp (IConst (`I "P", p_T, []),
  1064                                 IConst (`I "X", x_T, [])))))
  1065       | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
  1066     fun intro top_level args (IApp (tm1, tm2)) =
  1067         IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
  1068       | intro top_level args (IConst (name as (s, _), T, T_args)) =
  1069         (case proxify_const s of
  1070            SOME proxy_base =>
  1071            if top_level orelse is_type_enc_higher_order type_enc then
  1072              case (top_level, s) of
  1073                (_, "c_False") => IConst (`I tptp_false, T, [])
  1074              | (_, "c_True") => IConst (`I tptp_true, T, [])
  1075              | (false, "c_Not") => IConst (`I tptp_not, T, [])
  1076              | (false, "c_conj") => IConst (`I tptp_and, T, [])
  1077              | (false, "c_disj") => IConst (`I tptp_or, T, [])
  1078              | (false, "c_implies") => IConst (`I tptp_implies, T, [])
  1079              | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
  1080              | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
  1081              | (false, s) =>
  1082                if is_tptp_equal s andalso length args = 2 then
  1083                  IConst (`I tptp_equal, T, [])
  1084                else
  1085                  (* Use a proxy even for partially applied THF0 equality,
  1086                     because the LEO-II and Satallax parsers complain about not
  1087                     being able to infer the type of "=". *)
  1088                  IConst (proxy_base |>> prefix const_prefix, T, T_args)
  1089              | _ => IConst (name, T, [])
  1090            else
  1091              IConst (proxy_base |>> prefix const_prefix, T, T_args)
  1092           | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
  1093                     else IConst (name, T, T_args))
  1094       | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
  1095       | intro _ _ tm = tm
  1096   in intro true [] end
  1097 
  1098 fun mangle_type_args_in_const format type_enc (name as (s, _)) T_args =
  1099   case unprefix_and_unascii const_prefix s of
  1100     NONE => (name, T_args)
  1101   | SOME s'' =>
  1102     case type_arg_policy [] type_enc (invert_const s'') of
  1103       Mangled_Type_Args => (mangled_const_name format type_enc T_args name, [])
  1104     | _ => (name, T_args)
  1105 fun mangle_type_args_in_iterm format type_enc =
  1106   if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
  1107     let
  1108       fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
  1109         | mangle (tm as IConst (_, _, [])) = tm
  1110         | mangle (IConst (name, T, T_args)) =
  1111           mangle_type_args_in_const format type_enc name T_args
  1112           |> (fn (name, T_args) => IConst (name, T, T_args))
  1113         | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
  1114         | mangle tm = tm
  1115     in mangle end
  1116   else
  1117     I
  1118 
  1119 fun chop_fun 0 T = ([], T)
  1120   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
  1121     chop_fun (n - 1) ran_T |>> cons dom_T
  1122   | chop_fun _ T = ([], T)
  1123 
  1124 fun filter_const_type_args _ _ _ [] = []
  1125   | filter_const_type_args thy s ary T_args =
  1126     let
  1127       val U = robust_const_type thy s
  1128       val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
  1129       val U_args = (s, U) |> robust_const_typargs thy
  1130     in
  1131       U_args ~~ T_args
  1132       |> map (fn (U, T) =>
  1133                  if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
  1134     end
  1135     handle TYPE _ => T_args
  1136 
  1137 fun filter_type_args_in_const _ _ _ _ _ [] = []
  1138   | filter_type_args_in_const thy monom_constrs type_enc ary s T_args =
  1139     case unprefix_and_unascii const_prefix s of
  1140       NONE =>
  1141       if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
  1142       else T_args
  1143     | SOME s'' =>
  1144       let
  1145         val s'' = invert_const s''
  1146         fun filter_T_args false = T_args
  1147           | filter_T_args true = filter_const_type_args thy s'' ary T_args
  1148       in
  1149         case type_arg_policy monom_constrs type_enc s'' of
  1150           Explicit_Type_Args infer_from_term_args =>
  1151           filter_T_args infer_from_term_args
  1152         | No_Type_Args => []
  1153         | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
  1154       end
  1155 fun filter_type_args_in_iterm thy monom_constrs type_enc =
  1156   let
  1157     fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
  1158       | filt ary (IConst (name as (s, _), T, T_args)) =
  1159         filter_type_args_in_const thy monom_constrs type_enc ary s T_args
  1160         |> (fn T_args => IConst (name, T, T_args))
  1161       | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
  1162       | filt _ tm = tm
  1163   in filt 0 end
  1164 
  1165 fun iformula_from_prop ctxt format type_enc eq_as_iff =
  1166   let
  1167     val thy = Proof_Context.theory_of ctxt
  1168     fun do_term bs t atomic_Ts =
  1169       iterm_from_term thy format bs (Envir.eta_contract t)
  1170       |>> (introduce_proxies_in_iterm type_enc
  1171            #> mangle_type_args_in_iterm format type_enc #> AAtom)
  1172       ||> union (op =) atomic_Ts
  1173     fun do_quant bs q pos s T t' =
  1174       let
  1175         val s = singleton (Name.variant_list (map fst bs)) s
  1176         val universal = Option.map (q = AExists ? not) pos
  1177         val name =
  1178           s |> `(case universal of
  1179                    SOME true => make_all_bound_var
  1180                  | SOME false => make_exist_bound_var
  1181                  | NONE => make_bound_var)
  1182       in
  1183         do_formula ((s, (name, T)) :: bs) pos t'
  1184         #>> mk_aquant q [(name, SOME T)]
  1185         ##> union (op =) (atomic_types_of T)
  1186       end
  1187     and do_conn bs c pos1 t1 pos2 t2 =
  1188       do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
  1189     and do_formula bs pos t =
  1190       case t of
  1191         @{const Trueprop} $ t1 => do_formula bs pos t1
  1192       | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
  1193       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
  1194         do_quant bs AForall pos s T t'
  1195       | (t0 as Const (@{const_name All}, _)) $ t1 =>
  1196         do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
  1197       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
  1198         do_quant bs AExists pos s T t'
  1199       | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
  1200         do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
  1201       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
  1202       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
  1203       | @{const HOL.implies} $ t1 $ t2 =>
  1204         do_conn bs AImplies (Option.map not pos) t1 pos t2
  1205       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
  1206         if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
  1207       | _ => do_term bs t
  1208   in do_formula [] end
  1209 
  1210 fun presimplify_term ctxt t =
  1211   t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
  1212        ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
  1213           #> Meson.presimplify
  1214           #> prop_of)
  1215 
  1216 fun is_fun_equality (@{const_name HOL.eq},
  1217                      Type (_, [Type (@{type_name fun}, _), _])) = true
  1218   | is_fun_equality _ = false
  1219 
  1220 fun extensionalize_term ctxt t =
  1221   if exists_Const is_fun_equality t then
  1222     let val thy = Proof_Context.theory_of ctxt in
  1223       t |> cterm_of thy |> Meson.extensionalize_conv ctxt
  1224         |> prop_of |> Logic.dest_equals |> snd
  1225     end
  1226   else
  1227     t
  1228 
  1229 fun preprocess_abstractions_in_terms trans_lams facts =
  1230   let
  1231     val (facts, lambda_ts) =
  1232       facts |> map (snd o snd) |> trans_lams
  1233             |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
  1234     val lam_facts =
  1235       map2 (fn t => fn j =>
  1236                ((lam_fact_prefix ^ Int.toString j, (Global, Spec_Eq)),
  1237                 (Axiom, t)))
  1238            lambda_ts (1 upto length lambda_ts)
  1239   in (facts, lam_facts) end
  1240 
  1241 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
  1242    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
  1243 fun freeze_term t =
  1244   let
  1245     fun freeze (t $ u) = freeze t $ freeze u
  1246       | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
  1247       | freeze (Var ((s, i), T)) =
  1248         Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
  1249       | freeze t = t
  1250   in t |> exists_subterm is_Var t ? freeze end
  1251 
  1252 fun default_formula role = if role = Conjecture then @{term False} else @{term True}
  1253 
  1254 fun presimp_prop ctxt role t =
  1255   (let
  1256      val thy = Proof_Context.theory_of ctxt
  1257      val t = t |> Envir.beta_eta_contract
  1258                |> transform_elim_prop
  1259                |> Object_Logic.atomize_term thy
  1260      val need_trueprop = (fastype_of t = @{typ bool})
  1261    in
  1262      t |> need_trueprop ? HOLogic.mk_Trueprop
  1263        |> extensionalize_term ctxt
  1264        |> presimplify_term ctxt
  1265        |> HOLogic.dest_Trueprop
  1266    end
  1267    handle TERM _ => default_formula role)
  1268   |> pair role
  1269 
  1270 fun make_formula ctxt format type_enc eq_as_iff name stature kind t =
  1271   let
  1272     val (iformula, atomic_Ts) =
  1273       iformula_from_prop ctxt format type_enc eq_as_iff
  1274                          (SOME (kind <> Conjecture)) t []
  1275       |>> close_iformula_universally
  1276   in
  1277     {name = name, stature = stature, kind = kind, iformula = iformula,
  1278      atomic_types = atomic_Ts}
  1279   end
  1280 
  1281 fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
  1282   case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
  1283                          name stature Axiom of
  1284     formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
  1285     if s = tptp_true then NONE else SOME formula
  1286   | formula => SOME formula
  1287 
  1288 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
  1289   | s_not_trueprop t =
  1290     if fastype_of t = @{typ bool} then s_not t
  1291     else @{prop False} (* "t" is too meta *)
  1292 
  1293 fun make_conjecture ctxt format type_enc =
  1294   map (fn ((name, stature), (kind, t)) =>
  1295           t |> kind = Conjecture ? s_not_trueprop
  1296             |> make_formula ctxt format type_enc (format <> CNF) name stature
  1297                             kind)
  1298 
  1299 (** Finite and infinite type inference **)
  1300 
  1301 fun tvar_footprint thy s ary =
  1302   (case unprefix_and_unascii const_prefix s of
  1303      SOME s =>
  1304      s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
  1305        |> map (fn T => Term.add_tvarsT T [] |> map fst)
  1306    | NONE => [])
  1307   handle TYPE _ => []
  1308 
  1309 fun ghost_type_args thy s ary =
  1310   if is_tptp_equal s then
  1311     0 upto ary - 1
  1312   else
  1313     let
  1314       val footprint = tvar_footprint thy s ary
  1315       val eq = (s = @{const_name HOL.eq})
  1316       fun ghosts _ [] = []
  1317         | ghosts seen ((i, tvars) :: args) =
  1318           ghosts (union (op =) seen tvars) args
  1319           |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
  1320              ? cons i
  1321     in
  1322       if forall null footprint then
  1323         []
  1324       else
  1325         0 upto length footprint - 1 ~~ footprint
  1326         |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
  1327         |> ghosts []
  1328     end
  1329 
  1330 type monotonicity_info =
  1331   {maybe_finite_Ts : typ list,
  1332    surely_finite_Ts : typ list,
  1333    maybe_infinite_Ts : typ list,
  1334    surely_infinite_Ts : typ list,
  1335    maybe_nonmono_Ts : typ list}
  1336 
  1337 (* These types witness that the type classes they belong to allow infinite
  1338    models and hence that any types with these type classes is monotonic. *)
  1339 val known_infinite_types =
  1340   [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
  1341 
  1342 fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
  1343   strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
  1344 
  1345 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
  1346    dangerous because their "exhaust" properties can easily lead to unsound ATP
  1347    proofs. On the other hand, all HOL infinite types can be given the same
  1348    models in first-order logic (via Löwenheim-Skolem). *)
  1349 
  1350 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
  1351   | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
  1352                              maybe_nonmono_Ts, ...}
  1353                        (Noninf_Nonmono_Types (strictness, grain)) T =
  1354     grain = Ghost_Type_Arg_Vars orelse
  1355     (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  1356      not (exists (type_instance ctxt T) surely_infinite_Ts orelse
  1357           (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
  1358            is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
  1359                                            T)))
  1360   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
  1361                              maybe_nonmono_Ts, ...}
  1362                        (Fin_Nonmono_Types grain) T =
  1363     grain = Ghost_Type_Arg_Vars orelse
  1364     (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  1365      (exists (type_generalization ctxt T) surely_finite_Ts orelse
  1366       (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
  1367        is_type_surely_finite ctxt T)))
  1368   | should_encode_type _ _ _ _ = false
  1369 
  1370 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
  1371     should_guard_var () andalso should_encode_type ctxt mono level T
  1372   | should_guard_type _ _ _ _ _ = false
  1373 
  1374 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
  1375     String.isPrefix bound_var_prefix s orelse
  1376     String.isPrefix all_bound_var_prefix s
  1377   | is_maybe_universal_var (IVar _) = true
  1378   | is_maybe_universal_var _ = false
  1379 
  1380 datatype site =
  1381   Top_Level of bool option |
  1382   Eq_Arg of bool option |
  1383   Elsewhere
  1384 
  1385 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
  1386   | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
  1387     if granularity_of_type_level level = All_Vars then
  1388       should_encode_type ctxt mono level T
  1389     else
  1390       (case (site, is_maybe_universal_var u) of
  1391          (Eq_Arg _, true) => should_encode_type ctxt mono level T
  1392        | _ => false)
  1393   | should_tag_with_type _ _ _ _ _ _ = false
  1394 
  1395 fun fused_type ctxt mono level =
  1396   let
  1397     val should_encode = should_encode_type ctxt mono level
  1398     fun fuse 0 T = if should_encode T then T else fused_infinite_type
  1399       | fuse ary (Type (@{type_name fun}, [T1, T2])) =
  1400         fuse 0 T1 --> fuse (ary - 1) T2
  1401       | fuse _ _ = raise Fail "expected function type"
  1402   in fuse end
  1403 
  1404 (** predicators and application operators **)
  1405 
  1406 type sym_info =
  1407   {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
  1408    in_conj : bool}
  1409 
  1410 fun default_sym_tab_entries type_enc =
  1411   (make_fixed_const NONE @{const_name undefined},
  1412        {pred_sym = false, min_ary = 0, max_ary = 0, types = [],
  1413         in_conj = false}) ::
  1414   ([tptp_false, tptp_true]
  1415    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [],
  1416                   in_conj = false})) @
  1417   ([tptp_equal, tptp_old_equal]
  1418    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [],
  1419                   in_conj = false}))
  1420   |> not (is_type_enc_higher_order type_enc)
  1421      ? cons (prefixed_predicator_name,
  1422              {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
  1423               in_conj = false})
  1424 
  1425 datatype app_op_level = Incomplete_Apply | Sufficient_Apply | Full_Apply
  1426 
  1427 fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
  1428   let
  1429     val thy = Proof_Context.theory_of ctxt
  1430     fun consider_var_ary const_T var_T max_ary =
  1431       let
  1432         fun iter ary T =
  1433           if ary = max_ary orelse type_instance ctxt var_T T orelse
  1434              type_instance ctxt T var_T then
  1435             ary
  1436           else
  1437             iter (ary + 1) (range_type T)
  1438       in iter 0 const_T end
  1439     fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1440       if app_op_level = Sufficient_Apply andalso
  1441          (can dest_funT T orelse T = @{typ bool}) then
  1442         let
  1443           val bool_vars' = bool_vars orelse body_type T = @{typ bool}
  1444           fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
  1445             {pred_sym = pred_sym andalso not bool_vars',
  1446              min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
  1447              max_ary = max_ary, types = types, in_conj = in_conj}
  1448           val fun_var_Ts' =
  1449             fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
  1450         in
  1451           if bool_vars' = bool_vars andalso
  1452              pointer_eq (fun_var_Ts', fun_var_Ts) then
  1453             accum
  1454           else
  1455             ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
  1456         end
  1457       else
  1458         accum
  1459       fun add_iterm_syms conj_fact top_level tm
  1460                          (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1461         let val (head, args) = strip_iterm_comb tm in
  1462           (case head of
  1463              IConst ((s, _), T, _) =>
  1464              if String.isPrefix bound_var_prefix s orelse
  1465                 String.isPrefix all_bound_var_prefix s then
  1466                add_universal_var T accum
  1467              else if String.isPrefix exist_bound_var_prefix s then
  1468                accum
  1469              else
  1470                let val ary = length args in
  1471                  ((bool_vars, fun_var_Ts),
  1472                   case Symtab.lookup sym_tab s of
  1473                     SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
  1474                     let
  1475                       val pred_sym =
  1476                         pred_sym andalso top_level andalso not bool_vars
  1477                       val types' = types |> insert_type ctxt I T
  1478                       val in_conj = in_conj orelse conj_fact
  1479                       val min_ary =
  1480                         if app_op_level = Sufficient_Apply andalso
  1481                            not (pointer_eq (types', types)) then
  1482                           fold (consider_var_ary T) fun_var_Ts min_ary
  1483                         else
  1484                           min_ary
  1485                     in
  1486                       Symtab.update (s, {pred_sym = pred_sym,
  1487                                          min_ary = Int.min (ary, min_ary),
  1488                                          max_ary = Int.max (ary, max_ary),
  1489                                          types = types', in_conj = in_conj})
  1490                                     sym_tab
  1491                     end
  1492                   | NONE =>
  1493                     let
  1494                       val pred_sym = top_level andalso not bool_vars
  1495                       val ary =
  1496                         case unprefix_and_unascii const_prefix s of
  1497                           SOME s =>
  1498                           (if String.isSubstring uncurried_alias_sep s then
  1499                              ary
  1500                            else case try (robust_const_ary thy
  1501                                           o invert_const o hd
  1502                                           o unmangled_const_name) s of
  1503                              SOME ary0 => Int.min (ary0, ary)
  1504                            | NONE => ary)
  1505                         | NONE => ary
  1506                       val min_ary =
  1507                         case app_op_level of
  1508                           Incomplete_Apply => ary
  1509                         | Sufficient_Apply =>
  1510                           fold (consider_var_ary T) fun_var_Ts ary
  1511                         | Full_Apply => 0
  1512                     in
  1513                       Symtab.update_new (s,
  1514                           {pred_sym = pred_sym, min_ary = min_ary,
  1515                            max_ary = ary, types = [T], in_conj = conj_fact})
  1516                           sym_tab
  1517                     end)
  1518                end
  1519            | IVar (_, T) => add_universal_var T accum
  1520            | IAbs ((_, T), tm) =>
  1521              accum |> add_universal_var T |> add_iterm_syms conj_fact false tm
  1522            | _ => accum)
  1523           |> fold (add_iterm_syms conj_fact false) args
  1524         end
  1525     fun add_fact_syms conj_fact =
  1526       K (add_iterm_syms conj_fact true) |> formula_fold NONE |> fact_lift
  1527   in
  1528     ((false, []), Symtab.empty)
  1529     |> fold (add_fact_syms true) conjs
  1530     |> fold (add_fact_syms false) facts
  1531     |> snd
  1532     |> fold Symtab.update (default_sym_tab_entries type_enc)
  1533   end
  1534 
  1535 fun min_ary_of sym_tab s =
  1536   case Symtab.lookup sym_tab s of
  1537     SOME ({min_ary, ...} : sym_info) => min_ary
  1538   | NONE =>
  1539     case unprefix_and_unascii const_prefix s of
  1540       SOME s =>
  1541       let val s = s |> unmangled_const_name |> hd |> invert_const in
  1542         if s = predicator_name then 1
  1543         else if s = app_op_name then 2
  1544         else if s = type_guard_name then 1
  1545         else 0
  1546       end
  1547     | NONE => 0
  1548 
  1549 (* True if the constant ever appears outside of the top-level position in
  1550    literals, or if it appears with different arities (e.g., because of different
  1551    type instantiations). If false, the constant always receives all of its
  1552    arguments and is used as a predicate. *)
  1553 fun is_pred_sym sym_tab s =
  1554   case Symtab.lookup sym_tab s of
  1555     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
  1556     pred_sym andalso min_ary = max_ary
  1557   | NONE => false
  1558 
  1559 val app_op = `(make_fixed_const NONE) app_op_name
  1560 val predicator_combconst =
  1561   IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
  1562 
  1563 fun list_app head args = fold (curry (IApp o swap)) args head
  1564 fun predicator tm = IApp (predicator_combconst, tm)
  1565 
  1566 fun mk_app_op format type_enc head arg =
  1567   let
  1568     val head_T = ityp_of head
  1569     val (arg_T, res_T) = dest_funT head_T
  1570     val app =
  1571       IConst (app_op, head_T --> head_T, [arg_T, res_T])
  1572       |> mangle_type_args_in_iterm format type_enc
  1573   in list_app app [head, arg] end
  1574 
  1575 fun firstorderize_fact thy monom_constrs format type_enc sym_tab
  1576                        uncurried_aliases =
  1577   let
  1578     fun do_app arg head = mk_app_op format type_enc head arg
  1579     fun list_app_ops head args = fold do_app args head
  1580     fun introduce_app_ops tm =
  1581       let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
  1582         case head of
  1583           IConst (name as (s, _), T, T_args) =>
  1584           if uncurried_aliases andalso String.isPrefix const_prefix s then
  1585             let
  1586               val ary = length args
  1587               val name =
  1588                 name |> ary > min_ary_of sym_tab s ? aliased_uncurried ary
  1589             in list_app (IConst (name, T, T_args)) args end
  1590           else
  1591             args |> chop (min_ary_of sym_tab s)
  1592                  |>> list_app head |-> list_app_ops
  1593         | _ => list_app_ops head args
  1594       end
  1595     fun introduce_predicators tm =
  1596       case strip_iterm_comb tm of
  1597         (IConst ((s, _), _, _), _) =>
  1598         if is_pred_sym sym_tab s then tm else predicator tm
  1599       | _ => predicator tm
  1600     val do_iterm =
  1601       not (is_type_enc_higher_order type_enc)
  1602       ? (introduce_app_ops #> introduce_predicators)
  1603       #> filter_type_args_in_iterm thy monom_constrs type_enc
  1604   in update_iformula (formula_map do_iterm) end
  1605 
  1606 (** Helper facts **)
  1607 
  1608 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
  1609 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
  1610 
  1611 (* The Boolean indicates that a fairly sound type encoding is needed. *)
  1612 val helper_table =
  1613   [(("COMBI", false), @{thms Meson.COMBI_def}),
  1614    (("COMBK", false), @{thms Meson.COMBK_def}),
  1615    (("COMBB", false), @{thms Meson.COMBB_def}),
  1616    (("COMBC", false), @{thms Meson.COMBC_def}),
  1617    (("COMBS", false), @{thms Meson.COMBS_def}),
  1618    ((predicator_name, false), [not_ffalse, ftrue]),
  1619    (("fFalse", false), [not_ffalse]),
  1620    (("fFalse", true), @{thms True_or_False}),
  1621    (("fTrue", false), [ftrue]),
  1622    (("fTrue", true), @{thms True_or_False}),
  1623    (("fNot", false),
  1624     @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1625            fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
  1626    (("fconj", false),
  1627     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
  1628         by (unfold fconj_def) fast+}),
  1629    (("fdisj", false),
  1630     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
  1631         by (unfold fdisj_def) fast+}),
  1632    (("fimplies", false),
  1633     @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
  1634         by (unfold fimplies_def) fast+}),
  1635    (("fequal", true),
  1636     (* This is a lie: Higher-order equality doesn't need a sound type encoding.
  1637        However, this is done so for backward compatibility: Including the
  1638        equality helpers by default in Metis breaks a few existing proofs. *)
  1639     @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1640            fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
  1641    (* Partial characterization of "fAll" and "fEx". A complete characterization
  1642       would require the axiom of choice for replay with Metis. *)
  1643    (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
  1644    (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
  1645    (("If", true), @{thms if_True if_False True_or_False})]
  1646   |> map (apsnd (map zero_var_indexes))
  1647 
  1648 fun atype_of_type_vars (Simple_Types (_, Polymorphic, _)) = SOME atype_of_types
  1649   | atype_of_type_vars _ = NONE
  1650 
  1651 fun bound_tvars type_enc sorts Ts =
  1652   (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
  1653   #> mk_aquant AForall
  1654         (map_filter (fn TVar (x as (s, _), _) =>
  1655                         SOME ((make_schematic_type_var x, s),
  1656                               atype_of_type_vars type_enc)
  1657                       | _ => NONE) Ts)
  1658 
  1659 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
  1660   (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
  1661    else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
  1662   |> mk_aquant AForall bounds
  1663   |> close_formula_universally
  1664   |> bound_tvars type_enc true atomic_Ts
  1665 
  1666 val helper_rank = default_rank
  1667 val min_rank = 9 * helper_rank div 10
  1668 val max_rank = 4 * min_rank
  1669 
  1670 fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n
  1671 
  1672 val type_tag = `(make_fixed_const NONE) type_tag_name
  1673 
  1674 fun type_tag_idempotence_fact format type_enc =
  1675   let
  1676     fun var s = ATerm (`I s, [])
  1677     fun tag tm = ATerm (type_tag, [var "A", tm])
  1678     val tagged_var = tag (var "X")
  1679   in
  1680     Formula (type_tag_idempotence_helper_name, Axiom,
  1681              eq_formula type_enc [] [] false (tag tagged_var) tagged_var,
  1682              NONE, isabelle_info format spec_eqN helper_rank)
  1683   end
  1684 
  1685 fun should_specialize_helper type_enc t =
  1686   polymorphism_of_type_enc type_enc <> Polymorphic andalso
  1687   level_of_type_enc type_enc <> No_Types andalso
  1688   not (null (Term.hidden_polymorphism t))
  1689 
  1690 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
  1691   case unprefix_and_unascii const_prefix s of
  1692     SOME mangled_s =>
  1693     let
  1694       val thy = Proof_Context.theory_of ctxt
  1695       val unmangled_s = mangled_s |> unmangled_const_name |> hd
  1696       fun dub needs_fairly_sound j k =
  1697         unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
  1698         (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
  1699         (if needs_fairly_sound then typed_helper_suffix
  1700          else untyped_helper_suffix)
  1701       fun dub_and_inst needs_fairly_sound (th, j) =
  1702         let val t = prop_of th in
  1703           if should_specialize_helper type_enc t then
  1704             map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
  1705                 types
  1706           else
  1707             [t]
  1708         end
  1709         |> tag_list 1
  1710         |> map (fn (k, t) =>
  1711                    ((dub needs_fairly_sound j k, (Global, Spec_Eq)), t))
  1712       val make_facts = map_filter (make_fact ctxt format type_enc false)
  1713       val fairly_sound = is_type_enc_fairly_sound type_enc
  1714     in
  1715       helper_table
  1716       |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
  1717                   if helper_s <> unmangled_s orelse
  1718                      (needs_fairly_sound andalso not fairly_sound) then
  1719                     []
  1720                   else
  1721                     ths ~~ (1 upto length ths)
  1722                     |> maps (dub_and_inst needs_fairly_sound)
  1723                     |> make_facts)
  1724     end
  1725   | NONE => []
  1726 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
  1727   Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
  1728                   []
  1729 
  1730 (***************************************************************)
  1731 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
  1732 (***************************************************************)
  1733 
  1734 fun set_insert (x, s) = Symtab.update (x, ()) s
  1735 
  1736 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
  1737 
  1738 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
  1739 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
  1740 
  1741 fun classes_of_terms get_Ts =
  1742   map (map snd o get_Ts)
  1743   #> List.foldl add_classes Symtab.empty
  1744   #> delete_type #> Symtab.keys
  1745 
  1746 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
  1747 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
  1748 
  1749 fun fold_type_constrs f (Type (s, Ts)) x =
  1750     fold (fold_type_constrs f) Ts (f (s, x))
  1751   | fold_type_constrs _ _ x = x
  1752 
  1753 (* Type constructors used to instantiate overloaded constants are the only ones
  1754    needed. *)
  1755 fun add_type_constrs_in_term thy =
  1756   let
  1757     fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
  1758       | add (t $ u) = add t #> add u
  1759       | add (Const x) =
  1760         x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
  1761       | add (Abs (_, _, u)) = add u
  1762       | add _ = I
  1763   in add end
  1764 
  1765 fun type_constrs_of_terms thy ts =
  1766   Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
  1767 
  1768 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
  1769     let val (head, args) = strip_comb t in
  1770       (head |> dest_Const |> fst,
  1771        fold_rev (fn t as Var ((s, _), T) =>
  1772                     (fn u => Abs (s, T, abstract_over (t, u)))
  1773                   | _ => raise Fail "expected Var") args u)
  1774     end
  1775   | extract_lambda_def _ = raise Fail "malformed lifted lambda"
  1776 
  1777 fun trans_lams_from_string ctxt type_enc lam_trans =
  1778   if lam_trans = no_lamsN then
  1779     rpair []
  1780   else if lam_trans = hide_lamsN then
  1781     lift_lams ctxt type_enc ##> K []
  1782   else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
  1783     lift_lams ctxt type_enc
  1784   else if lam_trans = combsN then
  1785     map (introduce_combinators ctxt) #> rpair []
  1786   else if lam_trans = combs_and_liftingN then
  1787     lift_lams_part_1 ctxt type_enc
  1788     ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
  1789     #> lift_lams_part_2 ctxt
  1790   else if lam_trans = combs_or_liftingN then
  1791     lift_lams_part_1 ctxt type_enc
  1792     ##> map (fn t => case head_of (strip_qnt_body @{const_name All} t) of
  1793                        @{term "op =::bool => bool => bool"} => t
  1794                      | _ => introduce_combinators ctxt (intentionalize_def t))
  1795     #> lift_lams_part_2 ctxt
  1796   else if lam_trans = keep_lamsN then
  1797     map (Envir.eta_contract) #> rpair []
  1798   else
  1799     error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
  1800 
  1801 fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
  1802                        concl_t facts =
  1803   let
  1804     val thy = Proof_Context.theory_of ctxt
  1805     val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
  1806     val fact_ts = facts |> map snd
  1807     (* Remove existing facts from the conjecture, as this can dramatically
  1808        boost an ATP's performance (for some reason). *)
  1809     val hyp_ts =
  1810       hyp_ts
  1811       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
  1812     val facts = facts |> map (apsnd (pair Axiom))
  1813     val conjs =
  1814       map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
  1815       |> map (apsnd freeze_term)
  1816       |> map2 (pair o rpair (Local, General) o string_of_int)
  1817               (0 upto length hyp_ts)
  1818     val ((conjs, facts), lam_facts) =
  1819       (conjs, facts)
  1820       |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
  1821       |> (if lam_trans = no_lamsN then
  1822             rpair []
  1823           else
  1824             op @
  1825             #> preprocess_abstractions_in_terms trans_lams
  1826             #>> chop (length conjs))
  1827     val conjs = conjs |> make_conjecture ctxt format type_enc
  1828     val (fact_names, facts) =
  1829       facts
  1830       |> map_filter (fn (name, (_, t)) =>
  1831                         make_fact ctxt format type_enc true (name, t)
  1832                         |> Option.map (pair name))
  1833       |> ListPair.unzip
  1834     val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
  1835     val lam_facts =
  1836       lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
  1837     val all_ts = concl_t :: hyp_ts @ fact_ts
  1838     val subs = tfree_classes_of_terms all_ts
  1839     val supers = tvar_classes_of_terms all_ts
  1840     val tycons = type_constrs_of_terms thy all_ts
  1841     val (supers, arity_clauses) =
  1842       if level_of_type_enc type_enc = No_Types then ([], [])
  1843       else make_arity_clauses thy tycons supers
  1844     val class_rel_clauses = make_class_rel_clauses thy subs supers
  1845   in
  1846     (fact_names |> map single, union (op =) subs supers, conjs,
  1847      facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
  1848   end
  1849 
  1850 val type_guard = `(make_fixed_const NONE) type_guard_name
  1851 
  1852 fun type_guard_iterm format type_enc T tm =
  1853   IApp (IConst (type_guard, T --> @{typ bool}, [T])
  1854         |> mangle_type_args_in_iterm format type_enc, tm)
  1855 
  1856 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
  1857   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
  1858     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
  1859   | is_var_positively_naked_in_term _ _ _ _ = true
  1860 
  1861 fun is_var_ghost_type_arg_in_term thy polym_constrs name pos tm accum =
  1862   is_var_positively_naked_in_term name pos tm accum orelse
  1863   let
  1864     val var = ATerm (name, [])
  1865     fun is_nasty_in_term (ATerm (_, [])) = false
  1866       | is_nasty_in_term (ATerm ((s, _), tms)) =
  1867         let
  1868           val ary = length tms
  1869           val polym_constr = member (op =) polym_constrs s
  1870           val ghosts = ghost_type_args thy s ary
  1871         in
  1872           exists (fn (j, tm) =>
  1873                      if polym_constr then
  1874                        member (op =) ghosts j andalso
  1875                        (tm = var orelse is_nasty_in_term tm)
  1876                      else
  1877                        tm = var andalso member (op =) ghosts j)
  1878                  (0 upto ary - 1 ~~ tms)
  1879           orelse (not polym_constr andalso exists is_nasty_in_term tms)
  1880         end
  1881       | is_nasty_in_term _ = true
  1882   in is_nasty_in_term tm end
  1883 
  1884 fun should_guard_var_in_formula thy polym_constrs level pos phi (SOME true)
  1885                                 name =
  1886     (case granularity_of_type_level level of
  1887        All_Vars => true
  1888      | Positively_Naked_Vars =>
  1889        formula_fold pos (is_var_positively_naked_in_term name) phi false
  1890      | Ghost_Type_Arg_Vars =>
  1891        formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name) phi
  1892                     false)
  1893   | should_guard_var_in_formula _ _ _ _ _ _ _ = true
  1894 
  1895 fun always_guard_var_in_formula _ _ _ _ _ _ _ = true
  1896 
  1897 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
  1898   | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
  1899     granularity_of_type_level level <> All_Vars andalso
  1900     should_encode_type ctxt mono level T
  1901   | should_generate_tag_bound_decl _ _ _ _ _ = false
  1902 
  1903 fun mk_aterm format type_enc name T_args args =
  1904   ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
  1905 
  1906 fun do_bound_type ctxt format mono type_enc =
  1907   case type_enc of
  1908     Simple_Types (_, _, level) =>
  1909     fused_type ctxt mono level 0
  1910     #> ho_type_from_typ format type_enc false 0 #> SOME
  1911   | _ => K NONE
  1912 
  1913 fun tag_with_type ctxt format mono type_enc pos T tm =
  1914   IConst (type_tag, T --> T, [T])
  1915   |> mangle_type_args_in_iterm format type_enc
  1916   |> ho_term_from_iterm ctxt format mono type_enc pos
  1917   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
  1918        | _ => raise Fail "unexpected lambda-abstraction")
  1919 and ho_term_from_iterm ctxt format mono type_enc =
  1920   let
  1921     fun term site u =
  1922       let
  1923         val (head, args) = strip_iterm_comb u
  1924         val pos =
  1925           case site of
  1926             Top_Level pos => pos
  1927           | Eq_Arg pos => pos
  1928           | _ => NONE
  1929         val t =
  1930           case head of
  1931             IConst (name as (s, _), _, T_args) =>
  1932             let val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere in
  1933               map (term arg_site) args |> mk_aterm format type_enc name T_args
  1934             end
  1935           | IVar (name, _) =>
  1936             map (term Elsewhere) args |> mk_aterm format type_enc name []
  1937           | IAbs ((name, T), tm) =>
  1938             if is_type_enc_higher_order type_enc then
  1939               AAbs ((name, ho_type_from_typ format type_enc true 0 T),
  1940                     term Elsewhere tm)
  1941             else
  1942               ATerm (("LAMBDA", "LAMBDA"), []) (*###*)
  1943 (*###
  1944               raise Fail "unexpected lambda-abstraction"
  1945 *)
  1946           | IApp _ => raise Fail "impossible \"IApp\""
  1947         val T = ityp_of u
  1948       in
  1949         if should_tag_with_type ctxt mono type_enc site u T then
  1950           tag_with_type ctxt format mono type_enc pos T t
  1951         else
  1952           t
  1953       end
  1954   in term o Top_Level end
  1955 and formula_from_iformula ctxt polym_constrs format mono type_enc
  1956                           should_guard_var =
  1957   let
  1958     val thy = Proof_Context.theory_of ctxt
  1959     val level = level_of_type_enc type_enc
  1960     val do_term = ho_term_from_iterm ctxt format mono type_enc
  1961     fun do_out_of_bound_type pos phi universal (name, T) =
  1962       if should_guard_type ctxt mono type_enc
  1963              (fn () => should_guard_var thy polym_constrs level pos phi
  1964                                         universal name) T then
  1965         IVar (name, T)
  1966         |> type_guard_iterm format type_enc T
  1967         |> do_term pos |> AAtom |> SOME
  1968       else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
  1969         let
  1970           val var = ATerm (name, [])
  1971           val tagged_var = tag_with_type ctxt format mono type_enc pos T var
  1972         in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
  1973       else
  1974         NONE
  1975     fun do_formula pos (AQuant (q, xs, phi)) =
  1976         let
  1977           val phi = phi |> do_formula pos
  1978           val universal = Option.map (q = AExists ? not) pos
  1979           val do_bound_type = do_bound_type ctxt format mono type_enc
  1980         in
  1981           AQuant (q, xs |> map (apsnd (fn NONE => NONE
  1982                                         | SOME T => do_bound_type T)),
  1983                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
  1984                       (map_filter
  1985                            (fn (_, NONE) => NONE
  1986                              | (s, SOME T) =>
  1987                                do_out_of_bound_type pos phi universal (s, T))
  1988                            xs)
  1989                       phi)
  1990         end
  1991       | do_formula pos (AConn conn) = aconn_map pos do_formula conn
  1992       | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
  1993   in do_formula end
  1994 
  1995 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
  1996    of monomorphization). The TPTP explicitly forbids name clashes, and some of
  1997    the remote provers might care. *)
  1998 fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
  1999         mono type_enc rank (j, {name, stature, kind, iformula, atomic_types}) =
  2000   (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
  2001    iformula
  2002    |> formula_from_iformula ctxt polym_constrs format mono type_enc
  2003           should_guard_var_in_formula (if pos then SOME true else NONE)
  2004    |> close_formula_universally
  2005    |> bound_tvars type_enc true atomic_types,
  2006    NONE,
  2007    let val rank = rank j in
  2008      case snd stature of
  2009        Intro => isabelle_info format introN rank
  2010      | Elim => isabelle_info format elimN rank
  2011      | Simp => isabelle_info format simpN rank
  2012      | Spec_Eq => isabelle_info format spec_eqN rank
  2013      | _ => isabelle_info format "" rank
  2014    end)
  2015   |> Formula
  2016 
  2017 fun formula_line_for_class_rel_clause format type_enc
  2018         ({name, subclass, superclass, ...} : class_rel_clause) =
  2019   let val ty_arg = ATerm (tvar_a_name, []) in
  2020     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
  2021              AConn (AImplies,
  2022                     [type_class_formula type_enc subclass ty_arg,
  2023                      type_class_formula type_enc superclass ty_arg])
  2024              |> mk_aquant AForall
  2025                           [(tvar_a_name, atype_of_type_vars type_enc)],
  2026              NONE, isabelle_info format introN helper_rank)
  2027   end
  2028 
  2029 fun formula_from_arity_atom type_enc (class, t, args) =
  2030   ATerm (t, map (fn arg => ATerm (arg, [])) args)
  2031   |> type_class_formula type_enc class
  2032 
  2033 fun formula_line_for_arity_clause format type_enc
  2034         ({name, prem_atoms, concl_atom} : arity_clause) =
  2035   Formula (arity_clause_prefix ^ name, Axiom,
  2036            mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
  2037                     (formula_from_arity_atom type_enc concl_atom)
  2038            |> mk_aquant AForall
  2039                   (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
  2040            NONE, isabelle_info format introN helper_rank)
  2041 
  2042 fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
  2043         ({name, kind, iformula, atomic_types, ...} : translated_formula) =
  2044   Formula (conjecture_prefix ^ name, kind,
  2045            iformula
  2046            |> formula_from_iformula ctxt polym_constrs format mono type_enc
  2047                   should_guard_var_in_formula (SOME false)
  2048            |> close_formula_universally
  2049            |> bound_tvars type_enc true atomic_types, NONE, [])
  2050 
  2051 fun formula_line_for_free_type j phi =
  2052   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
  2053 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
  2054   let
  2055     val phis =
  2056       fold (union (op =)) (map #atomic_types facts) []
  2057       |> formulas_for_types type_enc add_sorts_on_tfree
  2058   in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
  2059 
  2060 (** Symbol declarations **)
  2061 
  2062 fun decl_line_for_class order s =
  2063   let val name as (s, _) = `make_type_class s in
  2064     Decl (sym_decl_prefix ^ s, name,
  2065           if order = First_Order then
  2066             ATyAbs ([tvar_a_name],
  2067                     if avoid_first_order_ghost_type_vars then
  2068                       AFun (a_itself_atype, bool_atype)
  2069                     else
  2070                       bool_atype)
  2071           else
  2072             AFun (atype_of_types, bool_atype))
  2073   end
  2074 
  2075 fun decl_lines_for_classes type_enc classes =
  2076   case type_enc of
  2077     Simple_Types (order, Polymorphic, _) =>
  2078     map (decl_line_for_class order) classes
  2079   | _ => []
  2080 
  2081 fun sym_decl_table_for_facts ctxt format type_enc sym_tab
  2082                              (conjs, facts, extra_tms) =
  2083   let
  2084     fun add_iterm_syms tm =
  2085       let val (head, args) = strip_iterm_comb tm in
  2086         (case head of
  2087            IConst ((s, s'), T, T_args) =>
  2088            let
  2089              val (pred_sym, in_conj) =
  2090                case Symtab.lookup sym_tab s of
  2091                  SOME ({pred_sym, in_conj, ...} : sym_info) =>
  2092                  (pred_sym, in_conj)
  2093                | NONE => (false, false)
  2094              val decl_sym =
  2095                (case type_enc of
  2096                   Guards _ => not pred_sym
  2097                 | _ => true) andalso
  2098                is_tptp_user_symbol s
  2099            in
  2100              if decl_sym then
  2101                Symtab.map_default (s, [])
  2102                    (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
  2103                                          in_conj))
  2104              else
  2105                I
  2106            end
  2107          | IAbs (_, tm) => add_iterm_syms tm
  2108          | _ => I)
  2109         #> fold add_iterm_syms args
  2110       end
  2111     val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
  2112     fun add_formula_var_types (AQuant (_, xs, phi)) =
  2113         fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
  2114         #> add_formula_var_types phi
  2115       | add_formula_var_types (AConn (_, phis)) =
  2116         fold add_formula_var_types phis
  2117       | add_formula_var_types _ = I
  2118     fun var_types () =
  2119       if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
  2120       else fold (fact_lift add_formula_var_types) (conjs @ facts) []
  2121     fun add_undefined_const T =
  2122       let
  2123         val (s, s') =
  2124           `(make_fixed_const NONE) @{const_name undefined}
  2125           |> (case type_arg_policy [] type_enc @{const_name undefined} of
  2126                 Mangled_Type_Args => mangled_const_name format type_enc [T]
  2127               | _ => I)
  2128       in
  2129         Symtab.map_default (s, [])
  2130                            (insert_type ctxt #3 (s', [T], T, false, 0, false))
  2131       end
  2132     fun add_TYPE_const () =
  2133       let val (s, s') = TYPE_name in
  2134         Symtab.map_default (s, [])
  2135             (insert_type ctxt #3
  2136                          (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
  2137       end
  2138   in
  2139     Symtab.empty
  2140     |> is_type_enc_fairly_sound type_enc
  2141        ? (fold (fold add_fact_syms) [conjs, facts]
  2142           #> fold add_iterm_syms extra_tms
  2143           #> (case type_enc of
  2144                 Simple_Types (First_Order, Polymorphic, _) =>
  2145                 if avoid_first_order_ghost_type_vars then add_TYPE_const ()
  2146                 else I
  2147               | Simple_Types _ => I
  2148               | _ => fold add_undefined_const (var_types ())))
  2149   end
  2150 
  2151 (* We add "bool" in case the helper "True_or_False" is included later. *)
  2152 fun default_mono level =
  2153   {maybe_finite_Ts = [@{typ bool}],
  2154    surely_finite_Ts = [@{typ bool}],
  2155    maybe_infinite_Ts = known_infinite_types,
  2156    surely_infinite_Ts =
  2157      case level of
  2158        Noninf_Nonmono_Types (Strict, _) => []
  2159      | _ => known_infinite_types,
  2160    maybe_nonmono_Ts = [@{typ bool}]}
  2161 
  2162 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
  2163    out with monotonicity" paper presented at CADE 2011. *)
  2164 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
  2165   | add_iterm_mononotonicity_info ctxt level _
  2166         (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
  2167         (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
  2168                   surely_infinite_Ts, maybe_nonmono_Ts}) =
  2169     if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
  2170       case level of
  2171         Noninf_Nonmono_Types (strictness, _) =>
  2172         if exists (type_instance ctxt T) surely_infinite_Ts orelse
  2173            member (type_equiv ctxt) maybe_finite_Ts T then
  2174           mono
  2175         else if is_type_kind_of_surely_infinite ctxt strictness
  2176                                                 surely_infinite_Ts T then
  2177           {maybe_finite_Ts = maybe_finite_Ts,
  2178            surely_finite_Ts = surely_finite_Ts,
  2179            maybe_infinite_Ts = maybe_infinite_Ts,
  2180            surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
  2181            maybe_nonmono_Ts = maybe_nonmono_Ts}
  2182         else
  2183           {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
  2184            surely_finite_Ts = surely_finite_Ts,
  2185            maybe_infinite_Ts = maybe_infinite_Ts,
  2186            surely_infinite_Ts = surely_infinite_Ts,
  2187            maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
  2188       | Fin_Nonmono_Types _ =>
  2189         if exists (type_instance ctxt T) surely_finite_Ts orelse
  2190            member (type_equiv ctxt) maybe_infinite_Ts T then
  2191           mono
  2192         else if is_type_surely_finite ctxt T then
  2193           {maybe_finite_Ts = maybe_finite_Ts,
  2194            surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
  2195            maybe_infinite_Ts = maybe_infinite_Ts,
  2196            surely_infinite_Ts = surely_infinite_Ts,
  2197            maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
  2198         else
  2199           {maybe_finite_Ts = maybe_finite_Ts,
  2200            surely_finite_Ts = surely_finite_Ts,
  2201            maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
  2202            surely_infinite_Ts = surely_infinite_Ts,
  2203            maybe_nonmono_Ts = maybe_nonmono_Ts}
  2204       | _ => mono
  2205     else
  2206       mono
  2207   | add_iterm_mononotonicity_info _ _ _ _ mono = mono
  2208 fun add_fact_mononotonicity_info ctxt level
  2209         ({kind, iformula, ...} : translated_formula) =
  2210   formula_fold (SOME (kind <> Conjecture))
  2211                (add_iterm_mononotonicity_info ctxt level) iformula
  2212 fun mononotonicity_info_for_facts ctxt type_enc facts =
  2213   let val level = level_of_type_enc type_enc in
  2214     default_mono level
  2215     |> is_type_level_monotonicity_based level
  2216        ? fold (add_fact_mononotonicity_info ctxt level) facts
  2217   end
  2218 
  2219 fun add_iformula_monotonic_types ctxt mono type_enc =
  2220   let
  2221     val level = level_of_type_enc type_enc
  2222     val should_encode = should_encode_type ctxt mono level
  2223     fun add_type T = not (should_encode T) ? insert_type ctxt I T
  2224     fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
  2225       | add_args _ = I
  2226     and add_term tm = add_type (ityp_of tm) #> add_args tm
  2227   in formula_fold NONE (K add_term) end
  2228 fun add_fact_monotonic_types ctxt mono type_enc =
  2229   add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
  2230 fun monotonic_types_for_facts ctxt mono type_enc facts =
  2231   let val level = level_of_type_enc type_enc in
  2232     [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
  2233            is_type_level_monotonicity_based level andalso
  2234            granularity_of_type_level level <> Ghost_Type_Arg_Vars)
  2235           ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
  2236   end
  2237 
  2238 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
  2239   Formula (guards_sym_formula_prefix ^
  2240            ascii_of (mangled_type format type_enc T),
  2241            Axiom,
  2242            IConst (`make_bound_var "X", T, [])
  2243            |> type_guard_iterm format type_enc T
  2244            |> AAtom
  2245            |> formula_from_iformula ctxt [] format mono type_enc
  2246                                     always_guard_var_in_formula (SOME true)
  2247            |> close_formula_universally
  2248            |> bound_tvars type_enc true (atomic_types_of T),
  2249            NONE, isabelle_info format introN helper_rank)
  2250 
  2251 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
  2252   let val x_var = ATerm (`make_bound_var "X", []) in
  2253     Formula (tags_sym_formula_prefix ^
  2254              ascii_of (mangled_type format type_enc T),
  2255              Axiom,
  2256              eq_formula type_enc (atomic_types_of T) [] false
  2257                   (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
  2258              NONE, isabelle_info format spec_eqN helper_rank)
  2259   end
  2260 
  2261 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
  2262   case type_enc of
  2263     Simple_Types _ => []
  2264   | Guards _ =>
  2265     map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
  2266   | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
  2267 
  2268 fun decl_line_for_sym ctxt format mono type_enc s
  2269                       (s', T_args, T, pred_sym, ary, _) =
  2270   let
  2271     val thy = Proof_Context.theory_of ctxt
  2272     val (T, T_args) =
  2273       if null T_args then
  2274         (T, [])
  2275       else case unprefix_and_unascii const_prefix s of
  2276         SOME s' =>
  2277         let
  2278           val s' = s' |> invert_const
  2279           val T = s' |> robust_const_type thy
  2280         in (T, robust_const_typargs thy (s', T)) end
  2281       | NONE => raise Fail "unexpected type arguments"
  2282   in
  2283     Decl (sym_decl_prefix ^ s, (s, s'),
  2284           T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
  2285             |> ho_type_from_typ format type_enc pred_sym ary
  2286             |> not (null T_args)
  2287                ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
  2288   end
  2289 
  2290 fun honor_conj_sym_kind in_conj conj_sym_kind =
  2291   if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  2292   else (Axiom, I)
  2293 
  2294 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
  2295                                      j (s', T_args, T, _, ary, in_conj) =
  2296   let
  2297     val thy = Proof_Context.theory_of ctxt
  2298     val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
  2299     val (arg_Ts, res_T) = chop_fun ary T
  2300     val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
  2301     val bounds =
  2302       bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
  2303     val bound_Ts =
  2304       if exists (curry (op =) dummyT) T_args then
  2305         case level_of_type_enc type_enc of
  2306           All_Types => map SOME arg_Ts
  2307         | level =>
  2308           if granularity_of_type_level level = Ghost_Type_Arg_Vars then
  2309             let val ghosts = ghost_type_args thy s ary in
  2310               map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
  2311                    (0 upto ary - 1) arg_Ts
  2312             end
  2313           else
  2314             replicate ary NONE
  2315       else
  2316         replicate ary NONE
  2317   in
  2318     Formula (guards_sym_formula_prefix ^ s ^
  2319              (if n > 1 then "_" ^ string_of_int j else ""), kind,
  2320              IConst ((s, s'), T, T_args)
  2321              |> fold (curry (IApp o swap)) bounds
  2322              |> type_guard_iterm format type_enc res_T
  2323              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
  2324              |> formula_from_iformula ctxt [] format mono type_enc
  2325                                       always_guard_var_in_formula (SOME true)
  2326              |> close_formula_universally
  2327              |> bound_tvars type_enc (n > 1) (atomic_types_of T)
  2328              |> maybe_negate,
  2329              NONE, isabelle_info format introN helper_rank)
  2330   end
  2331 
  2332 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
  2333         (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  2334   let
  2335     val thy = Proof_Context.theory_of ctxt
  2336     val level = level_of_type_enc type_enc
  2337     val grain = granularity_of_type_level level
  2338     val ident_base =
  2339       tags_sym_formula_prefix ^ s ^
  2340       (if n > 1 then "_" ^ string_of_int j else "")
  2341     val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
  2342     val (arg_Ts, res_T) = chop_fun ary T
  2343     val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
  2344     val bounds = bound_names |> map (fn name => ATerm (name, []))
  2345     val cst = mk_aterm format type_enc (s, s') T_args
  2346     val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
  2347     val should_encode = should_encode_type ctxt mono level
  2348     val tag_with = tag_with_type ctxt format mono type_enc NONE
  2349     val add_formula_for_res =
  2350       if should_encode res_T then
  2351         let
  2352           val tagged_bounds =
  2353             if grain = Ghost_Type_Arg_Vars then
  2354               let val ghosts = ghost_type_args thy s ary in
  2355                 map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
  2356                      (0 upto ary - 1 ~~ arg_Ts) bounds
  2357               end
  2358             else
  2359               bounds
  2360         in
  2361           cons (Formula (ident_base ^ "_res", kind,
  2362                          eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
  2363                          NONE, isabelle_info format spec_eqN helper_rank))
  2364         end
  2365       else
  2366         I
  2367     fun add_formula_for_arg k =
  2368       let val arg_T = nth arg_Ts k in
  2369         if should_encode arg_T then
  2370           case chop k bounds of
  2371             (bounds1, bound :: bounds2) =>
  2372             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
  2373                            eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
  2374                               (cst bounds),
  2375                            NONE, isabelle_info format spec_eqN helper_rank))
  2376           | _ => raise Fail "expected nonempty tail"
  2377         else
  2378           I
  2379       end
  2380   in
  2381     [] |> not pred_sym ? add_formula_for_res
  2382        |> (Config.get ctxt type_tag_arguments andalso
  2383            grain = Positively_Naked_Vars)
  2384           ? fold add_formula_for_arg (ary - 1 downto 0)
  2385   end
  2386 
  2387 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
  2388 
  2389 fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
  2390     let
  2391       val T = result_type_of_decl decl
  2392               |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
  2393     in
  2394       if forall (type_generalization ctxt T o result_type_of_decl) decls' then
  2395         [decl]
  2396       else
  2397         decls
  2398     end
  2399   | rationalize_decls _ decls = decls
  2400 
  2401 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
  2402                                 (s, decls) =
  2403   case type_enc of
  2404     Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
  2405   | Guards (_, level) =>
  2406     let
  2407       val decls = decls |> rationalize_decls ctxt
  2408       val n = length decls
  2409       val decls =
  2410         decls |> filter (should_encode_type ctxt mono level
  2411                          o result_type_of_decl)
  2412     in
  2413       (0 upto length decls - 1, decls)
  2414       |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
  2415                                                  type_enc n s)
  2416     end
  2417   | Tags (_, level) =>
  2418     if granularity_of_type_level level = All_Vars then
  2419       []
  2420     else
  2421       let val n = length decls in
  2422         (0 upto n - 1 ~~ decls)
  2423         |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono
  2424                                                  type_enc n s)
  2425       end
  2426 
  2427 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
  2428                                      mono_Ts sym_decl_tab =
  2429   let
  2430     val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
  2431     val mono_lines =
  2432       problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
  2433     val decl_lines =
  2434       fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
  2435                              mono type_enc)
  2436                syms []
  2437   in mono_lines @ decl_lines end
  2438 
  2439 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
  2440 
  2441 fun do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
  2442         mono type_enc sym_tab0 sym_tab base_s0 types in_conj =
  2443   let
  2444     fun do_alias ary =
  2445       let
  2446         val thy = Proof_Context.theory_of ctxt
  2447         val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
  2448         val base_name = base_s0 |> `(make_fixed_const (SOME format))
  2449         val T = case types of [T] => T | _ => robust_const_type thy base_s0
  2450         val T_args = robust_const_typargs thy (base_s0, T)
  2451         val (base_name as (base_s, _), T_args) =
  2452           mangle_type_args_in_const format type_enc base_name T_args
  2453         val base_ary = min_ary_of sym_tab0 base_s
  2454         fun do_const name = IConst (name, T, T_args)
  2455         val filter_ty_args =
  2456           filter_type_args_in_iterm thy monom_constrs type_enc
  2457         val ho_term_of =
  2458           ho_term_from_iterm ctxt format mono type_enc (SOME true)
  2459         val name1 as (s1, _) =
  2460           base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
  2461         val name2 as (s2, _) = base_name |> aliased_uncurried ary
  2462         val (arg_Ts, _) = chop_fun ary T
  2463         val bound_names =
  2464           1 upto ary |> map (`I o make_bound_var o string_of_int)
  2465         val bounds = bound_names ~~ arg_Ts
  2466         val (first_bounds, last_bound) =
  2467           bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last
  2468         val tm1 =
  2469           mk_app_op format type_enc (list_app (do_const name1) first_bounds)
  2470                     last_bound
  2471           |> filter_ty_args
  2472         val tm2 =
  2473           list_app (do_const name2) (first_bounds @ [last_bound])
  2474           |> filter_ty_args
  2475         val do_bound_type = do_bound_type ctxt format mono type_enc
  2476         val eq =
  2477           eq_formula type_enc (atomic_types_of T)
  2478                      (map (apsnd do_bound_type) bounds) false
  2479                      (ho_term_of tm1) (ho_term_of tm2)
  2480       in
  2481         ([tm1, tm2],
  2482          [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
  2483                    NONE, isabelle_info format spec_eqN helper_rank)])
  2484         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
  2485             else pair_append (do_alias (ary - 1)))
  2486       end
  2487   in do_alias end
  2488 fun uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
  2489         type_enc sym_tab0 sym_tab
  2490         (s, {min_ary, types, in_conj, ...} : sym_info) =
  2491   case unprefix_and_unascii const_prefix s of
  2492     SOME mangled_s =>
  2493     if String.isSubstring uncurried_alias_sep mangled_s then
  2494       let
  2495         val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
  2496       in
  2497         do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
  2498             mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary
  2499       end
  2500     else
  2501       ([], [])
  2502   | NONE => ([], [])
  2503 fun uncurried_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
  2504         mono type_enc uncurried_aliases sym_tab0 sym_tab =
  2505   ([], [])
  2506   |> uncurried_aliases
  2507      ? Symtab.fold_rev
  2508            (pair_append
  2509             o uncurried_alias_lines_for_sym ctxt monom_constrs format
  2510                   conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab
  2511 
  2512 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
  2513     Config.get ctxt type_tag_idempotence andalso
  2514     is_type_level_monotonicity_based level andalso
  2515     poly <> Mangled_Monomorphic
  2516   | needs_type_tag_idempotence _ _ = false
  2517 
  2518 val implicit_declsN = "Should-be-implicit typings"
  2519 val explicit_declsN = "Explicit typings"
  2520 val uncurried_alias_eqsN = "Uncurried aliases"
  2521 val factsN = "Relevant facts"
  2522 val class_relsN = "Class relationships"
  2523 val aritiesN = "Arities"
  2524 val helpersN = "Helper facts"
  2525 val conjsN = "Conjectures"
  2526 val free_typesN = "Type variables"
  2527 
  2528 (* TFF allows implicit declarations of types, function symbols, and predicate
  2529    symbols (with "$i" as the type of individuals), but some provers (e.g.,
  2530    SNARK) require explicit declarations. The situation is similar for THF. *)
  2531 
  2532 fun default_type type_enc pred_sym s =
  2533   let
  2534     val ind =
  2535       case type_enc of
  2536         Simple_Types _ =>
  2537         if String.isPrefix type_const_prefix s then atype_of_types
  2538         else individual_atype
  2539       | _ => individual_atype
  2540     fun typ 0 = if pred_sym then bool_atype else ind
  2541       | typ ary = AFun (ind, typ (ary - 1))
  2542   in typ end
  2543 
  2544 fun nary_type_constr_type n =
  2545   funpow n (curry AFun atype_of_types) atype_of_types
  2546 
  2547 fun undeclared_syms_in_problem type_enc problem =
  2548   let
  2549     val declared = declared_syms_in_problem problem
  2550     fun do_sym (name as (s, _)) ty =
  2551       if is_tptp_user_symbol s andalso not (member (op =) declared name) then
  2552         AList.default (op =) (name, ty)
  2553       else
  2554         I
  2555     fun do_type (AType (name, tys)) =
  2556         do_sym name (fn () => nary_type_constr_type (length tys))
  2557         #> fold do_type tys
  2558       | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
  2559       | do_type (ATyAbs (_, ty)) = do_type ty
  2560     fun do_term pred_sym (ATerm (name as (s, _), tms)) =
  2561         do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
  2562         #> fold (do_term false) tms
  2563       | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
  2564     fun do_formula (AQuant (_, xs, phi)) =
  2565         fold do_type (map_filter snd xs) #> do_formula phi
  2566       | do_formula (AConn (_, phis)) = fold do_formula phis
  2567       | do_formula (AAtom tm) = do_term true tm
  2568     fun do_problem_line (Decl (_, _, ty)) = do_type ty
  2569       | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
  2570   in
  2571     fold (fold do_problem_line o snd) problem []
  2572     |> filter_out (is_built_in_tptp_symbol o fst o fst)
  2573   end
  2574 
  2575 fun declare_undeclared_syms_in_atp_problem type_enc problem =
  2576   let
  2577     val decls =
  2578       problem
  2579       |> undeclared_syms_in_problem type_enc
  2580       |> sort_wrt (fst o fst)
  2581       |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
  2582   in (implicit_declsN, decls) :: problem end
  2583 
  2584 fun exists_subdtype P =
  2585   let
  2586     fun ex U = P U orelse
  2587       (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false)
  2588   in ex end
  2589 
  2590 fun is_poly_constr (_, Us) =
  2591   exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
  2592 
  2593 fun all_constrs_of_polymorphic_datatypes thy =
  2594   Symtab.fold (snd
  2595                #> #descr
  2596                #> maps (snd #> #3)
  2597                #> (fn cs => exists is_poly_constr cs ? append cs))
  2598               (Datatype.get_all thy) []
  2599   |> List.partition is_poly_constr
  2600   |> pairself (map fst)
  2601 
  2602 val app_op_threshold = 50
  2603 
  2604 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
  2605                         lam_trans uncurried_aliases readable_names preproc
  2606                         hyp_ts concl_t facts =
  2607   let
  2608     val thy = Proof_Context.theory_of ctxt
  2609     val type_enc = type_enc |> adjust_type_enc format
  2610     (* Forcing explicit applications is expensive for polymorphic encodings,
  2611        because it takes only one existential variable ranging over "'a => 'b" to
  2612        ruin everything. Hence we do it only if there are few facts (which is
  2613        normally the case for "metis" and the minimizer). *)
  2614     val app_op_level =
  2615       if polymorphism_of_type_enc type_enc = Polymorphic andalso
  2616          length facts >= app_op_threshold then
  2617         Incomplete_Apply
  2618       else
  2619         Sufficient_Apply
  2620     val lam_trans =
  2621       if lam_trans = keep_lamsN andalso
  2622          not (is_type_enc_higher_order type_enc) then
  2623         error ("Lambda translation scheme incompatible with first-order \
  2624                \encoding.")
  2625       else
  2626         lam_trans
  2627     val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
  2628          lifted) =
  2629       translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
  2630                          concl_t facts
  2631     val sym_tab0 = sym_table_for_facts ctxt type_enc app_op_level conjs facts
  2632     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
  2633     val (polym_constrs, monom_constrs) =
  2634       all_constrs_of_polymorphic_datatypes thy
  2635       |>> map (make_fixed_const (SOME format))
  2636     fun firstorderize in_helper =
  2637       firstorderize_fact thy monom_constrs format type_enc sym_tab0
  2638                          (uncurried_aliases andalso not in_helper)
  2639     val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
  2640     val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
  2641     val helpers =
  2642       sym_tab |> helper_facts_for_sym_table ctxt format type_enc
  2643               |> map (firstorderize true)
  2644     val mono_Ts =
  2645       helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
  2646     val class_decl_lines = decl_lines_for_classes type_enc classes
  2647     val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
  2648       uncurried_alias_lines_for_sym_table ctxt monom_constrs format
  2649           conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
  2650     val sym_decl_lines =
  2651       (conjs, helpers @ facts, uncurried_alias_eq_tms)
  2652       |> sym_decl_table_for_facts ctxt format type_enc sym_tab
  2653       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
  2654                                                type_enc mono_Ts
  2655     val num_facts = length facts
  2656     val fact_lines =
  2657       map (formula_line_for_fact ctxt polym_constrs format fact_prefix
  2658                ascii_of (not exporter) (not exporter) mono type_enc
  2659                (rank_of_fact_num num_facts))
  2660           (0 upto num_facts - 1 ~~ facts)
  2661     val helper_lines =
  2662       0 upto length helpers - 1 ~~ helpers
  2663       |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I
  2664                                     false true mono type_enc (K default_rank))
  2665       |> (if needs_type_tag_idempotence ctxt type_enc then
  2666             cons (type_tag_idempotence_fact format type_enc)
  2667           else
  2668             I)
  2669     (* Reordering these might confuse the proof reconstruction code or the SPASS
  2670        FLOTTER hack. *)
  2671     val problem =
  2672       [(explicit_declsN, class_decl_lines @ sym_decl_lines),
  2673        (uncurried_alias_eqsN, uncurried_alias_eq_lines),
  2674        (factsN, fact_lines),
  2675        (class_relsN,
  2676         map (formula_line_for_class_rel_clause format type_enc)
  2677             class_rel_clauses),
  2678        (aritiesN,
  2679         map (formula_line_for_arity_clause format type_enc) arity_clauses),
  2680        (helpersN, helper_lines),
  2681        (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)),
  2682        (conjsN,
  2683         map (formula_line_for_conjecture ctxt polym_constrs format mono
  2684                                          type_enc) conjs)]
  2685     val problem =
  2686       problem
  2687       |> (case format of
  2688             CNF => ensure_cnf_problem
  2689           | CNF_UEQ => filter_cnf_ueq_problem
  2690           | FOF => I
  2691           | TFF (_, TPTP_Implicit) => I
  2692           | THF (_, TPTP_Implicit, _) => I
  2693           | _ => declare_undeclared_syms_in_atp_problem type_enc)
  2694     val (problem, pool) = problem |> nice_atp_problem readable_names format
  2695     fun add_sym_ary (s, {min_ary, ...} : sym_info) =
  2696       min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
  2697   in
  2698     (problem,
  2699      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
  2700      fact_names |> Vector.fromList,
  2701      lifted,
  2702      Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
  2703   end
  2704 
  2705 (* FUDGE *)
  2706 val conj_weight = 0.0
  2707 val hyp_weight = 0.1
  2708 val fact_min_weight = 0.2
  2709 val fact_max_weight = 1.0
  2710 val type_info_default_weight = 0.8
  2711 
  2712 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
  2713 fun atp_problem_relevance_weights problem =
  2714   let
  2715     fun add_term_weights weight (ATerm (s, tms)) =
  2716         is_tptp_user_symbol s ? Symtab.default (s, weight)
  2717         #> fold (add_term_weights weight) tms
  2718       | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
  2719     fun add_line_weights weight (Formula (_, _, phi, _, _)) =
  2720         formula_fold NONE (K (add_term_weights weight)) phi
  2721       | add_line_weights _ _ = I
  2722     fun add_conjectures_weights [] = I
  2723       | add_conjectures_weights conjs =
  2724         let val (hyps, conj) = split_last conjs in
  2725           add_line_weights conj_weight conj
  2726           #> fold (add_line_weights hyp_weight) hyps
  2727         end
  2728     fun add_facts_weights facts =
  2729       let
  2730         val num_facts = length facts
  2731         fun weight_of j =
  2732           fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
  2733                             / Real.fromInt num_facts
  2734       in
  2735         map weight_of (0 upto num_facts - 1) ~~ facts
  2736         |> fold (uncurry add_line_weights)
  2737       end
  2738     val get = these o AList.lookup (op =) problem
  2739   in
  2740     Symtab.empty
  2741     |> add_conjectures_weights (get free_typesN @ get conjsN)
  2742     |> add_facts_weights (get factsN)
  2743     |> fold (fold (add_line_weights type_info_default_weight) o get)
  2744             [explicit_declsN, class_relsN, aritiesN]
  2745     |> Symtab.dest
  2746     |> sort (prod_ord Real.compare string_ord o pairself swap)
  2747   end
  2748 
  2749 fun have_head_rolling (ATerm (s, args)) =
  2750     (* ugly hack: may make innocent victims *)
  2751     if String.isPrefix app_op_name s andalso length args = 2 then
  2752       have_head_rolling (hd args) ||> append (tl args)
  2753     else
  2754       (s, args)
  2755   | have_head_rolling _ = ("", [])
  2756 
  2757 val max_kbo_weight = 2147483647
  2758 
  2759 fun atp_problem_kbo_weights problem =
  2760   let
  2761     fun add_term_deps head (ATerm (s, args)) =
  2762         is_tptp_user_symbol s ? perhaps (try (Graph.add_edge_acyclic (s, head)))
  2763         #> fold (add_term_deps head) args
  2764       | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm
  2765     fun add_eq_deps (ATerm (s, [lhs as _, rhs])) =
  2766         if is_tptp_equal s then
  2767           let val (head, rest) = have_head_rolling lhs in
  2768             fold (add_term_deps head) (rhs :: rest)
  2769           end
  2770         else
  2771           I
  2772       | add_eq_deps _ = I
  2773     fun add_line_deps _ (Decl (_, s, ty)) =
  2774         is_function_type ty ? Graph.default_node (s, ())
  2775       | add_line_deps status (Formula (_, _, phi, _, info)) =
  2776         if extract_isabelle_status info = SOME status then
  2777           formula_fold NONE (K add_eq_deps) phi
  2778         else
  2779           I
  2780     val graph =
  2781       Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem
  2782                   |> fold (fold (add_line_deps simpN) o snd) problem
  2783     fun next_weight w = if w + w <= max_kbo_weight then w + w else w + 1
  2784     fun add_weights _ [] = I
  2785       | add_weights weight syms =
  2786         fold (AList.update (op =) o rpair weight) syms
  2787         #> add_weights (next_weight weight)
  2788                (fold (union (op =) o Graph.immediate_succs graph) syms [])
  2789   in
  2790     [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o pairself snd)
  2791   end
  2792 
  2793 end;