# HG changeset patch # User blanchet # Date 1328288455 -3600 # Node ID 0e490b9e8422aba66417da7f4490332fa61acf69 # Parent 76ed3b7092fc642861d0e9723749698c57d2e437 extended SPASS/DFG output with ranks diff -r 76ed3b7092fc -r 0e490b9e8422 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Fri Feb 03 18:00:55 2012 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Fri Feb 03 18:00:55 2012 +0100 @@ -102,8 +102,8 @@ fun inference infers ident = these (AList.lookup (op =) infers ident) |> inference_term fun add_inferences_to_problem_line infers - (Formula (ident, Axiom, phi, NONE, NONE)) = - Formula (ident, Lemma, phi, inference infers ident, NONE) + (Formula (ident, Axiom, phi, NONE, tms)) = + Formula (ident, Lemma, phi, inference infers ident, tms) | add_inferences_to_problem_line _ line = line fun add_inferences_to_problem infers = map (apsnd (map (add_inferences_to_problem_line infers))) @@ -139,7 +139,7 @@ exists (fn prefix => String.isPrefix prefix ident) likely_tautology_prefixes andalso is_none (run_some_atp ctxt format - [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])]) + [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])]) | is_problem_line_tautology _ _ _ = false structure String_Graph = Graph(type key = string val ord = string_ord); diff -r 76ed3b7092fc -r 0e490b9e8422 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Fri Feb 03 18:00:55 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Feb 03 18:00:55 2012 +0100 @@ -41,15 +41,9 @@ Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula * (string, string ho_type) ho_term option - * (string, string ho_type) ho_term option + * (string, string ho_type) ho_term list type 'a problem = (string * 'a problem_line list) list - val isabelle_info_prefix : string - val isabelle_info : atp_format -> string -> (string, 'a) ho_term option - val introN : string - val elimN : string - val simpN : string - val spec_eqN : string val tptp_cnf : string val tptp_fof : string val tptp_tff : string @@ -80,6 +74,15 @@ val tptp_false : string val tptp_true : string val tptp_empty_list : string + val isabelle_info_prefix : string + val isabelle_info : atp_format -> string -> int -> (string, 'a) ho_term list + val introN : string + val elimN : string + val simpN : string + val spec_eqN : string + val rankN : string + val minimum_rank : int + val default_rank : int val is_tptp_equal : string -> bool val is_built_in_tptp_symbol : string -> bool val is_tptp_variable : string -> bool @@ -154,27 +157,12 @@ datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a ho_type | - Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula - * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option + Formula of string * formula_kind + * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula + * (string, string ho_type) ho_term option + * (string, string ho_type) ho_term list type 'a problem = (string * 'a problem_line list) list -val isabelle_info_prefix = "isabelle_" - -(* Currently, only newer versions of SPASS, with sorted DFG format support, can - process Isabelle metainformation. *) -fun isabelle_info (DFG DFG_Sorted) s = - SOME (ATerm ("[]", [ATerm (isabelle_info_prefix ^ s, [])])) - | isabelle_info _ _ = NONE - -val introN = "intro" -val elimN = "elim" -val simpN = "simp" -val spec_eqN = "spec_eq" - -fun extract_isabelle_info (SOME (ATerm ("[]", [ATerm (s, [])]))) = - try (unprefix isabelle_info_prefix) s - | extract_isabelle_info _ = NONE - (* official TPTP syntax *) val tptp_cnf = "cnf" val tptp_fof = "fof" @@ -207,6 +195,36 @@ val tptp_true = "$true" val tptp_empty_list = "[]" +val isabelle_info_prefix = "isabelle_" + +val introN = "intro" +val elimN = "elim" +val simpN = "simp" +val spec_eqN = "spec_eq" +val rankN = "rank" + +val minimum_rank = 0 +val default_rank = 1000 + +(* Currently, only newer versions of SPASS, with sorted DFG format support, can + process Isabelle metainformation. *) +fun isabelle_info (DFG DFG_Sorted) status rank = + [] |> rank <> default_rank + ? cons (ATerm (isabelle_info_prefix ^ rankN, + [ATerm (string_of_int rank, [])])) + |> status <> "" ? cons (ATerm (isabelle_info_prefix ^ status, [])) + | isabelle_info _ _ _ = [] + +fun extract_isabelle_status (ATerm (s, []) :: _) = + try (unprefix isabelle_info_prefix) s + | extract_isabelle_status _ = NONE + +fun extract_isabelle_rank (tms as _ :: _) = + (case List.last tms of + ATerm (_, [ATerm (rank, [])]) => the (Int.fromString rank) + | _ => default_rank) + | extract_isabelle_rank _ = default_rank + fun is_tptp_equal s = (s = tptp_equal orelse s = tptp_old_equal) fun is_built_in_tptp_symbol s = s = tptp_old_equal orelse not (Char.isAlpha (String.sub (s, 0))) @@ -406,11 +424,12 @@ tptp_string_for_kind kind ^ ",\n (" ^ tptp_string_for_formula format phi ^ ")" ^ (case (source, info) of - (NONE, NONE) => "" - | (SOME tm, NONE) => ", " ^ tptp_string_for_term format tm - | (_, SOME tm) => + (NONE, []) => "" + | (SOME tm, []) => ", " ^ tptp_string_for_term format tm + | (_, tms) => ", " ^ tptp_string_for_term format (the_source source) ^ - ", " ^ tptp_string_for_term format tm) ^ ").\n" + ", " ^ tptp_string_for_term format (ATerm (tptp_empty_list, tms))) ^ + ").\n" fun tptp_lines format = maps (fn (_, []) => [] @@ -439,7 +458,7 @@ let fun suffix_tag top_level s = if top_level then - case extract_isabelle_info info of + case extract_isabelle_status info of SOME s' => if s' = simpN then s ^ ":lr" else if s' = spec_eqN then s ^ ":lt" else s @@ -484,8 +503,11 @@ commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")." fun formula pred (Formula (ident, kind, phi, _, info)) = if pred kind then - SOME ("formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^ - ident ^ ").") + let val rank = extract_isabelle_rank info in + "formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^ ident ^ + (if rank = default_rank then "" else ", " ^ string_of_int rank) ^ + ")." |> SOME + end else NONE | formula _ _ = NONE diff -r 76ed3b7092fc -r 0e490b9e8422 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Feb 03 18:00:55 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Feb 03 18:00:55 2012 +0100 @@ -1622,6 +1622,12 @@ |> close_formula_universally |> bound_tvars type_enc true atomic_Ts +val helper_rank = default_rank +val min_rank = 9 * helper_rank div 10 +val max_rank = 4 * min_rank + +fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n + val type_tag = `(make_fixed_const NONE) type_tag_name fun type_tag_idempotence_fact format type_enc = @@ -1632,7 +1638,7 @@ in Formula (type_tag_idempotence_helper_name, Axiom, eq_formula type_enc [] [] false (tag tagged_var) tagged_var, - NONE, isabelle_info format spec_eqN) + NONE, isabelle_info format spec_eqN helper_rank) end fun should_specialize_helper type_enc t = @@ -1945,7 +1951,7 @@ of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos - mono type_enc (j, {name, stature, kind, iformula, atomic_types}) = + mono type_enc rank (j, {name, stature, kind, iformula, atomic_types}) = (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind, iformula |> formula_from_iformula ctxt polym_constrs format mono type_enc @@ -1953,12 +1959,14 @@ |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, - case snd stature of - Intro => isabelle_info format introN - | Elim => isabelle_info format elimN - | Simp => isabelle_info format simpN - | Spec_Eq => isabelle_info format spec_eqN - | _ => NONE) + let val rank = rank j in + case snd stature of + Intro => isabelle_info format introN rank + | Elim => isabelle_info format elimN rank + | Simp => isabelle_info format simpN rank + | Spec_Eq => isabelle_info format spec_eqN rank + | _ => isabelle_info format "" rank + end) |> Formula fun formula_line_for_class_rel_clause format type_enc @@ -1970,7 +1978,7 @@ type_class_formula type_enc superclass ty_arg]) |> mk_aquant AForall [(tvar_a_name, atype_of_type_vars type_enc)], - NONE, isabelle_info format introN) + NONE, isabelle_info format introN helper_rank) end fun formula_from_arity_atom type_enc (class, t, args) = @@ -1984,7 +1992,7 @@ (formula_from_arity_atom type_enc concl_atom) |> mk_aquant AForall (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)), - NONE, isabelle_info format introN) + NONE, isabelle_info format introN helper_rank) fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = @@ -1993,10 +2001,10 @@ |> formula_from_iformula ctxt polym_constrs format mono type_enc should_guard_var_in_formula (SOME false) |> close_formula_universally - |> bound_tvars type_enc true atomic_types, NONE, NONE) + |> bound_tvars type_enc true atomic_types, NONE, []) fun formula_line_for_free_type j phi = - Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE) + Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, []) fun formula_lines_for_free_types type_enc (facts : translated_formula list) = let val phis = @@ -2193,7 +2201,7 @@ always_guard_var_in_formula (SOME true) |> close_formula_universally |> bound_tvars type_enc true (atomic_types_of T), - NONE, isabelle_info format introN) + NONE, isabelle_info format introN helper_rank) fun formula_line_for_tags_mono_type ctxt format mono type_enc T = let val x_var = ATerm (`make_bound_var "X", []) in @@ -2202,7 +2210,7 @@ Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt format mono type_enc NONE T x_var) x_var, - NONE, isabelle_info format spec_eqN) + NONE, isabelle_info format spec_eqN helper_rank) end fun problem_lines_for_mono_types ctxt format mono type_enc Ts = @@ -2273,7 +2281,7 @@ |> close_formula_universally |> bound_tvars type_enc (n > 1) (atomic_types_of T) |> maybe_negate, - NONE, isabelle_info format introN) + NONE, isabelle_info format introN helper_rank) end fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s @@ -2307,7 +2315,7 @@ in cons (Formula (ident_base ^ "_res", kind, eq (tag_with res_T (cst bounds)) (cst tagged_bounds), - NONE, isabelle_info format spec_eqN)) + NONE, isabelle_info format spec_eqN helper_rank)) end else I @@ -2319,7 +2327,7 @@ cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind, eq (cst (bounds1 @ tag_with arg_T bound :: bounds2)) (cst bounds), - NONE, isabelle_info format spec_eqN)) + NONE, isabelle_info format spec_eqN helper_rank)) | _ => raise Fail "expected nonempty tail" else I @@ -2424,7 +2432,7 @@ in ([tm1, tm2], [Formula (app_op_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, NONE, - isabelle_info format spec_eqN)]) + isabelle_info format spec_eqN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end @@ -2596,10 +2604,16 @@ |> sym_decl_table_for_facts ctxt format type_enc sym_tab |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc mono_Ts + val num_facts = length facts + val fact_lines = + map (formula_line_for_fact ctxt polym_constrs format fact_prefix + ascii_of (not exporter) (not exporter) mono type_enc + (rank_of_fact_num num_facts)) + (0 upto num_facts - 1 ~~ facts) val helper_lines = 0 upto length helpers - 1 ~~ helpers |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I - false true mono type_enc) + false true mono type_enc (K default_rank)) |> (if needs_type_tag_idempotence ctxt type_enc then cons (type_tag_idempotence_fact format type_enc) else @@ -2609,10 +2623,7 @@ val problem = [(explicit_declsN, class_decl_lines @ sym_decl_lines), (app_op_alias_eqsN, app_op_alias_eq_lines), - (factsN, - map (formula_line_for_fact ctxt polym_constrs format fact_prefix - ascii_of (not exporter) (not exporter) mono type_enc) - (0 upto length facts - 1 ~~ facts)), + (factsN, fact_lines), (class_relsN, map (formula_line_for_class_rel_clause format type_enc) class_rel_clauses),