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