# HG changeset patch # User smolkas # Date 1372263913 -7200 # Node ID 2cba5906d836e9f8649295a475ac168ba2bd108a # Parent 2207825d67f31b29fa7f60cf68c1767d3282212e simplified data structure diff -r 2207825d67f3 -r 2cba5906d836 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Jun 26 18:24:41 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Jun 26 18:25:13 2013 +0200 @@ -77,8 +77,7 @@ 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) - | update_table (i, Obtain (_, _, 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) @@ -98,9 +97,7 @@ algorithm) *) fun add_if_cand step_vect (i, [j]) = ((case (the (get i step_vect), the (get j step_vect)) of - (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => - cons (Term.size_of_term t, i) - | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) => + (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") @@ -128,19 +125,14 @@ zero_preplay_time lazy_time_vector (* Merging *) - fun merge (Prove (_, lbl1, _, By_Metis (subproofs1, (lfs1, gfs1)))) step2 = - let - val (step_constructor, (subproofs2, (lfs2, gfs2))) = - (case step2 of - Prove (qs2, lbl2, t, By_Metis x) => - (fn by => Prove (qs2, lbl2, t, by), x) - | Obtain (qs2, xs, lbl2, t, By_Metis x) => - (fn by => Obtain (qs2, xs, lbl2, t, by), x) - | _ => raise Fail "sledgehammer_compress: unmergeable Isar steps" ) - val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1 - val gfs = union (op =) gfs1 gfs2 - val subproofs = subproofs1 @ subproofs2 - in step_constructor (By_Metis (subproofs, (lfs, gfs))) end + fun merge + (Prove (_, Fix [], lbl1, _, By_Metis (subproofs1, (lfs1, gfs1)))) + (Prove (qs2, fix, lbl2, t, By_Metis (subproofs2, (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 | merge _ _ = raise Fail "sledgehammer_compress: unmergeable Isar steps" fun try_merge metis_time (s1, i) (s2, j) = @@ -217,8 +209,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 - | enrich_with_step (Obtain (_, _, 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) @@ -243,9 +234,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, l, t, By_Metis(subproofs, facts))) = + fun compress (Prove (qs, fix, l, t, By_Metis(subproofs, facts))) = let val (subproofs, time) = compress_subproofs subproofs - in (Prove (qs, l, t, By_Metis(subproofs, facts)), time) end + in (Prove (qs, fix, l, t, By_Metis(subproofs, facts)), time) end | compress atomic_step = (atomic_step, zero_preplay_time) in compress_each_and_collect_time compress subproofs diff -r 2207825d67f3 -r 2cba5906d836 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Jun 26 18:24:41 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Jun 26 18:25:13 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 (_, _, 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) @@ -91,16 +91,15 @@ |> thm_of_term ctxt end -exception ZEROTIME - -fun try_metis debug trace type_enc lam_trans ctxt timeout step = +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))) = let - val (prop, subproofs, fact_names, obtain) = - (case step of - Prove (_, _, t, By_Metis (subproofs, fact_names)) => - (t, subproofs, fact_names, false) - | Obtain (_, Fix xs, _, t, By_Metis (subproofs, fact_names)) => - (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis + val (prop, obtain) = + (case xs of + [] => (t, false) + | _ => + (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis (see ~~/src/Pure/Isar/obtain.ML) *) let val thesis = Term.Free ("thesis", HOLogic.boolT) @@ -115,9 +114,8 @@ val prop = Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) in - (prop, subproofs, fact_names, true) - end - | _ => raise ZEROTIME) + (prop, true) + end) val facts = map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug @@ -138,7 +136,6 @@ preplay_time end end - handle ZEROTIME => K zero_preplay_time (* this version treats exceptions like timeouts *) fun try_metis_quietly debug trace type_enc lam_trans ctxt timeout = diff -r 2207825d67f3 -r 2cba5906d836 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jun 26 18:24:41 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jun 26 18:25:13 2013 +0200 @@ -20,8 +20,8 @@ Proof of fix * assms * isar_step list and isar_step = Let of term * term | - Prove of isar_qualifier list * label * term * byline | - Obtain of isar_qualifier list * fix * label * term * byline + (* for |fix|>0, this is an obtain step *) + Prove of isar_qualifier list * fix * label * term * byline and byline = By_Metis of isar_proof list * facts @@ -55,8 +55,8 @@ Proof of fix * assms * isar_step list and isar_step = Let of term * term | - Prove of isar_qualifier list * label * term * byline | - Obtain of isar_qualifier list * fix * label * term * byline + (* for |fix|>0, this is an obtain step *) + Prove of isar_qualifier list * fix * label * term * byline and byline = By_Metis of isar_proof list * facts @@ -69,12 +69,10 @@ fun assms_of_proof (Proof (_, assms, _)) = assms fun steps_of_proof (Proof (_, _, steps)) = steps -fun label_of_step (Obtain (_, _, l, _, _)) = SOME l - | label_of_step (Prove (_, l, _, _)) = SOME l +fun label_of_step (Prove (_, _, l, _, _)) = SOME l | label_of_step _ = NONE -fun byline_of_step (Obtain (_, _, _, _, byline)) = SOME byline - | byline_of_step (Prove (_, _, _, byline)) = SOME byline +fun byline_of_step (Prove (_, _, _, _, byline)) = SOME byline | byline_of_step _ = NONE val add_metis_steps_top_level = diff -r 2207825d67f3 -r 2cba5906d836 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jun 26 18:24:41 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jun 26 18:25:13 2013 +0200 @@ -519,23 +519,25 @@ #> add_suffix " = " #> add_term t2 #> add_suffix "\n" - | add_step ind (Prove (qs, l, t, By_Metis (subproofs, facts))) = - add_step_pre ind qs subproofs - #> add_suffix (of_prove qs (length subproofs) ^ " ") - #> add_step_post ind l t facts "" - | add_step ind (Obtain (qs, Fix xs, l, t, By_Metis (subproofs, facts))) = - add_step_pre ind qs subproofs - #> add_suffix (of_obtain qs (length subproofs) ^ " ") - #> add_frees xs - #> add_suffix " where " - (* The new skolemizer puts the arguments in the same order as the ATPs - (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding - Vampire). *) - #> add_step_post ind l t facts - (if exists (fn (_, T) => length (binder_types T) > 1) xs then - "using [[metis_new_skolem]] " - else - "") + | add_step ind (Prove (qs, Fix xs, l, t, By_Metis (subproofs, facts))) = + (case xs of + [] => (* have *) + add_step_pre ind qs subproofs + #> add_suffix (of_prove qs (length subproofs) ^ " ") + #> add_step_post ind l t facts "" + | _ => (* obtain *) + add_step_pre ind qs subproofs + #> add_suffix (of_obtain qs (length subproofs) ^ " ") + #> add_frees xs + #> add_suffix " where " + (* The new skolemizer puts the arguments in the same order as the + ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML" + regarding Vampire). *) + #> add_step_post ind l t facts + (if exists (fn (_, T) => length (binder_types T) > 1) xs then + "using [[metis_new_skolem]] " + else + "")) and add_steps ind = fold (add_step ind) and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) = ("", ctxt) @@ -547,7 +549,7 @@ (* One-step proofs are pointless; better use the Metis one-liner directly. *) case proof of - Proof (Fix [], Assume [], [Prove (_, _, _, By_Metis ([], _))]) => "" + Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, By_Metis ([], _))]) => "" | _ => (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") @@ -565,10 +567,8 @@ 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 (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) = - Obtain (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts)) - | do_step (Prove (qs, l, t, By_Metis (subproofs, facts))) = - Prove (qs, do_label l, t, By_Metis (map do_proof subproofs, facts)) + 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)) | do_step step = step and do_proof (Proof (fix, assms, steps)) = Proof (fix, do_assms assms, map do_step steps) @@ -599,18 +599,12 @@ |> apfst Assume |> apsnd fst fun do_steps _ _ _ [] = [] - | do_steps subst depth next (Obtain (qs, xs, l, t, by) :: steps) = + | do_steps subst depth next (Prove (qs, xs, l, t, by) :: steps) = let val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix val by = by |> do_byline subst depth - in Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps end - | do_steps subst depth next (Prove (qs, l, t, by) :: steps) = - let - val (l, subst, next) = - (l, subst, next) |> fresh_label depth have_prefix - val by = by |> do_byline subst depth - in Prove (qs, l, t, by) :: do_steps subst depth next steps end + in Prove (qs, xs, l, t, 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)) = @@ -628,16 +622,12 @@ | do_qs_lfs (SOME l0) lfs = if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs) - fun chain_step lbl (Obtain (qs, xs, l, t, + fun chain_step lbl (Prove (qs, xs, l, t, By_Metis (subproofs, (lfs, gfs)))) = - let val (qs', lfs) = do_qs_lfs lbl lfs in - Obtain (qs' @ qs, xs, l, t, - By_Metis (chain_proofs subproofs, (lfs, gfs))) - end - | chain_step lbl (Prove (qs, l, t, By_Metis (subproofs, (lfs, gfs)))) = - let val (qs', lfs) = do_qs_lfs lbl lfs in - Prove (qs' @ qs, l, t, By_Metis (chain_proofs subproofs, (lfs, gfs))) - end + let val (qs', lfs) = do_qs_lfs lbl lfs in + Prove (qs' @ qs, xs, l, t, + By_Metis (chain_proofs subproofs, (lfs, gfs))) + end | chain_step _ step = step and chain_steps _ [] = [] | chain_steps (prev as SOME _) (i :: is) = @@ -754,8 +744,8 @@ fun do_steps outer predecessor accum [] = accum |> (if tainted = [] then - cons (Prove (if outer then [Show] else [], no_label, - concl_t, + cons (Prove (if outer then [Show] else [], + Fix [], no_label, concl_t, By_Metis ([], ([the predecessor], [])))) else I) @@ -768,7 +758,7 @@ By_Metis ([], (fold (add_fact_of_dependencies fact_names) gamma no_facts)) - fun prove by = Prove (maybe_show outer c [], l, t, by) + fun prove by = Prove (maybe_show outer c [], Fix [], l, t, by) fun do_rest l step = do_steps outer (SOME l) (step :: accum) infs in @@ -790,7 +780,7 @@ | _ => do_rest l (prove by) else if is_clause_skolemize_rule c then - do_rest l (Obtain ([], Fix (skolems_of t), l, t, by)) + do_rest l (Prove ([], Fix (skolems_of t), l, t, by)) else do_rest l (prove by) end @@ -803,7 +793,7 @@ val l = label_of_clause c val t = prop_of_clause c val step = - Prove (maybe_show outer c [], l, t, + Prove (maybe_show outer c [], Fix [], l, t, By_Metis (map do_case cases, (the_list predecessor, []))) in do_steps outer (SOME l) (step :: accum) infs