use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
--- a/src/HOL/TPTP/atp_theory_export.ML Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Oct 24 12:43:33 2013 +0200
@@ -34,8 +34,8 @@
val prefix = Library.prefix
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
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Oct 24 12:43:33 2013 +0200
@@ -33,14 +33,13 @@
datatype polymorphism = Monomorphic | Polymorphic
datatype thf_choice = THF_Without_Choice | THF_With_Choice
- datatype thf_defs = THF_Without_Defs | THF_With_Defs
datatype atp_format =
CNF |
CNF_UEQ |
FOF |
TFF of polymorphism |
- THF of polymorphism * thf_choice * thf_defs |
+ THF of polymorphism * thf_choice |
DFG of polymorphism
datatype atp_formula_role =
@@ -179,14 +178,13 @@
datatype polymorphism = Monomorphic | Polymorphic
datatype thf_choice = THF_Without_Choice | THF_With_Choice
-datatype thf_defs = THF_Without_Defs | THF_With_Defs
datatype atp_format =
CNF |
CNF_UEQ |
FOF |
TFF of polymorphism |
- THF of polymorphism * thf_choice * thf_defs |
+ THF of polymorphism * thf_choice |
DFG of polymorphism
datatype atp_formula_role =
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Oct 24 12:43:33 2013 +0200
@@ -697,11 +697,9 @@
Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
-fun adjust_type_enc (THF (Polymorphic, choice, _))
- (Native (order, poly, level)) =
+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, _))
- (Native (order, _, level)) =
+ | adjust_type_enc (THF (Monomorphic, choice)) (Native (order, _, level)) =
Native (adjust_order choice order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
@@ -1317,7 +1315,7 @@
atomic_types = atomic_Ts}
end
-fun is_format_with_defs (THF (_, _, THF_With_Defs)) = true
+fun is_format_with_defs (THF _) = true
| is_format_with_defs _ = false
fun make_fact ctxt format type_enc iff_for_eq
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Oct 24 12:43:33 2013 +0200
@@ -211,7 +211,7 @@
(* agsyHOL *)
-val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
+val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice)
val agsyhol_config : atp_config =
{exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
@@ -461,7 +461,7 @@
(* LEO-II supports definitions, but it performs significantly better on our
benchmarks when they are not used. *)
-val leo2_thf0 = THF (Monomorphic, THF_Without_Choice, THF_Without_Defs)
+val leo2_thf0 = THF (Monomorphic, THF_Without_Choice)
val leo2_config : atp_config =
{exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
@@ -488,7 +488,7 @@
(* Satallax *)
(* Choice is disabled until there is proper reconstruction for it. *)
-val satallax_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
+val satallax_thf0 = THF (Monomorphic, THF_Without_Choice)
val satallax_config : atp_config =
{exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
@@ -653,7 +653,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, THF_With_Choice, THF_With_Defs)
+val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
val dummy_thf_config =
dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)