# HG changeset patch # User smolkas # Date 1372263960 -7200 # Node ID b528a975b256b0df48edea54f84b9683107745c8 # Parent 2cba5906d836e9f8649295a475ac168ba2bd108a tuned: cleaned up data structure diff -r 2cba5906d836 -r b528a975b256 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Jun 26 18:25:13 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Jun 26 18:26:00 2013 +0200 @@ -77,17 +77,19 @@ val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round (* table for mapping from (top-level-)label to step_vect position *) - fun update_table (i, Prove (_, _, l, _, _)) = Label_Table.update_new (l, i) + fun update_table (i, Prove (_, _, l, _, _, _)) = + Label_Table.update_new (l, i) | update_table _ = I val label_index_table = fold_index update_table steps Label_Table.empty val lookup_indices = map_filter (Label_Table.lookup label_index_table) (* proof step references *) fun refs step = - (case byline_of_step step of - NONE => [] - | SOME (By_Metis (subproofs, (lfs, _))) => - maps (steps_of_proof #> maps refs) subproofs @ lookup_indices lfs) + fold_isar_step + (byline_of_step + #> (fn SOME (By_Metis (lfs, _)) => append (lookup_indices lfs) + | _ => I)) + step [] val refed_by_vect = Vector.tabulate (Vector.length step_vect, K []) |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) steps @@ -97,8 +99,8 @@ algorithm) *) fun add_if_cand step_vect (i, [j]) = ((case (the (get i step_vect), the (get j step_vect)) of - (Prove (_, Fix [], _, t, By_Metis _), Prove (_, _, _, _, By_Metis _)) => - cons (Term.size_of_term t, i) + (Prove (_, Fix [], _, t, _, By_Metis _), + Prove (_, _, _, _, _, By_Metis _)) => cons (Term.size_of_term t, i) | _ => I) handle Option.Option => raise Fail "sledgehammer_compress: add_if_cand") | add_if_cand _ _ = I @@ -126,13 +128,13 @@ (* Merging *) fun merge - (Prove (_, Fix [], lbl1, _, By_Metis (subproofs1, (lfs1, gfs1)))) - (Prove (qs2, fix, lbl2, t, By_Metis (subproofs2, (lfs2, gfs2)))) = + (Prove (_, Fix [], lbl1, _, subproofs1, By_Metis (lfs1, gfs1))) + (Prove (qs2, fix, lbl2, t, subproofs2, By_Metis (lfs2, gfs2))) = let val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1 val gfs = union (op =) gfs1 gfs2 val subproofs = subproofs1 @ subproofs2 - in Prove (qs2, fix, lbl2, t, By_Metis (subproofs, (lfs, gfs))) end + in Prove (qs2, fix, lbl2, t, subproofs, By_Metis (lfs, gfs)) end | merge _ _ = raise Fail "sledgehammer_compress: unmergeable Isar steps" fun try_merge metis_time (s1, i) (s2, j) = @@ -209,7 +211,7 @@ fun enrich_with_fact l t = Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) - fun enrich_with_step (Prove (_, _, l, t, _)) = enrich_with_fact l t + fun enrich_with_step (Prove (_, _, l, t, _, _)) = enrich_with_fact l t | enrich_with_step _ = I val enrich_with_steps = fold enrich_with_step val enrich_with_assms = fold (uncurry enrich_with_fact) @@ -234,9 +236,9 @@ in fold_map f_m subproofs zero_preplay_time end val compress_subproofs = compress_each_and_collect_time (do_proof false ctxt) - fun compress (Prove (qs, fix, l, t, By_Metis(subproofs, facts))) = + fun compress (Prove (qs, fix, l, t, subproofs, By_Metis facts)) = let val (subproofs, time) = compress_subproofs subproofs - in (Prove (qs, fix, l, t, By_Metis(subproofs, facts)), time) end + in (Prove (qs, fix, l, t, subproofs, By_Metis facts), time) end | compress atomic_step = (atomic_step, zero_preplay_time) in compress_each_and_collect_time compress subproofs diff -r 2cba5906d836 -r b528a975b256 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Jun 26 18:25:13 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Jun 26 18:26:00 2013 +0200 @@ -79,7 +79,7 @@ fun thm_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) = let val concl = (case try List.last steps of - SOME (Prove (_, Fix [], _, t, _)) => t + SOME (Prove (_, Fix [], _, t, _, _)) => t | _ => raise Fail "preplay error: malformed subproof") val var_idx = maxidx_of_term concl + 1 fun var_of_free (x, T) = Var((x, var_idx), T) @@ -93,7 +93,7 @@ fun try_metis _ _ _ _ _ _ (Let _) = K zero_preplay_time | try_metis debug trace type_enc lam_trans ctxt timeout - (Prove (_, Fix xs, _, t, By_Metis (subproofs, fact_names))) = + (Prove (_, Fix xs, _, t, subproofs, By_Metis fact_names)) = let val (prop, obtain) = (case xs of diff -r 2cba5906d836 -r b528a975b256 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jun 26 18:25:13 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jun 26 18:26:00 2013 +0200 @@ -9,21 +9,21 @@ signature SLEDGEHAMMER_PROOF = sig type label = string * int - type facts = label list * string list (* local & global *) + type facts = label list * string list (* local & global facts *) datatype isar_qualifier = Show | Then datatype fix = Fix of (string * typ) list datatype assms = Assume of (label * term) list - datatype isar_proof = + datatype isar_proof = Proof of fix * assms * isar_step list and isar_step = Let of term * term | - (* for |fix|>0, this is an obtain step *) - Prove of isar_qualifier list * fix * label * term * byline + (* for |fix|>0, this is an obtain step; step may contain subproofs *) + Prove of isar_qualifier list * fix * label * term * isar_proof list * byline and byline = - By_Metis of isar_proof list * facts + By_Metis of facts val no_label : label val no_facts : facts @@ -34,8 +34,13 @@ val steps_of_proof : isar_proof -> isar_step list val label_of_step : isar_step -> label option + val subproofs_of_step : isar_step -> isar_proof list option val byline_of_step : isar_step -> byline option + val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a + val fold_isar_steps : + (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a + val add_metis_steps_top_level : isar_step list -> int -> int val add_metis_steps : isar_step list -> int -> int end @@ -44,21 +49,21 @@ struct type label = string * int -type facts = label list * string list +type facts = label list * string list (* local & global facts *) datatype isar_qualifier = Show | Then datatype fix = Fix of (string * typ) list datatype assms = Assume of (label * term) list -datatype isar_proof = +datatype isar_proof = Proof of fix * assms * isar_step list and isar_step = Let of term * term | - (* for |fix|>0, this is an obtain step *) - Prove of isar_qualifier list * fix * label * term * byline + (* for |fix|>0, this is an obtain step; step may contain subproofs *) + Prove of isar_qualifier list * fix * label * term * isar_proof list * byline and byline = - By_Metis of isar_proof list * facts + By_Metis of facts val no_label = ("", ~1) val no_facts = ([],[]) @@ -69,20 +74,26 @@ fun assms_of_proof (Proof (_, assms, _)) = assms fun steps_of_proof (Proof (_, _, steps)) = steps -fun label_of_step (Prove (_, _, l, _, _)) = SOME l +fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l | label_of_step _ = NONE -fun byline_of_step (Prove (_, _, _, _, byline)) = SOME byline +fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs + | subproofs_of_step _ = NONE + +fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline | byline_of_step _ = NONE +fun fold_isar_step f step s = + fold (steps_of_proof #> fold (fold_isar_step f)) + (the_default [] (subproofs_of_step step)) s + |> f step + +fun fold_isar_steps f = fold (fold_isar_step f) + val add_metis_steps_top_level = fold (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I)) -fun add_metis_steps steps = - fold (byline_of_step - #> (fn SOME (By_Metis (subproofs, _)) => - Integer.add 1 #> add_substeps subproofs - | _ => I)) steps -and add_substeps subproofs = fold (steps_of_proof #> add_metis_steps) subproofs - +val add_metis_steps = + fold_isar_steps + (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I)) end diff -r 2cba5906d836 -r b528a975b256 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jun 26 18:25:13 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jun 26 18:26:00 2013 +0200 @@ -519,7 +519,7 @@ #> add_suffix " = " #> add_term t2 #> add_suffix "\n" - | add_step ind (Prove (qs, Fix xs, l, t, By_Metis (subproofs, facts))) = + | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By_Metis facts)) = (case xs of [] => (* have *) add_step_pre ind qs subproofs @@ -549,26 +549,24 @@ (* One-step proofs are pointless; better use the Metis one-liner directly. *) case proof of - Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, By_Metis ([], _))]) => "" + Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, [], _)]) => "" | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ of_indent 0 ^ (if n <> 1 then "next" else "qed") end -fun add_labels_of_step step = - case byline_of_step step of - NONE => I - | SOME (By_Metis (subproofs, (ls, _))) => - union (op =) ls #> fold add_labels_of_proof subproofs -and add_labels_of_proof proof = fold add_labels_of_step (steps_of_proof proof) +val add_labels_of_proof = + steps_of_proof #> fold_isar_steps + (byline_of_step #> (fn SOME (By_Metis (ls, _)) => union (op =) ls + | _ => I)) fun kill_useless_labels_in_proof proof = let val used_ls = add_labels_of_proof proof [] fun do_label l = if member (op =) used_ls l then l else no_label fun do_assms (Assume assms) = Assume (map (apfst do_label) assms) - fun do_step (Prove (qs, xs, l, t, By_Metis (subproofs, facts))) = - Prove (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts)) + fun do_step (Prove (qs, xs, l, t, subproofs, by)) = + Prove (qs, xs, do_label l, t, map do_proof subproofs, by) | do_step step = step and do_proof (Proof (fix, assms, steps)) = Proof (fix, do_assms assms, map do_step steps) @@ -599,20 +597,21 @@ |> apfst Assume |> apsnd fst fun do_steps _ _ _ [] = [] - | do_steps subst depth next (Prove (qs, xs, l, t, by) :: steps) = + | do_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) = let val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix + val sub = do_proofs subst depth sub val by = by |> do_byline subst depth - in Prove (qs, xs, l, t, by) :: do_steps subst depth next steps end + in Prove (qs, xs, l, t, sub, by) :: do_steps subst depth next steps end | do_steps subst depth next (step :: steps) = step :: do_steps subst depth next steps and do_proof subst depth (Proof (fix, assms, steps)) = let val (assms, subst) = do_assms subst depth assms in Proof (fix, assms, do_steps subst depth 1 steps) end - and do_byline subst depth (By_Metis (subproofs, facts)) = - By_Metis (do_proofs subst depth subproofs, do_facts subst facts) + and do_byline subst depth (By_Metis facts) = + By_Metis (do_facts subst facts) and do_proofs subst depth = map (do_proof subst (depth + 1)) in do_proof [] 0 end @@ -622,11 +621,10 @@ | do_qs_lfs (SOME l0) lfs = if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs) - fun chain_step lbl (Prove (qs, xs, l, t, - By_Metis (subproofs, (lfs, gfs)))) = + fun chain_step lbl (Prove (qs, xs, l, t, subproofs, By_Metis (lfs, gfs))) = let val (qs', lfs) = do_qs_lfs lbl lfs in - Prove (qs' @ qs, xs, l, t, - By_Metis (chain_proofs subproofs, (lfs, gfs))) + Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, + By_Metis (lfs, gfs)) end | chain_step _ step = step and chain_steps _ [] = [] @@ -745,8 +743,8 @@ accum |> (if tainted = [] then cons (Prove (if outer then [Show] else [], - Fix [], no_label, concl_t, - By_Metis ([], ([the predecessor], [])))) + Fix [], no_label, concl_t, [], + By_Metis ([the predecessor], []))) else I) |> rev @@ -755,10 +753,10 @@ val l = label_of_clause c val t = prop_of_clause c val by = - By_Metis ([], - (fold (add_fact_of_dependencies fact_names) - gamma no_facts)) - fun prove by = Prove (maybe_show outer c [], Fix [], l, t, by) + By_Metis + (fold (add_fact_of_dependencies fact_names) gamma no_facts) + fun prove sub by = + Prove (maybe_show outer c [], Fix [], l, t, sub, by) fun do_rest l step = do_steps outer (SOME l) (step :: accum) infs in @@ -773,16 +771,16 @@ Assume [], rev accum) in do_steps outer (SOME l) - [prove (By_Metis ([subproof], no_facts))] [] + [prove [subproof] (By_Metis no_facts)] [] end else - do_rest l (prove by) - | _ => do_rest l (prove by) + do_rest l (prove [] by) + | _ => do_rest l (prove [] by) else if is_clause_skolemize_rule c then - do_rest l (Prove ([], Fix (skolems_of t), l, t, by)) + do_rest l (Prove ([], Fix (skolems_of t), l, t, [], by)) else - do_rest l (prove by) + do_rest l (prove [] by) end | do_steps outer predecessor accum (Cases cases :: infs) = let @@ -794,7 +792,7 @@ val t = prop_of_clause c val step = Prove (maybe_show outer c [], Fix [], l, t, - By_Metis (map do_case cases, (the_list predecessor, []))) + map do_case cases, By_Metis (the_list predecessor, [])) in do_steps outer (SOME l) (step :: accum) infs end