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