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