--- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
@@ -118,7 +118,7 @@
let
val thy = Proof_Context.theory_of ctxt
val prob_file = File.tmp_path (Path.explode "prob")
- val atp = if format = DFG then spassN else eN
+ val atp = case format of DFG _ => spassN | _ => eN
val {exec, arguments, proof_delims, known_failures, ...} =
get_atp thy atp ()
val ord = effective_term_order ctxt atp
@@ -174,7 +174,7 @@
let
val type_enc = type_enc |> type_enc_from_string Strict
|> adjust_type_enc format
- val mono = polymorphism_of_type_enc type_enc <> Raw_Polymorphic
+ val mono = not (is_type_enc_polymorphic type_enc)
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = facts_of thy
@@ -213,7 +213,7 @@
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
val atp_problem =
atp_problem
- |> (format <> DFG ? add_inferences_to_problem infers)
+ |> (case format of DFG _ => I | _ => add_inferences_to_problem infers)
|> order_problem_facts name_ord
val ord = effective_term_order ctxt eN (* dummy *)
val ss = lines_for_atp_problem format ord (K []) atp_problem
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
@@ -28,7 +28,7 @@
gen_prec : bool,
gen_simp : bool}
- datatype polymorphism = Monomorphic | Polymorphic
+ datatype polymorphism = Monomorphic | Polymorphic | Type_Classes
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
@@ -39,7 +39,7 @@
FOF |
TFF of polymorphism * tptp_explicitness |
THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
- DFG
+ DFG of polymorphism
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -160,7 +160,7 @@
gen_prec : bool,
gen_simp : bool}
-datatype polymorphism = Monomorphic | Polymorphic
+datatype polymorphism = Monomorphic | Polymorphic | Type_Classes
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
@@ -171,7 +171,7 @@
FOF |
TFF of polymorphism * tptp_explicitness |
THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
- DFG
+ DFG of polymorphism
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -306,7 +306,7 @@
| is_format_higher_order _ = false
fun is_format_typed (TFF _) = true
| is_format_typed (THF _) = true
- | is_format_typed DFG = true
+ | is_format_typed (DFG _) = true
| is_format_typed _ = false
fun tptp_string_for_role Axiom = "axiom"
@@ -336,7 +336,7 @@
fun str_for_type format ty =
let
- val dfg = (format = DFG)
+ val dfg = case format of DFG _ => true | _ => false
fun str _ (AType (s, [])) =
if dfg andalso s = tptp_individual_type then dfg_individual_type else s
| str _ (AType (s, tys)) =
@@ -438,7 +438,7 @@
| tptp_string_for_format FOF = tptp_fof
| tptp_string_for_format (TFF _) = tptp_tff
| tptp_string_for_format (THF _) = tptp_thf
- | tptp_string_for_format DFG = raise Fail "non-TPTP format"
+ | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format"
fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =
tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
@@ -464,7 +464,7 @@
fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
| binder_atypes _ = []
-fun dfg_string_for_formula gen_simp info =
+fun dfg_string_for_formula poly gen_simp info =
let
fun suffix_tag top_level s =
if top_level then
@@ -492,7 +492,7 @@
| str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
fun str_for_formula top_level (AQuant (q, xs, phi)) =
str_for_quant q ^ "(" ^ "[" ^
- commas (map (string_for_bound_var DFG) xs) ^ "], " ^
+ commas (map (string_for_bound_var (DFG poly)) xs) ^ "], " ^
str_for_formula top_level phi ^ ")"
| str_for_formula top_level (AConn (c, phis)) =
str_for_conn top_level c ^ "(" ^
@@ -503,19 +503,19 @@
fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
| maybe_enclose bef aft s = bef ^ s ^ aft
-fun dfg_lines {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
+fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
let
fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")"
fun ary sym = curry spair sym o arity_of_type
fun fun_typ sym ty =
- "function(" ^ sym ^ ", " ^ string_for_type DFG ty ^ ")."
+ "function(" ^ sym ^ ", " ^ string_for_type (DFG poly) ty ^ ")."
fun pred_typ sym ty =
"predicate(" ^
- commas (sym :: map (string_for_type DFG) (binder_atypes ty)) ^ ")."
+ commas (sym :: map (string_for_type (DFG poly)) (binder_atypes ty)) ^ ")."
fun formula pred (Formula (ident, kind, phi, _, info)) =
if pred kind then
let val rank = extract_isabelle_rank info in
- "formula(" ^ dfg_string_for_formula gen_simp info phi ^
+ "formula(" ^ dfg_string_for_formula poly gen_simp info phi ^
", " ^ ident ^
(if rank = default_rank then "" else ", " ^ string_of_int rank) ^
")." |> SOME
@@ -587,7 +587,9 @@
fun lines_for_atp_problem format ord ord_info problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
- (if format = DFG then dfg_lines ord ord_info else tptp_lines format) problem
+ (case format of
+ DFG poly => dfg_lines poly ord ord_info
+ | _ => tptp_lines format) problem
(** CNF (Metis) and CNF UEQ (Waldmeister) **)
@@ -787,7 +789,7 @@
val avoid_clash =
case format of
TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
- | DFG => avoid_clash_with_dfg_keywords
+ | DFG _ => avoid_clash_with_dfg_keywords
| _ => I
val nice_name = nice_name avoid_clash
fun nice_type (AType (name, tys)) =
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
@@ -22,7 +22,6 @@
General | Induction | Intro | Inductive | Elim | Simp | Def
type stature = scope * status
- datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype strictness = Strict | Non_Strict
datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
datatype type_level =
@@ -86,7 +85,7 @@
val atp_irrelevant_consts : string list
val atp_schematic_consts_of : term -> typ list Symtab.table
val is_type_enc_higher_order : type_enc -> bool
- val polymorphism_of_type_enc : type_enc -> polymorphism
+ val is_type_enc_polymorphic : type_enc -> bool
val level_of_type_enc : type_enc -> type_level
val is_type_enc_sound : type_enc -> bool
val type_enc_from_string : strictness -> string -> type_enc
@@ -126,7 +125,12 @@
datatype order =
First_Order |
Higher_Order of thf_choice
-datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
+datatype phantom_policy = Without_Phantom_Type_Vars | With_Phantom_Type_Vars
+datatype polymorphism =
+ Type_Class_Polymorphic |
+ Raw_Polymorphic of phantom_policy |
+ Raw_Monomorphic |
+ Mangled_Monomorphic
datatype strictness = Strict | Non_Strict
datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
datatype type_level =
@@ -149,6 +153,12 @@
| polymorphism_of_type_enc (Guards (poly, _)) = poly
| polymorphism_of_type_enc (Tags (poly, _)) = poly
+fun is_type_enc_polymorphic type_enc =
+ case polymorphism_of_type_enc type_enc of
+ Raw_Polymorphic _ => true
+ | Type_Class_Polymorphic => true
+ | _ => false
+
fun level_of_type_enc (Native (_, _, level)) = level
| level_of_type_enc (Guards (_, level)) = level
| level_of_type_enc (Tags (_, level)) = level
@@ -173,10 +183,6 @@
val keep_lamsN = "keep_lams"
val lam_liftingN = "lam_lifting" (* legacy *)
-(* It's still unclear whether all TFF1 implementations will support type
- signatures such as "!>[A : $tType] : $o", with phantom type variables. *)
-val avoid_first_order_phantom_type_vars = false
-
val bound_var_prefix = "B_"
val all_bound_var_prefix = "A_"
val exist_bound_var_prefix = "E_"
@@ -606,15 +612,21 @@
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
fun type_enc_from_string strictness s =
- (case try (unprefix "poly_") s of
- SOME s => (SOME Raw_Polymorphic, s)
+ (case try (unprefix "tc_") s of
+ SOME s => (SOME Type_Class_Polymorphic, s)
| NONE =>
- case try (unprefix "raw_mono_") s of
- SOME s => (SOME Raw_Monomorphic, s)
- | NONE =>
- case try (unprefix "mono_") s of
- SOME s => (SOME Mangled_Monomorphic, s)
- | NONE => (NONE, s))
+ 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. *)
+ SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
+ | NONE =>
+ case try (unprefix "raw_mono_") s of
+ SOME s => (SOME Raw_Monomorphic, s)
+ | NONE =>
+ case try (unprefix "mono_") s of
+ SOME s => (SOME Mangled_Monomorphic, s)
+ | NONE => (NONE, s))
||> (fn s =>
case try_unsuffixes queries s of
SOME s =>
@@ -629,26 +641,25 @@
case (core, (poly, level)) of
("native", (SOME poly, _)) =>
(case (poly, level) of
- (Raw_Polymorphic, All_Types) =>
- Native (First_Order, Raw_Polymorphic, All_Types)
- | (Mangled_Monomorphic, _) =>
+ (Mangled_Monomorphic, _) =>
if granularity_of_type_level level = All_Vars then
Native (First_Order, Mangled_Monomorphic, level)
else
raise Same.SAME
- | _ => raise Same.SAME)
+ | (Raw_Monomorphic, _) => raise Same.SAME
+ | (poly, All_Types) => Native (First_Order, poly, All_Types))
| ("native_higher", (SOME poly, _)) =>
(case (poly, level) of
- (Raw_Polymorphic, All_Types) =>
- Native (Higher_Order THF_With_Choice, Raw_Polymorphic, All_Types)
- | (_, Nonmono_Types _) => raise Same.SAME
+ (_, Nonmono_Types _) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
if granularity_of_type_level level = All_Vars then
Native (Higher_Order THF_With_Choice, Mangled_Monomorphic,
level)
else
raise Same.SAME
- | _ => raise Same.SAME)
+ | (Raw_Monomorphic, _) => raise Same.SAME
+ | (poly, All_Types) =>
+ Native (Higher_Order THF_With_Choice, poly, All_Types))
| ("guards", (SOME poly, _)) =>
if poly = Mangled_Monomorphic andalso
granularity_of_type_level level = Undercover_Vars then
@@ -666,7 +677,7 @@
if poly = Mangled_Monomorphic then raise Same.SAME
else Guards (poly, Const_Types true)
| ("erased", (NONE, All_Types (* naja *))) =>
- Guards (Raw_Polymorphic, No_Types)
+ Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
| _ => raise Same.SAME)
handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
@@ -682,7 +693,9 @@
Native (adjust_order choice order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
- | adjust_type_enc DFG (Native (_, _, level)) =
+ | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
+ Native (First_Order, poly, level)
+ | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF _) (Native (_, poly, level)) =
Native (First_Order, poly, level)
@@ -774,7 +787,7 @@
fun lift_lams_part_1 ctxt type_enc =
map close_form #> rpair ctxt
#-> Lambda_Lifting.lift_lambdas
- (SOME ((if polymorphism_of_type_enc type_enc = Raw_Polymorphic then
+ (SOME ((if is_type_enc_polymorphic type_enc then
lam_lifted_poly_prefix
else
lam_lifted_mono_prefix) ^ "_a"))
@@ -839,7 +852,8 @@
if s = type_tag_name then
if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args
else case type_enc of
- Native (_, Raw_Polymorphic, _) => All_Type_Args
+ Native (_, Raw_Polymorphic _, _) => All_Type_Args
+ | Native (_, Type_Class_Polymorphic, _) => All_Type_Args
| Tags (_, All_Types) => No_Type_Args
| _ =>
let val level = level_of_type_enc type_enc in
@@ -877,9 +891,8 @@
fun type_class_formula type_enc class arg =
AAtom (ATerm (class, arg ::
(case type_enc of
- Native (First_Order, Raw_Polymorphic, _) =>
- if avoid_first_order_phantom_type_vars then [ATerm (TYPE_name, [arg])]
- else []
+ Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
+ [ATerm (TYPE_name, [arg])]
| _ => [])))
fun formulas_for_types type_enc add_sorts_on_typ Ts =
[] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
@@ -981,7 +994,7 @@
fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
| to_poly_atype _ = raise Fail "unexpected type abstraction"
val to_atype =
- if polymorphism_of_type_enc type_enc = Raw_Polymorphic then to_poly_atype
+ if is_type_enc_polymorphic type_enc then to_poly_atype
else to_mangled_atype
fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
@@ -1703,7 +1716,9 @@
@{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
|> map (apsnd (map (apsnd zero_var_indexes)))
-fun atype_of_type_vars (Native (_, Raw_Polymorphic, _)) = SOME atype_of_types
+fun atype_of_type_vars (Native (_, Raw_Polymorphic _, _)) = SOME atype_of_types
+ | atype_of_type_vars (Native (_, Type_Class_Polymorphic, _)) =
+ SOME atype_of_types (* ### FIXME *)
| atype_of_type_vars _ = NONE
fun bound_tvars type_enc sorts Ts =
@@ -1730,7 +1745,7 @@
val type_tag = `(make_fixed_const NONE) type_tag_name
fun could_specialize_helpers type_enc =
- polymorphism_of_type_enc type_enc <> Raw_Polymorphic andalso
+ not (is_type_enc_polymorphic type_enc) andalso
level_of_type_enc type_enc <> No_Types
fun should_specialize_helper type_enc t =
could_specialize_helpers type_enc andalso
@@ -2118,7 +2133,7 @@
|> close_formula_universally
|> bound_tvars type_enc true atomic_types, NONE, [])
-fun type_enc_needs_free_types (Native (_, Raw_Polymorphic, _)) = true
+fun type_enc_needs_free_types (Native (_, Raw_Polymorphic _, _)) = true
| type_enc_needs_free_types (Native _) = false
| type_enc_needs_free_types _ = true
@@ -2136,12 +2151,12 @@
(** Symbol declarations **)
-fun decl_line_for_class order s =
+fun decl_line_for_class order phantoms s =
let val name as (s, _) = `make_type_class s in
Decl (sym_decl_prefix ^ s, name,
if order = First_Order then
ATyAbs ([tvar_a_name],
- if avoid_first_order_phantom_type_vars then
+ if phantoms = Without_Phantom_Type_Vars then
AFun (a_itself_atype, bool_atype)
else
bool_atype)
@@ -2151,8 +2166,8 @@
fun decl_lines_for_classes type_enc classes =
case type_enc of
- Native (order, Raw_Polymorphic, _) =>
- map (decl_line_for_class order) classes
+ Native (order, Raw_Polymorphic phantoms, _) =>
+ map (decl_line_for_class order phantoms) classes
| _ => []
fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
@@ -2192,7 +2207,7 @@
fold add_formula_var_types phis
| add_formula_var_types _ = I
fun var_types () =
- if polymorphism_of_type_enc type_enc = Raw_Polymorphic then [tvar_a]
+ if is_type_enc_polymorphic type_enc then [tvar_a]
else fold (ifact_lift add_formula_var_types) (conjs @ facts) []
fun add_undefined_const T =
let
@@ -2217,9 +2232,8 @@
? (fold (fold add_fact_syms) [conjs, facts]
#> fold add_iterm_syms extra_tms
#> (case type_enc of
- Native (First_Order, Raw_Polymorphic, _) =>
- if avoid_first_order_phantom_type_vars then add_TYPE_const ()
- else I
+ Native (First_Order, Raw_Polymorphic phantoms, _) =>
+ phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
| Native _ => I
| _ => fold add_undefined_const (var_types ())))
end
@@ -2284,7 +2298,7 @@
add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift
fun monotonic_types_for_facts ctxt mono type_enc facts =
let val level = level_of_type_enc type_enc in
- [] |> (polymorphism_of_type_enc type_enc = Raw_Polymorphic andalso
+ [] |> (is_type_enc_polymorphic type_enc andalso
is_type_level_monotonicity_based level andalso
granularity_of_type_level level <> Undercover_Vars)
? fold (add_fact_monotonic_types ctxt mono type_enc) facts
@@ -2631,7 +2645,7 @@
Full_App_Op_And_Predicator
else if length facts + length hyp_ts
> app_op_and_predicator_threshold then
- if polymorphism_of_type_enc type_enc = Raw_Polymorphic then Min_App_Op
+ if is_type_enc_polymorphic type_enc then Min_App_Op
else Sufficient_App_Op
else
Sufficient_App_Op_And_Predicator
@@ -2680,6 +2694,8 @@
map (formula_line_for_fact ctxt fact_prefix ascii_of (not exporter)
(not exporter) mono type_enc (rank_of_fact_num num_facts))
(0 upto num_facts - 1 ~~ facts)
+ val class_rel_lines =
+ map (formula_line_for_class_rel_clause type_enc) class_rel_clauses
val helper_lines =
0 upto length helpers - 1 ~~ helpers
|> map (formula_line_for_fact ctxt helper_prefix I false true mono
@@ -2689,8 +2705,7 @@
[(explicit_declsN, class_decl_lines @ sym_decl_lines),
(uncurried_alias_eqsN, uncurried_alias_eq_lines),
(factsN, fact_lines),
- (class_relsN,
- map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
+ (class_relsN, class_rel_lines),
(aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
(helpersN, helper_lines),
(free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)),
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
@@ -54,6 +54,7 @@
val satallaxN : string
val snarkN : string
val spassN : string
+ val spass_polyN : string
val vampireN : string
val waldmeisterN : string
val z3_tptpN : string
@@ -149,6 +150,7 @@
val satallaxN = "satallax"
val snarkN = "snark"
val spassN = "spass"
+val spass_polyN = "spass_poly"
val vampireN = "vampire"
val waldmeisterN = "waldmeister"
val z3_tptpN = "z3_tptp"
@@ -409,14 +411,14 @@
prem_role = Conjecture,
best_slices = fn _ =>
(* FUDGE *)
- [(0.1667, (false, ((150, DFG, "mono_native", combsN, true), ""))),
- (0.1667, (false, ((500, DFG, "mono_native", liftingN, true), spass_H2SOS))),
- (0.1666, (false, ((50, DFG, "mono_native", liftingN, true), spass_H2LR0LT0))),
- (0.1000, (false, ((250, DFG, "mono_native", combsN, true), spass_H2NuVS0))),
- (0.1000, (false, ((1000, DFG, "mono_native", liftingN, true), spass_H1SOS))),
- (0.1000, (false, ((150, DFG, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
- (0.1000, (false, ((300, DFG, "mono_native", combsN, true), spass_H2SOS))),
- (0.1000, (false, ((100, DFG, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
+ [(0.1667, (false, ((150, DFG Monomorphic, "mono_native", combsN, true), ""))),
+ (0.1667, (false, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS))),
+ (0.1666, (false, ((50, DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0))),
+ (0.1000, (false, ((250, DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0))),
+ (0.1000, (false, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS))),
+ (0.1000, (false, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
+ (0.1000, (false, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS))),
+ (0.1000, (false, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -495,7 +497,7 @@
val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
-(* Not really a prover: Experimental Polymorphic TFF and THF output *)
+(* Not really a prover: Experimental Polymorphic THF and DFG output *)
fun dummy_config format type_enc : atp_config =
{exec = (["ISABELLE_ATP"], "scripts/dummy_atp"),
@@ -516,6 +518,9 @@
val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
+val spass_poly_format = DFG Polymorphic
+val spass_poly_config = dummy_config spass_poly_format "tc_native"
+val spass_poly = (spass_polyN, fn () => spass_poly_config)
(* Remote ATP invocation via SystemOnTPTP *)
@@ -667,8 +672,8 @@
end
val atps=
- [alt_ergo, e, leo2, dummy_thf, satallax, spass, vampire, z3_tptp, remote_e,
- remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
+ [alt_ergo, e, leo2, satallax, spass, spass_poly, vampire, z3_tptp, dummy_thf,
+ remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
remote_waldmeister]
--- a/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200
@@ -211,7 +211,7 @@
fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
let
val (conj_clauses, fact_clauses) =
- if polymorphism_of_type_enc type_enc = Raw_Polymorphic then
+ if is_type_enc_polymorphic type_enc then
(conj_clauses, fact_clauses)
else
conj_clauses @ fact_clauses
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200
@@ -717,7 +717,7 @@
|> not sound
? filter_out (is_dangerous_prop ctxt o prop_of o snd)
|> take num_facts
- |> polymorphism_of_type_enc type_enc <> Raw_Polymorphic
+ |> not (is_type_enc_polymorphic type_enc)
? monomorphize_facts
|> map (apsnd prop_of)
|> prepare_atp_problem ctxt format prem_role type_enc