src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
author blanchet
Thu Feb 10 17:17:31 2011 +0100 (2011-02-10)
changeset 41748 657712cc8847
parent 41726 1ef01508bb9b
child 41769 eb2e39555f98
permissions -rw-r--r--
fix handling of "fequal" in generated ATP problems -- the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)
     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 problem = 'a ATP_Problem.problem
    12   type translated_formula
    13 
    14   datatype type_system =
    15     Tags of bool |
    16     Preds of bool |
    17     Const_Args |
    18     No_Types
    19 
    20   val precise_overloaded_args : bool Unsynchronized.ref
    21   val fact_prefix : string
    22   val conjecture_prefix : string
    23   val types_dangerous_types : type_system -> bool
    24   val num_atp_type_args : theory -> type_system -> string -> int
    25   val translate_atp_fact :
    26     Proof.context -> (string * 'a) * thm
    27     -> translated_formula option * ((string * 'a) * thm)
    28   val prepare_atp_problem :
    29     Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
    30     -> (translated_formula option * ((string * 'a) * thm)) list
    31     -> string problem * string Symtab.table * int * (string * 'a) list vector
    32   val atp_problem_weights : string problem -> (string * real) list
    33 end;
    34 
    35 structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
    36 struct
    37 
    38 open ATP_Problem
    39 open Metis_Translate
    40 open Sledgehammer_Util
    41 
    42 (* FIXME: Remove references once appropriate defaults have been determined
    43    empirically. *)
    44 val precise_overloaded_args = Unsynchronized.ref false
    45 
    46 val fact_prefix = "fact_"
    47 val conjecture_prefix = "conj_"
    48 val helper_prefix = "help_"
    49 val class_rel_clause_prefix = "clrel_";
    50 val arity_clause_prefix = "arity_"
    51 val tfree_prefix = "tfree_"
    52 
    53 (* Freshness almost guaranteed! *)
    54 val sledgehammer_weak_prefix = "Sledgehammer:"
    55 
    56 type translated_formula =
    57   {name: string,
    58    kind: kind,
    59    combformula: (name, combterm) formula,
    60    ctypes_sorts: typ list}
    61 
    62 datatype type_system =
    63   Tags of bool |
    64   Preds of bool |
    65   Const_Args |
    66   No_Types
    67 
    68 fun types_dangerous_types (Tags _) = true
    69   | types_dangerous_types (Preds _) = true
    70   | types_dangerous_types _ = false
    71 
    72 (* This is an approximation. If it returns "true" for a constant that isn't
    73    overloaded (i.e., that has one uniform definition), needless clutter is
    74    generated; if it returns "false" for an overloaded constant, the ATP gets a
    75    license to do unsound reasoning if the type system is "overloaded_args". *)
    76 fun is_overloaded thy s =
    77   not (s = @{const_name HOL.eq}) andalso
    78   not (s = @{const_name Metis.fequal}) andalso
    79   (not (!precise_overloaded_args) orelse s = @{const_name finite} orelse
    80    length (Defs.specifications_of (Theory.defs_of thy) s) > 1)
    81 
    82 fun needs_type_args thy type_sys s =
    83   case type_sys of
    84     Tags full_types => not full_types andalso is_overloaded thy s
    85   | Preds _ => is_overloaded thy s (* FIXME: could be more precise *)
    86   | Const_Args => is_overloaded thy s
    87   | No_Types => false
    88 
    89 fun num_atp_type_args thy type_sys s =
    90   if needs_type_args thy type_sys s then num_type_args thy s else 0
    91 
    92 fun atp_type_literals_for_types type_sys Ts =
    93   if type_sys = No_Types then [] else type_literals_for_types Ts
    94 
    95 fun mk_anot phi = AConn (ANot, [phi])
    96 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    97 fun mk_ahorn [] phi = phi
    98   | mk_ahorn (phi :: phis) psi =
    99     AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
   100 
   101 fun close_universally phi =
   102   let
   103     fun term_vars bounds (ATerm (name as (s, _), tms)) =
   104         (is_atp_variable s andalso not (member (op =) bounds name))
   105           ? insert (op =) name
   106         #> fold (term_vars bounds) tms
   107     fun formula_vars bounds (AQuant (_, xs, phi)) =
   108         formula_vars (xs @ bounds) phi
   109       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   110       | formula_vars bounds (AAtom tm) = term_vars bounds tm
   111   in
   112     case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   113   end
   114 
   115 fun combformula_for_prop thy eq_as_iff =
   116   let
   117     fun do_term bs t ts =
   118       combterm_from_term thy bs (Envir.eta_contract t)
   119       |>> AAtom ||> union (op =) ts
   120     fun do_quant bs q s T t' =
   121       let val s = Name.variant (map fst bs) s in
   122         do_formula ((s, T) :: bs) t'
   123         #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
   124       end
   125     and do_conn bs c t1 t2 =
   126       do_formula bs t1 ##>> do_formula bs t2
   127       #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
   128     and do_formula bs t =
   129       case t of
   130         @{const Not} $ t1 =>
   131         do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
   132       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   133         do_quant bs AForall s T t'
   134       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   135         do_quant bs AExists s T t'
   136       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
   137       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
   138       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
   139       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   140         if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
   141       | _ => do_term bs t
   142   in do_formula [] end
   143 
   144 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
   145 
   146 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
   147 fun conceal_bounds Ts t =
   148   subst_bounds (map (Free o apfst concealed_bound_name)
   149                     (0 upto length Ts - 1 ~~ Ts), t)
   150 fun reveal_bounds Ts =
   151   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   152                     (0 upto length Ts - 1 ~~ Ts))
   153 
   154 (* Removes the lambdas from an equation of the form "t = (%x. u)".
   155    (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
   156 fun extensionalize_term t =
   157   let
   158     fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
   159       | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
   160                                         Type (_, [_, res_T])]))
   161                     $ t2 $ Abs (var_s, var_T, t')) =
   162         if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
   163           let val var_t = Var ((var_s, j), var_T) in
   164             Const (s, T' --> T' --> res_T)
   165               $ betapply (t2, var_t) $ subst_bound (var_t, t')
   166             |> aux (j + 1)
   167           end
   168         else
   169           t
   170       | aux _ t = t
   171   in aux (maxidx_of_term t + 1) t end
   172 
   173 fun introduce_combinators_in_term ctxt kind t =
   174   let val thy = ProofContext.theory_of ctxt in
   175     if Meson.is_fol_term thy t then
   176       t
   177     else
   178       let
   179         fun aux Ts t =
   180           case t of
   181             @{const Not} $ t1 => @{const Not} $ aux Ts t1
   182           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   183             t0 $ Abs (s, T, aux (T :: Ts) t')
   184           | (t0 as Const (@{const_name All}, _)) $ t1 =>
   185             aux Ts (t0 $ eta_expand Ts t1 1)
   186           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   187             t0 $ Abs (s, T, aux (T :: Ts) t')
   188           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   189             aux Ts (t0 $ eta_expand Ts t1 1)
   190           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   191           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   192           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   193           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   194               $ t1 $ t2 =>
   195             t0 $ aux Ts t1 $ aux Ts t2
   196           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   197                    t
   198                  else
   199                    t |> conceal_bounds Ts
   200                      |> Envir.eta_contract
   201                      |> cterm_of thy
   202                      |> Meson_Clausify.introduce_combinators_in_cterm
   203                      |> prop_of |> Logic.dest_equals |> snd
   204                      |> reveal_bounds Ts
   205         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   206       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   207       handle THM _ =>
   208              (* A type variable of sort "{}" will make abstraction fail. *)
   209              if kind = Conjecture then HOLogic.false_const
   210              else HOLogic.true_const
   211   end
   212 
   213 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   214    same in Sledgehammer to prevent the discovery of unreplable proofs. *)
   215 fun freeze_term t =
   216   let
   217     fun aux (t $ u) = aux t $ aux u
   218       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   219       | aux (Var ((s, i), T)) =
   220         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   221       | aux t = t
   222   in t |> exists_subterm is_Var t ? aux end
   223 
   224 (* making fact and conjecture formulas *)
   225 fun make_formula ctxt eq_as_iff presimp name kind t =
   226   let
   227     val thy = ProofContext.theory_of ctxt
   228     val t = t |> Envir.beta_eta_contract
   229               |> transform_elim_term
   230               |> Object_Logic.atomize_term thy
   231     val need_trueprop = (fastype_of t = HOLogic.boolT)
   232     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   233               |> extensionalize_term
   234               |> presimp ? presimplify_term thy
   235               |> perhaps (try (HOLogic.dest_Trueprop))
   236               |> introduce_combinators_in_term ctxt kind
   237               |> kind <> Axiom ? freeze_term
   238     val (combformula, ctypes_sorts) = combformula_for_prop thy eq_as_iff t []
   239   in
   240     {name = name, combformula = combformula, kind = kind,
   241      ctypes_sorts = ctypes_sorts}
   242   end
   243 
   244 fun make_fact ctxt eq_as_iff presimp ((name, _), th) =
   245   case make_formula ctxt eq_as_iff presimp name Axiom (prop_of th) of
   246     {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
   247   | formula => SOME formula
   248 fun make_conjecture ctxt ts =
   249   let val last = length ts - 1 in
   250     map2 (fn j => make_formula ctxt true true (string_of_int j)
   251                                (if j = last then Conjecture else Hypothesis))
   252          (0 upto last) ts
   253   end
   254 
   255 (** Helper facts **)
   256 
   257 fun fold_formula f (AQuant (_, _, phi)) = fold_formula f phi
   258   | fold_formula f (AConn (_, phis)) = fold (fold_formula f) phis
   259   | fold_formula f (AAtom tm) = f tm
   260 
   261 fun count_term (ATerm ((s, _), tms)) =
   262   (if is_atp_variable s then I
   263    else Symtab.map_entry s (Integer.add 1))
   264   #> fold count_term tms
   265 fun count_formula x = fold_formula count_term x
   266 
   267 val init_counters =
   268   metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0)
   269   |> Symtab.make
   270 
   271 fun get_helper_facts ctxt explicit_forall type_sys formulas =
   272   let
   273     val no_dangerous_types = types_dangerous_types type_sys
   274     val ct = init_counters |> fold count_formula formulas
   275     fun is_used s = the (Symtab.lookup ct s) > 0
   276     fun dub c needs_full_types (th, j) =
   277       ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
   278         false), th)
   279     fun make_facts eq_as_iff = map_filter (make_fact ctxt eq_as_iff false)
   280   in
   281     (metis_helpers
   282      |> filter (is_used o fst)
   283      |> maps (fn (c, (needs_full_types, ths)) =>
   284                  if needs_full_types andalso not no_dangerous_types then
   285                    []
   286                  else
   287                    ths ~~ (1 upto length ths)
   288                    |> map (dub c needs_full_types)
   289                    |> make_facts (not needs_full_types)),
   290      if type_sys = Tags false then
   291        let
   292          fun var s = ATerm (`I s, [])
   293          fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
   294        in
   295          [Fof (helper_prefix ^ ascii_of "ti_ti", Axiom,
   296                AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
   297                |> explicit_forall ? close_universally)]
   298        end
   299      else
   300        [])
   301   end
   302 
   303 fun translate_atp_fact ctxt = `(make_fact ctxt true true)
   304 
   305 fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
   306   let
   307     val thy = ProofContext.theory_of ctxt
   308     val fact_ts = map (prop_of o snd o snd) rich_facts
   309     val (facts, fact_names) =
   310       rich_facts
   311       |> map_filter (fn (NONE, _) => NONE
   312                       | (SOME fact, (name, _)) => SOME (fact, name))
   313       |> ListPair.unzip
   314     (* Remove existing facts from the conjecture, as this can dramatically
   315        boost an ATP's performance (for some reason). *)
   316     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
   317     val goal_t = Logic.list_implies (hyp_ts, concl_t)
   318     val subs = tfree_classes_of_terms [goal_t]
   319     val supers = tvar_classes_of_terms fact_ts
   320     val tycons = type_consts_of_terms thy (goal_t :: fact_ts)
   321     (* TFrees in the conjecture; TVars in the facts *)
   322     val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
   323     val (supers', arity_clauses) =
   324       if type_sys = No_Types then ([], [])
   325       else make_arity_clauses thy tycons supers
   326     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   327   in
   328     (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
   329   end
   330 
   331 fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t])
   332 
   333 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   334   | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   335   | fo_term_for_combtyp (CombType (name, tys)) =
   336     ATerm (name, map fo_term_for_combtyp tys)
   337 
   338 fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   339     (true, ATerm (class, [ATerm (name, [])]))
   340   | fo_literal_for_type_literal (TyLitFree (class, name)) =
   341     (true, ATerm (class, [ATerm (name, [])]))
   342 
   343 fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   344 
   345 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
   346    considered dangerous because their "exhaust" properties can easily lead to
   347    unsound ATP proofs. The checks below are an (unsound) approximation of
   348    finiteness. *)
   349 
   350 fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true
   351   | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) =
   352     is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us
   353   | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false
   354 and is_type_dangerous ctxt (Type (s, Ts)) =
   355     is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts
   356   | is_type_dangerous _ _ = false
   357 and is_type_constr_dangerous ctxt s =
   358   let val thy = ProofContext.theory_of ctxt in
   359     case Datatype_Data.get_info thy s of
   360       SOME {descr, ...} =>
   361       forall (fn (_, (_, _, constrs)) =>
   362                  forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr
   363     | NONE =>
   364       case Typedef.get_info ctxt s of
   365         ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type
   366       | [] => true
   367   end
   368 
   369 fun is_combtyp_dangerous ctxt (CombType ((s, _), tys)) =
   370     (case strip_prefix_and_unascii type_const_prefix s of
   371        SOME s' => forall (is_combtyp_dangerous ctxt) tys andalso
   372                   is_type_constr_dangerous ctxt (invert_const s')
   373      | NONE => false)
   374   | is_combtyp_dangerous _ _ = false
   375 
   376 fun should_tag_with_type ctxt (Tags full_types) ty =
   377     full_types orelse is_combtyp_dangerous ctxt ty
   378   | should_tag_with_type _ _ _ = false
   379 
   380 val fname_table =
   381   [("c_False", (0, ("c_fFalse", @{const_name Metis.fFalse}))),
   382    ("c_True", (0, ("c_fTrue", @{const_name Metis.fTrue}))),
   383    ("c_Not", (1, ("c_fNot", @{const_name Metis.fNot}))),
   384    ("c_conj", (2, ("c_fconj", @{const_name Metis.fconj}))),
   385    ("c_disj", (2, ("c_fdisj", @{const_name Metis.fdisj}))),
   386    ("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))),
   387    ("equal", (2, ("c_fequal", @{const_name Metis.fequal})))]
   388 
   389 fun fo_term_for_combterm ctxt type_sys =
   390   let
   391     val thy = ProofContext.theory_of ctxt
   392     fun aux top_level u =
   393       let
   394         val (head, args) = strip_combterm_comb u
   395         val (x, ty_args) =
   396           case head of
   397             CombConst (name as (s, s'), _, ty_args) =>
   398             (case AList.lookup (op =) fname_table s of
   399                SOME (n, fname) =>
   400                (if top_level andalso length args = n then
   401                   case s of
   402                     "c_False" => ("$false", s')
   403                   | "c_True" => ("$true", s')
   404                   | _ => name
   405                 else
   406                   fname, [])
   407              | NONE =>
   408                case strip_prefix_and_unascii const_prefix s of
   409                  NONE => (name, ty_args)
   410                | SOME s'' =>
   411                  let
   412                    val s'' = invert_const s''
   413                    val ty_args =
   414                      if needs_type_args thy type_sys s'' then ty_args else []
   415                   in (name, ty_args) end)
   416           | CombVar (name, _) => (name, [])
   417           | CombApp _ => raise Fail "impossible \"CombApp\""
   418         val t =
   419           ATerm (x, map fo_term_for_combtyp ty_args @ map (aux false) args)
   420         val ty = combtyp_of u
   421     in
   422       t |> (if should_tag_with_type ctxt type_sys ty then
   423               tag_with_type (fo_term_for_combtyp ty)
   424             else
   425               I)
   426     end
   427   in aux true end
   428 
   429 fun formula_for_combformula ctxt type_sys =
   430   let
   431     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   432       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   433       | aux (AAtom tm) = AAtom (fo_term_for_combterm ctxt type_sys tm)
   434   in aux end
   435 
   436 fun formula_for_fact ctxt type_sys
   437                      ({combformula, ctypes_sorts, ...} : translated_formula) =
   438   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   439                 (atp_type_literals_for_types type_sys ctypes_sorts))
   440            (formula_for_combformula ctxt type_sys combformula)
   441 
   442 fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) =
   443   Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula)
   444 
   445 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   446                                                        superclass, ...}) =
   447   let val ty_arg = ATerm (("T", "T"), []) in
   448     Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
   449          AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   450                            AAtom (ATerm (superclass, [ty_arg]))]))
   451   end
   452 
   453 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   454     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   455   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   456     (false, ATerm (c, [ATerm (sort, [])]))
   457 
   458 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   459                                                 ...}) =
   460   Fof (arity_clause_prefix ^ ascii_of name, Axiom,
   461        mk_ahorn (map (formula_for_fo_literal o apfst not
   462                       o fo_literal_for_arity_literal) premLits)
   463                 (formula_for_fo_literal
   464                      (fo_literal_for_arity_literal conclLit)))
   465 
   466 fun problem_line_for_conjecture ctxt type_sys
   467         ({name, kind, combformula, ...} : translated_formula) =
   468   Fof (conjecture_prefix ^ name, kind,
   469        formula_for_combformula ctxt type_sys combformula)
   470 
   471 fun free_type_literals_for_conjecture type_sys
   472         ({ctypes_sorts, ...} : translated_formula) =
   473   ctypes_sorts |> atp_type_literals_for_types type_sys
   474                |> map fo_literal_for_type_literal
   475 
   476 fun problem_line_for_free_type j lit =
   477   Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
   478 fun problem_lines_for_free_types type_sys conjs =
   479   let
   480     val litss = map (free_type_literals_for_conjecture type_sys) conjs
   481     val lits = fold (union (op =)) litss []
   482   in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
   483 
   484 (** "hBOOL" and "hAPP" **)
   485 
   486 type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   487 
   488 fun consider_term top_level (ATerm ((s, _), ts)) =
   489   (if is_atp_variable s then
   490      I
   491    else
   492      let val n = length ts in
   493        Symtab.map_default
   494            (s, {min_arity = n, max_arity = 0, sub_level = false})
   495            (fn {min_arity, max_arity, sub_level} =>
   496                {min_arity = Int.min (n, min_arity),
   497                 max_arity = Int.max (n, max_arity),
   498                 sub_level = sub_level orelse not top_level})
   499      end)
   500   #> fold (consider_term (top_level andalso s = type_tag_name)) ts
   501 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   502   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   503   | consider_formula (AAtom tm) = consider_term true tm
   504 
   505 fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   506 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   507 
   508 (* needed for helper facts if the problem otherwise does not involve equality *)
   509 val equal_entry = ("equal", {min_arity = 2, max_arity = 2, sub_level = false})
   510 
   511 fun const_table_for_problem explicit_apply problem =
   512   if explicit_apply then
   513     NONE
   514   else
   515     SOME (Symtab.empty |> Symtab.default equal_entry |> consider_problem problem)
   516 
   517 fun min_arity_of thy type_sys NONE s =
   518     (if s = "equal" orelse s = type_tag_name orelse
   519         String.isPrefix type_const_prefix s orelse
   520         String.isPrefix class_prefix s then
   521        16383 (* large number *)
   522      else case strip_prefix_and_unascii const_prefix s of
   523        SOME s' => num_atp_type_args thy type_sys (invert_const s')
   524      | NONE => 0)
   525   | min_arity_of _ _ (SOME the_const_tab) s =
   526     case Symtab.lookup the_const_tab s of
   527       SOME ({min_arity, ...} : const_info) => min_arity
   528     | NONE => 0
   529 
   530 fun full_type_of (ATerm ((s, _), [ty, _])) =
   531     if s = type_tag_name then SOME ty else NONE
   532   | full_type_of _ = NONE
   533 
   534 fun list_hAPP_rev _ t1 [] = t1
   535   | list_hAPP_rev NONE t1 (t2 :: ts2) =
   536     ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   537   | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   538     case full_type_of t2 of
   539       SOME ty2 =>
   540       let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   541                            [ty2, ty]) in
   542         ATerm (`I "hAPP",
   543                [tag_with_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   544       end
   545     | NONE => list_hAPP_rev NONE t1 (t2 :: ts2)
   546 
   547 fun repair_applications_in_term thy type_sys const_tab =
   548   let
   549     fun aux opt_ty (ATerm (name as (s, _), ts)) =
   550       if s = type_tag_name then
   551         case ts of
   552           [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   553         | _ => raise Fail "malformed type tag"
   554       else
   555         let
   556           val ts = map (aux NONE) ts
   557           val (ts1, ts2) = chop (min_arity_of thy type_sys const_tab s) ts
   558         in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   559   in aux NONE end
   560 
   561 fun boolify t = ATerm (`I "hBOOL", [t])
   562 
   563 (* True if the constant ever appears outside of the top-level position in
   564    literals, or if it appears with different arities (e.g., because of different
   565    type instantiations). If false, the constant always receives all of its
   566    arguments and is used as a predicate. *)
   567 fun is_predicate NONE s =
   568     s = "equal" orelse s = "$false" orelse s = "$true" orelse
   569     String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
   570   | is_predicate (SOME the_const_tab) s =
   571     case Symtab.lookup the_const_tab s of
   572       SOME {min_arity, max_arity, sub_level} =>
   573       not sub_level andalso min_arity = max_arity
   574     | NONE => false
   575 
   576 fun repair_predicates_in_term pred_const_tab (t as ATerm ((s, _), ts)) =
   577   if s = type_tag_name then
   578     case ts of
   579       [_, t' as ATerm ((s', _), _)] =>
   580       if is_predicate pred_const_tab s' then t' else boolify t
   581     | _ => raise Fail "malformed type tag"
   582   else
   583     t |> not (is_predicate pred_const_tab s) ? boolify
   584 
   585 fun repair_formula thy explicit_forall type_sys const_tab =
   586   let
   587     val pred_const_tab = case type_sys of Tags _ => NONE | _ => const_tab
   588     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   589       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   590       | aux (AAtom tm) =
   591         AAtom (tm |> repair_applications_in_term thy type_sys const_tab
   592                   |> repair_predicates_in_term pred_const_tab)
   593   in aux #> explicit_forall ? close_universally end
   594 
   595 fun repair_problem_line thy explicit_forall type_sys const_tab
   596                         (Fof (ident, kind, phi)) =
   597   Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi)
   598 fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy
   599 
   600 fun dest_Fof (Fof z) = z
   601 
   602 val factsN = "Relevant facts"
   603 val class_relsN = "Class relationships"
   604 val aritiesN = "Arity declarations"
   605 val helpersN = "Helper facts"
   606 val conjsN = "Conjectures"
   607 val free_typesN = "Type variables"
   608 
   609 fun offset_of_heading_in_problem _ [] j = j
   610   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
   611     if heading = needle then j
   612     else offset_of_heading_in_problem needle problem (j + length lines)
   613 
   614 fun prepare_atp_problem ctxt readable_names explicit_forall type_sys
   615                         explicit_apply hyp_ts concl_t facts =
   616   let
   617     val thy = ProofContext.theory_of ctxt
   618     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   619       translate_formulas ctxt type_sys hyp_ts concl_t facts
   620     (* Reordering these might or might not confuse the proof reconstruction
   621        code or the SPASS Flotter hack. *)
   622     val problem =
   623       [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) facts),
   624        (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
   625        (aritiesN, map problem_line_for_arity_clause arity_clauses),
   626        (helpersN, []),
   627        (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
   628        (free_typesN, problem_lines_for_free_types type_sys conjs)]
   629     val const_tab = const_table_for_problem explicit_apply problem
   630     val problem =
   631       problem |> repair_problem thy explicit_forall type_sys const_tab
   632     val helper_lines =
   633       get_helper_facts ctxt explicit_forall type_sys
   634                        (maps (map (#3 o dest_Fof) o snd) problem)
   635       |>> map (problem_line_for_fact ctxt helper_prefix type_sys
   636                #> repair_problem_line thy explicit_forall type_sys const_tab)
   637       |> op @
   638     val (problem, pool) =
   639       problem |> AList.update (op =) (helpersN, helper_lines)
   640               |> nice_atp_problem readable_names
   641   in
   642     (problem,
   643      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   644      offset_of_heading_in_problem conjsN problem 0,
   645      fact_names |> Vector.fromList)
   646   end
   647 
   648 (* FUDGE *)
   649 val conj_weight = 0.0
   650 val hyp_weight = 0.05
   651 val fact_min_weight = 0.1
   652 val fact_max_weight = 1.0
   653 
   654 fun add_term_weights weight (ATerm (s, tms)) =
   655   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   656   #> fold (add_term_weights weight) tms
   657 fun add_problem_line_weights weight (Fof (_, _, phi)) =
   658   fold_formula (add_term_weights weight) phi
   659 
   660 fun add_conjectures_weights [] = I
   661   | add_conjectures_weights conjs =
   662     let val (hyps, conj) = split_last conjs in
   663       add_problem_line_weights conj_weight conj
   664       #> fold (add_problem_line_weights hyp_weight) hyps
   665     end
   666 
   667 fun add_facts_weights facts =
   668   let
   669     val num_facts = length facts
   670     fun weight_of j =
   671       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
   672                         / Real.fromInt num_facts
   673   in
   674     map weight_of (0 upto num_facts - 1) ~~ facts
   675     |> fold (uncurry add_problem_line_weights)
   676   end
   677 
   678 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
   679 fun atp_problem_weights problem =
   680   Symtab.empty
   681   |> add_conjectures_weights (these (AList.lookup (op =) problem conjsN))
   682   |> add_facts_weights (these (AList.lookup (op =) problem factsN))
   683   |> Symtab.dest
   684   |> sort (prod_ord Real.compare string_ord o pairself swap)
   685 
   686 end;