author blanchet Tue, 24 May 2011 00:01:33 +0200 changeset 42962 3b50fdeb6cfc parent 42961 f30ae82cb62e child 42963 5725deb11ae7
started adding support for THF output (but no lambdas)
```--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 24 00:01:33 2011 +0200
@@ -15,7 +15,7 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c

-  datatype format = CNF_UEQ | FOF | TFF
+  datatype format = CNF_UEQ | FOF | TFF | THF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a list * 'a |
@@ -27,9 +27,9 @@
val tptp_special_prefix : string
val tptp_false : string
val tptp_true : string
-  val tptp_tff_type_of_types : string
-  val tptp_tff_bool_type : string
-  val tptp_tff_individual_type : string
+  val tptp_type_of_types : string
+  val tptp_bool_type : string
+  val tptp_individual_type : string
val is_atp_variable : string -> bool
val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
val mk_aconn :
@@ -61,7 +61,7 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c

-datatype format = CNF_UEQ | FOF | TFF
+datatype format = CNF_UEQ | FOF | TFF | THF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a list * 'a |
@@ -73,9 +73,9 @@
val tptp_special_prefix = "\$"
val tptp_false = "\$false"
val tptp_true = "\$true"
-val tptp_tff_type_of_types = "\$tType"
-val tptp_tff_bool_type = "\$o"
-val tptp_tff_individual_type = "\$i"
+val tptp_type_of_types = "\$tType"
+val tptp_bool_type = "\$o"
+val tptp_individual_type = "\$i"

fun is_atp_variable s = Char.isUpper (String.sub (s, 0))

@@ -89,8 +89,8 @@

val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now

-(* This hash function is recommended in Compilers: Principles, Techniques, and
-   Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they
+(* This hash function is recommended in "Compilers: Principles, Techniques, and
+   Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
@@ -102,14 +102,18 @@
| string_for_kind Hypothesis = "hypothesis"
| string_for_kind Conjecture = "conjecture"

-fun string_for_term (ATerm (s, [])) = s
-  | string_for_term (ATerm ("equal", ts)) =
-    space_implode " = " (map string_for_term ts)
-  | string_for_term (ATerm ("[]", ts)) =
+fun string_for_term _ (ATerm (s, [])) = s
+  | string_for_term format (ATerm ("equal", ts)) =
+    space_implode " = " (map (string_for_term format) ts)
+    |> format = THF ? enclose "(" ")"
+  | string_for_term format (ATerm ("[]", ts)) =
(* used for lists in the optional "source" field of a derivation *)
-    "[" ^ commas (map string_for_term ts) ^ "]"
-  | string_for_term (ATerm (s, ts)) =
-    s ^ "(" ^ commas (map string_for_term ts) ^ ")"
+    "[" ^ commas (map (string_for_term format) ts) ^ "]"
+  | string_for_term format (ATerm (s, ts)) =
+    let val ss = map (string_for_term format) ts in
+      if format = THF then "(" ^ space_implode " @ " (s :: ss) ^ ")"
+      else s ^ "(" ^ commas ss ^ ")"
+    end
fun string_for_quantifier AForall = "!"
| string_for_quantifier AExists = "?"
fun string_for_connective ANot = "~"
@@ -119,43 +123,52 @@
| string_for_connective AIf = "<="
| string_for_connective AIff = "<=>"
| string_for_connective ANotIff = "<~>"
-fun string_for_bound_var TFF (s, ty) =
-    s ^ " : " ^ (ty |> the_default tptp_tff_individual_type)
-  | string_for_bound_var _ (s, _) = s
+fun string_for_bound_var format (s, ty) =
+    s ^ (if format = TFF orelse format = THF then
+           " : " ^ (ty |> the_default tptp_individual_type)
+         else
+           "")
fun string_for_formula format (AQuant (q, xs, phi)) =
"(" ^ string_for_quantifier q ^
"[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
string_for_formula format phi ^ ")"
-  | string_for_formula _ (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
-    space_implode " != " (map string_for_term ts)
+  | string_for_formula format (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
+    space_implode " != " (map (string_for_term format) ts)
| string_for_formula format (AConn (c, [phi])) =
"(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")"
| string_for_formula format (AConn (c, phis)) =
"(" ^ space_implode (" " ^ string_for_connective c ^ " ")
(map (string_for_formula format) phis) ^ ")"
-  | string_for_formula _ (AAtom tm) = string_for_term tm
+  | string_for_formula format (AAtom tm) = string_for_term format tm

-fun string_for_symbol_type [] res_ty = res_ty
-  | string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
-  | string_for_symbol_type arg_tys res_ty =
-    string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty
+fun string_for_symbol_type THF arg_tys res_ty =
+    space_implode " > " (arg_tys @ [res_ty])
+  | string_for_symbol_type _ [] res_ty = res_ty
+  | string_for_symbol_type _ [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
+  | string_for_symbol_type format arg_tys res_ty =
+    string_for_symbol_type format ["(" ^ space_implode " * " arg_tys ^ ")"]
+                           res_ty

val default_source =
ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))

-fun string_for_problem_line _ (Decl (ident, sym, arg_tys, res_ty)) =
-    "tff(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
-    string_for_symbol_type arg_tys res_ty ^ ").\n"
+fun string_for_format CNF_UEQ = "cnf"
+  | string_for_format FOF = "fof"
+  | string_for_format TFF = "tff"
+  | string_for_format THF = "thf"
+
+fun string_for_problem_line format (Decl (ident, sym, arg_tys, res_ty)) =
+    string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
+    string_for_symbol_type format arg_tys res_ty ^ ").\n"
| string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
-    (case format of CNF_UEQ => "cnf" | FOF => "fof" | TFF => "tff") ^
-    "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
-    string_for_formula format phi ^ ")" ^
+    string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^
+    ",\n    (" ^ string_for_formula format phi ^ ")" ^
(case (source, info) of
(NONE, NONE) => ""
-     | (SOME tm, NONE) => ", " ^ string_for_term tm
+     | (SOME tm, NONE) => ", " ^ string_for_term format tm
| (_, SOME tm) =>
-       ", " ^ string_for_term (source |> the_default default_source) ^
-       ", " ^ string_for_term tm) ^ ").\n"
+       ", " ^ string_for_term format (source |> the_default default_source) ^
+       ", " ^ string_for_term format tm) ^ ").\n"
fun tptp_strings_for_atp_problem format problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
@@ -191,11 +204,12 @@
Formula (ident, Hypothesis, mk_anot phi, source, info)
| negate_conjecture_line line = line

-val filter_cnf_ueq_problem =
-  map (apsnd (map open_formula_line
-              #> filter is_problem_line_cnf_ueq
-              #> map negate_conjecture_line))
-  #> (fn problem =>
+fun filter_cnf_ueq_problem problem =
+  problem
+  |> map (apsnd (map open_formula_line
+                 #> filter is_problem_line_cnf_ueq
+                 #> map negate_conjecture_line))
+  |> (fn problem =>
let
val conjs = problem |> maps snd |> filter is_problem_line_negated
in if length conjs = 1 then problem else [] end)
@@ -246,7 +260,7 @@

fun nice_name (full_name, _) NONE = (full_name, NONE)
| nice_name (full_name, desired_name) (SOME the_pool) =
-    if String.isPrefix "\$" full_name then
+    if String.isPrefix tptp_special_prefix full_name then
(full_name, SOME the_pool)
else case Symtab.lookup (fst the_pool) full_name of
SOME nice_name => (nice_name, SOME the_pool)```
```--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 00:01:33 2011 +0200
@@ -367,11 +367,12 @@
problem |> maps snd |> map_filter (matching_formula_line_identifier phi)
|> try hd

-(* Syntax: (cnf|fof|tff)\(<num>, <formula_role>, <formula> <extra_arguments>\).
+(* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
+            <formula> <extra_arguments>\).
The <num> could be an identifier, but we assume integers. *)
fun parse_tstp_line problem =
-  ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff")
-      -- \$\$ "(")
+  ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff"
+    || Scan.this_string "thf") -- \$\$ "(")
|-- scan_general_id --| \$\$ "," -- Symbol.scan_id --| \$\$ ","
-- parse_formula -- parse_tstp_extra_arguments --| \$\$ ")" --| \$\$ "."
>> (fn (((num, role), phi), deps) =>```
```--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
@@ -36,9 +36,11 @@
val eN : string
val spassN : string
val vampireN : string
-  val tofof_eN : string
+  val leo2N : string
+  val satallaxN : string
val sine_eN : string
val snarkN : string
+  val tofof_eN : string
val waldmeisterN : string
val z3_atpN : string
val remote_prefix : string
@@ -98,9 +100,11 @@
val spassN = "spass"
val vampireN = "vampire"
val z3_atpN = "z3_atp"
-val tofof_eN = "tofof_e"
+val leo2N = "leo2"
+val satallaxN = "satallax"
val sine_eN = "sine_e"
val snarkN = "snark"
+val tofof_eN = "tofof_e"
val waldmeisterN = "waldmeister"
val remote_prefix = "remote_"

@@ -126,7 +130,8 @@
if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000

val tstp_proof_delims =
-  ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
+  [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
+   ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]

val e_slicesN = "slices"
val e_autoN = "auto"
@@ -207,7 +212,7 @@
e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
" -tAutoDev --silent --cpu-limit=" ^
string_of_int (to_secs (e_bonus ()) timeout),
-   proof_delims = [tstp_proof_delims],
+   proof_delims = tstp_proof_delims,
known_failures =
[(Unprovable, "SZS status: CounterSatisfiable"),
(Unprovable, "SZS status CounterSatisfiable"),
@@ -379,7 +384,7 @@
arguments = fn _ => fn _ => fn timeout => fn _ =>
" -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
^ " -s " ^ the_system system_name system_versions,
-   proof_delims = insert (op =) tstp_proof_delims proof_delims,
+   proof_delims = union (op =) tstp_proof_delims proof_delims,
known_failures =
known_failures @ known_perl_failures @
[(Unprovable, "says Satisfiable"),
@@ -410,16 +415,23 @@
val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
-val remote_tofof_e =
-  remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             Axiom Conjecture [TFF] (K (200, ["simple"]) (* FUDGE *))
+val remote_leo2 =
+  remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
+             (K (200, ["simple"]) (* FUDGE *))
+val remote_satallax =
+  remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
+             (K (200, ["simple"]) (* FUDGE *))
val remote_sine_e =
-  remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [FOF]
+  remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
+             Axiom Conjecture [FOF]
(K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
-             [("refutation.", "end_refutation.")] [] Hypothesis Conjecture
+             [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
[TFF, FOF] (K (250, ["simple"]) (* FUDGE *))
+val remote_tofof_e =
+  remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
+             Axiom Hypothesis [TFF] (K (200, ["simple"]) (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
[("#START OF PROOF", "Proved Goals:")]
@@ -448,8 +460,9 @@
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())

-val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
-            remote_tofof_e, remote_sine_e, remote_snark, remote_waldmeister]
+val atps =
+  [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
+   remote_leo2, remote_sine_e, remote_snark, remote_tofof_e, remote_waldmeister]
val setup = fold add_atp atps

end;```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue May 24 00:01:33 2011 +0200
@@ -372,8 +372,8 @@
fun aux opt_T extra_us u =
case u of
ATerm (a, us) =>
-        if String.isPrefix tff_type_prefix a then
-          @{const True} (* ignore TFF type information *)
+        if String.isPrefix simple_type_prefix a then
+          @{const True} (* ignore TPTP type information *)
else case strip_prefix_and_unascii const_prefix a of
SOME "equal" =>
let val ts = map (aux NONE []) us in```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 24 00:01:33 2011 +0200
@@ -34,7 +34,7 @@
val predicator_base : string
val explicit_app_base : string
val type_pred_base : string
-  val tff_type_prefix : string
+  val simple_type_prefix : string
val type_sys_from_string : string -> type_system
val polymorphism_of_type_sys : type_system -> polymorphism
val level_of_type_sys : type_system -> type_level
@@ -42,7 +42,7 @@
val is_type_sys_fairly_sound : type_system -> bool
val unmangled_const : string -> string * string fo_term list
val translate_atp_fact :
-    Proof.context -> bool -> (string * locality) * thm
+    Proof.context -> format -> bool -> (string * locality) * thm
-> translated_formula option * ((string * locality) * thm)
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_system
@@ -96,9 +96,10 @@
val predicator_base = "hBOOL"
val explicit_app_base = "hAPP"
val type_pred_base = "is"
-val tff_type_prefix = "ty_"
+val simple_type_prefix = "ty_"

-fun make_tff_type s = tff_type_prefix ^ ascii_of s
+fun make_simple_type s =
+  if s = tptp_bool_type then s else simple_type_prefix ^ ascii_of s

(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"
@@ -279,11 +280,12 @@
#> fold term_vars tms
fun close_formula_universally phi = close_universally term_vars phi

-fun fo_term_from_typ (Type (s, Ts)) =
-    ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts)
-  | fo_term_from_typ (TFree (s, _)) =
-    ATerm (`make_fixed_type_var s, [])
-  | fo_term_from_typ (TVar ((x as (s, _)), _)) =
+fun fo_term_from_typ format (Type (s, Ts)) =
+    ATerm (if format = THF andalso s = @{type_name bool} then `I tptp_bool_type
+           else `make_fixed_type_const s,
+          map (fo_term_from_typ format) Ts)
+  | fo_term_from_typ _ (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
+  | fo_term_from_typ _ (TVar ((x as (s, _)), _)) =
ATerm ((make_schematic_type_var x, s), [])

(* This shouldn't clash with anything else. *)
@@ -293,16 +295,16 @@
| generic_mangled_type_name f (ATerm (name, tys)) =
f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
^ ")"
-val mangled_type_name =
-  fo_term_from_typ
-  #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),
+fun mangled_type_name format =
+  fo_term_from_typ format
+  #> (fn ty => (make_simple_type (generic_mangled_type_name fst ty),
generic_mangled_type_name snd ty))

