src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
author blanchet
Fri May 27 10:30:07 2011 +0200 (2011-05-27)
changeset 42998 1c80902d0456
parent 42994 fe291ab75eb5
child 43000 bd424c3dde46
permissions -rw-r--r--
fully support all type system encodings in typed formats (TFF, THF)
     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 SLEDGEHAMMER_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   type locality = Sledgehammer_Filter.locality
    16 
    17   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    18   datatype type_level =
    19     All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
    20   datatype type_heaviness = Heavy | Light
    21 
    22   datatype type_system =
    23     Simple_Types of type_level |
    24     Preds of polymorphism * type_level * type_heaviness |
    25     Tags of polymorphism * type_level * type_heaviness
    26 
    27   type translated_formula
    28 
    29   val readable_names : bool Config.T
    30   val fact_prefix : string
    31   val conjecture_prefix : string
    32   val helper_prefix : string
    33   val typed_helper_suffix : string
    34   val predicator_name : string
    35   val app_op_name : string
    36   val type_pred_name : string
    37   val simple_type_prefix : string
    38   val type_sys_from_string : string -> type_system
    39   val polymorphism_of_type_sys : type_system -> polymorphism
    40   val level_of_type_sys : type_system -> type_level
    41   val is_type_sys_virtually_sound : type_system -> bool
    42   val is_type_sys_fairly_sound : type_system -> bool
    43   val unmangled_const : string -> string * string fo_term list
    44   val translate_atp_fact :
    45     Proof.context -> format -> type_system -> bool -> (string * locality) * thm
    46     -> translated_formula option * ((string * locality) * thm)
    47   val prepare_atp_problem :
    48     Proof.context -> format -> formula_kind -> formula_kind -> type_system
    49     -> bool -> term list -> term
    50     -> (translated_formula option * ((string * 'a) * thm)) list
    51     -> string problem * string Symtab.table * int * int
    52        * (string * 'a) list vector * int list * int Symtab.table
    53   val atp_problem_weights : string problem -> (string * real) list
    54 end;
    55 
    56 structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
    57 struct
    58 
    59 open ATP_Problem
    60 open Metis_Translate
    61 open Sledgehammer_Util
    62 open Sledgehammer_Filter
    63 
    64 (* experimental *)
    65 val generate_useful_info = false
    66 
    67 fun useful_isabelle_info s =
    68   if generate_useful_info then
    69     SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
    70   else
    71     NONE
    72 
    73 val intro_info = useful_isabelle_info "intro"
    74 val elim_info = useful_isabelle_info "elim"
    75 val simp_info = useful_isabelle_info "simp"
    76 
    77 (* Readable names are often much shorter, especially if types are mangled in
    78    names. Also, the logic for generating legal SNARK sort names is only
    79    implemented for readable names. Finally, readable names are, well, more
    80    readable. For these reason, they are enabled by default. *)
    81 val readable_names =
    82   Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
    83 
    84 val type_decl_prefix = "ty_"
    85 val sym_decl_prefix = "sy_"
    86 val sym_formula_prefix = "sym_"
    87 val fact_prefix = "fact_"
    88 val conjecture_prefix = "conj_"
    89 val helper_prefix = "help_"
    90 val class_rel_clause_prefix = "crel_";
    91 val arity_clause_prefix = "arity_"
    92 val tfree_prefix = "tfree_"
    93 
    94 val typed_helper_suffix = "_T"
    95 val untyped_helper_suffix = "_U"
    96 
    97 val predicator_name = "hBOOL"
    98 val app_op_name = "hAPP"
    99 val type_pred_name = "is"
   100 val simple_type_prefix = "ty_"
   101 
   102 fun make_simple_type s =
   103   if s = tptp_bool_type orelse s = tptp_fun_type orelse
   104      s = tptp_individual_type then
   105     s
   106   else
   107     simple_type_prefix ^ ascii_of s
   108 
   109 (* Freshness almost guaranteed! *)
   110 val sledgehammer_weak_prefix = "Sledgehammer:"
   111 
   112 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
   113 datatype type_level =
   114   All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
   115 datatype type_heaviness = Heavy | Light
   116 
   117 datatype type_system =
   118   Simple_Types of type_level |
   119   Preds of polymorphism * type_level * type_heaviness |
   120   Tags of polymorphism * type_level * type_heaviness
   121 
   122 fun try_unsuffixes ss s =
   123   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
   124 
   125 fun type_sys_from_string s =
   126   (case try (unprefix "poly_") s of
   127      SOME s => (SOME Polymorphic, s)
   128    | NONE =>
   129      case try (unprefix "mono_") s of
   130        SOME s => (SOME Monomorphic, s)
   131      | NONE =>
   132        case try (unprefix "mangled_") s of
   133          SOME s => (SOME Mangled_Monomorphic, s)
   134        | NONE => (NONE, s))
   135   ||> (fn s =>
   136           (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
   137           case try_unsuffixes ["?", "_query"] s of
   138             SOME s => (Nonmonotonic_Types, s)
   139           | NONE =>
   140             case try_unsuffixes ["!", "_bang"] s of
   141               SOME s => (Finite_Types, s)
   142             | NONE => (All_Types, s))
   143   ||> apsnd (fn s =>
   144                 case try (unsuffix "_heavy") s of
   145                   SOME s => (Heavy, s)
   146                 | NONE => (Light, s))
   147   |> (fn (poly, (level, (heaviness, core))) =>
   148          case (core, (poly, level, heaviness)) of
   149            ("simple", (NONE, _, Light)) => Simple_Types level
   150          | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
   151          | ("tags", (SOME Polymorphic, All_Types, _)) =>
   152            Tags (Polymorphic, All_Types, heaviness)
   153          | ("tags", (SOME Polymorphic, _, _)) =>
   154            (* The actual light encoding is very unsound. *)
   155            Tags (Polymorphic, level, Heavy)
   156          | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
   157          | ("args", (SOME poly, All_Types (* naja *), Light)) =>
   158            Preds (poly, Const_Arg_Types, Light)
   159          | ("erased", (NONE, All_Types (* naja *), Light)) =>
   160            Preds (Polymorphic, No_Types, Light)
   161          | _ => raise Same.SAME)
   162   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
   163 
   164 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
   165   | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
   166   | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
   167 
   168 fun level_of_type_sys (Simple_Types level) = level
   169   | level_of_type_sys (Preds (_, level, _)) = level
   170   | level_of_type_sys (Tags (_, level, _)) = level
   171 
   172 fun heaviness_of_type_sys (Simple_Types _) = Heavy
   173   | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
   174   | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
   175 
   176 fun is_type_level_virtually_sound level =
   177   level = All_Types orelse level = Nonmonotonic_Types
   178 val is_type_sys_virtually_sound =
   179   is_type_level_virtually_sound o level_of_type_sys
   180 
   181 fun is_type_level_fairly_sound level =
   182   is_type_level_virtually_sound level orelse level = Finite_Types
   183 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
   184 
   185 fun is_setting_higher_order THF (Simple_Types _) = true
   186   | is_setting_higher_order _ _ = false
   187 
   188 type translated_formula =
   189   {name: string,
   190    locality: locality,
   191    kind: formula_kind,
   192    combformula: (name, typ, combterm) formula,
   193    atomic_types: typ list}
   194 
   195 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
   196                           : translated_formula) =
   197   {name = name, locality = locality, kind = kind, combformula = f combformula,
   198    atomic_types = atomic_types} : translated_formula
   199 
   200 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
   201 
   202 
   203 (* The Booleans indicate whether all type arguments should be kept. *)
   204 datatype type_arg_policy =
   205   Explicit_Type_Args of bool |
   206   Mangled_Type_Args of bool |
   207   No_Type_Args
   208 
   209 fun should_drop_arg_type_args (Simple_Types _) =
   210     false (* since TFF doesn't support overloading *)
   211   | should_drop_arg_type_args type_sys =
   212     level_of_type_sys type_sys = All_Types andalso
   213     heaviness_of_type_sys type_sys = Heavy
   214 
   215 fun general_type_arg_policy type_sys =
   216   if level_of_type_sys type_sys = No_Types then
   217     No_Type_Args
   218   else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
   219     Mangled_Type_Args (should_drop_arg_type_args type_sys)
   220   else
   221     Explicit_Type_Args (should_drop_arg_type_args type_sys)
   222 
   223 fun type_arg_policy type_sys s =
   224   if s = @{const_name HOL.eq} orelse
   225      (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
   226     No_Type_Args
   227   else
   228     general_type_arg_policy type_sys
   229 
   230 fun atp_type_literals_for_types format type_sys kind Ts =
   231   if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then
   232     []
   233   else
   234     Ts |> type_literals_for_types
   235        |> filter (fn TyLitVar _ => kind <> Conjecture
   236                    | TyLitFree _ => kind = Conjecture)
   237 
   238 fun mk_aconns c phis =
   239   let val (phis', phi') = split_last phis in
   240     fold_rev (mk_aconn c) phis' phi'
   241   end
   242 fun mk_ahorn [] phi = phi
   243   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
   244 fun mk_aquant _ [] phi = phi
   245   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
   246     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
   247   | mk_aquant q xs phi = AQuant (q, xs, phi)
   248 
   249 fun close_universally atom_vars phi =
   250   let
   251     fun formula_vars bounds (AQuant (_, xs, phi)) =
   252         formula_vars (map fst xs @ bounds) phi
   253       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   254       | formula_vars bounds (AAtom tm) =
   255         union (op =) (atom_vars tm []
   256                       |> filter_out (member (op =) bounds o fst))
   257   in mk_aquant AForall (formula_vars [] phi []) phi end
   258 
   259 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
   260   | combterm_vars (CombConst _) = I
   261   | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
   262 fun close_combformula_universally phi = close_universally combterm_vars phi
   263 
   264 fun term_vars (ATerm (name as (s, _), tms)) =
   265   is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
   266 fun close_formula_universally phi = close_universally term_vars phi
   267 
   268 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
   269 val homo_infinite_type = Type (homo_infinite_type_name, [])
   270 
   271 fun fo_term_from_typ higher_order =
   272   let
   273     fun term (Type (s, Ts)) =
   274       ATerm (case (higher_order, s) of
   275                (true, @{type_name bool}) => `I tptp_bool_type
   276              | (true, @{type_name fun}) => `I tptp_fun_type
   277              | _ => if s = homo_infinite_type_name then `I tptp_individual_type
   278                     else `make_fixed_type_const s,
   279              map term Ts)
   280     | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
   281     | term (TVar ((x as (s, _)), _)) =
   282       ATerm ((make_schematic_type_var x, s), [])
   283   in term end
   284 
   285 (* This shouldn't clash with anything else. *)
   286 val mangled_type_sep = "\000"
   287 
   288 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   289   | generic_mangled_type_name f (ATerm (name, tys)) =
   290     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
   291     ^ ")"
   292 
   293 val bool_atype = AType (`I tptp_bool_type)
   294 
   295 fun ho_type_from_fo_term higher_order pred_sym ary =
   296   let
   297     fun to_atype ty =
   298       AType ((make_simple_type (generic_mangled_type_name fst ty),
   299               generic_mangled_type_name snd ty))
   300     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
   301     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
   302       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
   303     fun to_ho (ty as ATerm ((s, _), tys)) =
   304       if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
   305   in if higher_order then to_ho else to_fo ary end
   306 
   307 fun mangled_type higher_order pred_sym ary =
   308   ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order
   309 
   310 fun mangled_const_name T_args (s, s') =
   311   let
   312     val ty_args = map (fo_term_from_typ false) T_args
   313     fun type_suffix f g =
   314       fold_rev (curry (op ^) o g o prefix mangled_type_sep
   315                 o generic_mangled_type_name f) ty_args ""
   316   in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
   317 
   318 val parse_mangled_ident =
   319   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
   320 
   321 fun parse_mangled_type x =
   322   (parse_mangled_ident
   323    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
   324                     [] >> ATerm) x
   325 and parse_mangled_types x =
   326   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
   327 
   328 fun unmangled_type s =
   329   s |> suffix ")" |> raw_explode
   330     |> Scan.finite Symbol.stopper
   331            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
   332                                                 quote s)) parse_mangled_type))
   333     |> fst
   334 
   335 val unmangled_const_name = space_explode mangled_type_sep #> hd
   336 fun unmangled_const s =
   337   let val ss = space_explode mangled_type_sep s in
   338     (hd ss, map unmangled_type (tl ss))
   339   end
   340 
   341 fun introduce_proxies format type_sys tm =
   342   let
   343     fun aux ary top_level (CombApp (tm1, tm2)) =
   344         CombApp (aux (ary + 1) top_level tm1, aux 0 false tm2)
   345       | aux ary top_level (CombConst (name as (s, s'), T, T_args)) =
   346         (case proxify_const s of
   347            SOME proxy_base =>
   348            (* Proxies are not needed in THF, except for partially applied
   349               equality since THF does not provide any syntax for it. *)
   350            if top_level orelse
   351               (is_setting_higher_order format type_sys andalso
   352                (s <> "equal" orelse ary = 2)) then
   353              (case s of
   354                 "c_False" => (tptp_false, s')
   355               | "c_True" => (tptp_true, s')
   356               | _ => name, [])
   357            else
   358              (proxy_base |>> prefix const_prefix, T_args)
   359           | NONE => (name, T_args))
   360         |> (fn (name, T_args) => CombConst (name, T, T_args))
   361       | aux _ _ tm = tm
   362   in aux 0 true tm end
   363 
   364 fun combformula_from_prop thy format type_sys eq_as_iff =
   365   let
   366     fun do_term bs t atomic_types =
   367       combterm_from_term thy bs (Envir.eta_contract t)
   368       |>> (introduce_proxies format type_sys #> AAtom)
   369       ||> union (op =) atomic_types
   370     fun do_quant bs q s T t' =
   371       let val s = Name.variant (map fst bs) s in
   372         do_formula ((s, T) :: bs) t'
   373         #>> mk_aquant q [(`make_bound_var s, SOME T)]
   374       end
   375     and do_conn bs c t1 t2 =
   376       do_formula bs t1 ##>> do_formula bs t2
   377       #>> uncurry (mk_aconn c)
   378     and do_formula bs t =
   379       case t of
   380         @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
   381       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   382         do_quant bs AForall s T t'
   383       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   384         do_quant bs AExists s T t'
   385       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
   386       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
   387       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
   388       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   389         if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
   390       | _ => do_term bs t
   391   in do_formula [] end
   392 
   393 fun presimplify_term ctxt =
   394   Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
   395   #> Meson.presimplify ctxt
   396   #> prop_of
   397 
   398 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
   399 fun conceal_bounds Ts t =
   400   subst_bounds (map (Free o apfst concealed_bound_name)
   401                     (0 upto length Ts - 1 ~~ Ts), t)
   402 fun reveal_bounds Ts =
   403   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   404                     (0 upto length Ts - 1 ~~ Ts))
   405 
   406 fun extensionalize_term ctxt t =
   407   let val thy = Proof_Context.theory_of ctxt in
   408     t |> cterm_of thy |> Meson.extensionalize_conv ctxt
   409       |> prop_of |> Logic.dest_equals |> snd
   410   end
   411 
   412 fun introduce_combinators_in_term ctxt kind t =
   413   let val thy = Proof_Context.theory_of ctxt in
   414     if Meson.is_fol_term thy t then
   415       t
   416     else
   417       let
   418         fun aux Ts t =
   419           case t of
   420             @{const Not} $ t1 => @{const Not} $ aux Ts t1
   421           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   422             t0 $ Abs (s, T, aux (T :: Ts) t')
   423           | (t0 as Const (@{const_name All}, _)) $ t1 =>
   424             aux Ts (t0 $ eta_expand Ts t1 1)
   425           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   426             t0 $ Abs (s, T, aux (T :: Ts) t')
   427           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   428             aux Ts (t0 $ eta_expand Ts t1 1)
   429           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   430           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   431           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   432           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   433               $ t1 $ t2 =>
   434             t0 $ aux Ts t1 $ aux Ts t2
   435           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   436                    t
   437                  else
   438                    t |> conceal_bounds Ts
   439                      |> Envir.eta_contract
   440                      |> cterm_of thy
   441                      |> Meson_Clausify.introduce_combinators_in_cterm
   442                      |> prop_of |> Logic.dest_equals |> snd
   443                      |> reveal_bounds Ts
   444         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   445       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   446       handle THM _ =>
   447              (* A type variable of sort "{}" will make abstraction fail. *)
   448              if kind = Conjecture then HOLogic.false_const
   449              else HOLogic.true_const
   450   end
   451 
   452 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   453    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
   454 fun freeze_term t =
   455   let
   456     fun aux (t $ u) = aux t $ aux u
   457       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   458       | aux (Var ((s, i), T)) =
   459         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   460       | aux t = t
   461   in t |> exists_subterm is_Var t ? aux end
   462 
   463 (* making fact and conjecture formulas *)
   464 fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t =
   465   let
   466     val thy = Proof_Context.theory_of ctxt
   467     val t = t |> Envir.beta_eta_contract
   468               |> transform_elim_prop
   469               |> Object_Logic.atomize_term thy
   470     val need_trueprop = (fastype_of t = @{typ bool})
   471     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   472               |> Raw_Simplifier.rewrite_term thy
   473                      (Meson.unfold_set_const_simps ctxt) []
   474               |> extensionalize_term ctxt
   475               |> presimp ? presimplify_term ctxt
   476               |> perhaps (try (HOLogic.dest_Trueprop))
   477               |> introduce_combinators_in_term ctxt kind
   478               |> kind <> Axiom ? freeze_term
   479     val (combformula, atomic_types) =
   480       combformula_from_prop thy format type_sys eq_as_iff t []
   481   in
   482     {name = name, locality = loc, kind = kind, combformula = combformula,
   483      atomic_types = atomic_types}
   484   end
   485 
   486 fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp
   487               ((name, loc), t) =
   488   case (keep_trivial,
   489         make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of
   490     (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
   491     NONE
   492   | (_, formula) => SOME formula
   493 
   494 fun make_conjecture ctxt format prem_kind type_sys ts =
   495   let val last = length ts - 1 in
   496     map2 (fn j => fn t =>
   497              let
   498                val (kind, maybe_negate) =
   499                  if j = last then
   500                    (Conjecture, I)
   501                  else
   502                    (prem_kind,
   503                     if prem_kind = Conjecture then update_combformula mk_anot
   504                     else I)
   505               in
   506                 t |> make_formula ctxt format type_sys true true
   507                                   (string_of_int j) General kind
   508                   |> maybe_negate
   509               end)
   510          (0 upto last) ts
   511   end
   512 
   513 (** Finite and infinite type inference **)
   514 
   515 fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
   516   | deep_freeze_atyp T = T
   517 val deep_freeze_type = map_atyps deep_freeze_atyp
   518 
   519 val type_instance = Sign.typ_instance o Proof_Context.theory_of
   520 
   521 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
   522    dangerous because their "exhaust" properties can easily lead to unsound ATP
   523    proofs. On the other hand, all HOL infinite types can be given the same
   524    models in first-order logic (via Löwenheim-Skolem). *)
   525 
   526 fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
   527     exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
   528   | should_encode_type _ _ All_Types _ = true
   529   | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
   530   | should_encode_type _ _ _ _ = false
   531 
   532 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
   533                              should_predicate_on_var T =
   534     (heaviness = Heavy orelse should_predicate_on_var ()) andalso
   535     should_encode_type ctxt nonmono_Ts level T
   536   | should_predicate_on_type _ _ _ _ _ = false
   537 
   538 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
   539     String.isPrefix bound_var_prefix s
   540   | is_var_or_bound_var (CombVar _) = true
   541   | is_var_or_bound_var _ = false
   542 
   543 datatype tag_site = Top_Level | Eq_Arg | Elsewhere
   544 
   545 fun should_tag_with_type _ _ _ Top_Level _ _ = false
   546   | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
   547     (case heaviness of
   548        Heavy => should_encode_type ctxt nonmono_Ts level T
   549      | Light =>
   550        case (site, is_var_or_bound_var u) of
   551          (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
   552        | _ => false)
   553   | should_tag_with_type _ _ _ _ _ _ = false
   554 
   555 fun homogenized_type ctxt nonmono_Ts level =
   556   let
   557     val should_encode = should_encode_type ctxt nonmono_Ts level
   558     fun homo 0 T = if should_encode T then T else homo_infinite_type
   559       | homo ary (Type (@{type_name fun}, [T1, T2])) =
   560         homo 0 T1 --> homo (ary - 1) T2
   561       | homo _ _ = raise Fail "expected function type"
   562   in homo end
   563 
   564 (** "hBOOL" and "hAPP" **)
   565 
   566 type sym_info =
   567   {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option}
   568 
   569 fun add_combterm_syms_to_table explicit_apply =
   570   let
   571     fun aux top_level tm =
   572       let val (head, args) = strip_combterm_comb tm in
   573         (case head of
   574            CombConst ((s, _), T, _) =>
   575            if String.isPrefix bound_var_prefix s then
   576              I
   577            else
   578              let val ary = length args in
   579                Symtab.map_default
   580                    (s, {pred_sym = true,
   581                         min_ary = if explicit_apply then 0 else ary,
   582                         max_ary = 0, typ = SOME T})
   583                    (fn {pred_sym, min_ary, max_ary, typ} =>
   584                        {pred_sym = pred_sym andalso top_level,
   585                         min_ary = Int.min (ary, min_ary),
   586                         max_ary = Int.max (ary, max_ary),
   587                         typ = if typ = SOME T then typ else NONE})
   588             end
   589          | _ => I)
   590         #> fold (aux false) args
   591       end
   592   in aux true end
   593 fun add_fact_syms_to_table explicit_apply =
   594   fact_lift (formula_fold NONE (K (add_combterm_syms_to_table explicit_apply)))
   595 
   596 val default_sym_table_entries : (string * sym_info) list =
   597   [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
   598    (make_fixed_const predicator_name,
   599     {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
   600   ([tptp_false, tptp_true]
   601    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
   602 
   603 fun sym_table_for_facts explicit_apply facts =
   604   Symtab.empty |> fold Symtab.default default_sym_table_entries
   605                |> fold (add_fact_syms_to_table explicit_apply) facts
   606 
   607 fun min_arity_of sym_tab s =
   608   case Symtab.lookup sym_tab s of
   609     SOME ({min_ary, ...} : sym_info) => min_ary
   610   | NONE =>
   611     case strip_prefix_and_unascii const_prefix s of
   612       SOME s =>
   613       let val s = s |> unmangled_const_name |> invert_const in
   614         if s = predicator_name then 1
   615         else if s = app_op_name then 2
   616         else if s = type_pred_name then 1
   617         else 0
   618       end
   619     | NONE => 0
   620 
   621 (* True if the constant ever appears outside of the top-level position in
   622    literals, or if it appears with different arities (e.g., because of different
   623    type instantiations). If false, the constant always receives all of its
   624    arguments and is used as a predicate. *)
   625 fun is_pred_sym sym_tab s =
   626   case Symtab.lookup sym_tab s of
   627     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
   628     pred_sym andalso min_ary = max_ary
   629   | NONE => false
   630 
   631 val predicator_combconst =
   632   CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
   633 fun predicator tm = CombApp (predicator_combconst, tm)
   634 
   635 fun introduce_predicators_in_combterm sym_tab tm =
   636   case strip_combterm_comb tm of
   637     (CombConst ((s, _), _, _), _) =>
   638     if is_pred_sym sym_tab s then tm else predicator tm
   639   | _ => predicator tm
   640 
   641 fun list_app head args = fold (curry (CombApp o swap)) args head
   642 
   643 fun explicit_app arg head =
   644   let
   645     val head_T = combtyp_of head
   646     val (arg_T, res_T) = dest_funT head_T
   647     val explicit_app =
   648       CombConst (`make_fixed_const app_op_name, head_T --> head_T,
   649                  [arg_T, res_T])
   650   in list_app explicit_app [head, arg] end
   651 fun list_explicit_app head args = fold explicit_app args head
   652 
   653 fun introduce_explicit_apps_in_combterm sym_tab =
   654   let
   655     fun aux tm =
   656       case strip_combterm_comb tm of
   657         (head as CombConst ((s, _), _, _), args) =>
   658         args |> map aux
   659              |> chop (min_arity_of sym_tab s)
   660              |>> list_app head
   661              |-> list_explicit_app
   662       | (head, args) => list_explicit_app head (map aux args)
   663   in aux end
   664 
   665 fun chop_fun 0 T = ([], T)
   666   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
   667     chop_fun (n - 1) ran_T |>> cons dom_T
   668   | chop_fun _ _ = raise Fail "unexpected non-function"
   669 
   670 fun filter_type_args _ _ _ [] = []
   671   | filter_type_args thy s arity T_args =
   672     let
   673       (* will throw "TYPE" for pseudo-constants *)
   674       val U = if s = app_op_name then
   675                 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
   676               else
   677                 s |> Sign.the_const_type thy
   678     in
   679       case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
   680         [] => []
   681       | res_U_vars =>
   682         let val U_args = (s, U) |> Sign.const_typargs thy in
   683           U_args ~~ T_args
   684           |> map_filter (fn (U, T) =>
   685                             if member (op =) res_U_vars (dest_TVar U) then
   686                               SOME T
   687                             else
   688                               NONE)
   689         end
   690     end
   691     handle TYPE _ => T_args
   692 
   693 fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
   694   let
   695     val thy = Proof_Context.theory_of ctxt
   696     fun aux arity (CombApp (tm1, tm2)) =
   697         CombApp (aux (arity + 1) tm1, aux 0 tm2)
   698       | aux arity (CombConst (name as (s, _), T, T_args)) =
   699         let
   700           val level = level_of_type_sys type_sys
   701           val (T, T_args) =
   702             (* Aggressively merge most "hAPPs" if the type system is unsound
   703                anyway, by distinguishing overloads only on the homogenized
   704                result type. Don't do it for lightweight type systems, though,
   705                since it leads to too many unsound proofs. *)
   706             if s = const_prefix ^ app_op_name andalso
   707                length T_args = 2 andalso
   708                not (is_type_sys_virtually_sound type_sys) andalso
   709                heaviness_of_type_sys type_sys = Heavy then
   710               T_args |> map (homogenized_type ctxt nonmono_Ts level 0)
   711                      |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
   712                                     (T --> T, tl Ts)
   713                                   end)
   714             else
   715               (T, T_args)
   716         in
   717           (case strip_prefix_and_unascii const_prefix s of
   718              NONE => (name, T_args)
   719            | SOME s'' =>
   720              let
   721                val s'' = invert_const s''
   722                fun filtered_T_args false = T_args
   723                  | filtered_T_args true = filter_type_args thy s'' arity T_args
   724              in
   725                case type_arg_policy type_sys s'' of
   726                  Explicit_Type_Args drop_args =>
   727                  (name, filtered_T_args drop_args)
   728                | Mangled_Type_Args drop_args =>
   729                  (mangled_const_name (filtered_T_args drop_args) name, [])
   730                | No_Type_Args => (name, [])
   731              end)
   732           |> (fn (name, T_args) => CombConst (name, T, T_args))
   733         end
   734       | aux _ tm = tm
   735   in aux 0 end
   736 
   737 fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =
   738   not (is_setting_higher_order format type_sys)
   739   ? (introduce_explicit_apps_in_combterm sym_tab
   740      #> introduce_predicators_in_combterm sym_tab)
   741   #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
   742 fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =
   743   update_combformula (formula_map
   744       (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))
   745 
   746 (** Helper facts **)
   747 
   748 fun ti_ti_helper_fact () =
   749   let
   750     fun var s = ATerm (`I s, [])
   751     fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
   752   in
   753     Formula (helper_prefix ^ "ti_ti", Axiom,
   754              AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
   755              |> close_formula_universally, simp_info, NONE)
   756   end
   757 
   758 fun helper_facts_for_sym ctxt format type_sys (s, {typ, ...} : sym_info) =
   759   case strip_prefix_and_unascii const_prefix s of
   760     SOME mangled_s =>
   761     let
   762       val thy = Proof_Context.theory_of ctxt
   763       val unmangled_s = mangled_s |> unmangled_const_name
   764       fun dub_and_inst c needs_fairly_sound (th, j) =
   765         ((c ^ "_" ^ string_of_int j ^
   766           (if needs_fairly_sound then typed_helper_suffix
   767            else untyped_helper_suffix),
   768           General),
   769          let val t = th |> prop_of in
   770            t |> ((case general_type_arg_policy type_sys of
   771                     Mangled_Type_Args _ => true
   772                   | _ => false) andalso
   773                  not (null (Term.hidden_polymorphism t)))
   774                 ? (case typ of
   775                      SOME T => specialize_type thy (invert_const unmangled_s, T)
   776                    | NONE => I)
   777          end)
   778       fun make_facts eq_as_iff =
   779         map_filter (make_fact ctxt format type_sys false eq_as_iff false)
   780       val fairly_sound = is_type_sys_fairly_sound type_sys
   781     in
   782       metis_helpers
   783       |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>
   784                   if metis_s <> unmangled_s orelse
   785                      (needs_fairly_sound andalso not fairly_sound) then
   786                     []
   787                   else
   788                     ths ~~ (1 upto length ths)
   789                     |> map (dub_and_inst mangled_s needs_fairly_sound)
   790                     |> make_facts (not needs_fairly_sound))
   791     end
   792   | NONE => []
   793 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
   794   Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
   795                   []
   796 
   797 fun translate_atp_fact ctxt format type_sys keep_trivial =
   798   `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of)
   799 
   800 fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t
   801                        rich_facts =
   802   let
   803     val thy = Proof_Context.theory_of ctxt
   804     val fact_ts = map (prop_of o snd o snd) rich_facts
   805     val (facts, fact_names) =
   806       rich_facts
   807       |> map_filter (fn (NONE, _) => NONE
   808                       | (SOME fact, (name, _)) => SOME (fact, name))
   809       |> ListPair.unzip
   810     (* Remove existing facts from the conjecture, as this can dramatically
   811        boost an ATP's performance (for some reason). *)
   812     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
   813     val goal_t = Logic.list_implies (hyp_ts, concl_t)
   814     val all_ts = goal_t :: fact_ts
   815     val subs = tfree_classes_of_terms all_ts
   816     val supers = tvar_classes_of_terms all_ts
   817     val tycons = type_consts_of_terms thy all_ts
   818     val conjs =
   819       hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys
   820     val (supers', arity_clauses) =
   821       if level_of_type_sys type_sys = No_Types then ([], [])
   822       else make_arity_clauses thy tycons supers
   823     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   824   in
   825     (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
   826   end
   827 
   828 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
   829     (true, ATerm (class, [ATerm (name, [])]))
   830   | fo_literal_from_type_literal (TyLitFree (class, name)) =
   831     (true, ATerm (class, [ATerm (name, [])]))
   832 
   833 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   834 
   835 fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =
   836   CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T])
   837            |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
   838            tm)
   839 
   840 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
   841   | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
   842     accum orelse (s = "equal" andalso member (op =) tms (ATerm (name, [])))
   843 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
   844   | is_var_nonmonotonic_in_formula pos phi _ name =
   845     formula_fold pos (var_occurs_positively_naked_in_term name) phi false
   846 
   847 fun mk_const_aterm x T_args args =
   848   ATerm (x, map (fo_term_from_typ false) T_args @ args)
   849 
   850 fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
   851   CombConst (`make_fixed_const type_tag_name, T --> T, [T])
   852   |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
   853   |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
   854   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
   855 and term_from_combterm ctxt format nonmono_Ts type_sys =
   856   let
   857     fun aux site u =
   858       let
   859         val (head, args) = strip_combterm_comb u
   860         val (x as (s, _), T_args) =
   861           case head of
   862             CombConst (name, _, T_args) => (name, T_args)
   863           | CombVar (name, _) => (name, [])
   864           | CombApp _ => raise Fail "impossible \"CombApp\""
   865         val arg_site = if site = Top_Level andalso s = "equal" then Eq_Arg
   866                        else Elsewhere
   867         val t = mk_const_aterm x T_args (map (aux arg_site) args)
   868         val T = combtyp_of u
   869       in
   870         t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
   871                 tag_with_type ctxt format nonmono_Ts type_sys T
   872               else
   873                 I)
   874       end
   875   in aux end
   876 and formula_from_combformula ctxt format nonmono_Ts type_sys
   877                              should_predicate_on_var =
   878   let
   879     val higher_order = is_setting_higher_order format type_sys
   880     val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
   881     val do_bound_type =
   882       case type_sys of
   883         Simple_Types level =>
   884         homogenized_type ctxt nonmono_Ts level 0
   885         #> mangled_type higher_order false 0 #> SOME
   886       | _ => K NONE
   887     fun do_out_of_bound_type pos phi universal (name, T) =
   888       if should_predicate_on_type ctxt nonmono_Ts type_sys
   889              (fn () => should_predicate_on_var pos phi universal name) T then
   890         CombVar (name, T)
   891         |> type_pred_combterm ctxt nonmono_Ts type_sys T
   892         |> do_term |> AAtom |> SOME
   893       else
   894         NONE
   895     fun do_formula pos (AQuant (q, xs, phi)) =
   896         let
   897           val phi = phi |> do_formula pos
   898           val universal = Option.map (q = AExists ? not) pos
   899         in
   900           AQuant (q, xs |> map (apsnd (fn NONE => NONE
   901                                         | SOME T => do_bound_type T)),
   902                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
   903                       (map_filter
   904                            (fn (_, NONE) => NONE
   905                              | (s, SOME T) =>
   906                                do_out_of_bound_type pos phi universal (s, T))
   907                            xs)
   908                       phi)
   909         end
   910       | do_formula pos (AConn conn) = aconn_map pos do_formula conn
   911       | do_formula _ (AAtom tm) = AAtom (do_term tm)
   912   in do_formula o SOME end
   913 
   914 fun bound_atomic_types format type_sys Ts =
   915   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
   916                 (atp_type_literals_for_types format type_sys Axiom Ts))
   917 
   918 fun formula_for_fact ctxt format nonmono_Ts type_sys
   919                      ({combformula, atomic_types, ...} : translated_formula) =
   920   combformula
   921   |> close_combformula_universally
   922   |> formula_from_combformula ctxt format nonmono_Ts type_sys
   923                               is_var_nonmonotonic_in_formula true
   924   |> bound_atomic_types format type_sys atomic_types
   925   |> close_formula_universally
   926 
   927 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   928    of monomorphization). The TPTP explicitly forbids name clashes, and some of
   929    the remote provers might care. *)
   930 fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys
   931                           (j, formula as {name, locality, kind, ...}) =
   932   Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
   933                      else string_of_int j ^ "_") ^
   934            ascii_of name,
   935            kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
   936            case locality of
   937              Intro => intro_info
   938            | Elim => elim_info
   939            | Simp => simp_info
   940            | _ => NONE)
   941 
   942 fun formula_line_for_class_rel_clause
   943         (ClassRelClause {name, subclass, superclass, ...}) =
   944   let val ty_arg = ATerm (`I "T", []) in
   945     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
   946              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   947                                AAtom (ATerm (superclass, [ty_arg]))])
   948              |> close_formula_universally, intro_info, NONE)
   949   end
   950 
   951 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
   952     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   953   | fo_literal_from_arity_literal (TVarLit (c, sort)) =
   954     (false, ATerm (c, [ATerm (sort, [])]))
   955 
   956 fun formula_line_for_arity_clause
   957         (ArityClause {name, prem_lits, concl_lits, ...}) =
   958   Formula (arity_clause_prefix ^ ascii_of name, Axiom,
   959            mk_ahorn (map (formula_from_fo_literal o apfst not
   960                           o fo_literal_from_arity_literal) prem_lits)
   961                     (formula_from_fo_literal
   962                          (fo_literal_from_arity_literal concl_lits))
   963            |> close_formula_universally, intro_info, NONE)
   964 
   965 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
   966         ({name, kind, combformula, ...} : translated_formula) =
   967   Formula (conjecture_prefix ^ name, kind,
   968            formula_from_combformula ctxt format nonmono_Ts type_sys
   969                is_var_nonmonotonic_in_formula false
   970                (close_combformula_universally combformula)
   971            |> close_formula_universally, NONE, NONE)
   972 
   973 fun free_type_literals format type_sys
   974                        ({atomic_types, ...} : translated_formula) =
   975   atomic_types |> atp_type_literals_for_types format type_sys Conjecture
   976                |> map fo_literal_from_type_literal
   977 
   978 fun formula_line_for_free_type j lit =
   979   Formula (tfree_prefix ^ string_of_int j, Hypothesis,
   980            formula_from_fo_literal lit, NONE, NONE)
   981 fun formula_lines_for_free_types format type_sys facts =
   982   let
   983     val litss = map (free_type_literals format type_sys) facts
   984     val lits = fold (union (op =)) litss []
   985   in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
   986 
   987 (** Symbol declarations **)
   988 
   989 fun insert_type ctxt get_T x xs =
   990   let val T = get_T x in
   991     if exists (curry (type_instance ctxt) T o get_T) xs then xs
   992     else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
   993   end
   994 
   995 fun should_declare_sym type_sys pred_sym s =
   996   is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
   997   (case type_sys of
   998      Simple_Types _ => true
   999    | Tags (_, _, Light) => true
  1000    | _ => not pred_sym)
  1001 
  1002 fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
  1003   let
  1004     fun add_combterm in_conj tm =
  1005       let val (head, args) = strip_combterm_comb tm in
  1006         (case head of
  1007            CombConst ((s, s'), T, T_args) =>
  1008            let val pred_sym = is_pred_sym repaired_sym_tab s in
  1009              if should_declare_sym type_sys pred_sym s then
  1010                Symtab.map_default (s, [])
  1011                    (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
  1012                                          in_conj))
  1013              else
  1014                I
  1015            end
  1016          | _ => I)
  1017         #> fold (add_combterm in_conj) args
  1018       end
  1019     fun add_fact in_conj =
  1020       fact_lift (formula_fold NONE (K (add_combterm in_conj)))
  1021   in
  1022     Symtab.empty
  1023     |> is_type_sys_fairly_sound type_sys
  1024        ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
  1025   end
  1026 
  1027 (* These types witness that the type classes they belong to allow infinite
  1028    models and hence that any types with these type classes is monotonic. *)
  1029 val known_infinite_types = [@{typ nat}, @{typ int}, @{typ "nat => bool"}]
  1030 
  1031 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
  1032    out with monotonicity" paper presented at CADE 2011. *)
  1033 fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
  1034   | add_combterm_nonmonotonic_types ctxt level _
  1035         (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
  1036                   tm2)) =
  1037     (exists is_var_or_bound_var [tm1, tm2] andalso
  1038      (case level of
  1039         Nonmonotonic_Types =>
  1040         not (is_type_surely_infinite ctxt known_infinite_types T)
  1041       | Finite_Types => is_type_surely_finite ctxt T
  1042       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
  1043   | add_combterm_nonmonotonic_types _ _ _ _ = I
  1044 fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}
  1045                                             : translated_formula) =
  1046   formula_fold (SOME (kind <> Conjecture))
  1047                (add_combterm_nonmonotonic_types ctxt level) combformula
  1048 fun nonmonotonic_types_for_facts ctxt type_sys facts =
  1049   let val level = level_of_type_sys type_sys in
  1050     if level = Nonmonotonic_Types orelse level = Finite_Types then
  1051       [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
  1052          (* We must add "bool" in case the helper "True_or_False" is added
  1053             later. In addition, several places in the code rely on the list of
  1054             nonmonotonic types not being empty. *)
  1055          |> insert_type ctxt I @{typ bool}
  1056     else
  1057       []
  1058   end
  1059 
  1060 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
  1061                       (s', T_args, T, pred_sym, ary, _) =
  1062   let
  1063     val (higher_order, T_arg_Ts, level) =
  1064       case type_sys of
  1065         Simple_Types level => (format = THF, [], level)
  1066       | _ => (false, replicate (length T_args) homo_infinite_type, No_Types)
  1067   in
  1068     Decl (sym_decl_prefix ^ s, (s, s'),
  1069           (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
  1070           |> mangled_type higher_order pred_sym (length T_arg_Ts + ary))
  1071   end
  1072 
  1073 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
  1074 
  1075 fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys
  1076                                    n s j (s', T_args, T, _, ary, in_conj) =
  1077   let
  1078     val (kind, maybe_negate) =
  1079       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  1080       else (Axiom, I)
  1081     val (arg_Ts, res_T) = chop_fun ary T
  1082     val bound_names =
  1083       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
  1084     val bounds =
  1085       bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
  1086     val bound_Ts =
  1087       arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
  1088                              else NONE)
  1089   in
  1090     Formula (sym_formula_prefix ^ s ^
  1091              (if n > 1 then "_" ^ string_of_int j else ""), kind,
  1092              CombConst ((s, s'), T, T_args)
  1093              |> fold (curry (CombApp o swap)) bounds
  1094              |> type_pred_combterm ctxt nonmono_Ts type_sys res_T
  1095              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
  1096              |> formula_from_combformula ctxt format nonmono_Ts type_sys
  1097                                          (K (K (K (K true)))) true
  1098              |> n > 1 ? bound_atomic_types format type_sys (atyps_of T)
  1099              |> close_formula_universally
  1100              |> maybe_negate,
  1101              intro_info, NONE)
  1102   end
  1103 
  1104 fun formula_lines_for_tag_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys
  1105         n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  1106   let
  1107     val ident_base =
  1108       sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
  1109     val (kind, maybe_negate) =
  1110       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  1111       else (Axiom, I)
  1112     val (arg_Ts, res_T) = chop_fun ary T
  1113     val bound_names =
  1114       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
  1115     val bounds = bound_names |> map (fn name => ATerm (name, []))
  1116     val cst = mk_const_aterm (s, s') T_args
  1117     val atomic_Ts = atyps_of T
  1118     fun eq tms =
  1119       (if pred_sym then AConn (AIff, map AAtom tms)
  1120        else AAtom (ATerm (`I "equal", tms)))
  1121       |> bound_atomic_types format type_sys atomic_Ts
  1122       |> close_formula_universally
  1123       |> maybe_negate
  1124     val should_encode = should_encode_type ctxt nonmono_Ts All_Types
  1125     val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
  1126     val add_formula_for_res =
  1127       if should_encode res_T then
  1128         cons (Formula (ident_base ^ "_res", kind,
  1129                        eq [tag_with res_T (cst bounds), cst bounds],
  1130                        simp_info, NONE))
  1131       else
  1132         I
  1133     fun add_formula_for_arg k =
  1134       let val arg_T = nth arg_Ts k in
  1135         if should_encode arg_T then
  1136           case chop k bounds of
  1137             (bounds1, bound :: bounds2) =>
  1138             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
  1139                            eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
  1140                                cst bounds],
  1141                            simp_info, NONE))
  1142           | _ => raise Fail "expected nonempty tail"
  1143         else
  1144           I
  1145       end
  1146   in
  1147     [] |> not pred_sym ? add_formula_for_res
  1148        |> fold add_formula_for_arg (ary - 1 downto 0)
  1149   end
  1150 
  1151 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
  1152 
  1153 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
  1154                                 (s, decls) =
  1155   case type_sys of
  1156     Simple_Types _ =>
  1157     decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
  1158   | Preds _ =>
  1159     let
  1160       val decls =
  1161         case decls of
  1162           decl :: (decls' as _ :: _) =>
  1163           let val T = result_type_of_decl decl in
  1164             if forall (curry (type_instance ctxt o swap) T
  1165                        o result_type_of_decl) decls' then
  1166               [decl]
  1167             else
  1168               decls
  1169           end
  1170         | _ => decls
  1171       val n = length decls
  1172       val decls =
  1173         decls
  1174         |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
  1175                    o result_type_of_decl)
  1176     in
  1177       (0 upto length decls - 1, decls)
  1178       |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
  1179                                                nonmono_Ts type_sys n s)
  1180     end
  1181   | Tags (_, _, heaviness) =>
  1182     (case heaviness of
  1183        Heavy => []
  1184      | Light =>
  1185        let val n = length decls in
  1186          (0 upto n - 1 ~~ decls)
  1187          |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
  1188                                                  nonmono_Ts type_sys n s)
  1189        end)
  1190 
  1191 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
  1192                                      type_sys sym_decl_tab =
  1193   sym_decl_tab
  1194   |> Symtab.dest
  1195   |> sort_wrt fst
  1196   |> rpair []
  1197   |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
  1198                                                      nonmono_Ts type_sys)
  1199 
  1200 fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
  1201     level = Nonmonotonic_Types orelse level = Finite_Types
  1202   | should_add_ti_ti_helper _ = false
  1203 
  1204 fun offset_of_heading_in_problem _ [] j = j
  1205   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
  1206     if heading = needle then j
  1207     else offset_of_heading_in_problem needle problem (j + length lines)
  1208 
  1209 val implicit_declsN = "Should-be-implicit typings"
  1210 val explicit_declsN = "Explicit typings"
  1211 val factsN = "Relevant facts"
  1212 val class_relsN = "Class relationships"
  1213 val aritiesN = "Arities"
  1214 val helpersN = "Helper facts"
  1215 val conjsN = "Conjectures"
  1216 val free_typesN = "Type variables"
  1217 
  1218 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
  1219                         explicit_apply hyp_ts concl_t facts =
  1220   let
  1221     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
  1222       translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts
  1223     val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
  1224     val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
  1225     val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab
  1226     val (conjs, facts) = (conjs, facts) |> pairself (map repair)
  1227     val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
  1228     val helpers =
  1229       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
  1230                        |> map repair
  1231     val lavish_nonmono_Ts =
  1232       if null nonmono_Ts orelse
  1233          polymorphism_of_type_sys type_sys <> Polymorphic then
  1234         nonmono_Ts
  1235       else
  1236         [TVar (("'a", 0), HOLogic.typeS)]
  1237     val sym_decl_lines =
  1238       (conjs, helpers @ facts)
  1239       |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
  1240       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind
  1241                                           lavish_nonmono_Ts type_sys
  1242     val helper_lines =
  1243       0 upto length helpers - 1 ~~ helpers
  1244       |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts
  1245                                     type_sys)
  1246       |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ())
  1247           else I)
  1248     (* Reordering these might confuse the proof reconstruction code or the SPASS
  1249        Flotter hack. *)
  1250     val problem =
  1251       [(explicit_declsN, sym_decl_lines),
  1252        (factsN,
  1253         map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)
  1254             (0 upto length facts - 1 ~~ facts)),
  1255        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
  1256        (aritiesN, map formula_line_for_arity_clause arity_clauses),
  1257        (helpersN, helper_lines),
  1258        (conjsN,
  1259         map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
  1260             conjs),
  1261        (free_typesN,
  1262         formula_lines_for_free_types format type_sys (facts @ conjs))]
  1263     val problem =
  1264       problem
  1265       |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
  1266       |> (if is_format_typed format then
  1267             declare_undeclared_syms_in_atp_problem type_decl_prefix
  1268                                                    implicit_declsN
  1269           else
  1270             I)
  1271     val (problem, pool) =
  1272       problem |> nice_atp_problem (Config.get ctxt readable_names)
  1273     val helpers_offset = offset_of_heading_in_problem helpersN problem 0
  1274     val typed_helpers =
  1275       map_filter (fn (j, {name, ...}) =>
  1276                      if String.isSuffix typed_helper_suffix name then SOME j
  1277                      else NONE)
  1278                  ((helpers_offset + 1 upto helpers_offset + length helpers)
  1279                   ~~ helpers)
  1280     fun add_sym_arity (s, {min_ary, ...} : sym_info) =
  1281       if min_ary > 0 then
  1282         case strip_prefix_and_unascii const_prefix s of
  1283           SOME s => Symtab.insert (op =) (s, min_ary)
  1284         | NONE => I
  1285       else
  1286         I
  1287   in
  1288     (problem,
  1289      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
  1290      offset_of_heading_in_problem conjsN problem 0,
  1291      offset_of_heading_in_problem factsN problem 0,
  1292      fact_names |> Vector.fromList,
  1293      typed_helpers,
  1294      Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
  1295   end
  1296 
  1297 (* FUDGE *)
  1298 val conj_weight = 0.0
  1299 val hyp_weight = 0.1
  1300 val fact_min_weight = 0.2
  1301 val fact_max_weight = 1.0
  1302 val type_info_default_weight = 0.8
  1303 
  1304 fun add_term_weights weight (ATerm (s, tms)) =
  1305   is_tptp_user_symbol s ? Symtab.default (s, weight)
  1306   #> fold (add_term_weights weight) tms
  1307 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
  1308     formula_fold NONE (K (add_term_weights weight)) phi
  1309   | add_problem_line_weights _ _ = I
  1310 
  1311 fun add_conjectures_weights [] = I
  1312   | add_conjectures_weights conjs =
  1313     let val (hyps, conj) = split_last conjs in
  1314       add_problem_line_weights conj_weight conj
  1315       #> fold (add_problem_line_weights hyp_weight) hyps
  1316     end
  1317 
  1318 fun add_facts_weights facts =
  1319   let
  1320     val num_facts = length facts
  1321     fun weight_of j =
  1322       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
  1323                         / Real.fromInt num_facts
  1324   in
  1325     map weight_of (0 upto num_facts - 1) ~~ facts
  1326     |> fold (uncurry add_problem_line_weights)
  1327   end
  1328 
  1329 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
  1330 fun atp_problem_weights problem =
  1331   let val get = these o AList.lookup (op =) problem in
  1332     Symtab.empty
  1333     |> add_conjectures_weights (get free_typesN @ get conjsN)
  1334     |> add_facts_weights (get factsN)
  1335     |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
  1336             [explicit_declsN, class_relsN, aritiesN]
  1337     |> Symtab.dest
  1338     |> sort (prod_ord Real.compare string_ord o pairself swap)
  1339   end
  1340 
  1341 end;