--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:14:18 2014 +0100
@@ -234,13 +234,6 @@
val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0
- (* FIXME: debugging *)
- val _ =
- if the (label_of_isar_step cand) <> l then
- raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
- else
- ()
-
(* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
val play_outcomes = map3 (preplay_isar_step ctxt) timeouts succ_meths succs'
@@ -282,16 +275,12 @@
|> remove (op =) dummy_isar_step
end
- (*
- 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.
- *)
+ (* 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 compress_proof (proof as (Proof (fix, assms, steps))) =
if compress_further () then Proof (fix, assms, compress_steps steps) else proof
and compress_steps steps =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 10:14:18 2014 +0100
@@ -33,7 +33,7 @@
val slack = seconds 0.1
fun minimize_isar_step_dependencies ctxt preplay_data
- (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
+ (step as Prove (qs, xs, l, t, subproofs, ((lfs0, gfs0), meths as meth :: _))) =
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
Played time =>
let
@@ -46,8 +46,8 @@
Played time => minimize_facts mk_step time min_facts facts
| _ => minimize_facts mk_step time (f :: min_facts) facts)
- val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs) time [] lfs
- val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+ val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) time [] lfs0
+ val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs0
val step' = mk_step_lfs_gfs min_lfs min_gfs
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:14:18 2014 +0100
@@ -181,17 +181,15 @@
end
| set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
-fun preplay_outcome_of_isar_step_for_method preplay_data l meth =
- let val SOME meths_outcomes = Canonical_Label_Tab.lookup preplay_data l in
- the (AList.lookup (op =) meths_outcomes meth)
- end
+fun preplay_outcome_of_isar_step_for_method preplay_data l =
+ the o AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
-fun fastest_method_of_isar_step preplay_data l =
- the (Canonical_Label_Tab.lookup preplay_data l)
- |> map (fn (meth, outcome) =>
+fun fastest_method_of_isar_step preplay_data =
+ Canonical_Label_Tab.lookup preplay_data #> the
+ #> map (fn (meth, outcome) =>
(meth, Time.toMilliseconds (case Lazy.force outcome of Played time => time | _ => one_year)))
- |> sort (int_ord o pairself snd)
- |> hd |> fst
+ #> sort (int_ord o pairself snd)
+ #> hd #> fst
fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meths))) =
Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))