--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Feb 14 21:31:25 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Feb 14 22:49:22 2013 +0100
@@ -92,7 +92,9 @@
:: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
| _ => error "preplay error: malformed case split")
#> make_thm)
- cases)
+ cases
+ (* TODO: implement *)
+ | Subblock _ => [])
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
|> obtain ? Config.put Metis_Tactic.new_skolem true
val goal =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Feb 14 21:31:25 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Feb 14 22:49:22 2013 +0100
@@ -22,7 +22,8 @@
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
- Case_Split of isar_step list list * facts
+ Case_Split of isar_step list list * facts |
+ Subblock of isar_step list
val string_for_label : label -> string
val metis_steps_top_level : isar_step list -> int
@@ -45,7 +46,8 @@
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
- Case_Split of isar_step list list * facts
+ Case_Split of isar_step list list * facts |
+ Subblock of isar_step list
fun string_for_label (s, num) = s ^ string_of_int num
@@ -57,6 +59,8 @@
| Prove (_, _, _, By_Metis _) => Integer.add 1
| Prove (_, _, _, Case_Split (cases, _)) =>
Integer.add (fold (Integer.add o metis_steps_total) cases 1)
+ | Prove (_, _, _, Subblock subproof) =>
+ Integer.add (metis_steps_total subproof)
| _ => I) proof 0
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 14 21:31:25 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 14 22:49:22 2013 +0100
@@ -499,14 +499,14 @@
(E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
Vampire). *)
do_metis ind "using [[metis_new_skolem]] " 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_metis ind "" facts ^ "\n"
+ | do_step ind (Prove (qs, l, t, By_Metis facts)) =
+ do_prove ind qs l t facts
| 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_metis ind "" facts ^ "\n"
+ do_prove ind qs l t facts
+ | do_step ind (Prove (qs, l, t, Subblock proof)) =
+ do_block ind proof ^ do_prove ind qs l t ([], [])
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 ^
@@ -515,6 +515,9 @@
suffix ^ "\n"
end
and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
+ and do_prove ind qs l t facts =
+ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^
+ do_metis ind "" facts ^ "\n"
(* One-step proofs are pointless; better use the Metis one-liner
directly. *)
and do_proof [Prove (_, _, _, By_Metis _)] = ""
@@ -529,7 +532,8 @@
(case by of
By_Metis (ls, _) => ls
| Case_Split (proofs, (ls, _)) =>
- fold (union (op =) o used_labels_of) proofs ls)
+ fold (union (op =) o used_labels_of) proofs ls
+ | Subblock proof => used_labels_of proof)
| used_labels_of_step _ = []
and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
@@ -543,10 +547,12 @@
Prove (qs, do_label l, t,
case by of
Case_Split (proofs, facts) =>
- Case_Split (map (map do_step) proofs, facts)
+ Case_Split (map do_proof proofs, facts)
+ | Subblock proof => Subblock (do_proof proof)
| _ => by)
| do_step step = step
- in map do_step proof end
+ and do_proof proof = map do_step proof
+ in do_proof proof end
fun prefix_for_depth n = replicate_string (n + 1)
@@ -561,12 +567,13 @@
end
fun do_facts subst =
apfst (maps (the_list o AList.lookup (op =) subst))
- fun do_byline subst depth by =
+ fun do_byline subst depth nexts 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)
+ | Subblock proof => Subblock (do_proof subst depth nexts proof)
and do_proof _ _ _ [] = []
| do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
if l = no_label then
@@ -576,26 +583,26 @@
Assume (l', t) ::
do_proof ((l, l') :: subst) depth (next_assum + 1, next_have) proof
end
- | do_proof subst depth (next_assum, next_have)
+ | do_proof subst depth (nexts as (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
+ val by = by |> do_byline subst depth nexts
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)
+ | do_proof subst depth (nexts as (next_assum, next_have))
(Prove (qs, l, t, by) :: proof) =
let
val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth
- val by = by |> do_byline subst depth
+ val by = by |> do_byline subst depth nexts
in
Prove (qs, l, t, by) ::
do_proof subst depth (next_assum, next_have) proof
end
- | do_proof subst depth nextp (step :: proof) =
- step :: do_proof subst depth nextp proof
+ | do_proof subst depth nexts (step :: proof) =
+ step :: do_proof subst depth nexts proof
in do_proof [] 0 (1, 1) end
val chain_direct_proof =
@@ -617,7 +624,9 @@
else
step
| chain_step _ (Prove (qs, l, t, Case_Split (proofs, facts))) =
- Prove (qs, l, t, Case_Split ((map (chain_proof NONE) proofs), facts))
+ Prove (qs, l, t, Case_Split (map (chain_proof NONE) proofs, facts))
+ | chain_step _ (Prove (qs, l, t, Subblock proof)) =
+ Prove (qs, l, t, Subblock (chain_proof NONE proof))
| chain_step _ step = step
and chain_proof _ [] = []
| chain_proof (prev as SOME _) (i :: is) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Feb 14 21:31:25 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Feb 14 22:49:22 2013 +0100
@@ -91,6 +91,7 @@
| refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs
| refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
lookup_indices lfs @ maps (maps refs) cases
+ | refs (Prove (_, _, _, Subblock proof)) = maps refs proof
| refs _ = []
val refed_by_vect =
Vector.tabulate (n, (fn _ => []))
@@ -218,24 +219,27 @@
| enrich_with_step _ = I
val rich_ctxt = fold enrich_with_step proof ctxt
- (* Shrink case_splits and top-levl *)
+ (* Shrink subproofs (case_splits and subblocks) and top-levl *)
val ((proof, top_level_time), lower_level_time) =
- proof |> do_case_splits rich_ctxt
+ proof |> do_subproof rich_ctxt
|>> shrink_top_level on_top_level rich_ctxt
in
(proof, add_preplay_time lower_level_time top_level_time)
end
- and do_case_splits ctxt proof =
+ and do_subproof ctxt proof =
let
fun shrink_each_and_collect_time shrink candidates =
let fun f_m cand time = shrink cand ||> add_preplay_time time
in fold_map f_m candidates zero_preplay_time end
- val shrink_case_split =
+ val shrink_subproof =
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
+ let val (cases, time) = shrink_subproof cases
in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
+ | shrink (Prove (qs, l, t, Subblock proof)) =
+ let val ([proof], time) = shrink_subproof [proof]
+ in (Prove (qs, l, t, Subblock proof), time) end
| shrink step = (step, zero_preplay_time)
in
shrink_each_and_collect_time shrink proof