--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon Dec 09 23:22:44 2013 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Tue Dec 10 15:24:17 2013 +0800
@@ -3,10 +3,7 @@
Author: Steffen Juilf Smolka, TU Muenchen
Compression of isar proofs by merging steps.
-Only proof steps using the MetisM proof_method are merged.
-
-PRE CONDITION: the proof must be labeled canocially, see
-Slegehammer_Proof.relabel_proof_canonically
+Only proof steps using the same proof method are merged.
*)
signature SLEDGEHAMMER_COMPRESS =
@@ -24,35 +21,26 @@
open Sledgehammer_Proof
open Sledgehammer_Preplay
-
-(*** util ***)
-
(* 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))
-
+ | do_steps [] accum = accum
+ | do_steps (step :: steps) accum = do_steps steps (do_step step accum)
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))
-
+ | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
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)
+ | do_subproofs (proof :: subproofs) x =
+ (case do_steps (steps_of_proof proof) x of
+ accum as ([], _) => accum
+ | accum => do_subproofs subproofs accum)
in
- case do_steps steps (lbls, []) of
+ (case do_steps steps (lbls, []) of
([], succs) => rev succs
- | _ => raise Fail "Sledgehammer_Compress: collect_successors"
+ | _ => raise Fail "Sledgehammer_Compress: collect_successors")
end
(* traverses steps in reverse post-order and inserts the given updates *)
@@ -60,130 +48,104 @@
let
fun do_steps [] updates = ([], updates)
| do_steps steps [] = (steps, [])
- | do_steps (step::steps) updates =
- do_step step (do_steps steps updates)
-
- and do_step step (steps, []) = (step::steps, [])
- | do_step (step as Let _) (steps, updates) = (step::steps, updates)
+ | do_steps (step :: steps) updates = do_step step (do_steps steps updates)
+ 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)"
-
+ (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)"
and do_subproofs [] updates = ([], updates)
| do_subproofs steps [] = (steps, [])
- | do_subproofs (proof::subproofs) updates =
- do_proof proof (do_subproofs subproofs updates)
-
+ | do_subproofs (proof :: subproofs) updates =
+ do_proof proof (do_subproofs subproofs updates)
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
+ let val (steps, updates) = do_steps steps updates in
+ (Proof (fix, assms, steps) :: proofs, updates)
+ end
in
- case do_steps steps (rev updates) of
+ (case do_steps steps (rev updates) of
(steps, []) => steps
- | _ => raise Fail "Sledgehammer_Compress: update_steps"
+ | _ => raise Fail "Sledgehammer_Compress: update_steps")
end
(* tries merging the first step into the second step *)
-fun try_merge
- (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), MetisM)))
- (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), MetisM))) =
+fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), meth1)))
+ (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
+ if meth1 = meth2 then
let
val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
val gfs = union (op =) gfs1 gfs2
in
- SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), MetisM)))
+ SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth1)))
end
+ else
+ NONE
| try_merge _ _ = NONE
-
-
-(*** main function ***)
-
val compress_degree = 2
val merge_timeout_slack = 1.2
-(* PRE CONDITION: the proof must be labeled canocially, see
- Slegehammer_Proof.relabel_proof_canonically *)
+(* Precondition: The proof must be labeled canonically
+ (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
fun compress_proof isar_compress
- ({get_preplay_time, set_preplay_time, preplay_quietly, ...}
- : preplay_interface)
- proof =
+ ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface) proof =
if isar_compress <= 1.0 then
proof
else
- let
- val (compress_further : unit -> bool,
- decrement_step_count : unit -> unit) =
- let
- val number_of_steps = add_proof_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 () => !delta > 0,
- fn () => delta := !delta - 1)
- end
+ let
+ val (compress_further, decrement_step_count) =
+ let
+ val number_of_steps = add_proof_steps (steps_of_proof proof) 0
+ val target_number_of_steps = Real.round (Real.fromInt number_of_steps / isar_compress)
+ val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
+ in
+ (fn () => !delta > 0, fn () => delta := !delta - 1)
+ end
-
- val (get_successors : label -> label list,
- replace_successor: label -> label list -> label -> unit) =
- let
- fun add_refs (Let _) tab = tab
- | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) tab =
- fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs tab
+ val (get_successors, replace_successor) =
+ let
+ fun add_refs (Let _) = I
+ | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
+ fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs
- 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
-
- 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)
+ 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
- in
- (get_successors, replace_successor)
- end
-
-
-
- (** elimination of trivial, one-step subproofs **)
+ 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 =
+ get_successors dest
+ |> Ord_List.remove canonical_label_ord old
+ |> Ord_List.union canonical_label_ord new
+ |> set_successors dest
+ in
+ (get_successors, replace_successor)
+ end
- fun elim_subproofs' time qs fix l t lfs gfs subs nontriv_subs =
- if null subs orelse not (compress_further ()) then
- (set_preplay_time l (false, time);
- Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), MetisM)))
- else
- case subs of
- ((sub as Proof (_, assms, sub_steps)) :: subs) =>
+ (** elimination of trivial, one-step subproofs **)
+
+ fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
+ if null subs orelse not (compress_further ()) then
+ (set_preplay_time l (false, time);
+ Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
+ else
+ (case subs of
+ (sub as Proof (_, assms, sub_steps)) :: subs =>
(let
(* trivial subproofs have exactly one Prove step *)
- val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), MetisM))) = try the_single sub_steps
+ val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
val (false, time') = get_preplay_time l'
@@ -194,7 +156,7 @@
subtract (op =) (map fst assms) lfs'
|> union (op =) lfs
val gfs'' = union (op =) gfs' gfs
- val by = ((lfs'', gfs''), MetisM)
+ val by = ((lfs'', gfs''), meth)
val step'' = Prove (qs, fix, l, t, subs'', by)
(* check if the modified step can be preplayed fast enough *)
@@ -204,165 +166,135 @@
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
- elim_subproofs' time'' qs fix l t lfs'' gfs'' subs nontriv_subs
+ elim_subproofs' time'' qs fix l t lfs'' gfs'' meth 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'"
-
+ elim_subproofs' time qs fix l t lfs gfs meth 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, ((lfs, gfs), MetisM))) =
- if subproofs = [] then step else
- case get_preplay_time l of
- (true, _) => step (* timeout or fail *)
- | (false, time) =>
- elim_subproofs' time qs fix l t lfs gfs subproofs []
-
-
+ fun elim_subproofs (step as Let _) = step
+ | elim_subproofs
+ (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+ if subproofs = [] then step else
+ case get_preplay_time l of
+ (true, _) => step (* timeout or fail *)
+ | (false, time) =>
+ elim_subproofs' time qs fix l t lfs gfs meth subproofs []
- (** top_level compression: eliminate steps by merging them into their
- successors **)
-
- fun compress_top_level steps =
- let
+ (** top_level compression: eliminate steps by merging them into their
+ successors **)
- (* #successors, (size_of_term t, position) *)
- fun cand_key (i, l, t_size) =
- (get_successors l |> length, (t_size, i))
+ fun compress_top_level steps =
+ let
+ (* (#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 compression_ord =
+ prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
+ #> rev_order
- val cand_ord = pairself cand_key #> compression_ord
+ 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)
+ 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 (_, 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
+ val candidates =
+ let
+ fun add_cand (_, Let _) = I
+ | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
+ in
+ (steps
+ |> split_last |> fst (* keep last step *)
+ |> fold_index add_cand) []
+ end
- fun try_eliminate (i, l, _) succ_lbls steps =
- let
- (* only touch steps that can be preplayed successfully *)
- val (false, time) = get_preplay_time l
-
- val succ_times =
- map (get_preplay_time #> (fn (false, t) => t)) succ_lbls
-
- val timeslice =
- time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
+ fun try_eliminate (i, l, _) succ_lbls steps =
+ let
+ (* only touch steps that can be preplayed successfully *)
+ val (false, time) = get_preplay_time l
- val timeouts =
- map (curry Time.+ timeslice #> time_mult merge_timeout_slack)
- succ_times
+ val succ_times = map (get_preplay_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, _, _, ((lfs, _), MetisM))) :: steps') = drop i steps
+ val ((cand as Prove (_, _, l, _, _, ((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
+ (* FIXME: debugging *)
+ val _ =
+ if the (label_of_step cand) <> l then
+ raise Fail "Sledgehammer_Compress: try_eliminate"
+ else
+ ()
- (* TODO: should be lazy: stop preplaying as soon as one step
- fails/times out *)
- val preplay_times =
- map (uncurry preplay_quietly) (timeouts ~~ succs')
+ val succs = collect_successors steps' succ_lbls
+ val succs' = map (try_merge cand #> the) succs
- (* ensure none of the modified successors timed out *)
- val false = List.exists fst preplay_times
+ (* TODO: should be lazy: stop preplaying as soon as one step
+ fails/times out *)
+ val preplay_times = map2 preplay_quietly timeouts succs'
- val (steps1, _::steps2) = chop i steps
+ (* ensure none of the modified successors timed out *)
+ val false = List.exists fst preplay_times
- (* replace successors with their modified versions *)
- val steps2 = update_steps steps2 succs'
-
- in
- decrement_step_count (); (* candidate successfully eliminated *)
- map (uncurry set_preplay_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
+ val (steps1, _ :: steps2) = chop i steps
+ (* replace successors with their modified versions *)
+ val steps2 = update_steps steps2 succs'
+ in
+ decrement_step_count (); (* candidate successfully eliminated *)
+ map2 set_preplay_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 > compress_degree
- then steps
- else compression_loop candidates
- (try_eliminate cand successors steps)
- end
-
-
- in
- compression_loop candidates steps
- |> filter_out (fn step => step = dummy_isar_step)
- end
-
-
+ 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 > compress_degree then steps
+ else compression_loop candidates (try_eliminate cand successors steps)
+ end)
+ in
+ compression_loop candidates steps
+ |> remove (op =) 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)) =
+ (** 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.
+ *)
+ 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 |> compress_further () ? do_sub_levels)
+ |> compress_further () ? 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 proof
- end
+ (* eliminate trivial subproofs *)
+ |> compress_further () ? elim_subproofs
+ in
+ do_proof proof
+ end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Mon Dec 09 23:22:44 2013 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Tue Dec 10 15:24:17 2013 +0800
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
+ Author: Steffen Juilf Smolka, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
Minimize dependencies (used facts) of Isar proof steps.
*)
@@ -8,9 +8,11 @@
signature SLEDGEHAMMER_MINIMIZE_ISAR =
sig
type preplay_interface = Sledgehammer_Preplay.preplay_interface
+ type isar_step = Sledgehammer_Proof.isar_step
type isar_proof = Sledgehammer_Proof.isar_proof
- val minimize_dependencies_and_remove_unrefed_steps :
- bool -> preplay_interface -> isar_proof -> isar_proof
+
+ val min_deps_of_step : preplay_interface -> isar_step -> isar_step
+ val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
end;
structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
@@ -20,49 +22,39 @@
open Sledgehammer_Proof
open Sledgehammer_Preplay
-val slack = 1.3
+val slack = seconds 0.1
fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
| min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
- (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))) =
- (case get_preplay_time l of
- (* don't touch steps that time out or fail; minimizing won't help *)
- (true, _) => step
- | (false, time) =>
- let
- fun mk_step_lfs_gfs lfs gfs =
- Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))
- val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
+ (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
+ (case get_preplay_time l of
+ (* don't touch steps that time out or fail; minimizing won't help (not true -- FIXME) *)
+ (true, _) => step
+ | (false, time) =>
+ let
+ fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
+ val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
- fun minimize_facts _ time min_facts [] = (time, min_facts)
- | minimize_facts mk_step time min_facts (f :: facts) =
- (case preplay_quietly (time_mult slack time)
- (mk_step (min_facts @ facts)) of
- (true, _) => minimize_facts mk_step time (f :: min_facts) facts
- | (false, time) => minimize_facts mk_step time min_facts facts)
-
- val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
- val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+ fun minimize_facts _ time min_facts [] = (time, min_facts)
+ | minimize_facts mk_step time min_facts (f :: facts) =
+ (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of
+ (true, _) => minimize_facts mk_step time (f :: min_facts) facts
+ | (false, time) => minimize_facts mk_step time min_facts facts)
- in
- set_preplay_time l (false, time);
- mk_step_lfs_gfs min_lfs min_gfs
- end)
+ val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
+ val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+ in
+ set_preplay_time l (false, time); mk_step_lfs_gfs min_lfs min_gfs
+ end)
-fun minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface
- proof =
+fun postprocess_remove_unreferenced_steps postproc_step =
let
- fun cons_to xs x = x :: xs
-
val add_lfs = fold (Ord_List.insert label_ord)
fun do_proof (Proof (fix, assms, steps)) =
- let
- val (refed, steps) = do_steps steps
- in
+ let val (refed, steps) = do_steps steps in
(refed, Proof (fix, assms, steps))
end
-
and do_steps steps =
let
(* the last step is always implicitly referenced *)
@@ -72,7 +64,6 @@
in
fold_rev do_step steps (refed, [concl])
end
-
and do_step step (refed, accu) =
case label_of_step step of
NONE => (refed, step :: accu)
@@ -80,15 +71,10 @@
if Ord_List.member label_ord refed l then
do_refed_step step
|>> Ord_List.union label_ord refed
- ||> cons_to accu
+ ||> (fn x => x :: accu)
else
(refed, accu)
-
- and do_refed_step step =
- step
- |> isar_try0 ? min_deps_of_step preplay_interface
- |> do_refed_step'
-
+ and do_refed_step step = step |> postproc_step |> do_refed_step'
and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
| do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
let
@@ -102,7 +88,7 @@
(refed, step)
end
in
- snd (do_proof proof)
+ snd o do_proof
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 09 23:22:44 2013 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Dec 10 15:24:17 2013 +0800
@@ -64,10 +64,8 @@
clsarity). *)
fun is_only_type_information t = t aconv @{term True}
-fun s_maybe_not role = role <> Conjecture ? s_not
-
fun is_same_inference (role, t) (_, role', t', _, _) =
- s_maybe_not role t aconv s_maybe_not role' t'
+ (t |> role = Conjecture ? s_not) aconv (t' |> role' = Conjecture ? s_not)
(* Discard facts; consolidate adjacent lines that prove the same formula, since
they differ only in type information.*)
@@ -86,11 +84,12 @@
(* Type information will be deleted later; skip repetition test. *)
if is_only_type_information t then
line :: lines
- (* Is there a repetition? If so, replace later line by earlier one. *)
- else case take_prefix (not o is_same_inference (role, t)) lines of
- (_, []) => line :: lines
- | (pre, (name', _, _, _, _) :: post) =>
- line :: pre @ map (replace_dependencies_in_line (name', [name])) post
+ else
+ (* Is there a repetition? If so, replace later line by earlier one. *)
+ (case take_prefix (not o is_same_inference (role, t)) lines of
+ (_, []) => line :: lines
+ | (pre, (name', _, _, _, _) :: post) =>
+ line :: pre @ map (replace_dependencies_in_line (name', [name])) post)
(* Recursively delete empty lines (type information) from the proof. *)
fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
@@ -201,6 +200,7 @@
in chain_proof end
fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
+val maybe_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
type isar_params =
bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
@@ -239,7 +239,7 @@
val assms = map_filter (get_role (curry (op =) Hypothesis)) atp_proof
val lems =
map_filter (get_role (curry (op =) Lemma)) atp_proof
- |> map (fn (l, t) => Prove ([], [], l, t, [], (([], []), ArithM)))
+ |> map (fn (l, t) => Prove ([], [], l, maybe_mk_Trueprop t, [], (([], []), ArithM)))
val bot = atp_proof |> List.last |> #1
@@ -258,7 +258,7 @@
|> fold (fn (name as (s, _), role, t, rule, _) =>
Symtab.update_new (s, (rule,
t |> (if is_clause_tainted [name] then
- s_maybe_not role
+ role <> Conjecture ? (maybe_dest_Trueprop #> s_not)
#> fold exists_of (map Var (Term.add_vars t []))
else
I))))
@@ -268,12 +268,14 @@
Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = SOME true
| is_clause_skolemize_rule _ = false
- (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s. *)
+ (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s (for ATPs) or
+ "prop"s (for Z3). TODO: Always use "prop". *)
fun prop_of_clause [(num, _)] =
Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form
| prop_of_clause names =
let
- val lits = map snd (map_filter (Symtab.lookup steps o fst) names)
+ val lits =
+ map (maybe_dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
in
case List.partition (can HOLogic.dest_not) lits of
(negs as _ :: _, pos as _ :: _) =>
@@ -305,7 +307,7 @@
fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
in
if is_clause_tainted c then
- case gamma of
+ (case gamma of
[g] =>
if is_clause_skolemize_rule g andalso is_clause_tainted g then
let
@@ -315,7 +317,7 @@
end
else
do_rest l (prove [] by)
- | _ => do_rest l (prove [] by)
+ | _ => do_rest l (prove [] by))
else
if is_clause_skolemize_rule c then
do_rest l (Prove ([], skolems_of t, l, t, [], by))
@@ -350,13 +352,14 @@
val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
refute_graph
(*
- |> tap (tracing o prefix "REFUTE: " o string_of_refute_graph)
+ |> tap (tracing o prefix "REFUTE GRAPH: " o string_of_refute_graph)
*)
|> redirect_graph axioms tainted bot
(*
- |> tap (tracing o prefix "DIRECT: " o string_of_direct_proof)
+ |> tap (tracing o prefix "DIRECT PROOF: " o string_of_direct_proof)
*)
|> isar_proof_of_direct_proof
+ |> postprocess_remove_unreferenced_steps I
|> relabel_proof_canonically
|> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
preplay_timeout)
@@ -365,7 +368,7 @@
|> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0)
preplay_interface
|> isar_try0 ? try0 preplay_timeout preplay_interface
- |> minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface
+ |> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface)
|> `overall_preplay_stats
||> clean_up_labels_in_proof
val isar_text =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 09 23:22:44 2013 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Tue Dec 10 15:24:17 2013 +0800
@@ -17,46 +17,40 @@
structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =
struct
+open Sledgehammer_Util
open Sledgehammer_Proof
open Sledgehammer_Preplay
-fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants"
- | variants (Prove (qs, xs, l, t, subproofs, (facts, _))) =
- let
- val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM]
- fun step method = Prove (qs, xs, l, t, subproofs, (facts, method))
- (*fun step_without_facts method =
- Prove (qs, xs, l, t, subproofs, (no_facts, method))*)
- in
- (* FIXME *)
- (* There seems to be a bias for methods earlier in the list, so we put
- the variants using no facts first. *)
- (*map step_without_facts methods @*) map step methods
- end
+val variant_methods = [SimpM, AutoM, ArithM, FastforceM, BlastM, ForceM, MetisM]
+
+fun variants_of_step (Let _) = raise Fail "Sledgehammer_Try0: variants_of_step"
+ | variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meth))) =
+ variant_methods
+ |> remove (op =) meth
+ |> map (fn meth' => Prove (qs, xs, l, t, subproofs, (facts, meth')))
+
+val slack = seconds 0.05
fun try0_step _ _ (step as Let _) = step
- | try0_step preplay_timeout ({preplay_quietly, get_preplay_time,
- set_preplay_time, ...} : preplay_interface)
- (step as Prove (_, _, l, _, _, _)) =
- let
-
- val timeout =
- case get_preplay_time l of
- (true, _) => preplay_timeout
- | (false, t) => t
+ | try0_step preplay_timeout
+ ({preplay_quietly, get_preplay_time, set_preplay_time, ...} : preplay_interface)
+ (step as Prove (_, _, l, _, _, _)) =
+ let
+ val timeout =
+ (case get_preplay_time l of
+ (true, _) => preplay_timeout
+ | (false, t) => Time.+ (t, slack))
- fun try_variant variant =
- case preplay_quietly timeout variant of
- (true, _) => NONE
- | time as (false, _) => SOME (variant, time)
+ fun try_variant variant =
+ (case preplay_quietly timeout variant of
+ (true, _) => NONE
+ | time as (false, _) => SOME (variant, time))
+ in
+ (case Par_List.get_some try_variant (variants_of_step step) of
+ SOME (step, time) => (set_preplay_time l time; step)
+ | NONE => step)
+ end
- in
- case Par_List.get_some try_variant (variants step) of
- SOME (step, time) => (set_preplay_time l time; step)
- | NONE => step
- end
-
-fun try0 preplay_timeout preplay_interface proof =
- map_isar_steps (try0_step preplay_timeout preplay_interface) proof
+val try0 = map_isar_steps oo try0_step
end;