src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
author blanchet
Wed Jun 02 17:19:44 2010 +0200 (2010-06-02)
changeset 37323 2f2f0d246d0f
parent 36966 adc11fb3f3aa
child 37399 34f080a12063
permissions -rw-r--r--
handle Vampire's definitions smoothly
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
     2     Author:     Jia Meng, NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 FOL clauses translated from HOL formulae.
     6 *)
     7 
     8 signature SLEDGEHAMMER_HOL_CLAUSE =
     9 sig
    10   type name = Sledgehammer_FOL_Clause.name
    11   type name_pool = Sledgehammer_FOL_Clause.name_pool
    12   type kind = Sledgehammer_FOL_Clause.kind
    13   type fol_type = Sledgehammer_FOL_Clause.fol_type
    14   type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
    15   type arity_clause = Sledgehammer_FOL_Clause.arity_clause
    16   type axiom_name = string
    17   type polarity = bool
    18   type hol_clause_id = int
    19 
    20   datatype combterm =
    21     CombConst of name * fol_type * fol_type list (* Const and Free *) |
    22     CombVar of name * fol_type |
    23     CombApp of combterm * combterm
    24   datatype literal = Literal of polarity * combterm
    25   datatype hol_clause =
    26     HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
    27                   kind: kind, literals: literal list, ctypes_sorts: typ list}
    28 
    29   val type_of_combterm : combterm -> fol_type
    30   val strip_combterm_comb : combterm -> combterm * combterm list
    31   val literals_of_term : theory -> term -> literal list * typ list
    32   exception TRIVIAL
    33   val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
    34   val make_axiom_clauses : bool -> theory ->
    35        (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
    36   val type_wrapper_name : string
    37   val get_helper_clauses : bool -> theory -> bool ->
    38        hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
    39        hol_clause list
    40   val write_tptp_file : bool -> bool -> bool -> Path.T ->
    41     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    42     classrel_clause list * arity_clause list -> name_pool option * int
    43   val write_dfg_file : bool -> bool -> Path.T ->
    44     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    45     classrel_clause list * arity_clause list -> name_pool option * int
    46 end
    47 
    48 structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    49 struct
    50 
    51 open Sledgehammer_Util
    52 open Sledgehammer_FOL_Clause
    53 open Sledgehammer_Fact_Preprocessor
    54 
    55 fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
    56 
    57 (*True if the constant ever appears outside of the top-level position in literals.
    58   If false, the constant always receives all of its arguments and is used as a predicate.*)
    59 fun needs_hBOOL explicit_apply const_needs_hBOOL c =
    60   explicit_apply orelse
    61     the_default false (Symtab.lookup const_needs_hBOOL c);
    62 
    63 
    64 (******************************************************)
    65 (* data types for typed combinator expressions        *)
    66 (******************************************************)
    67 
    68 type axiom_name = string;
    69 type polarity = bool;
    70 type hol_clause_id = int;
    71 
    72 datatype combterm =
    73   CombConst of name * fol_type * fol_type list (* Const and Free *) |
    74   CombVar of name * fol_type |
    75   CombApp of combterm * combterm
    76 
    77 datatype literal = Literal of polarity * combterm;
    78 
    79 datatype hol_clause =
    80   HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
    81                 kind: kind, literals: literal list, ctypes_sorts: typ list};
    82 
    83 
    84 (*********************************************************************)
    85 (* convert a clause with type Term.term to a clause with type clause *)
    86 (*********************************************************************)
    87 
    88 fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
    89       (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
    90   | isFalse _ = false;
    91 
    92 fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
    93       (pol andalso c = "c_True") orelse
    94       (not pol andalso c = "c_False")
    95   | isTrue _ = false;
    96 
    97 fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
    98 
    99 fun type_of dfg (Type (a, Ts)) =
   100     let val (folTypes,ts) = types_of dfg Ts in
   101       (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts)
   102     end
   103   | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
   104   | type_of _ (tp as TVar (x, _)) =
   105     (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
   106 and types_of dfg Ts =
   107       let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
   108       in  (folTyps, union_all ts)  end;
   109 
   110 (* same as above, but no gathering of sort information *)
   111 fun simp_type_of dfg (Type (a, Ts)) =
   112       TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts)
   113   | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a)
   114   | simp_type_of _ (TVar (x, _)) =
   115     TyVar (make_schematic_type_var x, string_of_indexname x);
   116 
   117 
   118 fun const_type_of dfg thy (c,t) =
   119       let val (tp,ts) = type_of dfg t
   120       in  (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
   121 
   122 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   123 fun combterm_of dfg thy (Const(c,t)) =
   124       let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
   125           val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
   126       in  (c',ts)  end
   127   | combterm_of dfg _ (Free(v,t)) =
   128       let val (tp,ts) = type_of dfg t
   129           val v' = CombConst (`make_fixed_var v, tp, [])
   130       in  (v',ts)  end
   131   | combterm_of dfg _ (Var(v,t)) =
   132       let val (tp,ts) = type_of dfg t
   133           val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
   134       in  (v',ts)  end
   135   | combterm_of dfg thy (P $ Q) =
   136       let val (P',tsP) = combterm_of dfg thy P
   137           val (Q',tsQ) = combterm_of dfg thy Q
   138       in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
   139   | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
   140 
   141 fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
   142   | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
   143 
   144 fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
   145   | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
   146       literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
   147   | literals_of_term1 dfg thy (lits,ts) P =
   148       let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
   149       in
   150           (Literal(pol,pred)::lits, union (op =) ts ts')
   151       end;
   152 
   153 fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
   154 val literals_of_term = literals_of_term_dfg false;
   155 
   156 (* Trivial problem, which resolution cannot handle (empty clause) *)
   157 exception TRIVIAL;
   158 
   159 (* making axiom and conjecture clauses *)
   160 fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
   161     let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
   162     in
   163         if forall isFalse lits then
   164             raise TRIVIAL
   165         else
   166             HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
   167                        kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
   168     end;
   169 
   170 
   171 fun add_axiom_clause dfg thy (th, (name, id)) =
   172   let val cls = make_clause dfg thy (id, name, Axiom, th) in
   173     not (isTaut cls) ? cons (name, cls)
   174   end
   175 
   176 fun make_axiom_clauses dfg thy clauses =
   177   fold (add_axiom_clause dfg thy) clauses []
   178 
   179 fun make_conjecture_clauses_aux _ _ _ [] = []
   180   | make_conjecture_clauses_aux dfg thy n (th::ths) =
   181       make_clause dfg thy (n,"conjecture", Conjecture, th) ::
   182       make_conjecture_clauses_aux dfg thy (n+1) ths;
   183 
   184 fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
   185 
   186 
   187 (**********************************************************************)
   188 (* convert clause into ATP specific formats:                          *)
   189 (* TPTP used by Vampire and E                                         *)
   190 (* DFG used by SPASS                                                  *)
   191 (**********************************************************************)
   192 
   193 (*Result of a function type; no need to check that the argument type matches.*)
   194 fun result_type (TyConstr (_, [_, tp2])) = tp2
   195   | result_type _ = raise Fail "non-function type"
   196 
   197 fun type_of_combterm (CombConst (_, tp, _)) = tp
   198   | type_of_combterm (CombVar (_, tp)) = tp
   199   | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
   200 
   201 (*gets the head of a combinator application, along with the list of arguments*)
   202 fun strip_combterm_comb u =
   203     let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   204         |   stripc  x =  x
   205     in  stripc(u,[])  end;
   206 
   207 val type_wrapper_name = "ti"
   208 
   209 fun head_needs_hBOOL explicit_apply const_needs_hBOOL
   210                      (CombConst ((c, _), _, _)) =
   211     needs_hBOOL explicit_apply const_needs_hBOOL c
   212   | head_needs_hBOOL _ _ _ = true
   213 
   214 fun wrap_type full_types (s, ty) pool =
   215   if full_types then
   216     let val (s', pool) = string_of_fol_type ty pool in
   217       (type_wrapper_name ^ paren_pack [s, s'], pool)
   218     end
   219   else
   220     (s, pool)
   221 
   222 fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
   223   if head_needs_hBOOL explicit_apply cnh head then
   224     wrap_type full_types (s, tp)
   225   else
   226     pair s
   227 
   228 fun apply ss = "hAPP" ^ paren_pack ss;
   229 
   230 fun rev_apply (v, []) = v
   231   | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
   232 
   233 fun string_apply (v, args) = rev_apply (v, rev args);
   234 
   235 (* Apply an operator to the argument strings, using either the "apply" operator
   236    or direct function application. *)
   237 fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
   238                           pool =
   239     let
   240       val s = if s = "equal" then "c_fequal" else s
   241       val nargs = min_arity_of cma s
   242       val args1 = List.take (args, nargs)
   243         handle Subscript =>
   244                raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
   245                            " but is applied to " ^ commas (map quote args))
   246       val args2 = List.drop (args, nargs)
   247       val (targs, pool) = if full_types then ([], pool)
   248                           else pool_map string_of_fol_type tvars pool
   249       val (s, pool) = nice_name (s, s') pool
   250     in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
   251   | string_of_application _ _ (CombVar (name, _), args) pool =
   252     nice_name name pool |>> (fn s => string_apply (s, args))
   253 
   254 fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t
   255                        pool =
   256   let
   257     val (head, args) = strip_combterm_comb t
   258     val (ss, pool) = pool_map (string_of_combterm params) args pool
   259     val (s, pool) = string_of_application full_types cma (head, ss) pool
   260   in
   261     wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t)
   262                  pool
   263   end
   264 
   265 (*Boolean-valued terms are here converted to literals.*)
   266 fun boolify params c =
   267   string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
   268 
   269 fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
   270   case t of
   271     (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
   272     (* DFG only: new TPTP prefers infix equality *)
   273     pool_map (string_of_combterm params) [t1, t2]
   274     #>> prefix "equal" o paren_pack
   275   | _ =>
   276     case #1 (strip_combterm_comb t) of
   277       CombConst ((s, _), _, _) =>
   278       (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
   279           params t
   280     | _ => boolify params t
   281 
   282 
   283 (*** TPTP format ***)
   284 
   285 fun tptp_of_equality params pos (t1, t2) =
   286   pool_map (string_of_combterm params) [t1, t2]
   287   #>> space_implode (if pos then " = " else " != ")
   288 
   289 fun tptp_literal params
   290         (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
   291                                          t2))) =
   292     tptp_of_equality params pos (t1, t2)
   293   | tptp_literal params (Literal (pos, pred)) =
   294     string_of_predicate params pred #>> tptp_sign pos
   295  
   296 (* Given a clause, returns its literals paired with a list of literals
   297    concerning TFrees; the latter should only occur in conjecture clauses. *)
   298 fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
   299                        pool =
   300   let
   301     val (lits, pool) = pool_map (tptp_literal params) literals pool
   302     val (tylits, pool) = pool_map (tptp_of_type_literal pos)
   303                                   (type_literals_for_types ctypes_sorts) pool
   304   in ((lits, tylits), pool) end
   305 
   306 fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
   307                 pool =
   308 let
   309     val ((lits, tylits), pool) =
   310       tptp_type_literals params (kind = Conjecture) cls pool
   311   in
   312     ((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool)
   313   end
   314 
   315 
   316 (*** DFG format ***)
   317 
   318 fun dfg_literal params (Literal (pos, pred)) =
   319   string_of_predicate params pred #>> dfg_sign pos
   320 
   321 fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
   322   pool_map (dfg_literal params) literals
   323   #>> rpair (map (dfg_of_type_literal pos)
   324                  (type_literals_for_types ctypes_sorts))
   325 
   326 fun get_uvars (CombConst _) vars pool = (vars, pool)
   327   | get_uvars (CombVar (name, _)) vars pool =
   328     nice_name name pool |>> (fn var => var :: vars)
   329   | get_uvars (CombApp (P, Q)) vars pool =
   330     let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end
   331 
   332 fun get_uvars_l (Literal (_, c)) = get_uvars c [];
   333 
   334 fun dfg_vars (HOLClause {literals, ...}) =
   335   pool_map get_uvars_l literals #>> union_all
   336 
   337 fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind,
   338                                          ctypes_sorts, ...}) pool =
   339   let
   340     val ((lits, tylits), pool) =
   341       dfg_type_literals params (kind = Conjecture) cls pool
   342     val (vars, pool) = dfg_vars cls pool
   343     val tvars = get_tvar_strs ctypes_sorts
   344   in
   345     ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars),
   346       tylits), pool)
   347   end
   348 
   349 
   350 (** For DFG format: accumulate function and predicate declarations **)
   351 
   352 fun add_types tvars = fold add_fol_type_funcs tvars
   353 
   354 fun add_decls (full_types, explicit_apply, cma, cnh)
   355               (CombConst ((c, _), ctp, tvars)) (funcs, preds) =
   356       (if c = "equal" then
   357          (add_types tvars funcs, preds)
   358        else
   359          let val arity = min_arity_of cma c
   360              val ntys = if not full_types then length tvars else 0
   361              val addit = Symtab.update(c, arity + ntys)
   362          in
   363              if needs_hBOOL explicit_apply cnh c then
   364                (add_types tvars (addit funcs), preds)
   365              else
   366                (add_types tvars funcs, addit preds)
   367          end) |>> full_types ? add_fol_type_funcs ctp
   368   | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
   369       (add_fol_type_funcs ctp funcs, preds)
   370   | add_decls params (CombApp (P, Q)) decls =
   371       decls |> add_decls params P |> add_decls params Q
   372 
   373 fun add_literal_decls params (Literal (_, c)) = add_decls params c
   374 
   375 fun add_clause_decls params (HOLClause {literals, ...}) decls =
   376     fold (add_literal_decls params) literals decls
   377     handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
   378 
   379 fun decls_of_clauses params clauses arity_clauses =
   380   let val functab =
   381         init_functab |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
   382                                             ("tc_bool", 0)]
   383       val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
   384       val (functab, predtab) =
   385         (functab, predtab) |> fold (add_clause_decls params) clauses
   386                            |>> fold add_arity_clause_funcs arity_clauses
   387   in (Symtab.dest functab, Symtab.dest predtab) end
   388 
   389 fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds =
   390   fold add_type_sort_preds ctypes_sorts preds
   391   handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
   392 
   393 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   394 fun preds_of_clauses clauses clsrel_clauses arity_clauses =
   395   Symtab.empty
   396   |> fold add_clause_preds clauses
   397   |> fold add_arity_clause_preds arity_clauses
   398   |> fold add_classrel_clause_preds clsrel_clauses
   399   |> Symtab.dest
   400 
   401 (**********************************************************************)
   402 (* write clauses to files                                             *)
   403 (**********************************************************************)
   404 
   405 val init_counters =
   406   Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
   407                ("c_COMBS", 0)];
   408 
   409 fun count_combterm (CombConst ((c, _), _, _)) =
   410     Symtab.map_entry c (Integer.add 1)
   411   | count_combterm (CombVar _) = I
   412   | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
   413 
   414 fun count_literal (Literal (_, t)) = count_combterm t
   415 
   416 fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
   417 
   418 fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) =
   419   member (op =) user_lemmas axiom_name ? fold count_literal literals
   420 
   421 fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint)
   422 
   423 fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
   424   if isFO then
   425     []
   426   else
   427     let
   428         val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
   429         val ct = init_counters |> fold count_clause conjectures
   430                                |> fold (count_user_clause user_lemmas) axclauses
   431         fun needed c = the (Symtab.lookup ct c) > 0
   432         val IK = if needed "c_COMBI" orelse needed "c_COMBK"
   433                  then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
   434                  else []
   435         val BC = if needed "c_COMBB" orelse needed "c_COMBC"
   436                  then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}]
   437                  else []
   438         val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}]
   439                 else []
   440         val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
   441                                          @{thm equal_imp_fequal}]
   442     in
   443         map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
   444     end;
   445 
   446 (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   447   are not at top level, to see if hBOOL is needed.*)
   448 fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
   449   let val (head, args) = strip_combterm_comb t
   450       val n = length args
   451       val (const_min_arity, const_needs_hBOOL) =
   452         (const_min_arity, const_needs_hBOOL)
   453         |> fold (count_constants_term false) args
   454   in
   455       case head of
   456           CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
   457             let val a = if a="equal" andalso not toplev then "c_fequal" else a
   458             in
   459               (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
   460                const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
   461             end
   462         | _ => (const_min_arity, const_needs_hBOOL)
   463   end;
   464 
   465 (*A literal is a top-level term*)
   466 fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
   467   count_constants_term true t (const_min_arity, const_needs_hBOOL);
   468 
   469 fun count_constants_clause (HOLClause {literals, ...})
   470                            (const_min_arity, const_needs_hBOOL) =
   471   fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
   472 
   473 fun display_arity explicit_apply const_needs_hBOOL (c,n) =
   474   trace_msg (fn () => "Constant: " ^ c ^
   475                 " arity:\t" ^ Int.toString n ^
   476                 (if needs_hBOOL explicit_apply const_needs_hBOOL c then
   477                    " needs hBOOL"
   478                  else
   479                    ""))
   480 
   481 fun count_constants explicit_apply
   482                     (conjectures, _, extra_clauses, helper_clauses, _, _) =
   483   if not explicit_apply then
   484      let val (const_min_arity, const_needs_hBOOL) =
   485           fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
   486        |> fold count_constants_clause extra_clauses
   487        |> fold count_constants_clause helper_clauses
   488      val _ = app (display_arity explicit_apply const_needs_hBOOL)
   489                  (Symtab.dest (const_min_arity))
   490      in (const_min_arity, const_needs_hBOOL) end
   491   else (Symtab.empty, Symtab.empty);
   492 
   493 fun header () =
   494   "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
   495   "% " ^ timestamp () ^ "\n"
   496 
   497 (* TPTP format *)
   498 
   499 fun write_tptp_file readable_names full_types explicit_apply file clauses =
   500   let
   501     fun section _ [] = []
   502       | section name ss =
   503         "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^
   504         ")\n" :: ss
   505     val pool = empty_name_pool readable_names
   506     val (conjectures, axclauses, _, helper_clauses,
   507       classrel_clauses, arity_clauses) = clauses
   508     val (cma, cnh) = count_constants explicit_apply clauses
   509     val params = (full_types, explicit_apply, cma, cnh)
   510     val ((conjecture_clss, tfree_litss), pool) =
   511       pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
   512     val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
   513     val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses
   514                                    pool
   515     val classrel_clss = map tptp_classrel_clause classrel_clauses
   516     val arity_clss = map tptp_arity_clause arity_clauses
   517     val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
   518                                        helper_clauses pool
   519     val conjecture_offset =
   520       length ax_clss + length classrel_clss + length arity_clss
   521       + length helper_clss
   522     val _ =
   523       File.write_list file
   524           (header () ::
   525            section "Relevant fact" ax_clss @
   526            section "Class relationship" classrel_clss @
   527            section "Arity declaration" arity_clss @
   528            section "Helper fact" helper_clss @
   529            section "Conjecture" conjecture_clss @
   530            section "Type variable" tfree_clss)
   531   in (pool, conjecture_offset) end
   532 
   533 (* DFG format *)
   534 
   535 fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1)
   536 
   537 fun write_dfg_file full_types explicit_apply file clauses =
   538   let
   539     (* Some of the helper functions below are not name-pool-aware. However,
   540        there's no point in adding name pool support if the DFG format is on its
   541        way out anyway. *)
   542     val pool = NONE
   543     val (conjectures, axclauses, _, helper_clauses,
   544       classrel_clauses, arity_clauses) = clauses
   545     val (cma, cnh) = count_constants explicit_apply clauses
   546     val params = (full_types, explicit_apply, cma, cnh)
   547     val ((conjecture_clss, tfree_litss), pool) =
   548       pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
   549     val tfree_lits = union_all tfree_litss
   550     val problem_name = Path.implode (Path.base file)
   551     val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
   552     val tfree_clss = map dfg_tfree_clause tfree_lits
   553     val tfree_preds = map dfg_tfree_predicate tfree_lits
   554     val (helper_clauses_strs, pool) =
   555       pool_map (apfst fst oo dfg_clause params) helper_clauses pool
   556     val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   557     val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   558     val preds = tfree_preds @ cl_preds @ ty_preds
   559     val conjecture_offset =
   560       length axclauses + length classrel_clauses + length arity_clauses
   561       + length helper_clauses
   562     val _ =
   563       File.write_list file
   564           (header () ::
   565            string_of_start problem_name ::
   566            string_of_descrip problem_name ::
   567            string_of_symbols (string_of_funcs funcs)
   568                              (string_of_preds preds) ::
   569            "list_of_clauses(axioms, cnf).\n" ::
   570            axstrs @
   571            map dfg_classrel_clause classrel_clauses @
   572            map dfg_arity_clause arity_clauses @
   573            helper_clauses_strs @
   574            ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
   575            conjecture_clss @
   576            tfree_clss @
   577            ["end_of_list.\n\n",
   578             "end_problem.\n"])
   579   in (pool, conjecture_offset) end
   580 
   581 end;