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