# HG changeset patch # User smolkas # Date 1354101943 -3600 # Node ID 20a01c3e8072564ad217691db10669bdec2a2e56 # Parent 5d6494332b0b29b5ead00a1b3cb1749edc8fdacd renaming, minor tweaks, added signature diff -r 5d6494332b0b -r 20a01c3e8072 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Nov 28 12:25:43 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Nov 28 12:25:43 2012 +0100 @@ -24,7 +24,7 @@ val string_for_label : label -> string val metis_steps_top_level : isar_step list -> int - val metis_steps_recursive : isar_step list -> int + val metis_steps_total : isar_step list -> int end structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = @@ -48,10 +48,10 @@ val inc = curry op+ fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0 -fun metis_steps_recursive proof = +fun metis_steps_total proof = fold (fn Prove (_,_,_, By_Metis _) => inc 1 | Prove (_,_,_, Case_Split (cases, _)) => - inc (fold (inc o metis_steps_recursive) cases 1) + inc (fold (inc o metis_steps_total) cases 1) | _ => I) proof 0 end diff -r 5d6494332b0b -r 20a01c3e8072 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:25:43 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:25:43 2012 +0100 @@ -702,7 +702,7 @@ |>> kill_useless_labels_in_proof |>> relabel_proof |>> not (null params) ? cons (Fix params) - val num_steps = metis_steps_recursive isar_proof + val num_steps = metis_steps_total isar_proof val isar_text = string_for_proof ctxt type_enc lam_trans subgoal subgoal_count isar_proof diff -r 5d6494332b0b -r 20a01c3e8072 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100 @@ -13,7 +13,7 @@ -> isar_step list -> isar_step list * (bool * Time.time) end -structure Sledgehammer_Shrink (* : SLEDGEHAMMER_SHRINK *) = +structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK = struct open Sledgehammer_Util @@ -38,11 +38,11 @@ Timing.result timing |> #cpu |> SOME) handle _ => NONE end -fun sum_up_time timeout = +fun sum_up_time timeout lazy_time_vector = Vector.foldl ((fn (SOME t, (b, ts)) => (b, t+ts) | (NONE, (_, ts)) => (true, ts+timeout)) o apfst Lazy.force) - no_time + no_time lazy_time_vector (* clean vector interface *) fun get i v = Vector.sub (v, i) @@ -63,7 +63,7 @@ fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout isar_shrink proof = let - fun shrink_top_level top_level ctxt proof = + fun shrink_top_level on_top_level ctxt proof = let (* proof vector *) val proof_vect = proof |> map SOME |> Vector.fromList @@ -81,9 +81,9 @@ (* proof references *) fun refs (Prove (_, _, _, By_Metis (lfs, _))) = - maps (the_list o Label_Table.lookup label_index_table) lfs + map_filter (Label_Table.lookup label_index_table) lfs | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = - maps (the_list o Label_Table.lookup label_index_table) lfs + map_filter (Label_Table.lookup label_index_table) lfs @ maps (maps refs) cases | refs _ = [] val refed_by_vect = @@ -119,9 +119,10 @@ in take_time timeout (fn () => goal tac) end + (* FIXME: Add case_split preplaying *) | try_metis _ _ = (fn () => SOME (seconds 0.0) ) - (* Lazy metis time vector, cache *) + (* Lazy metis time vector = cache *) val metis_time = Vector.map (Lazy.lazy o try_metis preplay_timeout o the) proof_vect @@ -129,9 +130,9 @@ fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) (Prove (qs2, label2 , t, By_Metis (lfs2, gfs2))) = let - val ls = remove (op =) label1 lfs2 |> union (op =) lfs1 - val ss = union (op =) gfs1 gfs2 - in Prove (qs2, label2, t, By_Metis (ls, ss)) end + val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 + val gfs = union (op =) gfs1 gfs2 + in Prove (qs2, label2, t, By_Metis (lfs, gfs)) end fun try_merge metis_time (s1, i) (s2, j) = (case get i metis_time |> Lazy.force of NONE => (NONE, metis_time) @@ -155,7 +156,7 @@ fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' = if Inttab.is_empty cand_tab orelse n_metis' <= target_n_metis - orelse (top_level andalso n'<3) + orelse (on_top_level andalso n'<3) then (Vector.foldr (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof) @@ -189,7 +190,7 @@ merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis end - fun shrink_proof' top_level ctxt proof = + fun shrink_proof' on_top_level ctxt proof = let (* Enrich context with top-level facts *) val thy = Proof_Context.theory_of ctxt @@ -205,23 +206,23 @@ (* Shrink case_splits and top-levl *) val ((proof, top_level_time), lower_level_time) = proof |> shrink_case_splits rich_ctxt - |>> shrink_top_level top_level rich_ctxt + |>> shrink_top_level on_top_level rich_ctxt in (proof, ext_time_add lower_level_time top_level_time) end and shrink_case_splits ctxt proof = let - fun shrink_and_collect_time shrink candidates = + fun shrink_each_and_collect_time shrink candidates = let fun f_m cand time = shrink cand ||> ext_time_add time in fold_map f_m candidates no_time end - val shrink_case_split = shrink_and_collect_time (shrink_proof' false ctxt) + val shrink_case_split = shrink_each_and_collect_time (shrink_proof' false ctxt) fun shrink (Prove (qs, lbl, t, Case_Split (cases, facts))) = let val (cases, time) = shrink_case_split cases in (Prove (qs, lbl, t, Case_Split (cases, facts)), time) end | shrink step = (step, no_time) in - shrink_and_collect_time shrink proof + shrink_each_and_collect_time shrink proof end in shrink_proof' true ctxt proof