--- a/src/HOL/IMP/Hoare_Examples.thy Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy Wed Jul 10 12:35:18 2013 +0200
@@ -2,37 +2,33 @@
theory Hoare_Examples imports Hoare begin
-text{* The following lemmas improve proof automation and should be included
-(globally?) when dealing with negative numerals. *}
+text{* Improves proof automation for negative numerals: *}
lemma add_neg1R[simp]:
- "x + -1 = x - (1 :: 'a :: neg_numeral)"
-unfolding minus_one[symmetric] by (rule diff_minus[symmetric])
-lemma add_neg1L[simp]:
- "-1 + x = x - (1 :: 'a :: {neg_numeral, ab_group_add})"
-unfolding minus_one[symmetric] by simp
+ "x + -1 = x - (1 :: int)"
+by arith
-lemma add_neg_numeralL[simp]:
+lemma add_neg_numeralR[simp]:
"x + neg_numeral n = (x::'a::neg_numeral) - numeral(n)"
by (simp only: diff_minus_eq_add[symmetric] minus_neg_numeral)
-lemma add_neg_numeralR[simp]:
- "neg_numeral n + x = (x::'a::{neg_numeral,ab_group_add}) - numeral(n)"
-by simp
text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
fun sum :: "int \<Rightarrow> int" where
-"sum i = (if i <= 0 then 0 else sum (i - 1) + i)"
+"sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)"
-lemma [simp]: "0 < i \<Longrightarrow> sum i = sum (i - 1) + i" "i <= 0 \<Longrightarrow> sum i = 0"
+lemma sum_simps[simp]:
+ "0 < i \<Longrightarrow> sum i = sum (i - 1) + i"
+ "i \<le> 0 \<Longrightarrow> sum i = 0"
by(simp_all)
declare sum.simps[simp del]
abbreviation "wsum ==
WHILE Less (N 0) (V ''x'')
- DO (''y'' ::= Plus (V ''y'') (V ''x'');; ''x'' ::= Plus (V ''x'') (N -1))"
+ DO (''y'' ::= Plus (V ''y'') (V ''x'');;
+ ''x'' ::= Plus (V ''x'') (N -1))"
subsubsection{* Proof by Operational Semantics *}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 10 12:35:18 2013 +0200
@@ -462,7 +462,7 @@
fun failed failure =
({outcome = SOME failure, used_facts = [], used_from = [],
run_time = Time.zeroTime,
- preplay = Lazy.value (Sledgehammer_Reconstruct.Failed_to_Play
+ preplay = Lazy.value (Sledgehammer_Reconstructor.Failed_to_Play
Sledgehammer_Provers.plain_metis),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
--- a/src/HOL/Sledgehammer.thy Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Sledgehammer.thy Wed Jul 10 12:35:18 2013 +0200
@@ -14,9 +14,11 @@
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML"
ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_print.ML"
ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Wed Jul 10 12:35:18 2013 +0200
@@ -36,6 +36,7 @@
val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
val ((v', s''), _) = post_traverse_term_type' f env v s'
in f (u' $ v') T s'' end
+ handle Bind => raise Fail "Sledgehammer_Annotate: post_traverse_term_type'"
fun post_traverse_term_type f s t =
post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Jul 10 12:35:18 2013 +0200
@@ -2,18 +2,22 @@
Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
-Compression of reconstructed isar proofs.
+Compression of isar proofs.
+
+PRE CONDITION: the proof must be labeled canocially, see
+Slegehammer_Proof.relabel_proof_canonically
*)
signature SLEDGEHAMMER_COMPRESS =
sig
type isar_proof = Sledgehammer_Proof.isar_proof
- type preplay_time = Sledgehammer_Preplay.preplay_time
- val compress_and_preplay_proof :
- bool -> Proof.context -> string -> string -> bool -> Time.time option
- -> bool -> real -> isar_proof -> isar_proof * (bool * preplay_time)
+ type preplay_interface = Sledgehammer_Preplay.preplay_interface
+
+ val compress_proof :
+ real -> int -> real -> preplay_interface -> isar_proof -> isar_proof
end
+
structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
struct
@@ -21,231 +25,345 @@
open Sledgehammer_Proof
open Sledgehammer_Preplay
-(* Parameters *)
-val merge_timeout_slack = 1.2
+
+(*** util ***)
-(* 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_fold_index f v s =
- Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
+(* traverses steps in post-order and collects the steps with the given labels *)
+fun collect_successors steps lbls =
+ let
+ fun do_steps _ ([], accu) = ([], accu)
+ | do_steps [] (lbls, accu) = (lbls, accu)
+ | do_steps (step::steps) (lbls, accu) =
+ do_steps steps (do_step step (lbls, accu))
-(* 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) handle List.Empty => raise Fail "sledgehammer_compress: pop"
-fun pop_max tab = pop tab (fst (the (Inttab.max tab)))
- handle Option.Option => raise Fail "sledgehammer_compress: pop_max"
-fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
+ and do_step (Let _) x = x
+ | do_step (step as Prove (_, _, l, _, subproofs, _)) x =
+ (case do_subproofs subproofs x of
+ ([], accu) => ([], accu)
+ | (lbls as l'::lbls', accu) =>
+ if l=l'
+ then (lbls', step::accu)
+ else (lbls, accu))
-(* Main function for compresing proofs *)
-fun compress_and_preplay_proof debug ctxt type_enc lam_trans preplay
- preplay_timeout preplay_trace 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
- val metis_fail = Unsynchronized.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
+ and do_subproofs [] x = x
+ | do_subproofs (proof::subproofs) x =
+ (case do_steps (steps_of_proof proof) x of
+ ([], accu) => ([], accu)
+ | x => do_subproofs subproofs x)
+ in
+ case do_steps steps (lbls, []) of
+ ([], succs) => rev succs
+ | _ => raise Fail "Sledgehammer_Compress: collect_successors"
+ end
- (* compress top level steps - do not compress subproofs *)
- fun compress_top_level on_top_level ctxt n steps =
- let
- (* proof step vector *)
- val step_vect = steps |> map SOME |> Vector.fromList
- val n_metis = add_metis_steps_top_level steps 0
- 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
- val label_index_table = fold_index update_table steps Label_Table.empty
- val lookup_indices = map_filter (Label_Table.lookup label_index_table)
+(* traverses steps in reverse post-order and inserts the given updates *)
+fun update_steps steps updates =
+ let
+ fun do_steps [] updates = ([], updates)
+ | do_steps steps [] = (steps, [])
+ | do_steps (step::steps) updates =
+ do_step step (do_steps steps updates)
- (* proof step references *)
- fun refs step =
- 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
- |> Vector.map rev (* after rev, indices are sorted in ascending order *)
+ and do_step step (steps, []) = (step::steps, [])
+ | do_step (step as Let _) (steps, updates) = (step::steps, updates)
+ | do_step (Prove (qs, xs, l, t, subproofs, by))
+ (steps, updates as
+ Prove(qs', xs', l', t', subproofs', by') :: updates') =
+ let
+ val (subproofs, updates) =
+ if l=l'
+ then do_subproofs subproofs' updates'
+ else do_subproofs subproofs updates
+ in
+ if l=l'
+ then (Prove (qs', xs', l', t', subproofs, by') :: steps,
+ updates)
+ else (Prove (qs, xs, l, t, subproofs, by) :: steps,
+ updates)
+ end
+ | do_step _ _ =
+ raise Fail "Sledgehammer_Compress: update_steps (invalid update)"
- (* candidates for elimination, use table as priority queue (greedy
- 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)
- | _ => I)
- handle Option.Option => raise Fail "sledgehammer_compress: add_if_cand")
- | add_if_cand _ _ = I
- val cand_tab =
- v_fold_index (add_if_cand step_vect) refed_by_vect []
- |> Inttab.make_list
-
- (* cache metis preplay times in lazy time vector *)
- val metis_time =
- Vector.map
- (if not preplay then K (zero_preplay_time) #> Lazy.value
- else
- the
- #> try_metis debug preplay_trace type_enc lam_trans ctxt
- preplay_timeout
- #> handle_metis_fail
- #> Lazy.lazy)
- step_vect
- handle Option.Option => raise Fail "sledgehammer_compress: metis_time"
+ and do_subproofs [] updates = ([], updates)
+ | do_subproofs steps [] = (steps, [])
+ | do_subproofs (proof::subproofs) updates =
+ do_proof proof (do_subproofs subproofs updates)
- 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 (_, 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, subproofs, By_Metis (lfs, gfs)) end
- | merge _ _ = raise Fail "sledgehammer_compress: unmergeable Isar steps"
+ and do_proof proof (proofs, []) = (proof :: proofs, [])
+ | do_proof (Proof (fix, assms, steps)) (proofs, updates) =
+ let val (steps, updates) = do_steps steps updates in
+ (Proof (fix, assms, steps) :: proofs, updates)
+ end
+ in
+ case do_steps steps (rev updates) of
+ (steps, []) => steps
+ | _ => raise Fail "Sledgehammer_Compress: update_steps"
+ end
- 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 preplay_trace type_enc
- lam_trans ctxt timeout 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)
+(* tries merging the first step into the second step *)
+fun try_merge
+ (Prove (_, Fix [], lbl1, _, [], By_Metis (lfs1, gfs1)))
+ (Prove (qs2, fix, lbl2, t, subproofs, By_Metis (lfs2, gfs2))) =
+ let
+ val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
+ val gfs = union (op =) gfs1 gfs2
+ in
+ SOME (Prove (qs2, fix, lbl2, t, subproofs, By_Metis (lfs, gfs)))
+ end
+ | try_merge _ _ = NONE
- end))
+
+
+(*** main function ***)
+
+(* PRE CONDITION: the proof must be labeled canocially, see
+ Slegehammer_Proof.relabel_proof_canonically *)
+fun compress_proof isar_compress isar_compress_degree merge_timeout_slack
+ { get_time, set_time, preplay_quietly, preplay_fail, ... } proof =
+ if isar_compress <= 1.0 then
+ proof
+ else
+ let
- fun merge_steps metis_time step_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)
- orelse metis_fail()
- then
- (Vector.foldr
- (fn (NONE, steps) => steps | (SOME s, steps) => s :: steps)
- [] step_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 step_vect |> the
- val s2 = get j step_vect |> the
- in
- case try_merge metis_time (s1, i) (s2, j) of
- (NONE, metis_time) =>
- merge_steps metis_time step_vect refed_by cand_tab n' n_metis'
- | (s, metis_time) =>
- let
- val refs_s1 = refs s1
- val refed_by = refed_by |> fold
- (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j))
- refs_s1
- val shared_refs = Ord_List.inter int_ord refs_s1 (refs s2)
- val new_candidates =
- fold (add_if_cand step_vect)
- (map (fn i => (i, get i refed_by)) shared_refs) []
- val cand_tab = add_list cand_tab new_candidates
- val step_vect = step_vect |> replace NONE i |> replace s j
- in
- merge_steps metis_time step_vect refed_by cand_tab (n' - 1)
- (n_metis' - 1)
- end
- end
- handle Option.Option => raise Fail "sledgehammer_compress: merge_steps"
- | List.Empty => raise Fail "sledgehammer_compress: merge_steps"
- in
- merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis
- end
+ val (compress_further : unit -> bool,
+ decrement_step_count : unit -> unit) =
+ let
+ val number_of_steps = add_metis_steps (steps_of_proof proof) 0
+ val target_number_of_steps =
+ Real.fromInt number_of_steps / isar_compress
+ |> Real.round
+ |> curry Int.max 2 (* don't produce one-step isar proofs *)
+ val delta =
+ number_of_steps - target_number_of_steps |> Unsynchronized.ref
+ in
+ (fn () => not (preplay_fail ()) andalso !delta > 0,
+ fn () => delta := !delta - 1)
+ end
+
+
+ val (get_successors : label -> label list,
+ replace_successor: label -> label list -> label -> unit) =
+ let
- fun do_proof on_top_level ctxt (Proof (Fix fix, Assume assms, steps)) =
- 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_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 _ = I
- val enrich_with_steps = fold enrich_with_step
- val enrich_with_assms = fold (uncurry enrich_with_fact)
- val rich_ctxt =
- ctxt |> enrich_with_assms assms |> enrich_with_steps steps
+ fun add_refs (Let _) tab = tab
+ | add_refs (Prove (_, _, l as v, _, _, By_Metis (lfs, _))) tab =
+ fold (fn lf as key => Canonical_Lbl_Tab.cons_list (key, v)) lfs tab
+
+ val tab =
+ Canonical_Lbl_Tab.empty
+ |> fold_isar_steps add_refs (steps_of_proof proof)
+ (* rev should have the same effect as sort canonical_label_ord *)
+ |> Canonical_Lbl_Tab.map (K rev)
+ |> Unsynchronized.ref
- val n = List.length fix + List.length assms + List.length steps
+ fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l
+ fun set_successors l refs =
+ tab := Canonical_Lbl_Tab.update (l, refs) (!tab)
+ fun replace_successor old new dest =
+ set_successors dest
+ (get_successors dest |> Ord_List.remove canonical_label_ord old
+ |> Ord_List.union canonical_label_ord new)
- (* compress subproofs and top-levl steps *)
- val ((steps, top_level_time), lower_level_time) =
- steps |> do_subproofs rich_ctxt
- |>> compress_top_level on_top_level rich_ctxt n
in
- (Proof (Fix fix, Assume assms, steps),
- add_preplay_time lower_level_time top_level_time)
+ (get_successors, replace_successor)
end
- and do_subproofs ctxt subproofs =
+
+ (** elimination of trivial, one-step subproofs **)
+
+ fun elim_subproofs' time qs fix l t lfs gfs subs nontriv_subs =
+ if null subs orelse not (compress_further ()) then
+ (set_time l (false, time);
+ Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs),
+ By_Metis (lfs, gfs) ))
+ else
+ case subs of
+ ((sub as Proof(_, Assume assms, sub_steps)) :: subs) =>
+ (let
+
+ (* trivial subproofs have exactly one Prove step *)
+ val SOME (Prove (_, Fix [], l', _, [], By_Metis(lfs', gfs'))) =
+ (try the_single) sub_steps
+
+ (* only touch proofs that can be preplayed sucessfully *)
+ val (false, time') = get_time l'
+
+ (* merge steps *)
+ val subs'' = subs @ nontriv_subs
+ val lfs'' =
+ subtract (op =) (map fst assms) lfs'
+ |> union (op =) lfs
+ val gfs'' = union (op =) gfs' gfs
+ val by = By_Metis (lfs'', gfs'')
+ val step'' = Prove (qs, fix, l, t, subs'', by)
+
+ (* check if the modified step can be preplayed fast enough *)
+ val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
+ val (false, time'') = preplay_quietly timeout step''
+
+ in
+ set_time l' zero_preplay_time; (* l' successfully eliminated! *)
+ map (replace_successor l' [l]) lfs';
+ decrement_step_count ();
+ elim_subproofs' time'' qs fix l t lfs'' gfs'' subs nontriv_subs
+ end
+ handle Bind =>
+ elim_subproofs' time qs fix l t lfs gfs subs (sub::nontriv_subs))
+ | _ => raise Fail "Sledgehammer_Compress: elim_subproofs'"
+
+
+ fun elim_subproofs (step as Let _) = step
+ | elim_subproofs
+ (step as Prove (qs, fix, l, t, subproofs, By_Metis(lfs, gfs))) =
+ if subproofs = [] then step else
+ case get_time l of
+ (true, _) => step (* timeout *)
+ | (false, time) =>
+ elim_subproofs' time qs fix l t lfs gfs subproofs []
+
+
+
+ (** top_level compression: eliminate steps by merging them into their
+ successors **)
+
+ fun compress_top_level steps =
let
- fun compress_each_and_collect_time compress subproofs =
- let fun f_m proof time = compress proof ||> add_preplay_time time
- 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, subproofs, By_Metis facts)) =
- let val (subproofs, time) = compress_subproofs subproofs
- in (Prove (qs, fix, l, t, subproofs, By_Metis facts), time) end
- | compress atomic_step = (atomic_step, zero_preplay_time)
+
+ (* #successors, (size_of_term t, position) *)
+ fun cand_key (i, l, t_size) =
+ (get_successors l |> length, (t_size, i))
+
+ val compression_ord =
+ prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
+ #> rev_order
+
+ val cand_ord = pairself cand_key #> compression_ord
+
+ fun pop_next_cand candidates =
+ case max_list cand_ord candidates of
+ NONE => (NONE, [])
+ | cand as SOME (i, _, _) =>
+ (cand, filter_out (fn (j, _, _) => j=i) candidates)
+
+ val candidates =
+ let
+ fun add_cand (i, Let _) = I
+ | add_cand (i, Prove (_, _, l, t, _, _)) =
+ cons (i, l, size_of_term t)
+ in
+ (steps
+ |> split_last |> fst (* last step must NOT be eliminated *)
+ |> fold_index add_cand) []
+ end
+
+ fun try_eliminate (cand as (i, l, _)) succ_lbls steps =
+ let
+ (* only touch steps that can be preplayed successfully *)
+ val (false, time) = get_time l
+
+ val succ_times = map (get_time #> (fn (false, t) => t)) succ_lbls
+
+ val timeslice =
+ time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
+
+ val timeouts =
+ map (curry Time.+ timeslice #> time_mult merge_timeout_slack)
+ succ_times
+
+ val ((cand as Prove (_, _, l, _, _, By_Metis(lfs, _))) :: steps') =
+ drop i steps
+
+ (* FIXME: debugging *)
+ val _ = (if (label_of_step cand |> the) <> l then
+ raise Fail "Sledgehammer_Compress: try_eliminate"
+ else ())
+
+ val succs = collect_successors steps' succ_lbls
+ val succs' = map (try_merge cand #> the) succs
+
+ val preplay_times =
+ map (uncurry preplay_quietly) (timeouts ~~ succs')
+
+ (* ensure none of the modified successors timed out *)
+ val false = List.exists fst preplay_times
+
+ val (steps1, _::steps2) = chop i steps
+
+ (* replace successors with their modified versions *)
+ val steps2 = update_steps steps2 succs'
+
+ in
+ set_time l zero_preplay_time; (* candidate successfully eliminated *)
+ decrement_step_count ();
+ map (uncurry set_time) (succ_lbls ~~ preplay_times);
+ map (replace_successor l succ_lbls) lfs;
+ (* removing the step would mess up the indices
+ -> replace with dummy step instead *)
+ steps1 @ dummy_isar_step :: steps2
+ end
+ handle Bind => steps
+ | Match => steps
+ | Option.Option => steps
+
+ fun compression_loop candidates steps =
+ if not (compress_further ()) then
+ steps
+ else
+ case pop_next_cand candidates of
+ (NONE, _) => steps (* no more candidates for elimination *)
+ | (SOME (cand as (_, l, _)), candidates) =>
+ let
+ val successors = get_successors l
+ in
+ if length successors > isar_compress_degree
+ then steps
+ else compression_loop candidates
+ (try_eliminate cand successors steps)
+ end
+
+
in
- compress_each_and_collect_time compress subproofs
+ compression_loop candidates steps
+ |> filter_out (fn step => step = dummy_isar_step)
end
+
+
+
+ (** recusion over the proof tree **)
+ (*
+ Proofs are compressed bottom-up, beginning with the innermost
+ subproofs.
+ On the innermost proof level, the proof steps have no subproofs.
+ In the best case, these steps can be merged into just one step,
+ resulting in a trivial subproof. Going one level up, trivial subproofs
+ can be eliminated. In the best case, this once again leads to a proof
+ whose proof steps do not have subproofs. Applying this approach
+ recursively will result in a flat proof in the best cast.
+ *)
+
+ infix 1 ?>
+ fun x ?> f = if compress_further () then f x else x
+
+ fun do_proof (proof as (Proof (fix, assms, steps))) =
+ if compress_further ()
+ then Proof (fix, assms, do_steps steps)
+ else proof
+
+ and do_steps steps =
+ (* bottom-up: compress innermost proofs first *)
+ steps |> map (fn step => step ?> do_sub_levels)
+ ?> compress_top_level
+
+ and do_sub_levels (Let x) = Let x
+ | do_sub_levels (Prove (qs, xs, l, t, subproofs, by)) =
+ (* compress subproofs *)
+ Prove (qs, xs, l, t, map do_proof subproofs, by)
+ (* eliminate trivial subproofs *)
+ ?> elim_subproofs
+
in
- do_proof true ctxt proof
- |> apsnd (pair (metis_fail ()))
+ do_proof proof
end
+
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 10 12:35:18 2013 +0200
@@ -100,6 +100,8 @@
("max_new_mono_instances", "smart"),
("isar_proofs", "smart"),
("isar_compress", "10"),
+ ("isar_compress_degree", "2"), (* TODO: document; right value?? *)
+ ("merge_timeout_slack", "1.2"), (* TODO: document *)
("slice", "true"),
("minimize", "smart"),
("preplay_timeout", "3"),
@@ -127,7 +129,7 @@
["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
"uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
"learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"]
-(* TODO: add preplay_trace? *)
+(* TODO: add isar_compress_degree, merge_timeout_slack, preplay_trace? *)
val property_dependent_params = ["provers", "timeout"]
@@ -309,6 +311,8 @@
lookup_option lookup_int "max_new_mono_instances"
val isar_proofs = lookup_option lookup_bool "isar_proofs"
val isar_compress = Real.max (1.0, lookup_real "isar_compress")
+ val isar_compress_degree = Int.max (1, lookup_int "isar_compress_degree")
+ val merge_timeout_slack = Real.max (1.0, lookup_real "merge_timeout_slack")
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize =
if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -325,8 +329,9 @@
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_compress = isar_compress, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout,
+ isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
+ merge_timeout_slack = merge_timeout_slack, slice = slice,
+ minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
preplay_trace = preplay_trace, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 10 12:35:18 2013 +0200
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_MINIMIZE =
sig
type stature = ATP_Problem_Generate.stature
- type play = Sledgehammer_Reconstruct.play
+ type play = Sledgehammer_Reconstructor.play
type mode = Sledgehammer_Provers.mode
type params = Sledgehammer_Provers.params
type prover = Sledgehammer_Provers.prover
@@ -38,6 +38,7 @@
open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact
+open Sledgehammer_Reconstructor
open Sledgehammer_Reconstruct
open Sledgehammer_Provers
@@ -57,6 +58,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_compress,
+ isar_compress_degree, merge_timeout_slack,
preplay_timeout, preplay_trace, ...} : params)
silent (prover : prover) timeout i n state facts =
let
@@ -79,6 +81,8 @@
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_compress = isar_compress,
+ isar_compress_degree = isar_compress_degree,
+ merge_timeout_slack = merge_timeout_slack,
slice = false, minimize = SOME false, timeout = timeout,
preplay_timeout = preplay_timeout, preplay_trace = preplay_trace,
expect = ""}
@@ -251,8 +255,8 @@
({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_compress, slice, minimize, timeout, preplay_timeout,
- preplay_trace, expect} : params) =
+ isar_compress, isar_compress_degree, merge_timeout_slack, slice,
+ minimize, timeout, preplay_timeout, preplay_trace, expect} : params) =
let
fun lookup_override name default_value =
case AList.lookup (op =) override_params name of
@@ -269,8 +273,9 @@
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_compress = isar_compress, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout,
+ isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
+ merge_timeout_slack = merge_timeout_slack, slice = slice,
+ minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
preplay_trace = preplay_trace, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Jul 10 12:35:18 2013 +0200
@@ -7,16 +7,29 @@
signature SLEDGEHAMMER_PREPLAY =
sig
+ type isar_proof = Sledgehammer_Proof.isar_proof
type isar_step = Sledgehammer_Proof.isar_step
+ type label = Sledgehammer_Proof.label
+
eqtype preplay_time
val zero_preplay_time : preplay_time
val some_preplay_time : preplay_time
val add_preplay_time : preplay_time -> preplay_time -> preplay_time
val string_of_preplay_time : preplay_time -> string
- val try_metis : bool -> bool -> string -> string -> Proof.context ->
- Time.time -> isar_step -> unit -> preplay_time
- val try_metis_quietly : bool -> bool -> string -> string -> Proof.context ->
- Time.time -> isar_step -> unit -> preplay_time
+ val preplay : bool -> bool -> string -> string -> Proof.context ->
+ Time.time -> isar_step -> preplay_time
+
+ type preplay_interface =
+ { get_time : label -> preplay_time,
+ set_time : label -> preplay_time -> unit,
+ preplay_quietly : Time.time -> isar_step -> preplay_time,
+ preplay_fail : unit -> bool,
+ overall_preplay_stats : unit -> preplay_time * bool }
+
+ val proof_preplay_interface :
+ bool -> Proof.context -> string -> string -> bool -> Time.time option
+ -> bool -> isar_proof -> preplay_interface
+
end
structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
@@ -91,8 +104,10 @@
|> thm_of_term ctxt
end
-fun try_metis _ _ _ _ _ _ (Let _) = K zero_preplay_time
- | try_metis debug trace type_enc lam_trans ctxt timeout
+
+(* main function for preplaying isar_steps *)
+fun preplay _ _ _ _ _ _ (Let _) = zero_preplay_time
+ | preplay debug trace type_enc lam_trans ctxt timeout
(Prove (_, Fix xs, _, t, subproofs, By_Metis fact_names)) =
let
val (prop, obtain) =
@@ -126,20 +141,132 @@
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
fun run_tac () = goal tac
handle ERROR msg => error ("preplay error: " ^ msg)
+ val preplay_time = take_time timeout run_tac ()
in
- fn () =>
- let
- val preplay_time = take_time timeout run_tac ()
- (* tracing *)
- val _ = if trace then preplay_trace ctxt facts prop preplay_time else ()
- in
- preplay_time
- end
+ (* tracing *)
+ (if trace then preplay_trace ctxt facts prop preplay_time else () ;
+ preplay_time)
+ end
+
+
+
+(*** proof preplay interface ***)
+
+type preplay_interface =
+ { get_time : label -> preplay_time,
+ set_time : label -> preplay_time -> unit,
+ preplay_quietly : Time.time -> isar_step -> preplay_time,
+ preplay_fail : unit -> bool,
+ overall_preplay_stats : unit -> preplay_time * bool }
+
+
+(* enriches context with local proof facts *)
+fun enrich_context proof ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+
+ fun enrich_with_fact l t =
+ Proof_Context.put_thms false
+ (string_of_label l, SOME [Skip_Proof.make_thm thy t])
+
+ val enrich_with_assms = fold (uncurry enrich_with_fact)
+
+ fun enrich_with_proof (Proof (_, Assume assms, isar_steps)) =
+ enrich_with_assms assms #> fold enrich_with_step isar_steps
+
+ and enrich_with_step (Let _) = I
+ | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
+ enrich_with_fact l t #> fold enrich_with_proof subproofs
+ in
+ enrich_with_proof proof ctxt
end
-(* this version treats exceptions like timeouts *)
-fun try_metis_quietly debug trace type_enc lam_trans ctxt timeout =
- the_default (true, timeout) oo try
- o try_metis debug trace type_enc lam_trans ctxt timeout
+
+(* Given a proof, produces an imperative preplay interface with a shared state.
+ The preplay times are caluclated lazyly and cached to avoid repeated
+ calculation.
+
+ PRE CONDITION: the proof must be labeled canocially, see
+ Slegehammer_Proof.relabel_proof_canonically
+*)
+fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
+ preplay_timeout preplay_trace proof : preplay_interface =
+ if not do_preplay then
+ (* the dont_preplay option pretends that everything works just fine *)
+ { get_time = K zero_preplay_time,
+ set_time = K (K ()),
+ preplay_quietly = K (K zero_preplay_time),
+ preplay_fail = K false,
+ overall_preplay_stats = K (zero_preplay_time, false)}
+ else
+ let
+
+ (* 60 seconds seems like a good interpreation of "no timeout" *)
+ val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
+
+ (* add local proof facts to context *)
+ val ctxt = enrich_context proof ctxt
+
+ val fail = Unsynchronized.ref false
+ fun preplay_fail () = !fail
+
+ fun preplay' timeout step =
+ (* after preplay has failed once, exact preplay times are pointless *)
+ if preplay_fail () then some_preplay_time
+ else preplay debug preplay_trace type_enc lam_trans ctxt timeout step
+
+ (* preplay steps without registering preplay_fails, treating exceptions
+ like timeouts *)
+ fun preplay_quietly timeout step =
+ try (preplay' timeout) step
+ |> the_default (true, timeout)
+
+ val preplay_time_tab =
+ let
+ fun add_step_to_tab step tab =
+ case label_of_step step of
+ NONE => tab
+ | SOME l =>
+ Canonical_Lbl_Tab.update_new
+ (l, (fn () => preplay' preplay_timeout step) |> Lazy.lazy)
+ tab
+ handle (exn as Canonical_Lbl_Tab.DUP _) =>
+ raise Fail ("Sledgehammer_Preplay: preplay time table - "
+ ^ PolyML.makestring exn)
+ in
+ Canonical_Lbl_Tab.empty
+ |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
+ |> Unsynchronized.ref
+ end
+
+ fun register_preplay_fail lazy_time = Lazy.force lazy_time
+ handle exn =>
+ if Exn.is_interrupt exn orelse debug then reraise exn
+ else (fail := true; some_preplay_time)
+
+ fun get_time lbl =
+ register_preplay_fail
+ (Canonical_Lbl_Tab.lookup (!preplay_time_tab) lbl |> the)
+ handle
+ Option.Option =>
+ raise Fail "Sledgehammer_Preplay: preplay time table"
+
+ fun set_time lbl time =
+ preplay_time_tab :=
+ Canonical_Lbl_Tab.update (lbl, Lazy.value time) (!preplay_time_tab)
+
+ fun total_preplay_time () =
+ Canonical_Lbl_Tab.fold
+ (snd #> register_preplay_fail #> add_preplay_time)
+ (!preplay_time_tab) zero_preplay_time
+
+ fun overall_preplay_stats () = (total_preplay_time (), preplay_fail ())
+ in
+ { get_time = get_time,
+ set_time = set_time,
+ preplay_quietly = preplay_quietly,
+ preplay_fail = preplay_fail,
+ overall_preplay_stats = overall_preplay_stats}
+ end
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Jul 10 12:35:18 2013 +0200
@@ -0,0 +1,246 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Basic mapping from proof data structures to proof strings.
+*)
+
+signature SLEDGEHAMMER_PRINT =
+sig
+ type isar_proof = Sledgehammer_Proof.isar_proof
+ type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type one_line_params = Sledgehammer_Reconstructor.one_line_params
+
+ val string_of_reconstructor : reconstructor -> string
+
+ val one_line_proof_text : int -> one_line_params -> string
+
+ val string_of_proof :
+ Proof.context -> string -> string -> int -> int -> isar_proof -> string
+end;
+
+structure Sledgehammer_Print : SLEDGEHAMMER_PRINT =
+struct
+
+open ATP_Util
+open ATP_Proof
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Proof
+open Sledgehammer_Annotate
+
+
+(** reconstructors **)
+
+fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
+ metis_call type_enc lam_trans
+ | string_of_reconstructor SMT = smtN
+
+
+
+(** one-liner reconstructor proofs **)
+
+fun show_time NONE = ""
+ | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
+
+(* FIXME: Various bugs, esp. with "unfolding"
+fun unusing_chained_facts _ 0 = ""
+ | unusing_chained_facts used_chaineds num_chained =
+ if length used_chaineds = num_chained then ""
+ else if null used_chaineds then "(* using no facts *) "
+ else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
+*)
+
+fun apply_on_subgoal _ 1 = "by "
+ | apply_on_subgoal 1 _ = "apply "
+ | apply_on_subgoal i n =
+ "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
+
+fun using_labels [] = ""
+ | using_labels ls =
+ "using " ^ space_implode " " (map string_of_label ls) ^ " "
+
+fun command_call name [] =
+ name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
+ | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+
+fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
+ (* unusing_chained_facts used_chaineds num_chained ^ *)
+ using_labels ls ^ apply_on_subgoal i n ^
+ command_call (string_of_reconstructor reconstr) ss
+
+fun try_command_line banner time command =
+ banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
+
+fun minimize_line _ [] = ""
+ | minimize_line minimize_command ss =
+ case minimize_command ss of
+ "" => ""
+ | command =>
+ "\nTo minimize: " ^ Active.sendback_markup command ^ "."
+
+fun split_used_facts facts =
+ facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
+ |> pairself (sort_distinct (string_ord o pairself fst))
+
+fun one_line_proof_text num_chained
+ (preplay, banner, used_facts, minimize_command, subgoal,
+ subgoal_count) =
+ let
+ val (chained, extra) = split_used_facts used_facts
+ val (failed, reconstr, ext_time) =
+ case preplay of
+ Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
+ | Trust_Playable (reconstr, time) =>
+ (false, reconstr,
+ case time of
+ NONE => NONE
+ | SOME time =>
+ if time = Time.zeroTime then NONE else SOME (true, time))
+ | Failed_to_Play reconstr => (true, reconstr, NONE)
+ val try_line =
+ ([], map fst extra)
+ |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
+ num_chained
+ |> (if failed then
+ enclose "One-line proof reconstruction failed: "
+ ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
+ \solve this.)"
+ else
+ try_command_line banner ext_time)
+ in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
+
+
+
+
+(** detailed Isar proofs **)
+
+val indent_size = 2
+
+fun string_of_proof ctxt type_enc lam_trans i n proof =
+ let
+ val ctxt =
+ (* make sure type constraint are actually printed *)
+ ctxt |> Config.put show_markup false
+ (* make sure only type constraints inserted by sh_annotate are printed *)
+ |> Config.put Printer.show_type_emphasis false
+ |> Config.put show_types false
+ |> Config.put show_sorts false
+ |> Config.put show_consts false
+ val register_fixes = map Free #> fold Variable.auto_fixes
+ fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
+ fun of_indent ind = replicate_string (ind * indent_size) " "
+ fun of_moreover ind = of_indent ind ^ "moreover\n"
+ fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
+ fun of_obtain qs nr =
+ (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
+ "ultimately "
+ else if nr=1 orelse member (op =) qs Then then
+ "then "
+ else
+ "") ^ "obtain"
+ fun of_show_have qs = if member (op =) qs Show then "show" else "have"
+ fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
+ fun of_prove qs nr =
+ if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
+ "ultimately " ^ of_show_have qs
+ else if nr=1 orelse member (op =) qs Then then
+ of_thus_hence qs
+ else
+ of_show_have qs
+ fun add_term term (s, ctxt) =
+ (s ^ (term
+ |> singleton (Syntax.uncheck_terms ctxt)
+ |> annotate_types ctxt
+ |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
+ |> simplify_spaces
+ |> maybe_quote),
+ ctxt |> Variable.auto_fixes term)
+ val reconstr = Metis (type_enc, lam_trans)
+ fun of_metis ind options (ls, ss) =
+ "\n" ^ of_indent (ind + 1) ^ options ^
+ reconstructor_command reconstr 1 1 [] 0
+ (ls |> sort_distinct (prod_ord string_ord int_ord),
+ ss |> sort_distinct string_ord)
+ fun of_free (s, T) =
+ maybe_quote s ^ " :: " ^
+ maybe_quote (simplify_spaces (with_vanilla_print_mode
+ (Syntax.string_of_typ ctxt) T))
+ fun add_frees xs (s, ctxt) =
+ (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
+ fun add_fix _ [] = I
+ | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
+ #> add_frees xs
+ #> add_suffix "\n"
+ fun add_assm ind (l, t) =
+ add_suffix (of_indent ind ^ "assume " ^ of_label l)
+ #> add_term t
+ #> add_suffix "\n"
+ fun add_assms ind assms = fold (add_assm ind) assms
+ fun add_step_post ind l t facts options =
+ add_suffix (of_label l)
+ #> add_term t
+ #> add_suffix (of_metis ind options facts ^ "\n")
+ fun of_subproof ind ctxt proof =
+ let
+ val ind = ind + 1
+ val s = of_proof ind ctxt proof
+ val prefix = "{ "
+ val suffix = " }"
+ in
+ replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
+ String.extract (s, ind * indent_size,
+ SOME (size s - ind * indent_size - 1)) ^
+ suffix ^ "\n"
+ end
+ and of_subproofs _ _ _ [] = ""
+ | of_subproofs ind ctxt qs subproofs =
+ (if member (op =) qs Then then of_moreover ind else "") ^
+ space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
+ and add_step_pre ind qs subproofs (s, ctxt) =
+ (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
+ and add_step ind (Let (t1, t2)) =
+ add_suffix (of_indent ind ^ "let ")
+ #> add_term t1
+ #> add_suffix " = "
+ #> add_term t2
+ #> add_suffix "\n"
+ | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By_Metis 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)
+ |> add_fix ind xs
+ |> add_assms ind assms
+ |> add_steps ind steps
+ |> fst
+ in
+ (* One-step proofs are pointless; better use the Metis one-liner
+ directly. *)
+ case proof of
+ 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
+
+ end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jul 10 12:35:18 2013 +0200
@@ -28,6 +28,10 @@
val no_label : label
val no_facts : facts
+ (*val label_ord : label * label -> order*)
+
+ val dummy_isar_step : isar_step
+
val string_of_label : label -> string
val fix_of_proof : isar_proof -> fix
val assms_of_proof : isar_proof -> assms
@@ -43,6 +47,13 @@
val add_metis_steps_top_level : isar_step list -> int -> int
val add_metis_steps : isar_step list -> int -> int
+
+ (** canonical proof labels: 1, 2, 3, ... in post traversal order **)
+ val canonical_label_ord : (label * label) -> order
+ val relabel_proof_canonically : isar_proof -> isar_proof
+
+ structure Canonical_Lbl_Tab : TABLE
+
end
structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
@@ -68,6 +79,10 @@
val no_label = ("", ~1)
val no_facts = ([],[])
+(*val label_ord = pairself swap #> prod_ord int_ord fast_string_ord*)
+
+val dummy_isar_step = Let (Term.dummy, Term.dummy)
+
fun string_of_label (s, num) = s ^ string_of_int num
fun fix_of_proof (Proof (fix, _, _)) = fix
@@ -83,17 +98,64 @@
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
+fun fold_isar_steps f = fold (fold_isar_step f)
+and fold_isar_step f step s =
+ fold (steps_of_proof #> fold_isar_steps f)
+ (these (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))
val add_metis_steps =
fold_isar_steps
(byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I))
+
+
+(** canonical proof labels: 1, 2, 3, ... in post traversal order **)
+
+fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
+
+structure Canonical_Lbl_Tab = Table(
+ type key = label
+ val ord = canonical_label_ord)
+
+fun relabel_proof_canonically proof =
+ let
+ val lbl = pair ""
+
+ fun next_label l (next, subst) =
+ (lbl next, (next + 1, (l, lbl next) :: subst))
+
+ fun do_byline (By_Metis (lfs, gfs)) (_, subst) =
+ By_Metis (map (AList.lookup (op =) subst #> the) lfs, gfs)
+ handle Option.Option =>
+ raise Fail "Sledgehammer_Compress: relabel_proof_canonically"
+
+ fun do_assm (l, t) state =
+ let
+ val (l, state) = next_label l state
+ in ((l, t), state) end
+
+ fun do_proof (Proof (fix, Assume assms, steps)) state =
+ let
+ val (assms, state) = fold_map do_assm assms state
+ val (steps, state) = fold_map do_step steps state
+ in
+ (Proof (fix, Assume assms, steps), state)
+ end
+
+ and do_step (step as Let _) state = (step, state)
+ | do_step (Prove (qs, fix, l, t, subproofs, by)) state=
+ let
+ val by = do_byline by state
+ val (subproofs, state) = fold_map do_proof subproofs state
+ val (l, state) = next_label l state
+ in
+ (Prove (qs, fix, l, t, subproofs, by), state)
+ end
+ in
+ fst (do_proof proof (0, []))
+ end
+
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 10 12:35:18 2013 +0200
@@ -12,9 +12,9 @@
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
type fact = Sledgehammer_Fact.fact
- type reconstructor = Sledgehammer_Reconstruct.reconstructor
- type play = Sledgehammer_Reconstruct.play
- type minimize_command = Sledgehammer_Reconstruct.minimize_command
+ type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type play = Sledgehammer_Reconstructor.play
+ type minimize_command = Sledgehammer_Reconstructor.minimize_command
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
@@ -36,6 +36,8 @@
max_new_mono_instances : int option,
isar_proofs : bool option,
isar_compress : real,
+ isar_compress_degree : int,
+ merge_timeout_slack : real,
slice : bool,
minimize : bool option,
timeout : Time.time option,
@@ -150,6 +152,8 @@
open Metis_Tactic
open Sledgehammer_Util
open Sledgehammer_Fact
+open Sledgehammer_Reconstructor
+open Sledgehammer_Print
open Sledgehammer_Reconstruct
@@ -345,6 +349,8 @@
max_new_mono_instances : int option,
isar_proofs : bool option,
isar_compress : real,
+ isar_compress_degree : int,
+ merge_timeout_slack : real,
slice : bool,
minimize : bool option,
timeout : Time.time option,
@@ -677,6 +683,7 @@
(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_compress,
+ isar_compress_degree, merge_timeout_slack,
slice, timeout, preplay_timeout, preplay_trace, ...})
minimize_command
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
@@ -951,6 +958,7 @@
()
val isar_params =
(debug, verbose, preplay_timeout, preplay_trace, isar_compress,
+ isar_compress_degree, merge_timeout_slack,
pool, fact_names, lifted, sym_tab, atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jul 10 12:35:18 2013 +0200
@@ -9,26 +9,13 @@
sig
type 'a proof = 'a ATP_Proof.proof
type stature = ATP_Problem_Generate.stature
-
- datatype reconstructor =
- Metis of string * string |
- SMT
-
- datatype play =
- Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option |
- Failed_to_Play of reconstructor
+ type one_line_params = Sledgehammer_Print.one_line_params
- type minimize_command = string list -> string
- type one_line_params =
- play * string * (string * stature) list * minimize_command * int * int
type isar_params =
- bool * bool * Time.time option * bool * real * string Symtab.table
- * (string * stature) list vector * (string * term) list * int Symtab.table
- * string proof * thm
+ bool * bool * Time.time option * bool * real * int * real
+ * string Symtab.table * (string * stature) list vector
+ * (string * term) list * int Symtab.table * string proof * thm
- val smtN : string
- val string_of_reconstructor : reconstructor -> string
val lam_trans_of_atp_proof : string proof -> string -> string
val is_typed_helper_used_in_atp_proof : string proof -> bool
val used_facts_in_atp_proof :
@@ -37,7 +24,6 @@
val used_facts_in_unsound_atp_proof :
Proof.context -> (string * stature) list vector -> 'a proof ->
string list option
- val one_line_proof_text : int -> one_line_params -> string
val isar_proof_text :
Proof.context -> bool option -> isar_params -> one_line_params -> string
val proof_text :
@@ -54,8 +40,11 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
+open Sledgehammer_Reconstructor
open Sledgehammer_Proof
open Sledgehammer_Annotate
+open Sledgehammer_Print
+open Sledgehammer_Preplay
open Sledgehammer_Compress
structure String_Redirect = ATP_Proof_Redirect(
@@ -65,25 +54,6 @@
open String_Redirect
-
-(** reconstructors **)
-
-datatype reconstructor =
- Metis of string * string |
- SMT
-
-datatype play =
- Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option |
- Failed_to_Play of reconstructor
-
-val smtN = "smt"
-
-fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
- metis_call type_enc lam_trans
- | string_of_reconstructor SMT = smtN
-
-
(** fact extraction from ATP proofs **)
fun find_first_in_list_vector vec key =
@@ -189,83 +159,6 @@
end
-(** one-liner reconstructor proofs **)
-
-fun show_time NONE = ""
- | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
-
-(* FIXME: Various bugs, esp. with "unfolding"
-fun unusing_chained_facts _ 0 = ""
- | unusing_chained_facts used_chaineds num_chained =
- if length used_chaineds = num_chained then ""
- else if null used_chaineds then "(* using no facts *) "
- else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
-*)
-
-fun apply_on_subgoal _ 1 = "by "
- | apply_on_subgoal 1 _ = "apply "
- | apply_on_subgoal i n =
- "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
-
-fun using_labels [] = ""
- | using_labels ls =
- "using " ^ space_implode " " (map string_of_label ls) ^ " "
-
-fun command_call name [] =
- name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
- | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-
-fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
- (* unusing_chained_facts used_chaineds num_chained ^ *)
- using_labels ls ^ apply_on_subgoal i n ^
- command_call (string_of_reconstructor reconstr) ss
-
-fun try_command_line banner time command =
- banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
-
-fun minimize_line _ [] = ""
- | minimize_line minimize_command ss =
- case minimize_command ss of
- "" => ""
- | command =>
- "\nTo minimize: " ^ Active.sendback_markup command ^ "."
-
-fun split_used_facts facts =
- facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
- |> pairself (sort_distinct (string_ord o pairself fst))
-
-type minimize_command = string list -> string
-type one_line_params =
- play * string * (string * stature) list * minimize_command * int * int
-
-fun one_line_proof_text num_chained
- (preplay, banner, used_facts, minimize_command, subgoal,
- subgoal_count) =
- let
- val (chained, extra) = split_used_facts used_facts
- val (failed, reconstr, ext_time) =
- case preplay of
- Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
- | Trust_Playable (reconstr, time) =>
- (false, reconstr,
- case time of
- NONE => NONE
- | SOME time =>
- if time = Time.zeroTime then NONE else SOME (true, time))
- | Failed_to_Play reconstr => (true, reconstr, NONE)
- val try_line =
- ([], map fst extra)
- |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
- num_chained
- |> (if failed then
- enclose "One-line proof reconstruction failed: "
- ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
- \solve this.)"
- else
- try_command_line banner ext_time)
- in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
-
-
(** Isar proof construction and manipulation **)
val assume_prefix = "a"
@@ -429,131 +322,6 @@
else
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
-val indent_size = 2
-
-fun string_of_proof ctxt type_enc lam_trans i n proof =
- let
- val ctxt =
- (* make sure type constraint are actually printed *)
- ctxt |> Config.put show_markup false
- (* make sure only type constraints inserted by sh_annotate are printed *)
- |> Config.put Printer.show_type_emphasis false
- |> Config.put show_types false
- |> Config.put show_sorts false
- |> Config.put show_consts false
- val register_fixes = map Free #> fold Variable.auto_fixes
- fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
- fun of_indent ind = replicate_string (ind * indent_size) " "
- fun of_moreover ind = of_indent ind ^ "moreover\n"
- fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
- fun of_obtain qs nr =
- (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
- "ultimately "
- else if nr=1 orelse member (op =) qs Then then
- "then "
- else
- "") ^ "obtain"
- fun of_show_have qs = if member (op =) qs Show then "show" else "have"
- fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
- fun of_prove qs nr =
- if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
- "ultimately " ^ of_show_have qs
- else if nr=1 orelse member (op =) qs Then then
- of_thus_hence qs
- else
- of_show_have qs
- fun add_term term (s, ctxt) =
- (s ^ (term
- |> singleton (Syntax.uncheck_terms ctxt)
- |> annotate_types ctxt
- |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
- |> simplify_spaces
- |> maybe_quote),
- ctxt |> Variable.auto_fixes term)
- val reconstr = Metis (type_enc, lam_trans)
- fun of_metis ind options (ls, ss) =
- "\n" ^ of_indent (ind + 1) ^ options ^
- reconstructor_command reconstr 1 1 [] 0
- (ls |> sort_distinct (prod_ord string_ord int_ord),
- ss |> sort_distinct string_ord)
- fun of_free (s, T) =
- maybe_quote s ^ " :: " ^
- maybe_quote (simplify_spaces (with_vanilla_print_mode
- (Syntax.string_of_typ ctxt) T))
- fun add_frees xs (s, ctxt) =
- (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
- fun add_fix _ [] = I
- | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
- #> add_frees xs
- #> add_suffix "\n"
- fun add_assm ind (l, t) =
- add_suffix (of_indent ind ^ "assume " ^ of_label l)
- #> add_term t
- #> add_suffix "\n"
- fun add_assms ind assms = fold (add_assm ind) assms
- fun add_step_post ind l t facts options =
- add_suffix (of_label l)
- #> add_term t
- #> add_suffix (of_metis ind options facts ^ "\n")
- fun of_subproof ind ctxt proof =
- let
- val ind = ind + 1
- val s = of_proof ind ctxt proof
- val prefix = "{ "
- val suffix = " }"
- in
- replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
- String.extract (s, ind * indent_size,
- SOME (size s - ind * indent_size - 1)) ^
- suffix ^ "\n"
- end
- and of_subproofs _ _ _ [] = ""
- | of_subproofs ind ctxt qs subproofs =
- (if member (op =) qs Then then of_moreover ind else "") ^
- space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
- and add_step_pre ind qs subproofs (s, ctxt) =
- (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
- and add_step ind (Let (t1, t2)) =
- add_suffix (of_indent ind ^ "let ")
- #> add_term t1
- #> add_suffix " = "
- #> add_term t2
- #> add_suffix "\n"
- | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By_Metis 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)
- |> add_fix ind xs
- |> add_assms ind assms
- |> add_steps ind steps
- |> fst
- in
- (* One-step proofs are pointless; better use the Metis one-liner
- directly. *)
- case proof of
- 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
val add_labels_of_proof =
steps_of_proof #> fold_isar_steps
@@ -638,13 +406,14 @@
in chain_proof end
type isar_params =
- bool * bool * Time.time option * bool * real * string Symtab.table
- * (string * stature) list vector * (string * term) list * int Symtab.table
- * string proof * thm
+ bool * bool * Time.time option * bool * real * int * real
+ * string Symtab.table * (string * stature) list vector
+ * (string * term) list * int Symtab.table * string proof * thm
fun isar_proof_text ctxt isar_proofs
- (debug, verbose, preplay_timeout, preplay_trace, isar_compress, pool,
- fact_names, lifted, sym_tab, atp_proof, goal)
+ (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
+ isar_compress_degree, merge_timeout_slack, pool, fact_names, lifted,
+ sym_tab, atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -659,7 +428,7 @@
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
else partial_typesN
val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans
- val preplay = preplay_timeout <> SOME Time.zeroTime
+ val do_preplay = preplay_timeout <> SOME Time.zeroTime
fun isar_proof_of () =
let
@@ -806,20 +575,24 @@
chain_direct_proof
#> kill_useless_labels_in_proof
#> relabel_proof
- val (isar_proof, (preplay_fail, preplay_time)) =
+ val (preplay_interface as { overall_preplay_stats, ... }, isar_proof) =
refute_graph
|> redirect_graph axioms tainted bot
|> isar_proof_of_direct_proof
- |> (if not preplay andalso isar_compress <= 1.0 then
- rpair (false, (true, seconds 0.0))
- else
- compress_and_preplay_proof debug ctxt type_enc lam_trans preplay
- preplay_timeout preplay_trace
- (if isar_proofs = SOME true then isar_compress else 1000.0))
- |>> clean_up_labels_in_proof
+ |> relabel_proof_canonically
+ |> `(proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
+ preplay_timeout preplay_trace)
+ val isar_proof =
+ isar_proof
+ |> compress_proof
+ (if isar_proofs = SOME true then isar_compress else 1000.0)
+ (if isar_proofs = SOME true then isar_compress_degree else 100)
+ merge_timeout_slack preplay_interface
+ |> clean_up_labels_in_proof
val isar_text =
string_of_proof ctxt type_enc lam_trans subgoal subgoal_count
isar_proof
+ val (preplay_time, preplay_fail) = overall_preplay_stats ()
in
case isar_text of
"" =>
@@ -836,9 +609,9 @@
in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
else
[]) @
- (if preplay then
+ (if do_preplay then
[(if preplay_fail then "may fail, " else "") ^
- Sledgehammer_Preplay.string_of_preplay_time preplay_time]
+ string_of_preplay_time preplay_time]
else
[])
in
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Wed Jul 10 12:35:18 2013 +0200
@@ -0,0 +1,52 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Reconstructors.
+*)
+
+signature SLEDGEHAMMER_RECONSTRUCTOR =
+sig
+
+ type stature = ATP_Problem_Generate.stature
+
+ datatype reconstructor =
+ Metis of string * string |
+ SMT
+
+ datatype play =
+ Played of reconstructor * Time.time |
+ Trust_Playable of reconstructor * Time.time option |
+ Failed_to_Play of reconstructor
+
+ type minimize_command = string list -> string
+
+ type one_line_params =
+ play * string * (string * stature) list * minimize_command * int * int
+
+ val smtN : string
+
+end
+
+structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
+struct
+
+open ATP_Problem_Generate
+
+datatype reconstructor =
+ Metis of string * string |
+ SMT
+
+datatype play =
+ Played of reconstructor * Time.time |
+ Trust_Playable of reconstructor * Time.time option |
+ Failed_to_Play of reconstructor
+
+type minimize_command = string list -> string
+
+type one_line_params =
+ play * string * (string * stature) list * minimize_command * int * int
+
+val smtN = "smt"
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 10 12:35:18 2013 +0200
@@ -10,7 +10,7 @@
sig
type fact = Sledgehammer_Fact.fact
type fact_override = Sledgehammer_Fact.fact_override
- type minimize_command = Sledgehammer_Reconstruct.minimize_command
+ type minimize_command = Sledgehammer_Reconstructor.minimize_command
type mode = Sledgehammer_Provers.mode
type params = Sledgehammer_Provers.params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 10 12:33:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 10 12:35:18 2013 +0200
@@ -26,6 +26,11 @@
val one_year : Time.time
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
+
+ (** extrema **)
+ val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
+ val max_option : ('a * 'a -> order) -> 'a option -> 'a option -> 'a option
+ val max_list : ('a * 'a -> order) -> 'a list -> 'a option
end;
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -152,4 +157,12 @@
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ())) f x
+(** extrema **)
+
+fun max ord x y = case ord(x,y) of LESS => y | _ => x
+
+fun max_option ord = max (option_ord ord)
+
+fun max_list ord xs = fold (SOME #> max_option ord) xs NONE
+
end;