1.1 --- a/src/HOL/IsaMakefile	Tue Jun 22 19:10:12 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jun 22 23:54:02 2010 +0200
     1.3 @@ -322,6 +322,7 @@
     1.4    Tools/Sledgehammer/sledgehammer_hol_clause.ML \
     1.5    Tools/Sledgehammer/sledgehammer_isar.ML \
     1.6    Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
     1.7 +  Tools/Sledgehammer/sledgehammer_tptp_format.ML \
     1.8    Tools/Sledgehammer/sledgehammer_util.ML \
     1.9    Tools/SMT/cvc3_solver.ML \
    1.10    Tools/SMT/smtlib_interface.ML \

     2.1 --- a/src/HOL/Sledgehammer.thy	Tue Jun 22 19:10:12 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Tue Jun 22 23:54:02 2010 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
     2.5    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
     2.6    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
     2.7 +  ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
     2.8    ("Tools/ATP_Manager/atp_manager.ML")
     2.9    ("Tools/ATP_Manager/atp_systems.ML")
    2.10    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    2.11 @@ -103,6 +104,7 @@
    2.12  use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
    2.13  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    2.14  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    2.15 +use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
    2.16  use "Tools/ATP_Manager/atp_manager.ML"
    2.17  use "Tools/ATP_Manager/atp_systems.ML"
    2.18  setup ATP_Systems.setup

     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 22 19:10:12 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 22 23:54:02 2010 +0200
     3.3 @@ -27,6 +27,7 @@
     3.4  open Sledgehammer_HOL_Clause
     3.5  open Sledgehammer_Fact_Filter
     3.6  open Sledgehammer_Proof_Reconstruct
     3.7 +open Sledgehammer_TPTP_Format
     3.8  open ATP_Manager
     3.9  
    3.10  (** generic ATP **)
    3.11 @@ -191,8 +192,8 @@
    3.12          val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
    3.13          val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
    3.14        in (output, as_time t) end;
    3.15 -    fun split_time' s =
    3.16 -      if Config.get ctxt measure_runtime then split_time s else (s, 0)
    3.17 +    val split_time' =
    3.18 +      if Config.get ctxt measure_runtime then split_time else rpair 0
    3.19      fun run_on probfile =
    3.20        if File.exists command then
    3.21          write_tptp_file (debug andalso overlord) full_types explicit_apply
    3.22 @@ -244,35 +245,8 @@
    3.23  
    3.24  fun tptp_prover name p = (name, generic_tptp_prover (name, p));
    3.25  
    3.26 -
    3.27 -(** common provers **)
    3.28 -
    3.29  fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
    3.30  
    3.31 -(* Vampire *)
    3.32 -
    3.33 -(* Vampire requires an explicit time limit. *)
    3.34 -
    3.35 -val vampire_config : prover_config =
    3.36 -  {home_var = "VAMPIRE_HOME",
    3.37 -   executable = "vampire",
    3.38 -   arguments = fn timeout =>
    3.39 -     "--output_syntax tptp --mode casc -t " ^
    3.40 -     string_of_int (to_generous_secs timeout),
    3.41 -   proof_delims =
    3.42 -     [("=========== Refutation ==========",
    3.43 -       "======= End of refutation ======="),
    3.44 -      ("% SZS output start Refutation", "% SZS output end Refutation")],
    3.45 -   known_failures =
    3.46 -     [(Unprovable, "UNPROVABLE"),
    3.47 -      (IncompleteUnprovable, "CANNOT PROVE"),
    3.48 -      (Unprovable, "Satisfiability detected"),
    3.49 -      (OutOfResources, "Refutation not found")],
    3.50 -   max_axiom_clauses = 60,
    3.51 -   prefers_theory_relevant = false}
    3.52 -val vampire = tptp_prover "vampire" vampire_config
    3.53 -
    3.54 -
    3.55  (* E prover *)
    3.56  
    3.57  val tstp_proof_delims =
    3.58 @@ -299,8 +273,6 @@
    3.59  val e = tptp_prover "e" e_config
    3.60  
    3.61  
    3.62 -(* SPASS *)
    3.63 -
    3.64  (* The "-VarWeight=3" option helps the higher-order problems, probably by
    3.65     counteracting the presence of "hAPP". *)
    3.66  val spass_config : prover_config =
    3.67 @@ -322,7 +294,28 @@
    3.68     prefers_theory_relevant = true}
    3.69  val spass = tptp_prover "spass" spass_config
    3.70  
    3.71 -(* remote prover invocation via SystemOnTPTP *)
    3.72 +(* Vampire *)
    3.73 +
    3.74 +val vampire_config : prover_config =
    3.75 +  {home_var = "VAMPIRE_HOME",
    3.76 +   executable = "vampire",
    3.77 +   arguments = fn timeout =>
    3.78 +     "--output_syntax tptp --mode casc -t " ^
    3.79 +     string_of_int (to_generous_secs timeout),
    3.80 +   proof_delims =
    3.81 +     [("=========== Refutation ==========",
    3.82 +       "======= End of refutation ======="),
    3.83 +      ("% SZS output start Refutation", "% SZS output end Refutation")],
    3.84 +   known_failures =
    3.85 +     [(Unprovable, "UNPROVABLE"),
    3.86 +      (IncompleteUnprovable, "CANNOT PROVE"),
    3.87 +      (Unprovable, "Satisfiability detected"),
    3.88 +      (OutOfResources, "Refutation not found")],
    3.89 +   max_axiom_clauses = 60,
    3.90 +   prefers_theory_relevant = false}
    3.91 +val vampire = tptp_prover "vampire" vampire_config
    3.92 +
    3.93 +(* Remote prover invocation via SystemOnTPTP *)
    3.94  
    3.95  val systems = Synchronized.var "atp_systems" ([]: string list);
    3.96  
    3.97 @@ -333,7 +326,7 @@
    3.98      error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
    3.99  
   3.100  fun refresh_systems_on_tptp () =
   3.101 -  Synchronized.change systems (fn _ => get_systems ());
   3.102 +  Synchronized.change systems (fn _ => get_systems ())
   3.103  
   3.104  fun get_system prefix = Synchronized.change_result systems (fn systems =>
   3.105    (if null systems then get_systems () else systems)
   3.106 @@ -341,15 +334,14 @@
   3.107  
   3.108  fun the_system prefix =
   3.109    (case get_system prefix of
   3.110 -    NONE => error ("System " ^ quote prefix ^
   3.111 -                   " not available at SystemOnTPTP.")
   3.112 +    NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
   3.113    | SOME sys => sys);
   3.114  
   3.115  val remote_known_failures =
   3.116    [(TimedOut, "says Timeout"),
   3.117     (MalformedOutput, "Remote script could not extract proof")]
   3.118  
   3.119 -fun remote_prover_config atp_prefix args
   3.120 +fun remote_config atp_prefix args
   3.121          ({proof_delims, known_failures, max_axiom_clauses,
   3.122            prefers_theory_relevant, ...} : prover_config) : prover_config =
   3.123    {home_var = "ISABELLE_ATP_MANAGER",
   3.124 @@ -362,17 +354,12 @@
   3.125     max_axiom_clauses = max_axiom_clauses,
   3.126     prefers_theory_relevant = prefers_theory_relevant}
   3.127  
   3.128 -val remote_vampire =
   3.129 -  tptp_prover (remotify (fst vampire))
   3.130 -              (remote_prover_config "Vampire---9" "" vampire_config)
   3.131 +fun remote_tptp_prover prover atp_prefix args config =
   3.132 +  tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)
   3.133  
   3.134 -val remote_e =
   3.135 -  tptp_prover (remotify (fst e))
   3.136 -              (remote_prover_config "EP---" "" e_config)
   3.137 -
   3.138 -val remote_spass =
   3.139 -  tptp_prover (remotify (fst spass))
   3.140 -              (remote_prover_config "SPASS---" "-x" spass_config)
   3.141 +val remote_e = remote_tptp_prover e "EP---" "" e_config
   3.142 +val remote_spass = remote_tptp_prover spass "SPASS---" "-x" spass_config
   3.143 +val remote_vampire = remote_tptp_prover vampire "Vampire---9" "" vampire_config
   3.144  
   3.145  fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
   3.146    name |> getenv home_var = "" ? remotify
   3.147 @@ -381,7 +368,7 @@
   3.148    space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
   3.149                       remotify (fst vampire)]
   3.150  
   3.151 -val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e]
   3.152 +val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
   3.153  val prover_setup = fold add_prover provers
   3.154  
   3.155  val setup =

     4.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jun 22 19:10:12 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jun 22 23:54:02 2010 +0200
     4.3 @@ -24,6 +24,7 @@
     4.4  open Sledgehammer_HOL_Clause
     4.5  open Sledgehammer_Proof_Reconstruct
     4.6  open Sledgehammer_Fact_Filter
     4.7 +open Sledgehammer_TPTP_Format
     4.8  
     4.9  val trace = Unsynchronized.ref false;
    4.10  fun trace_msg msg = if !trace then tracing (msg ()) else ();

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 19:10:12 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 23:54:02 2010 +0200
     5.3 @@ -576,6 +576,47 @@
     5.4        |> has_override ? make_unique
     5.5      end
     5.6  
     5.7 +(** Helper clauses **)
     5.8 +
     5.9 +fun count_combterm (CombConst ((c, _), _, _)) =
    5.10 +    Symtab.map_entry c (Integer.add 1)
    5.11 +  | count_combterm (CombVar _) = I
    5.12 +  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
    5.13 +fun count_literal (Literal (_, t)) = count_combterm t
    5.14 +fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
    5.15 +
    5.16 +val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
    5.17 +fun cnf_helper_thms thy raw =
    5.18 +  map (`Thm.get_name_hint)
    5.19 +  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
    5.20 +
    5.21 +val optional_helpers =
    5.22 +  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
    5.23 +   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
    5.24 +   (["c_COMBS"], (false, @{thms COMBS_def}))]
    5.25 +val optional_typed_helpers =
    5.26 +  [(["c_True", "c_False"], (true, @{thms True_or_False})),
    5.27 +   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
    5.28 +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
    5.29 +
    5.30 +val init_counters =
    5.31 +  Symtab.make (maps (maps (map (rpair 0) o fst))
    5.32 +                    [optional_helpers, optional_typed_helpers])
    5.33 +
    5.34 +fun get_helper_clauses thy is_FO full_types conjectures axcls =
    5.35 +  let
    5.36 +    val axclauses = map snd (make_axiom_clauses thy axcls)
    5.37 +    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
    5.38 +    fun is_needed c = the (Symtab.lookup ct c) > 0
    5.39 +    val cnfs =
    5.40 +      (optional_helpers
    5.41 +       |> full_types ? append optional_typed_helpers
    5.42 +       |> maps (fn (ss, (raw, ths)) =>
    5.43 +                   if exists is_needed ss then cnf_helper_thms thy raw ths
    5.44 +                   else []))
    5.45 +      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
    5.46 +  in map snd (make_axiom_clauses thy cnfs) end
    5.47 +
    5.48  (* prepare for passing to writer,
    5.49     create additional clauses based on the information from extra_cls *)
    5.50  fun prepare_clauses full_types goal_cls axcls extra_cls thy =

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 19:10:12 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 23:54:02 2010 +0200
     6.3 @@ -10,11 +10,11 @@
     6.4  
     6.5  signature SLEDGEHAMMER_FOL_CLAUSE =
     6.6  sig
     6.7 +  val type_wrapper_name : string
     6.8    val schematic_var_prefix: string
     6.9    val fixed_var_prefix: string
    6.10    val tvar_prefix: string
    6.11    val tfree_prefix: string
    6.12 -  val clause_prefix: string
    6.13    val const_prefix: string
    6.14    val tconst_prefix: string
    6.15    val class_prefix: string
    6.16 @@ -23,7 +23,6 @@
    6.17    val type_const_trans_table: string Symtab.table
    6.18    val ascii_of: string -> string
    6.19    val undo_ascii_of: string -> string
    6.20 -  val paren_pack : string list -> string
    6.21    val make_schematic_var : string * int -> string
    6.22    val make_fixed_var : string -> string
    6.23    val make_schematic_type_var : string * int -> string
    6.24 @@ -37,12 +36,6 @@
    6.25    val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    6.26    val nice_name : name -> name_pool option -> string * name_pool option
    6.27    datatype kind = Axiom | Conjecture
    6.28 -  datatype fol_type =
    6.29 -    TyVar of name |
    6.30 -    TyFree of name |
    6.31 -    TyConstr of name * fol_type list
    6.32 -  val string_of_fol_type :
    6.33 -    fol_type -> name_pool option -> string * name_pool option
    6.34    datatype type_literal =
    6.35      TyLitVar of string * name |
    6.36      TyLitFree of string * name
    6.37 @@ -57,13 +50,6 @@
    6.38     {axiom_name: string, subclass: class, superclass: class}
    6.39    val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
    6.40    val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    6.41 -  val tptp_sign: bool -> string -> string
    6.42 -  val tptp_of_type_literal :
    6.43 -    bool -> type_literal -> name_pool option -> string * name_pool option
    6.44 -  val gen_tptp_cls : int * string * kind * string list * string list -> string
    6.45 -  val tptp_tfree_clause : string -> string
    6.46 -  val tptp_arity_clause : arity_clause -> string
    6.47 -  val tptp_classrel_clause : classrel_clause -> string
    6.48  end
    6.49  
    6.50  structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
    6.51 @@ -71,15 +57,15 @@
    6.52  
    6.53  open Sledgehammer_Util
    6.54  
    6.55 +val type_wrapper_name = "ti"
    6.56 +
    6.57  val schematic_var_prefix = "V_";
    6.58  val fixed_var_prefix = "v_";
    6.59  
    6.60  val tvar_prefix = "T_";
    6.61  val tfree_prefix = "t_";
    6.62  
    6.63 -val clause_prefix = "cls_";
    6.64 -val arclause_prefix = "clsarity_"
    6.65 -val clrelclause_prefix = "clsrel_";
    6.66 +val classrel_clause_prefix = "clsrel_";
    6.67  
    6.68  val const_prefix = "c_";
    6.69  val tconst_prefix = "tc_";
    6.70 @@ -152,12 +138,6 @@
    6.71  
    6.72  val undo_ascii_of = undo_ascii_aux [] o String.explode;
    6.73  
    6.74 -(* convert a list of strings into one single string; surrounded by brackets *)
    6.75 -fun paren_pack [] = ""   (*empty argument list*)
    6.76 -  | paren_pack strings = "(" ^ commas strings ^ ")";
    6.77 -
    6.78 -fun tptp_clause strings = "(" ^ space_implode " | " strings ^ ")"
    6.79 -
    6.80  (*Remove the initial ' character from a type variable, if it is present*)
    6.81  fun trim_type_var s =
    6.82    if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
    6.83 @@ -260,19 +240,6 @@
    6.84  
    6.85  (**** Isabelle FOL clauses ****)
    6.86  
    6.87 -datatype fol_type =
    6.88 -  TyVar of name |
    6.89 -  TyFree of name |
    6.90 -  TyConstr of name * fol_type list
    6.91 -
    6.92 -fun string_of_fol_type (TyVar sp) pool = nice_name sp pool
    6.93 -  | string_of_fol_type (TyFree sp) pool = nice_name sp pool
    6.94 -  | string_of_fol_type (TyConstr (sp, tys)) pool =
    6.95 -    let
    6.96 -      val (s, pool) = nice_name sp pool
    6.97 -      val (ss, pool) = pool_map string_of_fol_type tys pool
    6.98 -    in (s ^ paren_pack ss, pool) end
    6.99 -
   6.100  (* The first component is the type class; the second is a TVar or TFree. *)
   6.101  datatype type_literal =
   6.102    TyLitVar of string * name |
   6.103 @@ -341,7 +308,8 @@
   6.104        in fold add_supers subs [] end
   6.105  
   6.106  fun make_classrel_clause (sub,super) =
   6.107 -  ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
   6.108 +  ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
   6.109 +                               ascii_of super,
   6.110                    subclass = make_type_class sub,
   6.111                    superclass = make_type_class super};
   6.112  
   6.113 @@ -390,48 +358,4 @@
   6.114    let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   6.115    in  (classes', multi_arity_clause cpairs)  end;
   6.116  
   6.117 -
   6.118 -(**** Produce TPTP files ****)
   6.119 -
   6.120 -fun string_of_clausename (cls_id, ax_name) =
   6.121 -    clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id
   6.122 -
   6.123 -fun tptp_sign true s = s
   6.124 -  | tptp_sign false s = "~ " ^ s
   6.125 -
   6.126 -fun tptp_of_type_literal pos (TyLitVar (s, name)) =
   6.127 -    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
   6.128 -  | tptp_of_type_literal pos (TyLitFree (s, name)) =
   6.129 -    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
   6.130 -
   6.131 -fun tptp_cnf name kind formula =
   6.132 -  "cnf(" ^ name ^ ", " ^ kind ^ ",\n    " ^ formula ^ ").\n"
   6.133 -
   6.134 -fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
   6.135 -      tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
   6.136 -               (tptp_clause (tylits @ lits))
   6.137 -  | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
   6.138 -      tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
   6.139 -               (tptp_clause lits)
   6.140 -
   6.141 -fun tptp_tfree_clause tfree_lit =
   6.142 -    tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit])
   6.143 -
   6.144 -fun tptp_of_arLit (TConsLit (c,t,args)) =
   6.145 -      tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   6.146 -  | tptp_of_arLit (TVarLit (c,str)) =
   6.147 -      tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
   6.148 -
   6.149 -fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) =
   6.150 -  tptp_cnf (arclause_prefix ^ ascii_of axiom_name) "axiom"
   6.151 -           (tptp_clause (map tptp_of_arLit (conclLit :: premLits)))
   6.152 -
   6.153 -fun tptp_classrelLits sub sup =
   6.154 -  let val tvar = "(T)"
   6.155 -  in  tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
   6.156 -
   6.157 -fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass,
   6.158 -                                          ...}) =
   6.159 -  tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
   6.160 -
   6.161  end;

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 19:10:12 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 23:54:02 2010 +0200
     7.3 @@ -2,7 +2,7 @@
     7.4      Author:     Jia Meng, NICTA
     7.5      Author:     Jasmin Blanchette, TU Muenchen
     7.6  
     7.7 -FOL clauses translated from HOL formulae.
     7.8 +FOL clauses translated from HOL formulas.
     7.9  *)
    7.10  
    7.11  signature SLEDGEHAMMER_HOL_CLAUSE =
    7.12 @@ -11,21 +11,24 @@
    7.13    type name = Sledgehammer_FOL_Clause.name
    7.14    type name_pool = Sledgehammer_FOL_Clause.name_pool
    7.15    type kind = Sledgehammer_FOL_Clause.kind
    7.16 -  type fol_type = Sledgehammer_FOL_Clause.fol_type
    7.17    type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
    7.18    type arity_clause = Sledgehammer_FOL_Clause.arity_clause
    7.19    type polarity = bool
    7.20  
    7.21 +  datatype combtyp =
    7.22 +    TyVar of name |
    7.23 +    TyFree of name |
    7.24 +    TyConstr of name * combtyp list
    7.25    datatype combterm =
    7.26 -    CombConst of name * fol_type * fol_type list (* Const and Free *) |
    7.27 -    CombVar of name * fol_type |
    7.28 +    CombConst of name * combtyp * combtyp list (* Const and Free *) |
    7.29 +    CombVar of name * combtyp |
    7.30      CombApp of combterm * combterm
    7.31    datatype literal = Literal of polarity * combterm
    7.32    datatype hol_clause =
    7.33      HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    7.34                    literals: literal list, ctypes_sorts: typ list}
    7.35  
    7.36 -  val type_of_combterm : combterm -> fol_type
    7.37 +  val type_of_combterm : combterm -> combtyp
    7.38    val strip_combterm_comb : combterm -> combterm * combterm list
    7.39    val literals_of_term : theory -> term -> literal list * typ list
    7.40    val conceal_skolem_somes :
    7.41 @@ -33,12 +36,6 @@
    7.42    exception TRIVIAL of unit
    7.43    val make_conjecture_clauses : theory -> thm list -> hol_clause list
    7.44    val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
    7.45 -  val type_wrapper_name : string
    7.46 -  val get_helper_clauses :
    7.47 -    theory -> bool -> bool -> hol_clause list -> cnf_thm list -> hol_clause list
    7.48 -  val write_tptp_file : bool -> bool -> bool -> Path.T ->
    7.49 -    hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    7.50 -    classrel_clause list * arity_clause list -> name_pool option * int
    7.51  end
    7.52  
    7.53  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    7.54 @@ -48,24 +45,20 @@
    7.55  open Sledgehammer_FOL_Clause
    7.56  open Sledgehammer_Fact_Preprocessor
    7.57  
    7.58 -fun min_arity_of const_min_arity c =
    7.59 -  the_default 0 (Symtab.lookup const_min_arity c)
    7.60 -
    7.61 -(*True if the constant ever appears outside of the top-level position in literals.
    7.62 -  If false, the constant always receives all of its arguments and is used as a predicate.*)
    7.63 -fun needs_hBOOL explicit_apply const_needs_hBOOL c =
    7.64 -  explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c)
    7.65 -
    7.66 -
    7.67  (******************************************************)
    7.68  (* data types for typed combinator expressions        *)
    7.69  (******************************************************)
    7.70  
    7.71  type polarity = bool
    7.72  
    7.73 +datatype combtyp =
    7.74 +  TyVar of name |
    7.75 +  TyFree of name |
    7.76 +  TyConstr of name * combtyp list
    7.77 +
    7.78  datatype combterm =
    7.79 -  CombConst of name * fol_type * fol_type list (* Const and Free *) |
    7.80 -  CombVar of name * fol_type |
    7.81 +  CombConst of name * combtyp * combtyp list (* Const and Free *) |
    7.82 +  CombVar of name * combtyp |
    7.83    CombApp of combterm * combterm
    7.84  
    7.85  datatype literal = Literal of polarity * combterm;
    7.86 @@ -74,11 +67,24 @@
    7.87    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    7.88                  literals: literal list, ctypes_sorts: typ list}
    7.89  
    7.90 -
    7.91  (*********************************************************************)
    7.92  (* convert a clause with type Term.term to a clause with type clause *)
    7.93  (*********************************************************************)
    7.94  
    7.95 +(*Result of a function type; no need to check that the argument type matches.*)
    7.96 +fun result_type (TyConstr (_, [_, tp2])) = tp2
    7.97 +  | result_type _ = raise Fail "non-function type"
    7.98 +
    7.99 +fun type_of_combterm (CombConst (_, tp, _)) = tp
   7.100 +  | type_of_combterm (CombVar (_, tp)) = tp
   7.101 +  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
   7.102 +
   7.103 +(*gets the head of a combinator application, along with the list of arguments*)
   7.104 +fun strip_combterm_comb u =
   7.105 +    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   7.106 +        |   stripc  x =  x
   7.107 +    in stripc(u,[]) end
   7.108 +
   7.109  fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
   7.110        (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
   7.111    | isFalse _ = false;
   7.112 @@ -109,7 +115,6 @@
   7.113    | simp_type_of (TVar (x, _)) =
   7.114      TyVar (make_schematic_type_var x, string_of_indexname x)
   7.115  
   7.116 -
   7.117  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   7.118  fun combterm_of thy (Const (c, T)) =
   7.119        let
   7.120 @@ -224,254 +229,4 @@
   7.121          in cls :: aux (n + 1) skolem_somes ths end
   7.122    in aux 0 [] end
   7.123  
   7.124 -(**********************************************************************)
   7.125 -(* convert clause into TPTP format                                    *)
   7.126 -(**********************************************************************)
   7.127 -
   7.128 -(*Result of a function type; no need to check that the argument type matches.*)
   7.129 -fun result_type (TyConstr (_, [_, tp2])) = tp2
   7.130 -  | result_type _ = raise Fail "non-function type"
   7.131 -
   7.132 -fun type_of_combterm (CombConst (_, tp, _)) = tp
   7.133 -  | type_of_combterm (CombVar (_, tp)) = tp
   7.134 -  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
   7.135 -
   7.136 -(*gets the head of a combinator application, along with the list of arguments*)
   7.137 -fun strip_combterm_comb u =
   7.138 -    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   7.139 -        |   stripc  x =  x
   7.140 -    in  stripc(u,[])  end;
   7.141 -
   7.142 -val type_wrapper_name = "ti"
   7.143 -
   7.144 -fun head_needs_hBOOL explicit_apply const_needs_hBOOL
   7.145 -                     (CombConst ((c, _), _, _)) =
   7.146 -    needs_hBOOL explicit_apply const_needs_hBOOL c
   7.147 -  | head_needs_hBOOL _ _ _ = true
   7.148 -
   7.149 -fun wrap_type full_types (s, ty) pool =
   7.150 -  if full_types then
   7.151 -    let val (s', pool) = string_of_fol_type ty pool in
   7.152 -      (type_wrapper_name ^ paren_pack [s, s'], pool)
   7.153 -    end
   7.154 -  else
   7.155 -    (s, pool)
   7.156 -
   7.157 -fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
   7.158 -  if head_needs_hBOOL explicit_apply cnh head then
   7.159 -    wrap_type full_types (s, tp)
   7.160 -  else
   7.161 -    pair s
   7.162 -
   7.163 -fun apply ss = "hAPP" ^ paren_pack ss;
   7.164 -
   7.165 -fun rev_apply (v, []) = v
   7.166 -  | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
   7.167 -
   7.168 -fun string_apply (v, args) = rev_apply (v, rev args);
   7.169 -
   7.170 -(* Apply an operator to the argument strings, using either the "apply" operator
   7.171 -   or direct function application. *)
   7.172 -fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
   7.173 -                          pool =
   7.174 -    let
   7.175 -      val s = if s = "equal" then "c_fequal" else s
   7.176 -      val nargs = min_arity_of cma s
   7.177 -      val args1 = List.take (args, nargs)
   7.178 -        handle Subscript =>
   7.179 -               raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
   7.180 -                           " but is applied to " ^ commas (map quote args))
   7.181 -      val args2 = List.drop (args, nargs)
   7.182 -      val (targs, pool) = if full_types then ([], pool)
   7.183 -                          else pool_map string_of_fol_type tvars pool
   7.184 -      val (s, pool) = nice_name (s, s') pool
   7.185 -    in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
   7.186 -  | string_of_application _ _ (CombVar (name, _), args) pool =
   7.187 -    nice_name name pool |>> (fn s => string_apply (s, args))
   7.188 -
   7.189 -fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t
   7.190 -                       pool =
   7.191 -  let
   7.192 -    val (head, args) = strip_combterm_comb t
   7.193 -    val (ss, pool) = pool_map (string_of_combterm params) args pool
   7.194 -    val (s, pool) = string_of_application full_types cma (head, ss) pool
   7.195 -  in
   7.196 -    wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t)
   7.197 -                 pool
   7.198 -  end
   7.199 -
   7.200 -(*Boolean-valued terms are here converted to literals.*)
   7.201 -fun boolify params c =
   7.202 -  string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
   7.203 -
   7.204 -fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
   7.205 -  case #1 (strip_combterm_comb t) of
   7.206 -    CombConst ((s, _), _, _) =>
   7.207 -    (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
   7.208 -        params t
   7.209 -  | _ => boolify params t
   7.210 -
   7.211 -
   7.212 -(*** TPTP format ***)
   7.213 -
   7.214 -fun tptp_of_equality params pos (t1, t2) =
   7.215 -  pool_map (string_of_combterm params) [t1, t2]
   7.216 -  #>> space_implode (if pos then " = " else " != ")
   7.217 -
   7.218 -fun tptp_literal params
   7.219 -        (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
   7.220 -                                         t2))) =
   7.221 -    tptp_of_equality params pos (t1, t2)
   7.222 -  | tptp_literal params (Literal (pos, pred)) =
   7.223 -    string_of_predicate params pred #>> tptp_sign pos
   7.224 - 
   7.225 -(* Given a clause, returns its literals paired with a list of literals
   7.226 -   concerning TFrees; the latter should only occur in conjecture clauses. *)
   7.227 -fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
   7.228 -                       pool =
   7.229 -  let
   7.230 -    val (lits, pool) = pool_map (tptp_literal params) literals pool
   7.231 -    val (tylits, pool) = pool_map (tptp_of_type_literal pos)
   7.232 -                                  (type_literals_for_types ctypes_sorts) pool
   7.233 -  in ((lits, tylits), pool) end
   7.234 -
   7.235 -fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
   7.236 -                pool =
   7.237 -  let
   7.238 -    val ((lits, tylits), pool) =
   7.239 -      tptp_type_literals params (kind = Conjecture) cls pool
   7.240 -  in
   7.241 -    ((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool)
   7.242 -  end
   7.243 -
   7.244 -
   7.245 -(**********************************************************************)
   7.246 -(* write clauses to files                                             *)
   7.247 -(**********************************************************************)
   7.248 -
   7.249 -fun count_combterm (CombConst ((c, _), _, _)) =
   7.250 -    Symtab.map_entry c (Integer.add 1)
   7.251 -  | count_combterm (CombVar _) = I
   7.252 -  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
   7.253 -
   7.254 -fun count_literal (Literal (_, t)) = count_combterm t
   7.255 -
   7.256 -fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
   7.257 -
   7.258 -val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
   7.259 -fun cnf_helper_thms thy raw =
   7.260 -  map (`Thm.get_name_hint)
   7.261 -  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
   7.262 -
   7.263 -val optional_helpers =
   7.264 -  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
   7.265 -   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
   7.266 -   (["c_COMBS"], (false, @{thms COMBS_def}))]
   7.267 -val optional_typed_helpers =
   7.268 -  [(["c_True", "c_False"], (true, @{thms True_or_False})),
   7.269 -   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
   7.270 -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   7.271 -
   7.272 -val init_counters =
   7.273 -  Symtab.make (maps (maps (map (rpair 0) o fst))
   7.274 -                    [optional_helpers, optional_typed_helpers])
   7.275 -
   7.276 -fun get_helper_clauses thy is_FO full_types conjectures axcls =
   7.277 -  let
   7.278 -    val axclauses = map snd (make_axiom_clauses thy axcls)
   7.279 -    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
   7.280 -    fun is_needed c = the (Symtab.lookup ct c) > 0
   7.281 -    val cnfs =
   7.282 -      (optional_helpers
   7.283 -       |> full_types ? append optional_typed_helpers
   7.284 -       |> maps (fn (ss, (raw, ths)) =>
   7.285 -                   if exists is_needed ss then cnf_helper_thms thy raw ths
   7.286 -                   else []))
   7.287 -      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   7.288 -  in map snd (make_axiom_clauses thy cnfs) end
   7.289 -
   7.290 -(*Find the minimal arity of each function mentioned in the term. Also, note which uses
   7.291 -  are not at top level, to see if hBOOL is needed.*)
   7.292 -fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
   7.293 -  let val (head, args) = strip_combterm_comb t
   7.294 -      val n = length args
   7.295 -      val (const_min_arity, const_needs_hBOOL) =
   7.296 -        (const_min_arity, const_needs_hBOOL)
   7.297 -        |> fold (count_constants_term false) args
   7.298 -  in
   7.299 -      case head of
   7.300 -          CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
   7.301 -            let val a = if a="equal" andalso not toplev then "c_fequal" else a
   7.302 -            in
   7.303 -              (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
   7.304 -               const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
   7.305 -            end
   7.306 -        | _ => (const_min_arity, const_needs_hBOOL)
   7.307 -  end;
   7.308 -
   7.309 -(*A literal is a top-level term*)
   7.310 -fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
   7.311 -  count_constants_term true t (const_min_arity, const_needs_hBOOL);
   7.312 -
   7.313 -fun count_constants_clause (HOLClause {literals, ...})
   7.314 -                           (const_min_arity, const_needs_hBOOL) =
   7.315 -  fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
   7.316 -
   7.317 -fun display_arity explicit_apply const_needs_hBOOL (c, n) =
   7.318 -  trace_msg (fn () => "Constant: " ^ c ^
   7.319 -                " arity:\t" ^ Int.toString n ^
   7.320 -                (if needs_hBOOL explicit_apply const_needs_hBOOL c then
   7.321 -                   " needs hBOOL"
   7.322 -                 else
   7.323 -                   ""))
   7.324 -
   7.325 -fun count_constants explicit_apply
   7.326 -                    (conjectures, _, extra_clauses, helper_clauses, _, _) =
   7.327 -  if not explicit_apply then
   7.328 -     let val (const_min_arity, const_needs_hBOOL) =
   7.329 -          fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
   7.330 -       |> fold count_constants_clause extra_clauses
   7.331 -       |> fold count_constants_clause helper_clauses
   7.332 -     val _ = app (display_arity explicit_apply const_needs_hBOOL)
   7.333 -                 (Symtab.dest (const_min_arity))
   7.334 -     in (const_min_arity, const_needs_hBOOL) end
   7.335 -  else (Symtab.empty, Symtab.empty);
   7.336 -
   7.337 -(* TPTP format *)
   7.338 -
   7.339 -fun write_tptp_file readable_names full_types explicit_apply file clauses =
   7.340 -  let
   7.341 -    fun section _ [] = []
   7.342 -      | section name ss =
   7.343 -        "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^
   7.344 -        ")\n" :: ss
   7.345 -    val pool = empty_name_pool readable_names
   7.346 -    val (conjectures, axclauses, _, helper_clauses,
   7.347 -      classrel_clauses, arity_clauses) = clauses
   7.348 -    val (cma, cnh) = count_constants explicit_apply clauses
   7.349 -    val params = (full_types, explicit_apply, cma, cnh)
   7.350 -    val ((conjecture_clss, tfree_litss), pool) =
   7.351 -      pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
   7.352 -    val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
   7.353 -    val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses
   7.354 -                                   pool
   7.355 -    val classrel_clss = map tptp_classrel_clause classrel_clauses
   7.356 -    val arity_clss = map tptp_arity_clause arity_clauses
   7.357 -    val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
   7.358 -                                       helper_clauses pool
   7.359 -    val conjecture_offset =
   7.360 -      length ax_clss + length classrel_clss + length arity_clss
   7.361 -      + length helper_clss
   7.362 -    val _ =
   7.363 -      File.write_list file
   7.364 -          ("% This file was generated by Isabelle (most likely Sledgehammer)\n\
   7.365 -           \% " ^ timestamp () ^ "\n" ::
   7.366 -           section "Relevant fact" ax_clss @
   7.367 -           section "Class relationship" classrel_clss @
   7.368 -           section "Arity declaration" arity_clss @
   7.369 -           section "Helper fact" helper_clss @
   7.370 -           section "Conjecture" conjecture_clss @
   7.371 -           section "Type variable" tfree_clss)
   7.372 -  in (pool, conjecture_offset) end
   7.373 -
   7.374  end;

     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Tue Jun 22 23:54:02 2010 +0200
     8.3 @@ -0,0 +1,255 @@
     8.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
     8.5 +    Author:     Jia Meng, NICTA
     8.6 +    Author:     Jasmin Blanchette, TU Muenchen
     8.7 +
     8.8 +TPTP syntax.
     8.9 +*)
    8.10 +
    8.11 +signature SLEDGEHAMMER_TPTP_FORMAT =
    8.12 +sig
    8.13 +  type name_pool = Sledgehammer_FOL_Clause.name_pool
    8.14 +  type type_literal = Sledgehammer_FOL_Clause.type_literal
    8.15 +  type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
    8.16 +  type arity_clause = Sledgehammer_FOL_Clause.arity_clause
    8.17 +  type hol_clause = Sledgehammer_HOL_Clause.hol_clause
    8.18 +
    8.19 +  val tptp_of_type_literal :
    8.20 +    bool -> type_literal -> name_pool option -> string * name_pool option
    8.21 +  val write_tptp_file :
    8.22 +    bool -> bool -> bool -> Path.T
    8.23 +    -> hol_clause list * hol_clause list * hol_clause list * hol_clause list
    8.24 +       * classrel_clause list * arity_clause list
    8.25 +    -> name_pool option * int
    8.26 +end;
    8.27 +
    8.28 +structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
    8.29 +struct
    8.30 +
    8.31 +open Sledgehammer_Util
    8.32 +open Sledgehammer_FOL_Clause
    8.33 +open Sledgehammer_HOL_Clause
    8.34 +
    8.35 +val clause_prefix = "cls_"
    8.36 +val arity_clause_prefix = "clsarity_"
    8.37 +
    8.38 +fun paren_pack [] = ""
    8.39 +  | paren_pack strings = "(" ^ commas strings ^ ")"
    8.40 +
    8.41 +fun string_of_fol_type (TyVar sp) pool = nice_name sp pool
    8.42 +  | string_of_fol_type (TyFree sp) pool = nice_name sp pool
    8.43 +  | string_of_fol_type (TyConstr (sp, tys)) pool =
    8.44 +    let
    8.45 +      val (s, pool) = nice_name sp pool
    8.46 +      val (ss, pool) = pool_map string_of_fol_type tys pool
    8.47 +    in (s ^ paren_pack ss, pool) end
    8.48 +
    8.49 +(* True if the constant ever appears outside of the top-level position in
    8.50 +   literals. If false, the constant always receives all of its arguments and is
    8.51 +   used as a predicate. *)
    8.52 +fun needs_hBOOL explicit_apply const_needs_hBOOL c =
    8.53 +  explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c)
    8.54 +
    8.55 +fun head_needs_hBOOL explicit_apply const_needs_hBOOL
    8.56 +                     (CombConst ((c, _), _, _)) =
    8.57 +    needs_hBOOL explicit_apply const_needs_hBOOL c
    8.58 +  | head_needs_hBOOL _ _ _ = true
    8.59 +
    8.60 +fun wrap_type full_types (s, ty) pool =
    8.61 +  if full_types then
    8.62 +    let val (s', pool) = string_of_fol_type ty pool in
    8.63 +      (type_wrapper_name ^ paren_pack [s, s'], pool)
    8.64 +    end
    8.65 +  else
    8.66 +    (s, pool)
    8.67 +
    8.68 +fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
    8.69 +  if head_needs_hBOOL explicit_apply cnh head then
    8.70 +    wrap_type full_types (s, tp)
    8.71 +  else
    8.72 +    pair s
    8.73 +
    8.74 +fun apply ss = "hAPP" ^ paren_pack ss;
    8.75 +
    8.76 +fun rev_apply (v, []) = v
    8.77 +  | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
    8.78 +
    8.79 +fun string_apply (v, args) = rev_apply (v, rev args)
    8.80 +
    8.81 +fun min_arity_of const_min_arity = the_default 0 o Symtab.lookup const_min_arity
    8.82 +
    8.83 +(* Apply an operator to the argument strings, using either the "apply" operator
    8.84 +   or direct function application. *)
    8.85 +fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
    8.86 +                          pool =
    8.87 +    let
    8.88 +      val s = if s = "equal" then "c_fequal" else s
    8.89 +      val nargs = min_arity_of cma s
    8.90 +      val args1 = List.take (args, nargs)
    8.91 +        handle Subscript =>
    8.92 +               raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
    8.93 +                           " but is applied to " ^ commas (map quote args))
    8.94 +      val args2 = List.drop (args, nargs)
    8.95 +      val (targs, pool) = if full_types then ([], pool)
    8.96 +                          else pool_map string_of_fol_type tvars pool
    8.97 +      val (s, pool) = nice_name (s, s') pool
    8.98 +    in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
    8.99 +  | string_of_application _ _ (CombVar (name, _), args) pool =
   8.100 +    nice_name name pool |>> (fn s => string_apply (s, args))
   8.101 +
   8.102 +fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t
   8.103 +                       pool =
   8.104 +  let
   8.105 +    val (head, args) = strip_combterm_comb t
   8.106 +    val (ss, pool) = pool_map (string_of_combterm params) args pool
   8.107 +    val (s, pool) = string_of_application full_types cma (head, ss) pool
   8.108 +  in
   8.109 +    wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t)
   8.110 +                 pool
   8.111 +  end
   8.112 +
   8.113 +(*Boolean-valued terms are here converted to literals.*)
   8.114 +fun boolify params c =
   8.115 +  string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
   8.116 +
   8.117 +fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
   8.118 +  case #1 (strip_combterm_comb t) of
   8.119 +    CombConst ((s, _), _, _) =>
   8.120 +    (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
   8.121 +        params t
   8.122 +  | _ => boolify params t
   8.123 +
   8.124 +fun tptp_of_equality params pos (t1, t2) =
   8.125 +  pool_map (string_of_combterm params) [t1, t2]
   8.126 +  #>> space_implode (if pos then " = " else " != ")
   8.127 +
   8.128 +fun tptp_sign true s = s
   8.129 +  | tptp_sign false s = "~ " ^ s
   8.130 +
   8.131 +fun tptp_literal params
   8.132 +        (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
   8.133 +                                         t2))) =
   8.134 +    tptp_of_equality params pos (t1, t2)
   8.135 +  | tptp_literal params (Literal (pos, pred)) =
   8.136 +    string_of_predicate params pred #>> tptp_sign pos
   8.137 + 
   8.138 +fun tptp_of_type_literal pos (TyLitVar (s, name)) =
   8.139 +    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
   8.140 +  | tptp_of_type_literal pos (TyLitFree (s, name)) =
   8.141 +    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
   8.142 +
   8.143 +(* Given a clause, returns its literals paired with a list of literals
   8.144 +   concerning TFrees; the latter should only occur in conjecture clauses. *)
   8.145 +fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
   8.146 +                       pool =
   8.147 +  let
   8.148 +    val (lits, pool) = pool_map (tptp_literal params) literals pool
   8.149 +    val (tylits, pool) = pool_map (tptp_of_type_literal pos)
   8.150 +                                  (type_literals_for_types ctypes_sorts) pool
   8.151 +  in ((lits, tylits), pool) end
   8.152 +
   8.153 +fun tptp_cnf name kind formula =
   8.154 +  "cnf(" ^ name ^ ", " ^ kind ^ ",\n    " ^ formula ^ ").\n"
   8.155 +
   8.156 +fun tptp_raw_clause strings = "(" ^ space_implode " | " strings ^ ")"
   8.157 +
   8.158 +val tptp_tfree_clause =
   8.159 +  tptp_cnf "tfree_tcs" "negated_conjecture" o tptp_raw_clause o single
   8.160 +
   8.161 +fun tptp_classrel_literals sub sup =
   8.162 +  let val tvar = "(T)" in
   8.163 +    tptp_raw_clause [tptp_sign false (sub ^ tvar), tptp_sign true (sup ^ tvar)]
   8.164 +  end
   8.165 +
   8.166 +fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
   8.167 +                pool =
   8.168 +  let
   8.169 +    val ((lits, tylits), pool) =
   8.170 +      tptp_type_literals params (kind = Conjecture) cls pool
   8.171 +    val name = clause_prefix ^ ascii_of axiom_name ^ "_" ^
   8.172 +               Int.toString clause_id
   8.173 +    val cnf =
   8.174 +      case kind of
   8.175 +        Axiom => tptp_cnf name "axiom" (tptp_raw_clause (tylits @ lits))
   8.176 +      | Conjecture => tptp_cnf name "negated_conjecture" (tptp_raw_clause lits)
   8.177 +  in ((cnf, tylits), pool) end
   8.178 +
   8.179 +fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass,
   8.180 +                                          ...}) =
   8.181 +  tptp_cnf axiom_name "axiom" (tptp_classrel_literals subclass superclass)
   8.182 +
   8.183 +fun tptp_of_arity_literal (TConsLit (c, t, args)) =
   8.184 +    tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   8.185 +  | tptp_of_arity_literal (TVarLit (c, str)) =
   8.186 +    tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
   8.187 +
   8.188 +fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) =
   8.189 +  tptp_cnf (arity_clause_prefix ^ ascii_of axiom_name) "axiom"
   8.190 +           (tptp_raw_clause (map tptp_of_arity_literal (conclLit :: premLits)))
   8.191 +
   8.192 +(*Find the minimal arity of each function mentioned in the term. Also, note which uses
   8.193 +  are not at top level, to see if hBOOL is needed.*)
   8.194 +fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
   8.195 +  let
   8.196 +    val (head, args) = strip_combterm_comb t
   8.197 +    val n = length args
   8.198 +    val (const_min_arity, const_needs_hBOOL) =
   8.199 +      (const_min_arity, const_needs_hBOOL)
   8.200 +      |> fold (count_constants_term false) args
   8.201 +  in
   8.202 +    case head of
   8.203 +      CombConst ((a, _), _, _) => (*predicate or function version of "equal"?*)
   8.204 +        let val a = if a="equal" andalso not toplev then "c_fequal" else a
   8.205 +        in
   8.206 +          (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
   8.207 +           const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
   8.208 +        end
   8.209 +      | _ => (const_min_arity, const_needs_hBOOL)
   8.210 +  end
   8.211 +fun count_constants_lit (Literal (_, t)) = count_constants_term true t
   8.212 +fun count_constants_clause (HOLClause {literals, ...}) =
   8.213 +  fold count_constants_lit literals
   8.214 +fun count_constants explicit_apply
   8.215 +                    (conjectures, _, extra_clauses, helper_clauses, _, _) =
   8.216 +  (Symtab.empty, Symtab.empty)
   8.217 +  |> (if explicit_apply then
   8.218 +        I
   8.219 +      else
   8.220 +        fold (fold count_constants_clause)
   8.221 +             [conjectures, extra_clauses, helper_clauses])
   8.222 +
   8.223 +fun write_tptp_file readable_names full_types explicit_apply file clauses =
   8.224 +  let
   8.225 +    fun section _ [] = []
   8.226 +      | section name ss =
   8.227 +        "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^
   8.228 +        ")\n" :: ss
   8.229 +    val pool = empty_name_pool readable_names
   8.230 +    val (conjectures, axclauses, _, helper_clauses,
   8.231 +      classrel_clauses, arity_clauses) = clauses
   8.232 +    val (cma, cnh) = count_constants explicit_apply clauses
   8.233 +    val params = (full_types, explicit_apply, cma, cnh)
   8.234 +    val ((conjecture_clss, tfree_litss), pool) =
   8.235 +      pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
   8.236 +    val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
   8.237 +    val (ax_clss, pool) =
   8.238 +      pool_map (apfst fst oo tptp_clause params) axclauses pool
   8.239 +    val classrel_clss = map tptp_classrel_clause classrel_clauses
   8.240 +    val arity_clss = map tptp_arity_clause arity_clauses
   8.241 +    val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
   8.242 +                                       helper_clauses pool
   8.243 +    val conjecture_offset =
   8.244 +      length ax_clss + length classrel_clss + length arity_clss
   8.245 +      + length helper_clss
   8.246 +    val _ =
   8.247 +      File.write_list file
   8.248 +          ("% This file was generated by Isabelle (most likely Sledgehammer)\n\
   8.249 +           \% " ^ timestamp () ^ "\n" ::
   8.250 +           section "Relevant fact" ax_clss @
   8.251 +           section "Class relationship" classrel_clss @
   8.252 +           section "Arity declaration" arity_clss @
   8.253 +           section "Helper fact" helper_clss @
   8.254 +           section "Conjecture" conjecture_clss @
   8.255 +           section "Type variable" tfree_clss)
   8.256 +  in (pool, conjecture_offset) end
   8.257 +
   8.258 +end;