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