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