src/HOL/Tools/ATP/atp_problem_generate.ML
author blanchet
Wed May 23 21:19:48 2012 +0200 (2012-05-23)
changeset 47975 adc977fec17e
parent 47971 2aea51a14200
child 47981 df35a8dd6368
permissions -rw-r--r--
order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy)
     1 (*  Title:      HOL/Tools/ATP/atp_problem_generate.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_PROBLEM_GENERATE =
    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 atp_format = ATP_Problem.atp_format
    15   type formula_role = ATP_Problem.formula_role
    16   type 'a problem = 'a ATP_Problem.problem
    17 
    18   datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
    19 
    20   datatype scope = Global | Local | Assum | Chained
    21   datatype status =
    22     General | Induction | Intro | Inductive | Elim | Simp | Def
    23   type stature = scope * status
    24 
    25   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    26   datatype strictness = Strict | Non_Strict
    27   datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
    28   datatype type_level =
    29     All_Types |
    30     Noninf_Nonmono_Types of strictness * granularity |
    31     Fin_Nonmono_Types of granularity |
    32     Const_Arg_Types |
    33     No_Types
    34   type type_enc
    35 
    36   val no_lamsN : string
    37   val hide_lamsN : string
    38   val liftingN : string
    39   val combsN : string
    40   val combs_and_liftingN : string
    41   val combs_or_liftingN : string
    42   val lam_liftingN : string
    43   val keep_lamsN : string
    44   val schematic_var_prefix : string
    45   val fixed_var_prefix : string
    46   val tvar_prefix : string
    47   val tfree_prefix : string
    48   val const_prefix : string
    49   val type_const_prefix : string
    50   val class_prefix : string
    51   val lam_lifted_prefix : string
    52   val lam_lifted_mono_prefix : string
    53   val lam_lifted_poly_prefix : string
    54   val skolem_const_prefix : string
    55   val old_skolem_const_prefix : string
    56   val new_skolem_const_prefix : string
    57   val combinator_prefix : string
    58   val type_decl_prefix : string
    59   val sym_decl_prefix : string
    60   val guards_sym_formula_prefix : string
    61   val tags_sym_formula_prefix : string
    62   val fact_prefix : string
    63   val conjecture_prefix : string
    64   val helper_prefix : string
    65   val class_rel_clause_prefix : string
    66   val arity_clause_prefix : string
    67   val tfree_clause_prefix : string
    68   val lam_fact_prefix : string
    69   val typed_helper_suffix : string
    70   val untyped_helper_suffix : string
    71   val predicator_name : string
    72   val app_op_name : string
    73   val type_guard_name : string
    74   val type_tag_name : string
    75   val native_type_prefix : string
    76   val prefixed_predicator_name : string
    77   val prefixed_app_op_name : string
    78   val prefixed_type_tag_name : string
    79   val ascii_of : string -> string
    80   val unascii_of : string -> string
    81   val unprefix_and_unascii : string -> string -> string option
    82   val proxy_table : (string * (string * (thm * (string * string)))) list
    83   val proxify_const : string -> (string * string) option
    84   val invert_const : string -> string
    85   val unproxify_const : string -> string
    86   val new_skolem_var_name_from_const : string -> string
    87   val atp_irrelevant_consts : string list
    88   val atp_schematic_consts_of : term -> typ list Symtab.table
    89   val is_type_enc_higher_order : type_enc -> bool
    90   val polymorphism_of_type_enc : type_enc -> polymorphism
    91   val level_of_type_enc : type_enc -> type_level
    92   val is_type_enc_quasi_sound : type_enc -> bool
    93   val is_type_enc_fairly_sound : type_enc -> bool
    94   val type_enc_from_string : strictness -> string -> type_enc
    95   val adjust_type_enc : atp_format -> type_enc -> type_enc
    96   val mk_aconns :
    97     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    98   val unmangled_const : string -> string * (string, 'b) ho_term list
    99   val unmangled_const_name : string -> string list
   100   val helper_table : ((string * bool) * (status * thm) list) list
   101   val trans_lams_from_string :
   102     Proof.context -> type_enc -> string -> term list -> term list * term list
   103   val factsN : string
   104   val prepare_atp_problem :
   105     Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string
   106     -> bool -> bool -> bool -> term list -> term
   107     -> ((string * stature) * term) list
   108     -> string problem * string Symtab.table * (string * stature) list vector
   109        * (string * term) list * int Symtab.table
   110   val atp_problem_selection_weights : string problem -> (string * real) list
   111   val atp_problem_term_order_info : string problem -> (string * int) list
   112 end;
   113 
   114 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
   115 struct
   116 
   117 open ATP_Util
   118 open ATP_Problem
   119 
   120 type name = string * string
   121 
   122 datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
   123 
   124 datatype scope = Global | Local | Assum | Chained
   125 datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
   126 type stature = scope * status
   127 
   128 datatype order =
   129   First_Order |
   130   Higher_Order of thf_flavor
   131 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
   132 datatype strictness = Strict | Non_Strict
   133 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
   134 datatype type_level =
   135   All_Types |
   136   Noninf_Nonmono_Types of strictness * granularity |
   137   Fin_Nonmono_Types of granularity |
   138   Const_Arg_Types |
   139   No_Types
   140 
   141 datatype type_enc =
   142   Native of order * polymorphism * type_level |
   143   Guards of polymorphism * type_level |
   144   Tags of polymorphism * type_level
   145 
   146 fun is_type_enc_native (Native _) = true
   147   | is_type_enc_native _ = false
   148 fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
   149   | is_type_enc_higher_order _ = false
   150 
   151 fun polymorphism_of_type_enc (Native (_, poly, _)) = poly
   152   | polymorphism_of_type_enc (Guards (poly, _)) = poly
   153   | polymorphism_of_type_enc (Tags (poly, _)) = poly
   154 
   155 fun level_of_type_enc (Native (_, _, level)) = level
   156   | level_of_type_enc (Guards (_, level)) = level
   157   | level_of_type_enc (Tags (_, level)) = level
   158 
   159 fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
   160   | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
   161   | granularity_of_type_level _ = All_Vars
   162 
   163 fun is_type_level_quasi_sound All_Types = true
   164   | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
   165   | is_type_level_quasi_sound _ = false
   166 val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
   167 
   168 fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
   169   | is_type_level_fairly_sound level = is_type_level_quasi_sound level
   170 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
   171 
   172 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
   173   | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
   174   | is_type_level_monotonicity_based _ = false
   175 
   176 val no_lamsN = "no_lams" (* used internally; undocumented *)
   177 val hide_lamsN = "hide_lams"
   178 val liftingN = "lifting"
   179 val combsN = "combs"
   180 val combs_and_liftingN = "combs_and_lifting"
   181 val combs_or_liftingN = "combs_or_lifting"
   182 val keep_lamsN = "keep_lams"
   183 val lam_liftingN = "lam_lifting" (* legacy *)
   184 
   185 (* It's still unclear whether all TFF1 implementations will support type
   186    signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
   187 val avoid_first_order_ghost_type_vars = false
   188 
   189 val bound_var_prefix = "B_"
   190 val all_bound_var_prefix = "A_"
   191 val exist_bound_var_prefix = "E_"
   192 val schematic_var_prefix = "V_"
   193 val fixed_var_prefix = "v_"
   194 val tvar_prefix = "T_"
   195 val tfree_prefix = "t_"
   196 val const_prefix = "c_"
   197 val type_const_prefix = "tc_"
   198 val native_type_prefix = "n_"
   199 val class_prefix = "cl_"
   200 
   201 (* Freshness almost guaranteed! *)
   202 val atp_prefix = "ATP" ^ Long_Name.separator
   203 val atp_weak_prefix = "ATP:"
   204 
   205 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
   206 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
   207 val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
   208 
   209 val skolem_const_prefix = atp_prefix ^ "Sko"
   210 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
   211 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
   212 
   213 val combinator_prefix = "COMB"
   214 
   215 val type_decl_prefix = "ty_"
   216 val sym_decl_prefix = "sy_"
   217 val guards_sym_formula_prefix = "gsy_"
   218 val tags_sym_formula_prefix = "tsy_"
   219 val uncurried_alias_eq_prefix = "unc_"
   220 val fact_prefix = "fact_"
   221 val conjecture_prefix = "conj_"
   222 val helper_prefix = "help_"
   223 val class_rel_clause_prefix = "clar_"
   224 val arity_clause_prefix = "arity_"
   225 val tfree_clause_prefix = "tfree_"
   226 
   227 val lam_fact_prefix = "ATP.lambda_"
   228 val typed_helper_suffix = "_T"
   229 val untyped_helper_suffix = "_U"
   230 
   231 val predicator_name = "pp"
   232 val app_op_name = "aa"
   233 val type_guard_name = "gg"
   234 val type_tag_name = "tt"
   235 
   236 val prefixed_predicator_name = const_prefix ^ predicator_name
   237 val prefixed_app_op_name = const_prefix ^ app_op_name
   238 val prefixed_type_tag_name = const_prefix ^ type_tag_name
   239 
   240 (*Escaping of special characters.
   241   Alphanumeric characters are left unchanged.
   242   The character _ goes to __
   243   Characters in the range ASCII space to / go to _A to _P, respectively.
   244   Other characters go to _nnn where nnn is the decimal ASCII code.*)
   245 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
   246 
   247 fun stringN_of_int 0 _ = ""
   248   | stringN_of_int k n =
   249     stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
   250 
   251 fun ascii_of_char c =
   252   if Char.isAlphaNum c then
   253     String.str c
   254   else if c = #"_" then
   255     "__"
   256   else if #" " <= c andalso c <= #"/" then
   257     "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
   258   else
   259     (* fixed width, in case more digits follow *)
   260     "_" ^ stringN_of_int 3 (Char.ord c)
   261 
   262 val ascii_of = String.translate ascii_of_char
   263 
   264 (** Remove ASCII armoring from names in proof files **)
   265 
   266 (* We don't raise error exceptions because this code can run inside a worker
   267    thread. Also, the errors are impossible. *)
   268 val unascii_of =
   269   let
   270     fun un rcs [] = String.implode (rev rcs)
   271       | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
   272         (* Three types of _ escapes: __, _A to _P, _nnn *)
   273       | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
   274       | un rcs (#"_" :: c :: cs) =
   275         if #"A" <= c andalso c<= #"P" then
   276           (* translation of #" " to #"/" *)
   277           un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
   278         else
   279           let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
   280             case Int.fromString (String.implode digits) of
   281               SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
   282             | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
   283           end
   284       | un rcs (c :: cs) = un (c :: rcs) cs
   285   in un [] o String.explode end
   286 
   287 (* If string s has the prefix s1, return the result of deleting it,
   288    un-ASCII'd. *)
   289 fun unprefix_and_unascii s1 s =
   290   if String.isPrefix s1 s then
   291     SOME (unascii_of (String.extract (s, size s1, NONE)))
   292   else
   293     NONE
   294 
   295 val proxy_table =
   296   [("c_False", (@{const_name False}, (@{thm fFalse_def},
   297        ("fFalse", @{const_name ATP.fFalse})))),
   298    ("c_True", (@{const_name True}, (@{thm fTrue_def},
   299        ("fTrue", @{const_name ATP.fTrue})))),
   300    ("c_Not", (@{const_name Not}, (@{thm fNot_def},
   301        ("fNot", @{const_name ATP.fNot})))),
   302    ("c_conj", (@{const_name conj}, (@{thm fconj_def},
   303        ("fconj", @{const_name ATP.fconj})))),
   304    ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
   305        ("fdisj", @{const_name ATP.fdisj})))),
   306    ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
   307        ("fimplies", @{const_name ATP.fimplies})))),
   308    ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
   309        ("fequal", @{const_name ATP.fequal})))),
   310    ("c_All", (@{const_name All}, (@{thm fAll_def},
   311        ("fAll", @{const_name ATP.fAll})))),
   312    ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
   313        ("fEx", @{const_name ATP.fEx}))))]
   314 
   315 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
   316 
   317 (* Readable names for the more common symbolic functions. Do not mess with the
   318    table unless you know what you are doing. *)
   319 val const_trans_table =
   320   [(@{type_name Product_Type.prod}, "prod"),
   321    (@{type_name Sum_Type.sum}, "sum"),
   322    (@{const_name False}, "False"),
   323    (@{const_name True}, "True"),
   324    (@{const_name Not}, "Not"),
   325    (@{const_name conj}, "conj"),
   326    (@{const_name disj}, "disj"),
   327    (@{const_name implies}, "implies"),
   328    (@{const_name HOL.eq}, "equal"),
   329    (@{const_name All}, "All"),
   330    (@{const_name Ex}, "Ex"),
   331    (@{const_name If}, "If"),
   332    (@{const_name Set.member}, "member"),
   333    (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
   334    (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
   335    (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
   336    (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
   337    (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
   338   |> Symtab.make
   339   |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
   340 
   341 (* Invert the table of translations between Isabelle and ATPs. *)
   342 val const_trans_table_inv =
   343   const_trans_table |> Symtab.dest |> map swap |> Symtab.make
   344 val const_trans_table_unprox =
   345   Symtab.empty
   346   |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
   347 
   348 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
   349 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
   350 
   351 fun lookup_const c =
   352   case Symtab.lookup const_trans_table c of
   353     SOME c' => c'
   354   | NONE => ascii_of c
   355 
   356 fun ascii_of_indexname (v, 0) = ascii_of v
   357   | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
   358 
   359 fun make_bound_var x = bound_var_prefix ^ ascii_of x
   360 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
   361 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
   362 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
   363 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
   364 
   365 fun make_schematic_type_var (x, i) =
   366   tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
   367 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
   368 
   369 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
   370 local
   371   val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
   372   fun default c = const_prefix ^ lookup_const c
   373 in
   374   fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
   375     | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _))) c =
   376       if c = choice_const then tptp_choice else default c
   377     | make_fixed_const _ c = default c
   378 end
   379 
   380 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
   381 
   382 fun make_type_class clas = class_prefix ^ ascii_of clas
   383 
   384 fun new_skolem_var_name_from_const s =
   385   let val ss = s |> space_explode Long_Name.separator in
   386     nth ss (length ss - 2)
   387   end
   388 
   389 (* These are either simplified away by "Meson.presimplify" (most of the time) or
   390    handled specially via "fFalse", "fTrue", ..., "fequal". *)
   391 val atp_irrelevant_consts =
   392   [@{const_name False}, @{const_name True}, @{const_name Not},
   393    @{const_name conj}, @{const_name disj}, @{const_name implies},
   394    @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
   395 
   396 val atp_monomorph_bad_consts =
   397   atp_irrelevant_consts @
   398   (* These are ignored anyway by the relevance filter (unless they appear in
   399      higher-order places) but not by the monomorphizer. *)
   400   [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
   401    @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
   402    @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
   403 
   404 fun add_schematic_const (x as (_, T)) =
   405   Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
   406 val add_schematic_consts_of =
   407   Term.fold_aterms (fn Const (x as (s, _)) =>
   408                        not (member (op =) atp_monomorph_bad_consts s)
   409                        ? add_schematic_const x
   410                       | _ => I)
   411 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
   412 
   413 (** Definitions and functions for FOL clauses and formulas for TPTP **)
   414 
   415 (** Isabelle arities **)
   416 
   417 type arity_atom = name * name * name list
   418 
   419 val type_class = the_single @{sort type}
   420 
   421 type arity_clause =
   422   {name : string,
   423    prem_atoms : arity_atom list,
   424    concl_atom : arity_atom}
   425 
   426 fun add_prem_atom tvar =
   427   fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
   428 
   429 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
   430 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
   431   let
   432     val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
   433     val tvars_srts = ListPair.zip (tvars, args)
   434   in
   435     {name = name,
   436      prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
   437      concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
   438                    tvars ~~ tvars)}
   439   end
   440 
   441 fun arity_clause _ _ (_, []) = []
   442   | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)
   443     arity_clause seen n (tcons, ars)
   444   | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
   445     if member (op =) seen class then
   446       (* multiple arities for the same (tycon, class) pair *)
   447       make_axiom_arity_clause (tcons,
   448           lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
   449           ar) ::
   450       arity_clause seen (n + 1) (tcons, ars)
   451     else
   452       make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
   453                                ascii_of class, ar) ::
   454       arity_clause (class :: seen) n (tcons, ars)
   455 
   456 fun multi_arity_clause [] = []
   457   | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   458     arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   459 
   460 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
   461    theory thy provided its arguments have the corresponding sorts. *)
   462 fun type_class_pairs thy tycons classes =
   463   let
   464     val alg = Sign.classes_of thy
   465     fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
   466     fun add_class tycon class =
   467       cons (class, domain_sorts tycon class)
   468       handle Sorts.CLASS_ERROR _ => I
   469     fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
   470   in map try_classes tycons end
   471 
   472 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
   473 fun iter_type_class_pairs _ _ [] = ([], [])
   474   | iter_type_class_pairs thy tycons classes =
   475       let
   476         fun maybe_insert_class s =
   477           (s <> type_class andalso not (member (op =) classes s))
   478           ? insert (op =) s
   479         val cpairs = type_class_pairs thy tycons classes
   480         val newclasses =
   481           [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
   482         val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   483       in (classes' @ classes, union (op =) cpairs' cpairs) end
   484 
   485 fun make_arity_clauses thy tycons =
   486   iter_type_class_pairs thy tycons ##> multi_arity_clause
   487 
   488 
   489 (** Isabelle class relations **)
   490 
   491 type class_rel_clause =
   492   {name : string,
   493    subclass : name,
   494    superclass : name}
   495 
   496 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
   497    in theory "thy". *)
   498 fun class_pairs _ [] _ = []
   499   | class_pairs thy subs supers =
   500       let
   501         val class_less = Sorts.class_less (Sign.classes_of thy)
   502         fun add_super sub super = class_less (sub, super) ? cons (sub, super)
   503         fun add_supers sub = fold (add_super sub) supers
   504       in fold add_supers subs [] end
   505 
   506 fun make_class_rel_clause (sub, super) =
   507   {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
   508    superclass = `make_type_class super}
   509 
   510 fun make_class_rel_clauses thy subs supers =
   511   map make_class_rel_clause (class_pairs thy subs supers)
   512 
   513 (* intermediate terms *)
   514 datatype iterm =
   515   IConst of name * typ * typ list |
   516   IVar of name * typ |
   517   IApp of iterm * iterm |
   518   IAbs of (name * typ) * iterm
   519 
   520 fun ityp_of (IConst (_, T, _)) = T
   521   | ityp_of (IVar (_, T)) = T
   522   | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
   523   | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
   524 
   525 (*gets the head of a combinator application, along with the list of arguments*)
   526 fun strip_iterm_comb u =
   527   let
   528     fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
   529       | stripc x = x
   530   in stripc (u, []) end
   531 
   532 fun atomic_types_of T = fold_atyps (insert (op =)) T []
   533 
   534 val tvar_a_str = "'a"
   535 val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
   536 val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
   537 val itself_name = `make_fixed_type_const @{type_name itself}
   538 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
   539 val tvar_a_atype = AType (tvar_a_name, [])
   540 val a_itself_atype = AType (itself_name, [tvar_a_atype])
   541 
   542 fun new_skolem_const_name s num_T_args =
   543   [new_skolem_const_prefix, s, string_of_int num_T_args]
   544   |> Long_Name.implode
   545 
   546 val alpha_to_beta = Logic.varifyT_global @{typ "'a => 'b"}
   547 val alpha_to_beta_to_alpha_to_beta = alpha_to_beta --> alpha_to_beta
   548 
   549 fun robust_const_type thy s =
   550   if s = app_op_name then
   551     alpha_to_beta_to_alpha_to_beta
   552   else if String.isPrefix lam_lifted_prefix s then
   553     alpha_to_beta
   554   else
   555     (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
   556     s |> Sign.the_const_type thy
   557 
   558 val robust_const_ary =
   559   let
   560     fun ary (Type (@{type_name fun}, [_, T])) = 1 + ary T
   561       | ary _ = 0
   562   in ary oo robust_const_type end
   563 
   564 (* This function only makes sense if "T" is as general as possible. *)
   565 fun robust_const_typargs thy (s, T) =
   566   if s = app_op_name then
   567     let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
   568   else if String.isPrefix old_skolem_const_prefix s then
   569     [] |> Term.add_tvarsT T |> rev |> map TVar
   570   else if String.isPrefix lam_lifted_prefix s then
   571     if String.isPrefix lam_lifted_poly_prefix s then
   572       let val (T1, T2) = T |> dest_funT in [T1, T2] end
   573     else
   574       []
   575   else
   576     (s, T) |> Sign.const_typargs thy
   577 
   578 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
   579    Also accumulates sort infomation. *)
   580 fun iterm_from_term thy type_enc bs (P $ Q) =
   581     let
   582       val (P', P_atomics_Ts) = iterm_from_term thy type_enc bs P
   583       val (Q', Q_atomics_Ts) = iterm_from_term thy type_enc bs Q
   584     in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
   585   | iterm_from_term thy type_enc _ (Const (c, T)) =
   586     (IConst (`(make_fixed_const (SOME type_enc)) c, T,
   587              robust_const_typargs thy (c, T)),
   588      atomic_types_of T)
   589   | iterm_from_term _ _ _ (Free (s, T)) =
   590     (IConst (`make_fixed_var s, T, []), atomic_types_of T)
   591   | iterm_from_term _ type_enc _ (Var (v as (s, _), T)) =
   592     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
   593        let
   594          val Ts = T |> strip_type |> swap |> op ::
   595          val s' = new_skolem_const_name s (length Ts)
   596        in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
   597      else
   598        IVar ((make_schematic_var v, s), T), atomic_types_of T)
   599   | iterm_from_term _ _ bs (Bound j) =
   600     nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
   601   | iterm_from_term thy type_enc bs (Abs (s, T, t)) =
   602     let
   603       fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
   604       val s = vary s
   605       val name = `make_bound_var s
   606       val (tm, atomic_Ts) =
   607         iterm_from_term thy type_enc ((s, (name, T)) :: bs) t
   608     in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
   609 
   610 (* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
   611    Mirabelle. *)
   612 val queries = ["?", "_query"]
   613 val bangs = ["!", "_bang"]
   614 val ats = ["@", "_at"]
   615 
   616 fun try_unsuffixes ss s =
   617   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
   618 
   619 fun try_nonmono constr suffixes fallback s =
   620   case try_unsuffixes suffixes s of
   621     SOME s =>
   622     (case try_unsuffixes suffixes s of
   623        SOME s => (constr Positively_Naked_Vars, s)
   624      | NONE =>
   625        case try_unsuffixes ats s of
   626          SOME s => (constr Ghost_Type_Arg_Vars, s)
   627        | NONE => (constr All_Vars, s))
   628   | NONE => fallback s
   629 
   630 fun type_enc_from_string strictness s =
   631   (case try (unprefix "poly_") s of
   632      SOME s => (SOME Polymorphic, s)
   633    | NONE =>
   634      case try (unprefix "raw_mono_") s of
   635        SOME s => (SOME Raw_Monomorphic, s)
   636      | NONE =>
   637        case try (unprefix "mono_") s of
   638          SOME s => (SOME Mangled_Monomorphic, s)
   639        | NONE => (NONE, s))
   640   ||> (pair All_Types
   641        |> try_nonmono Fin_Nonmono_Types bangs
   642        |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
   643   |> (fn (poly, (level, core)) =>
   644          case (core, (poly, level)) of
   645            ("native", (SOME poly, _)) =>
   646            (case (poly, level) of
   647               (Polymorphic, All_Types) =>
   648               Native (First_Order, Polymorphic, All_Types)
   649             | (Mangled_Monomorphic, _) =>
   650               if granularity_of_type_level level = All_Vars then
   651                 Native (First_Order, Mangled_Monomorphic, level)
   652               else
   653                 raise Same.SAME
   654             | _ => raise Same.SAME)
   655          | ("native_higher", (SOME poly, _)) =>
   656            (case (poly, level) of
   657               (Polymorphic, All_Types) =>
   658               Native (Higher_Order THF_With_Choice, Polymorphic, All_Types)
   659             | (_, Noninf_Nonmono_Types _) => raise Same.SAME
   660             | (Mangled_Monomorphic, _) =>
   661               if granularity_of_type_level level = All_Vars then
   662                 Native (Higher_Order THF_With_Choice, Mangled_Monomorphic,
   663                         level)
   664               else
   665                 raise Same.SAME
   666             | _ => raise Same.SAME)
   667          | ("guards", (SOME poly, _)) =>
   668            if poly = Mangled_Monomorphic andalso
   669               granularity_of_type_level level = Ghost_Type_Arg_Vars then
   670              raise Same.SAME
   671            else
   672              Guards (poly, level)
   673          | ("tags", (SOME poly, _)) =>
   674            if granularity_of_type_level level = Ghost_Type_Arg_Vars then
   675              raise Same.SAME
   676            else
   677              Tags (poly, level)
   678          | ("args", (SOME poly, All_Types (* naja *))) =>
   679            Guards (poly, Const_Arg_Types)
   680          | ("erased", (NONE, All_Types (* naja *))) =>
   681            Guards (Polymorphic, No_Types)
   682          | _ => raise Same.SAME)
   683   handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
   684 
   685 fun adjust_order THF_Without_Choice (Higher_Order _) =
   686     Higher_Order THF_Without_Choice
   687   | adjust_order _ type_enc = type_enc
   688 
   689 fun adjust_type_enc (THF (TPTP_Polymorphic, _, flavor))
   690                     (Native (order, poly, level)) =
   691     Native (adjust_order flavor order, poly, level)
   692   | adjust_type_enc (THF (TPTP_Monomorphic, _, flavor))
   693                          (Native (order, _, level)) =
   694     Native (adjust_order flavor order, Mangled_Monomorphic, level)
   695   | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Native (_, _, level)) =
   696     Native (First_Order, Mangled_Monomorphic, level)
   697   | adjust_type_enc (DFG DFG_Sorted) (Native (_, _, level)) =
   698     Native (First_Order, Mangled_Monomorphic, level)
   699   | adjust_type_enc (TFF _) (Native (_, poly, level)) =
   700     Native (First_Order, poly, level)
   701   | adjust_type_enc format (Native (_, poly, level)) =
   702     adjust_type_enc format (Guards (poly, level))
   703   | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
   704     (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
   705   | adjust_type_enc _ type_enc = type_enc
   706 
   707 fun is_fol_term t =
   708   case t of
   709     @{const Not} $ t1 => is_fol_term t1
   710   | Const (@{const_name All}, _) $ Abs (_, _, t') => is_fol_term t'
   711   | Const (@{const_name All}, _) $ t1 => is_fol_term t1
   712   | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_fol_term t'
   713   | Const (@{const_name Ex}, _) $ t1 => is_fol_term t1
   714   | @{const HOL.conj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
   715   | @{const HOL.disj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
   716   | @{const HOL.implies} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
   717   | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   718     is_fol_term t1 andalso is_fol_term t2
   719   | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)
   720 
   721 fun simple_translate_lambdas do_lambdas ctxt t =
   722   if is_fol_term t then
   723     t
   724   else
   725     let
   726       fun trans Ts t =
   727         case t of
   728           @{const Not} $ t1 => @{const Not} $ trans Ts t1
   729         | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   730           t0 $ Abs (s, T, trans (T :: Ts) t')
   731         | (t0 as Const (@{const_name All}, _)) $ t1 =>
   732           trans Ts (t0 $ eta_expand Ts t1 1)
   733         | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   734           t0 $ Abs (s, T, trans (T :: Ts) t')
   735         | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   736           trans Ts (t0 $ eta_expand Ts t1 1)
   737         | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
   738           t0 $ trans Ts t1 $ trans Ts t2
   739         | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
   740           t0 $ trans Ts t1 $ trans Ts t2
   741         | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
   742           t0 $ trans Ts t1 $ trans Ts t2
   743         | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   744             $ t1 $ t2 =>
   745           t0 $ trans Ts t1 $ trans Ts t2
   746         | _ =>
   747           if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
   748           else t |> Envir.eta_contract |> do_lambdas ctxt Ts
   749       val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   750     in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
   751 
   752 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
   753     do_cheaply_conceal_lambdas Ts t1
   754     $ do_cheaply_conceal_lambdas Ts t2
   755   | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
   756     Const (lam_lifted_poly_prefix ^ serial_string (),
   757            T --> fastype_of1 (T :: Ts, t))
   758   | do_cheaply_conceal_lambdas _ t = t
   759 
   760 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
   761 fun conceal_bounds Ts t =
   762   subst_bounds (map (Free o apfst concealed_bound_name)
   763                     (0 upto length Ts - 1 ~~ Ts), t)
   764 fun reveal_bounds Ts =
   765   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   766                     (0 upto length Ts - 1 ~~ Ts))
   767 
   768 fun do_introduce_combinators ctxt Ts t =
   769   let val thy = Proof_Context.theory_of ctxt in
   770     t |> conceal_bounds Ts
   771       |> cterm_of thy
   772       |> Meson_Clausify.introduce_combinators_in_cterm
   773       |> prop_of |> Logic.dest_equals |> snd
   774       |> reveal_bounds Ts
   775   end
   776   (* A type variable of sort "{}" will make abstraction fail. *)
   777   handle THM _ => t |> do_cheaply_conceal_lambdas Ts
   778 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
   779 
   780 fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
   781   | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
   782   | constify_lifted (Free (x as (s, _))) =
   783     (if String.isPrefix lam_lifted_prefix s then Const else Free) x
   784   | constify_lifted t = t
   785 
   786 fun lift_lams_part_1 ctxt type_enc =
   787   map close_form #> rpair ctxt
   788   #-> Lambda_Lifting.lift_lambdas
   789           (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
   790                     lam_lifted_poly_prefix
   791                   else
   792                     lam_lifted_mono_prefix) ^ "_a"))
   793           Lambda_Lifting.is_quantifier
   794   #> fst
   795 
   796 fun lift_lams_part_2 ctxt (facts, lifted) =
   797   (facts, lifted)
   798   (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid
   799      of them *)
   800   |> pairself (map (introduce_combinators ctxt))
   801   |> pairself (map constify_lifted)
   802   (* Requires bound variables not to clash with any schematic variables (as
   803      should be the case right after lambda-lifting). *)
   804   |>> map (open_form (unprefix close_form_prefix))
   805   ||> map (open_form I)
   806 
   807 fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
   808 
   809 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
   810     intentionalize_def t
   811   | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
   812     let
   813       fun lam T t = Abs (Name.uu, T, t)
   814       val (head, args) = strip_comb t ||> rev
   815       val head_T = fastype_of head
   816       val n = length args
   817       val arg_Ts = head_T |> binder_types |> take n |> rev
   818       val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
   819     in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
   820   | intentionalize_def t = t
   821 
   822 type translated_formula =
   823   {name : string,
   824    stature : stature,
   825    role : formula_role,
   826    iformula : (name, typ, iterm) formula,
   827    atomic_types : typ list}
   828 
   829 fun update_iformula f ({name, stature, role, iformula, atomic_types}
   830                        : translated_formula) =
   831   {name = name, stature = stature, role = role, iformula = f iformula,
   832    atomic_types = atomic_types} : translated_formula
   833 
   834 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
   835 
   836 fun insert_type thy get_T x xs =
   837   let val T = get_T x in
   838     if exists (type_instance thy T o get_T) xs then xs
   839     else x :: filter_out (type_generalization thy T o get_T) xs
   840   end
   841 
   842 (* The Booleans indicate whether all type arguments should be kept. *)
   843 datatype type_arg_policy =
   844   Explicit_Type_Args of bool (* infer_from_term_args *) |
   845   Mangled_Type_Args |
   846   No_Type_Args
   847 
   848 fun type_arg_policy monom_constrs type_enc s =
   849   let val poly = polymorphism_of_type_enc type_enc in
   850     if s = type_tag_name then
   851       if poly = Mangled_Monomorphic then Mangled_Type_Args
   852       else Explicit_Type_Args false
   853     else case type_enc of
   854       Native (_, Polymorphic, _) => Explicit_Type_Args false
   855     | Tags (_, All_Types) => No_Type_Args
   856     | _ =>
   857       let val level = level_of_type_enc type_enc in
   858         if level = No_Types orelse s = @{const_name HOL.eq} orelse
   859            (s = app_op_name andalso level = Const_Arg_Types) then
   860           No_Type_Args
   861         else if poly = Mangled_Monomorphic then
   862           Mangled_Type_Args
   863         else if member (op =) monom_constrs s andalso
   864                 granularity_of_type_level level = Positively_Naked_Vars then
   865           No_Type_Args
   866         else
   867           Explicit_Type_Args
   868               (level = All_Types orelse
   869                granularity_of_type_level level = Ghost_Type_Arg_Vars)
   870       end
   871   end
   872 
   873 (* Make atoms for sorted type variables. *)
   874 fun generic_add_sorts_on_type (_, []) = I
   875   | generic_add_sorts_on_type ((x, i), s :: ss) =
   876     generic_add_sorts_on_type ((x, i), ss)
   877     #> (if s = the_single @{sort HOL.type} then
   878           I
   879         else if i = ~1 then
   880           insert (op =) (`make_type_class s, `make_fixed_type_var x)
   881         else
   882           insert (op =) (`make_type_class s,
   883                          (make_schematic_type_var (x, i), x)))
   884 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
   885   | add_sorts_on_tfree _ = I
   886 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
   887   | add_sorts_on_tvar _ = I
   888 
   889 fun type_class_formula type_enc class arg =
   890   AAtom (ATerm (class, arg ::
   891       (case type_enc of
   892          Native (First_Order, Polymorphic, _) =>
   893          if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
   894          else []
   895        | _ => [])))
   896 fun formulas_for_types type_enc add_sorts_on_typ Ts =
   897   [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
   898      |> map (fn (class, name) =>
   899                 type_class_formula type_enc class (ATerm (name, [])))
   900 
   901 fun mk_aconns c phis =
   902   let val (phis', phi') = split_last phis in
   903     fold_rev (mk_aconn c) phis' phi'
   904   end
   905 fun mk_ahorn [] phi = phi
   906   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
   907 fun mk_aquant _ [] phi = phi
   908   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
   909     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
   910   | mk_aquant q xs phi = AQuant (q, xs, phi)
   911 
   912 fun close_universally add_term_vars phi =
   913   let
   914     fun add_formula_vars bounds (AQuant (_, xs, phi)) =
   915         add_formula_vars (map fst xs @ bounds) phi
   916       | add_formula_vars bounds (AConn (_, phis)) =
   917         fold (add_formula_vars bounds) phis
   918       | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
   919   in mk_aquant AForall (add_formula_vars [] phi []) phi end
   920 
   921 fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
   922     (if is_tptp_variable s andalso
   923         not (String.isPrefix tvar_prefix s) andalso
   924         not (member (op =) bounds name) then
   925        insert (op =) (name, NONE)
   926      else
   927        I)
   928     #> fold (add_term_vars bounds) tms
   929   | add_term_vars bounds (AAbs (((name, _), tm), args)) =
   930     add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
   931 fun close_formula_universally phi = close_universally add_term_vars phi
   932 
   933 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
   934     fold (add_iterm_vars bounds) [tm1, tm2]
   935   | add_iterm_vars _ (IConst _) = I
   936   | add_iterm_vars bounds (IVar (name, T)) =
   937     not (member (op =) bounds name) ? insert (op =) (name, SOME T)
   938   | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
   939 
   940 fun close_iformula_universally phi = close_universally add_iterm_vars phi
   941 
   942 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
   943 val fused_infinite_type = Type (fused_infinite_type_name, [])
   944 
   945 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
   946 
   947 fun ho_term_from_typ type_enc =
   948   let
   949     fun term (Type (s, Ts)) =
   950       ATerm (case (is_type_enc_higher_order type_enc, s) of
   951                (true, @{type_name bool}) => `I tptp_bool_type
   952              | (true, @{type_name fun}) => `I tptp_fun_type
   953              | _ => if s = fused_infinite_type_name andalso
   954                        is_type_enc_native type_enc then
   955                       `I tptp_individual_type
   956                     else
   957                       `make_fixed_type_const s,
   958              map term Ts)
   959     | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
   960     | term (TVar (x, _)) = ATerm (tvar_name x, [])
   961   in term end
   962 
   963 fun ho_term_for_type_arg type_enc T =
   964   if T = dummyT then NONE else SOME (ho_term_from_typ type_enc T)
   965 
   966 (* This shouldn't clash with anything else. *)
   967 val uncurried_alias_sep = "\000"
   968 val mangled_type_sep = "\001"
   969 
   970 val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
   971 
   972 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   973   | generic_mangled_type_name f (ATerm (name, tys)) =
   974     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
   975     ^ ")"
   976   | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
   977 
   978 fun mangled_type type_enc =
   979   generic_mangled_type_name fst o ho_term_from_typ type_enc
   980 
   981 fun make_native_type s =
   982   if s = tptp_bool_type orelse s = tptp_fun_type orelse
   983      s = tptp_individual_type then
   984     s
   985   else
   986     native_type_prefix ^ ascii_of s
   987 
   988 fun ho_type_from_ho_term type_enc pred_sym ary =
   989   let
   990     fun to_mangled_atype ty =
   991       AType ((make_native_type (generic_mangled_type_name fst ty),
   992               generic_mangled_type_name snd ty), [])
   993     fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
   994       | to_poly_atype _ = raise Fail "unexpected type abstraction"
   995     val to_atype =
   996       if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
   997       else to_mangled_atype
   998     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
   999     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
  1000       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
  1001       | to_fo _ _ = raise Fail "unexpected type abstraction"
  1002     fun to_ho (ty as ATerm ((s, _), tys)) =
  1003         if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
  1004       | to_ho _ = raise Fail "unexpected type abstraction"
  1005   in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
  1006 
  1007 fun ho_type_from_typ type_enc pred_sym ary =
  1008   ho_type_from_ho_term type_enc pred_sym ary
  1009   o ho_term_from_typ type_enc
  1010 
  1011 fun aliased_uncurried ary (s, s') =
  1012   (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
  1013 fun unaliased_uncurried (s, s') =
  1014   case space_explode uncurried_alias_sep s of
  1015     [_] => (s, s')
  1016   | [s1, s2] => (s1, unsuffix s2 s')
  1017   | _ => raise Fail "ill-formed explicit application alias"
  1018 
  1019 fun raw_mangled_const_name type_name ty_args (s, s') =
  1020   let
  1021     fun type_suffix f g =
  1022       fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
  1023                ty_args ""
  1024   in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
  1025 fun mangled_const_name type_enc =
  1026   map_filter (ho_term_for_type_arg type_enc)
  1027   #> raw_mangled_const_name generic_mangled_type_name
  1028 
  1029 val parse_mangled_ident =
  1030   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
  1031 
  1032 fun parse_mangled_type x =
  1033   (parse_mangled_ident
  1034    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
  1035                     [] >> ATerm) x
  1036 and parse_mangled_types x =
  1037   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
  1038 
  1039 fun unmangled_type s =
  1040   s |> suffix ")" |> raw_explode
  1041     |> Scan.finite Symbol.stopper
  1042            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
  1043                                                 quote s)) parse_mangled_type))
  1044     |> fst
  1045 
  1046 fun unmangled_const_name s =
  1047   (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
  1048 fun unmangled_const s =
  1049   let val ss = unmangled_const_name s in
  1050     (hd ss, map unmangled_type (tl ss))
  1051   end
  1052 
  1053 fun introduce_proxies_in_iterm type_enc =
  1054   let
  1055     fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
  1056       | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
  1057                        _ =
  1058         (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
  1059            limitation. This works in conjuction with special code in
  1060            "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
  1061            possible. *)
  1062         IAbs ((`I "P", p_T),
  1063               IApp (IConst (`I ho_quant, T, []),
  1064                     IAbs ((`I "X", x_T),
  1065                           IApp (IConst (`I "P", p_T, []),
  1066                                 IConst (`I "X", x_T, [])))))
  1067       | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
  1068     fun intro top_level args (IApp (tm1, tm2)) =
  1069         IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
  1070       | intro top_level args (IConst (name as (s, _), T, T_args)) =
  1071         (case proxify_const s of
  1072            SOME proxy_base =>
  1073            if top_level orelse is_type_enc_higher_order type_enc then
  1074              case (top_level, s) of
  1075                (_, "c_False") => IConst (`I tptp_false, T, [])
  1076              | (_, "c_True") => IConst (`I tptp_true, T, [])
  1077              | (false, "c_Not") => IConst (`I tptp_not, T, [])
  1078              | (false, "c_conj") => IConst (`I tptp_and, T, [])
  1079              | (false, "c_disj") => IConst (`I tptp_or, T, [])
  1080              | (false, "c_implies") => IConst (`I tptp_implies, T, [])
  1081              | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
  1082              | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
  1083              | (false, s) =>
  1084                if is_tptp_equal s then
  1085                  if length args = 2 then
  1086                    IConst (`I tptp_equal, T, [])
  1087                  else
  1088                    (* Eta-expand partially applied THF equality, because the
  1089                       LEO-II and Satallax parsers complain about not being able to
  1090                       infer the type of "=". *)
  1091                    let val i_T = domain_type T in
  1092                      IAbs ((`I "Y", i_T),
  1093                            IAbs ((`I "Z", i_T),
  1094                                  IApp (IApp (IConst (`I tptp_equal, T, []),
  1095                                              IConst (`I "Y", i_T, [])),
  1096                                        IConst (`I "Z", i_T, []))))
  1097                    end
  1098                else
  1099                  IConst (name, T, [])
  1100              | _ => IConst (name, T, [])
  1101            else
  1102              IConst (proxy_base |>> prefix const_prefix, T, T_args)
  1103           | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
  1104                     else IConst (name, T, T_args))
  1105       | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
  1106       | intro _ _ tm = tm
  1107   in intro true [] end
  1108 
  1109 fun mangle_type_args_in_const type_enc (name as (s, _)) T_args =
  1110   case unprefix_and_unascii const_prefix s of
  1111     NONE => (name, T_args)
  1112   | SOME s'' =>
  1113     case type_arg_policy [] type_enc (invert_const s'') of
  1114       Mangled_Type_Args => (mangled_const_name type_enc T_args name, [])
  1115     | _ => (name, T_args)
  1116 fun mangle_type_args_in_iterm type_enc =
  1117   if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
  1118     let
  1119       fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
  1120         | mangle (tm as IConst (_, _, [])) = tm
  1121         | mangle (IConst (name, T, T_args)) =
  1122           mangle_type_args_in_const type_enc name T_args
  1123           |> (fn (name, T_args) => IConst (name, T, T_args))
  1124         | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
  1125         | mangle tm = tm
  1126     in mangle end
  1127   else
  1128     I
  1129 
  1130 fun chop_fun 0 T = ([], T)
  1131   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
  1132     chop_fun (n - 1) ran_T |>> cons dom_T
  1133   | chop_fun _ T = ([], T)
  1134 
  1135 fun filter_const_type_args _ _ _ [] = []
  1136   | filter_const_type_args thy s ary T_args =
  1137     let
  1138       val U = robust_const_type thy s
  1139       val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
  1140       val U_args = (s, U) |> robust_const_typargs thy
  1141     in
  1142       U_args ~~ T_args
  1143       |> map (fn (U, T) =>
  1144                  if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
  1145     end
  1146     handle TYPE _ => T_args
  1147 
  1148 fun filter_type_args_in_const _ _ _ _ _ [] = []
  1149   | filter_type_args_in_const thy monom_constrs type_enc ary s T_args =
  1150     case unprefix_and_unascii const_prefix s of
  1151       NONE =>
  1152       if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
  1153       else T_args
  1154     | SOME s'' =>
  1155       let
  1156         val s'' = invert_const s''
  1157         fun filter_T_args false = T_args
  1158           | filter_T_args true = filter_const_type_args thy s'' ary T_args
  1159       in
  1160         case type_arg_policy monom_constrs type_enc s'' of
  1161           Explicit_Type_Args infer_from_term_args =>
  1162           filter_T_args infer_from_term_args
  1163         | No_Type_Args => []
  1164         | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
  1165       end
  1166 fun filter_type_args_in_iterm thy monom_constrs type_enc =
  1167   let
  1168     fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
  1169       | filt ary (IConst (name as (s, _), T, T_args)) =
  1170         filter_type_args_in_const thy monom_constrs type_enc ary s T_args
  1171         |> (fn T_args => IConst (name, T, T_args))
  1172       | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
  1173       | filt _ tm = tm
  1174   in filt 0 end
  1175 
  1176 fun iformula_from_prop ctxt type_enc iff_for_eq =
  1177   let
  1178     val thy = Proof_Context.theory_of ctxt
  1179     fun do_term bs t atomic_Ts =
  1180       iterm_from_term thy type_enc bs (Envir.eta_contract t)
  1181       |>> (introduce_proxies_in_iterm type_enc
  1182            #> mangle_type_args_in_iterm type_enc #> AAtom)
  1183       ||> union (op =) atomic_Ts
  1184     fun do_quant bs q pos s T t' =
  1185       let
  1186         val s = singleton (Name.variant_list (map fst bs)) s
  1187         val universal = Option.map (q = AExists ? not) pos
  1188         val name =
  1189           s |> `(case universal of
  1190                    SOME true => make_all_bound_var
  1191                  | SOME false => make_exist_bound_var
  1192                  | NONE => make_bound_var)
  1193       in
  1194         do_formula ((s, (name, T)) :: bs) pos t'
  1195         #>> mk_aquant q [(name, SOME T)]
  1196         ##> union (op =) (atomic_types_of T)
  1197       end
  1198     and do_conn bs c pos1 t1 pos2 t2 =
  1199       do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
  1200     and do_formula bs pos t =
  1201       case t of
  1202         @{const Trueprop} $ t1 => do_formula bs pos t1
  1203       | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
  1204       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
  1205         do_quant bs AForall pos s T t'
  1206       | (t0 as Const (@{const_name All}, _)) $ t1 =>
  1207         do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
  1208       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
  1209         do_quant bs AExists pos s T t'
  1210       | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
  1211         do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
  1212       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
  1213       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
  1214       | @{const HOL.implies} $ t1 $ t2 =>
  1215         do_conn bs AImplies (Option.map not pos) t1 pos t2
  1216       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
  1217         if iff_for_eq then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
  1218       | _ => do_term bs t
  1219   in do_formula [] end
  1220 
  1221 fun presimplify_term thy t =
  1222   if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
  1223     t |> Skip_Proof.make_thm thy
  1224       |> Meson.presimplify
  1225       |> prop_of
  1226   else
  1227     t
  1228 
  1229 fun preprocess_abstractions_in_terms trans_lams facts =
  1230   let
  1231     val (facts, lambda_ts) =
  1232       facts |> map (snd o snd) |> trans_lams
  1233             |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
  1234     val lam_facts =
  1235       map2 (fn t => fn j =>
  1236                ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t)))
  1237            lambda_ts (1 upto length lambda_ts)
  1238   in (facts, lam_facts) end
  1239 
  1240 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
  1241    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
  1242 fun freeze_term t =
  1243   let
  1244     fun freeze (t $ u) = freeze t $ freeze u
  1245       | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
  1246       | freeze (Var ((s, i), T)) =
  1247         Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
  1248       | freeze t = t
  1249   in t |> exists_subterm is_Var t ? freeze end
  1250 
  1251 fun unextensionalize_def t =
  1252   case t of
  1253     @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
  1254     (case strip_comb lhs of
  1255        (c as Const (_, T), args) =>
  1256        if forall is_Var args andalso not (has_duplicates (op =) args) then
  1257          @{const Trueprop}
  1258          $ (Const (@{const_name HOL.eq}, T --> T --> @{typ bool})
  1259             $ c $ fold_rev lambda args rhs)
  1260        else
  1261          t
  1262      | _ => t)
  1263   | _ => t
  1264 
  1265 fun presimp_prop ctxt type_enc t =
  1266   let
  1267     val thy = Proof_Context.theory_of ctxt
  1268     val t = t |> Envir.beta_eta_contract
  1269               |> transform_elim_prop
  1270               |> Object_Logic.atomize_term thy
  1271     val need_trueprop = (fastype_of t = @{typ bool})
  1272     val is_ho = is_type_enc_higher_order type_enc
  1273   in
  1274     t |> need_trueprop ? HOLogic.mk_Trueprop
  1275       |> (if is_ho then unextensionalize_def
  1276           else cong_extensionalize_term thy #> abs_extensionalize_term ctxt)
  1277       |> presimplify_term thy
  1278       |> HOLogic.dest_Trueprop
  1279   end
  1280   handle TERM _ => @{const True}
  1281 
  1282 (* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "="
  1283    for obscure technical reasons. *)
  1284 fun should_use_iff_for_eq CNF _ = false
  1285   | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
  1286   | should_use_iff_for_eq _ _ = true
  1287 
  1288 fun make_formula ctxt format type_enc iff_for_eq name stature role t =
  1289   let
  1290     val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
  1291     val (iformula, atomic_Ts) =
  1292       iformula_from_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t
  1293                          []
  1294       |>> close_iformula_universally
  1295   in
  1296     {name = name, stature = stature, role = role, iformula = iformula,
  1297      atomic_types = atomic_Ts}
  1298   end
  1299 
  1300 fun is_legitimate_thf_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
  1301     (is_Const t orelse is_Free t) andalso
  1302     not (exists_subterm (curry (op =) t) u)
  1303   | is_legitimate_thf_def _ = false
  1304 
  1305 fun make_fact ctxt format type_enc iff_for_eq
  1306               ((name, stature as (_, status)), t) =
  1307   let
  1308     val role =
  1309       if is_type_enc_higher_order type_enc andalso status = Def andalso
  1310          is_legitimate_thf_def t then
  1311         Definition
  1312       else
  1313         Axiom
  1314   in
  1315     case t |> make_formula ctxt format type_enc iff_for_eq name stature role of
  1316       formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
  1317       if s = tptp_true then NONE else SOME formula
  1318     | formula => SOME formula
  1319   end
  1320 
  1321 fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
  1322   | s_not_prop _ = @{prop True} (* "t" is too meta for "metis" *)
  1323 (*
  1324   | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
  1325   | s_not_prop t = @{const "==>"} $ t $ @{prop False}
  1326 *)
  1327 
  1328 fun make_conjecture ctxt format type_enc =
  1329   map (fn ((name, stature), (role, t)) =>
  1330           t |> role = Conjecture ? s_not
  1331             |> make_formula ctxt format type_enc true name stature role)
  1332 
  1333 (** Finite and infinite type inference **)
  1334 
  1335 fun tvar_footprint thy s ary =
  1336   (case unprefix_and_unascii const_prefix s of
  1337      SOME s =>
  1338      s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
  1339        |> map (fn T => Term.add_tvarsT T [] |> map fst)
  1340    | NONE => [])
  1341   handle TYPE _ => []
  1342 
  1343 fun ghost_type_args thy s ary =
  1344   if is_tptp_equal s then
  1345     0 upto ary - 1
  1346   else
  1347     let
  1348       val footprint = tvar_footprint thy s ary
  1349       val eq = (s = @{const_name HOL.eq})
  1350       fun ghosts _ [] = []
  1351         | ghosts seen ((i, tvars) :: args) =
  1352           ghosts (union (op =) seen tvars) args
  1353           |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
  1354              ? cons i
  1355     in
  1356       if forall null footprint then
  1357         []
  1358       else
  1359         0 upto length footprint - 1 ~~ footprint
  1360         |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
  1361         |> ghosts []
  1362     end
  1363 
  1364 type monotonicity_info =
  1365   {maybe_finite_Ts : typ list,
  1366    surely_finite_Ts : typ list,
  1367    maybe_infinite_Ts : typ list,
  1368    surely_infinite_Ts : typ list,
  1369    maybe_nonmono_Ts : typ list}
  1370 
  1371 (* These types witness that the type classes they belong to allow infinite
  1372    models and hence that any types with these type classes is monotonic. *)
  1373 val known_infinite_types =
  1374   [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
  1375 
  1376 fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
  1377   strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
  1378 
  1379 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
  1380    dangerous because their "exhaust" properties can easily lead to unsound ATP
  1381    proofs. On the other hand, all HOL infinite types can be given the same
  1382    models in first-order logic (via Löwenheim-Skolem). *)
  1383 
  1384 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
  1385   | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
  1386                              maybe_nonmono_Ts, ...}
  1387                        (Noninf_Nonmono_Types (strictness, grain)) T =
  1388     let val thy = Proof_Context.theory_of ctxt in
  1389       grain = Ghost_Type_Arg_Vars orelse
  1390       (exists (type_intersect thy T) maybe_nonmono_Ts andalso
  1391        not (exists (type_instance thy T) surely_infinite_Ts orelse
  1392             (not (member (type_equiv thy) maybe_finite_Ts T) andalso
  1393              is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
  1394                                              T)))
  1395     end
  1396   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
  1397                              maybe_nonmono_Ts, ...}
  1398                        (Fin_Nonmono_Types grain) T =
  1399     let val thy = Proof_Context.theory_of ctxt in
  1400       grain = Ghost_Type_Arg_Vars orelse
  1401       (exists (type_intersect thy T) maybe_nonmono_Ts andalso
  1402        (exists (type_generalization thy T) surely_finite_Ts orelse
  1403         (not (member (type_equiv thy) maybe_infinite_Ts T) andalso
  1404          is_type_surely_finite ctxt T)))
  1405     end
  1406   | should_encode_type _ _ _ _ = false
  1407 
  1408 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
  1409     should_guard_var () andalso should_encode_type ctxt mono level T
  1410   | should_guard_type _ _ _ _ _ = false
  1411 
  1412 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
  1413     String.isPrefix bound_var_prefix s orelse
  1414     String.isPrefix all_bound_var_prefix s
  1415   | is_maybe_universal_var (IVar _) = true
  1416   | is_maybe_universal_var _ = false
  1417 
  1418 datatype site =
  1419   Top_Level of bool option |
  1420   Eq_Arg of bool option |
  1421   Elsewhere
  1422 
  1423 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
  1424   | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
  1425     if granularity_of_type_level level = All_Vars then
  1426       should_encode_type ctxt mono level T
  1427     else
  1428       (case (site, is_maybe_universal_var u) of
  1429          (Eq_Arg _, true) => should_encode_type ctxt mono level T
  1430        | _ => false)
  1431   | should_tag_with_type _ _ _ _ _ _ = false
  1432 
  1433 fun fused_type ctxt mono level =
  1434   let
  1435     val should_encode = should_encode_type ctxt mono level
  1436     fun fuse 0 T = if should_encode T then T else fused_infinite_type
  1437       | fuse ary (Type (@{type_name fun}, [T1, T2])) =
  1438         fuse 0 T1 --> fuse (ary - 1) T2
  1439       | fuse _ _ = raise Fail "expected function type"
  1440   in fuse end
  1441 
  1442 (** predicators and application operators **)
  1443 
  1444 type sym_info =
  1445   {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
  1446    in_conj : bool}
  1447 
  1448 fun default_sym_tab_entries type_enc =
  1449   (make_fixed_const NONE @{const_name undefined},
  1450        {pred_sym = false, min_ary = 0, max_ary = 0, types = [],
  1451         in_conj = false}) ::
  1452   ([tptp_false, tptp_true]
  1453    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [],
  1454                   in_conj = false})) @
  1455   ([tptp_equal, tptp_old_equal]
  1456    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [],
  1457                   in_conj = false}))
  1458   |> not (is_type_enc_higher_order type_enc)
  1459      ? cons (prefixed_predicator_name,
  1460              {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
  1461               in_conj = false})
  1462 
  1463 datatype app_op_level =
  1464   Min_App_Op |
  1465   Sufficient_App_Op |
  1466   Sufficient_App_Op_And_Predicator |
  1467   Full_App_Op_And_Predicator
  1468 
  1469 fun add_iterm_syms_to_sym_table ctxt app_op_level conj_fact =
  1470   let
  1471     val thy = Proof_Context.theory_of ctxt
  1472     fun consider_var_ary const_T var_T max_ary =
  1473       let
  1474         fun iter ary T =
  1475           if ary = max_ary orelse type_instance thy var_T T orelse
  1476              type_instance thy T var_T then
  1477             ary
  1478           else
  1479             iter (ary + 1) (range_type T)
  1480       in iter 0 const_T end
  1481     fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1482       if (app_op_level = Sufficient_App_Op andalso can dest_funT T) orelse
  1483          (app_op_level = Sufficient_App_Op_And_Predicator andalso
  1484           (can dest_funT T orelse T = @{typ bool})) then
  1485         let
  1486           val bool_vars' =
  1487             bool_vars orelse
  1488             (app_op_level = Sufficient_App_Op_And_Predicator andalso
  1489              body_type T = @{typ bool})
  1490           fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
  1491             {pred_sym = pred_sym andalso not bool_vars',
  1492              min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
  1493              max_ary = max_ary, types = types, in_conj = in_conj}
  1494           val fun_var_Ts' =
  1495             fun_var_Ts |> can dest_funT T ? insert_type thy I T
  1496         in
  1497           if bool_vars' = bool_vars andalso
  1498              pointer_eq (fun_var_Ts', fun_var_Ts) then
  1499             accum
  1500           else
  1501             ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
  1502         end
  1503       else
  1504         accum
  1505     fun add_iterm_syms top_level tm
  1506                        (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1507       let val (head, args) = strip_iterm_comb tm in
  1508         (case head of
  1509            IConst ((s, _), T, _) =>
  1510            if String.isPrefix bound_var_prefix s orelse
  1511               String.isPrefix all_bound_var_prefix s then
  1512              add_universal_var T accum
  1513            else if String.isPrefix exist_bound_var_prefix s then
  1514              accum
  1515            else
  1516              let val ary = length args in
  1517                ((bool_vars, fun_var_Ts),
  1518                 case Symtab.lookup sym_tab s of
  1519                   SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
  1520                   let
  1521                     val pred_sym =
  1522                       pred_sym andalso top_level andalso not bool_vars
  1523                     val types' = types |> insert_type thy I T
  1524                     val in_conj = in_conj orelse conj_fact
  1525                     val min_ary =
  1526                       if (app_op_level = Sufficient_App_Op orelse
  1527                           app_op_level = Sufficient_App_Op_And_Predicator)
  1528                          andalso not (pointer_eq (types', types)) then
  1529                         fold (consider_var_ary T) fun_var_Ts min_ary
  1530                       else
  1531                         min_ary
  1532                   in
  1533                     Symtab.update (s, {pred_sym = pred_sym,
  1534                                        min_ary = Int.min (ary, min_ary),
  1535                                        max_ary = Int.max (ary, max_ary),
  1536                                        types = types', in_conj = in_conj})
  1537                                   sym_tab
  1538                   end
  1539                 | NONE =>
  1540                   let
  1541                     val pred_sym = top_level andalso not bool_vars
  1542                     val ary =
  1543                       case unprefix_and_unascii const_prefix s of
  1544                         SOME s =>
  1545                         (if String.isSubstring uncurried_alias_sep s then
  1546                            ary
  1547                          else case try (robust_const_ary thy
  1548                                         o invert_const o hd
  1549                                         o unmangled_const_name) s of
  1550                            SOME ary0 => Int.min (ary0, ary)
  1551                          | NONE => ary)
  1552                       | NONE => ary
  1553                     val min_ary =
  1554                       case app_op_level of
  1555                         Min_App_Op => ary
  1556                       | Full_App_Op_And_Predicator => 0
  1557                       | _ => fold (consider_var_ary T) fun_var_Ts ary
  1558                   in
  1559                     Symtab.update_new (s,
  1560                         {pred_sym = pred_sym, min_ary = min_ary,
  1561                          max_ary = ary, types = [T], in_conj = conj_fact})
  1562                         sym_tab
  1563                   end)
  1564              end
  1565          | IVar (_, T) => add_universal_var T accum
  1566          | IAbs ((_, T), tm) =>
  1567            accum |> add_universal_var T |> add_iterm_syms false tm
  1568          | _ => accum)
  1569         |> fold (add_iterm_syms false) args
  1570       end
  1571   in add_iterm_syms end
  1572 
  1573 fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
  1574   let
  1575     fun add_iterm_syms conj_fact =
  1576       add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
  1577     fun add_fact_syms conj_fact =
  1578       K (add_iterm_syms conj_fact) |> formula_fold NONE |> fact_lift
  1579   in
  1580     ((false, []), Symtab.empty)
  1581     |> fold (add_fact_syms true) conjs
  1582     |> fold (add_fact_syms false) facts
  1583     ||> fold Symtab.update (default_sym_tab_entries type_enc)
  1584   end
  1585 
  1586 fun min_ary_of sym_tab s =
  1587   case Symtab.lookup sym_tab s of
  1588     SOME ({min_ary, ...} : sym_info) => min_ary
  1589   | NONE =>
  1590     case unprefix_and_unascii const_prefix s of
  1591       SOME s =>
  1592       let val s = s |> unmangled_const_name |> hd |> invert_const in
  1593         if s = predicator_name then 1
  1594         else if s = app_op_name then 2
  1595         else if s = type_guard_name then 1
  1596         else 0
  1597       end
  1598     | NONE => 0
  1599 
  1600 (* True if the constant ever appears outside of the top-level position in
  1601    literals, or if it appears with different arities (e.g., because of different
  1602    type instantiations). If false, the constant always receives all of its
  1603    arguments and is used as a predicate. *)
  1604 fun is_pred_sym sym_tab s =
  1605   case Symtab.lookup sym_tab s of
  1606     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
  1607     pred_sym andalso min_ary = max_ary
  1608   | NONE => false
  1609 
  1610 val fTrue_iconst =
  1611   IConst ((const_prefix ^ "fTrue", @{const_name ATP.fTrue}), @{typ bool}, [])
  1612 val predicator_iconst =
  1613   IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
  1614 
  1615 fun predicatify aggressive tm =
  1616   if aggressive then
  1617     IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm),
  1618           fTrue_iconst)
  1619   else
  1620     IApp (predicator_iconst, tm)
  1621 
  1622 val app_op = `(make_fixed_const NONE) app_op_name
  1623 
  1624 fun list_app head args = fold (curry (IApp o swap)) args head
  1625 
  1626 fun mk_app_op type_enc head arg =
  1627   let
  1628     val head_T = ityp_of head
  1629     val (arg_T, res_T) = dest_funT head_T
  1630     val app =
  1631       IConst (app_op, head_T --> head_T, [arg_T, res_T])
  1632       |> mangle_type_args_in_iterm type_enc
  1633   in list_app app [head, arg] end
  1634 
  1635 fun firstorderize_fact thy monom_constrs type_enc sym_tab uncurried_aliases
  1636                        aggressive =
  1637   let
  1638     fun do_app arg head = mk_app_op type_enc head arg
  1639     fun list_app_ops head args = fold do_app args head
  1640     fun introduce_app_ops tm =
  1641       let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
  1642         case head of
  1643           IConst (name as (s, _), T, T_args) =>
  1644           if uncurried_aliases andalso String.isPrefix const_prefix s then
  1645             let
  1646               val ary = length args
  1647               val name =
  1648                 name |> ary > min_ary_of sym_tab s ? aliased_uncurried ary
  1649             in list_app (IConst (name, T, T_args)) args end
  1650           else
  1651             args |> chop (min_ary_of sym_tab s)
  1652                  |>> list_app head |-> list_app_ops
  1653         | _ => list_app_ops head args
  1654       end
  1655     fun introduce_predicators tm =
  1656       case strip_iterm_comb tm of
  1657         (IConst ((s, _), _, _), _) =>
  1658         if is_pred_sym sym_tab s then tm else predicatify aggressive tm
  1659       | _ => predicatify aggressive tm
  1660     val do_iterm =
  1661       not (is_type_enc_higher_order type_enc)
  1662       ? (introduce_app_ops #> introduce_predicators)
  1663       #> filter_type_args_in_iterm thy monom_constrs type_enc
  1664   in update_iformula (formula_map do_iterm) end
  1665 
  1666 (** Helper facts **)
  1667 
  1668 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
  1669 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
  1670 
  1671 (* The Boolean indicates that a fairly sound type encoding is needed. *)
  1672 val base_helper_table =
  1673   [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]),
  1674    (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]),
  1675    (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]),
  1676    (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]),
  1677    (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]),
  1678    ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
  1679    (("fFalse", false), [(General, not_ffalse)]),
  1680    (("fFalse", true), [(General, @{thm True_or_False})]),
  1681    (("fTrue", false), [(General, ftrue)]),
  1682    (("fTrue", true), [(General, @{thm True_or_False})]),
  1683    (("If", true),
  1684     [(Def, @{thm if_True}), (Def, @{thm if_False}),
  1685      (General, @{thm True_or_False})])]
  1686 
  1687 val helper_table =
  1688   base_helper_table @
  1689   [(("fNot", false),
  1690     @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1691            fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
  1692     |> map (pair Def)),
  1693    (("fconj", false),
  1694     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
  1695         by (unfold fconj_def) fast+}
  1696     |> map (pair General)),
  1697    (("fdisj", false),
  1698     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
  1699         by (unfold fdisj_def) fast+}
  1700     |> map (pair General)),
  1701    (("fimplies", false),
  1702     @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
  1703         by (unfold fimplies_def) fast+}
  1704     |> map (pair General)),
  1705    (("fequal", true),
  1706     (* This is a lie: Higher-order equality doesn't need a sound type encoding.
  1707        However, this is done so for backward compatibility: Including the
  1708        equality helpers by default in Metis breaks a few existing proofs. *)
  1709     @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1710            fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
  1711     |> map (pair General)),
  1712    (* Partial characterization of "fAll" and "fEx". A complete characterization
  1713       would require the axiom of choice for replay with Metis. *)
  1714    (("fAll", false),
  1715     [(General, @{lemma "~ fAll P | P x" by (auto simp: fAll_def)})]),
  1716    (("fEx", false),
  1717     [(General, @{lemma "~ P x | fEx P" by (auto simp: fEx_def)})])]
  1718   |> map (apsnd (map (apsnd zero_var_indexes)))
  1719 
  1720 val aggressive_helper_table =
  1721   base_helper_table @
  1722   [((predicator_name, true),
  1723     @{thms True_or_False fTrue_ne_fFalse} |> map (pair General)),
  1724    ((app_op_name, true),
  1725     [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
  1726    (("fconj", false),
  1727     @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)),
  1728    (("fdisj", false),
  1729     @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)),
  1730    (("fimplies", false),
  1731     @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
  1732     |> map (pair Def)),
  1733    (("fequal", false),
  1734     (@{thms fequal_table} |> map (pair Def)) @
  1735     (@{thms fequal_laws} |> map (pair General))),
  1736    (("fAll", false),
  1737     @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)),
  1738    (("fEx", false),
  1739     @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
  1740   |> map (apsnd (map (apsnd zero_var_indexes)))
  1741 
  1742 fun atype_of_type_vars (Native (_, Polymorphic, _)) = SOME atype_of_types
  1743   | atype_of_type_vars _ = NONE
  1744 
  1745 fun bound_tvars type_enc sorts Ts =
  1746   (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
  1747   #> mk_aquant AForall
  1748         (map_filter (fn TVar (x as (s, _), _) =>
  1749                         SOME ((make_schematic_type_var x, s),
  1750                               atype_of_type_vars type_enc)
  1751                       | _ => NONE) Ts)
  1752 
  1753 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
  1754   (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
  1755    else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
  1756   |> mk_aquant AForall bounds
  1757   |> close_formula_universally
  1758   |> bound_tvars type_enc true atomic_Ts
  1759 
  1760 val helper_rank = default_rank
  1761 val min_rank = 9 * helper_rank div 10
  1762 val max_rank = 4 * min_rank
  1763 
  1764 fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n
  1765 
  1766 val type_tag = `(make_fixed_const NONE) type_tag_name
  1767 
  1768 fun could_specialize_helpers type_enc =
  1769   polymorphism_of_type_enc type_enc <> Polymorphic andalso
  1770   level_of_type_enc type_enc <> No_Types
  1771 fun should_specialize_helper type_enc t =
  1772   could_specialize_helpers type_enc andalso
  1773   not (null (Term.hidden_polymorphism t))
  1774 
  1775 fun add_helper_facts_for_sym ctxt format type_enc aggressive
  1776                              (s, {types, ...} : sym_info) =
  1777   case unprefix_and_unascii const_prefix s of
  1778     SOME mangled_s =>
  1779     let
  1780       val thy = Proof_Context.theory_of ctxt
  1781       val unmangled_s = mangled_s |> unmangled_const_name |> hd
  1782       fun dub needs_fairly_sound j k =
  1783         ascii_of unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
  1784         (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
  1785         (if needs_fairly_sound then typed_helper_suffix
  1786          else untyped_helper_suffix)
  1787       fun specialize_helper t T =
  1788         if unmangled_s = app_op_name then
  1789           let
  1790             val tyenv =
  1791               Sign.typ_match thy (alpha_to_beta, domain_type T) Vartab.empty
  1792           in monomorphic_term tyenv t end
  1793         else
  1794           specialize_type thy (invert_const unmangled_s, T) t
  1795       fun dub_and_inst needs_fairly_sound ((status, t), j) =
  1796         (if should_specialize_helper type_enc t then
  1797            map_filter (try (specialize_helper t)) types
  1798          else
  1799            [t])
  1800         |> tag_list 1
  1801         |> map (fn (k, t) =>
  1802                    ((dub needs_fairly_sound j k, (Global, status)), t))
  1803       val make_facts = map_filter (make_fact ctxt format type_enc false)
  1804       val fairly_sound = is_type_enc_fairly_sound type_enc
  1805       val could_specialize = could_specialize_helpers type_enc
  1806     in
  1807       fold (fn ((helper_s, needs_fairly_sound), ths) =>
  1808                if (needs_fairly_sound andalso not fairly_sound) orelse
  1809                   (helper_s <> unmangled_s andalso
  1810                    (not aggressive orelse could_specialize)) then
  1811                  I
  1812                else
  1813                  ths ~~ (1 upto length ths)
  1814                  |> maps (dub_and_inst needs_fairly_sound
  1815                           o apfst (apsnd prop_of))
  1816                  |> make_facts
  1817                  |> union (op = o pairself #iformula))
  1818            (if aggressive then aggressive_helper_table else helper_table)
  1819     end
  1820   | NONE => I
  1821 fun helper_facts_for_sym_table ctxt format type_enc aggressive sym_tab =
  1822   Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc aggressive)
  1823                   sym_tab []
  1824 
  1825 (***************************************************************)
  1826 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
  1827 (***************************************************************)
  1828 
  1829 fun set_insert (x, s) = Symtab.update (x, ()) s
  1830 
  1831 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
  1832 
  1833 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
  1834 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
  1835 
  1836 fun classes_of_terms get_Ts =
  1837   map (map snd o get_Ts)
  1838   #> List.foldl add_classes Symtab.empty
  1839   #> delete_type #> Symtab.keys
  1840 
  1841 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
  1842 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
  1843 
  1844 fun fold_type_constrs f (Type (s, Ts)) x =
  1845     fold (fold_type_constrs f) Ts (f (s, x))
  1846   | fold_type_constrs _ _ x = x
  1847 
  1848 (* Type constructors used to instantiate overloaded constants are the only ones
  1849    needed. *)
  1850 fun add_type_constrs_in_term thy =
  1851   let
  1852     fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
  1853       | add (t $ u) = add t #> add u
  1854       | add (Const x) =
  1855         x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
  1856       | add (Abs (_, _, u)) = add u
  1857       | add _ = I
  1858   in add end
  1859 
  1860 fun type_constrs_of_terms thy ts =
  1861   Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
  1862 
  1863 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
  1864     let val (head, args) = strip_comb t in
  1865       (head |> dest_Const |> fst,
  1866        fold_rev (fn t as Var ((s, _), T) =>
  1867                     (fn u => Abs (s, T, abstract_over (t, u)))
  1868                   | _ => raise Fail "expected \"Var\"") args u)
  1869     end
  1870   | extract_lambda_def _ = raise Fail "malformed lifted lambda"
  1871 
  1872 fun trans_lams_from_string ctxt type_enc lam_trans =
  1873   if lam_trans = no_lamsN then
  1874     rpair []
  1875   else if lam_trans = hide_lamsN then
  1876     lift_lams ctxt type_enc ##> K []
  1877   else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
  1878     lift_lams ctxt type_enc
  1879   else if lam_trans = combsN then
  1880     map (introduce_combinators ctxt) #> rpair []
  1881   else if lam_trans = combs_and_liftingN then
  1882     lift_lams_part_1 ctxt type_enc
  1883     ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
  1884     #> lift_lams_part_2 ctxt
  1885   else if lam_trans = combs_or_liftingN then
  1886     lift_lams_part_1 ctxt type_enc
  1887     ##> map (fn t => case head_of (strip_qnt_body @{const_name All} t) of
  1888                        @{term "op =::bool => bool => bool"} => t
  1889                      | _ => introduce_combinators ctxt (intentionalize_def t))
  1890     #> lift_lams_part_2 ctxt
  1891   else if lam_trans = keep_lamsN then
  1892     map (Envir.eta_contract) #> rpair []
  1893   else
  1894     error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
  1895 
  1896 fun order_definitions facts =
  1897   let
  1898     fun add_consts (IApp (t, u)) = fold add_consts [t, u]
  1899       | add_consts (IAbs (_, t)) = add_consts t
  1900       | add_consts (IConst (name, _, _)) = insert (op =) name
  1901       | add_consts (IVar _) = I
  1902     fun consts_of_hs l_or_r (_, {iformula, ...} : translated_formula) =
  1903       case iformula of
  1904         AAtom (IApp (IApp (IConst _, t), u)) => add_consts (l_or_r (t, u)) []
  1905       | _ => []
  1906     (* Quadratic, but usually OK. *)
  1907     fun order [] [] = []
  1908       | order (fact :: skipped) [] = fact :: order [] skipped (* break cycle *)
  1909       | order skipped (fact :: facts) =
  1910         let val rhs_consts = consts_of_hs snd fact in
  1911           if exists (exists (member (op =) rhs_consts o the_single
  1912                      o consts_of_hs fst))
  1913                     [skipped, facts] then
  1914             order (fact :: skipped) facts
  1915           else
  1916             fact :: order [] (facts @ skipped)
  1917         end
  1918   in order [] facts end
  1919 
  1920 fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
  1921                        concl_t facts =
  1922   let
  1923     val thy = Proof_Context.theory_of ctxt
  1924     val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
  1925     val fact_ts = facts |> map snd
  1926     (* Remove existing facts from the conjecture, as this can dramatically
  1927        boost an ATP's performance (for some reason). *)
  1928     val hyp_ts =
  1929       hyp_ts
  1930       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
  1931     val facts = facts |> map (apsnd (pair Axiom))
  1932     val conjs =
  1933       map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
  1934       |> map (apsnd freeze_term)
  1935       |> map2 (pair o rpair (Local, General) o string_of_int)
  1936               (0 upto length hyp_ts)
  1937     val ((conjs, facts), lam_facts) =
  1938       (conjs, facts)
  1939       |> presimp ? pairself (map (apsnd (apsnd (presimp_prop ctxt type_enc))))
  1940       |> (if lam_trans = no_lamsN then
  1941             rpair []
  1942           else
  1943             op @
  1944             #> preprocess_abstractions_in_terms trans_lams
  1945             #>> chop (length conjs))
  1946     val conjs = conjs |> make_conjecture ctxt format type_enc
  1947     val (fact_names, facts) =
  1948       facts
  1949       |> map_filter (fn (name, (_, t)) =>
  1950                         make_fact ctxt format type_enc true (name, t)
  1951                         |> Option.map (pair name))
  1952       |> List.partition (fn (_, {role, ...}) => role = Definition)
  1953       |>> order_definitions
  1954       |> op @ |> ListPair.unzip
  1955     val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
  1956     val lam_facts =
  1957       lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
  1958     val all_ts = concl_t :: hyp_ts @ fact_ts
  1959     val subs = tfree_classes_of_terms all_ts
  1960     val supers = tvar_classes_of_terms all_ts
  1961     val tycons = type_constrs_of_terms thy all_ts
  1962     val (supers, arity_clauses) =
  1963       if level_of_type_enc type_enc = No_Types then ([], [])
  1964       else make_arity_clauses thy tycons supers
  1965     val class_rel_clauses = make_class_rel_clauses thy subs supers
  1966   in
  1967     (fact_names |> map single, union (op =) subs supers, conjs,
  1968      facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
  1969   end
  1970 
  1971 val type_guard = `(make_fixed_const NONE) type_guard_name
  1972 
  1973 fun type_guard_iterm type_enc T tm =
  1974   IApp (IConst (type_guard, T --> @{typ bool}, [T])
  1975         |> mangle_type_args_in_iterm type_enc, tm)
  1976 
  1977 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
  1978   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
  1979     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
  1980   | is_var_positively_naked_in_term _ _ _ _ = true
  1981 
  1982 fun is_var_ghost_type_arg_in_term thy polym_constrs name pos tm accum =
  1983   is_var_positively_naked_in_term name pos tm accum orelse
  1984   let
  1985     val var = ATerm (name, [])
  1986     fun is_nasty_in_term (ATerm (_, [])) = false
  1987       | is_nasty_in_term (ATerm ((s, _), tms)) =
  1988         let
  1989           val ary = length tms
  1990           val polym_constr = member (op =) polym_constrs s
  1991           val ghosts = ghost_type_args thy s ary
  1992         in
  1993           exists (fn (j, tm) =>
  1994                      if polym_constr then
  1995                        member (op =) ghosts j andalso
  1996                        (tm = var orelse is_nasty_in_term tm)
  1997                      else
  1998                        tm = var andalso member (op =) ghosts j)
  1999                  (0 upto ary - 1 ~~ tms)
  2000           orelse (not polym_constr andalso exists is_nasty_in_term tms)
  2001         end
  2002       | is_nasty_in_term _ = true
  2003   in is_nasty_in_term tm end
  2004 
  2005 fun should_guard_var_in_formula thy polym_constrs level pos phi (SOME true)
  2006                                 name =
  2007     (case granularity_of_type_level level of
  2008        All_Vars => true
  2009      | Positively_Naked_Vars =>
  2010        formula_fold pos (is_var_positively_naked_in_term name) phi false
  2011      | Ghost_Type_Arg_Vars =>
  2012        formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name) phi
  2013                     false)
  2014   | should_guard_var_in_formula _ _ _ _ _ _ _ = true
  2015 
  2016 fun always_guard_var_in_formula _ _ _ _ _ _ _ = true
  2017 
  2018 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
  2019   | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
  2020     granularity_of_type_level level <> All_Vars andalso
  2021     should_encode_type ctxt mono level T
  2022   | should_generate_tag_bound_decl _ _ _ _ _ = false
  2023 
  2024 fun mk_aterm type_enc name T_args args =
  2025   ATerm (name, map_filter (ho_term_for_type_arg type_enc) T_args @ args)
  2026 
  2027 fun do_bound_type ctxt mono type_enc =
  2028   case type_enc of
  2029     Native (_, _, level) =>
  2030     fused_type ctxt mono level 0 #> ho_type_from_typ type_enc false 0 #> SOME
  2031   | _ => K NONE
  2032 
  2033 fun tag_with_type ctxt mono type_enc pos T tm =
  2034   IConst (type_tag, T --> T, [T])
  2035   |> mangle_type_args_in_iterm type_enc
  2036   |> ho_term_from_iterm ctxt mono type_enc pos
  2037   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
  2038        | _ => raise Fail "unexpected lambda-abstraction")
  2039 and ho_term_from_iterm ctxt mono type_enc pos =
  2040   let
  2041     fun term site u =
  2042       let
  2043         val (head, args) = strip_iterm_comb u
  2044         val pos =
  2045           case site of
  2046             Top_Level pos => pos
  2047           | Eq_Arg pos => pos
  2048           | _ => NONE
  2049         val t =
  2050           case head of
  2051             IConst (name as (s, _), _, T_args) =>
  2052             let
  2053               val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
  2054             in map (term arg_site) args |> mk_aterm type_enc name T_args end
  2055           | IVar (name, _) =>
  2056             map (term Elsewhere) args |> mk_aterm type_enc name []
  2057           | IAbs ((name, T), tm) =>
  2058             if is_type_enc_higher_order type_enc then
  2059               AAbs (((name, ho_type_from_typ type_enc true 0 T),
  2060                      term Elsewhere tm), map (term Elsewhere) args)
  2061             else
  2062               raise Fail "unexpected lambda-abstraction"
  2063           | IApp _ => raise Fail "impossible \"IApp\""
  2064         val T = ityp_of u
  2065       in
  2066         if should_tag_with_type ctxt mono type_enc site u T then
  2067           tag_with_type ctxt mono type_enc pos T t
  2068         else
  2069           t
  2070       end
  2071   in term (Top_Level pos) end
  2072 and formula_from_iformula ctxt polym_constrs mono type_enc should_guard_var =
  2073   let
  2074     val thy = Proof_Context.theory_of ctxt
  2075     val level = level_of_type_enc type_enc
  2076     val do_term = ho_term_from_iterm ctxt mono type_enc
  2077     fun do_out_of_bound_type pos phi universal (name, T) =
  2078       if should_guard_type ctxt mono type_enc
  2079              (fn () => should_guard_var thy polym_constrs level pos phi
  2080                                         universal name) T then
  2081         IVar (name, T)
  2082         |> type_guard_iterm type_enc T
  2083         |> do_term pos |> AAtom |> SOME
  2084       else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
  2085         let
  2086           val var = ATerm (name, [])
  2087           val tagged_var = tag_with_type ctxt mono type_enc pos T var
  2088         in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
  2089       else
  2090         NONE
  2091     fun do_formula pos (AQuant (q, xs, phi)) =
  2092         let
  2093           val phi = phi |> do_formula pos
  2094           val universal = Option.map (q = AExists ? not) pos
  2095           val do_bound_type = do_bound_type ctxt mono type_enc
  2096         in
  2097           AQuant (q, xs |> map (apsnd (fn NONE => NONE
  2098                                         | SOME T => do_bound_type T)),
  2099                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
  2100                       (map_filter
  2101                            (fn (_, NONE) => NONE
  2102                              | (s, SOME T) =>
  2103                                do_out_of_bound_type pos phi universal (s, T))
  2104                            xs)
  2105                       phi)
  2106         end
  2107       | do_formula pos (AConn conn) = aconn_map pos do_formula conn
  2108       | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
  2109   in do_formula end
  2110 
  2111 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
  2112    of monomorphization). The TPTP explicitly forbids name clashes, and some of
  2113    the remote provers might care. *)
  2114 fun formula_line_for_fact ctxt polym_constrs prefix encode freshen pos
  2115         mono type_enc rank (j, {name, stature, role, iformula, atomic_types}) =
  2116   (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role,
  2117    iformula
  2118    |> formula_from_iformula ctxt polym_constrs mono type_enc
  2119           should_guard_var_in_formula (if pos then SOME true else NONE)
  2120    |> close_formula_universally
  2121    |> bound_tvars type_enc true atomic_types,
  2122    NONE,
  2123    let val rank = rank j in
  2124      case snd stature of
  2125        Intro => isabelle_info introN rank
  2126      | Inductive => isabelle_info inductiveN rank
  2127      | Elim => isabelle_info elimN rank
  2128      | Simp => isabelle_info simpN rank
  2129      | Def => isabelle_info defN rank
  2130      | _ => isabelle_info "" rank
  2131    end)
  2132   |> Formula
  2133 
  2134 fun formula_line_for_class_rel_clause type_enc
  2135         ({name, subclass, superclass, ...} : class_rel_clause) =
  2136   let val ty_arg = ATerm (tvar_a_name, []) in
  2137     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
  2138              AConn (AImplies,
  2139                     [type_class_formula type_enc subclass ty_arg,
  2140                      type_class_formula type_enc superclass ty_arg])
  2141              |> mk_aquant AForall
  2142                           [(tvar_a_name, atype_of_type_vars type_enc)],
  2143              NONE, isabelle_info inductiveN helper_rank)
  2144   end
  2145 
  2146 fun formula_from_arity_atom type_enc (class, t, args) =
  2147   ATerm (t, map (fn arg => ATerm (arg, [])) args)
  2148   |> type_class_formula type_enc class
  2149 
  2150 fun formula_line_for_arity_clause type_enc
  2151         ({name, prem_atoms, concl_atom} : arity_clause) =
  2152   Formula (arity_clause_prefix ^ name, Axiom,
  2153            mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
  2154                     (formula_from_arity_atom type_enc concl_atom)
  2155            |> mk_aquant AForall
  2156                   (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
  2157            NONE, isabelle_info inductiveN helper_rank)
  2158 
  2159 fun formula_line_for_conjecture ctxt polym_constrs mono type_enc
  2160         ({name, role, iformula, atomic_types, ...} : translated_formula) =
  2161   Formula (conjecture_prefix ^ name, role,
  2162            iformula
  2163            |> formula_from_iformula ctxt polym_constrs mono type_enc
  2164                   should_guard_var_in_formula (SOME false)
  2165            |> close_formula_universally
  2166            |> bound_tvars type_enc true atomic_types, NONE, [])
  2167 
  2168 fun type_enc_needs_free_types (Native (_, Polymorphic, _)) = true
  2169   | type_enc_needs_free_types (Native _) = false
  2170   | type_enc_needs_free_types _ = true
  2171 
  2172 fun formula_line_for_free_type j phi =
  2173   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
  2174 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
  2175   if type_enc_needs_free_types type_enc then
  2176     let
  2177       val phis =
  2178         fold (union (op =)) (map #atomic_types facts) []
  2179         |> formulas_for_types type_enc add_sorts_on_tfree
  2180     in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
  2181   else
  2182     []
  2183 
  2184 (** Symbol declarations **)
  2185 
  2186 fun decl_line_for_class order s =
  2187   let val name as (s, _) = `make_type_class s in
  2188     Decl (sym_decl_prefix ^ s, name,
  2189           if order = First_Order then
  2190             ATyAbs ([tvar_a_name],
  2191                     if avoid_first_order_ghost_type_vars then
  2192                       AFun (a_itself_atype, bool_atype)
  2193                     else
  2194                       bool_atype)
  2195           else
  2196             AFun (atype_of_types, bool_atype))
  2197   end
  2198 
  2199 fun decl_lines_for_classes type_enc classes =
  2200   case type_enc of
  2201     Native (order, Polymorphic, _) => map (decl_line_for_class order) classes
  2202   | _ => []
  2203 
  2204 fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
  2205   let
  2206     fun add_iterm_syms tm =
  2207       let val (head, args) = strip_iterm_comb tm in
  2208         (case head of
  2209            IConst ((s, s'), T, T_args) =>
  2210            let
  2211              val (pred_sym, in_conj) =
  2212                case Symtab.lookup sym_tab s of
  2213                  SOME ({pred_sym, in_conj, ...} : sym_info) =>
  2214                  (pred_sym, in_conj)
  2215                | NONE => (false, false)
  2216              val decl_sym =
  2217                (case type_enc of
  2218                   Guards _ => not pred_sym
  2219                 | _ => true) andalso
  2220                is_tptp_user_symbol s
  2221            in
  2222              if decl_sym then
  2223                Symtab.map_default (s, [])
  2224                    (insert_type thy #3 (s', T_args, T, pred_sym, length args,
  2225                                         in_conj))
  2226              else
  2227                I
  2228            end
  2229          | IAbs (_, tm) => add_iterm_syms tm
  2230          | _ => I)
  2231         #> fold add_iterm_syms args
  2232       end
  2233     val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
  2234     fun add_formula_var_types (AQuant (_, xs, phi)) =
  2235         fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
  2236         #> add_formula_var_types phi
  2237       | add_formula_var_types (AConn (_, phis)) =
  2238         fold add_formula_var_types phis
  2239       | add_formula_var_types _ = I
  2240     fun var_types () =
  2241       if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
  2242       else fold (fact_lift add_formula_var_types) (conjs @ facts) []
  2243     fun add_undefined_const T =
  2244       let
  2245         val (s, s') =
  2246           `(make_fixed_const NONE) @{const_name undefined}
  2247           |> (case type_arg_policy [] type_enc @{const_name undefined} of
  2248                 Mangled_Type_Args => mangled_const_name type_enc [T]
  2249               | _ => I)
  2250       in
  2251         Symtab.map_default (s, [])
  2252                            (insert_type thy #3 (s', [T], T, false, 0, false))
  2253       end
  2254     fun add_TYPE_const () =
  2255       let val (s, s') = TYPE_name in
  2256         Symtab.map_default (s, [])
  2257             (insert_type thy #3
  2258                          (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
  2259       end
  2260   in
  2261     Symtab.empty
  2262     |> is_type_enc_fairly_sound type_enc
  2263        ? (fold (fold add_fact_syms) [conjs, facts]
  2264           #> fold add_iterm_syms extra_tms
  2265           #> (case type_enc of
  2266                 Native (First_Order, Polymorphic, _) =>
  2267                 if avoid_first_order_ghost_type_vars then add_TYPE_const ()
  2268                 else I
  2269               | Native _ => I
  2270               | _ => fold add_undefined_const (var_types ())))
  2271   end
  2272 
  2273 (* We add "bool" in case the helper "True_or_False" is included later. *)
  2274 fun default_mono level =
  2275   {maybe_finite_Ts = [@{typ bool}],
  2276    surely_finite_Ts = [@{typ bool}],
  2277    maybe_infinite_Ts = known_infinite_types,
  2278    surely_infinite_Ts =
  2279      case level of
  2280        Noninf_Nonmono_Types (Strict, _) => []
  2281      | _ => known_infinite_types,
  2282    maybe_nonmono_Ts = [@{typ bool}]}
  2283 
  2284 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
  2285    out with monotonicity" paper presented at CADE 2011. *)
  2286 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
  2287   | add_iterm_mononotonicity_info ctxt level _
  2288         (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
  2289         (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
  2290                   surely_infinite_Ts, maybe_nonmono_Ts}) =
  2291     let val thy = Proof_Context.theory_of ctxt in
  2292       if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
  2293         case level of
  2294           Noninf_Nonmono_Types (strictness, _) =>
  2295           if exists (type_instance thy T) surely_infinite_Ts orelse
  2296              member (type_equiv thy) maybe_finite_Ts T then
  2297             mono
  2298           else if is_type_kind_of_surely_infinite ctxt strictness
  2299                                                   surely_infinite_Ts T then
  2300             {maybe_finite_Ts = maybe_finite_Ts,
  2301              surely_finite_Ts = surely_finite_Ts,
  2302              maybe_infinite_Ts = maybe_infinite_Ts,
  2303              surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
  2304              maybe_nonmono_Ts = maybe_nonmono_Ts}
  2305           else
  2306             {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
  2307              surely_finite_Ts = surely_finite_Ts,
  2308              maybe_infinite_Ts = maybe_infinite_Ts,
  2309              surely_infinite_Ts = surely_infinite_Ts,
  2310              maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
  2311         | Fin_Nonmono_Types _ =>
  2312           if exists (type_instance thy T) surely_finite_Ts orelse
  2313              member (type_equiv thy) maybe_infinite_Ts T then
  2314             mono
  2315           else if is_type_surely_finite ctxt T then
  2316             {maybe_finite_Ts = maybe_finite_Ts,
  2317              surely_finite_Ts = surely_finite_Ts |> insert_type thy I T,
  2318              maybe_infinite_Ts = maybe_infinite_Ts,
  2319              surely_infinite_Ts = surely_infinite_Ts,
  2320              maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
  2321           else
  2322             {maybe_finite_Ts = maybe_finite_Ts,
  2323              surely_finite_Ts = surely_finite_Ts,
  2324              maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv thy) T,
  2325              surely_infinite_Ts = surely_infinite_Ts,
  2326              maybe_nonmono_Ts = maybe_nonmono_Ts}
  2327         | _ => mono
  2328       else
  2329         mono
  2330     end
  2331   | add_iterm_mononotonicity_info _ _ _ _ mono = mono
  2332 fun add_fact_mononotonicity_info ctxt level
  2333         ({role, iformula, ...} : translated_formula) =
  2334   formula_fold (SOME (role <> Conjecture))
  2335                (add_iterm_mononotonicity_info ctxt level) iformula
  2336 fun mononotonicity_info_for_facts ctxt type_enc facts =
  2337   let val level = level_of_type_enc type_enc in
  2338     default_mono level
  2339     |> is_type_level_monotonicity_based level
  2340        ? fold (add_fact_mononotonicity_info ctxt level) facts
  2341   end
  2342 
  2343 fun add_iformula_monotonic_types ctxt mono type_enc =
  2344   let
  2345     val thy = Proof_Context.theory_of ctxt
  2346     val level = level_of_type_enc type_enc
  2347     val should_encode = should_encode_type ctxt mono level
  2348     fun add_type T = not (should_encode T) ? insert_type thy I T
  2349     fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
  2350       | add_args _ = I
  2351     and add_term tm = add_type (ityp_of tm) #> add_args tm
  2352   in formula_fold NONE (K add_term) end
  2353 fun add_fact_monotonic_types ctxt mono type_enc =
  2354   add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
  2355 fun monotonic_types_for_facts ctxt mono type_enc facts =
  2356   let val level = level_of_type_enc type_enc in
  2357     [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
  2358            is_type_level_monotonicity_based level andalso
  2359            granularity_of_type_level level <> Ghost_Type_Arg_Vars)
  2360           ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
  2361   end
  2362 
  2363 fun formula_line_for_guards_mono_type ctxt mono type_enc T =
  2364   Formula (guards_sym_formula_prefix ^
  2365            ascii_of (mangled_type type_enc T),
  2366            Axiom,
  2367            IConst (`make_bound_var "X", T, [])
  2368            |> type_guard_iterm type_enc T
  2369            |> AAtom
  2370            |> formula_from_iformula ctxt [] mono type_enc
  2371                                     always_guard_var_in_formula (SOME true)
  2372            |> close_formula_universally
  2373            |> bound_tvars type_enc true (atomic_types_of T),
  2374            NONE, isabelle_info inductiveN helper_rank)
  2375 
  2376 fun formula_line_for_tags_mono_type ctxt mono type_enc T =
  2377   let val x_var = ATerm (`make_bound_var "X", []) in
  2378     Formula (tags_sym_formula_prefix ^
  2379              ascii_of (mangled_type type_enc T),
  2380              Axiom,
  2381              eq_formula type_enc (atomic_types_of T) [] false
  2382                   (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
  2383              NONE, isabelle_info defN helper_rank)
  2384   end
  2385 
  2386 fun problem_lines_for_mono_types ctxt mono type_enc Ts =
  2387   case type_enc of
  2388     Native _ => []
  2389   | Guards _ => map (formula_line_for_guards_mono_type ctxt mono type_enc) Ts
  2390   | Tags _ => map (formula_line_for_tags_mono_type ctxt mono type_enc) Ts
  2391 
  2392 fun decl_line_for_sym ctxt mono type_enc s
  2393                       (s', T_args, T, pred_sym, ary, _) =
  2394   let
  2395     val thy = Proof_Context.theory_of ctxt
  2396     val (T, T_args) =
  2397       if null T_args then
  2398         (T, [])
  2399       else case unprefix_and_unascii const_prefix s of
  2400         SOME s' =>
  2401         let
  2402           val s' = s' |> invert_const
  2403           val T = s' |> robust_const_type thy
  2404         in (T, robust_const_typargs thy (s', T)) end
  2405       | NONE => raise Fail "unexpected type arguments"
  2406   in
  2407     Decl (sym_decl_prefix ^ s, (s, s'),
  2408           T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
  2409             |> ho_type_from_typ type_enc pred_sym ary
  2410             |> not (null T_args)
  2411                ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
  2412   end
  2413 
  2414 fun honor_conj_sym_role in_conj =
  2415   if in_conj then (Hypothesis, I) else (Axiom, I)
  2416 
  2417 fun formula_line_for_guards_sym_decl ctxt mono type_enc n s j
  2418                                      (s', T_args, T, _, ary, in_conj) =
  2419   let
  2420     val thy = Proof_Context.theory_of ctxt
  2421     val (role, maybe_negate) = honor_conj_sym_role in_conj
  2422     val (arg_Ts, res_T) = chop_fun ary T
  2423     val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
  2424     val bounds =
  2425       bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
  2426     val bound_Ts =
  2427       if exists (curry (op =) dummyT) T_args then
  2428         case level_of_type_enc type_enc of
  2429           All_Types => map SOME arg_Ts
  2430         | level =>
  2431           if granularity_of_type_level level = Ghost_Type_Arg_Vars then
  2432             let val ghosts = ghost_type_args thy s ary in
  2433               map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
  2434                    (0 upto ary - 1) arg_Ts
  2435             end
  2436           else
  2437             replicate ary NONE
  2438       else
  2439         replicate ary NONE
  2440   in
  2441     Formula (guards_sym_formula_prefix ^ s ^
  2442              (if n > 1 then "_" ^ string_of_int j else ""), role,
  2443              IConst ((s, s'), T, T_args)
  2444              |> fold (curry (IApp o swap)) bounds
  2445              |> type_guard_iterm type_enc res_T
  2446              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
  2447              |> formula_from_iformula ctxt [] mono type_enc
  2448                                       always_guard_var_in_formula (SOME true)
  2449              |> close_formula_universally
  2450              |> bound_tvars type_enc (n > 1) (atomic_types_of T)
  2451              |> maybe_negate,
  2452              NONE, isabelle_info inductiveN helper_rank)
  2453   end
  2454 
  2455 fun formula_lines_for_tags_sym_decl ctxt mono type_enc n s
  2456         (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  2457   let
  2458     val thy = Proof_Context.theory_of ctxt
  2459     val level = level_of_type_enc type_enc
  2460     val grain = granularity_of_type_level level
  2461     val ident_base =
  2462       tags_sym_formula_prefix ^ s ^
  2463       (if n > 1 then "_" ^ string_of_int j else "")
  2464     val (role, maybe_negate) = honor_conj_sym_role in_conj
  2465     val (arg_Ts, res_T) = chop_fun ary T
  2466     val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
  2467     val bounds = bound_names |> map (fn name => ATerm (name, []))
  2468     val cst = mk_aterm type_enc (s, s') T_args
  2469     val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
  2470     val should_encode = should_encode_type ctxt mono level
  2471     val tag_with = tag_with_type ctxt mono type_enc NONE
  2472     val add_formula_for_res =
  2473       if should_encode res_T then
  2474         let
  2475           val tagged_bounds =
  2476             if grain = Ghost_Type_Arg_Vars then
  2477               let val ghosts = ghost_type_args thy s ary in
  2478                 map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
  2479                      (0 upto ary - 1 ~~ arg_Ts) bounds
  2480               end
  2481             else
  2482               bounds
  2483         in
  2484           cons (Formula (ident_base ^ "_res", role,
  2485                          eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
  2486                          NONE, isabelle_info defN helper_rank))
  2487         end
  2488       else
  2489         I
  2490   in [] |> not pred_sym ? add_formula_for_res end
  2491 
  2492 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
  2493 
  2494 fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
  2495     let
  2496       val T = result_type_of_decl decl
  2497               |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
  2498     in
  2499       if forall (type_generalization thy T o result_type_of_decl) decls' then
  2500         [decl]
  2501       else
  2502         decls
  2503     end
  2504   | rationalize_decls _ decls = decls
  2505 
  2506 fun problem_lines_for_sym_decls ctxt mono type_enc (s, decls) =
  2507   case type_enc of
  2508     Native _ => [decl_line_for_sym ctxt mono type_enc s (hd decls)]
  2509   | Guards (_, level) =>
  2510     let
  2511       val thy = Proof_Context.theory_of ctxt
  2512       val decls = decls |> rationalize_decls thy
  2513       val n = length decls
  2514       val decls =
  2515         decls |> filter (should_encode_type ctxt mono level
  2516                          o result_type_of_decl)
  2517     in
  2518       (0 upto length decls - 1, decls)
  2519       |-> map2 (formula_line_for_guards_sym_decl ctxt mono type_enc n s)
  2520     end
  2521   | Tags (_, level) =>
  2522     if granularity_of_type_level level = All_Vars then
  2523       []
  2524     else
  2525       let val n = length decls in
  2526         (0 upto n - 1 ~~ decls)
  2527         |> maps (formula_lines_for_tags_sym_decl ctxt mono type_enc n s)
  2528       end
  2529 
  2530 fun problem_lines_for_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
  2531   let
  2532     val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
  2533     val mono_lines = problem_lines_for_mono_types ctxt mono type_enc mono_Ts
  2534     val decl_lines =
  2535       fold_rev (append o problem_lines_for_sym_decls ctxt mono type_enc) syms []
  2536   in mono_lines @ decl_lines end
  2537 
  2538 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
  2539 
  2540 fun do_uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc sym_tab0
  2541                                      sym_tab base_s0 types in_conj =
  2542   let
  2543     fun do_alias ary =
  2544       let
  2545         val thy = Proof_Context.theory_of ctxt
  2546         val (role, maybe_negate) = honor_conj_sym_role in_conj
  2547         val base_name = base_s0 |> `(make_fixed_const (SOME type_enc))
  2548         val T = case types of [T] => T | _ => robust_const_type thy base_s0
  2549         val T_args = robust_const_typargs thy (base_s0, T)
  2550         val (base_name as (base_s, _), T_args) =
  2551           mangle_type_args_in_const type_enc base_name T_args
  2552         val base_ary = min_ary_of sym_tab0 base_s
  2553         fun do_const name = IConst (name, T, T_args)
  2554         val filter_ty_args =
  2555           filter_type_args_in_iterm thy monom_constrs type_enc
  2556         val ho_term_of = ho_term_from_iterm ctxt mono type_enc (SOME true)
  2557         val name1 as (s1, _) =
  2558           base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
  2559         val name2 as (s2, _) = base_name |> aliased_uncurried ary
  2560         val (arg_Ts, _) = chop_fun ary T
  2561         val bound_names =
  2562           1 upto ary |> map (`I o make_bound_var o string_of_int)
  2563         val bounds = bound_names ~~ arg_Ts
  2564         val (first_bounds, last_bound) =
  2565           bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last
  2566         val tm1 =
  2567           mk_app_op type_enc (list_app (do_const name1) first_bounds) last_bound
  2568           |> filter_ty_args
  2569         val tm2 =
  2570           list_app (do_const name2) (first_bounds @ [last_bound])
  2571           |> filter_ty_args
  2572         val do_bound_type = do_bound_type ctxt mono type_enc
  2573         val eq =
  2574           eq_formula type_enc (atomic_types_of T)
  2575                      (map (apsnd do_bound_type) bounds) false
  2576                      (ho_term_of tm1) (ho_term_of tm2)
  2577       in
  2578         ([tm1, tm2],
  2579          [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate,
  2580                    NONE, isabelle_info defN helper_rank)])
  2581         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
  2582             else pair_append (do_alias (ary - 1)))
  2583       end
  2584   in do_alias end
  2585 fun uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc sym_tab0
  2586         sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) =
  2587   case unprefix_and_unascii const_prefix s of
  2588     SOME mangled_s =>
  2589     if String.isSubstring uncurried_alias_sep mangled_s then
  2590       let
  2591         val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
  2592       in
  2593         do_uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc
  2594             sym_tab0 sym_tab base_s0 types in_conj min_ary
  2595       end
  2596     else
  2597       ([], [])
  2598   | NONE => ([], [])
  2599 fun uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc
  2600                                         uncurried_aliases sym_tab0 sym_tab =
  2601   ([], [])
  2602   |> uncurried_aliases
  2603      ? Symtab.fold_rev
  2604            (pair_append
  2605             o uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc
  2606                                             sym_tab0 sym_tab) sym_tab
  2607 
  2608 val implicit_declsN = "Should-be-implicit typings"
  2609 val explicit_declsN = "Explicit typings"
  2610 val uncurried_alias_eqsN = "Uncurried aliases"
  2611 val factsN = "Relevant facts"
  2612 val class_relsN = "Class relationships"
  2613 val aritiesN = "Arities"
  2614 val helpersN = "Helper facts"
  2615 val conjsN = "Conjectures"
  2616 val free_typesN = "Type variables"
  2617 
  2618 (* TFF allows implicit declarations of types, function symbols, and predicate
  2619    symbols (with "$i" as the type of individuals), but some provers (e.g.,
  2620    SNARK) require explicit declarations. The situation is similar for THF. *)
  2621 
  2622 fun default_type type_enc pred_sym s =
  2623   let
  2624     val ind =
  2625       case type_enc of
  2626         Native _ =>
  2627         if String.isPrefix type_const_prefix s orelse
  2628            String.isPrefix tfree_prefix s then
  2629           atype_of_types
  2630         else
  2631           individual_atype
  2632       | _ => individual_atype
  2633     fun typ 0 = if pred_sym then bool_atype else ind
  2634       | typ ary = AFun (ind, typ (ary - 1))
  2635   in typ end
  2636 
  2637 fun nary_type_constr_type n =
  2638   funpow n (curry AFun atype_of_types) atype_of_types
  2639 
  2640 fun undeclared_syms_in_problem type_enc problem =
  2641   let
  2642     fun do_sym (name as (s, _)) ty =
  2643       if is_tptp_user_symbol s then
  2644         Symtab.default (s, (name, ty))
  2645       else
  2646         I
  2647     fun do_type (AType (name, tys)) =
  2648         do_sym name (fn () => nary_type_constr_type (length tys))
  2649         #> fold do_type tys
  2650       | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
  2651       | do_type (ATyAbs (_, ty)) = do_type ty
  2652     fun do_term pred_sym (ATerm (name as (s, _), tms)) =
  2653         do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
  2654         #> fold (do_term false) tms
  2655       | do_term _ (AAbs (((_, ty), tm), args)) =
  2656         do_type ty #> do_term false tm #> fold (do_term false) args
  2657     fun do_formula (AQuant (_, xs, phi)) =
  2658         fold do_type (map_filter snd xs) #> do_formula phi
  2659       | do_formula (AConn (_, phis)) = fold do_formula phis
  2660       | do_formula (AAtom tm) = do_term true tm
  2661     fun do_problem_line (Decl (_, _, ty)) = do_type ty
  2662       | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
  2663   in
  2664     Symtab.empty
  2665     |> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype)))
  2666             (declared_syms_in_problem problem)
  2667     |> fold (fold do_problem_line o snd) problem
  2668   end
  2669 
  2670 fun declare_undeclared_syms_in_atp_problem type_enc problem =
  2671   let
  2672     val decls =
  2673       Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
  2674                     | (s, (sym, ty)) =>
  2675                       cons (Decl (type_decl_prefix ^ s, sym, ty ())))
  2676                   (undeclared_syms_in_problem type_enc problem) []
  2677   in (implicit_declsN, decls) :: problem end
  2678 
  2679 fun exists_subdtype P =
  2680   let
  2681     fun ex U = P U orelse
  2682       (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false)
  2683   in ex end
  2684 
  2685 fun is_poly_constr (_, Us) =
  2686   exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
  2687 
  2688 fun all_constrs_of_polymorphic_datatypes thy =
  2689   Symtab.fold (snd
  2690                #> #descr
  2691                #> maps (snd #> #3)
  2692                #> (fn cs => exists is_poly_constr cs ? append cs))
  2693               (Datatype.get_all thy) []
  2694   |> List.partition is_poly_constr
  2695   |> pairself (map fst)
  2696 
  2697 val app_op_and_predicator_threshold = 50
  2698 
  2699 fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans
  2700                         uncurried_aliases readable_names preproc hyp_ts concl_t
  2701                         facts =
  2702   let
  2703     val thy = Proof_Context.theory_of ctxt
  2704     val type_enc = type_enc |> adjust_type_enc format
  2705     (* Forcing explicit applications is expensive for polymorphic encodings,
  2706        because it takes only one existential variable ranging over "'a => 'b" to
  2707        ruin everything. Hence we do it only if there are few facts (which is
  2708        normally the case for "metis" and the minimizer). *)
  2709     val app_op_level =
  2710       if mode = Sledgehammer_Aggressive then
  2711         Full_App_Op_And_Predicator
  2712       else if length facts + length hyp_ts
  2713               > app_op_and_predicator_threshold then
  2714         if polymorphism_of_type_enc type_enc = Polymorphic then Min_App_Op
  2715         else Sufficient_App_Op
  2716       else
  2717         Sufficient_App_Op_And_Predicator
  2718     val exporter = (mode = Exporter)
  2719     val aggressive = (mode = Sledgehammer_Aggressive)
  2720     val lam_trans =
  2721       if lam_trans = keep_lamsN andalso
  2722          not (is_type_enc_higher_order type_enc) then
  2723         error ("Lambda translation scheme incompatible with first-order \
  2724                \encoding.")
  2725       else
  2726         lam_trans
  2727     val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
  2728          lifted) =
  2729       translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts
  2730                          concl_t facts
  2731     val (_, sym_tab0) =
  2732       sym_table_for_facts ctxt type_enc app_op_level conjs facts
  2733     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
  2734     val (polym_constrs, monom_constrs) =
  2735       all_constrs_of_polymorphic_datatypes thy
  2736       |>> map (make_fixed_const (SOME type_enc))
  2737     fun firstorderize in_helper =
  2738       firstorderize_fact thy monom_constrs type_enc sym_tab0
  2739           (uncurried_aliases andalso not in_helper) aggressive
  2740     val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
  2741     val (ho_stuff, sym_tab) =
  2742       sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
  2743     val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
  2744       uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc
  2745                                           uncurried_aliases sym_tab0 sym_tab
  2746     val (_, sym_tab) =
  2747       (ho_stuff, sym_tab)
  2748       |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
  2749               uncurried_alias_eq_tms
  2750     val helpers =
  2751       sym_tab |> helper_facts_for_sym_table ctxt format type_enc aggressive
  2752               |> map (firstorderize true)
  2753     val mono_Ts =
  2754       helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
  2755     val class_decl_lines = decl_lines_for_classes type_enc classes
  2756     val sym_decl_lines =
  2757       (conjs, helpers @ facts, uncurried_alias_eq_tms)
  2758       |> sym_decl_table_for_facts thy type_enc sym_tab
  2759       |> problem_lines_for_sym_decl_table ctxt mono type_enc mono_Ts
  2760     val num_facts = length facts
  2761     val fact_lines =
  2762       map (formula_line_for_fact ctxt polym_constrs fact_prefix
  2763                ascii_of (not exporter) (not exporter) mono type_enc
  2764                (rank_of_fact_num num_facts))
  2765           (0 upto num_facts - 1 ~~ facts)
  2766     val helper_lines =
  2767       0 upto length helpers - 1 ~~ helpers
  2768       |> map (formula_line_for_fact ctxt polym_constrs helper_prefix I false
  2769                                     true mono type_enc (K default_rank))
  2770     (* Reordering these might confuse the proof reconstruction code or the SPASS
  2771        FLOTTER hack. *)
  2772     val problem =
  2773       [(explicit_declsN, class_decl_lines @ sym_decl_lines),
  2774        (uncurried_alias_eqsN, uncurried_alias_eq_lines),
  2775        (factsN, fact_lines),
  2776        (class_relsN,
  2777         map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
  2778        (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
  2779        (helpersN, helper_lines),
  2780        (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)),
  2781        (conjsN,
  2782         map (formula_line_for_conjecture ctxt polym_constrs mono type_enc)
  2783                                          conjs)]
  2784     val problem =
  2785       problem
  2786       |> (case format of
  2787             CNF => ensure_cnf_problem
  2788           | CNF_UEQ => filter_cnf_ueq_problem
  2789           | FOF => I
  2790           | TFF (_, TPTP_Implicit) => I
  2791           | THF (_, TPTP_Implicit, _) => I
  2792           | _ => declare_undeclared_syms_in_atp_problem type_enc)
  2793     val (problem, pool) = problem |> nice_atp_problem readable_names format
  2794     fun add_sym_ary (s, {min_ary, ...} : sym_info) =
  2795       min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
  2796   in
  2797     (problem,
  2798      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
  2799      fact_names |> Vector.fromList,
  2800      lifted,
  2801      Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
  2802   end
  2803 
  2804 (* FUDGE *)
  2805 val conj_weight = 0.0
  2806 val hyp_weight = 0.1
  2807 val fact_min_weight = 0.2
  2808 val fact_max_weight = 1.0
  2809 val type_info_default_weight = 0.8
  2810 
  2811 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
  2812 fun atp_problem_selection_weights problem =
  2813   let
  2814     fun add_term_weights weight (ATerm (s, tms)) =
  2815         is_tptp_user_symbol s ? Symtab.default (s, weight)
  2816         #> fold (add_term_weights weight) tms
  2817       | add_term_weights weight (AAbs ((_, tm), args)) =
  2818         add_term_weights weight tm #> fold (add_term_weights weight) args
  2819     fun add_line_weights weight (Formula (_, _, phi, _, _)) =
  2820         formula_fold NONE (K (add_term_weights weight)) phi
  2821       | add_line_weights _ _ = I
  2822     fun add_conjectures_weights [] = I
  2823       | add_conjectures_weights conjs =
  2824         let val (hyps, conj) = split_last conjs in
  2825           add_line_weights conj_weight conj
  2826           #> fold (add_line_weights hyp_weight) hyps
  2827         end
  2828     fun add_facts_weights facts =
  2829       let
  2830         val num_facts = length facts
  2831         fun weight_of j =
  2832           fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
  2833                             / Real.fromInt num_facts
  2834       in
  2835         map weight_of (0 upto num_facts - 1) ~~ facts
  2836         |> fold (uncurry add_line_weights)
  2837       end
  2838     val get = these o AList.lookup (op =) problem
  2839   in
  2840     Symtab.empty
  2841     |> add_conjectures_weights (get free_typesN @ get conjsN)
  2842     |> add_facts_weights (get factsN)
  2843     |> fold (fold (add_line_weights type_info_default_weight) o get)
  2844             [explicit_declsN, class_relsN, aritiesN]
  2845     |> Symtab.dest
  2846     |> sort (prod_ord Real.compare string_ord o pairself swap)
  2847   end
  2848 
  2849 (* Ugly hack: may make innocent victims (collateral damage) *)
  2850 fun may_be_app s args = String.isPrefix app_op_name s andalso length args = 2
  2851 fun may_be_predicator s =
  2852   member (op =) [predicator_name, prefixed_predicator_name] s
  2853 
  2854 fun strip_predicator (tm as ATerm (s, [tm'])) =
  2855     if may_be_predicator s then tm' else tm
  2856   | strip_predicator tm = tm
  2857 
  2858 fun make_head_roll (ATerm (s, tms)) =
  2859     if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms)
  2860     else (s, tms)
  2861   | make_head_roll _ = ("", [])
  2862 
  2863 fun strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
  2864   | strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis
  2865   | strip_up_to_predicator (AAtom tm) = [strip_predicator tm]
  2866 
  2867 fun strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
  2868   | strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) =
  2869     strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1)
  2870   | strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi))
  2871 
  2872 fun strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
  2873   | strip_iff_etc (AConn (AIff, [phi1, phi2])) =
  2874     pairself strip_up_to_predicator (phi1, phi2)
  2875   | strip_iff_etc _ = ([], [])
  2876 
  2877 val max_term_order_weight = 2147483647
  2878 
  2879 fun atp_problem_term_order_info problem =
  2880   let
  2881     fun add_edge s s' =
  2882       Graph.default_node (s, ())
  2883       #> Graph.default_node (s', ())
  2884       #> Graph.add_edge_acyclic (s, s')
  2885     fun add_term_deps head (ATerm (s, args)) =
  2886         if is_tptp_user_symbol head then
  2887           (if is_tptp_user_symbol s then perhaps (try (add_edge s head)) else I)
  2888           #> fold (add_term_deps head) args
  2889         else
  2890           I
  2891       | add_term_deps head (AAbs ((_, tm), args)) =
  2892         add_term_deps head tm #> fold (add_term_deps head) args
  2893     fun add_intro_deps pred (Formula (_, role, phi, _, info)) =
  2894         if pred (role, info) then
  2895           let val (hyps, concl) = strip_ahorn_etc phi in
  2896             case make_head_roll concl of
  2897               (head, args as _ :: _) => fold (add_term_deps head) (hyps @ args)
  2898             | _ => I
  2899           end
  2900         else
  2901           I
  2902       | add_intro_deps _ _ = I
  2903     fun add_atom_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) =
  2904         if is_tptp_equal s then
  2905           case make_head_roll lhs of
  2906             (head, args as _ :: _) => fold (add_term_deps head) (rhs :: args)
  2907           | _ => I
  2908         else
  2909           I
  2910       | add_atom_eq_deps _ _ = I
  2911     fun add_eq_deps pred (Formula (_, role, phi, _, info)) =
  2912         if pred (role, info) then
  2913           case strip_iff_etc phi of
  2914             ([lhs], rhs) =>
  2915             (case make_head_roll lhs of
  2916                (head, args as _ :: _) => fold (add_term_deps head) (rhs @ args)
  2917              | _ => I)
  2918           | _ => formula_fold (SOME (role <> Conjecture)) add_atom_eq_deps phi
  2919         else
  2920           I
  2921       | add_eq_deps _ _ = I
  2922     fun has_status status (_, info) = extract_isabelle_status info = SOME status
  2923     fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
  2924     val graph =
  2925       Graph.empty
  2926       |> fold (fold (add_eq_deps (has_status defN)) o snd) problem
  2927       |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem
  2928       |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem
  2929       |> fold (fold (add_intro_deps (has_status introN)) o snd) problem
  2930     fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
  2931     fun add_weights _ [] = I
  2932       | add_weights weight syms =
  2933         fold (AList.update (op =) o rpair weight) syms
  2934         #> add_weights (next_weight weight)
  2935                (fold (union (op =) o Graph.immediate_succs graph) syms [])
  2936   in
  2937     (* Sorting is not just for aesthetics: It specifies the precedence order
  2938        for the term ordering (KBO or LPO), from smaller to larger values. *)
  2939     [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o pairself snd)
  2940   end
  2941 
  2942 end;