--- a/src/HOL/TPTP/ATP_Theory_Export.thy Mon Jun 25 18:21:18 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy Tue Jun 26 11:14:39 2012 +0200
@@ -23,8 +23,7 @@
ML {*
if do_it then
"/tmp/axs_mono_native.dfg"
- |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted)
- "mono_native"
+ |> generate_tptp_inference_file_for_theory ctxt thy DFG "mono_native"
else
()
*}
--- a/src/HOL/TPTP/atp_theory_export.ML Mon Jun 25 18:21:18 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 = case format of DFG _ => spassN | _ => eN
+ val atp = if format = DFG then spassN else eN
val {exec, arguments, proof_delims, known_failures, ...} =
get_atp thy atp ()
val ord = effective_term_order ctxt atp
@@ -213,7 +213,7 @@
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
val atp_problem =
atp_problem
- |> (case format of DFG _ => I | _ => add_inferences_to_problem infers)
+ |> (format <> DFG ? 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 Mon Jun 25 18:21:18 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
@@ -32,7 +32,6 @@
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
- datatype dfg_flavor = DFG_Unsorted | DFG_Sorted
datatype atp_format =
CNF |
@@ -40,7 +39,7 @@
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
- DFG of dfg_flavor
+ DFG
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -165,7 +164,6 @@
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
-datatype dfg_flavor = DFG_Unsorted | DFG_Sorted
datatype atp_format =
CNF |
@@ -173,7 +171,7 @@
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
- DFG of dfg_flavor
+ DFG
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -229,8 +227,7 @@
val default_rank = 1000
val default_term_order_weight = 1
-(* Currently, only newer versions of SPASS, with sorted DFG format support, can
- process Isabelle metainformation. *)
+(* Currently, only SPASS 3.8ds can process Isabelle metainformation. *)
fun isabelle_info status rank =
[] |> rank <> default_rank
? cons (ATerm (isabelle_info_prefix ^ rankN,
@@ -309,7 +306,7 @@
| is_format_higher_order _ = false
fun is_format_typed (TFF _) = true
| is_format_typed (THF _) = true
- | is_format_typed (DFG DFG_Sorted) = true
+ | is_format_typed DFG = true
| is_format_typed _ = false
fun tptp_string_for_role Axiom = "axiom"
@@ -339,7 +336,7 @@
fun str_for_type format ty =
let
- val dfg = (format = DFG DFG_Sorted)
+ val dfg = (format = DFG)
fun str _ (AType (s, [])) =
if dfg andalso s = tptp_individual_type then dfg_individual_type else s
| str _ (AType (s, tys)) =
@@ -441,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 ^
@@ -467,10 +464,10 @@
fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
| binder_atypes _ = []
-fun dfg_string_for_formula gen_simp flavor info =
+fun dfg_string_for_formula gen_simp info =
let
fun suffix_tag top_level s =
- if flavor = DFG_Sorted andalso top_level then
+ if top_level then
case extract_isabelle_status info of
SOME s' => if s' = defN then s ^ ":lt"
else if s' = simpN andalso gen_simp then s ^ ":lr"
@@ -495,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 flavor)) xs) ^ "], " ^
+ commas (map (string_for_bound_var DFG) xs) ^ "], " ^
str_for_formula top_level phi ^ ")"
| str_for_formula top_level (AConn (c, phis)) =
str_for_conn top_level c ^ "(" ^
@@ -506,26 +503,19 @@
fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
| maybe_enclose bef aft s = bef ^ s ^ aft
-fun dfg_lines flavor {is_lpo, gen_weights, gen_prec, gen_simp} ord_info
- problem =
+fun dfg_lines {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
let
- val sorted = (flavor = DFG_Sorted)
- val format = DFG flavor
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 format ty ^ ")."
+ "function(" ^ sym ^ ", " ^ string_for_type DFG ty ^ ")."
fun pred_typ sym ty =
"predicate(" ^
- commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")."
+ commas (sym :: map (string_for_type DFG) (binder_atypes ty)) ^ ")."
fun formula pred (Formula (ident, kind, phi, _, info)) =
if pred kind then
- let
- val rank =
- if flavor = DFG_Sorted then extract_isabelle_rank info
- else default_rank
- in
- "formula(" ^ dfg_string_for_formula gen_simp flavor info phi ^
+ let val rank = extract_isabelle_rank info in
+ "formula(" ^ dfg_string_for_formula gen_simp info phi ^
", " ^ ident ^
(if rank = default_rank then "" else ", " ^ string_of_int rank) ^
")." |> SOME
@@ -544,31 +534,28 @@
if is_predicate_type ty then SOME (ary sym ty) else NONE
| _ => NONE)
|> flat |> commas |> maybe_enclose "predicates [" "]."
- fun sorts () =
+ val sorts =
filt (fn Decl (_, sym, AType (s, [])) =>
if s = tptp_type_of_types then SOME sym else NONE
| _ => NONE) @ [[dfg_individual_type]]
|> flat |> commas |> maybe_enclose "sorts [" "]."
- val ord_info =
- if sorted andalso (gen_weights orelse gen_prec) then ord_info () else []
- fun do_term_order_weights () =
+ val ord_info = if gen_weights orelse gen_prec then ord_info () else []
+ val do_term_order_weights =
(if gen_weights then ord_info else [])
|> map spair |> commas |> maybe_enclose "weights [" "]."
- val syms =
- [func_aries, pred_aries] @
- (if sorted then [do_term_order_weights (), sorts ()] else [])
- fun func_sigs () =
+ val syms = [func_aries, pred_aries, do_term_order_weights, sorts]
+ val func_sigs =
filt (fn Decl (_, sym, ty) =>
if is_function_type ty then SOME (fun_typ sym ty) else NONE
| _ => NONE)
|> flat
- fun pred_sigs () =
+ val pred_sigs =
filt (fn Decl (_, sym, ty) =>
if is_nontrivial_predicate_type ty then SOME (pred_typ sym ty)
else NONE
| _ => NONE)
|> flat
- val decls = if sorted then func_sigs () @ pred_sigs () else []
+ val decls = func_sigs @ pred_sigs
val axioms =
filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
val conjs =
@@ -600,9 +587,7 @@
fun lines_for_atp_problem format ord ord_info problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
- (case format of
- DFG flavor => dfg_lines flavor ord ord_info
- | _ => tptp_lines format) problem
+ (if format = DFG then dfg_lines ord ord_info else tptp_lines format) problem
(** CNF (Metis) and CNF UEQ (Waldmeister) **)
@@ -802,7 +787,7 @@
val avoid_clash =
case format of
TFF (TPTP_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 Mon Jun 25 18:21:18 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
@@ -682,7 +682,7 @@
Native (adjust_order choice order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
- | adjust_type_enc (DFG DFG_Sorted) (Native (_, _, level)) =
+ | adjust_type_enc DFG (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF _) (Native (_, poly, level)) =
Native (First_Order, poly, level)
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 25 18:21:18 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
@@ -409,14 +409,14 @@
prem_role = Conjecture,
best_slices = fn _ =>
(* FUDGE *)
- [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
- (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_H2SOS))),
- (0.1666, (false, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_H2LR0LT0))),
- (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_H2NuVS0))),
- (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_H1SOS))),
- (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
- (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_H2SOS))),
- (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
+ [(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)))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}