src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
author blanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 42747 f132d13fcf75
parent 42742 369dfc819056
child 42750 c8b1d9ee3758
permissions -rw-r--r--
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_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 SLEDGEHAMMER_ATP_TRANSLATE =
    10 sig
    11   type 'a fo_term = 'a ATP_Problem.fo_term
    12   type formula_kind = ATP_Problem.formula_kind
    13   type 'a problem = 'a ATP_Problem.problem
    14   type locality = Sledgehammer_Filter.locality
    15 
    16   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    17   datatype type_level =
    18     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    19 
    20   datatype type_system =
    21     Simple_Types of type_level |
    22     Preds of polymorphism * type_level |
    23     Tags of polymorphism * type_level
    24 
    25   type translated_formula
    26 
    27   val readable_names : bool Config.T
    28   val fact_prefix : string
    29   val conjecture_prefix : string
    30   val predicator_base : string
    31   val explicit_app_base : string
    32   val type_pred_base : string
    33   val tff_type_prefix : string
    34   val type_sys_from_string : string -> type_system
    35   val polymorphism_of_type_sys : type_system -> polymorphism
    36   val level_of_type_sys : type_system -> type_level
    37   val is_type_sys_virtually_sound : type_system -> bool
    38   val is_type_sys_fairly_sound : type_system -> bool
    39   val num_atp_type_args : theory -> type_system -> string -> int
    40   val unmangled_const : string -> string * string fo_term list
    41   val translate_atp_fact :
    42     Proof.context -> bool -> (string * locality) * thm
    43     -> translated_formula option * ((string * locality) * thm)
    44   val prepare_atp_problem :
    45     Proof.context -> formula_kind -> formula_kind -> type_system -> bool
    46     -> term list -> term
    47     -> (translated_formula option * ((string * 'a) * thm)) list
    48     -> string problem * string Symtab.table * int * int
    49        * (string * 'a) list vector
    50   val atp_problem_weights : string problem -> (string * real) list
    51 end;
    52 
    53 structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
    54 struct
    55 
    56 open ATP_Problem
    57 open Metis_Translate
    58 open Sledgehammer_Util
    59 open Sledgehammer_Filter
    60 
    61 (* experimental *)
    62 val generate_useful_info = false
    63 
    64 (* Readable names are often much shorter, especially if types are mangled in
    65    names. Also, the logic for generating legal SNARK sort names is only
    66    implemented for readable names. Finally, readable names are, well, more
    67    readable. For these reason, they are enabled by default. *)
    68 val readable_names =
    69   Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
    70 
    71 val type_decl_prefix = "type_"
    72 val sym_decl_prefix = "sym_"
    73 val fact_prefix = "fact_"
    74 val conjecture_prefix = "conj_"
    75 val helper_prefix = "help_"
    76 val class_rel_clause_prefix = "crel_";
    77 val arity_clause_prefix = "arity_"
    78 val tfree_prefix = "tfree_"
    79 
    80 val predicator_base = "hBOOL"
    81 val explicit_app_base = "hAPP"
    82 val type_pred_base = "is"
    83 val tff_type_prefix = "ty_"
    84 
    85 fun make_tff_type s = tff_type_prefix ^ ascii_of s
    86 
    87 (* Freshness almost guaranteed! *)
    88 val sledgehammer_weak_prefix = "Sledgehammer:"
    89 
    90 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    91 datatype type_level =
    92   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    93 
    94 datatype type_system =
    95   Simple_Types of type_level |
    96   Preds of polymorphism * type_level |
    97   Tags of polymorphism * type_level
    98 
    99 fun try_unsuffixes ss s =
   100   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
   101 
   102 fun type_sys_from_string s =
   103   (case try (unprefix "poly_") s of
   104      SOME s => (SOME Polymorphic, s)
   105    | NONE =>
   106      case try (unprefix "mono_") s of
   107        SOME s => (SOME Monomorphic, s)
   108      | NONE =>
   109        case try (unprefix "mangled_") s of
   110          SOME s => (SOME Mangled_Monomorphic, s)
   111        | NONE => (NONE, s))
   112   ||> (fn s =>
   113           (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
   114           case try_unsuffixes ["?", "_query"] s of
   115             SOME s => (Nonmonotonic_Types, s)
   116           | NONE =>
   117             case try_unsuffixes ["!", "_bang"] s of
   118               SOME s => (Finite_Types, s)
   119             | NONE => (All_Types, s))
   120   |> (fn (poly, (level, core)) =>
   121          case (core, (poly, level)) of
   122            ("simple_types", (NONE, level)) => Simple_Types level
   123          | ("preds", (SOME poly, level)) => Preds (poly, level)
   124          | ("tags", (SOME poly, level)) => Tags (poly, level)
   125          | ("args", (SOME poly, All_Types (* naja *))) =>
   126            Preds (poly, Const_Arg_Types)
   127          | ("erased", (NONE, All_Types (* naja *))) =>
   128            Preds (Polymorphic, No_Types)
   129          | _ => error ("Unknown type system: " ^ quote s ^ "."))
   130 
   131 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
   132   | polymorphism_of_type_sys (Preds (poly, _)) = poly
   133   | polymorphism_of_type_sys (Tags (poly, _)) = poly
   134 
   135 fun level_of_type_sys (Simple_Types level) = level
   136   | level_of_type_sys (Preds (_, level)) = level
   137   | level_of_type_sys (Tags (_, level)) = level
   138 
   139 fun is_type_level_virtually_sound level =
   140   level = All_Types orelse level = Nonmonotonic_Types
   141 val is_type_sys_virtually_sound =
   142   is_type_level_virtually_sound o level_of_type_sys
   143 
   144 fun is_type_level_fairly_sound level =
   145   is_type_level_virtually_sound level orelse level = Finite_Types
   146 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
   147 
   148 fun is_type_level_partial level =
   149   level = Nonmonotonic_Types orelse level = Finite_Types
   150 
   151 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
   152   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
   153   | formula_map f (AAtom tm) = AAtom (f tm)
   154 
   155 fun formula_fold pos f =
   156   let
   157     fun aux pos (AQuant (_, _, phi)) = aux pos phi
   158       | aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi
   159       | aux pos (AConn (AImplies, [phi1, phi2])) =
   160         aux (Option.map not pos) phi1 #> aux pos phi2
   161       | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
   162       | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
   163       | aux _ (AConn (_, phis)) = fold (aux NONE) phis
   164       | aux pos (AAtom tm) = f pos tm
   165   in aux (SOME pos) end
   166 
   167 type translated_formula =
   168   {name: string,
   169    locality: locality,
   170    kind: formula_kind,
   171    combformula: (name, typ, combterm) formula,
   172    atomic_types: typ list}
   173 
   174 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
   175                           : translated_formula) =
   176   {name = name, locality = locality, kind = kind, combformula = f combformula,
   177    atomic_types = atomic_types} : translated_formula
   178 
   179 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
   180 
   181 val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
   182 
   183 fun should_omit_type_args type_sys s =
   184   s <> type_pred_base andalso s <> type_tag_name andalso
   185   (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse
   186    (case type_sys of
   187       Tags (_, All_Types) => true
   188     | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
   189            member (op =) boring_consts s))
   190 
   191 datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Type_Args
   192 
   193 fun general_type_arg_policy type_sys =
   194   if level_of_type_sys type_sys = No_Types then
   195     No_Type_Args
   196   else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
   197     Mangled_Type_Args
   198   else
   199     Explicit_Type_Args
   200 
   201 fun type_arg_policy type_sys s =
   202   if should_omit_type_args type_sys s then No_Type_Args
   203   else general_type_arg_policy type_sys
   204 
   205 fun num_atp_type_args thy type_sys s =
   206   if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
   207   else 0
   208 
   209 fun atp_type_literals_for_types type_sys kind Ts =
   210   if level_of_type_sys type_sys = No_Types then
   211     []
   212   else
   213     Ts |> type_literals_for_types
   214        |> filter (fn TyLitVar _ => kind <> Conjecture
   215                    | TyLitFree _ => kind = Conjecture)
   216 
   217 fun mk_anot phi = AConn (ANot, [phi])
   218 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
   219 fun mk_aconns c phis =
   220   let val (phis', phi') = split_last phis in
   221     fold_rev (mk_aconn c) phis' phi'
   222   end
   223 fun mk_ahorn [] phi = phi
   224   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
   225 fun mk_aquant _ [] phi = phi
   226   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
   227     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
   228   | mk_aquant q xs phi = AQuant (q, xs, phi)
   229 
   230 fun close_universally atom_vars phi =
   231   let
   232     fun formula_vars bounds (AQuant (_, xs, phi)) =
   233         formula_vars (map fst xs @ bounds) phi
   234       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   235       | formula_vars bounds (AAtom tm) =
   236         union (op =) (atom_vars tm []
   237                       |> filter_out (member (op =) bounds o fst))
   238   in mk_aquant AForall (formula_vars [] phi []) phi end
   239 
   240 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
   241   | combterm_vars (CombConst _) = I
   242   | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
   243 fun close_combformula_universally phi = close_universally combterm_vars phi
   244 
   245 fun term_vars (ATerm (name as (s, _), tms)) =
   246   is_atp_variable s ? insert (op =) (name, NONE)
   247   #> fold term_vars tms
   248 fun close_formula_universally phi = close_universally term_vars phi
   249 
   250 fun fo_term_from_typ (Type (s, Ts)) =
   251     ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts)
   252   | fo_term_from_typ (TFree (s, _)) =
   253     ATerm (`make_fixed_type_var s, [])
   254   | fo_term_from_typ (TVar ((x as (s, _)), _)) =
   255     ATerm ((make_schematic_type_var x, s), [])
   256 
   257 (* This shouldn't clash with anything else. *)
   258 val mangled_type_sep = "\000"
   259 
   260 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   261   | generic_mangled_type_name f (ATerm (name, tys)) =
   262     f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")"
   263 val mangled_type_name =
   264   fo_term_from_typ
   265   #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),
   266                 generic_mangled_type_name snd ty))
   267 
   268 fun generic_mangled_type_suffix f g Ts =
   269   fold_rev (curry (op ^) o g o prefix mangled_type_sep
   270             o generic_mangled_type_name f) Ts ""
   271 fun mangled_const_name T_args (s, s') =
   272   let val ty_args = map fo_term_from_typ T_args in
   273     (s ^ generic_mangled_type_suffix fst ascii_of ty_args,
   274      s' ^ generic_mangled_type_suffix snd I ty_args)
   275   end
   276 
   277 val parse_mangled_ident =
   278   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
   279 
   280 fun parse_mangled_type x =
   281   (parse_mangled_ident
   282    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
   283                     [] >> ATerm) x
   284 and parse_mangled_types x =
   285   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
   286 
   287 fun unmangled_type s =
   288   s |> suffix ")" |> raw_explode
   289     |> Scan.finite Symbol.stopper
   290            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
   291                                                 quote s)) parse_mangled_type))
   292     |> fst
   293 
   294 val unmangled_const_name = space_explode mangled_type_sep #> hd
   295 fun unmangled_const s =
   296   let val ss = space_explode mangled_type_sep s in
   297     (hd ss, map unmangled_type (tl ss))
   298   end
   299 
   300 fun introduce_proxies tm =
   301   let
   302     fun aux top_level (CombApp (tm1, tm2)) =
   303         CombApp (aux top_level tm1, aux false tm2)
   304       | aux top_level (CombConst (name as (s, s'), T, T_args)) =
   305         (case proxify_const s of
   306            SOME proxy_base =>
   307            if top_level then
   308              (case s of
   309                 "c_False" => (tptp_false, s')
   310               | "c_True" => (tptp_true, s')
   311               | _ => name, [])
   312            else
   313              (proxy_base |>> prefix const_prefix, T_args)
   314           | NONE => (name, T_args))
   315         |> (fn (name, T_args) => CombConst (name, T, T_args))
   316       | aux _ tm = tm
   317   in aux true tm end
   318 
   319 fun combformula_from_prop thy eq_as_iff =
   320   let
   321     fun do_term bs t atomic_types =
   322       combterm_from_term thy bs (Envir.eta_contract t)
   323       |>> (introduce_proxies #> AAtom)
   324       ||> union (op =) atomic_types
   325     fun do_quant bs q s T t' =
   326       let val s = Name.variant (map fst bs) s in
   327         do_formula ((s, T) :: bs) t'
   328         #>> mk_aquant q [(`make_bound_var s, SOME T)]
   329       end
   330     and do_conn bs c t1 t2 =
   331       do_formula bs t1 ##>> do_formula bs t2
   332       #>> uncurry (mk_aconn c)
   333     and do_formula bs t =
   334       case t of
   335         @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
   336       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   337         do_quant bs AForall s T t'
   338       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   339         do_quant bs AExists s T t'
   340       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
   341       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
   342       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
   343       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   344         if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
   345       | _ => do_term bs t
   346   in do_formula [] end
   347 
   348 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
   349 
   350 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
   351 fun conceal_bounds Ts t =
   352   subst_bounds (map (Free o apfst concealed_bound_name)
   353                     (0 upto length Ts - 1 ~~ Ts), t)
   354 fun reveal_bounds Ts =
   355   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   356                     (0 upto length Ts - 1 ~~ Ts))
   357 
   358 fun extensionalize_term ctxt t =
   359   let val thy = Proof_Context.theory_of ctxt in
   360     t |> cterm_of thy |> Meson.extensionalize_conv ctxt
   361       |> prop_of |> Logic.dest_equals |> snd
   362   end
   363 
   364 fun introduce_combinators_in_term ctxt kind t =
   365   let val thy = Proof_Context.theory_of ctxt in
   366     if Meson.is_fol_term thy t then
   367       t
   368     else
   369       let
   370         fun aux Ts t =
   371           case t of
   372             @{const Not} $ t1 => @{const Not} $ aux Ts t1
   373           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   374             t0 $ Abs (s, T, aux (T :: Ts) t')
   375           | (t0 as Const (@{const_name All}, _)) $ t1 =>
   376             aux Ts (t0 $ eta_expand Ts t1 1)
   377           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   378             t0 $ Abs (s, T, aux (T :: Ts) t')
   379           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   380             aux Ts (t0 $ eta_expand Ts t1 1)
   381           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   382           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   383           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   384           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   385               $ t1 $ t2 =>
   386             t0 $ aux Ts t1 $ aux Ts t2
   387           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   388                    t
   389                  else
   390                    t |> conceal_bounds Ts
   391                      |> Envir.eta_contract
   392                      |> cterm_of thy
   393                      |> Meson_Clausify.introduce_combinators_in_cterm
   394                      |> prop_of |> Logic.dest_equals |> snd
   395                      |> reveal_bounds Ts
   396         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   397       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   398       handle THM _ =>
   399              (* A type variable of sort "{}" will make abstraction fail. *)
   400              if kind = Conjecture then HOLogic.false_const
   401              else HOLogic.true_const
   402   end
   403 
   404 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   405    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
   406 fun freeze_term t =
   407   let
   408     fun aux (t $ u) = aux t $ aux u
   409       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   410       | aux (Var ((s, i), T)) =
   411         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   412       | aux t = t
   413   in t |> exists_subterm is_Var t ? aux end
   414 
   415 (* making fact and conjecture formulas *)
   416 fun make_formula ctxt eq_as_iff presimp name loc kind t =
   417   let
   418     val thy = Proof_Context.theory_of ctxt
   419     val t = t |> Envir.beta_eta_contract
   420               |> transform_elim_term
   421               |> Object_Logic.atomize_term thy
   422     val need_trueprop = (fastype_of t = @{typ bool})
   423     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   424               |> Raw_Simplifier.rewrite_term thy
   425                      (Meson.unfold_set_const_simps ctxt) []
   426               |> extensionalize_term ctxt
   427               |> presimp ? presimplify_term thy
   428               |> perhaps (try (HOLogic.dest_Trueprop))
   429               |> introduce_combinators_in_term ctxt kind
   430               |> kind <> Axiom ? freeze_term
   431     val (combformula, atomic_types) =
   432       combformula_from_prop thy eq_as_iff t []
   433   in
   434     {name = name, locality = loc, kind = kind, combformula = combformula,
   435      atomic_types = atomic_types}
   436   end
   437 
   438 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, loc), t) =
   439   case (keep_trivial, make_formula ctxt eq_as_iff presimp name loc Axiom t) of
   440     (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
   441     NONE
   442   | (_, formula) => SOME formula
   443 
   444 fun make_conjecture ctxt prem_kind ts =
   445   let val last = length ts - 1 in
   446     map2 (fn j => fn t =>
   447              let
   448                val (kind, maybe_negate) =
   449                  if j = last then
   450                    (Conjecture, I)
   451                  else
   452                    (prem_kind,
   453                     if prem_kind = Conjecture then update_combformula mk_anot
   454                     else I)
   455               in
   456                 make_formula ctxt true true (string_of_int j) Chained kind t
   457                 |> maybe_negate
   458               end)
   459          (0 upto last) ts
   460   end
   461 
   462 (** Finite and infinite type inference **)
   463 
   464 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
   465    dangerous because their "exhaust" properties can easily lead to unsound ATP
   466    proofs. On the other hand, all HOL infinite types can be given the same
   467    models in first-order logic (via Löwenheim-Skolem). *)
   468 
   469 fun should_encode_type _ _ All_Types _ = true
   470   | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
   471   | should_encode_type _ nonmono_Ts Nonmonotonic_Types T =
   472     exists (curry Type.raw_instance T) nonmono_Ts
   473   | should_encode_type _ _ _ _ = false
   474 
   475 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T =
   476     should_encode_type ctxt nonmono_Ts level T
   477   | should_predicate_on_type _ _ _ _ = false
   478 
   479 fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T =
   480     should_encode_type ctxt nonmono_Ts level T
   481   | should_tag_with_type _ _ _ _ = false
   482 
   483 val homo_infinite_T = @{typ ind} (* any infinite type *)
   484 
   485 fun homogenized_type ctxt nonmono_Ts level T =
   486   if should_encode_type ctxt nonmono_Ts level T then T else homo_infinite_T
   487 
   488 (** "hBOOL" and "hAPP" **)
   489 
   490 type sym_info =
   491   {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option}
   492 
   493 fun add_combterm_syms_to_table explicit_apply =
   494   let
   495     fun aux top_level tm =
   496       let val (head, args) = strip_combterm_comb tm in
   497         (case head of
   498            CombConst ((s, _), T, _) =>
   499            if String.isPrefix bound_var_prefix s then
   500              I
   501            else
   502              let val ary = length args in
   503                Symtab.map_default
   504                    (s, {pred_sym = true,
   505                         min_ary = if explicit_apply then 0 else ary,
   506                         max_ary = 0, typ = SOME T})
   507                    (fn {pred_sym, min_ary, max_ary, typ} =>
   508                        {pred_sym = pred_sym andalso top_level,
   509                         min_ary = Int.min (ary, min_ary),
   510                         max_ary = Int.max (ary, max_ary),
   511                         typ = if typ = SOME T then typ else NONE})
   512             end
   513          | _ => I)
   514         #> fold (aux false) args
   515       end
   516   in aux true end
   517 fun add_fact_syms_to_table explicit_apply =
   518   fact_lift (formula_fold true (K (add_combterm_syms_to_table explicit_apply)))
   519 
   520 val default_sym_table_entries : (string * sym_info) list =
   521   [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
   522    (make_fixed_const predicator_base,
   523     {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
   524   ([tptp_false, tptp_true]
   525    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
   526 
   527 fun sym_table_for_facts explicit_apply facts =
   528   Symtab.empty |> fold Symtab.default default_sym_table_entries
   529                |> fold (add_fact_syms_to_table explicit_apply) facts
   530 
   531 fun min_arity_of sym_tab s =
   532   case Symtab.lookup sym_tab s of
   533     SOME ({min_ary, ...} : sym_info) => min_ary
   534   | NONE =>
   535     case strip_prefix_and_unascii const_prefix s of
   536       SOME s =>
   537       let val s = s |> unmangled_const_name |> invert_const in
   538         if s = predicator_base then 1
   539         else if s = explicit_app_base then 2
   540         else if s = type_pred_base then 1
   541         else 0
   542       end
   543     | NONE => 0
   544 
   545 (* True if the constant ever appears outside of the top-level position in
   546    literals, or if it appears with different arities (e.g., because of different
   547    type instantiations). If false, the constant always receives all of its
   548    arguments and is used as a predicate. *)
   549 fun is_pred_sym sym_tab s =
   550   case Symtab.lookup sym_tab s of
   551     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
   552     pred_sym andalso min_ary = max_ary
   553   | NONE => false
   554 
   555 val predicator_combconst =
   556   CombConst (`make_fixed_const predicator_base, @{typ "bool => bool"}, [])
   557 fun predicator tm = CombApp (predicator_combconst, tm)
   558 
   559 fun introduce_predicators_in_combterm sym_tab tm =
   560   case strip_combterm_comb tm of
   561     (CombConst ((s, _), _, _), _) =>
   562     if is_pred_sym sym_tab s then tm else predicator tm
   563   | _ => predicator tm
   564 
   565 fun list_app head args = fold (curry (CombApp o swap)) args head
   566 
   567 fun explicit_app arg head =
   568   let
   569     val head_T = combtyp_of head
   570     val (arg_T, res_T) = dest_funT head_T
   571     val explicit_app =
   572       CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
   573                  [arg_T, res_T])
   574   in list_app explicit_app [head, arg] end
   575 fun list_explicit_app head args = fold explicit_app args head
   576 
   577 fun introduce_explicit_apps_in_combterm sym_tab =
   578   let
   579     fun aux tm =
   580       case strip_combterm_comb tm of
   581         (head as CombConst ((s, _), _, _), args) =>
   582         args |> map aux
   583              |> chop (min_arity_of sym_tab s)
   584              |>> list_app head
   585              |-> list_explicit_app
   586       | (head, args) => list_explicit_app head (map aux args)
   587   in aux end
   588 
   589 fun impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
   590   let
   591     fun aux (CombApp tmp) = CombApp (pairself aux tmp)
   592       | aux (CombConst (name as (s, _), T, T_args)) =
   593         let
   594           val level = level_of_type_sys type_sys
   595           val (T, T_args) =
   596             (* Aggressively merge most "hAPPs" if the type system is unsound
   597                anyway, by distinguishing overloads only on the homogenized
   598                result type. *)
   599             if s = const_prefix ^ explicit_app_base andalso
   600                length T_args = 2 andalso
   601                not (is_type_sys_virtually_sound type_sys) then
   602               T_args |> map (homogenized_type ctxt nonmono_Ts level)
   603                      |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
   604                                     (T --> T, tl Ts)
   605                                   end)
   606             else
   607               (T, T_args)
   608         in
   609           (case strip_prefix_and_unascii const_prefix s of
   610              NONE => (name, T_args)
   611            | SOME s'' =>
   612              let val s'' = invert_const s'' in
   613                case type_arg_policy type_sys s'' of
   614                  No_Type_Args => (name, [])
   615                | Explicit_Type_Args => (name, T_args)
   616                | Mangled_Type_Args => (mangled_const_name T_args name, [])
   617              end)
   618           |> (fn (name, T_args) => CombConst (name, T, T_args))
   619         end
   620       | aux tm = tm
   621   in aux end
   622 
   623 fun repair_combterm ctxt nonmono_Ts type_sys sym_tab =
   624   introduce_explicit_apps_in_combterm sym_tab
   625   #> introduce_predicators_in_combterm sym_tab
   626   #> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
   627 fun repair_fact ctxt nonmono_Ts type_sys sym_tab =
   628   update_combformula (formula_map
   629       (repair_combterm ctxt nonmono_Ts type_sys sym_tab))
   630 
   631 (** Helper facts **)
   632 
   633 fun ti_ti_helper_fact () =
   634   let
   635     fun var s = ATerm (`I s, [])
   636     fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
   637   in
   638     Formula (helper_prefix ^ "ti_ti", Axiom,
   639              AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
   640              |> close_formula_universally, NONE, NONE)
   641   end
   642 
   643 fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) =
   644   case strip_prefix_and_unascii const_prefix s of
   645     SOME mangled_s =>
   646     let
   647       val thy = Proof_Context.theory_of ctxt
   648       val unmangled_s = mangled_s |> unmangled_const_name
   649       fun dub_and_inst c needs_some_types (th, j) =
   650         ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
   651           Chained),
   652          let val t = th |> prop_of in
   653            t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso
   654                  not (null (Term.hidden_polymorphism t)))
   655                 ? (case typ of
   656                      SOME T => specialize_type thy (invert_const unmangled_s, T)
   657                    | NONE => I)
   658          end)
   659       fun make_facts eq_as_iff =
   660         map_filter (make_fact ctxt false eq_as_iff false)
   661       val has_some_types = is_type_sys_fairly_sound type_sys
   662     in
   663       metis_helpers
   664       |> maps (fn (metis_s, (needs_some_types, ths)) =>
   665                   if metis_s <> unmangled_s orelse
   666                      (needs_some_types andalso not has_some_types) then
   667                     []
   668                   else
   669                     ths ~~ (1 upto length ths)
   670                     |> map (dub_and_inst mangled_s needs_some_types)
   671                     |> make_facts (not needs_some_types))
   672     end
   673   | NONE => []
   674 fun helper_facts_for_sym_table ctxt type_sys sym_tab =
   675   Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab []
   676 
   677 fun translate_atp_fact ctxt keep_trivial =
   678   `(make_fact ctxt keep_trivial true true o apsnd prop_of)
   679 
   680 fun translate_formulas ctxt prem_kind type_sys hyp_ts concl_t rich_facts =
   681   let
   682     val thy = Proof_Context.theory_of ctxt
   683     val fact_ts = map (prop_of o snd o snd) rich_facts
   684     val (facts, fact_names) =
   685       rich_facts
   686       |> map_filter (fn (NONE, _) => NONE
   687                       | (SOME fact, (name, _)) => SOME (fact, name))
   688       |> ListPair.unzip
   689     (* Remove existing facts from the conjecture, as this can dramatically
   690        boost an ATP's performance (for some reason). *)
   691     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
   692     val goal_t = Logic.list_implies (hyp_ts, concl_t)
   693     val all_ts = goal_t :: fact_ts
   694     val subs = tfree_classes_of_terms all_ts
   695     val supers = tvar_classes_of_terms all_ts
   696     val tycons = type_consts_of_terms thy all_ts
   697     val conjs = make_conjecture ctxt prem_kind (hyp_ts @ [concl_t])
   698     val (supers', arity_clauses) =
   699       if level_of_type_sys type_sys = No_Types then ([], [])
   700       else make_arity_clauses thy tycons supers
   701     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   702   in
   703     (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
   704   end
   705 
   706 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
   707     (true, ATerm (class, [ATerm (name, [])]))
   708   | fo_literal_from_type_literal (TyLitFree (class, name)) =
   709     (true, ATerm (class, [ATerm (name, [])]))
   710 
   711 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   712 
   713 fun type_pred_combatom ctxt nonmono_Ts type_sys T tm =
   714   CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
   715            tm)
   716   |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
   717   |> AAtom
   718 
   719 fun formula_from_combformula ctxt nonmono_Ts type_sys =
   720   let
   721     fun tag_with_type type_sys T tm =
   722       CombConst (`make_fixed_const type_tag_name, T --> T, [T])
   723       |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
   724       |> do_term true
   725       |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
   726     and do_term top_level u =
   727       let
   728         val (head, args) = strip_combterm_comb u
   729         val (x, T_args) =
   730           case head of
   731             CombConst (name, _, T_args) => (name, T_args)
   732           | CombVar (name, _) => (name, [])
   733           | CombApp _ => raise Fail "impossible \"CombApp\""
   734         val t = ATerm (x, map fo_term_from_typ T_args @
   735                           map (do_term false) args)
   736         val T = combtyp_of u
   737       in
   738         t |> (if not top_level andalso
   739                 should_tag_with_type ctxt nonmono_Ts type_sys T then
   740                 tag_with_type type_sys T
   741               else
   742                 I)
   743       end
   744     val do_bound_type =
   745       case type_sys of
   746         Simple_Types level =>
   747         SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
   748       | _ => K NONE
   749     fun do_out_of_bound_type (s, T) =
   750       if should_predicate_on_type ctxt nonmono_Ts type_sys T then
   751         type_pred_combatom ctxt nonmono_Ts type_sys T (CombVar (s, T))
   752         |> do_formula |> SOME
   753       else
   754         NONE
   755     and do_formula (AQuant (q, xs, phi)) =
   756         AQuant (q, xs |> map (apsnd (fn NONE => NONE
   757                                       | SOME T => do_bound_type T)),
   758                 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
   759                     (map_filter
   760                          (fn (_, NONE) => NONE
   761                            | (s, SOME T) => do_out_of_bound_type (s, T)) xs)
   762                     (do_formula phi))
   763       | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
   764       | do_formula (AAtom tm) = AAtom (do_term true tm)
   765   in do_formula end
   766 
   767 fun bound_atomic_types type_sys Ts =
   768   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
   769                 (atp_type_literals_for_types type_sys Axiom Ts))
   770 
   771 fun formula_for_fact ctxt nonmono_Ts type_sys
   772                      ({combformula, atomic_types, ...} : translated_formula) =
   773   combformula
   774   |> close_combformula_universally
   775   |> formula_from_combformula ctxt nonmono_Ts type_sys
   776   |> bound_atomic_types type_sys atomic_types
   777   |> close_formula_universally
   778 
   779 fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
   780 
   781 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   782    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   783    the remote provers might care. *)
   784 fun formula_line_for_fact ctxt prefix nonmono_Ts type_sys
   785                           (j, formula as {name, locality, kind, ...}) =
   786   Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
   787                      else string_of_int j ^ "_") ^
   788            ascii_of name,
   789            kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE,
   790            if generate_useful_info then
   791              case locality of
   792                Intro => useful_isabelle_info "intro"
   793              | Elim => useful_isabelle_info "elim"
   794              | Simp => useful_isabelle_info "simp"
   795              | _ => NONE
   796            else
   797              NONE)
   798 
   799 fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
   800                                                        superclass, ...}) =
   801   let val ty_arg = ATerm (`I "T", []) in
   802     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
   803              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   804                                AAtom (ATerm (superclass, [ty_arg]))])
   805              |> close_formula_universally, NONE, NONE)
   806   end
   807 
   808 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
   809     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   810   | fo_literal_from_arity_literal (TVarLit (c, sort)) =
   811     (false, ATerm (c, [ATerm (sort, [])]))
   812 
   813 fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   814                                                 ...}) =
   815   Formula (arity_clause_prefix ^ ascii_of name, Axiom,
   816            mk_ahorn (map (formula_from_fo_literal o apfst not
   817                           o fo_literal_from_arity_literal) premLits)
   818                     (formula_from_fo_literal
   819                          (fo_literal_from_arity_literal conclLit))
   820            |> close_formula_universally, NONE, NONE)
   821 
   822 fun formula_line_for_conjecture ctxt nonmono_Ts type_sys
   823         ({name, kind, combformula, ...} : translated_formula) =
   824   Formula (conjecture_prefix ^ name, kind,
   825            formula_from_combformula ctxt nonmono_Ts type_sys
   826                                     (close_combformula_universally combformula)
   827            |> close_formula_universally, NONE, NONE)
   828 
   829 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
   830   atomic_types |> atp_type_literals_for_types type_sys Conjecture
   831                |> map fo_literal_from_type_literal
   832 
   833 fun formula_line_for_free_type j lit =
   834   Formula (tfree_prefix ^ string_of_int j, Hypothesis,
   835            formula_from_fo_literal lit, NONE, NONE)
   836 fun formula_lines_for_free_types type_sys facts =
   837   let
   838     val litss = map (free_type_literals type_sys) facts
   839     val lits = fold (union (op =)) litss []
   840   in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
   841 
   842 (** Symbol declarations **)
   843 
   844 fun insert_type get_T x xs =
   845   let val T = get_T x in
   846     if exists (curry Type.raw_instance T o get_T) xs then xs
   847     else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs
   848   end
   849 
   850 fun should_declare_sym type_sys pred_sym s =
   851   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   852   not (String.isPrefix "$" s) andalso
   853   ((case type_sys of Simple_Types _ => true | _ => false) orelse not pred_sym)
   854 
   855 fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
   856   let
   857     fun add_combterm in_conj tm =
   858       let val (head, args) = strip_combterm_comb tm in
   859         (case head of
   860            CombConst ((s, s'), T, T_args) =>
   861            let val pred_sym = is_pred_sym repaired_sym_tab s in
   862              if should_declare_sym type_sys pred_sym s then
   863                Symtab.map_default (s, [])
   864                    (insert_type #3 (s', T_args, T, pred_sym, length args,
   865                                     in_conj))
   866              else
   867                I
   868            end
   869          | _ => I)
   870         #> fold (add_combterm in_conj) args
   871       end
   872     fun add_fact in_conj =
   873       fact_lift (formula_fold true (K (add_combterm in_conj)))
   874   in
   875     Symtab.empty
   876     |> is_type_sys_fairly_sound type_sys
   877        ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
   878   end
   879 
   880 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
   881     String.isPrefix bound_var_prefix s
   882   | is_var_or_bound_var (CombVar _) = true
   883   | is_var_or_bound_var _ = false
   884 
   885 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
   886    out with monotonicity" paper presented at CADE 2011. *)
   887 fun add_combterm_nonmonotonic_types _ (SOME false) _ = I
   888   | add_combterm_nonmonotonic_types ctxt _
   889         (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
   890                   tm2)) =
   891     (exists is_var_or_bound_var [tm1, tm2] andalso
   892      not (is_type_surely_infinite ctxt T)) ? insert_type I T
   893   | add_combterm_nonmonotonic_types _ _ _ = I
   894 fun add_fact_nonmonotonic_types ctxt ({kind, combformula, ...}
   895                                       : translated_formula) =
   896   formula_fold (kind <> Conjecture) (add_combterm_nonmonotonic_types ctxt)
   897                combformula
   898 fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
   899   level_of_type_sys type_sys = Nonmonotonic_Types
   900   ? (fold (add_fact_nonmonotonic_types ctxt) facts
   901      (* in case helper "True_or_False" is included *)
   902      #> insert_type I @{typ bool})
   903 
   904 fun n_ary_strip_type 0 T = ([], T)
   905   | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) =
   906     n_ary_strip_type (n - 1) ran_T |>> cons dom_T
   907   | n_ary_strip_type _ _ = raise Fail "unexpected non-function"
   908 
   909 fun result_type_of_decl (_, _, T, _, ary, _) = n_ary_strip_type ary T |> snd
   910 
   911 fun decl_line_for_sym s (s', _, T, pred_sym, ary, _) =
   912   let val (arg_Ts, res_T) = n_ary_strip_type ary T in
   913     Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
   914           if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
   915   end
   916 
   917 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
   918 
   919 fun formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s j
   920                               (s', T_args, T, _, ary, in_conj) =
   921   let
   922     val (kind, maybe_negate) =
   923       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
   924       else (Axiom, I)
   925     val (arg_Ts, res_T) = n_ary_strip_type ary T
   926     val bound_names =
   927       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
   928     val bound_tms =
   929       bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
   930     val bound_Ts =
   931       arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
   932                              else NONE)
   933   in
   934     Formula (sym_decl_prefix ^ s ^
   935              (if n > 1 then "_" ^ string_of_int j else ""), kind,
   936              CombConst ((s, s'), T, T_args)
   937              |> fold (curry (CombApp o swap)) bound_tms
   938              |> type_pred_combatom ctxt nonmono_Ts type_sys res_T
   939              |> mk_aquant AForall (bound_names ~~ bound_Ts)
   940              |> formula_from_combformula ctxt nonmono_Ts type_sys
   941              |> n > 1 ? bound_atomic_types type_sys (atyps_of T)
   942              |> close_formula_universally
   943              |> maybe_negate,
   944              NONE, NONE)
   945   end
   946 
   947 fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys
   948                                 (s, decls) =
   949   case type_sys of
   950     Simple_Types _ => map (decl_line_for_sym s) decls
   951   | _ =>
   952     let
   953       val decls =
   954         case decls of
   955           decl :: (decls' as _ :: _) =>
   956           let val T = result_type_of_decl decl in
   957             if forall ((fn T' => Type.raw_instance (T', T))
   958                        o result_type_of_decl) decls' then
   959               [decl]
   960             else
   961               decls
   962           end
   963         | _ => decls
   964       val n = length decls
   965       val decls =
   966         decls |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys
   967                          o result_type_of_decl)
   968     in
   969       (0 upto length decls - 1, decls)
   970       |-> map2 (formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys
   971                                           n s)
   972     end
   973 
   974 fun problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
   975                                      sym_decl_tab =
   976   Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt conj_sym_kind
   977                                                         nonmono_Ts type_sys)
   978                   sym_decl_tab []
   979 
   980 fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
   981     union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
   982   | add_tff_types_in_formula (AConn (_, phis)) =
   983     fold add_tff_types_in_formula phis
   984   | add_tff_types_in_formula (AAtom _) = I
   985 
   986 fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
   987     union (op =) (res_T :: arg_Ts)
   988   | add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) =
   989     add_tff_types_in_formula phi
   990 
   991 fun tff_types_in_problem problem =
   992   fold (fold add_tff_types_in_problem_line o snd) problem []
   993 
   994 fun decl_line_for_tff_type (s, s') =
   995   Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types)
   996 
   997 val type_declsN = "Types"
   998 val sym_declsN = "Symbol types"
   999 val factsN = "Relevant facts"
  1000 val class_relsN = "Class relationships"
  1001 val aritiesN = "Arities"
  1002 val helpersN = "Helper facts"
  1003 val conjsN = "Conjectures"
  1004 val free_typesN = "Type variables"
  1005 
  1006 fun offset_of_heading_in_problem _ [] j = j
  1007   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
  1008     if heading = needle then j
  1009     else offset_of_heading_in_problem needle problem (j + length lines)
  1010 
  1011 fun prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys explicit_apply
  1012                         hyp_ts concl_t facts =
  1013   let
  1014     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
  1015       translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts
  1016     val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
  1017     val nonmono_Ts =
  1018       [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
  1019     val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab
  1020     val (conjs, facts) = (conjs, facts) |> pairself (map repair)
  1021     val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
  1022     val helpers =
  1023       repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
  1024     val sym_decl_lines =
  1025       (conjs, helpers @ facts)
  1026       |> sym_decl_table_for_facts type_sys repaired_sym_tab
  1027       |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
  1028     (* Reordering these might confuse the proof reconstruction code or the SPASS
  1029        Flotter hack. *)
  1030     val problem =
  1031       [(sym_declsN, sym_decl_lines),
  1032        (factsN, map (formula_line_for_fact ctxt fact_prefix nonmono_Ts type_sys)
  1033                     (0 upto length facts - 1 ~~ facts)),
  1034        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
  1035        (aritiesN, map formula_line_for_arity_clause arity_clauses),
  1036        (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
  1037                                              type_sys)
  1038                       (0 upto length helpers - 1 ~~ helpers)
  1039                   |> (case type_sys of
  1040                         Tags (Polymorphic, level) =>
  1041                         is_type_level_partial level
  1042                         ? cons (ti_ti_helper_fact ())
  1043                       | _ => I)),
  1044        (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
  1045                     conjs),
  1046        (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
  1047     val problem =
  1048       problem
  1049       |> (case type_sys of
  1050             Simple_Types _ =>
  1051             cons (type_declsN,
  1052                   map decl_line_for_tff_type (tff_types_in_problem problem))
  1053           | _ => I)
  1054     val (problem, pool) =
  1055       problem |> nice_atp_problem (Config.get ctxt readable_names)
  1056   in
  1057     (problem,
  1058      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
  1059      offset_of_heading_in_problem conjsN problem 0,
  1060      offset_of_heading_in_problem factsN problem 0,
  1061      fact_names |> Vector.fromList)
  1062   end
  1063 
  1064 (* FUDGE *)
  1065 val conj_weight = 0.0
  1066 val hyp_weight = 0.1
  1067 val fact_min_weight = 0.2
  1068 val fact_max_weight = 1.0
  1069 val type_info_default_weight = 0.8
  1070 
  1071 fun add_term_weights weight (ATerm (s, tms)) =
  1072   (not (is_atp_variable s) andalso s <> "equal" andalso
  1073    not (String.isPrefix "$" s)) ? Symtab.default (s, weight)
  1074   #> fold (add_term_weights weight) tms
  1075 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
  1076     formula_fold true (K (add_term_weights weight)) phi
  1077   | add_problem_line_weights _ _ = I
  1078 
  1079 fun add_conjectures_weights [] = I
  1080   | add_conjectures_weights conjs =
  1081     let val (hyps, conj) = split_last conjs in
  1082       add_problem_line_weights conj_weight conj
  1083       #> fold (add_problem_line_weights hyp_weight) hyps
  1084     end
  1085 
  1086 fun add_facts_weights facts =
  1087   let
  1088     val num_facts = length facts
  1089     fun weight_of j =
  1090       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
  1091                         / Real.fromInt num_facts
  1092   in
  1093     map weight_of (0 upto num_facts - 1) ~~ facts
  1094     |> fold (uncurry add_problem_line_weights)
  1095   end
  1096 
  1097 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
  1098 fun atp_problem_weights problem =
  1099   let val get = these o AList.lookup (op =) problem in
  1100     Symtab.empty
  1101     |> add_conjectures_weights (get free_typesN @ get conjsN)
  1102     |> add_facts_weights (get factsN)
  1103     |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
  1104             [sym_declsN, class_relsN, aritiesN]
  1105     |> Symtab.dest
  1106     |> sort (prod_ord Real.compare string_ord o pairself swap)
  1107   end
  1108 
  1109 end;