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