--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 12:47:59 2011 +0200
@@ -14,7 +14,7 @@
type minimize_command = string list -> string
type metis_params =
string * minimize_command * type_system * string proof * int
- * (string * locality) list vector * thm * int
+ * (string * locality) list vector * int list * thm * int
type isar_params =
Proof.context * bool * int * string Symtab.table * int list list
* int Symtab.table
@@ -22,8 +22,8 @@
val repair_conjecture_shape_and_fact_names :
type_system -> string -> int list list -> int
- -> (string * locality) list vector
- -> int list list * int * (string * locality) list vector
+ -> (string * locality) list vector -> int list
+ -> int list list * int * (string * locality) list vector * int list
val used_facts_in_atp_proof :
type_system -> int -> (string * locality) list vector -> string proof
-> (string * locality) list
@@ -55,7 +55,7 @@
type minimize_command = string list -> string
type metis_params =
string * minimize_command * type_system * string proof * int
- * (string * locality) list vector * thm * int
+ * (string * locality) list vector * int list * thm * int
type isar_params =
Proof.context * bool * int * string Symtab.table * int list list
* int Symtab.table
@@ -64,6 +64,9 @@
fun is_head_digit s = Char.isDigit (String.sub (s, 0))
val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
+val is_typed_helper_name =
+ String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
+
fun find_first_in_list_vector vec key =
Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
| (_, value) => value) NONE vec
@@ -102,7 +105,7 @@
? (space_implode "_" o tl o space_explode "_")
fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape
- fact_offset fact_names =
+ fact_offset fact_names typed_helpers =
if String.isSubstring set_ClauseFormulaRelationN output then
let
val j0 = hd (hd conjecture_shape)
@@ -122,13 +125,17 @@
error ("No such fact: " ^ quote name ^ "."))
in
(conjecture_shape |> map (maps renumber_conjecture), 0,
- seq |> map names_for_number |> Vector.fromList)
+ seq |> map names_for_number |> Vector.fromList,
+ name_map |> filter (forall is_typed_helper_name o snd) |> map fst)
end
else
- (conjecture_shape, fact_offset, fact_names)
+ (conjecture_shape, fact_offset, fact_names, typed_helpers)
val vampire_step_prefix = "f" (* grrr... *)
+val extract_step_number =
+ Int.fromString o perhaps (try (unprefix vampire_step_prefix))
+
fun resolve_fact type_sys _ fact_names (_, SOME s) =
(case try (unprefix fact_prefix) s of
SOME s' =>
@@ -139,15 +146,18 @@
end
| NONE => [])
| resolve_fact _ facts_offset fact_names (num, NONE) =
- case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
- SOME j =>
- let val j = j - facts_offset in
- if j > 0 andalso j <= Vector.length fact_names then
- Vector.sub (fact_names, j - 1)
- else
- []
- end
- | NONE => []
+ (case extract_step_number num of
+ SOME j =>
+ let val j = j - facts_offset in
+ if j > 0 andalso j <= Vector.length fact_names then
+ Vector.sub (fact_names, j - 1)
+ else
+ []
+ end
+ | NONE => [])
+
+fun is_fact type_sys conjecture_shape =
+ not o null o resolve_fact type_sys 0 conjecture_shape
fun resolve_conjecture _ (_, SOME s) =
(case try (unprefix conjecture_prefix) s of
@@ -157,18 +167,21 @@
| NONE => [])
| NONE => [])
| resolve_conjecture conjecture_shape (num, NONE) =
- case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
- SOME i =>
- (case find_index (exists (curry (op =) i)) conjecture_shape of
- ~1 => []
- | j => [j])
+ case extract_step_number num of
+ SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of
+ ~1 => []
+ | j => [j])
| NONE => []
-fun is_fact type_sys conjecture_shape =
- not o null o resolve_fact type_sys 0 conjecture_shape
fun is_conjecture conjecture_shape =
not o null o resolve_conjecture conjecture_shape
+fun is_typed_helper _ (_, SOME s) = is_typed_helper_name s
+ | is_typed_helper typed_helpers (num, NONE) =
+ (case extract_step_number num of
+ SOME i => member (op =) typed_helpers i
+ | NONE => false)
+
fun add_fact type_sys facts_offset fact_names (Inference (name, _, [])) =
append (resolve_fact type_sys facts_offset fact_names name)
| add_fact _ _ _ _ = I
@@ -227,15 +240,21 @@
List.partition (curry (op =) Chained o snd)
#> pairself (sort_distinct (string_ord o pairself fst))
+fun uses_typed_helpers typed_helpers =
+ exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name
+ | _ => false)
+
fun metis_proof_text (banner, minimize_command, type_sys, atp_proof,
- facts_offset, fact_names, goal, i) =
+ facts_offset, fact_names, typed_helpers, goal, i) =
let
val (chained, extra) =
atp_proof |> used_facts_in_atp_proof type_sys facts_offset fact_names
|> split_used_facts
+ val full_types = uses_typed_helpers typed_helpers atp_proof
val n = Logic.count_prems (prop_of goal)
+ val metis = metis_command full_types i n ([], map fst extra)
in
- (try_command_line banner (metis_command false i n ([], map fst extra)) ^
+ (try_command_line banner metis ^
minimize_line minimize_command (map fst (extra @ chained)),
extra @ chained)
end
@@ -919,7 +938,7 @@
step :: aux subst depth nextp proof
in aux [] 0 (1, 1) end
-fun string_for_proof ctxt0 i n =
+fun string_for_proof ctxt0 full_types i n =
let
val ctxt =
ctxt0 |> Config.put show_free_types false
@@ -942,7 +961,7 @@
if member (op =) qs Show then "show" else "have")
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
fun do_facts (ls, ss) =
- metis_command false 1 1
+ metis_command full_types 1 1
(ls |> sort_distinct (prod_ord string_ord int_ord),
ss |> sort_distinct string_ord)
and do_step ind (Fix xs) =
@@ -979,11 +998,12 @@
fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape,
sym_tab)
(metis_params as (_, _, type_sys, atp_proof, facts_offset,
- fact_names, goal, i)) =
+ fact_names, typed_helpers, goal, i)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal i
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
+ val full_types = uses_typed_helpers typed_helpers atp_proof
val n = Logic.count_prems (prop_of goal)
val (one_line_proof, lemma_names) = metis_proof_text metis_params
fun isar_proof_for () =
@@ -995,7 +1015,7 @@
|> then_chain_proof
|> kill_useless_labels_in_proof
|> relabel_proof
- |> string_for_proof ctxt i n of
+ |> string_for_proof ctxt full_types i n of
"" => "\nNo structured proof available (proof too short)."
| proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200
@@ -28,6 +28,8 @@
val readable_names : bool Config.T
val fact_prefix : string
val conjecture_prefix : string
+ val helper_prefix : string
+ val typed_helper_suffix : string
val predicator_base : string
val explicit_app_base : string
val type_pred_base : string
@@ -46,7 +48,7 @@
-> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
-> string problem * string Symtab.table * int * int
- * (string * 'a) list vector * int Symtab.table
+ * (string * 'a) list vector * int list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
end;
@@ -87,6 +89,9 @@
val arity_clause_prefix = "arity_"
val tfree_prefix = "tfree_"
+val typed_helper_suffix = "_T"
+val untyped_helper_suffix = "_U"
+
val predicator_base = "hBOOL"
val explicit_app_base = "hAPP"
val type_pred_base = "is"
@@ -487,7 +492,7 @@
if prem_kind = Conjecture then update_combformula mk_anot
else I)
in
- make_formula ctxt true true (string_of_int j) Chained kind t
+ make_formula ctxt true true (string_of_int j) General kind t
|> maybe_negate
end)
(0 upto last) ts
@@ -734,8 +739,10 @@
val thy = Proof_Context.theory_of ctxt
val unmangled_s = mangled_s |> unmangled_const_name
fun dub_and_inst c needs_some_types (th, j) =
- ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
- Chained),
+ ((c ^ "_" ^ string_of_int j ^
+ (if needs_some_types then typed_helper_suffix
+ else untyped_helper_suffix),
+ General),
let val t = th |> prop_of in
t |> ((case general_type_arg_policy type_sys of
Mangled_Type_Args _ => true
@@ -1203,6 +1210,10 @@
(conjs, helpers @ facts)
|> sym_decl_table_for_facts type_sys repaired_sym_tab
|> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
+ val helper_lines =
+ map (formula_line_for_fact ctxt helper_prefix nonmono_Ts type_sys)
+ (0 upto length helpers - 1 ~~ helpers)
+ |> should_add_ti_ti_helper type_sys ? cons (ti_ti_helper_fact ())
(* Reordering these might confuse the proof reconstruction code or the SPASS
Flotter hack. *)
val problem =
@@ -1211,11 +1222,7 @@
(0 upto length facts - 1 ~~ facts)),
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map formula_line_for_arity_clause arity_clauses),
- (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
- type_sys)
- (0 upto length helpers - 1 ~~ helpers)
- |> should_add_ti_ti_helper type_sys
- ? cons (ti_ti_helper_fact ())),
+ (helpersN, helper_lines),
(conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
conjs),
(free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
@@ -1228,6 +1235,13 @@
| _ => I)
val (problem, pool) =
problem |> nice_atp_problem (Config.get ctxt readable_names)
+ val helpers_offset = offset_of_heading_in_problem helpersN problem 0
+ val typed_helpers =
+ map_filter (fn (j, {name, ...}) =>
+ if String.isSuffix typed_helper_suffix name then SOME j
+ else NONE)
+ ((helpers_offset + 1 upto helpers_offset + length helpers)
+ ~~ helpers)
fun add_sym_arity (s, {min_ary, ...} : sym_info) =
if min_ary > 0 then
case strip_prefix_and_unascii const_prefix s of
@@ -1241,6 +1255,7 @@
offset_of_heading_in_problem conjsN problem 0,
offset_of_heading_in_problem factsN problem 0,
fact_names |> Vector.fromList,
+ typed_helpers,
Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 12:47:59 2011 +0200
@@ -534,7 +534,7 @@
else
()
val (atp_problem, pool, conjecture_offset, facts_offset,
- fact_names, sym_tab) =
+ fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys
explicit_apply hyp_ts concl_t facts
fun weights () = atp_problem_weights atp_problem
@@ -567,13 +567,14 @@
extract_tstplike_proof_and_outcome verbose complete res_code
proof_delims known_failures output
|>> atp_proof_from_tstplike_proof
- val (conjecture_shape, facts_offset, fact_names) =
+ val (conjecture_shape, facts_offset, fact_names,
+ typed_helpers) =
if is_none outcome then
repair_conjecture_shape_and_fact_names type_sys output
- conjecture_shape facts_offset fact_names
+ conjecture_shape facts_offset fact_names typed_helpers
else
(* don't bother repairing *)
- (conjecture_shape, facts_offset, fact_names)
+ (conjecture_shape, facts_offset, fact_names, typed_helpers)
val outcome =
case outcome of
NONE =>
@@ -587,7 +588,8 @@
else SOME IncompleteUnprovable
| _ => outcome
in
- ((pool, conjecture_shape, facts_offset, fact_names, sym_tab),
+ ((pool, conjecture_shape, facts_offset, fact_names,
+ typed_helpers, sym_tab),
(output, msecs, type_sys, atp_proof, outcome))
end
val timer = Timer.startRealTimer ()
@@ -607,7 +609,7 @@
end
| maybe_run_slice _ _ result = result
fun maybe_blacklist_facts_and_retry iter blacklist
- (result as ((_, _, facts_offset, fact_names, _),
+ (result as ((_, _, facts_offset, fact_names, _, _),
(_, _, type_sys, atp_proof,
SOME (UnsoundProof (false, _))))) =
(case used_facts_in_atp_proof type_sys facts_offset fact_names
@@ -624,7 +626,7 @@
result)
| maybe_blacklist_facts_and_retry _ _ result = result
in
- ((Symtab.empty, [], 0, Vector.fromList [], Symtab.empty),
+ ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
("", SOME 0, hd fallback_best_type_systems, [],
SOME InternalError))
|> fold (maybe_run_slice []) actual_slices
@@ -644,7 +646,8 @@
()
else
File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
- val ((pool, conjecture_shape, facts_offset, fact_names, sym_tab),
+ val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
+ sym_tab),
(output, msecs, type_sys, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
val important_message =
@@ -668,7 +671,7 @@
(ctxt, debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
val metis_params =
(proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset,
- fact_names, goal, subgoal)
+ fact_names, typed_helpers, goal, subgoal)
val (outcome, (message, used_facts)) =
case outcome of
NONE =>
--- a/src/HOL/ex/tptp_export.ML Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Fri May 20 12:47:59 2011 +0200
@@ -103,7 +103,7 @@
else Sledgehammer_ATP_Translate.Const_Arg_Types,
Sledgehammer_ATP_Translate.Heavy)
val explicit_apply = false
- val (atp_problem, _, _, _, _, _) =
+ val (atp_problem, _, _, _, _, _, _) =
Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom
ATP_Problem.Axiom type_sys explicit_apply [] @{prop False} facts
val infers =