# HG changeset patch # User blanchet # Date 1306188093 -7200 # Node ID 3b50fdeb6cfc8e07f4acde19d8028de5d35ed5f2 # Parent f30ae82cb62e8b18aa552f241a8cf5ead012434d started adding support for THF output (but no lambdas) diff -r f30ae82cb62e -r 3b50fdeb6cfc src/HOL/Tools/ATP/atp_problem.ML --- 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) diff -r f30ae82cb62e -r 3b50fdeb6cfc src/HOL/Tools/ATP/atp_proof.ML --- 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)\(, , \). +(* Syntax: (cnf|fof|tff|thf)\(, , + \). The 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) => diff -r f30ae82cb62e -r 3b50fdeb6cfc src/HOL/Tools/ATP/atp_systems.ML --- 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; diff -r f30ae82cb62e -r 3b50fdeb6cfc src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- 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 diff -r f30ae82cb62e -r 3b50fdeb6cfc src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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) diff -r f30ae82cb62e -r 3b50fdeb6cfc src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r f30ae82cb62e -r 3b50fdeb6cfc src/HOL/ex/tptp_export.ML --- 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 =