src/HOL/Tools/ATP/atp_translate.ML
author blanchet
Fri Jul 01 15:53:37 2011 +0200 (2011-07-01)
changeset 43622 80673841372b
parent 43572 ae612a423dad
child 43623 e096b1effbbb
permissions -rw-r--r--
tuning
     1 (*  Title:      HOL/Tools/ATP/atp_translate.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Translation of HOL to FOL for Sledgehammer.
     7 *)
     8 
     9 signature ATP_TRANSLATE =
    10 sig
    11   type 'a fo_term = 'a ATP_Problem.fo_term
    12   type connective = ATP_Problem.connective
    13   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
    14   type format = ATP_Problem.format
    15   type formula_kind = ATP_Problem.formula_kind
    16   type 'a problem = 'a ATP_Problem.problem
    17 
    18   datatype locality =
    19     General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
    20     Chained
    21 
    22   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    23   datatype type_level =
    24     All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
    25     No_Types
    26   datatype type_heaviness = Heavyweight | Lightweight
    27 
    28   datatype type_sys =
    29     Simple_Types of type_level |
    30     Preds of polymorphism * type_level * type_heaviness |
    31     Tags of polymorphism * type_level * type_heaviness
    32 
    33   val bound_var_prefix : string
    34   val schematic_var_prefix : string
    35   val fixed_var_prefix : string
    36   val tvar_prefix : string
    37   val tfree_prefix : string
    38   val const_prefix : string
    39   val type_const_prefix : string
    40   val class_prefix : string
    41   val skolem_const_prefix : string
    42   val old_skolem_const_prefix : string
    43   val new_skolem_const_prefix : string
    44   val type_decl_prefix : string
    45   val sym_decl_prefix : string
    46   val preds_sym_formula_prefix : string
    47   val lightweight_tags_sym_formula_prefix : string
    48   val fact_prefix : string
    49   val conjecture_prefix : string
    50   val helper_prefix : string
    51   val class_rel_clause_prefix : string
    52   val arity_clause_prefix : string
    53   val tfree_clause_prefix : string
    54   val typed_helper_suffix : string
    55   val untyped_helper_suffix : string
    56   val type_tag_idempotence_helper_name : string
    57   val predicator_name : string
    58   val app_op_name : string
    59   val type_tag_name : string
    60   val type_pred_name : string
    61   val simple_type_prefix : string
    62   val prefixed_predicator_name : string
    63   val prefixed_app_op_name : string
    64   val prefixed_type_tag_name : string
    65   val ascii_of : string -> string
    66   val unascii_of : string -> string
    67   val strip_prefix_and_unascii : string -> string -> string option
    68   val proxy_table : (string * (string * (thm * (string * string)))) list
    69   val proxify_const : string -> (string * string) option
    70   val invert_const : string -> string
    71   val unproxify_const : string -> string
    72   val new_skolem_var_name_from_const : string -> string
    73   val num_type_args : theory -> string -> int
    74   val atp_irrelevant_consts : string list
    75   val atp_schematic_consts_of : term -> typ list Symtab.table
    76   val is_locality_global : locality -> bool
    77   val type_sys_from_string : string -> type_sys
    78   val polymorphism_of_type_sys : type_sys -> polymorphism
    79   val level_of_type_sys : type_sys -> type_level
    80   val is_type_sys_virtually_sound : type_sys -> bool
    81   val is_type_sys_fairly_sound : type_sys -> bool
    82   val choose_format : format list -> type_sys -> format * type_sys
    83   val mk_aconns :
    84     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    85   val unmangled_const : string -> string * string fo_term list
    86   val unmangled_const_name : string -> string
    87   val helper_table : ((string * bool) * thm list) list
    88   val factsN : string
    89   val prepare_atp_problem :
    90     Proof.context -> format -> formula_kind -> formula_kind -> type_sys -> bool
    91     -> bool -> bool -> bool -> term list -> term
    92     -> ((string * locality) * term) list
    93     -> string problem * string Symtab.table * int * int
    94        * (string * locality) list vector * int list * int Symtab.table
    95   val atp_problem_weights : string problem -> (string * real) list
    96 end;
    97 
    98 structure ATP_Translate : ATP_TRANSLATE =
    99 struct
   100 
   101 open ATP_Util
   102 open ATP_Problem
   103 
   104 type name = string * string
   105 
   106 (* experimental *)
   107 val generate_useful_info = false
   108 
   109 fun useful_isabelle_info s =
   110   if generate_useful_info then
   111     SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
   112   else
   113     NONE
   114 
   115 val intro_info = useful_isabelle_info "intro"
   116 val elim_info = useful_isabelle_info "elim"
   117 val simp_info = useful_isabelle_info "simp"
   118 
   119 val bound_var_prefix = "B_"
   120 val schematic_var_prefix = "V_"
   121 val fixed_var_prefix = "v_"
   122 
   123 val tvar_prefix = "T_"
   124 val tfree_prefix = "t_"
   125 
   126 val const_prefix = "c_"
   127 val type_const_prefix = "tc_"
   128 val class_prefix = "cl_"
   129 
   130 val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
   131 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
   132 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
   133 
   134 val type_decl_prefix = "ty_"
   135 val sym_decl_prefix = "sy_"
   136 val preds_sym_formula_prefix = "psy_"
   137 val lightweight_tags_sym_formula_prefix = "tsy_"
   138 val fact_prefix = "fact_"
   139 val conjecture_prefix = "conj_"
   140 val helper_prefix = "help_"
   141 val class_rel_clause_prefix = "clar_"
   142 val arity_clause_prefix = "arity_"
   143 val tfree_clause_prefix = "tfree_"
   144 
   145 val typed_helper_suffix = "_T"
   146 val untyped_helper_suffix = "_U"
   147 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
   148 
   149 val predicator_name = "hBOOL"
   150 val app_op_name = "hAPP"
   151 val type_tag_name = "ti"
   152 val type_pred_name = "is"
   153 val simple_type_prefix = "ty_"
   154 
   155 val prefixed_predicator_name = const_prefix ^ predicator_name
   156 val prefixed_app_op_name = const_prefix ^ app_op_name
   157 val prefixed_type_tag_name = const_prefix ^ type_tag_name
   158 
   159 (* Freshness almost guaranteed! *)
   160 val sledgehammer_weak_prefix = "Sledgehammer:"
   161 
   162 (*Escaping of special characters.
   163   Alphanumeric characters are left unchanged.
   164   The character _ goes to __
   165   Characters in the range ASCII space to / go to _A to _P, respectively.
   166   Other characters go to _nnn where nnn is the decimal ASCII code.*)
   167 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
   168 
   169 fun stringN_of_int 0 _ = ""
   170   | stringN_of_int k n =
   171     stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
   172 
   173 fun ascii_of_char c =
   174   if Char.isAlphaNum c then
   175     String.str c
   176   else if c = #"_" then
   177     "__"
   178   else if #" " <= c andalso c <= #"/" then
   179     "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
   180   else
   181     (* fixed width, in case more digits follow *)
   182     "_" ^ stringN_of_int 3 (Char.ord c)
   183 
   184 val ascii_of = String.translate ascii_of_char
   185 
   186 (** Remove ASCII armoring from names in proof files **)
   187 
   188 (* We don't raise error exceptions because this code can run inside a worker
   189    thread. Also, the errors are impossible. *)
   190 val unascii_of =
   191   let
   192     fun un rcs [] = String.implode(rev rcs)
   193       | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
   194         (* Three types of _ escapes: __, _A to _P, _nnn *)
   195       | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
   196       | un rcs (#"_" :: c :: cs) =
   197         if #"A" <= c andalso c<= #"P" then
   198           (* translation of #" " to #"/" *)
   199           un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
   200         else
   201           let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
   202             case Int.fromString (String.implode digits) of
   203               SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
   204             | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
   205           end
   206       | un rcs (c :: cs) = un (c :: rcs) cs
   207   in un [] o String.explode end
   208 
   209 (* If string s has the prefix s1, return the result of deleting it,
   210    un-ASCII'd. *)
   211 fun strip_prefix_and_unascii s1 s =
   212   if String.isPrefix s1 s then
   213     SOME (unascii_of (String.extract (s, size s1, NONE)))
   214   else
   215     NONE
   216 
   217 val proxy_table =
   218   [("c_False", (@{const_name False}, (@{thm fFalse_def},
   219        ("fFalse", @{const_name ATP.fFalse})))),
   220    ("c_True", (@{const_name True}, (@{thm fTrue_def},
   221        ("fTrue", @{const_name ATP.fTrue})))),
   222    ("c_Not", (@{const_name Not}, (@{thm fNot_def},
   223        ("fNot", @{const_name ATP.fNot})))),
   224    ("c_conj", (@{const_name conj}, (@{thm fconj_def},
   225        ("fconj", @{const_name ATP.fconj})))),
   226    ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
   227        ("fdisj", @{const_name ATP.fdisj})))),
   228    ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
   229        ("fimplies", @{const_name ATP.fimplies})))),
   230    ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
   231        ("fequal", @{const_name ATP.fequal}))))]
   232 
   233 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
   234 
   235 (* Readable names for the more common symbolic functions. Do not mess with the
   236    table unless you know what you are doing. *)
   237 val const_trans_table =
   238   [(@{type_name Product_Type.prod}, "prod"),
   239    (@{type_name Sum_Type.sum}, "sum"),
   240    (@{const_name False}, "False"),
   241    (@{const_name True}, "True"),
   242    (@{const_name Not}, "Not"),
   243    (@{const_name conj}, "conj"),
   244    (@{const_name disj}, "disj"),
   245    (@{const_name implies}, "implies"),
   246    (@{const_name HOL.eq}, "equal"),
   247    (@{const_name If}, "If"),
   248    (@{const_name Set.member}, "member"),
   249    (@{const_name Meson.COMBI}, "COMBI"),
   250    (@{const_name Meson.COMBK}, "COMBK"),
   251    (@{const_name Meson.COMBB}, "COMBB"),
   252    (@{const_name Meson.COMBC}, "COMBC"),
   253    (@{const_name Meson.COMBS}, "COMBS")]
   254   |> Symtab.make
   255   |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
   256 
   257 (* Invert the table of translations between Isabelle and ATPs. *)
   258 val const_trans_table_inv =
   259   const_trans_table |> Symtab.dest |> map swap |> Symtab.make
   260 val const_trans_table_unprox =
   261   Symtab.empty
   262   |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
   263 
   264 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
   265 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
   266 
   267 fun lookup_const c =
   268   case Symtab.lookup const_trans_table c of
   269     SOME c' => c'
   270   | NONE => ascii_of c
   271 
   272 fun ascii_of_indexname (v, 0) = ascii_of v
   273   | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
   274 
   275 fun make_bound_var x = bound_var_prefix ^ ascii_of x
   276 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
   277 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
   278 
   279 fun make_schematic_type_var (x, i) =
   280       tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
   281 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
   282 
   283 (* "HOL.eq" is mapped to the ATP's equality. *)
   284 fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal
   285   | make_fixed_const c = const_prefix ^ lookup_const c
   286 
   287 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
   288 
   289 fun make_type_class clas = class_prefix ^ ascii_of clas
   290 
   291 fun new_skolem_var_name_from_const s =
   292   let val ss = s |> space_explode Long_Name.separator in
   293     nth ss (length ss - 2)
   294   end
   295 
   296 (* The number of type arguments of a constant, zero if it's monomorphic. For
   297    (instances of) Skolem pseudoconstants, this information is encoded in the
   298    constant name. *)
   299 fun num_type_args thy s =
   300   if String.isPrefix skolem_const_prefix s then
   301     s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
   302   else
   303     (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
   304 
   305 (* These are either simplified away by "Meson.presimplify" (most of the time) or
   306    handled specially via "fFalse", "fTrue", ..., "fequal". *)
   307 val atp_irrelevant_consts =
   308   [@{const_name False}, @{const_name True}, @{const_name Not},
   309    @{const_name conj}, @{const_name disj}, @{const_name implies},
   310    @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
   311 
   312 val atp_monomorph_bad_consts =
   313   atp_irrelevant_consts @
   314   (* These are ignored anyway by the relevance filter (unless they appear in
   315      higher-order places) but not by the monomorphizer. *)
   316   [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
   317    @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
   318    @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
   319 
   320 fun add_schematic_const (x as (_, T)) =
   321   Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
   322 val add_schematic_consts_of =
   323   Term.fold_aterms (fn Const (x as (s, _)) =>
   324                        not (member (op =) atp_monomorph_bad_consts s)
   325                        ? add_schematic_const x
   326                       | _ => I)
   327 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
   328 
   329 (** Definitions and functions for FOL clauses and formulas for TPTP **)
   330 
   331 (* The first component is the type class; the second is a "TVar" or "TFree". *)
   332 datatype type_literal =
   333   TyLitVar of name * name |
   334   TyLitFree of name * name
   335 
   336 
   337 (** Isabelle arities **)
   338 
   339 datatype arity_literal =
   340   TConsLit of name * name * name list |
   341   TVarLit of name * name
   342 
   343 fun gen_TVars 0 = []
   344   | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
   345 
   346 val type_class = the_single @{sort type}
   347 
   348 fun add_packed_sort tvar =
   349   fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
   350 
   351 type arity_clause =
   352   {name : string,
   353    prem_lits : arity_literal list,
   354    concl_lits : arity_literal}
   355 
   356 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
   357 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
   358   let
   359     val tvars = gen_TVars (length args)
   360     val tvars_srts = ListPair.zip (tvars, args)
   361   in
   362     {name = name,
   363      prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
   364      concl_lits = TConsLit (`make_type_class cls,
   365                             `make_fixed_type_const tcons,
   366                             tvars ~~ tvars)}
   367   end
   368 
   369 fun arity_clause _ _ (_, []) = []
   370   | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)
   371     arity_clause seen n (tcons, ars)
   372   | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
   373     if member (op =) seen class then
   374       (* multiple arities for the same (tycon, class) pair *)
   375       make_axiom_arity_clause (tcons,
   376           lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
   377           ar) ::
   378       arity_clause seen (n + 1) (tcons, ars)
   379     else
   380       make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
   381                                ascii_of class, ar) ::
   382       arity_clause (class :: seen) n (tcons, ars)
   383 
   384 fun multi_arity_clause [] = []
   385   | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   386       arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   387 
   388 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
   389    theory thy provided its arguments have the corresponding sorts. *)
   390 fun type_class_pairs thy tycons classes =
   391   let
   392     val alg = Sign.classes_of thy
   393     fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
   394     fun add_class tycon class =
   395       cons (class, domain_sorts tycon class)
   396       handle Sorts.CLASS_ERROR _ => I
   397     fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
   398   in map try_classes tycons end
   399 
   400 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
   401 fun iter_type_class_pairs _ _ [] = ([], [])
   402   | iter_type_class_pairs thy tycons classes =
   403       let
   404         fun maybe_insert_class s =
   405           (s <> type_class andalso not (member (op =) classes s))
   406           ? insert (op =) s
   407         val cpairs = type_class_pairs thy tycons classes
   408         val newclasses =
   409           [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
   410         val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   411       in (classes' @ classes, union (op =) cpairs' cpairs) end
   412 
   413 fun make_arity_clauses thy tycons =
   414   iter_type_class_pairs thy tycons ##> multi_arity_clause
   415 
   416 
   417 (** Isabelle class relations **)
   418 
   419 type class_rel_clause =
   420   {name : string,
   421    subclass : name,
   422    superclass : name}
   423 
   424 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
   425    in theory "thy". *)
   426 fun class_pairs _ [] _ = []
   427   | class_pairs thy subs supers =
   428       let
   429         val class_less = Sorts.class_less (Sign.classes_of thy)
   430         fun add_super sub super = class_less (sub, super) ? cons (sub, super)
   431         fun add_supers sub = fold (add_super sub) supers
   432       in fold add_supers subs [] end
   433 
   434 fun make_class_rel_clause (sub, super) =
   435   {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
   436    superclass = `make_type_class super}
   437 
   438 fun make_class_rel_clauses thy subs supers =
   439   map make_class_rel_clause (class_pairs thy subs supers)
   440 
   441 datatype combterm =
   442   CombConst of name * typ * typ list |
   443   CombVar of name * typ |
   444   CombApp of combterm * combterm
   445 
   446 fun combtyp_of (CombConst (_, T, _)) = T
   447   | combtyp_of (CombVar (_, T)) = T
   448   | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
   449 
   450 (*gets the head of a combinator application, along with the list of arguments*)
   451 fun strip_combterm_comb u =
   452   let
   453     fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts)
   454       | stripc x = x
   455   in stripc (u, []) end
   456 
   457 fun atyps_of T = fold_atyps (insert (op =)) T []
   458 
   459 fun new_skolem_const_name s num_T_args =
   460   [new_skolem_const_prefix, s, string_of_int num_T_args]
   461   |> space_implode Long_Name.separator
   462 
   463 (* Converts a term (with combinators) into a combterm. Also accumulates sort
   464    infomation. *)
   465 fun combterm_from_term thy bs (P $ Q) =
   466     let
   467       val (P', P_atomics_Ts) = combterm_from_term thy bs P
   468       val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
   469     in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
   470   | combterm_from_term thy _ (Const (c, T)) =
   471     let
   472       val tvar_list =
   473         (if String.isPrefix old_skolem_const_prefix c then
   474            [] |> Term.add_tvarsT T |> map TVar
   475          else
   476            (c, T) |> Sign.const_typargs thy)
   477       val c' = CombConst (`make_fixed_const c, T, tvar_list)
   478     in (c', atyps_of T) end
   479   | combterm_from_term _ _ (Free (v, T)) =
   480     (CombConst (`make_fixed_var v, T, []), atyps_of T)
   481   | combterm_from_term _ _ (Var (v as (s, _), T)) =
   482     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
   483        let
   484          val Ts = T |> strip_type |> swap |> op ::
   485          val s' = new_skolem_const_name s (length Ts)
   486        in CombConst (`make_fixed_const s', T, Ts) end
   487      else
   488        CombVar ((make_schematic_var v, s), T), atyps_of T)
   489   | combterm_from_term _ bs (Bound j) =
   490     nth bs j
   491     |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
   492   | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
   493 
   494 datatype locality =
   495   General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
   496   Chained
   497 
   498 (* (quasi-)underapproximation of the truth *)
   499 fun is_locality_global Local = false
   500   | is_locality_global Assum = false
   501   | is_locality_global Chained = false
   502   | is_locality_global _ = true
   503 
   504 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
   505 datatype type_level =
   506   All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
   507   No_Types
   508 datatype type_heaviness = Heavyweight | Lightweight
   509 
   510 datatype type_sys =
   511   Simple_Types of type_level |
   512   Preds of polymorphism * type_level * type_heaviness |
   513   Tags of polymorphism * type_level * type_heaviness
   514 
   515 fun try_unsuffixes ss s =
   516   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
   517 
   518 fun type_sys_from_string s =
   519   (case try (unprefix "poly_") s of
   520      SOME s => (SOME Polymorphic, s)
   521    | NONE =>
   522      case try (unprefix "mono_") s of
   523        SOME s => (SOME Monomorphic, s)
   524      | NONE =>
   525        case try (unprefix "mangled_") s of
   526          SOME s => (SOME Mangled_Monomorphic, s)
   527        | NONE => (NONE, s))
   528   ||> (fn s =>
   529           (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
   530           case try_unsuffixes ["?", "_query"] s of
   531             SOME s => (Noninf_Nonmono_Types, s)
   532           | NONE =>
   533             case try_unsuffixes ["!", "_bang"] s of
   534               SOME s => (Fin_Nonmono_Types, s)
   535             | NONE => (All_Types, s))
   536   ||> apsnd (fn s =>
   537                 case try (unsuffix "_heavy") s of
   538                   SOME s => (Heavyweight, s)
   539                 | NONE => (Lightweight, s))
   540   |> (fn (poly, (level, (heaviness, core))) =>
   541          case (core, (poly, level, heaviness)) of
   542            ("simple", (NONE, _, Lightweight)) => Simple_Types level
   543          | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
   544          | ("tags", (SOME Polymorphic, _, _)) =>
   545            Tags (Polymorphic, level, heaviness)
   546          | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
   547          | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
   548            Preds (poly, Const_Arg_Types, Lightweight)
   549          | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
   550            Preds (Polymorphic, No_Types, Lightweight)
   551          | _ => raise Same.SAME)
   552   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
   553 
   554 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
   555   | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
   556   | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
   557 
   558 fun level_of_type_sys (Simple_Types level) = level
   559   | level_of_type_sys (Preds (_, level, _)) = level
   560   | level_of_type_sys (Tags (_, level, _)) = level
   561 
   562 fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
   563   | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
   564   | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
   565 
   566 fun is_type_level_virtually_sound level =
   567   level = All_Types orelse level = Noninf_Nonmono_Types
   568 val is_type_sys_virtually_sound =
   569   is_type_level_virtually_sound o level_of_type_sys
   570 
   571 fun is_type_level_fairly_sound level =
   572   is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
   573 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
   574 
   575 fun is_setting_higher_order THF (Simple_Types _) = true
   576   | is_setting_higher_order _ _ = false
   577 
   578 fun choose_format formats (Simple_Types level) =
   579     if member (op =) formats THF then (THF, Simple_Types level)
   580     else if member (op =) formats TFF then (TFF, Simple_Types level)
   581     else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
   582   | choose_format formats type_sys =
   583     (case hd formats of
   584        CNF_UEQ =>
   585        (CNF_UEQ, case type_sys of
   586                    Preds stuff =>
   587                    (if is_type_sys_fairly_sound type_sys then Tags else Preds)
   588                        stuff
   589                  | _ => type_sys)
   590      | format => (format, type_sys))
   591 
   592 type translated_formula =
   593   {name : string,
   594    locality : locality,
   595    kind : formula_kind,
   596    combformula : (name, typ, combterm) formula,
   597    atomic_types : typ list}
   598 
   599 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
   600                           : translated_formula) =
   601   {name = name, locality = locality, kind = kind, combformula = f combformula,
   602    atomic_types = atomic_types} : translated_formula
   603 
   604 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
   605 
   606 val type_instance = Sign.typ_instance o Proof_Context.theory_of
   607 
   608 fun insert_type ctxt get_T x xs =
   609   let val T = get_T x in
   610     if exists (curry (type_instance ctxt) T o get_T) xs then xs
   611     else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
   612   end
   613 
   614 (* The Booleans indicate whether all type arguments should be kept. *)
   615 datatype type_arg_policy =
   616   Explicit_Type_Args of bool |
   617   Mangled_Type_Args of bool |
   618   No_Type_Args
   619 
   620 fun should_drop_arg_type_args (Simple_Types _) =
   621     false (* since TFF doesn't support overloading *)
   622   | should_drop_arg_type_args type_sys =
   623     level_of_type_sys type_sys = All_Types andalso
   624     heaviness_of_type_sys type_sys = Heavyweight
   625 
   626 fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
   627   | general_type_arg_policy type_sys =
   628     if level_of_type_sys type_sys = No_Types then
   629       No_Type_Args
   630     else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
   631       Mangled_Type_Args (should_drop_arg_type_args type_sys)
   632     else
   633       Explicit_Type_Args (should_drop_arg_type_args type_sys)
   634 
   635 fun type_arg_policy type_sys s =
   636   if s = @{const_name HOL.eq} orelse
   637      (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
   638     No_Type_Args
   639   else if s = type_tag_name then
   640     Explicit_Type_Args false
   641   else
   642     general_type_arg_policy type_sys
   643 
   644 (*Make literals for sorted type variables*)
   645 fun generic_add_sorts_on_type (_, []) = I
   646   | generic_add_sorts_on_type ((x, i), s :: ss) =
   647     generic_add_sorts_on_type ((x, i), ss)
   648     #> (if s = the_single @{sort HOL.type} then
   649           I
   650         else if i = ~1 then
   651           insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
   652         else
   653           insert (op =) (TyLitVar (`make_type_class s,
   654                                    (make_schematic_type_var (x, i), x))))
   655 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
   656   | add_sorts_on_tfree _ = I
   657 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
   658   | add_sorts_on_tvar _ = I
   659 
   660 fun type_literals_for_types type_sys add_sorts_on_typ Ts =
   661   [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
   662 
   663 fun mk_aconns c phis =
   664   let val (phis', phi') = split_last phis in
   665     fold_rev (mk_aconn c) phis' phi'
   666   end
   667 fun mk_ahorn [] phi = phi
   668   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
   669 fun mk_aquant _ [] phi = phi
   670   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
   671     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
   672   | mk_aquant q xs phi = AQuant (q, xs, phi)
   673 
   674 fun close_universally atom_vars phi =
   675   let
   676     fun formula_vars bounds (AQuant (_, xs, phi)) =
   677         formula_vars (map fst xs @ bounds) phi
   678       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   679       | formula_vars bounds (AAtom tm) =
   680         union (op =) (atom_vars tm []
   681                       |> filter_out (member (op =) bounds o fst))
   682   in mk_aquant AForall (formula_vars [] phi []) phi end
   683 
   684 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
   685   | combterm_vars (CombConst _) = I
   686   | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
   687 fun close_combformula_universally phi = close_universally combterm_vars phi
   688 
   689 fun term_vars (ATerm (name as (s, _), tms)) =
   690   is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
   691 fun close_formula_universally phi = close_universally term_vars phi
   692 
   693 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
   694 val homo_infinite_type = Type (homo_infinite_type_name, [])
   695 
   696 fun fo_term_from_typ format type_sys =
   697   let
   698     fun term (Type (s, Ts)) =
   699       ATerm (case (is_setting_higher_order format type_sys, s) of
   700                (true, @{type_name bool}) => `I tptp_bool_type
   701              | (true, @{type_name fun}) => `I tptp_fun_type
   702              | _ => if s = homo_infinite_type_name andalso
   703                        (format = TFF orelse format = THF) then
   704                       `I tptp_individual_type
   705                     else
   706                       `make_fixed_type_const s,
   707              map term Ts)
   708     | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
   709     | term (TVar ((x as (s, _)), _)) =
   710       ATerm ((make_schematic_type_var x, s), [])
   711   in term end
   712 
   713 fun fo_term_for_type_arg format type_sys T =
   714   if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T)
   715 
   716 (* This shouldn't clash with anything else. *)
   717 val mangled_type_sep = "\000"
   718 
   719 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   720   | generic_mangled_type_name f (ATerm (name, tys)) =
   721     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
   722     ^ ")"
   723 
   724 val bool_atype = AType (`I tptp_bool_type)
   725 
   726 fun make_simple_type s =
   727   if s = tptp_bool_type orelse s = tptp_fun_type orelse
   728      s = tptp_individual_type then
   729     s
   730   else
   731     simple_type_prefix ^ ascii_of s
   732 
   733 fun ho_type_from_fo_term format type_sys pred_sym ary =
   734   let
   735     fun to_atype ty =
   736       AType ((make_simple_type (generic_mangled_type_name fst ty),
   737               generic_mangled_type_name snd ty))
   738     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
   739     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
   740       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
   741     fun to_ho (ty as ATerm ((s, _), tys)) =
   742       if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
   743   in if is_setting_higher_order format type_sys then to_ho else to_fo ary end
   744 
   745 fun mangled_type format type_sys pred_sym ary =
   746   ho_type_from_fo_term format type_sys pred_sym ary
   747   o fo_term_from_typ format type_sys
   748 
   749 fun mangled_const_name format type_sys T_args (s, s') =
   750   let
   751     val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
   752     fun type_suffix f g =
   753       fold_rev (curry (op ^) o g o prefix mangled_type_sep
   754                 o generic_mangled_type_name f) ty_args ""
   755   in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
   756 
   757 val parse_mangled_ident =
   758   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
   759 
   760 fun parse_mangled_type x =
   761   (parse_mangled_ident
   762    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
   763                     [] >> ATerm) x
   764 and parse_mangled_types x =
   765   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
   766 
   767 fun unmangled_type s =
   768   s |> suffix ")" |> raw_explode
   769     |> Scan.finite Symbol.stopper
   770            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
   771                                                 quote s)) parse_mangled_type))
   772     |> fst
   773 
   774 val unmangled_const_name = space_explode mangled_type_sep #> hd
   775 fun unmangled_const s =
   776   let val ss = space_explode mangled_type_sep s in
   777     (hd ss, map unmangled_type (tl ss))
   778   end
   779 
   780 fun introduce_proxies format type_sys =
   781   let
   782     fun intro top_level (CombApp (tm1, tm2)) =
   783         CombApp (intro top_level tm1, intro false tm2)
   784       | intro top_level (CombConst (name as (s, _), T, T_args)) =
   785         (case proxify_const s of
   786            SOME proxy_base =>
   787            if top_level orelse is_setting_higher_order format type_sys then
   788              case (top_level, s) of
   789                (_, "c_False") => (`I tptp_false, [])
   790              | (_, "c_True") => (`I tptp_true, [])
   791              | (false, "c_Not") => (`I tptp_not, [])
   792              | (false, "c_conj") => (`I tptp_and, [])
   793              | (false, "c_disj") => (`I tptp_or, [])
   794              | (false, "c_implies") => (`I tptp_implies, [])
   795              | (false, s) =>
   796                if is_tptp_equal s then (`I tptp_equal, [])
   797                else (proxy_base |>> prefix const_prefix, T_args)
   798              | _ => (name, [])
   799            else
   800              (proxy_base |>> prefix const_prefix, T_args)
   801           | NONE => (name, T_args))
   802         |> (fn (name, T_args) => CombConst (name, T, T_args))
   803       | intro _ tm = tm
   804   in intro true end
   805 
   806 fun combformula_from_prop thy format type_sys eq_as_iff =
   807   let
   808     fun do_term bs t atomic_types =
   809       combterm_from_term thy bs (Envir.eta_contract t)
   810       |>> (introduce_proxies format type_sys #> AAtom)
   811       ||> union (op =) atomic_types
   812     fun do_quant bs q s T t' =
   813       let val s = singleton (Name.variant_list (map fst bs)) s in
   814         do_formula ((s, T) :: bs) t'
   815         #>> mk_aquant q [(`make_bound_var s, SOME T)]
   816       end
   817     and do_conn bs c t1 t2 =
   818       do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
   819     and do_formula bs t =
   820       case t of
   821         @{const Trueprop} $ t1 => do_formula bs t1
   822       | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
   823       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   824         do_quant bs AForall s T t'
   825       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   826         do_quant bs AExists s T t'
   827       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
   828       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
   829       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
   830       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   831         if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
   832       | _ => do_term bs t
   833   in do_formula [] end
   834 
   835 fun presimplify_term _ [] t = t
   836   | presimplify_term ctxt presimp_consts t =
   837     t |> exists_Const (member (op =) presimp_consts o fst) t
   838          ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
   839             #> Meson.presimplify ctxt
   840             #> prop_of)
   841 
   842 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
   843 fun conceal_bounds Ts t =
   844   subst_bounds (map (Free o apfst concealed_bound_name)
   845                     (0 upto length Ts - 1 ~~ Ts), t)
   846 fun reveal_bounds Ts =
   847   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   848                     (0 upto length Ts - 1 ~~ Ts))
   849 
   850 fun is_fun_equality (@{const_name HOL.eq},
   851                      Type (_, [Type (@{type_name fun}, _), _])) = true
   852   | is_fun_equality _ = false
   853 
   854 fun extensionalize_term ctxt t =
   855   if exists_Const is_fun_equality t then
   856     let val thy = Proof_Context.theory_of ctxt in
   857       t |> cterm_of thy |> Meson.extensionalize_conv ctxt
   858         |> prop_of |> Logic.dest_equals |> snd
   859     end
   860   else
   861     t
   862 
   863 fun introduce_combinators_in_term ctxt kind t =
   864   let val thy = Proof_Context.theory_of ctxt in
   865     if Meson.is_fol_term thy t then
   866       t
   867     else
   868       let
   869         fun aux Ts t =
   870           case t of
   871             @{const Not} $ t1 => @{const Not} $ aux Ts t1
   872           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   873             t0 $ Abs (s, T, aux (T :: Ts) t')
   874           | (t0 as Const (@{const_name All}, _)) $ t1 =>
   875             aux Ts (t0 $ eta_expand Ts t1 1)
   876           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   877             t0 $ Abs (s, T, aux (T :: Ts) t')
   878           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   879             aux Ts (t0 $ eta_expand Ts t1 1)
   880           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   881           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   882           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   883           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   884               $ t1 $ t2 =>
   885             t0 $ aux Ts t1 $ aux Ts t2
   886           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   887                    t
   888                  else
   889                    t |> conceal_bounds Ts
   890                      |> Envir.eta_contract
   891                      |> cterm_of thy
   892                      |> Meson_Clausify.introduce_combinators_in_cterm
   893                      |> prop_of |> Logic.dest_equals |> snd
   894                      |> reveal_bounds Ts
   895         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   896       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   897       handle THM _ =>
   898              (* A type variable of sort "{}" will make abstraction fail. *)
   899              if kind = Conjecture then HOLogic.false_const
   900              else HOLogic.true_const
   901   end
   902 
   903 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   904    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
   905 fun freeze_term t =
   906   let
   907     fun aux (t $ u) = aux t $ aux u
   908       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   909       | aux (Var ((s, i), T)) =
   910         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   911       | aux t = t
   912   in t |> exists_subterm is_Var t ? aux end
   913 
   914 fun preprocess_prop ctxt presimp_consts kind t =
   915   let
   916     val thy = Proof_Context.theory_of ctxt
   917     val t = t |> Envir.beta_eta_contract
   918               |> transform_elim_prop
   919               |> Object_Logic.atomize_term thy
   920     val need_trueprop = (fastype_of t = @{typ bool})
   921   in
   922     t |> need_trueprop ? HOLogic.mk_Trueprop
   923       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
   924       |> extensionalize_term ctxt
   925       |> presimplify_term ctxt presimp_consts
   926       |> perhaps (try (HOLogic.dest_Trueprop))
   927       |> introduce_combinators_in_term ctxt kind
   928   end
   929 
   930 (* making fact and conjecture formulas *)
   931 fun make_formula thy format type_sys eq_as_iff name loc kind t =
   932   let
   933     val (combformula, atomic_types) =
   934       combformula_from_prop thy format type_sys eq_as_iff t []
   935   in
   936     {name = name, locality = loc, kind = kind, combformula = combformula,
   937      atomic_types = atomic_types}
   938   end
   939 
   940 fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
   941               ((name, loc), t) =
   942   let val thy = Proof_Context.theory_of ctxt in
   943     case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
   944            |> make_formula thy format type_sys (eq_as_iff andalso format <> CNF)
   945                            name loc Axiom of
   946       formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
   947       if s = tptp_true then NONE else SOME formula
   948     | formula => SOME formula
   949   end
   950 
   951 fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
   952   let
   953     val thy = Proof_Context.theory_of ctxt
   954     val last = length ts - 1
   955   in
   956     map2 (fn j => fn t =>
   957              let
   958                val (kind, maybe_negate) =
   959                  if j = last then
   960                    (Conjecture, I)
   961                  else
   962                    (prem_kind,
   963                     if prem_kind = Conjecture then update_combformula mk_anot
   964                     else I)
   965               in
   966                 t |> preproc ?
   967                      (preprocess_prop ctxt presimp_consts kind #> freeze_term)
   968                   |> make_formula thy format type_sys (format <> CNF)
   969                                   (string_of_int j) Local kind
   970                   |> maybe_negate
   971               end)
   972          (0 upto last) ts
   973   end
   974 
   975 (** Finite and infinite type inference **)
   976 
   977 fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
   978   | deep_freeze_atyp T = T
   979 val deep_freeze_type = map_atyps deep_freeze_atyp
   980 
   981 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
   982    dangerous because their "exhaust" properties can easily lead to unsound ATP
   983    proofs. On the other hand, all HOL infinite types can be given the same
   984    models in first-order logic (via Löwenheim-Skolem). *)
   985 
   986 fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
   987     exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
   988   | should_encode_type _ _ All_Types _ = true
   989   | should_encode_type ctxt _ Fin_Nonmono_Types T =
   990     is_type_surely_finite ctxt false T
   991   | should_encode_type _ _ _ _ = false
   992 
   993 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
   994                              should_predicate_on_var T =
   995     (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
   996     should_encode_type ctxt nonmono_Ts level T
   997   | should_predicate_on_type _ _ _ _ _ = false
   998 
   999 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
  1000     String.isPrefix bound_var_prefix s
  1001   | is_var_or_bound_var (CombVar _) = true
  1002   | is_var_or_bound_var _ = false
  1003 
  1004 datatype tag_site =
  1005   Top_Level of bool option |
  1006   Eq_Arg of bool option |
  1007   Elsewhere
  1008 
  1009 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
  1010   | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
  1011                          u T =
  1012     (case heaviness of
  1013        Heavyweight => should_encode_type ctxt nonmono_Ts level T
  1014      | Lightweight =>
  1015        case (site, is_var_or_bound_var u) of
  1016          (Eq_Arg pos, true) =>
  1017          (* The first disjunct prevents a subtle soundness issue explained in
  1018             Blanchette's Ph.D. thesis. See also
  1019             "formula_lines_for_lightweight_tags_sym_decl". *)
  1020          (pos <> SOME false andalso poly = Polymorphic andalso
  1021           level <> All_Types andalso heaviness = Lightweight andalso
  1022           exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
  1023          should_encode_type ctxt nonmono_Ts level T
  1024        | _ => false)
  1025   | should_tag_with_type _ _ _ _ _ _ = false
  1026 
  1027 fun homogenized_type ctxt nonmono_Ts level =
  1028   let
  1029     val should_encode = should_encode_type ctxt nonmono_Ts level
  1030     fun homo 0 T = if should_encode T then T else homo_infinite_type
  1031       | homo ary (Type (@{type_name fun}, [T1, T2])) =
  1032         homo 0 T1 --> homo (ary - 1) T2
  1033       | homo _ _ = raise Fail "expected function type"
  1034   in homo end
  1035 
  1036 (** "hBOOL" and "hAPP" **)
  1037 
  1038 type sym_info =
  1039   {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
  1040 
  1041 fun add_combterm_syms_to_table ctxt explicit_apply =
  1042   let
  1043     fun consider_var_arity const_T var_T max_ary =
  1044       let
  1045         fun iter ary T =
  1046           if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
  1047              type_instance ctxt (T, var_T) then
  1048             ary
  1049           else
  1050             iter (ary + 1) (range_type T)
  1051       in iter 0 const_T end
  1052     fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1053       if explicit_apply = NONE andalso
  1054          (can dest_funT T orelse T = @{typ bool}) then
  1055         let
  1056           val bool_vars' = bool_vars orelse body_type T = @{typ bool}
  1057           fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
  1058             {pred_sym = pred_sym andalso not bool_vars',
  1059              min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
  1060              max_ary = max_ary, types = types}
  1061           val fun_var_Ts' =
  1062             fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
  1063         in
  1064           if bool_vars' = bool_vars andalso
  1065              pointer_eq (fun_var_Ts', fun_var_Ts) then
  1066             accum
  1067           else
  1068             ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
  1069         end
  1070       else
  1071         accum
  1072     fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1073       let val (head, args) = strip_combterm_comb tm in
  1074         (case head of
  1075            CombConst ((s, _), T, _) =>
  1076            if String.isPrefix bound_var_prefix s then
  1077              add_var_or_bound_var T accum
  1078            else
  1079              let val ary = length args in
  1080                ((bool_vars, fun_var_Ts),
  1081                 case Symtab.lookup sym_tab s of
  1082                   SOME {pred_sym, min_ary, max_ary, types} =>
  1083                   let
  1084                     val pred_sym =
  1085                       pred_sym andalso top_level andalso not bool_vars
  1086                     val types' = types |> insert_type ctxt I T
  1087                     val min_ary =
  1088                       if is_some explicit_apply orelse
  1089                          pointer_eq (types', types) then
  1090                         min_ary
  1091                       else
  1092                         fold (consider_var_arity T) fun_var_Ts min_ary
  1093                   in
  1094                     Symtab.update (s, {pred_sym = pred_sym,
  1095                                        min_ary = Int.min (ary, min_ary),
  1096                                        max_ary = Int.max (ary, max_ary),
  1097                                        types = types'})
  1098                                   sym_tab
  1099                   end
  1100                 | NONE =>
  1101                   let
  1102                     val pred_sym = top_level andalso not bool_vars
  1103                     val min_ary =
  1104                       case explicit_apply of
  1105                         SOME true => 0
  1106                       | SOME false => ary
  1107                       | NONE => fold (consider_var_arity T) fun_var_Ts ary
  1108                   in
  1109                     Symtab.update_new (s, {pred_sym = pred_sym,
  1110                                            min_ary = min_ary, max_ary = ary,
  1111                                            types = [T]})
  1112                                       sym_tab
  1113                   end)
  1114              end
  1115          | CombVar (_, T) => add_var_or_bound_var T accum
  1116          | _ => accum)
  1117         |> fold (add false) args
  1118       end
  1119   in add true end
  1120 fun add_fact_syms_to_table ctxt explicit_apply =
  1121   fact_lift (formula_fold NONE
  1122                           (K (add_combterm_syms_to_table ctxt explicit_apply)))
  1123 
  1124 val default_sym_tab_entries : (string * sym_info) list =
  1125   (prefixed_predicator_name,
  1126    {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
  1127   ([tptp_false, tptp_true]
  1128    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
  1129   ([tptp_equal, tptp_old_equal]
  1130    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
  1131 
  1132 fun sym_table_for_facts ctxt explicit_apply facts =
  1133   ((false, []), Symtab.empty)
  1134   |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
  1135   |> fold Symtab.update default_sym_tab_entries
  1136 
  1137 fun min_arity_of sym_tab s =
  1138   case Symtab.lookup sym_tab s of
  1139     SOME ({min_ary, ...} : sym_info) => min_ary
  1140   | NONE =>
  1141     case strip_prefix_and_unascii const_prefix s of
  1142       SOME s =>
  1143       let val s = s |> unmangled_const_name |> invert_const in
  1144         if s = predicator_name then 1
  1145         else if s = app_op_name then 2
  1146         else if s = type_pred_name then 1
  1147         else 0
  1148       end
  1149     | NONE => 0
  1150 
  1151 (* True if the constant ever appears outside of the top-level position in
  1152    literals, or if it appears with different arities (e.g., because of different
  1153    type instantiations). If false, the constant always receives all of its
  1154    arguments and is used as a predicate. *)
  1155 fun is_pred_sym sym_tab s =
  1156   case Symtab.lookup sym_tab s of
  1157     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
  1158     pred_sym andalso min_ary = max_ary
  1159   | NONE => false
  1160 
  1161 val predicator_combconst =
  1162   CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
  1163 fun predicator tm = CombApp (predicator_combconst, tm)
  1164 
  1165 fun introduce_predicators_in_combterm sym_tab tm =
  1166   case strip_combterm_comb tm of
  1167     (CombConst ((s, _), _, _), _) =>
  1168     if is_pred_sym sym_tab s then tm else predicator tm
  1169   | _ => predicator tm
  1170 
  1171 fun list_app head args = fold (curry (CombApp o swap)) args head
  1172 
  1173 val app_op = `make_fixed_const app_op_name
  1174 
  1175 fun explicit_app arg head =
  1176   let
  1177     val head_T = combtyp_of head
  1178     val (arg_T, res_T) = dest_funT head_T
  1179     val explicit_app =
  1180       CombConst (app_op, head_T --> head_T, [arg_T, res_T])
  1181   in list_app explicit_app [head, arg] end
  1182 fun list_explicit_app head args = fold explicit_app args head
  1183 
  1184 fun introduce_explicit_apps_in_combterm sym_tab =
  1185   let
  1186     fun aux tm =
  1187       case strip_combterm_comb tm of
  1188         (head as CombConst ((s, _), _, _), args) =>
  1189         args |> map aux
  1190              |> chop (min_arity_of sym_tab s)
  1191              |>> list_app head
  1192              |-> list_explicit_app
  1193       | (head, args) => list_explicit_app head (map aux args)
  1194   in aux end
  1195 
  1196 fun chop_fun 0 T = ([], T)
  1197   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
  1198     chop_fun (n - 1) ran_T |>> cons dom_T
  1199   | chop_fun _ _ = raise Fail "unexpected non-function"
  1200 
  1201 fun filter_type_args _ _ _ [] = []
  1202   | filter_type_args thy s arity T_args =
  1203     let
  1204       (* will throw "TYPE" for pseudo-constants *)
  1205       val U = if s = app_op_name then
  1206                 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
  1207               else
  1208                 s |> Sign.the_const_type thy
  1209     in
  1210       case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
  1211         [] => []
  1212       | res_U_vars =>
  1213         let val U_args = (s, U) |> Sign.const_typargs thy in
  1214           U_args ~~ T_args
  1215           |> map (fn (U, T) =>
  1216                      if member (op =) res_U_vars (dest_TVar U) then T
  1217                      else dummyT)
  1218         end
  1219     end
  1220     handle TYPE _ => T_args
  1221 
  1222 fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
  1223   let
  1224     val thy = Proof_Context.theory_of ctxt
  1225     fun aux arity (CombApp (tm1, tm2)) =
  1226         CombApp (aux (arity + 1) tm1, aux 0 tm2)
  1227       | aux arity (CombConst (name as (s, _), T, T_args)) =
  1228         (case strip_prefix_and_unascii const_prefix s of
  1229            NONE => (name, T_args)
  1230          | SOME s'' =>
  1231            let
  1232              val s'' = invert_const s''
  1233              fun filtered_T_args false = T_args
  1234                | filtered_T_args true = filter_type_args thy s'' arity T_args
  1235            in
  1236              case type_arg_policy type_sys s'' of
  1237                Explicit_Type_Args drop_args =>
  1238                (name, filtered_T_args drop_args)
  1239              | Mangled_Type_Args drop_args =>
  1240                (mangled_const_name format type_sys (filtered_T_args drop_args)
  1241                                    name, [])
  1242              | No_Type_Args => (name, [])
  1243            end)
  1244         |> (fn (name, T_args) => CombConst (name, T, T_args))
  1245       | aux _ tm = tm
  1246   in aux 0 end
  1247 
  1248 fun repair_combterm ctxt format type_sys sym_tab =
  1249   not (is_setting_higher_order format type_sys)
  1250   ? (introduce_explicit_apps_in_combterm sym_tab
  1251      #> introduce_predicators_in_combterm sym_tab)
  1252   #> enforce_type_arg_policy_in_combterm ctxt format type_sys
  1253 fun repair_fact ctxt format type_sys sym_tab =
  1254   update_combformula (formula_map
  1255       (repair_combterm ctxt format type_sys sym_tab))
  1256 
  1257 (** Helper facts **)
  1258 
  1259 (* The Boolean indicates that a fairly sound type encoding is needed. *)
  1260 val helper_table =
  1261   [(("COMBI", false), @{thms Meson.COMBI_def}),
  1262    (("COMBK", false), @{thms Meson.COMBK_def}),
  1263    (("COMBB", false), @{thms Meson.COMBB_def}),
  1264    (("COMBC", false), @{thms Meson.COMBC_def}),
  1265    (("COMBS", false), @{thms Meson.COMBS_def}),
  1266    (("fequal", true),
  1267     (* This is a lie: Higher-order equality doesn't need a sound type encoding.
  1268        However, this is done so for backward compatibility: Including the
  1269        equality helpers by default in Metis breaks a few existing proofs. *)
  1270     @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1271            fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
  1272    (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
  1273    (("fFalse", true), @{thms True_or_False}),
  1274    (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
  1275    (("fTrue", true), @{thms True_or_False}),
  1276    (("fNot", false),
  1277     @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1278            fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
  1279    (("fconj", false),
  1280     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
  1281         by (unfold fconj_def) fast+}),
  1282    (("fdisj", false),
  1283     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
  1284         by (unfold fdisj_def) fast+}),
  1285    (("fimplies", false),
  1286     @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
  1287         by (unfold fimplies_def) fast+}),
  1288    (("If", true), @{thms if_True if_False True_or_False})]
  1289   |> map (apsnd (map zero_var_indexes))
  1290 
  1291 val type_tag = `make_fixed_const type_tag_name
  1292 
  1293 fun type_tag_idempotence_fact () =
  1294   let
  1295     fun var s = ATerm (`I s, [])
  1296     fun tag tm = ATerm (type_tag, [var "T", tm])
  1297     val tagged_a = tag (var "A")
  1298   in
  1299     Formula (type_tag_idempotence_helper_name, Axiom,
  1300              AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
  1301              |> close_formula_universally, simp_info, NONE)
  1302   end
  1303 
  1304 fun should_specialize_helper type_sys t =
  1305   case general_type_arg_policy type_sys of
  1306     Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
  1307   | _ => false
  1308 
  1309 fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
  1310   case strip_prefix_and_unascii const_prefix s of
  1311     SOME mangled_s =>
  1312     let
  1313       val thy = Proof_Context.theory_of ctxt
  1314       val unmangled_s = mangled_s |> unmangled_const_name
  1315       fun dub_and_inst needs_fairly_sound (th, j) =
  1316         ((unmangled_s ^ "_" ^ string_of_int j ^
  1317           (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
  1318           (if needs_fairly_sound then typed_helper_suffix
  1319            else untyped_helper_suffix),
  1320           Helper),
  1321          let val t = th |> prop_of in
  1322            t |> should_specialize_helper type_sys t
  1323                 ? (case types of
  1324                      [T] => specialize_type thy (invert_const unmangled_s, T)
  1325                    | _ => I)
  1326          end)
  1327       val make_facts =
  1328         map_filter (make_fact ctxt format type_sys false false [])
  1329       val fairly_sound = is_type_sys_fairly_sound type_sys
  1330     in
  1331       helper_table
  1332       |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
  1333                   if helper_s <> unmangled_s orelse
  1334                      (needs_fairly_sound andalso not fairly_sound) then
  1335                     []
  1336                   else
  1337                     ths ~~ (1 upto length ths)
  1338                     |> map (dub_and_inst needs_fairly_sound)
  1339                     |> make_facts)
  1340     end
  1341   | NONE => []
  1342 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
  1343   Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
  1344                   []
  1345 
  1346 (***************************************************************)
  1347 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
  1348 (***************************************************************)
  1349 
  1350 fun set_insert (x, s) = Symtab.update (x, ()) s
  1351 
  1352 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
  1353 
  1354 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
  1355 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
  1356 
  1357 fun classes_of_terms get_Ts =
  1358   map (map snd o get_Ts)
  1359   #> List.foldl add_classes Symtab.empty
  1360   #> delete_type #> Symtab.keys
  1361 
  1362 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
  1363 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
  1364 
  1365 fun fold_type_constrs f (Type (s, Ts)) x =
  1366     fold (fold_type_constrs f) Ts (f (s, x))
  1367   | fold_type_constrs _ _ x = x
  1368 
  1369 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
  1370 fun add_type_constrs_in_term thy =
  1371   let
  1372     fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
  1373       | add (t $ u) = add t #> add u
  1374       | add (Const (x as (s, _))) =
  1375         if String.isPrefix skolem_const_prefix s then I
  1376         else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
  1377       | add (Abs (_, _, u)) = add u
  1378       | add _ = I
  1379   in add end
  1380 
  1381 fun type_constrs_of_terms thy ts =
  1382   Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
  1383 
  1384 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
  1385                        facts =
  1386   let
  1387     val thy = Proof_Context.theory_of ctxt
  1388     val fact_ts = facts |> map snd
  1389     val presimp_consts = Meson.presimplified_consts ctxt
  1390     val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
  1391     val (facts, fact_names) =
  1392       facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
  1393             |> map_filter (try (apfst the))
  1394             |> ListPair.unzip
  1395     (* Remove existing facts from the conjecture, as this can dramatically
  1396        boost an ATP's performance (for some reason). *)
  1397     val hyp_ts =
  1398       hyp_ts
  1399       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
  1400     val goal_t = Logic.list_implies (hyp_ts, concl_t)
  1401     val all_ts = goal_t :: fact_ts
  1402     val subs = tfree_classes_of_terms all_ts
  1403     val supers = tvar_classes_of_terms all_ts
  1404     val tycons = type_constrs_of_terms thy all_ts
  1405     val conjs =
  1406       hyp_ts @ [concl_t]
  1407       |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
  1408     val (supers', arity_clauses) =
  1409       if level_of_type_sys type_sys = No_Types then ([], [])
  1410       else make_arity_clauses thy tycons supers
  1411     val class_rel_clauses = make_class_rel_clauses thy subs supers'
  1412   in
  1413     (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
  1414   end
  1415 
  1416 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
  1417     (true, ATerm (class, [ATerm (name, [])]))
  1418   | fo_literal_from_type_literal (TyLitFree (class, name)) =
  1419     (true, ATerm (class, [ATerm (name, [])]))
  1420 
  1421 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
  1422 
  1423 val type_pred = `make_fixed_const type_pred_name
  1424 
  1425 fun type_pred_combterm ctxt format type_sys T tm =
  1426   CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
  1427            |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
  1428 
  1429 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
  1430   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
  1431     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
  1432 fun should_predicate_on_var_in_formula pos phi (SOME true) name =
  1433     formula_fold pos (is_var_positively_naked_in_term name) phi false
  1434   | should_predicate_on_var_in_formula _ _ _ _ = true
  1435 
  1436 fun mk_const_aterm format type_sys x T_args args =
  1437   ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
  1438 
  1439 fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
  1440   CombConst (type_tag, T --> T, [T])
  1441   |> enforce_type_arg_policy_in_combterm ctxt format type_sys
  1442   |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
  1443   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
  1444 and term_from_combterm ctxt format nonmono_Ts type_sys =
  1445   let
  1446     fun aux site u =
  1447       let
  1448         val (head, args) = strip_combterm_comb u
  1449         val (x as (s, _), T_args) =
  1450           case head of
  1451             CombConst (name, _, T_args) => (name, T_args)
  1452           | CombVar (name, _) => (name, [])
  1453           | CombApp _ => raise Fail "impossible \"CombApp\""
  1454         val (pos, arg_site) =
  1455           case site of
  1456             Top_Level pos =>
  1457             (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
  1458           | Eq_Arg pos => (pos, Elsewhere)
  1459           | Elsewhere => (NONE, Elsewhere)
  1460         val t = mk_const_aterm format type_sys x T_args
  1461                     (map (aux arg_site) args)
  1462         val T = combtyp_of u
  1463       in
  1464         t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
  1465                 tag_with_type ctxt format nonmono_Ts type_sys pos T
  1466               else
  1467                 I)
  1468       end
  1469   in aux end
  1470 and formula_from_combformula ctxt format nonmono_Ts type_sys
  1471                              should_predicate_on_var =
  1472   let
  1473     fun do_term pos =
  1474       term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
  1475     val do_bound_type =
  1476       case type_sys of
  1477         Simple_Types level =>
  1478         homogenized_type ctxt nonmono_Ts level 0
  1479         #> mangled_type format type_sys false 0 #> SOME
  1480       | _ => K NONE
  1481     fun do_out_of_bound_type pos phi universal (name, T) =
  1482       if should_predicate_on_type ctxt nonmono_Ts type_sys
  1483              (fn () => should_predicate_on_var pos phi universal name) T then
  1484         CombVar (name, T)
  1485         |> type_pred_combterm ctxt format type_sys T
  1486         |> do_term pos |> AAtom |> SOME
  1487       else
  1488         NONE
  1489     fun do_formula pos (AQuant (q, xs, phi)) =
  1490         let
  1491           val phi = phi |> do_formula pos
  1492           val universal = Option.map (q = AExists ? not) pos
  1493         in
  1494           AQuant (q, xs |> map (apsnd (fn NONE => NONE
  1495                                         | SOME T => do_bound_type T)),
  1496                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
  1497                       (map_filter
  1498                            (fn (_, NONE) => NONE
  1499                              | (s, SOME T) =>
  1500                                do_out_of_bound_type pos phi universal (s, T))
  1501                            xs)
  1502                       phi)
  1503         end
  1504       | do_formula pos (AConn conn) = aconn_map pos do_formula conn
  1505       | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
  1506   in do_formula end
  1507 
  1508 fun bound_tvars type_sys Ts =
  1509   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
  1510                 (type_literals_for_types type_sys add_sorts_on_tvar Ts))
  1511 
  1512 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
  1513    of monomorphization). The TPTP explicitly forbids name clashes, and some of
  1514    the remote provers might care. *)
  1515 fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
  1516         type_sys (j, {name, locality, kind, combformula, atomic_types}) =
  1517   (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
  1518    kind,
  1519    combformula
  1520    |> close_combformula_universally
  1521    |> formula_from_combformula ctxt format nonmono_Ts type_sys
  1522                                should_predicate_on_var_in_formula
  1523                                (if pos then SOME true else NONE)
  1524    |> bound_tvars type_sys atomic_types
  1525    |> close_formula_universally,
  1526    NONE,
  1527    case locality of
  1528      Intro => intro_info
  1529    | Elim => elim_info
  1530    | Simp => simp_info
  1531    | _ => NONE)
  1532   |> Formula
  1533 
  1534 fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
  1535                                        : class_rel_clause) =
  1536   let val ty_arg = ATerm (`I "T", []) in
  1537     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
  1538              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
  1539                                AAtom (ATerm (superclass, [ty_arg]))])
  1540              |> close_formula_universally, intro_info, NONE)
  1541   end
  1542 
  1543 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
  1544     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
  1545   | fo_literal_from_arity_literal (TVarLit (c, sort)) =
  1546     (false, ATerm (c, [ATerm (sort, [])]))
  1547 
  1548 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
  1549                                    : arity_clause) =
  1550   Formula (arity_clause_prefix ^ name, Axiom,
  1551            mk_ahorn (map (formula_from_fo_literal o apfst not
  1552                           o fo_literal_from_arity_literal) prem_lits)
  1553                     (formula_from_fo_literal
  1554                          (fo_literal_from_arity_literal concl_lits))
  1555            |> close_formula_universally, intro_info, NONE)
  1556 
  1557 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
  1558         ({name, kind, combformula, atomic_types, ...} : translated_formula) =
  1559   Formula (conjecture_prefix ^ name, kind,
  1560            formula_from_combformula ctxt format nonmono_Ts type_sys
  1561                should_predicate_on_var_in_formula (SOME false)
  1562                (close_combformula_universally combformula)
  1563            |> bound_tvars type_sys atomic_types
  1564            |> close_formula_universally, NONE, NONE)
  1565 
  1566 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
  1567   atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
  1568                |> map fo_literal_from_type_literal
  1569 
  1570 fun formula_line_for_free_type j lit =
  1571   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
  1572            formula_from_fo_literal lit, NONE, NONE)
  1573 fun formula_lines_for_free_types type_sys facts =
  1574   let
  1575     val litss = map (free_type_literals type_sys) facts
  1576     val lits = fold (union (op =)) litss []
  1577   in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
  1578 
  1579 (** Symbol declarations **)
  1580 
  1581 fun should_declare_sym type_sys pred_sym s =
  1582   is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
  1583   (case type_sys of
  1584      Simple_Types _ => true
  1585    | Tags (_, _, Lightweight) => true
  1586    | _ => not pred_sym)
  1587 
  1588 fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
  1589   let
  1590     fun add_combterm in_conj tm =
  1591       let val (head, args) = strip_combterm_comb tm in
  1592         (case head of
  1593            CombConst ((s, s'), T, T_args) =>
  1594            let val pred_sym = is_pred_sym repaired_sym_tab s in
  1595              if should_declare_sym type_sys pred_sym s then
  1596                Symtab.map_default (s, [])
  1597                    (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
  1598                                          in_conj))
  1599              else
  1600                I
  1601            end
  1602          | _ => I)
  1603         #> fold (add_combterm in_conj) args
  1604       end
  1605     fun add_fact in_conj =
  1606       fact_lift (formula_fold NONE (K (add_combterm in_conj)))
  1607   in
  1608     Symtab.empty
  1609     |> is_type_sys_fairly_sound type_sys
  1610        ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
  1611   end
  1612 
  1613 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
  1614    out with monotonicity" paper presented at CADE 2011. *)
  1615 fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
  1616   | add_combterm_nonmonotonic_types ctxt level sound locality _
  1617         (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
  1618                            tm2)) =
  1619     (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
  1620      (case level of
  1621         Noninf_Nonmono_Types =>
  1622         not (is_locality_global locality) orelse
  1623         not (is_type_surely_infinite ctxt sound T)
  1624       | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
  1625       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
  1626   | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I
  1627 fun add_fact_nonmonotonic_types ctxt level sound
  1628         ({kind, locality, combformula, ...} : translated_formula) =
  1629   formula_fold (SOME (kind <> Conjecture))
  1630                (add_combterm_nonmonotonic_types ctxt level sound locality)
  1631                combformula
  1632 fun nonmonotonic_types_for_facts ctxt type_sys sound facts =
  1633   let val level = level_of_type_sys type_sys in
  1634     if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
  1635       [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
  1636          (* We must add "bool" in case the helper "True_or_False" is added
  1637             later. In addition, several places in the code rely on the list of
  1638             nonmonotonic types not being empty. *)
  1639          |> insert_type ctxt I @{typ bool}
  1640     else
  1641       []
  1642   end
  1643 
  1644 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
  1645                       (s', T_args, T, pred_sym, ary, _) =
  1646   let
  1647     val (T_arg_Ts, level) =
  1648       case type_sys of
  1649         Simple_Types level => ([], level)
  1650       | _ => (replicate (length T_args) homo_infinite_type, No_Types)
  1651   in
  1652     Decl (sym_decl_prefix ^ s, (s, s'),
  1653           (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
  1654           |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
  1655   end
  1656 
  1657 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
  1658         poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) =
  1659   let
  1660     val (kind, maybe_negate) =
  1661       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  1662       else (Axiom, I)
  1663     val (arg_Ts, res_T) = chop_fun ary T
  1664     val num_args = length arg_Ts
  1665     val bound_names =
  1666       1 upto num_args |> map (`I o make_bound_var o string_of_int)
  1667     val bounds =
  1668       bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
  1669     val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
  1670     fun should_keep_arg_type T =
  1671       sym_needs_arg_types orelse
  1672       not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T)
  1673     val bound_Ts =
  1674       arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
  1675   in
  1676     Formula (preds_sym_formula_prefix ^ s ^
  1677              (if n > 1 then "_" ^ string_of_int j else ""), kind,
  1678              CombConst ((s, s'), T, T_args)
  1679              |> fold (curry (CombApp o swap)) bounds
  1680              |> type_pred_combterm ctxt format type_sys res_T
  1681              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
  1682              |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
  1683                                          (K (K (K (K true)))) (SOME true)
  1684              |> n > 1 ? bound_tvars type_sys (atyps_of T)
  1685              |> close_formula_universally
  1686              |> maybe_negate,
  1687              intro_info, NONE)
  1688   end
  1689 
  1690 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
  1691         poly_nonmono_Ts type_sys n s
  1692         (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  1693   let
  1694     val ident_base =
  1695       lightweight_tags_sym_formula_prefix ^ s ^
  1696       (if n > 1 then "_" ^ string_of_int j else "")
  1697     val (kind, maybe_negate) =
  1698       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  1699       else (Axiom, I)
  1700     val (arg_Ts, res_T) = chop_fun ary T
  1701     val bound_names =
  1702       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
  1703     val bounds = bound_names |> map (fn name => ATerm (name, []))
  1704     val cst = mk_const_aterm format type_sys (s, s') T_args
  1705     val atomic_Ts = atyps_of T
  1706     fun eq tms =
  1707       (if pred_sym then AConn (AIff, map AAtom tms)
  1708        else AAtom (ATerm (`I tptp_equal, tms)))
  1709       |> bound_tvars type_sys atomic_Ts
  1710       |> close_formula_universally
  1711       |> maybe_negate
  1712     (* See also "should_tag_with_type". *)
  1713     fun should_encode T =
  1714       should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
  1715       (case type_sys of
  1716          Tags (Polymorphic, level, Lightweight) =>
  1717          level <> All_Types andalso Monomorph.typ_has_tvars T
  1718        | _ => false)
  1719     val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE
  1720     val add_formula_for_res =
  1721       if should_encode res_T then
  1722         cons (Formula (ident_base ^ "_res", kind,
  1723                        eq [tag_with res_T (cst bounds), cst bounds],
  1724                        simp_info, NONE))
  1725       else
  1726         I
  1727     fun add_formula_for_arg k =
  1728       let val arg_T = nth arg_Ts k in
  1729         if should_encode arg_T then
  1730           case chop k bounds of
  1731             (bounds1, bound :: bounds2) =>
  1732             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
  1733                            eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
  1734                                cst bounds],
  1735                            simp_info, NONE))
  1736           | _ => raise Fail "expected nonempty tail"
  1737         else
  1738           I
  1739       end
  1740   in
  1741     [] |> not pred_sym ? add_formula_for_res
  1742        |> fold add_formula_for_arg (ary - 1 downto 0)
  1743   end
  1744 
  1745 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
  1746 
  1747 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
  1748                                 poly_nonmono_Ts type_sys (s, decls) =
  1749   case type_sys of
  1750     Simple_Types _ =>
  1751     decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
  1752   | Preds _ =>
  1753     let
  1754       val decls =
  1755         case decls of
  1756           decl :: (decls' as _ :: _) =>
  1757           let val T = result_type_of_decl decl in
  1758             if forall (curry (type_instance ctxt o swap) T
  1759                        o result_type_of_decl) decls' then
  1760               [decl]
  1761             else
  1762               decls
  1763           end
  1764         | _ => decls
  1765       val n = length decls
  1766       val decls =
  1767         decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys
  1768                                                   (K true)
  1769                          o result_type_of_decl)
  1770     in
  1771       (0 upto length decls - 1, decls)
  1772       |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
  1773                    nonmono_Ts poly_nonmono_Ts type_sys n s)
  1774     end
  1775   | Tags (_, _, heaviness) =>
  1776     (case heaviness of
  1777        Heavyweight => []
  1778      | Lightweight =>
  1779        let val n = length decls in
  1780          (0 upto n - 1 ~~ decls)
  1781          |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
  1782                       conj_sym_kind poly_nonmono_Ts type_sys n s)
  1783        end)
  1784 
  1785 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
  1786                                      poly_nonmono_Ts type_sys sym_decl_tab =
  1787   sym_decl_tab
  1788   |> Symtab.dest
  1789   |> sort_wrt fst
  1790   |> rpair []
  1791   |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
  1792                              nonmono_Ts poly_nonmono_Ts type_sys)
  1793 
  1794 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
  1795     poly <> Mangled_Monomorphic andalso
  1796     ((level = All_Types andalso heaviness = Lightweight) orelse
  1797      level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types)
  1798   | needs_type_tag_idempotence _ = false
  1799 
  1800 fun offset_of_heading_in_problem _ [] j = j
  1801   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
  1802     if heading = needle then j
  1803     else offset_of_heading_in_problem needle problem (j + length lines)
  1804 
  1805 val implicit_declsN = "Should-be-implicit typings"
  1806 val explicit_declsN = "Explicit typings"
  1807 val factsN = "Relevant facts"
  1808 val class_relsN = "Class relationships"
  1809 val aritiesN = "Arities"
  1810 val helpersN = "Helper facts"
  1811 val conjsN = "Conjectures"
  1812 val free_typesN = "Type variables"
  1813 
  1814 val explicit_apply = NONE (* for experimental purposes *)
  1815 
  1816 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys sound
  1817         exporter readable_names preproc hyp_ts concl_t facts =
  1818   let
  1819     val (format, type_sys) = choose_format [format] type_sys
  1820     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
  1821       translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
  1822                          facts
  1823     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
  1824     val nonmono_Ts =
  1825       conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys sound
  1826     val repair = repair_fact ctxt format type_sys sym_tab
  1827     val (conjs, facts) = (conjs, facts) |> pairself (map repair)
  1828     val repaired_sym_tab =
  1829       conjs @ facts |> sym_table_for_facts ctxt (SOME false)
  1830     val helpers =
  1831       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
  1832                        |> map repair
  1833     val poly_nonmono_Ts =
  1834       if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
  1835          polymorphism_of_type_sys type_sys <> Polymorphic then
  1836         nonmono_Ts
  1837       else
  1838         [TVar (("'a", 0), HOLogic.typeS)]
  1839     val sym_decl_lines =
  1840       (conjs, helpers @ facts)
  1841       |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
  1842       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
  1843                                                poly_nonmono_Ts type_sys
  1844     val helper_lines =
  1845       0 upto length helpers - 1 ~~ helpers
  1846       |> map (formula_line_for_fact ctxt format helper_prefix I false true
  1847                                     poly_nonmono_Ts type_sys)
  1848       |> (if needs_type_tag_idempotence type_sys then
  1849             cons (type_tag_idempotence_fact ())
  1850           else
  1851             I)
  1852     (* Reordering these might confuse the proof reconstruction code or the SPASS
  1853        FLOTTER hack. *)
  1854     val problem =
  1855       [(explicit_declsN, sym_decl_lines),
  1856        (factsN,
  1857         map (formula_line_for_fact ctxt format fact_prefix ascii_of
  1858                                    (not exporter) (not exporter) nonmono_Ts
  1859                                    type_sys)
  1860             (0 upto length facts - 1 ~~ facts)),
  1861        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
  1862        (aritiesN, map formula_line_for_arity_clause arity_clauses),
  1863        (helpersN, helper_lines),
  1864        (conjsN,
  1865         map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
  1866             conjs),
  1867        (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
  1868     val problem =
  1869       problem
  1870       |> (case format of
  1871             CNF => ensure_cnf_problem
  1872           | CNF_UEQ => filter_cnf_ueq_problem
  1873           | _ => I)
  1874       |> (if is_format_typed format then
  1875             declare_undeclared_syms_in_atp_problem type_decl_prefix
  1876                                                    implicit_declsN
  1877           else
  1878             I)
  1879     val (problem, pool) = problem |> nice_atp_problem readable_names
  1880     val helpers_offset = offset_of_heading_in_problem helpersN problem 0
  1881     val typed_helpers =
  1882       map_filter (fn (j, {name, ...}) =>
  1883                      if String.isSuffix typed_helper_suffix name then SOME j
  1884                      else NONE)
  1885                  ((helpers_offset + 1 upto helpers_offset + length helpers)
  1886                   ~~ helpers)
  1887     fun add_sym_arity (s, {min_ary, ...} : sym_info) =
  1888       if min_ary > 0 then
  1889         case strip_prefix_and_unascii const_prefix s of
  1890           SOME s => Symtab.insert (op =) (s, min_ary)
  1891         | NONE => I
  1892       else
  1893         I
  1894   in
  1895     (problem,
  1896      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
  1897      offset_of_heading_in_problem conjsN problem 0,
  1898      offset_of_heading_in_problem factsN problem 0,
  1899      fact_names |> Vector.fromList,
  1900      typed_helpers,
  1901      Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
  1902   end
  1903 
  1904 (* FUDGE *)
  1905 val conj_weight = 0.0
  1906 val hyp_weight = 0.1
  1907 val fact_min_weight = 0.2
  1908 val fact_max_weight = 1.0
  1909 val type_info_default_weight = 0.8
  1910 
  1911 fun add_term_weights weight (ATerm (s, tms)) =
  1912   is_tptp_user_symbol s ? Symtab.default (s, weight)
  1913   #> fold (add_term_weights weight) tms
  1914 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
  1915     formula_fold NONE (K (add_term_weights weight)) phi
  1916   | add_problem_line_weights _ _ = I
  1917 
  1918 fun add_conjectures_weights [] = I
  1919   | add_conjectures_weights conjs =
  1920     let val (hyps, conj) = split_last conjs in
  1921       add_problem_line_weights conj_weight conj
  1922       #> fold (add_problem_line_weights hyp_weight) hyps
  1923     end
  1924 
  1925 fun add_facts_weights facts =
  1926   let
  1927     val num_facts = length facts
  1928     fun weight_of j =
  1929       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
  1930                         / Real.fromInt num_facts
  1931   in
  1932     map weight_of (0 upto num_facts - 1) ~~ facts
  1933     |> fold (uncurry add_problem_line_weights)
  1934   end
  1935 
  1936 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
  1937 fun atp_problem_weights problem =
  1938   let val get = these o AList.lookup (op =) problem in
  1939     Symtab.empty
  1940     |> add_conjectures_weights (get free_typesN @ get conjsN)
  1941     |> add_facts_weights (get factsN)
  1942     |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
  1943             [explicit_declsN, class_relsN, aritiesN]
  1944     |> Symtab.dest
  1945     |> sort (prod_ord Real.compare string_ord o pairself swap)
  1946   end
  1947 
  1948 end;