# HG changeset patch # User blanchet # Date 1357137840 -3600 # Node ID ab5b8b5c9cbe677cff96e11d89568c470ead3a4e # Parent 6632cb8df708cf399c3b4cc3335ef2bd96afaa5a added "obtain" to Isar proof construction data structure diff -r 6632cb8df708 -r ab5b8b5c9cbe src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jan 02 13:31:13 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jan 02 15:44:00 2013 +0100 @@ -17,6 +17,8 @@ Fix of (string * typ) list | Let of term * term | Assume of label * term | + Obtain of + isar_qualifier list * (string * typ) list * label * term * byline | Prove of isar_qualifier list * label * term * byline and byline = By_Metis of facts | @@ -27,7 +29,7 @@ val metis_steps_total : isar_step list -> int end -structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = +structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = struct type label = string * int @@ -39,6 +41,7 @@ Fix of (string * typ) list | Let of term * term | Assume of label * term | + Obtain of isar_qualifier list * (string * typ) list * label * term * byline | Prove of isar_qualifier list * label * term * byline and byline = By_Metis of facts | @@ -46,12 +49,14 @@ fun string_for_label (s, num) = s ^ string_of_int num -val inc = curry op+ -fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0 -fun metis_steps_total proof = - fold (fn Prove (_,_,_, By_Metis _) => inc 1 - | Prove (_,_,_, Case_Split (cases, _)) => - inc (fold (inc o metis_steps_total) cases 1) +fun metis_steps_top_level proof = + fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I) + proof 0 +fun metis_steps_total proof = + fold (fn Obtain _ => Integer.add 1 + | Prove (_, _, _, By_Metis _) => Integer.add 1 + | Prove (_, _, _, Case_Split (cases, _)) => + Integer.add (fold (Integer.add o metis_steps_total) cases 1) | _ => I) proof 0 end diff -r 6632cb8df708 -r ab5b8b5c9cbe src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 13:31:13 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 15:44:00 2013 +0100 @@ -467,13 +467,16 @@ if member (op =) qs Show then "thus" else "hence" else if member (op =) qs Show then "show" else "have") + fun do_obtain qs xs = + (if member (op =) qs Then then "then " else "") ^ "obtain " ^ + (space_implode " " (map fst xs)) val do_term = annotate_types ctxt #> with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces #> maybe_quote val reconstr = Metis (type_enc, lam_trans) - fun do_facts ind (ls, ss) = + fun do_metis ind (ls, ss) = "\n" ^ do_indent (ind + 1) ^ reconstructor_command reconstr 1 1 [] 0 (ls |> sort_distinct (prod_ord string_ord int_ord), @@ -484,14 +487,17 @@ do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" | do_step ind (Assume (l, t)) = do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" + | do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) = + do_indent ind ^ do_obtain qs xs ^ " " ^ + do_label l ^ do_term t ^ do_metis ind facts ^ "\n" | do_step ind (Prove (qs, l, t, By_Metis facts)) = do_indent ind ^ do_have qs ^ " " ^ - do_label l ^ do_term t ^ do_facts ind facts ^ "\n" + do_label l ^ do_term t ^ do_metis ind facts ^ "\n" | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) proofs) ^ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ - do_facts ind facts ^ "\n" + do_metis ind facts ^ "\n" and do_steps prefix suffix ind steps = let val s = implode (map (do_step ind) steps) in replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ @@ -509,7 +515,8 @@ (if n <> 1 then "next" else "qed") in do_proof end -fun used_labels_of_step (Prove (_, _, _, by)) = +fun used_labels_of_step (Obtain (_, _, _, _, By_Metis (ls, _))) = ls + | used_labels_of_step (Prove (_, _, _, by)) = (case by of By_Metis (ls, _) => ls | Case_Split (proofs, (ls, _)) => @@ -522,6 +529,7 @@ val used_ls = used_labels_of proof fun do_label l = if member (op =) used_ls l then l else no_label fun do_step (Assume (l, t)) = Assume (do_label l, t) + | do_step (Obtain (qs, xs, l, t, by)) = Obtain (qs, xs, do_label l, t, by) | do_step (Prove (qs, l, t, by)) = Prove (qs, do_label l, t, case by of @@ -535,60 +543,77 @@ val relabel_proof = let - fun aux _ _ _ [] = [] - | aux subst depth (next_assum, next_have) (Assume (l, t) :: proof) = + fun fresh_label depth (old as (l, subst, next_have)) = + if l = no_label then + old + else + let val l' = (prefix_for_depth depth have_prefix, next_have) in + (l', (l, l') :: subst, next_have + 1) + end + fun do_facts subst = + apfst (maps (the_list o AList.lookup (op =) subst)) + fun do_byline subst depth by = + case by of + By_Metis facts => By_Metis (do_facts subst facts) + | Case_Split (proofs, facts) => + Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs, + do_facts subst facts) + and do_proof _ _ _ [] = [] + | do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) = if l = no_label then - Assume (l, t) :: aux subst depth (next_assum, next_have) proof + Assume (l, t) :: do_proof subst depth (next_assum, next_have) proof else let val l' = (prefix_for_depth depth assume_prefix, next_assum) in Assume (l', t) :: - aux ((l, l') :: subst) depth (next_assum + 1, next_have) proof + do_proof ((l, l') :: subst) depth (next_assum + 1, next_have) proof end - | aux subst depth (next_assum, next_have) + | do_proof subst depth (next_assum, next_have) + (Obtain (qs, xs, l, t, by) :: proof) = + let + val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth + val by = by |> do_byline subst depth + in + Obtain (qs, xs, l, t, by) :: + do_proof subst depth (next_assum, next_have) proof + end + | do_proof subst depth (next_assum, next_have) (Prove (qs, l, t, by) :: proof) = let - val (l', subst, next_have) = - if l = no_label then - (l, subst, next_have) - else - let val l' = (prefix_for_depth depth have_prefix, next_have) in - (l', (l, l') :: subst, next_have + 1) - end - val relabel_facts = - apfst (maps (the_list o AList.lookup (op =) subst)) - val by = - case by of - By_Metis facts => By_Metis (relabel_facts facts) - | Case_Split (proofs, facts) => - Case_Split (map (aux subst (depth + 1) (1, 1)) proofs, - relabel_facts facts) + val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth + val by = by |> do_byline subst depth in - Prove (qs, l', t, by) :: aux subst depth (next_assum, next_have) proof + Prove (qs, l, t, by) :: + do_proof subst depth (next_assum, next_have) proof end - | aux subst depth nextp (step :: proof) = - step :: aux subst depth nextp proof - in aux [] 0 (1, 1) end + | do_proof subst depth nextp (step :: proof) = + step :: do_proof subst depth nextp proof + in do_proof [] 0 (1, 1) end val chain_direct_proof = let - fun succedent_of_step (Prove (_, label, _, _)) = SOME label - | succedent_of_step (Assume (label, _)) = SOME label - | succedent_of_step _ = NONE - fun chain_inf (SOME label0) - (step as Prove (qs, label, t, By_Metis (lfs, gfs))) = - if member (op =) lfs label0 then - Prove (Then :: qs, label, t, - By_Metis (filter_out (curry (op =) label0) lfs, gfs)) + fun label_of (Assume (l, _)) = SOME l + | label_of (Obtain (_, _, l, _, _)) = SOME l + | label_of (Prove (_, l, _, _)) = SOME l + | label_of _ = NONE + fun chain_step (SOME l0) + (step as Obtain (qs, xs, l, t, By_Metis (lfs, gfs))) = + if member (op =) lfs l0 then + Obtain (Then :: qs, xs, l, t, By_Metis (lfs |> remove (op =) l0, gfs)) else step - | chain_inf _ (Prove (qs, label, t, Case_Split (proofs, facts))) = - Prove (qs, label, t, Case_Split ((map (chain_proof NONE) proofs), facts)) - | chain_inf _ step = step + | chain_step (SOME l0) + (step as Prove (qs, l, t, By_Metis (lfs, gfs))) = + if member (op =) lfs l0 then + Prove (Then :: qs, l, t, By_Metis (lfs |> remove (op =) l0, gfs)) + else + step + | chain_step _ (Prove (qs, l, t, Case_Split (proofs, facts))) = + Prove (qs, l, t, Case_Split ((map (chain_proof NONE) proofs), facts)) + | chain_step _ step = step and chain_proof _ [] = [] | chain_proof (prev as SOME _) (i :: is) = - chain_inf prev i :: chain_proof (succedent_of_step i) is - | chain_proof _ (i :: is) = - i :: chain_proof (succedent_of_step i) is + chain_step prev i :: chain_proof (label_of i) is + | chain_proof _ (i :: is) = i :: chain_proof (label_of i) is in chain_proof NONE end type isar_params = diff -r 6632cb8df708 -r ab5b8b5c9cbe src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Jan 02 13:31:13 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Jan 02 15:44:00 2013 +0100 @@ -8,7 +8,7 @@ signature SLEDGEHAMMER_SHRINK = sig type isar_step = Sledgehammer_Proof.isar_step - val shrink_proof : + val shrink_proof : bool -> Proof.context -> string -> string -> bool -> Time.time option -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time)) end @@ -58,225 +58,229 @@ (* Main function for shrinking proofs *) fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout isar_shrink proof = -let - (* 60 seconds seems like a good interpreation of "no timeout" *) - val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) - - (* handle metis preplay fail *) - local - open Unsynchronized - val metis_fail = ref false - in - fun handle_metis_fail try_metis () = - try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime) - fun get_time lazy_time = - if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time - val metis_fail = fn () => !metis_fail - end - - (* Shrink top level proof - do not shrink case splits *) - fun shrink_top_level on_top_level ctxt proof = let - (* proof vector *) - val proof_vect = proof |> map SOME |> Vector.fromList - val n = Vector.length proof_vect - val n_metis = metis_steps_top_level proof - val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round - - (* table for mapping from (top-level-)label to proof position *) - fun update_table (i, Assume (label, _)) = - Label_Table.update_new (label, i) - | update_table (i, Prove (_, label, _, _)) = - Label_Table.update_new (label, i) - | update_table _ = I - val label_index_table = fold_index update_table proof Label_Table.empty - - (* proof references *) - fun refs (Prove (_, _, _, By_Metis (lfs, _))) = - map_filter (Label_Table.lookup label_index_table) lfs - | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = - map_filter (Label_Table.lookup label_index_table) lfs - @ maps (maps refs) cases - | refs _ = [] - val refed_by_vect = - Vector.tabulate (n, (fn _ => [])) - |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof - |> Vector.map rev (* after rev, indices are sorted in ascending order *) - - (* candidates for elimination, use table as priority queue (greedy - algorithm) *) - fun add_if_cand proof_vect (i, [j]) = - (case (the (get i proof_vect), the (get j proof_vect)) of - (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => - cons (Term.size_of_term t, i) - | _ => I) - | add_if_cand _ _ = I - val cand_tab = - v_fold_index (add_if_cand proof_vect) refed_by_vect [] - |> Inttab.make_list - - (* Metis Preplaying *) - fun resolve_fact_names names = - names - |>> map string_for_label - |> op @ - |> maps (thms_of_name ctxt) - - fun try_metis timeout (succedent, Prove (_, _, t, byline)) = - if not preplay then (fn () => SOME Time.zeroTime) else - (case byline of - By_Metis fact_names => - let - val facts = resolve_fact_names fact_names - val goal = - Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t - fun tac {context = ctxt, prems = _} = - Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 - in - take_time timeout (fn () => goal tac) - end - | Case_Split (cases, fact_names) => - let - val facts = - resolve_fact_names fact_names - @ (case the succedent of - Prove (_, _, t, _) => - Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t - | Assume (_, t) => - Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t - | _ => error "Internal error: unexpected succedent of case split") - :: map - (hd #> (fn Assume (_, a) => Logic.mk_implies(a, t) - | _ => error "Internal error: malformed case split") - #> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)) - cases - val goal = - Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t - fun tac {context = ctxt, prems = _} = - Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 - in - take_time timeout (fn () => goal tac) - end) - | try_metis _ _ = (fn () => SOME Time.zeroTime) + (* 60 seconds seems like a good interpreation of "no timeout" *) + val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) - val try_metis_quietly = the_default NONE oo try oo try_metis - - (* cache metis preplay times in lazy time vector *) - val metis_time = - v_map_index - (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout - o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the) - proof_vect - fun sum_up_time lazy_time_vector = - Vector.foldl - ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts)) - | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout))) - o apfst get_time) - no_time lazy_time_vector - - (* Merging *) - fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) - (Prove (qs2, label2 , t, By_Metis (lfs2, gfs2))) = - let - 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 - | merge _ _ = error "Internal error: Tring to merge unmergable isar steps" - - fun try_merge metis_time (s1, i) (s2, j) = - (case get i metis_time |> Lazy.force of - NONE => (NONE, metis_time) - | SOME t1 => - (case get j metis_time |> Lazy.force of - NONE => (NONE, metis_time) - | SOME t2 => - let - val s12 = merge s1 s2 - val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) - in - case try_metis_quietly timeout (NONE, s12) () of - NONE => (NONE, metis_time) - | some_t12 => - (SOME s12, metis_time - |> replace (Time.zeroTime |> SOME |> Lazy.value) i - |> replace (Lazy.value some_t12) j) - - end)) - - 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 (on_top_level andalso n'<3) - then - (Vector.foldr - (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof) - [] proof_vect, - sum_up_time metis_time) - else - let - val (i, cand_tab) = pop_max cand_tab - val j = get i refed_by |> the_single - val s1 = get i proof_vect |> the - val s2 = get j proof_vect |> the - in - case try_merge metis_time (s1, i) (s2, j) of - (NONE, metis_time) => - merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' - | (s, metis_time) => - let - val refs = refs s1 - val refed_by = refed_by |> fold - (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs - val new_candidates = - fold (add_if_cand proof_vect) - (map (fn i => (i, get i refed_by)) refs) [] - val cand_tab = add_list cand_tab new_candidates - val proof_vect = proof_vect |> replace NONE i |> replace s j - in - merge_steps metis_time proof_vect refed_by cand_tab (n' - 1) (n_metis' - 1) - end - end - in - merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis - end - - fun shrink_proof' on_top_level ctxt proof = - let - (* Enrich context with top-level facts *) - val thy = Proof_Context.theory_of ctxt - fun enrich_ctxt (Assume (label, t)) ctxt = - Proof_Context.put_thms false - (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt - | enrich_ctxt (Prove (_, label, t, _)) ctxt = - Proof_Context.put_thms false - (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt - | enrich_ctxt _ ctxt = ctxt - val rich_ctxt = fold enrich_ctxt proof ctxt - - (* Shrink case_splits and top-levl *) - val ((proof, top_level_time), lower_level_time) = - proof |> shrink_case_splits rich_ctxt - |>> shrink_top_level on_top_level rich_ctxt + (* handle metis preplay fail *) + local + open Unsynchronized + val metis_fail = ref false in - (proof, ext_time_add lower_level_time top_level_time) + fun handle_metis_fail try_metis () = + try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime) + fun get_time lazy_time = + if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time + val metis_fail = fn () => !metis_fail end - and shrink_case_splits ctxt proof = + (* Shrink top level proof - do not shrink case splits *) + fun shrink_top_level on_top_level ctxt proof = let - 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_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_each_and_collect_time shrink proof + (* proof vector *) + val proof_vect = proof |> map SOME |> Vector.fromList + val n = Vector.length proof_vect + val n_metis = metis_steps_top_level proof + val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round + + (* table for mapping from (top-level-)label to proof position *) + fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i) + | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i) + | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i) + | update_table _ = I + val label_index_table = fold_index update_table proof Label_Table.empty + val filter_refs = map_filter (Label_Table.lookup label_index_table) + + (* proof references *) + fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = filter_refs lfs + | refs (Prove (_, _, _, By_Metis (lfs, _))) = filter_refs lfs + | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = + filter_refs lfs @ maps (maps refs) cases + | refs _ = [] + val refed_by_vect = + Vector.tabulate (n, (fn _ => [])) + |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof + |> Vector.map rev (* after rev, indices are sorted in ascending order *) + + (* candidates for elimination, use table as priority queue (greedy + algorithm) *) + (* TODO: consider adding "Obtain" cases *) + fun add_if_cand proof_vect (i, [j]) = + (case (the (get i proof_vect), the (get j proof_vect)) of + (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => + cons (Term.size_of_term t, i) + | _ => I) + | add_if_cand _ _ = I + val cand_tab = + v_fold_index (add_if_cand proof_vect) refed_by_vect [] + |> Inttab.make_list + + (* Metis Preplaying *) + fun resolve_fact_names names = + names + |>> map string_for_label + |> op @ + |> maps (thms_of_name ctxt) + + (* TODO: add "Obtain" case *) + fun try_metis timeout (succedent, Prove (_, _, t, byline)) = + if not preplay then K (SOME Time.zeroTime) else + (case byline of + By_Metis fact_names => + let + val facts = resolve_fact_names fact_names + val goal = + Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t + fun tac {context = ctxt, prems = _} = + Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 + in + take_time timeout (fn () => goal tac) + end + | Case_Split (cases, fact_names) => + let + val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) + val facts = + resolve_fact_names fact_names + @ (case the succedent of + Assume (_, t) => make_thm t + | Obtain (_, _, _, t, _) => make_thm t + | Prove (_, _, t, _) => make_thm t + | _ => error "Internal error: unexpected succedent of case split") + :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) + | _ => error "Internal error: malformed case split") + #> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)) + cases + val goal = + Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t + fun tac {context = ctxt, prems = _} = + Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 + in + take_time timeout (fn () => goal tac) + end) + | try_metis _ _ = K (SOME Time.zeroTime) + + val try_metis_quietly = the_default NONE oo try oo try_metis + + (* cache metis preplay times in lazy time vector *) + val metis_time = + v_map_index + (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout + o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the) + proof_vect + fun sum_up_time lazy_time_vector = + Vector.foldl + ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts)) + | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout))) + o apfst get_time) + no_time lazy_time_vector + + (* Merging *) + (* TODO: consider adding "Obtain" cases *) + fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) + (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) = + let + 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 + | merge _ _ = error "Internal error: Unmergeable Isar steps" + + fun try_merge metis_time (s1, i) (s2, j) = + (case get i metis_time |> Lazy.force of + NONE => (NONE, metis_time) + | SOME t1 => + (case get j metis_time |> Lazy.force of + NONE => (NONE, metis_time) + | SOME t2 => + let + val s12 = merge s1 s2 + val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) + in + case try_metis_quietly timeout (NONE, s12) () of + NONE => (NONE, metis_time) + | some_t12 => + (SOME s12, metis_time + |> replace (Time.zeroTime |> SOME |> Lazy.value) i + |> replace (Lazy.value some_t12) j) + + end)) + + 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 (on_top_level andalso n'<3) + then + (Vector.foldr + (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof) + [] proof_vect, + sum_up_time metis_time) + else + let + val (i, cand_tab) = pop_max cand_tab + val j = get i refed_by |> the_single + val s1 = get i proof_vect |> the + val s2 = get j proof_vect |> the + in + case try_merge metis_time (s1, i) (s2, j) of + (NONE, metis_time) => + merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' + | (s, metis_time) => + let + val refs = refs s1 + val refed_by = refed_by |> fold + (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs + val new_candidates = + fold (add_if_cand proof_vect) + (map (fn i => (i, get i refed_by)) refs) [] + val cand_tab = add_list cand_tab new_candidates + val proof_vect = proof_vect |> replace NONE i |> replace s j + in + merge_steps metis_time proof_vect refed_by cand_tab (n' - 1) + (n_metis' - 1) + end + end + in + merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis end -in - shrink_proof' true ctxt proof - |> apsnd (pair (metis_fail () ) ) -end + + fun do_proof on_top_level ctxt proof = + let + (* Enrich context with top-level facts *) + val thy = Proof_Context.theory_of ctxt + (* TODO: add Skolem variables to context? *) + fun enrich_with_fact l t = + Proof_Context.put_thms false + (string_for_label l, SOME [Skip_Proof.make_thm thy t]) + fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t + | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t + | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t + | enrich_with_step _ = I + val rich_ctxt = fold enrich_with_step proof ctxt + + (* Shrink case_splits and top-levl *) + val ((proof, top_level_time), lower_level_time) = + proof |> do_case_splits rich_ctxt + |>> shrink_top_level on_top_level rich_ctxt + in + (proof, ext_time_add lower_level_time top_level_time) + end + + and do_case_splits ctxt proof = + let + 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_each_and_collect_time (do_proof false ctxt) + fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) = + let val (cases, time) = shrink_case_split cases + in (Prove (qs, l, t, Case_Split (cases, facts)), time) end + | shrink step = (step, no_time) + in + shrink_each_and_collect_time shrink proof + end + in + do_proof true ctxt proof + |> apsnd (pair (metis_fail ())) + end end