# HG changeset patch # User blanchet # Date 1340702079 -7200 # Node ID 933d43c31689355db234d727eb16ce77771727a5 # Parent bf172a5929bbbaaa6aef2aef28bc54918b9ff6e4 removed support for unsorted DFG, now that SPASS 3.7 is no longer supported diff -r bf172a5929bb -r 933d43c31689 src/HOL/TPTP/ATP_Theory_Export.thy --- 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 () *} diff -r bf172a5929bb -r 933d43c31689 src/HOL/TPTP/atp_theory_export.ML --- 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 diff -r bf172a5929bb -r 933d43c31689 src/HOL/Tools/ATP/atp_problem.ML --- 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)) = diff -r bf172a5929bb -r 933d43c31689 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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) diff -r bf172a5929bb -r 933d43c31689 src/HOL/Tools/ATP/atp_systems.ML --- 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}