--- 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) =
- case head of
- 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) =
+ case head of
+ 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
val add_formula_for_res =
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)) =
- fold add_tff_types_in_formula 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)) =
+ fold add_simple_types_in_formula 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_tff_types_in_formula phi
+ | add_simple_types_in_problem_line (Formula (_, _, phi, _, _)) =
+ add_simple_types_in_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)))
| adjust_dumb_type_sys formats type_sys =
- (* 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) =
adjust_dumb_type_sys formats 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 =