1.1 --- a/src/HOL/TPTP/ATP_Theory_Export.thy Mon Jun 25 18:21:18 2012 +0200
1.2 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Tue Jun 26 11:14:39 2012 +0200
1.3 @@ -23,8 +23,7 @@
1.4 ML {*
1.5 if do_it then
1.6 "/tmp/axs_mono_native.dfg"
1.7 - |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted)
1.8 - "mono_native"
1.9 + |> generate_tptp_inference_file_for_theory ctxt thy DFG "mono_native"
1.10 else
1.11 ()
1.12 *}
2.1 --- a/src/HOL/TPTP/atp_theory_export.ML Mon Jun 25 18:21:18 2012 +0200
2.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200
2.3 @@ -118,7 +118,7 @@
2.4 let
2.5 val thy = Proof_Context.theory_of ctxt
2.6 val prob_file = File.tmp_path (Path.explode "prob")
2.7 - val atp = case format of DFG _ => spassN | _ => eN
2.8 + val atp = if format = DFG then spassN else eN
2.9 val {exec, arguments, proof_delims, known_failures, ...} =
2.10 get_atp thy atp ()
2.11 val ord = effective_term_order ctxt atp
2.12 @@ -213,7 +213,7 @@
2.13 val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
2.14 val atp_problem =
2.15 atp_problem
2.16 - |> (case format of DFG _ => I | _ => add_inferences_to_problem infers)
2.17 + |> (format <> DFG ? add_inferences_to_problem infers)
2.18 |> order_problem_facts name_ord
2.19 val ord = effective_term_order ctxt eN (* dummy *)
2.20 val ss = lines_for_atp_problem format ord (K []) atp_problem
3.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jun 25 18:21:18 2012 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200
3.3 @@ -32,7 +32,6 @@
3.4 datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
3.5 datatype thf_choice = THF_Without_Choice | THF_With_Choice
3.6 datatype thf_defs = THF_Without_Defs | THF_With_Defs
3.7 - datatype dfg_flavor = DFG_Unsorted | DFG_Sorted
3.8
3.9 datatype atp_format =
3.10 CNF |
3.11 @@ -40,7 +39,7 @@
3.12 FOF |
3.13 TFF of tptp_polymorphism * tptp_explicitness |
3.14 THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
3.15 - DFG of dfg_flavor
3.16 + DFG
3.17
3.18 datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
3.19 datatype 'a problem_line =
3.20 @@ -165,7 +164,6 @@
3.21 datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
3.22 datatype thf_choice = THF_Without_Choice | THF_With_Choice
3.23 datatype thf_defs = THF_Without_Defs | THF_With_Defs
3.24 -datatype dfg_flavor = DFG_Unsorted | DFG_Sorted
3.25
3.26 datatype atp_format =
3.27 CNF |
3.28 @@ -173,7 +171,7 @@
3.29 FOF |
3.30 TFF of tptp_polymorphism * tptp_explicitness |
3.31 THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs |
3.32 - DFG of dfg_flavor
3.33 + DFG
3.34
3.35 datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
3.36 datatype 'a problem_line =
3.37 @@ -229,8 +227,7 @@
3.38 val default_rank = 1000
3.39 val default_term_order_weight = 1
3.40
3.41 -(* Currently, only newer versions of SPASS, with sorted DFG format support, can
3.42 - process Isabelle metainformation. *)
3.43 +(* Currently, only SPASS 3.8ds can process Isabelle metainformation. *)
3.44 fun isabelle_info status rank =
3.45 [] |> rank <> default_rank
3.46 ? cons (ATerm (isabelle_info_prefix ^ rankN,
3.47 @@ -309,7 +306,7 @@
3.48 | is_format_higher_order _ = false
3.49 fun is_format_typed (TFF _) = true
3.50 | is_format_typed (THF _) = true
3.51 - | is_format_typed (DFG DFG_Sorted) = true
3.52 + | is_format_typed DFG = true
3.53 | is_format_typed _ = false
3.54
3.55 fun tptp_string_for_role Axiom = "axiom"
3.56 @@ -339,7 +336,7 @@
3.57
3.58 fun str_for_type format ty =
3.59 let
3.60 - val dfg = (format = DFG DFG_Sorted)
3.61 + val dfg = (format = DFG)
3.62 fun str _ (AType (s, [])) =
3.63 if dfg andalso s = tptp_individual_type then dfg_individual_type else s
3.64 | str _ (AType (s, tys)) =
3.65 @@ -441,7 +438,7 @@
3.66 | tptp_string_for_format FOF = tptp_fof
3.67 | tptp_string_for_format (TFF _) = tptp_tff
3.68 | tptp_string_for_format (THF _) = tptp_thf
3.69 - | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format"
3.70 + | tptp_string_for_format DFG = raise Fail "non-TPTP format"
3.71
3.72 fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =
3.73 tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
3.74 @@ -467,10 +464,10 @@
3.75 fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
3.76 | binder_atypes _ = []
3.77
3.78 -fun dfg_string_for_formula gen_simp flavor info =
3.79 +fun dfg_string_for_formula gen_simp info =
3.80 let
3.81 fun suffix_tag top_level s =
3.82 - if flavor = DFG_Sorted andalso top_level then
3.83 + if top_level then
3.84 case extract_isabelle_status info of
3.85 SOME s' => if s' = defN then s ^ ":lt"
3.86 else if s' = simpN andalso gen_simp then s ^ ":lr"
3.87 @@ -495,7 +492,7 @@
3.88 | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
3.89 fun str_for_formula top_level (AQuant (q, xs, phi)) =
3.90 str_for_quant q ^ "(" ^ "[" ^
3.91 - commas (map (string_for_bound_var (DFG flavor)) xs) ^ "], " ^
3.92 + commas (map (string_for_bound_var DFG) xs) ^ "], " ^
3.93 str_for_formula top_level phi ^ ")"
3.94 | str_for_formula top_level (AConn (c, phis)) =
3.95 str_for_conn top_level c ^ "(" ^
3.96 @@ -506,26 +503,19 @@
3.97 fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
3.98 | maybe_enclose bef aft s = bef ^ s ^ aft
3.99
3.100 -fun dfg_lines flavor {is_lpo, gen_weights, gen_prec, gen_simp} ord_info
3.101 - problem =
3.102 +fun dfg_lines {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
3.103 let
3.104 - val sorted = (flavor = DFG_Sorted)
3.105 - val format = DFG flavor
3.106 fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")"
3.107 fun ary sym = curry spair sym o arity_of_type
3.108 fun fun_typ sym ty =
3.109 - "function(" ^ sym ^ ", " ^ string_for_type format ty ^ ")."
3.110 + "function(" ^ sym ^ ", " ^ string_for_type DFG ty ^ ")."
3.111 fun pred_typ sym ty =
3.112 "predicate(" ^
3.113 - commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")."
3.114 + commas (sym :: map (string_for_type DFG) (binder_atypes ty)) ^ ")."
3.115 fun formula pred (Formula (ident, kind, phi, _, info)) =
3.116 if pred kind then
3.117 - let
3.118 - val rank =
3.119 - if flavor = DFG_Sorted then extract_isabelle_rank info
3.120 - else default_rank
3.121 - in
3.122 - "formula(" ^ dfg_string_for_formula gen_simp flavor info phi ^
3.123 + let val rank = extract_isabelle_rank info in
3.124 + "formula(" ^ dfg_string_for_formula gen_simp info phi ^
3.125 ", " ^ ident ^
3.126 (if rank = default_rank then "" else ", " ^ string_of_int rank) ^
3.127 ")." |> SOME
3.128 @@ -544,31 +534,28 @@
3.129 if is_predicate_type ty then SOME (ary sym ty) else NONE
3.130 | _ => NONE)
3.131 |> flat |> commas |> maybe_enclose "predicates [" "]."
3.132 - fun sorts () =
3.133 + val sorts =
3.134 filt (fn Decl (_, sym, AType (s, [])) =>
3.135 if s = tptp_type_of_types then SOME sym else NONE
3.136 | _ => NONE) @ [[dfg_individual_type]]
3.137 |> flat |> commas |> maybe_enclose "sorts [" "]."
3.138 - val ord_info =
3.139 - if sorted andalso (gen_weights orelse gen_prec) then ord_info () else []
3.140 - fun do_term_order_weights () =
3.141 + val ord_info = if gen_weights orelse gen_prec then ord_info () else []
3.142 + val do_term_order_weights =
3.143 (if gen_weights then ord_info else [])
3.144 |> map spair |> commas |> maybe_enclose "weights [" "]."
3.145 - val syms =
3.146 - [func_aries, pred_aries] @
3.147 - (if sorted then [do_term_order_weights (), sorts ()] else [])
3.148 - fun func_sigs () =
3.149 + val syms = [func_aries, pred_aries, do_term_order_weights, sorts]
3.150 + val func_sigs =
3.151 filt (fn Decl (_, sym, ty) =>
3.152 if is_function_type ty then SOME (fun_typ sym ty) else NONE
3.153 | _ => NONE)
3.154 |> flat
3.155 - fun pred_sigs () =
3.156 + val pred_sigs =
3.157 filt (fn Decl (_, sym, ty) =>
3.158 if is_nontrivial_predicate_type ty then SOME (pred_typ sym ty)
3.159 else NONE
3.160 | _ => NONE)
3.161 |> flat
3.162 - val decls = if sorted then func_sigs () @ pred_sigs () else []
3.163 + val decls = func_sigs @ pred_sigs
3.164 val axioms =
3.165 filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
3.166 val conjs =
3.167 @@ -600,9 +587,7 @@
3.168 fun lines_for_atp_problem format ord ord_info problem =
3.169 "% This file was generated by Isabelle (most likely Sledgehammer)\n\
3.170 \% " ^ timestamp () ^ "\n" ::
3.171 - (case format of
3.172 - DFG flavor => dfg_lines flavor ord ord_info
3.173 - | _ => tptp_lines format) problem
3.174 + (if format = DFG then dfg_lines ord ord_info else tptp_lines format) problem
3.175
3.176
3.177 (** CNF (Metis) and CNF UEQ (Waldmeister) **)
3.178 @@ -802,7 +787,7 @@
3.179 val avoid_clash =
3.180 case format of
3.181 TFF (TPTP_Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
3.182 - | DFG _ => avoid_clash_with_dfg_keywords
3.183 + | DFG => avoid_clash_with_dfg_keywords
3.184 | _ => I
3.185 val nice_name = nice_name avoid_clash
3.186 fun nice_type (AType (name, tys)) =
4.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jun 25 18:21:18 2012 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200
4.3 @@ -682,7 +682,7 @@
4.4 Native (adjust_order choice order, Mangled_Monomorphic, level)
4.5 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Native (_, _, level)) =
4.6 Native (First_Order, Mangled_Monomorphic, level)
4.7 - | adjust_type_enc (DFG DFG_Sorted) (Native (_, _, level)) =
4.8 + | adjust_type_enc DFG (Native (_, _, level)) =
4.9 Native (First_Order, Mangled_Monomorphic, level)
4.10 | adjust_type_enc (TFF _) (Native (_, poly, level)) =
4.11 Native (First_Order, poly, level)
5.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 25 18:21:18 2012 +0200
5.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200
5.3 @@ -409,14 +409,14 @@
5.4 prem_role = Conjecture,
5.5 best_slices = fn _ =>
5.6 (* FUDGE *)
5.7 - [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
5.8 - (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_H2SOS))),
5.9 - (0.1666, (false, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_H2LR0LT0))),
5.10 - (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_H2NuVS0))),
5.11 - (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_H1SOS))),
5.12 - (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
5.13 - (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_H2SOS))),
5.14 - (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
5.15 + [(0.1667, (false, ((150, DFG, "mono_native", combsN, true), ""))),
5.16 + (0.1667, (false, ((500, DFG, "mono_native", liftingN, true), spass_H2SOS))),
5.17 + (0.1666, (false, ((50, DFG, "mono_native", liftingN, true), spass_H2LR0LT0))),
5.18 + (0.1000, (false, ((250, DFG, "mono_native", combsN, true), spass_H2NuVS0))),
5.19 + (0.1000, (false, ((1000, DFG, "mono_native", liftingN, true), spass_H1SOS))),
5.20 + (0.1000, (false, ((150, DFG, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
5.21 + (0.1000, (false, ((300, DFG, "mono_native", combsN, true), spass_H2SOS))),
5.22 + (0.1000, (false, ((100, DFG, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
5.23 best_max_mono_iters = default_max_mono_iters,
5.24 best_max_new_mono_instances = default_max_new_mono_instances}
5.25