# HG changeset patch # User blanchet # Date 1387126898 -3600 # Node ID 6b0ca7f79e9369af1ce793ef294cda8e6307e7d2 # Parent 688da3388b2da642acece1f0f48eb3ecf0acf4d8 robustness in degenerate case + tuning diff -r 688da3388b2d -r 6b0ca7f79e93 src/HOL/Tools/ATP/atp_proof_redirect.ML --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Sun Dec 15 18:01:38 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Sun Dec 15 18:01:38 2013 +0100 @@ -76,9 +76,10 @@ let fun add_edge to from = Atom_Graph.default_node (from, ()) - #> Atom_Graph.default_node (to, ()) #> Atom_Graph.add_edge_acyclic (from, to) - fun add_infer (froms, to) = fold (add_edge to) froms + fun add_infer (froms, to) = + Atom_Graph.default_node (to, ()) + #> fold (add_edge to) froms val graph = fold add_infer infers Atom_Graph.empty val reachable = Atom_Graph.all_preds graph [bot] diff -r 688da3388b2d -r 6b0ca7f79e93 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Sun Dec 15 18:01:38 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Sun Dec 15 18:01:38 2013 +0100 @@ -55,17 +55,18 @@ let val (refed, steps) = do_steps steps in (refed, Proof (fix, assms, steps)) end - and do_steps steps = - let - (* the last step is always implicitly referenced *) - val (steps, (refed, concl)) = - split_last steps - ||> do_refed_step - in - fold_rev do_step steps (refed, [concl]) - end + and do_steps [] = ([], []) + | do_steps steps = + let + (* the last step is always implicitly referenced *) + val (steps, (refed, concl)) = + split_last steps + ||> do_refed_step + in + fold_rev do_step steps (refed, [concl]) + end and do_step step (refed, accu) = - case label_of_step step of + (case label_of_step step of NONE => (refed, step :: accu) | SOME l => if Ord_List.member label_ord refed l then @@ -73,7 +74,7 @@ |>> Ord_List.union label_ord refed ||> (fn x => x :: accu) else - (refed, accu) + (refed, accu)) and do_refed_step step = step |> postproc_step |> do_refed_step' and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar" | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) = diff -r 688da3388b2d -r 6b0ca7f79e93 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Sun Dec 15 18:01:38 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Sun Dec 15 18:01:38 2013 +0100 @@ -279,7 +279,8 @@ in (* One-step Metis proofs are pointless; better use the one-liner directly. *) (case proof of - Proof ([], [], [Prove (_, [], _, _, [], (_, MetisM))]) => "" + Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *) + | Proof ([], [], [Prove (_, [], _, _, [], (_, MetisM))]) => "" | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ diff -r 688da3388b2d -r 6b0ca7f79e93 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:01:38 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:01:38 2013 +0100 @@ -323,10 +323,10 @@ val lits = map (maybe_dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) in - case List.partition (can HOLogic.dest_not) lits of + (case List.partition (can HOLogic.dest_not) lits of (negs as _ :: _, pos as _ :: _) => s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) - | _ => fold (curry s_disj) lits @{term False} + | _ => fold (curry s_disj) lits @{term False}) end |> HOLogic.mk_Trueprop |> close_form @@ -380,15 +380,9 @@ and isar_proof outer fix assms lems infs = Proof (fix, assms, lems @ isar_steps outer NONE [] infs) - val isar_proof_of_direct_proof = isar_proof true params assms lems - (* 60 seconds seems like a good interpreation of "no timeout" *) val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) - val clean_up_labels_in_proof = - chain_direct_proof - #> kill_useless_labels_in_proof - #> relabel_proof val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) = refute_graph (* @@ -398,11 +392,12 @@ (* |> tap (tracing o prefix "Direct proof: " o string_of_direct_proof) *) - |> isar_proof_of_direct_proof + |> isar_proof true params assms lems |> postprocess_remove_unreferenced_steps I |> relabel_proof_canonically |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay preplay_timeout) + val ((preplay_time, preplay_fail), isar_proof) = isar_proof |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0) @@ -410,11 +405,14 @@ |> isar_try0 ? try0 preplay_timeout preplay_interface |> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface) |> `overall_preplay_stats - ||> clean_up_labels_in_proof + ||> (chain_direct_proof + #> kill_useless_labels_in_proof + #> relabel_proof) + val isar_text = string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof in - case isar_text of + (case isar_text of "" => if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)." @@ -437,24 +435,23 @@ in "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ Active.sendback_markup [Markup.padding_command] isar_text - end + end) end val isar_proof = if debug then isar_proof_of () - else case try isar_proof_of () of - SOME s => s - | NONE => if isar_proofs = SOME true then - "\nWarning: The Isar proof construction failed." - else - "" + else + (case try isar_proof_of () of + SOME s => s + | NONE => + if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "") in one_line_proof ^ isar_proof end fun isar_proof_would_be_a_good_idea preplay = - case preplay of + (case preplay of Played (reconstr, _) => reconstr = SMT | Trust_Playable _ => false - | Failed_to_Play _ => true + | Failed_to_Play _ => true) fun proof_text ctxt isar_proofs isar_params num_chained (one_line_params as (preplay, _, _, _, _, _)) =