--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jun 16 19:40:59 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jun 16 19:41:00 2014 +0200
@@ -608,9 +608,8 @@
SOME s => (SOME Type_Class_Polymorphic, s)
| NONE =>
(case try (unprefix "poly_") s of
- (* It's still unclear whether all TFF1 implementations will support
- type signatures such as "!>[A : $tType] : $o", with phantom type
- variables. *)
+ (* It's still unclear whether all TFF1 implementations will support type signatures such as
+ "!>[A : $tType] : $o", with phantom type variables. *)
SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
| NONE =>
(case try (unprefix "raw_mono_") s of
@@ -651,15 +650,13 @@
Native (Higher_Order THF_With_Choice, poly, All_Types)
| _ => raise Same.SAME)
| ("guards", (SOME poly, _)) =>
- if (poly = Mangled_Monomorphic andalso
- level = Undercover_Types) orelse
+ if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
poly = Type_Class_Polymorphic then
raise Same.SAME
else
Guards (poly, level)
| ("tags", (SOME poly, _)) =>
- if (poly = Mangled_Monomorphic andalso
- level = Undercover_Types) orelse
+ if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
poly = Type_Class_Polymorphic then
raise Same.SAME
else
@@ -668,8 +665,7 @@
if poly = Type_Class_Polymorphic then raise Same.SAME
else Guards (poly, Const_Types Without_Ctr_Optim)
| ("args", (SOME poly, Nonmono_Types (_, Uniform) (* naja *))) =>
- if poly = Mangled_Monomorphic orelse
- poly = Type_Class_Polymorphic then
+ if poly = Mangled_Monomorphic orelse poly = Type_Class_Polymorphic then
raise Same.SAME
else
Guards (poly, Const_Types With_Ctr_Optim)
@@ -682,8 +678,7 @@
Higher_Order THF_Without_Choice
| adjust_order _ type_enc = type_enc
-fun no_type_classes Type_Class_Polymorphic =
- Raw_Polymorphic With_Phantom_Type_Vars
+fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
fun adjust_type_enc (THF (Polymorphic, choice)) (Native (order, poly, level)) =
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 19:40:59 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 19:41:00 2014 +0200
@@ -717,6 +717,15 @@
(remote_prefix ^ name,
remotify_config system_name system_versions best_slice o config)
+fun gen_remote_waldmeister name =
+ remote_atp name "Waldmeister" ["710"]
+ [("#START OF PROOF", "Proved Goals:")]
+ [(OutOfResources, "Too many function symbols"),
+ (Inappropriate, "**** Unexpected end of file."),
+ (Crashed, "Unrecoverable Segmentation Fault")]
+ Hypothesis
+ (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
+
val explicit_tff0 = TFF Monomorphic
val remote_agsyhol =
@@ -750,14 +759,8 @@
val remote_e_tofof =
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
(K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
-val remote_waldmeister =
- remote_atp waldmeisterN "Waldmeister" ["710"]
- [("#START OF PROOF", "Proved Goals:")]
- [(OutOfResources, "Too many function symbols"),
- (Inappropriate, "**** Unexpected end of file."),
- (Crashed, "Unrecoverable Segmentation Fault")]
- Hypothesis
- (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
+val remote_waldmeister = gen_remote_waldmeister waldmeisterN
+val remote_waldmeister_new = gen_remote_waldmeister waldmeister_newN
(* Setup *)
@@ -796,7 +799,7 @@
[agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
z3_tptp, zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
- remote_spass_pirate, remote_waldmeister]
+ remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
val _ = Theory.setup (fold add_atp atps)