1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Sun Feb 05 17:43:15 2012 +0100
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Feb 06 23:01:01 2012 +0100
1.3 @@ -1059,25 +1059,26 @@
1.4 $\const{t}(\tau, t)$ becomes a unary function
1.5 $\const{t\_}\tau(t)$.
1.6
1.7 -\item[\labelitemi] \textbf{\textit{mono\_simple} (sound):} Exploits simple
1.8 +\item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native
1.9 first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
1.10 falls back on \textit{mono\_guards}. The problem is monomorphized.
1.11
1.12 -\item[\labelitemi] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
1.13 -higher-order types if the prover supports the THF0 syntax; otherwise, falls back
1.14 -on \textit{mono\_simple} or \textit{mono\_guards}. The problem is monomorphized.
1.15 +\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits
1.16 +native higher-order types if the prover supports the THF0 syntax; otherwise,
1.17 +falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is
1.18 +monomorphized.
1.19
1.20 \item[\labelitemi]
1.21 \textbf{%
1.22 \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
1.23 \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
1.24 -\textit{mono\_simple}? (sound*):} \\
1.25 +\textit{mono\_native}? (sound*):} \\
1.26 The type encodings \textit{poly\_guards}, \textit{poly\_tags},
1.27 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
1.28 -\textit{mono\_tags}, and \textit{mono\_simple} are fully
1.29 +\textit{mono\_tags}, and \textit{mono\_native} are fully
1.30 typed and sound. For each of these, Sledgehammer also provides a lighter,
1.31 virtually sound variant identified by a question mark (`\hbox{?}')\ that detects
1.32 -and erases monotonic types, notably infinite types. (For \textit{mono\_simple},
1.33 +and erases monotonic types, notably infinite types. (For \textit{mono\_native},
1.34 the types are not actually erased but rather replaced by a shared uniform type
1.35 of individuals.) As argument to the \textit{metis} proof method, the question
1.36 mark is replaced by a \hbox{``\textit{\_query\/}''} suffix.
1.37 @@ -1102,14 +1103,14 @@
1.38 \textbf{%
1.39 \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
1.40 \textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
1.41 -\textit{mono\_simple}!, \textit{mono\_simple\_higher}! (mildly unsound):} \\
1.42 +\textit{mono\_native}!, \textit{mono\_native\_higher}! (mildly unsound):} \\
1.43 The type encodings \textit{poly\_guards}, \textit{poly\_tags},
1.44 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
1.45 -\textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}
1.46 +\textit{mono\_tags}, \textit{mono\_native}, and \textit{mono\_native\_higher}
1.47 also admit a mildly unsound (but very efficient) variant identified by an
1.48 exclamation mark (`\hbox{!}') that detects and erases erases all types except
1.49 -those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple}
1.50 -and \textit{mono\_simple\_higher}, the types are not actually erased but rather
1.51 +those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_native}
1.52 +and \textit{mono\_native\_higher}, the types are not actually erased but rather
1.53 replaced by a shared uniform type of individuals.) As argument to the
1.54 \textit{metis} proof method, the exclamation mark is replaced by the suffix
1.55 \hbox{``\textit{\_bang\/}''}.
1.56 @@ -1134,7 +1135,7 @@
1.57 the ATP and should be the most efficient virtually sound encoding for that ATP.
1.58 \end{enum}
1.59
1.60 -For SMT solvers, the type encoding is always \textit{mono\_simple}, irrespective
1.61 +For SMT solvers, the type encoding is always \textit{mono\_native}, irrespective
1.62 of the value of this option.
1.63
1.64 \nopagebreak
2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Feb 05 17:43:15 2012 +0100
2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 06 23:01:01 2012 +0100
2.3 @@ -581,7 +581,7 @@
2.4 relevance_override
2.5 in
2.6 if !reconstructor = "sledgehammer_tac" then
2.7 - sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_simple"
2.8 + sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_native"
2.9 ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
2.10 ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
2.11 ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
3.1 --- a/src/HOL/TPTP/ATP_Theory_Export.thy Sun Feb 05 17:43:15 2012 +0100
3.2 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Mon Feb 06 23:01:01 2012 +0100
3.3 @@ -22,9 +22,9 @@
3.4
3.5 ML {*
3.6 if do_it then
3.7 - "/tmp/axs_mono_simple.dfg"
3.8 + "/tmp/axs_mono_native.dfg"
3.9 |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted)
3.10 - "mono_simple"
3.11 + "mono_native"
3.12 else
3.13 ()
3.14 *}
4.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Feb 05 17:43:15 2012 +0100
4.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Feb 06 23:01:01 2012 +0100
4.3 @@ -72,7 +72,7 @@
4.4 val app_op_name : string
4.5 val type_guard_name : string
4.6 val type_tag_name : string
4.7 - val simple_type_prefix : string
4.8 + val native_type_prefix : string
4.9 val prefixed_predicator_name : string
4.10 val prefixed_app_op_name : string
4.11 val prefixed_type_tag_name : string
4.12 @@ -145,7 +145,7 @@
4.13 val tfree_prefix = "t_"
4.14 val const_prefix = "c_"
4.15 val type_const_prefix = "tc_"
4.16 -val simple_type_prefix = "s_"
4.17 +val native_type_prefix = "n_"
4.18 val class_prefix = "cl_"
4.19
4.20 (* Freshness almost guaranteed! *)
4.21 @@ -631,7 +631,7 @@
4.22 |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
4.23 |> (fn (poly, (level, core)) =>
4.24 case (core, (poly, level)) of
4.25 - ("simple", (SOME poly, _)) =>
4.26 + ("native", (SOME poly, _)) =>
4.27 (case (poly, level) of
4.28 (Polymorphic, All_Types) =>
4.29 Simple_Types (First_Order, Polymorphic, All_Types)
4.30 @@ -641,7 +641,7 @@
4.31 else
4.32 raise Same.SAME
4.33 | _ => raise Same.SAME)
4.34 - | ("simple_higher", (SOME poly, _)) =>
4.35 + | ("native_higher", (SOME poly, _)) =>
4.36 (case (poly, level) of
4.37 (Polymorphic, All_Types) =>
4.38 Simple_Types (Higher_Order, Polymorphic, All_Types)
4.39 @@ -889,17 +889,17 @@
4.40 fun mangled_type format type_enc =
4.41 generic_mangled_type_name fst o ho_term_from_typ format type_enc
4.42
4.43 -fun make_simple_type s =
4.44 +fun make_native_type s =
4.45 if s = tptp_bool_type orelse s = tptp_fun_type orelse
4.46 s = tptp_individual_type then
4.47 s
4.48 else
4.49 - simple_type_prefix ^ ascii_of s
4.50 + native_type_prefix ^ ascii_of s
4.51
4.52 fun ho_type_from_ho_term type_enc pred_sym ary =
4.53 let
4.54 fun to_mangled_atype ty =
4.55 - AType ((make_simple_type (generic_mangled_type_name fst ty),
4.56 + AType ((make_native_type (generic_mangled_type_name fst ty),
4.57 generic_mangled_type_name snd ty), [])
4.58 fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
4.59 | to_poly_atype _ = raise Fail "unexpected type abstraction"
5.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Feb 05 17:43:15 2012 +0100
5.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 06 23:01:01 2012 +0100
5.3 @@ -381,7 +381,7 @@
5.4 fun do_term extra_ts opt_T u =
5.5 case u of
5.6 ATerm (s, us) =>
5.7 - if String.isPrefix simple_type_prefix s then
5.8 + if String.isPrefix native_type_prefix s then
5.9 @{const True} (* ignore TPTP type information *)
5.10 else if s = tptp_equal then
5.11 let val ts = map (do_term [] NONE) us in
6.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Sun Feb 05 17:43:15 2012 +0100
6.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Feb 06 23:01:01 2012 +0100
6.3 @@ -279,9 +279,9 @@
6.4 prem_kind = Hypothesis,
6.5 best_slices = fn ctxt =>
6.6 (* FUDGE *)
6.7 - [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN, false),
6.8 + [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false),
6.9 sosN))),
6.10 - (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN, false),
6.11 + (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false),
6.12 no_sosN)))]
6.13 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
6.14 else I)}
6.15 @@ -306,7 +306,7 @@
6.16 prem_kind = Hypothesis,
6.17 best_slices =
6.18 (* FUDGE *)
6.19 - K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN,
6.20 + K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN,
6.21 false), "")))]}
6.22
6.23 val satallax = (satallaxN, satallax_config)
6.24 @@ -350,9 +350,9 @@
6.25
6.26 val spass = (spassN, spass_config)
6.27
6.28 -val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN, true)
6.29 -val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN, true)
6.30 -val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN, true)
6.31 +val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_native", combsN, true)
6.32 +val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_native", combsN, true)
6.33 +val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_native", liftingN, true)
6.34
6.35 (* Experimental *)
6.36 val spass_new_config : atp_config =
6.37 @@ -420,9 +420,9 @@
6.38 else
6.39 [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
6.40 combs_or_liftingN, false), sosN))),
6.41 - (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN,
6.42 + (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN,
6.43 false), sosN))),
6.44 - (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN,
6.45 + (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN,
6.46 false), no_sosN)))])
6.47 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
6.48 else I)}
6.49 @@ -445,10 +445,10 @@
6.50 prem_kind = Hypothesis,
6.51 best_slices =
6.52 (* FUDGE *)
6.53 - K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN, false), ""))),
6.54 - (0.25, (false, ((125, z3_tff0, "mono_simple", combsN, false), ""))),
6.55 - (0.125, (false, ((62, z3_tff0, "mono_simple", combsN, false), ""))),
6.56 - (0.125, (false, ((31, z3_tff0, "mono_simple", combsN, false), "")))]}
6.57 + K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))),
6.58 + (0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))),
6.59 + (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))),
6.60 + (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))]}
6.61
6.62 val z3_tptp = (z3_tptpN, z3_tptp_config)
6.63
6.64 @@ -469,11 +469,11 @@
6.65 else combsN, false), "")))]}
6.66
6.67 val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
6.68 -val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
6.69 +val dummy_tff1_config = dummy_config dummy_tff1_format "poly_native"
6.70 val dummy_tff1 = (dummy_tff1N, dummy_tff1_config)
6.71
6.72 val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
6.73 -val dummy_thf_config = dummy_config dummy_thf_format "poly_simple_higher"
6.74 +val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
6.75 val dummy_thf = (dummy_thfN, dummy_thf_config)
6.76
6.77
6.78 @@ -547,17 +547,17 @@
6.79 (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *))
6.80 val remote_leo2 =
6.81 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
6.82 - (K (100, leo2_thf0, "mono_simple_higher", liftingN, false) (* FUDGE *))
6.83 + (K (100, leo2_thf0, "mono_native_higher", liftingN, false) (* FUDGE *))
6.84 val remote_satallax =
6.85 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
6.86 - (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN, false)
6.87 + (K (100, satallax_thf0, "mono_native_higher", keep_lamsN, false)
6.88 (* FUDGE *))
6.89 val remote_vampire =
6.90 remotify_atp vampire "Vampire" ["1.8"]
6.91 (K (250, FOF, "mono_guards??", combs_or_liftingN, false) (* FUDGE *))
6.92 val remote_z3_tptp =
6.93 remotify_atp z3_tptp "Z3" ["3.0"]
6.94 - (K (250, z3_tff0, "mono_simple", combsN, false) (* FUDGE *))
6.95 + (K (250, z3_tff0, "mono_native", combsN, false) (* FUDGE *))
6.96 val remote_e_sine =
6.97 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
6.98 Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *))
6.99 @@ -570,11 +570,11 @@
6.100 val remote_snark =
6.101 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
6.102 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
6.103 - (K (100, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
6.104 + (K (100, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *))
6.105 val remote_e_tofof =
6.106 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
6.107 Hypothesis
6.108 - (K (150, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
6.109 + (K (150, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *))
6.110 val remote_waldmeister =
6.111 remote_atp waldmeisterN "Waldmeister" ["710"]
6.112 [("#START OF PROOF", "Proved Goals:")]
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 05 17:43:15 2012 +0100
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 06 23:01:01 2012 +0100
7.3 @@ -163,7 +163,7 @@
7.4 error ("Unknown parameter: " ^ quote name ^ "."))
7.5
7.6
7.7 -(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are
7.8 +(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
7.9 read correctly. *)
7.10 val implode_param = strip_spaces_except_between_idents o space_implode " "
7.11