diff -r 4e17a6a0ef4f -r cf441f4a358b src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 14:26:45 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 15:05:17 2012 +0200 @@ -23,7 +23,7 @@ type one_line_params = play * string * (string * stature) list * minimize_command * int * int type isar_params = - bool * int * string Symtab.table * (string * stature) list vector + bool * bool * real * string Symtab.table * (string * stature) list vector * int Symtab.table * string proof * thm val smtN : string @@ -52,6 +52,7 @@ open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct +open Sledgehammer_Util structure String_Redirect = ATP_Proof_Redirect( type key = step_name @@ -448,9 +449,9 @@ fun is_bad_free frees (Free x) = not (member (op =) frees x) | is_bad_free _ _ = false -fun add_desired_line _ _ _ (line as Definition_Step (name, _, _)) (j, lines) = +fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) = (j, line :: map (replace_dependencies_in_line (name, [])) lines) - | add_desired_line isar_shrink_factor fact_names frees + | add_desired_line fact_names frees (Inference_Step (name as (_, ss), t, rule, deps)) (j, lines) = (j + 1, if is_fact fact_names ss orelse @@ -460,7 +461,7 @@ (not (is_only_type_information t) andalso null (Term.add_tvars t []) andalso not (exists_subterm (is_bad_free frees) t) andalso - length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso + length deps >= 2 andalso (* kill next to last line, which usually results in a trivial step *) j <> 1) then Inference_Step (name, t, rule, deps) :: lines (* keep line *) @@ -751,7 +752,7 @@ val merge_timeout_slack = 1.2 -fun minimize_locally ctxt type_enc lam_trans proof = +fun shrink_locally ctxt type_enc lam_trans isar_shrinkage proof = let (* Merging spots, greedy algorithm *) fun cost (Prove (_, _ , t, _)) = Term.size_of_term t @@ -824,24 +825,26 @@ SOME (front @ (the_list s0 @ s12 :: tail))) handle _ => NONE end - fun merge_steps proof [] = proof - | merge_steps proof (i :: is) = - case try_merge proof i of - NONE => merge_steps proof is + fun spill_shrinkage shrinkage = isar_shrinkage + shrinkage - 1.0 + fun merge_steps _ proof [] = proof + | merge_steps shrinkage proof (i :: is) = + if shrinkage < 1.5 then + merge_steps (spill_shrinkage shrinkage) proof is + else case try_merge proof i of + NONE => merge_steps (spill_shrinkage shrinkage) proof is | SOME proof' => - merge_steps proof' (map (fn j => if j > i then j - 1 else j) is) - in merge_steps proof merge_spots end + merge_steps (shrinkage - 1.0) proof' + (map (fn j => if j > i then j - 1 else j) is) + in merge_steps isar_shrinkage proof merge_spots end type isar_params = - bool * int * string Symtab.table * (string * stature) list vector + bool * bool * real * string Symtab.table * (string * stature) list vector * int Symtab.table * string proof * thm -fun isar_proof_text ctxt isar_proof_requested - (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal) - (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = +fun isar_proof_text ctxt isar_proofs + (debug, verbose, isar_shrinkage, pool, fact_names, sym_tab, atp_proof, goal) + (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let - val isar_shrink_factor = - (if isar_proof_requested then 1 else 2) * isar_shrink_factor val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val one_line_proof = one_line_proof_text 0 one_line_params @@ -862,7 +865,7 @@ |> repair_waldmeister_endgame |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) - |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees) + |-> fold_rev (add_desired_line fact_names frees) |> snd val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) val conjs = @@ -908,42 +911,54 @@ map (do_inf outer) infs val isar_proof = (if null params then [] else [Fix params]) @ - (ref_graph + (ref_graph |> redirect_graph axioms tainted |> chain_direct_proof |> map (do_inf true) |> kill_duplicate_assumptions_in_proof |> kill_useless_labels_in_proof |> relabel_proof - |> minimize_locally ctxt type_enc lam_trans) - |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count + |> shrink_locally ctxt type_enc lam_trans + (if isar_proofs then isar_shrinkage else 1000.0)) + val num_steps = length isar_proof + val isar_text = + string_for_proof ctxt type_enc lam_trans subgoal subgoal_count + isar_proof in - case isar_proof of + case isar_text of "" => - if isar_proof_requested then + if isar_proofs then "\nNo structured proof available (proof too short)." else "" | _ => - "\n\n" ^ (if isar_proof_requested then "Structured proof" - else "Perhaps this will work") ^ - ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof + "\n\n" ^ + (if isar_proofs then + "Structured proof" ^ + (if verbose then + " (" ^ string_of_int num_steps ^ " step" ^ plural_s num_steps ^ + ")" + else + "") + else + "Perhaps this will work") ^ + ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text end val isar_proof = if debug then isar_proof_of () else case try isar_proof_of () of SOME s => s - | NONE => if isar_proof_requested then + | NONE => if isar_proofs then "\nWarning: The Isar proof construction failed." else "" in one_line_proof ^ isar_proof end -fun proof_text ctxt isar_proof isar_params num_chained +fun proof_text ctxt isar_proofs isar_params num_chained (one_line_params as (preplay, _, _, _, _, _)) = - (if case preplay of Failed_to_Play _ => true | _ => isar_proof then - isar_proof_text ctxt isar_proof isar_params + (if case preplay of Failed_to_Play _ => true | _ => isar_proofs then + isar_proof_text ctxt isar_proofs isar_params else one_line_proof_text num_chained) one_line_params