--- 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);
--- 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
--- 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),