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