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