--- a/src/Doc/Sledgehammer/document/root.tex Thu Feb 14 22:49:22 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Feb 14 22:49:22 2013 +0100
@@ -369,7 +369,7 @@
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
that Isar proofs should be generated, instead of one-liner \textit{metis} or
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
-\textit{isar\_shrink} (\S\ref{output-format}).
+\textit{isar\_compress} (\S\ref{output-format}).
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
@@ -508,7 +508,7 @@
is highly experimental. Work on a new implementation has begun. There is a large body of
research into transforming resolution proofs into natural deduction proofs (such
as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
-set the \textit{isar\_shrink} option (\S\ref{output-format}) to a larger
+set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger
value or to try several provers and keep the nicest-looking proof.
\point{How can I tell whether a suggested proof is sound?}
@@ -1302,7 +1302,7 @@
fails; however, they are usually faster and sometimes more robust than
\textit{metis} proofs.
-\opdefault{isar\_shrink}{int}{\upshape 10}
+\opdefault{isar\_compress}{int}{\upshape 10}
Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
is enabled. A value of $n$ indicates that each Isar proof step should correspond
to a group of up to $n$ consecutive proof steps in the ATP proof.
--- a/src/HOL/Metis_Examples/Big_O.thy Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Thu Feb 14 22:49:22 2013 +0100
@@ -29,7 +29,7 @@
(*** Now various verions with an increasing shrink factor ***)
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
lemma
"(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -60,7 +60,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
qed
-sledgehammer_params [isar_proofs, isar_shrink = 2]
+sledgehammer_params [isar_proofs, isar_compress = 2]
lemma
"(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -83,7 +83,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
qed
-sledgehammer_params [isar_proofs, isar_shrink = 3]
+sledgehammer_params [isar_proofs, isar_compress = 3]
lemma
"(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -103,7 +103,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
qed
-sledgehammer_params [isar_proofs, isar_shrink = 4]
+sledgehammer_params [isar_proofs, isar_compress = 4]
lemma
"(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -123,7 +123,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
qed
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
by (auto simp add: bigo_def bigo_pos_const)
--- a/src/HOL/Metis_Examples/Sets.thy Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy Thu Feb 14 22:49:22 2013 +0100
@@ -21,7 +21,7 @@
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
by metis
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
(*multiple versions of this example*)
lemma (*equal_union: *)
@@ -70,7 +70,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
-sledgehammer_params [isar_proofs, isar_shrink = 2]
+sledgehammer_params [isar_proofs, isar_compress = 2]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -107,7 +107,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
-sledgehammer_params [isar_proofs, isar_shrink = 3]
+sledgehammer_params [isar_proofs, isar_compress = 3]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -124,7 +124,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
qed
-sledgehammer_params [isar_proofs, isar_shrink = 4]
+sledgehammer_params [isar_proofs, isar_compress = 4]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -140,7 +140,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
qed
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
--- a/src/HOL/Metis_Examples/Trans_Closure.thy Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy Thu Feb 14 22:49:22 2013 +0100
@@ -44,7 +44,7 @@
lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
\<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proofs, isar_shrink = 2] *)
+(* sledgehammer [isar_proofs, isar_compress = 2] *)
proof -
assume A1: "f c = Intg x"
assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
--- a/src/HOL/Sledgehammer.thy Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Sledgehammer.thy Thu Feb 14 22:49:22 2013 +0100
@@ -17,7 +17,7 @@
ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Feb 14 22:49:22 2013 +0100
@@ -0,0 +1,252 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_compress.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Compression of reconstructed isar proofs.
+*)
+
+signature SLEDGEHAMMER_COMPRESS =
+sig
+ type isar_step = Sledgehammer_Proof.isar_step
+ type preplay_time = Sledgehammer_Preplay.preplay_time
+ val compress_proof :
+ bool -> Proof.context -> string -> string -> bool -> Time.time option
+ -> real -> isar_step list -> isar_step list * (bool * preplay_time)
+end
+
+structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Proof
+open Sledgehammer_Preplay
+
+(* Parameters *)
+val merge_timeout_slack = 1.2
+
+(* Data structures, orders *)
+val label_ord = prod_ord int_ord fast_string_ord o pairself swap
+structure Label_Table = Table(
+ type key = label
+ val ord = label_ord)
+
+(* clean vector interface *)
+fun get i v = Vector.sub (v, i)
+fun replace x i v = Vector.update (v, i, x)
+fun update f i v = replace (get i v |> f) i v
+fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList
+fun v_fold_index f v s =
+ Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
+
+(* Queue interface to table *)
+fun pop tab key =
+ let val v = hd (Inttab.lookup_list tab key) in
+ (v, Inttab.remove_list (op =) (key, v) tab)
+ end
+fun pop_max tab = pop tab (the (Inttab.max_key tab))
+fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
+
+(* Main function for compresing proofs *)
+fun compress_proof debug ctxt type_enc lam_trans preplay preplay_timeout
+ isar_compress 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 exn =>
+ (if Exn.is_interrupt exn orelse debug then reraise exn
+ else metis_fail := true; some_preplay_time)
+ fun get_time lazy_time =
+ if !metis_fail andalso not (Lazy.is_finished lazy_time)
+ then some_preplay_time
+ else Lazy.force lazy_time
+ val metis_fail = fn () => !metis_fail
+ end
+
+ (* compress proof on top level - do not compress case splits *)
+ fun compress_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_compress |> 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 lookup_indices = map_filter (Label_Table.lookup label_index_table)
+
+ (* proof references *)
+ fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
+ | 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 _ => []))
+ |> 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)
+ | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, 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
+
+ (* cache metis preplay times in lazy time vector *)
+ val metis_time =
+ v_map_index
+ (if not preplay then K (zero_preplay_time) #> Lazy.value
+ else
+ apsnd the (* step *)
+ #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
+ #> try_metis debug type_enc lam_trans ctxt preplay_timeout
+ #> handle_metis_fail
+ #> Lazy.lazy)
+ proof_vect
+
+ fun sum_up_time lazy_time_vector =
+ Vector.foldl
+ (apfst get_time #> uncurry add_preplay_time)
+ zero_preplay_time lazy_time_vector
+
+ (* Merging *)
+ fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
+ let
+ val (step_constructor, lfs2, gfs2) =
+ (case step2 of
+ (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
+ (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
+ | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
+ (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
+ | _ => error "sledgehammer_compress: unmergeable Isar steps" )
+ val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
+ val gfs = union (op =) gfs1 gfs2
+ in step_constructor (By_Metis (lfs, gfs)) end
+ | merge _ _ = error "sledgehammer_compress: unmergeable Isar steps"
+
+ fun try_merge metis_time (s1, i) (s2, j) =
+ if not preplay then (merge s1 s2 |> SOME, metis_time)
+ else
+ (case get i metis_time |> Lazy.force of
+ (true, _) => (NONE, metis_time)
+ | (_, t1) =>
+ (case get j metis_time |> Lazy.force of
+ (true, _) => (NONE, metis_time)
+ | (_, t2) =>
+ let
+ val s12 = merge s1 s2
+ val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
+ in
+ case try_metis_quietly debug type_enc lam_trans ctxt timeout
+ (NONE, s12) () of
+ (true, _) => (NONE, metis_time)
+ | exact_time =>
+ (SOME s12, metis_time
+ |> replace (zero_preplay_time |> Lazy.value) i
+ |> replace (Lazy.value exact_time) 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 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
+
+ (* compress subproofs (case_splits and subblocks) and top-levl *)
+ val ((proof, top_level_time), lower_level_time) =
+ proof |> do_subproof rich_ctxt
+ |>> compress_top_level on_top_level rich_ctxt
+ in
+ (proof, add_preplay_time lower_level_time top_level_time)
+ end
+
+ and do_subproof ctxt proof =
+ let
+ fun compress_each_and_collect_time compress candidates =
+ let fun f_m cand time = compress cand ||> add_preplay_time time
+ in fold_map f_m candidates zero_preplay_time end
+ val compress_subproof =
+ compress_each_and_collect_time (do_proof false ctxt)
+ fun compress (Prove (qs, l, t, Case_Split (cases, facts))) =
+ let val (cases, time) = compress_subproof cases
+ in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
+ | compress (Prove (qs, l, t, Subblock proof)) =
+ let val ([proof], time) = compress_subproof [proof]
+ in (Prove (qs, l, t, Subblock proof), time) end
+ | compress step = (step, zero_preplay_time)
+ in
+ compress_each_and_collect_time compress proof
+ end
+ in
+ do_proof true ctxt proof
+ |> apsnd (pair (metis_fail ()))
+ end
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 14 22:49:22 2013 +0100
@@ -95,7 +95,7 @@
("max_mono_iters", "smart"),
("max_new_mono_instances", "smart"),
("isar_proofs", "false"),
- ("isar_shrink", "10"),
+ ("isar_compress", "10"),
("slice", "true"),
("minimize", "smart"),
("preplay_timeout", "3")]
@@ -119,7 +119,7 @@
val params_for_minimize =
["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
"uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
- "learn", "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
+ "learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"]
val property_dependent_params = ["provers", "timeout"]
@@ -314,7 +314,7 @@
val max_new_mono_instances =
lookup_option lookup_int "max_new_mono_instances"
val isar_proofs = lookup_bool "isar_proofs"
- val isar_shrink = Real.max (1.0, lookup_real "isar_shrink")
+ val isar_compress = Real.max (1.0, lookup_real "isar_compress")
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize =
if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -330,7 +330,7 @@
learn = learn, fact_filter = fact_filter, max_facts = max_facts,
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- isar_shrink = isar_shrink, slice = slice, minimize = minimize,
+ isar_compress = isar_compress, slice = slice, minimize = minimize,
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 14 22:49:22 2013 +0100
@@ -54,7 +54,7 @@
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
max_new_mono_instances, type_enc, strict, lam_trans,
- uncurried_aliases, isar_proofs, isar_shrink,
+ uncurried_aliases, isar_proofs, isar_compress,
preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state facts =
let
@@ -76,7 +76,7 @@
learn = false, fact_filter = NONE, max_facts = SOME (length facts),
fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances,
- isar_proofs = isar_proofs, isar_shrink = isar_shrink,
+ isar_proofs = isar_proofs, isar_compress = isar_compress,
slice = false, minimize = SOME false, timeout = timeout,
preplay_timeout = preplay_timeout, expect = ""}
val problem =
@@ -243,7 +243,7 @@
({debug, verbose, overlord, blocking, provers, type_enc, strict,
lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
- isar_shrink, slice, minimize, timeout, preplay_timeout, expect}
+ isar_compress, slice, minimize, timeout, preplay_timeout, expect}
: params) =
let
fun lookup_override name default_value =
@@ -261,7 +261,7 @@
learn = learn, fact_filter = fact_filter, max_facts = max_facts,
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- isar_shrink = isar_shrink, slice = slice, minimize = minimize,
+ isar_compress = isar_compress, slice = slice, minimize = minimize,
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Feb 14 22:49:22 2013 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 14 22:49:22 2013 +0100
@@ -35,7 +35,7 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool,
- isar_shrink : real,
+ isar_compress : real,
slice : bool,
minimize : bool option,
timeout : Time.time option,
@@ -322,7 +322,7 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool,
- isar_shrink : real,
+ isar_compress : real,
slice : bool,
minimize : bool option,
timeout : Time.time option,
@@ -635,7 +635,7 @@
best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
(params as {debug, verbose, overlord, type_enc, strict, lam_trans,
uncurried_aliases, fact_filter, max_facts, max_mono_iters,
- max_new_mono_instances, isar_proofs, isar_shrink,
+ max_new_mono_instances, isar_proofs, isar_compress,
slice, timeout, preplay_timeout, ...})
minimize_command
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
@@ -898,7 +898,7 @@
else
()
val isar_params =
- (debug, verbose, preplay_timeout, isar_shrink,
+ (debug, verbose, preplay_timeout, isar_compress,
pool, fact_names, sym_tab, atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 14 22:49:22 2013 +0100
@@ -54,7 +54,7 @@
open Sledgehammer_Util
open Sledgehammer_Proof
open Sledgehammer_Annotate
-open Sledgehammer_Shrink
+open Sledgehammer_Compress
structure String_Redirect = ATP_Proof_Redirect(
type key = step_name
@@ -639,7 +639,7 @@
* (string * stature) list vector * int Symtab.table * string proof * thm
fun isar_proof_text ctxt isar_proofs
- (debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab,
+ (debug, verbose, preplay_timeout, isar_compress, pool, fact_names, sym_tab,
atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
@@ -757,12 +757,12 @@
|> redirect_graph axioms tainted bot
|> map (isar_step_of_direct_inf true)
|> append assms
- |> (if not preplay andalso isar_shrink <= 1.0 then
+ |> (if not preplay andalso isar_compress <= 1.0 then
rpair (false, (true, seconds 0.0))
else
- shrink_proof debug ctxt type_enc lam_trans preplay
+ compress_proof debug ctxt type_enc lam_trans preplay
preplay_timeout
- (if isar_proofs then isar_shrink else 1000.0))
+ (if isar_proofs then isar_compress else 1000.0))
(* |>> reorder_proof_to_minimize_jumps (* ? *) *)
|>> chain_direct_proof
|>> kill_useless_labels_in_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Feb 14 22:49:22 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,252 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
- Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
-
-Shrinking of reconstructed isar proofs.
-*)
-
-signature SLEDGEHAMMER_SHRINK =
-sig
- type isar_step = Sledgehammer_Proof.isar_step
- type preplay_time = Sledgehammer_Preplay.preplay_time
- val shrink_proof :
- bool -> Proof.context -> string -> string -> bool -> Time.time option
- -> real -> isar_step list -> isar_step list * (bool * preplay_time)
-end
-
-structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Proof
-open Sledgehammer_Preplay
-
-(* Parameters *)
-val merge_timeout_slack = 1.2
-
-(* Data structures, orders *)
-val label_ord = prod_ord int_ord fast_string_ord o pairself swap
-structure Label_Table = Table(
- type key = label
- val ord = label_ord)
-
-(* clean vector interface *)
-fun get i v = Vector.sub (v, i)
-fun replace x i v = Vector.update (v, i, x)
-fun update f i v = replace (get i v |> f) i v
-fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList
-fun v_fold_index f v s =
- Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
-
-(* Queue interface to table *)
-fun pop tab key =
- let val v = hd (Inttab.lookup_list tab key) in
- (v, Inttab.remove_list (op =) (key, v) tab)
- end
-fun pop_max tab = pop tab (the (Inttab.max_key tab))
-fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
-
-(* 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 exn =>
- (if Exn.is_interrupt exn orelse debug then reraise exn
- else metis_fail := true; some_preplay_time)
- fun get_time lazy_time =
- if !metis_fail andalso not (Lazy.is_finished lazy_time)
- then some_preplay_time
- else Lazy.force lazy_time
- val metis_fail = fn () => !metis_fail
- end
-
- (* Shrink proof on top level - 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 (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 lookup_indices = map_filter (Label_Table.lookup label_index_table)
-
- (* proof references *)
- fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
- | 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 _ => []))
- |> 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)
- | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, 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
-
- (* cache metis preplay times in lazy time vector *)
- val metis_time =
- v_map_index
- (if not preplay then K (zero_preplay_time) #> Lazy.value
- else
- apsnd the (* step *)
- #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
- #> try_metis debug type_enc lam_trans ctxt preplay_timeout
- #> handle_metis_fail
- #> Lazy.lazy)
- proof_vect
-
- fun sum_up_time lazy_time_vector =
- Vector.foldl
- (apfst get_time #> uncurry add_preplay_time)
- zero_preplay_time lazy_time_vector
-
- (* Merging *)
- fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
- let
- val (step_constructor, lfs2, gfs2) =
- (case step2 of
- (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
- (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
- | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
- (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
- | _ => error "sledgehammer_shrink: unmergeable Isar steps" )
- val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
- val gfs = union (op =) gfs1 gfs2
- in step_constructor (By_Metis (lfs, gfs)) end
- | merge _ _ = error "sledgehammer_shrink: unmergeable Isar steps"
-
- fun try_merge metis_time (s1, i) (s2, j) =
- if not preplay then (merge s1 s2 |> SOME, metis_time)
- else
- (case get i metis_time |> Lazy.force of
- (true, _) => (NONE, metis_time)
- | (_, t1) =>
- (case get j metis_time |> Lazy.force of
- (true, _) => (NONE, metis_time)
- | (_, t2) =>
- let
- val s12 = merge s1 s2
- val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
- in
- case try_metis_quietly debug type_enc lam_trans ctxt timeout
- (NONE, s12) () of
- (true, _) => (NONE, metis_time)
- | exact_time =>
- (SOME s12, metis_time
- |> replace (zero_preplay_time |> Lazy.value) i
- |> replace (Lazy.value exact_time) 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 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 subproofs (case_splits and subblocks) and top-levl *)
- val ((proof, top_level_time), lower_level_time) =
- 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_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_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_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
- end
- in
- do_proof true ctxt proof
- |> apsnd (pair (metis_fail ()))
- end
-
-end