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