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