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