Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
--- a/src/HOL/TPTP/atp_theory_export.ML Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Aug 13 10:26:56 2013 +0200
@@ -33,12 +33,12 @@
val fact_name_of = prefix fact_prefix o ascii_of
-fun atp_of_format (THF (Polymorphic, _, _, _)) = dummy_thfN
- | atp_of_format (THF (Monomorphic, _, _, _)) = satallaxN
+fun atp_of_format (THF (Polymorphic, _, _)) = dummy_thfN
+ | atp_of_format (THF (Monomorphic, _, _)) = satallaxN
| atp_of_format (DFG Polymorphic) = spass_polyN
| atp_of_format (DFG Monomorphic) = spassN
- | atp_of_format (TFF (Polymorphic, _)) = alt_ergoN
- | atp_of_format (TFF (Monomorphic, _)) = vampireN
+ | atp_of_format (TFF Polymorphic) = alt_ergoN
+ | atp_of_format (TFF Monomorphic) = vampireN
| atp_of_format FOF = eN
| atp_of_format CNF_UEQ = waldmeisterN
| atp_of_format CNF = eN
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 13 10:26:56 2013 +0200
@@ -30,7 +30,6 @@
gen_simp : bool}
datatype polymorphism = Monomorphic | Polymorphic
- datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_choice = THF_Without_Choice | THF_With_Choice
datatype thf_defs = THF_Without_Defs | THF_With_Defs
@@ -38,8 +37,8 @@
CNF |
CNF_UEQ |
FOF |
- TFF of polymorphism * tptp_explicitness |
- THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
+ TFF of polymorphism |
+ THF of polymorphism * thf_choice * thf_defs |
DFG of polymorphism
datatype formula_role =
@@ -175,7 +174,6 @@
gen_simp : bool}
datatype polymorphism = Monomorphic | Polymorphic
-datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_choice = THF_Without_Choice | THF_With_Choice
datatype thf_defs = THF_Without_Defs | THF_With_Defs
@@ -183,8 +181,8 @@
CNF |
CNF_UEQ |
FOF |
- TFF of polymorphism * tptp_explicitness |
- THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
+ TFF of polymorphism |
+ THF of polymorphism * thf_choice * thf_defs |
DFG of polymorphism
datatype formula_role =
@@ -911,7 +909,7 @@
if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
val avoid_clash =
case format of
- TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
+ TFF Polymorphic => avoid_clash_with_alt_ergo_type_vars
| DFG _ => avoid_clash_with_dfg_keywords
| _ => I
val nice_name = nice_name avoid_clash
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Aug 13 10:26:56 2013 +0200
@@ -688,13 +688,13 @@
Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
-fun adjust_type_enc (THF (Polymorphic, _, choice, _))
+fun adjust_type_enc (THF (Polymorphic, choice, _))
(Native (order, poly, level)) =
Native (adjust_order choice order, no_type_classes poly, level)
- | adjust_type_enc (THF (Monomorphic, _, choice, _))
+ | adjust_type_enc (THF (Monomorphic, choice, _))
(Native (order, _, level)) =
Native (adjust_order choice order, Mangled_Monomorphic, level)
- | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) =
+ | adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
Native (First_Order, poly, level)
@@ -1308,7 +1308,7 @@
atomic_types = atomic_Ts}
end
-fun is_format_with_defs (THF (_, _, _, THF_With_Defs)) = true
+fun is_format_with_defs (THF (_, _, THF_With_Defs)) = true
| is_format_with_defs _ = false
fun make_fact ctxt format type_enc iff_for_eq
@@ -2652,7 +2652,7 @@
o uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0
sym_tab) sym_tab
-val implicit_declsN = "Should-be-implicit typings"
+val implicit_declsN = "Could-be-implicit typings"
val explicit_declsN = "Explicit typings"
val uncurried_alias_eqsN = "Uncurried aliases"
val factsN = "Relevant facts"
@@ -2842,8 +2842,6 @@
CNF => ensure_cnf_problem
| CNF_UEQ => filter_cnf_ueq_problem
| FOF => I
- | TFF (_, TPTP_Implicit) => I
- | THF (_, TPTP_Implicit, _, _) => I
| _ => declare_undeclared_in_problem implicit_declsN)
val (problem, pool) = problem |> nice_atp_problem readable_names format
fun add_sym_ary (s, {min_ary, ...} : sym_info) =
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 13 10:26:56 2013 +0200
@@ -211,8 +211,7 @@
(* agsyHOL *)
-val agsyhol_thf0 =
- THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
+val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
val agsyhol_config : atp_config =
{exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
@@ -233,7 +232,7 @@
(* Alt-Ergo *)
-val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
+val alt_ergo_tff1 = TFF Polymorphic
val alt_ergo_config : atp_config =
{exec = K (["WHY3_HOME"], ["why3"]),
@@ -462,8 +461,7 @@
(* LEO-II supports definitions, but it performs significantly better on our
benchmarks when they are not used. *)
-val leo2_thf0 =
- THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
+val leo2_thf0 = THF (Monomorphic, THF_Without_Choice, THF_Without_Defs)
val leo2_config : atp_config =
{exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
@@ -490,8 +488,7 @@
(* Satallax *)
(* Choice is disabled until there is proper reconstruction for it. *)
-val satallax_thf0 =
- THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
+val satallax_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
val satallax_config : atp_config =
{exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
@@ -568,7 +565,7 @@
fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
-val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
+val vampire_tff0 = TFF Monomorphic
val vampire_config : atp_config =
{exec = K (["VAMPIRE_HOME"], ["vampire"]),
@@ -620,7 +617,7 @@
(* Z3 with TPTP syntax (half experimental, half legacy) *)
-val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
+val z3_tff0 = TFF Monomorphic
val z3_tptp_config : atp_config =
{exec = K (["Z3_HOME"], ["z3"]),
@@ -657,8 +654,7 @@
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
-val dummy_thf_format =
- THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
+val dummy_thf_format = THF (Polymorphic, THF_With_Choice, THF_With_Defs)
val dummy_thf_config =
dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
@@ -743,7 +739,7 @@
(remote_prefix ^ name,
remotify_config system_name system_versions best_slice o config)
-val explicit_tff0 = TFF (Monomorphic, TPTP_Explicit)
+val explicit_tff0 = TFF Monomorphic
val remote_agsyhol =
remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
@@ -764,7 +760,7 @@
remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
(K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_vampire =
- remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
+ remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5", "1.8"]
(K (((250, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Tue Aug 13 10:26:56 2013 +0200
@@ -13,7 +13,6 @@
bool -> preplay_interface -> isar_proof -> isar_proof
end
-
structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
struct
@@ -107,5 +106,4 @@
snd (do_proof proof)
end
-
end