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