rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 04 12:28:42 2014 +0200
@@ -78,7 +78,7 @@
dont_know ()
else
let
- val fact_names = used_facts |> map fst |> sort string_ord
+ val fact_names = map fst used_facts
val {context = ctxt, facts = chained, goal} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 04 12:28:42 2014 +0200
@@ -93,8 +93,8 @@
map (replace_dependencies_in_line (name, [])) lines
| add_line_pass1 line lines = line :: lines
-fun normalize role t =
- t |> role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
+fun normalize role =
+ role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
fun add_lines_pass2 res [] = rev res
| add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
@@ -242,7 +242,7 @@
accum
|> (if tainted = [] then
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- (the_list predecessor, []), massage_methods systematic_methods', ""))
+ sort_facts (the_list predecessor, []), massage_methods systematic_methods', ""))
else
I)
|> rev
@@ -253,7 +253,9 @@
val rule = rule_of_clause_id id
val skolem = is_skolemize_rule rule
- val deps = fold add_fact_of_dependencies gamma ([], [])
+ val deps = ([], [])
+ |> fold add_fact_of_dependencies gamma
+ |> sort_facts
val meths =
(if skolem then skolem_methods
else if is_arith_rule rule then arith_methods
@@ -296,7 +298,7 @@
val step =
Prove (maybe_show outer c [], [], l, t,
map isar_case (filter_out (null o snd) cases),
- (the_list predecessor, []), massage_methods systematic_methods', "")
+ sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")
in
isar_steps outer (SOME l) (step :: accum) infs
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Aug 04 12:28:42 2014 +0200
@@ -95,7 +95,8 @@
val gfs = union (op =) gfs1 gfs2
in
(Prove (qs2, inter (op =) (Term.add_frees t []) (xs1 @ xs2), l2, t,
- subproofs1 @ subproofs2, (lfs, gfs), meths, comment1 ^ comment2), hopeless)
+ subproofs1 @ subproofs2, sort_facts (lfs, gfs), meths, comment1 ^ comment2),
+ hopeless)
end
val merge_slack_time = seconds 0.01
@@ -203,7 +204,7 @@
fun try_eliminate i l labels steps =
let
- val (steps_before, (cand as Prove (_, xs, _, _, _, (lfs, _), _, _)) :: steps_after) =
+ val (steps_before, (cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps_after) =
chop i steps
val succs = collect_successors steps_after labels
val (succs', hopelesses) = split_list (map (merge_steps (!preplay_data) cand) succs)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Aug 04 12:28:42 2014 +0200
@@ -26,9 +26,9 @@
val label_ord : label * label -> order
val string_of_label : label -> string
+ val sort_facts : facts -> facts
val steps_of_isar_proof : isar_proof -> isar_step list
-
val label_of_isar_step : isar_step -> label option
val facts_of_isar_step : isar_step -> facts
val proof_methods_of_isar_step : isar_step -> proof_method list
@@ -75,10 +75,24 @@
val no_label = ("", ~1)
-val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
+(* cf. "label_ord" below *)
+val assume_prefix = "a"
+val have_prefix = "f"
+
+fun label_ord ((s1, i1), (s2, i2)) =
+ (case int_ord (pairself String.size (s1, s2)) of
+ EQUAL =>
+ (case string_ord (s1, s2) of
+ EQUAL => int_ord (i1, i2)
+ | ord => ord (* "assume" before "have" *))
+ | ord => ord)
fun string_of_label (s, num) = s ^ string_of_int num
+(* Put the nearest local label first, since it's the most likely to be replaced by a "hence".
+ (Some preplaying proof methods, e.g. "blast", react poorly to fact reorderings.) *)
+fun sort_facts (lfs, gfs) = (sort (label_ord o swap) lfs, sort string_ord gfs)
+
fun steps_of_isar_proof (Proof (_, _, steps)) = steps
fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
@@ -174,9 +188,6 @@
fst (relabel_proof proof (0, []))
end
-val assume_prefix = "a"
-val have_prefix = "f"
-
val relabel_isar_proof_nicely =
let
fun next_label depth prefix l (accum as (next, subst)) =
@@ -290,18 +301,17 @@
and add_step_pre ind qs subs (s, ctxt) =
(s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt)
and add_step ind (Let (t1, t2)) =
- add_str (of_indent ind ^ "let ")
- #> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n"
+ add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2
+ #> add_str "\n"
| add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) =
add_step_pre ind qs subs
#> (case xs of
- [] => add_str (of_have qs (length subs) ^ " ")
- | _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ")
+ [] => add_str (of_have qs (length subs) ^ " ")
+ | _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ")
#> add_str (of_label l)
#> add_term t
- #> add_str (" " ^
- of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
- (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
+ #> add_str (" " ^ of_method ls ss meth ^
+ (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
and add_steps ind = fold (add_step ind)
and of_proof ind ctxt (Proof (xs, assms, steps)) =
("", ctxt)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Aug 04 12:28:42 2014 +0200
@@ -182,7 +182,6 @@
fun split_used_facts facts =
facts
|> List.partition (fn (_, (sc, _)) => sc = Chained)
- |> pairself (sort_distinct (string_ord o pairself fst))
fun one_line_proof_text ctxt num_chained
((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Aug 04 12:28:42 2014 +0200
@@ -294,19 +294,21 @@
|>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
|> fst |> split_time
|> (fn accum as (output, _) =>
- (accum,
- extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
- |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) atp_problem
- handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
+ (accum,
+ extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
+ |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name)
+ atp_problem
+ handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
val outcome =
(case outcome of
NONE =>
- (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof
- |> Option.map (sort string_ord) of
+ (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of
SOME facts =>
- let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
+ let
+ val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts)
+ in
if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
end
| NONE => NONE)
@@ -357,7 +359,7 @@
(case outcome of
NONE =>
let
- val used_facts = used_facts_in_atp_proof ctxt (map fst used_from) atp_proof
+ val used_facts = sort_wrt fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
val preferred_methss =
bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Aug 04 12:28:42 2014 +0200
@@ -73,7 +73,7 @@
fun n_facts names =
let val n = length names in
string_of_int n ^ " fact" ^ plural_s n ^
- (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
+ (if n > 0 then ": " ^ (names |> map fst |> space_implode " ") else "")
end
fun print silent f = if silent then () else Output.urgent_message (f ())
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Mon Aug 04 12:28:42 2014 +0200
@@ -189,7 +189,7 @@
val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
smt2_filter_loop name params state goal subgoal factss
val used_named_facts = map snd fact_ids
- val used_facts = map fst used_named_facts
+ val used_facts = sort_wrt fst (map fst used_named_facts)
val outcome = Option.map failure_of_smt2_failure outcome
val (preferred_methss, message) =