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