--- 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
--- 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 =
--- 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 =
--- 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