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