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