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