# HG changeset patch # User blanchet # Date 1328565661 -3600 # Node ID e9c90516bc0de846b5688b3d048bf10ec1ececa3 # Parent 6d2af424d0f811b9303a224b82188a30bffefcd2 renamed type encoding diff -r 6d2af424d0f8 -r e9c90516bc0d doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Sun Feb 05 17:43:15 2012 +0100 +++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Feb 06 23:01:01 2012 +0100 @@ -1059,25 +1059,26 @@ $\const{t}(\tau, t)$ becomes a unary function $\const{t\_}\tau(t)$. -\item[\labelitemi] \textbf{\textit{mono\_simple} (sound):} Exploits simple +\item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native first-order types if the prover supports the TFF0 or THF0 syntax; otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized. -\item[\labelitemi] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple -higher-order types if the prover supports the THF0 syntax; otherwise, falls back -on \textit{mono\_simple} or \textit{mono\_guards}. The problem is monomorphized. +\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits +native higher-order types if the prover supports the THF0 syntax; otherwise, +falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is +monomorphized. \item[\labelitemi] \textbf{% \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\ \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\ -\textit{mono\_simple}? (sound*):} \\ +\textit{mono\_native}? (sound*):} \\ The type encodings \textit{poly\_guards}, \textit{poly\_tags}, \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, -\textit{mono\_tags}, and \textit{mono\_simple} are fully +\textit{mono\_tags}, and \textit{mono\_native} are fully typed and sound. For each of these, Sledgehammer also provides a lighter, virtually sound variant identified by a question mark (`\hbox{?}')\ that detects -and erases monotonic types, notably infinite types. (For \textit{mono\_simple}, +and erases monotonic types, notably infinite types. (For \textit{mono\_native}, the types are not actually erased but rather replaced by a shared uniform type of individuals.) As argument to the \textit{metis} proof method, the question mark is replaced by a \hbox{``\textit{\_query\/}''} suffix. @@ -1102,14 +1103,14 @@ \textbf{% \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\ \textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\ -\textit{mono\_simple}!, \textit{mono\_simple\_higher}! (mildly unsound):} \\ +\textit{mono\_native}!, \textit{mono\_native\_higher}! (mildly unsound):} \\ The type encodings \textit{poly\_guards}, \textit{poly\_tags}, \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards}, -\textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher} +\textit{mono\_tags}, \textit{mono\_native}, and \textit{mono\_native\_higher} also admit a mildly unsound (but very efficient) variant identified by an exclamation mark (`\hbox{!}') that detects and erases erases all types except -those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple} -and \textit{mono\_simple\_higher}, the types are not actually erased but rather +those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_native} +and \textit{mono\_native\_higher}, the types are not actually erased but rather replaced by a shared uniform type of individuals.) As argument to the \textit{metis} proof method, the exclamation mark is replaced by the suffix \hbox{``\textit{\_bang\/}''}. @@ -1134,7 +1135,7 @@ the ATP and should be the most efficient virtually sound encoding for that ATP. \end{enum} -For SMT solvers, the type encoding is always \textit{mono\_simple}, irrespective +For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective of the value of this option. \nopagebreak diff -r 6d2af424d0f8 -r e9c90516bc0d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Feb 05 17:43:15 2012 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 06 23:01:01 2012 +0100 @@ -581,7 +581,7 @@ relevance_override in if !reconstructor = "sledgehammer_tac" then - sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_simple" + sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_native" ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??" ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??" ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags" diff -r 6d2af424d0f8 -r e9c90516bc0d src/HOL/TPTP/ATP_Theory_Export.thy --- a/src/HOL/TPTP/ATP_Theory_Export.thy Sun Feb 05 17:43:15 2012 +0100 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Mon Feb 06 23:01:01 2012 +0100 @@ -22,9 +22,9 @@ ML {* if do_it then - "/tmp/axs_mono_simple.dfg" + "/tmp/axs_mono_native.dfg" |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted) - "mono_simple" + "mono_native" else () *} diff -r 6d2af424d0f8 -r e9c90516bc0d src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Feb 05 17:43:15 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Feb 06 23:01:01 2012 +0100 @@ -72,7 +72,7 @@ val app_op_name : string val type_guard_name : string val type_tag_name : string - val simple_type_prefix : string + val native_type_prefix : string val prefixed_predicator_name : string val prefixed_app_op_name : string val prefixed_type_tag_name : string @@ -145,7 +145,7 @@ val tfree_prefix = "t_" val const_prefix = "c_" val type_const_prefix = "tc_" -val simple_type_prefix = "s_" +val native_type_prefix = "n_" val class_prefix = "cl_" (* Freshness almost guaranteed! *) @@ -631,7 +631,7 @@ |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries) |> (fn (poly, (level, core)) => case (core, (poly, level)) of - ("simple", (SOME poly, _)) => + ("native", (SOME poly, _)) => (case (poly, level) of (Polymorphic, All_Types) => Simple_Types (First_Order, Polymorphic, All_Types) @@ -641,7 +641,7 @@ else raise Same.SAME | _ => raise Same.SAME) - | ("simple_higher", (SOME poly, _)) => + | ("native_higher", (SOME poly, _)) => (case (poly, level) of (Polymorphic, All_Types) => Simple_Types (Higher_Order, Polymorphic, All_Types) @@ -889,17 +889,17 @@ fun mangled_type format type_enc = generic_mangled_type_name fst o ho_term_from_typ format type_enc -fun make_simple_type s = +fun make_native_type s = if s = tptp_bool_type orelse s = tptp_fun_type orelse s = tptp_individual_type then s else - simple_type_prefix ^ ascii_of s + native_type_prefix ^ ascii_of s fun ho_type_from_ho_term type_enc pred_sym ary = let fun to_mangled_atype ty = - AType ((make_simple_type (generic_mangled_type_name fst ty), + AType ((make_native_type (generic_mangled_type_name fst ty), generic_mangled_type_name snd ty), []) fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys) | to_poly_atype _ = raise Fail "unexpected type abstraction" diff -r 6d2af424d0f8 -r e9c90516bc0d src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Feb 05 17:43:15 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 06 23:01:01 2012 +0100 @@ -381,7 +381,7 @@ fun do_term extra_ts opt_T u = case u of ATerm (s, us) => - if String.isPrefix simple_type_prefix s then + if String.isPrefix native_type_prefix s then @{const True} (* ignore TPTP type information *) else if s = tptp_equal then let val ts = map (do_term [] NONE) us in diff -r 6d2af424d0f8 -r e9c90516bc0d src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun Feb 05 17:43:15 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Feb 06 23:01:01 2012 +0100 @@ -279,9 +279,9 @@ prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN, false), + [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false), sosN))), - (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN, false), + (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false), no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -306,7 +306,7 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN, + K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]} val satallax = (satallaxN, satallax_config) @@ -350,9 +350,9 @@ val spass = (spassN, spass_config) -val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN, true) -val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN, true) -val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN, true) +val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_native", combsN, true) +val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_native", combsN, true) +val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_native", liftingN, true) (* Experimental *) val spass_new_config : atp_config = @@ -420,9 +420,9 @@ else [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))), - (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN, + (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))), - (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN, + (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -445,10 +445,10 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN, false), ""))), - (0.25, (false, ((125, z3_tff0, "mono_simple", combsN, false), ""))), - (0.125, (false, ((62, z3_tff0, "mono_simple", combsN, false), ""))), - (0.125, (false, ((31, z3_tff0, "mono_simple", combsN, false), "")))]} + K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))), + (0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))), + (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))), + (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))]} val z3_tptp = (z3_tptpN, z3_tptp_config) @@ -469,11 +469,11 @@ else combsN, false), "")))]} val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit) -val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple" +val dummy_tff1_config = dummy_config dummy_tff1_format "poly_native" val dummy_tff1 = (dummy_tff1N, dummy_tff1_config) val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice) -val dummy_thf_config = dummy_config dummy_thf_format "poly_simple_higher" +val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher" val dummy_thf = (dummy_thfN, dummy_thf_config) @@ -547,17 +547,17 @@ (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"] - (K (100, leo2_thf0, "mono_simple_higher", liftingN, false) (* FUDGE *)) + (K (100, leo2_thf0, "mono_native_higher", liftingN, false) (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.1", "2.0", "2"] - (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN, false) + (K (100, satallax_thf0, "mono_native_higher", keep_lamsN, false) (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["1.8"] (K (250, FOF, "mono_guards??", combs_or_liftingN, false) (* FUDGE *)) val remote_z3_tptp = remotify_atp z3_tptp "Z3" ["3.0"] - (K (250, z3_tff0, "mono_simple", combsN, false) (* FUDGE *)) + (K (250, z3_tff0, "mono_native", combsN, false) (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *)) @@ -570,11 +570,11 @@ val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis - (K (100, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *)) + (K (100, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *)) val remote_e_tofof = remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom Hypothesis - (K (150, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *)) + (K (150, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] diff -r 6d2af424d0f8 -r e9c90516bc0d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 05 17:43:15 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 06 23:01:01 2012 +0100 @@ -163,7 +163,7 @@ error ("Unknown parameter: " ^ quote name ^ ".")) -(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are +(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) val implode_param = strip_spaces_except_between_idents o space_implode " "