src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
author blanchet
Tue Sep 14 19:38:44 2010 +0200 (2010-09-14)
changeset 39370 f8292d3020db
parent 39005 42fcb25de082
child 39452 70a57e40f795
permissions -rw-r--r--
use same hack as in "Async_Manager" to work around Proof General bug
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Translation of HOL to FOL.
     7 *)
     8 
     9 signature SLEDGEHAMMER_TRANSLATE =
    10 sig
    11   type 'a problem = 'a ATP_Problem.problem
    12   type fol_formula
    13 
    14   val axiom_prefix : string
    15   val conjecture_prefix : string
    16   val helper_prefix : string
    17   val class_rel_clause_prefix : string
    18   val arity_clause_prefix : string
    19   val tfrees_name : string
    20   val prepare_axiom :
    21     Proof.context -> (string * 'a) * thm
    22     -> term * ((string * 'a) * fol_formula) option
    23   val prepare_problem :
    24     Proof.context -> bool -> bool -> bool -> bool -> term list -> term
    25     -> (term * ((string * 'a) * fol_formula) option) list
    26     -> string problem * string Symtab.table * int * (string * 'a) list vector
    27 end;
    28 
    29 structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
    30 struct
    31 
    32 open ATP_Problem
    33 open Metis_Clauses
    34 open Sledgehammer_Util
    35 
    36 val axiom_prefix = "ax_"
    37 val conjecture_prefix = "conj_"
    38 val helper_prefix = "help_"
    39 val class_rel_clause_prefix = "clrel_";
    40 val arity_clause_prefix = "arity_"
    41 val tfrees_name = "tfrees"
    42 
    43 (* Freshness almost guaranteed! *)
    44 val sledgehammer_weak_prefix = "Sledgehammer:"
    45 
    46 type fol_formula =
    47   {name: string,
    48    kind: kind,
    49    combformula: (name, combterm) formula,
    50    ctypes_sorts: typ list}
    51 
    52 fun mk_anot phi = AConn (ANot, [phi])
    53 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    54 fun mk_ahorn [] phi = phi
    55   | mk_ahorn (phi :: phis) psi =
    56     AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
    57 
    58 fun combformula_for_prop thy =
    59   let
    60     val do_term = combterm_from_term thy
    61     fun do_quant bs q s T t' =
    62       let val s = Name.variant (map fst bs) s in
    63         do_formula ((s, T) :: bs) t'
    64         #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
    65       end
    66     and do_conn bs c t1 t2 =
    67       do_formula bs t1 ##>> do_formula bs t2
    68       #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
    69     and do_formula bs t =
    70       case t of
    71         @{const Not} $ t1 =>
    72         do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
    73       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
    74         do_quant bs AForall s T t'
    75       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
    76         do_quant bs AExists s T t'
    77       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
    78       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
    79       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
    80       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
    81         do_conn bs AIff t1 t2
    82       | _ => (fn ts => do_term bs (Envir.eta_contract t)
    83                        |>> AAtom ||> union (op =) ts)
    84   in do_formula [] end
    85 
    86 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
    87 
    88 fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
    89 fun conceal_bounds Ts t =
    90   subst_bounds (map (Free o apfst concealed_bound_name)
    91                     (0 upto length Ts - 1 ~~ Ts), t)
    92 fun reveal_bounds Ts =
    93   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
    94                     (0 upto length Ts - 1 ~~ Ts))
    95 
    96 (* Removes the lambdas from an equation of the form "t = (%x. u)".
    97    (Cf. "extensionalize_theorem" in "Clausifier".) *)
    98 fun extensionalize_term t =
    99   let
   100     fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
   101       | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
   102                                         Type (_, [_, res_T])]))
   103                     $ t2 $ Abs (var_s, var_T, t')) =
   104         if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
   105           let val var_t = Var ((var_s, j), var_T) in
   106             Const (s, T' --> T' --> res_T)
   107               $ betapply (t2, var_t) $ subst_bound (var_t, t')
   108             |> aux (j + 1)
   109           end
   110         else
   111           t
   112       | aux _ t = t
   113   in aux (maxidx_of_term t + 1) t end
   114 
   115 fun introduce_combinators_in_term ctxt kind t =
   116   let val thy = ProofContext.theory_of ctxt in
   117     if Meson.is_fol_term thy t then
   118       t
   119     else
   120       let
   121         fun aux Ts t =
   122           case t of
   123             @{const Not} $ t1 => @{const Not} $ aux Ts t1
   124           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   125             t0 $ Abs (s, T, aux (T :: Ts) t')
   126           | (t0 as Const (@{const_name All}, _)) $ t1 =>
   127             aux Ts (t0 $ eta_expand Ts t1 1)
   128           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   129             t0 $ Abs (s, T, aux (T :: Ts) t')
   130           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   131             aux Ts (t0 $ eta_expand Ts t1 1)
   132           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   133           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   134           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   135           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   136               $ t1 $ t2 =>
   137             t0 $ aux Ts t1 $ aux Ts t2
   138           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   139                    t
   140                  else
   141                    t |> conceal_bounds Ts
   142                      |> Envir.eta_contract
   143                      |> cterm_of thy
   144                      |> Clausifier.introduce_combinators_in_cterm
   145                      |> prop_of |> Logic.dest_equals |> snd
   146                      |> reveal_bounds Ts
   147         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   148       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   149       handle THM _ =>
   150              (* A type variable of sort "{}" will make abstraction fail. *)
   151              if kind = Conjecture then HOLogic.false_const
   152              else HOLogic.true_const
   153   end
   154 
   155 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   156    same in Sledgehammer to prevent the discovery of unreplable proofs. *)
   157 fun freeze_term t =
   158   let
   159     fun aux (t $ u) = aux t $ aux u
   160       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   161       | aux (Var ((s, i), T)) =
   162         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   163       | aux t = t
   164   in t |> exists_subterm is_Var t ? aux end
   165 
   166 (* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
   167     it leaves metaequalities over "prop"s alone. *)
   168 val atomize_term =
   169   let
   170     fun aux (@{const Trueprop} $ t1) = t1
   171       | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
   172         HOLogic.all_const T $ Abs (s, T, aux t')
   173       | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
   174       | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
   175         HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
   176       | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
   177         HOLogic.eq_const T $ t1 $ t2
   178       | aux _ = raise Fail "aux"
   179   in perhaps (try aux) end
   180 
   181 (* making axiom and conjecture formulas *)
   182 fun make_formula ctxt presimp name kind t =
   183   let
   184     val thy = ProofContext.theory_of ctxt
   185     val t = t |> Envir.beta_eta_contract
   186               |> transform_elim_term
   187               |> atomize_term
   188     val need_trueprop = (fastype_of t = HOLogic.boolT)
   189     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   190               |> extensionalize_term
   191               |> presimp ? presimplify_term thy
   192               |> perhaps (try (HOLogic.dest_Trueprop))
   193               |> introduce_combinators_in_term ctxt kind
   194               |> kind <> Axiom ? freeze_term
   195     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   196   in
   197     {name = name, combformula = combformula, kind = kind,
   198      ctypes_sorts = ctypes_sorts}
   199   end
   200 
   201 fun make_axiom ctxt presimp ((name, loc), th) =
   202   case make_formula ctxt presimp name Axiom (prop_of th) of
   203     {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
   204   | formula => SOME ((name, loc), formula)
   205 fun make_conjecture ctxt ts =
   206   let val last = length ts - 1 in
   207     map2 (fn j => make_formula ctxt true (Int.toString j)
   208                                (if j = last then Conjecture else Hypothesis))
   209          (0 upto last) ts
   210   end
   211 
   212 (** Helper facts **)
   213 
   214 fun count_combterm (CombConst ((s, _), _, _)) =
   215     Symtab.map_entry s (Integer.add 1)
   216   | count_combterm (CombVar _) = I
   217   | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
   218 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   219   | count_combformula (AConn (_, phis)) = fold count_combformula phis
   220   | count_combformula (AAtom tm) = count_combterm tm
   221 fun count_fol_formula ({combformula, ...} : fol_formula) =
   222   count_combformula combformula
   223 
   224 val optional_helpers =
   225   [(["c_COMBI"], @{thms COMBI_def}),
   226    (["c_COMBK"], @{thms COMBK_def}),
   227    (["c_COMBB"], @{thms COMBB_def}),
   228    (["c_COMBC"], @{thms COMBC_def}),
   229    (["c_COMBS"], @{thms COMBS_def})]
   230 val optional_typed_helpers =
   231   [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
   232    (["c_If"], @{thms if_True if_False})]
   233 val mandatory_helpers = @{thms fequal_def}
   234 
   235 val init_counters =
   236   [optional_helpers, optional_typed_helpers] |> maps (maps fst)
   237   |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
   238 
   239 fun get_helper_facts ctxt is_FO full_types conjectures axioms =
   240   let
   241     val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
   242     fun is_needed c = the (Symtab.lookup ct c) > 0
   243     fun baptize th = ((Thm.get_name_hint th, false), th)
   244   in
   245     (optional_helpers
   246      |> full_types ? append optional_typed_helpers
   247      |> maps (fn (ss, ths) =>
   248                  if exists is_needed ss then map baptize ths else [])) @
   249     (if is_FO then [] else map baptize mandatory_helpers)
   250     |> map_filter (Option.map snd o make_axiom ctxt false)
   251   end
   252 
   253 fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
   254 
   255 fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
   256   let
   257     val thy = ProofContext.theory_of ctxt
   258     val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
   259     (* Remove existing axioms from the conjecture, as this can dramatically
   260        boost an ATP's performance (for some reason). *)
   261     val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
   262     val goal_t = Logic.list_implies (hyp_ts, concl_t)
   263     val is_FO = Meson.is_fol_term thy goal_t
   264     val subs = tfree_classes_of_terms [goal_t]
   265     val supers = tvar_classes_of_terms axiom_ts
   266     val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
   267     (* TFrees in the conjecture; TVars in the axioms *)
   268     val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
   269     val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
   270     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
   271     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   272     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   273   in
   274     (axiom_names |> map single |> Vector.fromList,
   275      (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
   276   end
   277 
   278 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   279 
   280 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   281   | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   282   | fo_term_for_combtyp (CombType (name, tys)) =
   283     ATerm (name, map fo_term_for_combtyp tys)
   284 
   285 fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   286     (true, ATerm (class, [ATerm (name, [])]))
   287   | fo_literal_for_type_literal (TyLitFree (class, name)) =
   288     (true, ATerm (class, [ATerm (name, [])]))
   289 
   290 fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   291 
   292 fun fo_term_for_combterm full_types =
   293   let
   294     fun aux top_level u =
   295       let
   296         val (head, args) = strip_combterm_comb u
   297         val (x, ty_args) =
   298           case head of
   299             CombConst (name as (s, s'), _, ty_args) =>
   300             let val ty_args = if full_types then [] else ty_args in
   301               if s = "equal" then
   302                 if top_level andalso length args = 2 then (name, [])
   303                 else (("c_fequal", @{const_name fequal}), ty_args)
   304               else if top_level then
   305                 case s of
   306                   "c_False" => (("$false", s'), [])
   307                 | "c_True" => (("$true", s'), [])
   308                 | _ => (name, ty_args)
   309               else
   310                 (name, ty_args)
   311             end
   312           | CombVar (name, _) => (name, [])
   313           | CombApp _ => raise Fail "impossible \"CombApp\""
   314         val t = ATerm (x, map fo_term_for_combtyp ty_args @
   315                           map (aux false) args)
   316     in
   317       if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   318     end
   319   in aux true end
   320 
   321 fun formula_for_combformula full_types =
   322   let
   323     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   324       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   325       | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
   326   in aux end
   327 
   328 fun formula_for_axiom full_types
   329                       ({combformula, ctypes_sorts, ...} : fol_formula) =
   330   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   331                 (type_literals_for_types ctypes_sorts))
   332            (formula_for_combformula full_types combformula)
   333 
   334 fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
   335   Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
   336 
   337 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   338                                                        superclass, ...}) =
   339   let val ty_arg = ATerm (("T", "T"), []) in
   340     Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
   341          AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   342                            AAtom (ATerm (superclass, [ty_arg]))]))
   343   end
   344 
   345 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   346     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   347   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   348     (false, ATerm (c, [ATerm (sort, [])]))
   349 
   350 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   351                                                 ...}) =
   352   Fof (arity_clause_prefix ^ ascii_of name, Axiom,
   353        mk_ahorn (map (formula_for_fo_literal o apfst not
   354                       o fo_literal_for_arity_literal) premLits)
   355                 (formula_for_fo_literal
   356                      (fo_literal_for_arity_literal conclLit)))
   357 
   358 fun problem_line_for_conjecture full_types
   359                                 ({name, kind, combformula, ...} : fol_formula) =
   360   Fof (conjecture_prefix ^ name, kind,
   361        formula_for_combformula full_types combformula)
   362 
   363 fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
   364   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   365 
   366 fun problem_line_for_free_type lit =
   367   Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit)
   368 fun problem_lines_for_free_types conjectures =
   369   let
   370     val litss = map free_type_literals_for_conjecture conjectures
   371     val lits = fold (union (op =)) litss []
   372   in map problem_line_for_free_type lits end
   373 
   374 (** "hBOOL" and "hAPP" **)
   375 
   376 type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   377 
   378 fun consider_term top_level (ATerm ((s, _), ts)) =
   379   (if is_tptp_variable s then
   380      I
   381    else
   382      let val n = length ts in
   383        Symtab.map_default
   384            (s, {min_arity = n, max_arity = 0, sub_level = false})
   385            (fn {min_arity, max_arity, sub_level} =>
   386                {min_arity = Int.min (n, min_arity),
   387                 max_arity = Int.max (n, max_arity),
   388                 sub_level = sub_level orelse not top_level})
   389      end)
   390   #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
   391 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   392   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   393   | consider_formula (AAtom tm) = consider_term true tm
   394 
   395 fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   396 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   397 
   398 fun const_table_for_problem explicit_apply problem =
   399   if explicit_apply then NONE
   400   else SOME (Symtab.empty |> consider_problem problem)
   401 
   402 fun min_arity_of thy full_types NONE s =
   403     (if s = "equal" orelse s = type_wrapper_name orelse
   404         String.isPrefix type_const_prefix s orelse
   405         String.isPrefix class_prefix s then
   406        16383 (* large number *)
   407      else if full_types then
   408        0
   409      else case strip_prefix_and_unascii const_prefix s of
   410        SOME s' => num_type_args thy (invert_const s')
   411      | NONE => 0)
   412   | min_arity_of _ _ (SOME the_const_tab) s =
   413     case Symtab.lookup the_const_tab s of
   414       SOME ({min_arity, ...} : const_info) => min_arity
   415     | NONE => 0
   416 
   417 fun full_type_of (ATerm ((s, _), [ty, _])) =
   418     if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
   419   | full_type_of _ = raise Fail "expected type wrapper"
   420 
   421 fun list_hAPP_rev _ t1 [] = t1
   422   | list_hAPP_rev NONE t1 (t2 :: ts2) =
   423     ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   424   | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   425     let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   426                          [full_type_of t2, ty]) in
   427       ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   428     end
   429 
   430 fun repair_applications_in_term thy full_types const_tab =
   431   let
   432     fun aux opt_ty (ATerm (name as (s, _), ts)) =
   433       if s = type_wrapper_name then
   434         case ts of
   435           [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   436         | _ => raise Fail "malformed type wrapper"
   437       else
   438         let
   439           val ts = map (aux NONE) ts
   440           val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   441         in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   442   in aux NONE end
   443 
   444 fun boolify t = ATerm (`I "hBOOL", [t])
   445 
   446 (* True if the constant ever appears outside of the top-level position in
   447    literals, or if it appears with different arities (e.g., because of different
   448    type instantiations). If false, the constant always receives all of its
   449    arguments and is used as a predicate. *)
   450 fun is_predicate NONE s =
   451     s = "equal" orelse s = "$false" orelse s = "$true" orelse
   452     String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
   453   | is_predicate (SOME the_const_tab) s =
   454     case Symtab.lookup the_const_tab s of
   455       SOME {min_arity, max_arity, sub_level} =>
   456       not sub_level andalso min_arity = max_arity
   457     | NONE => false
   458 
   459 fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
   460   if s = type_wrapper_name then
   461     case ts of
   462       [_, t' as ATerm ((s', _), _)] =>
   463       if is_predicate const_tab s' then t' else boolify t
   464     | _ => raise Fail "malformed type wrapper"
   465   else
   466     t |> not (is_predicate const_tab s) ? boolify
   467 
   468 fun close_universally phi =
   469   let
   470     fun term_vars bounds (ATerm (name as (s, _), tms)) =
   471         (is_tptp_variable s andalso not (member (op =) bounds name))
   472           ? insert (op =) name
   473         #> fold (term_vars bounds) tms
   474     fun formula_vars bounds (AQuant (_, xs, phi)) =
   475         formula_vars (xs @ bounds) phi
   476       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   477       | formula_vars bounds (AAtom tm) = term_vars bounds tm
   478   in
   479     case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   480   end
   481 
   482 fun repair_formula thy explicit_forall full_types const_tab =
   483   let
   484     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   485       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   486       | aux (AAtom tm) =
   487         AAtom (tm |> repair_applications_in_term thy full_types const_tab
   488                   |> repair_predicates_in_term const_tab)
   489   in aux #> explicit_forall ? close_universally end
   490 
   491 fun repair_problem_line thy explicit_forall full_types const_tab
   492                         (Fof (ident, kind, phi)) =
   493   Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   494 fun repair_problem_with_const_table thy =
   495   map o apsnd o map ooo repair_problem_line thy
   496 
   497 fun repair_problem thy explicit_forall full_types explicit_apply problem =
   498   repair_problem_with_const_table thy explicit_forall full_types
   499       (const_table_for_problem explicit_apply problem) problem
   500 
   501 fun prepare_problem ctxt readable_names explicit_forall full_types
   502                     explicit_apply hyp_ts concl_t axioms =
   503   let
   504     val thy = ProofContext.theory_of ctxt
   505     val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
   506                        arity_clauses)) =
   507       prepare_formulas ctxt full_types hyp_ts concl_t axioms
   508     val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
   509     val helper_lines =
   510       map (problem_line_for_fact helper_prefix full_types) helper_facts
   511     val conjecture_lines =
   512       map (problem_line_for_conjecture full_types) conjectures
   513     val tfree_lines = problem_lines_for_free_types conjectures
   514     val class_rel_lines =
   515       map problem_line_for_class_rel_clause class_rel_clauses
   516     val arity_lines = map problem_line_for_arity_clause arity_clauses
   517     (* Reordering these might or might not confuse the proof reconstruction
   518        code or the SPASS Flotter hack. *)
   519     val problem =
   520       [("Relevant facts", axiom_lines),
   521        ("Class relationships", class_rel_lines),
   522        ("Arity declarations", arity_lines),
   523        ("Helper facts", helper_lines),
   524        ("Conjectures", conjecture_lines),
   525        ("Type variables", tfree_lines)]
   526       |> repair_problem thy explicit_forall full_types explicit_apply
   527     val (problem, pool) = nice_tptp_problem readable_names problem
   528     val conjecture_offset =
   529       length axiom_lines + length class_rel_lines + length arity_lines
   530       + length helper_lines
   531   in
   532     (problem,
   533      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   534      conjecture_offset, axiom_names)
   535   end
   536 
   537 end;