fun generic_mangled_type_suffix f g Ts =
fold_rev (curry (op ^) o g o prefix mangled_type_sep
o generic_mangled_type_name f) Ts ""
-fun mangled_const_name T_args (s, s') =
-  let val ty_args = map fo_term_from_typ T_args in
+fun mangled_const_name format T_args (s, s') =
+  let val ty_args = map (fo_term_from_typ format) T_args in
(s ^ generic_mangled_type_suffix fst ascii_of ty_args,
s' ^ generic_mangled_type_suffix snd I ty_args)
end
@@ -330,14 +332,14 @@
(hd ss, map unmangled_type (tl ss))
end

-fun introduce_proxies tm =
+fun introduce_proxies format tm =
let
fun aux top_level (CombApp (tm1, tm2)) =
CombApp (aux top_level tm1, aux false tm2)
| aux top_level (CombConst (name as (s, s'), T, T_args)) =
(case proxify_const s of
SOME proxy_base =>
-           if top_level then
+           if top_level orelse format = THF then
(case s of
"c_False" => (tptp_false, s')
| "c_True" => (tptp_true, s')
@@ -349,11 +351,11 @@
| aux _ tm = tm
in aux true tm end

-fun combformula_from_prop thy eq_as_iff =
+fun combformula_from_prop thy format eq_as_iff =
let
fun do_term bs t atomic_types =
combterm_from_term thy bs (Envir.eta_contract t)
-      |>> (introduce_proxies #> AAtom)
+      |>> (introduce_proxies format #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q s T t' =
let val s = Name.variant (map fst bs) s in
@@ -449,7 +451,7 @@
in t |> exists_subterm is_Var t ? aux end

(* making fact and conjecture formulas *)
-fun make_formula ctxt eq_as_iff presimp name loc kind t =
+fun make_formula ctxt format eq_as_iff presimp name loc kind t =
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
@@ -464,19 +466,21 @@
|> perhaps (try (HOLogic.dest_Trueprop))
|> introduce_combinators_in_term ctxt kind
|> kind <> Axiom ? freeze_term
-    val (combformula, atomic_types) = combformula_from_prop thy eq_as_iff t []
+    val (combformula, atomic_types) =
+      combformula_from_prop thy format eq_as_iff t []
in
{name = name, locality = loc, kind = kind, combformula = combformula,
atomic_types = atomic_types}
end

-fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, loc), t) =
-  case (keep_trivial, make_formula ctxt eq_as_iff presimp name loc Axiom t) of
+fun make_fact ctxt format keep_trivial eq_as_iff presimp ((name, loc), t) =
+  case (keep_trivial,
+        make_formula ctxt format eq_as_iff presimp name loc Axiom t) of
(false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
NONE
| (_, formula) => SOME formula

-fun make_conjecture ctxt prem_kind ts =
+fun make_conjecture ctxt format prem_kind ts =
let val last = length ts - 1 in
map2 (fn j => fn t =>
let
@@ -488,8 +492,9 @@
if prem_kind = Conjecture then update_combformula mk_anot
else I)
in
-                make_formula ctxt true true (string_of_int j) General kind t
-                |> maybe_negate
+                t |> make_formula ctxt format true true (string_of_int j)
+                                  General kind
+                  |> maybe_negate
end)
(0 upto last) ts
end
@@ -670,7 +675,7 @@
end
handle TYPE _ => T_args

-fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
+fun enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts type_sys =
let
val thy = Proof_Context.theory_of ctxt
fun aux arity (CombApp (tm1, tm2)) =
@@ -706,7 +711,8 @@
Explicit_Type_Args drop_args =>
(name, filtered_T_args drop_args)
| Mangled_Type_Args drop_args =>
-                 (mangled_const_name (filtered_T_args drop_args) name, [])
+                 (mangled_const_name format (filtered_T_args drop_args) name,
+                  [])
| No_Type_Args => (name, [])
end)
|> (fn (name, T_args) => CombConst (name, T, T_args))
@@ -714,13 +720,13 @@
| aux _ tm = tm
in aux 0 end

-fun repair_combterm ctxt nonmono_Ts type_sys sym_tab =
-  introduce_explicit_apps_in_combterm sym_tab
-  #> introduce_predicators_in_combterm sym_tab
-  #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
-fun repair_fact ctxt nonmono_Ts type_sys sym_tab =
+fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =
+  format <> THF ? (introduce_explicit_apps_in_combterm sym_tab
+                   #> introduce_predicators_in_combterm sym_tab)
+  #> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts type_sys
+fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =
update_combformula (formula_map
-      (repair_combterm ctxt nonmono_Ts type_sys sym_tab))
+      (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))

(** Helper facts **)

@@ -734,7 +740,7 @@
|> close_formula_universally, simp_info, NONE)
end

-fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_sys (s, {typ, ...} : sym_info) =
case strip_prefix_and_unascii const_prefix s of
SOME mangled_s =>
let
@@ -755,7 +761,7 @@
| NONE => I)
end)
fun make_facts eq_as_iff =
-        map_filter (make_fact ctxt false eq_as_iff false)
+        map_filter (make_fact ctxt format false eq_as_iff false)
val fairly_sound = is_type_sys_fairly_sound type_sys
in
metis_helpers
@@ -769,13 +775,15 @@
|> make_facts (not needs_fairly_sound))
end
| NONE => []
-fun helper_facts_for_sym_table ctxt type_sys sym_tab =
-  Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab []
+fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
+  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
+                  []

-fun translate_atp_fact ctxt keep_trivial =
-  `(make_fact ctxt keep_trivial true true o apsnd prop_of)
+fun translate_atp_fact ctxt format keep_trivial =
+  `(make_fact ctxt format keep_trivial true true o apsnd prop_of)

-fun translate_formulas ctxt prem_kind type_sys hyp_ts concl_t rich_facts =
+fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t
+                       rich_facts =
let
val thy = Proof_Context.theory_of ctxt
val fact_ts = map (prop_of o snd o snd) rich_facts
@@ -792,7 +800,7 @@
val subs = tfree_classes_of_terms all_ts
val supers = tvar_classes_of_terms all_ts
val tycons = type_consts_of_terms thy all_ts
-    val conjs = make_conjecture ctxt prem_kind (hyp_ts @ [concl_t])
+    val conjs = make_conjecture ctxt format prem_kind (hyp_ts @ [concl_t])
val (supers', arity_clauses) =
if level_of_type_sys type_sys = No_Types then ([], [])
else make_arity_clauses thy tycons supers
@@ -808,9 +816,10 @@

fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot

-fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =
+fun type_pred_combterm ctxt format nonmono_Ts type_sys T tm =
CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T])
-           |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
+           |> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts
+                                                  type_sys,
tm)

fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
@@ -820,44 +829,47 @@
| is_var_nonmonotonic_in_formula pos phi _ name =
formula_fold pos (var_occurs_positively_naked_in_term name) phi false

-fun tag_with_type ctxt nonmono_Ts type_sys T tm =
+fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
CombConst (`make_fixed_const type_tag_name, T --> T, [T])
-  |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
-  |> term_from_combterm ctxt nonmono_Ts type_sys Top_Level
+  |> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts type_sys
+  |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
-and term_from_combterm ctxt nonmono_Ts type_sys site u =
+and term_from_combterm ctxt format nonmono_Ts type_sys =
let
-    val (head, args) = strip_combterm_comb u
-    val (x as (s, _), T_args) =
-        CombConst (name, _, T_args) => (name, T_args)
-      | CombVar (name, _) => (name, [])
-      | CombApp _ => raise Fail "impossible \"CombApp\""
-    val arg_site = if site = Top_Level andalso s = "equal" then Eq_Arg
-                   else Elsewhere
-    val t = ATerm (x, map fo_term_from_typ T_args @
-                      map (term_from_combterm ctxt nonmono_Ts type_sys arg_site)
-                          args)
-    val T = combtyp_of u
-  in
-    t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
-            tag_with_type ctxt nonmono_Ts type_sys T
-          else
-            I)
-  end
-and formula_from_combformula ctxt nonmono_Ts type_sys should_predicate_on_var =
+    fun aux site u =
+      let
+        val (head, args) = strip_combterm_comb u
+        val (x as (s, _), T_args) =
+            CombConst (name, _, T_args) => (name, T_args)
+          | CombVar (name, _) => (name, [])
+          | CombApp _ => raise Fail "impossible \"CombApp\""
+        val arg_site = if site = Top_Level andalso s = "equal" then Eq_Arg
+                       else Elsewhere
+        val t = ATerm (x, map (fo_term_from_typ format) T_args @
+                          map (aux arg_site) args)
+        val T = combtyp_of u
+      in
+        t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
+                tag_with_type ctxt format nonmono_Ts type_sys T
+              else
+                I)
+      end
+  in aux end
+and formula_from_combformula ctxt format nonmono_Ts type_sys
+                             should_predicate_on_var =
let
-    val do_term = term_from_combterm ctxt nonmono_Ts type_sys Top_Level
+    val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
val do_bound_type =
case type_sys of
Simple_Types level =>
-        SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
+        SOME o mangled_type_name format o homogenized_type ctxt nonmono_Ts level
| _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
if should_predicate_on_type ctxt nonmono_Ts type_sys
(fn () => should_predicate_on_var pos phi universal name) T then
CombVar (name, T)
-        |> type_pred_combterm ctxt nonmono_Ts type_sys T
+        |> type_pred_combterm ctxt format nonmono_Ts type_sys T
|> do_term |> AAtom |> SOME
else
NONE
@@ -888,7 +900,7 @@
({combformula, atomic_types, ...} : translated_formula) =
combformula
|> close_combformula_universally
-  |> formula_from_combformula ctxt nonmono_Ts type_sys
+  |> formula_from_combformula ctxt format nonmono_Ts type_sys
is_var_nonmonotonic_in_formula true
|> bound_atomic_types format type_sys atomic_types
|> close_formula_universally
@@ -931,10 +943,10 @@
(fo_literal_from_arity_literal concl_lits))
|> close_formula_universally, intro_info, NONE)

-fun formula_line_for_conjecture ctxt nonmono_Ts type_sys
+fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
({name, kind, combformula, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
-           formula_from_combformula ctxt nonmono_Ts type_sys
+           formula_from_combformula ctxt format nonmono_Ts type_sys
is_var_nonmonotonic_in_formula false
(close_combformula_universally combformula)
|> close_formula_universally, NONE, NONE)
@@ -1027,15 +1039,16 @@
[]
end

-fun decl_line_for_sym ctxt nonmono_Ts level s (s', _, T, pred_sym, ary, _) =
+fun decl_line_for_sym ctxt format nonmono_Ts level s
+                      (s', _, T, pred_sym, ary, _) =
let
val translate_type =
-      mangled_type_name o homogenized_type ctxt nonmono_Ts level
+      mangled_type_name format o homogenized_type ctxt nonmono_Ts level
val (arg_tys, res_ty) =
T |> chop_fun ary |>> map translate_type ||> translate_type
in
Decl (sym_decl_prefix ^ s, (s, s'), arg_tys,
-          if pred_sym then `I tptp_tff_bool_type else res_ty)
+          if pred_sym then `I tptp_bool_type else res_ty)
end

fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
@@ -1059,10 +1072,10 @@
(if n > 1 then "_" ^ string_of_int j else ""), kind,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bounds
-             |> type_pred_combterm ctxt nonmono_Ts type_sys res_T
+             |> type_pred_combterm ctxt format nonmono_Ts type_sys res_T
|> AAtom
|> mk_aquant AForall (bound_names ~~ bound_Ts)
-             |> formula_from_combformula ctxt nonmono_Ts type_sys
+             |> formula_from_combformula ctxt format nonmono_Ts type_sys
(K (K (K (K true)))) true
|> n > 1 ? bound_atomic_types format type_sys (atyps_of T)
|> close_formula_universally
@@ -1082,7 +1095,8 @@
val bound_names =
1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
val bounds = bound_names |> map (fn name => ATerm (name, []))
-    fun const args = ATerm ((s, s'), map fo_term_from_typ T_args @ args)
+    fun const args =
+      ATerm ((s, s'), map (fo_term_from_typ format) T_args @ args)
val atomic_Ts = atyps_of T
fun eq tms =
(if pred_sym then AConn (AIff, map AAtom tms)
@@ -1091,7 +1105,7 @@
|> close_formula_universally
|> maybe_negate
val should_encode = should_encode_type ctxt nonmono_Ts All_Types
-    val tag_with = tag_with_type ctxt nonmono_Ts type_sys
+    val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
if should_encode res_T then
cons (Formula (ident_base ^ "_res", kind,
@@ -1123,7 +1137,8 @@
fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
(s, decls) =
case type_sys of
-    Simple_Types level => map (decl_line_for_sym ctxt nonmono_Ts level s) decls
+    Simple_Types level =>
+    map (decl_line_for_sym ctxt format nonmono_Ts level s) decls
| Preds _ =>
let
val decls =
@@ -1164,22 +1179,23 @@
type_sys)
sym_decl_tab []

-fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
-    union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
-  | add_tff_types_in_formula (AConn (_, phis)) =
-  | add_tff_types_in_formula (AAtom _) = I
+fun add_simple_types_in_formula (AQuant (_, xs, phi)) =
+    union (op =) (map_filter snd xs) #> add_simple_types_in_formula phi
+  | add_simple_types_in_formula (AConn (_, phis)) =
+  | add_simple_types_in_formula (AAtom _) = I

-fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
+fun add_simple_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
union (op =) (res_T :: arg_Ts)
-  | add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) =
+  | add_simple_types_in_problem_line (Formula (_, _, phi, _, _)) =

-fun tff_types_in_problem problem =
-  fold (fold add_tff_types_in_problem_line o snd) problem []
+fun simple_types_in_problem problem =
+  fold (fold add_simple_types_in_problem_line o snd) problem []
+  |> filter_out (String.isPrefix tptp_special_prefix o fst)

-fun decl_line_for_tff_type (s, s') =
-  Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types)
+fun decl_line_for_simple_type (s, s') =
+  Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_type_of_types)

fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
level = Nonmonotonic_Types orelse level = Finite_Types
@@ -1203,14 +1219,15 @@
explicit_apply hyp_ts concl_t facts =
let
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
-      translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts
+      translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts
val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
-    val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab
+    val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
val helpers =
-      repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
+      repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
+                       |> map repair
val lavish_nonmono_Ts =
if null nonmono_Ts orelse
polymorphism_of_type_sys type_sys <> Polymorphic then
@@ -1238,16 +1255,17 @@
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map formula_line_for_arity_clause arity_clauses),
(helpersN, helper_lines),
-       (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
-                    conjs),
+       (conjsN,
+        map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
+            conjs),
(free_typesN,
formula_lines_for_free_types format type_sys (facts @ conjs))]
val problem =
problem
|> (case type_sys of
Simple_Types _ =>
-            cons (type_declsN,
-                  map decl_line_for_tff_type (tff_types_in_problem problem))
+            cons (type_declsN, problem |> simple_types_in_problem
+                                       |> map decl_line_for_simple_type)
| _ => I)
val problem =
problem |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 00:01:33 2011 +0200
@@ -359,8 +359,8 @@

fun untranslated_fact (Untranslated_Fact p) = p
| untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
-fun atp_translated_fact ctxt fact =
-  translate_atp_fact ctxt false (untranslated_fact fact)
+fun atp_translated_fact ctxt format fact =
+  translate_atp_fact ctxt format false (untranslated_fact fact)
fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
| smt_weighted_fact ctxt num_facts (fact, j) =
(untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts
@@ -439,12 +439,11 @@
[Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]

fun adjust_dumb_type_sys formats (Simple_Types level) =
-    if member (op =) formats TFF then (TFF, Simple_Types level)
-    else (FOF, Preds (Mangled_Monomorphic, level, Heavy))
+    (case inter (op =) formats [TFF, THF] of
+       format :: _ => (format, Simple_Types level)
+     | [] => adjust_dumb_type_sys formats
+                                  (Preds (Mangled_Monomorphic, level, Heavy)))
-    (* We could return (TFF, type_sys) in all cases but this would require the
-       TFF provers to accept problems in which constants are implicitly
-       declared. Today neither SNARK nor ToFoF-E satisfy this criterion. *)
if member (op =) formats CNF_UEQ then
(CNF_UEQ, case type_sys of
Tags _ => type_sys
@@ -453,7 +452,11 @@
else if member (op =) formats FOF then
(FOF, type_sys)
else
-      (TFF, Simple_Types All_Types)
+      (* We could return "type_sys" in all cases but this would require the
+         TFF and THF provers to accept problems in which constants are
+         implicitly declared. Today neither SNARK nor ToFoF-E satisfy this
+         criterion. (FIXME: what about LEO-II?) *)
+      (hd formats, Simple_Types All_Types)
fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
| determine_format_and_type_sys best_type_systems formats
@@ -554,7 +557,7 @@
o untranslated_fact)
|> polymorphism_of_type_sys type_sys <> Polymorphic
? monomorphize_facts
-                        |> map (atp_translated_fact ctxt)
+                        |> map (atp_translated_fact ctxt format)
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
((real_ms time_left```
```--- a/src/HOL/ex/tptp_export.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Tue May 24 00:01:33 2011 +0200
@@ -89,13 +89,14 @@

fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name =
let
+    val format = ATP_Problem.FOF
val path = file_name |> Path.explode
val _ = File.write path ""
val facts0 = facts_of thy
val facts =
facts0 |> map_filter (try (fn ((_, loc), (_, th)) =>
-                    Sledgehammer_ATP_Translate.translate_atp_fact ctxt true
-                    ((Thm.get_name_hint th, loc), th)))
+                    Sledgehammer_ATP_Translate.translate_atp_fact ctxt format
+                    true ((Thm.get_name_hint th, loc), th)))
val type_sys =
Sledgehammer_ATP_Translate.Preds
(Sledgehammer_ATP_Translate.Polymorphic,
@@ -104,7 +105,7 @@
Sledgehammer_ATP_Translate.Heavy)
val explicit_apply = false
val (atp_problem, _, _, _, _, _, _) =
-      Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.FOF
+      Sledgehammer_ATP_Translate.prepare_atp_problem ctxt format
ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply []
@{prop False} facts
val infers =```