1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 04 23:11:18 2014 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 04 23:11:18 2014 +0100
1.3 @@ -316,15 +316,19 @@
1.4 val (play_outcome, isar_proof) =
1.5 canonical_isar_proof
1.6 |> tap (trace_isar_proof "Original")
1.7 - |> compress_isar_proof ctxt compress_isar preplay_data
1.8 + |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
1.9 |> tap (trace_isar_proof "Compressed")
1.10 |> postprocess_isar_proof_remove_unreferenced_steps
1.11 (keep_fastest_method_of_isar_step (!preplay_data)
1.12 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
1.13 |> tap (trace_isar_proof "Minimized")
1.14 + (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
1.15 + unnatural semantics): *)
1.16 +(*
1.17 |> minimize
1.18 - ? (compress_isar_proof ctxt compress_isar preplay_data
1.19 + ? (compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
1.20 #> tap (trace_isar_proof "Compressed again"))
1.21 +*)
1.22 |> `(preplay_outcome_of_isar_proof (!preplay_data))
1.23 ||> (comment_isar_proof comment_of
1.24 #> chain_isar_proof
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Tue Feb 04 23:11:18 2014 +0100
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Tue Feb 04 23:11:18 2014 +0100
2.3 @@ -11,8 +11,8 @@
2.4 type isar_proof = Sledgehammer_Isar_Proof.isar_proof
2.5 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
2.6
2.7 - val compress_isar_proof : Proof.context -> real -> isar_preplay_data Unsynchronized.ref ->
2.8 - isar_proof -> isar_proof
2.9 + val compress_isar_proof : Proof.context -> real -> Time.time ->
2.10 + isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof
2.11 end;
2.12
2.13 structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
2.14 @@ -27,17 +27,17 @@
2.15
2.16 fun collect_successors steps lbls =
2.17 let
2.18 - fun collect_steps _ ([], accu) = ([], accu)
2.19 + fun collect_steps _ (accum as ([], _)) = accum
2.20 | collect_steps [] accum = accum
2.21 | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)
2.22 - and collect_step (Let _) x = x
2.23 - | collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x =
2.24 + and collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x =
2.25 (case collect_subproofs subproofs x of
2.26 - ([], accu) => ([], accu)
2.27 + (accum as ([], _)) => accum
2.28 | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
2.29 - and collect_subproofs [] x = x
2.30 - | collect_subproofs (proof :: subproofs) x =
2.31 - (case collect_steps (steps_of_isar_proof proof) x of
2.32 + | collect_step _ accum = accum
2.33 + and collect_subproofs [] accum = accum
2.34 + | collect_subproofs (proof :: subproofs) accum =
2.35 + (case collect_steps (steps_of_isar_proof proof) accum of
2.36 accum as ([], _) => accum
2.37 | accum => collect_subproofs subproofs accum)
2.38 in
2.39 @@ -50,7 +50,6 @@
2.40 | update_steps steps [] = (steps, [])
2.41 | update_steps (step :: steps) updates = update_step step (update_steps steps updates)
2.42 and update_step step (steps, []) = (step :: steps, [])
2.43 - | update_step (step as Let _) (steps, updates) = (step :: steps, updates)
2.44 | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment))
2.45 (steps,
2.46 updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') =
2.47 @@ -61,6 +60,7 @@
2.48 update_subproofs subproofs updates
2.49 |>> (fn subproofs => Prove (qs, xs, l, t, subproofs, facts, meths, comment)))
2.50 |>> (fn step => step :: steps)
2.51 + | update_step step (steps, updates) = (step :: steps, updates)
2.52 and update_subproofs [] updates = ([], updates)
2.53 | update_subproofs steps [] = (steps, [])
2.54 | update_subproofs (proof :: subproofs) updates =
2.55 @@ -89,29 +89,30 @@
2.56 (hopeful @ hopeless, hopeless)
2.57 end
2.58
2.59 -fun try_merge_steps preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
2.60 - (Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
2.61 - (case merge_methods preplay_data (l1, meths1) (l2, meths2) of
2.62 - ([], _) => NONE
2.63 - | (meths, hopeless) =>
2.64 - let
2.65 - val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
2.66 - val gfs = union (op =) gfs1 gfs2
2.67 - in
2.68 - SOME (Prove (qs2, fix, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths,
2.69 - comment1 ^ comment2), hopeless)
2.70 - end)
2.71 +fun try_merge_steps preplay_data (Prove ([], fix1, l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
2.72 + (Prove (qs2, fix2, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
2.73 + let
2.74 + val (meths, hopeless) = merge_methods preplay_data (l1, meths1) (l2, meths2)
2.75 + val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
2.76 + val gfs = union (op =) gfs1 gfs2
2.77 + in
2.78 + SOME (Prove (qs2, union (op =) fix1 fix2, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths,
2.79 + comment1 ^ comment2), hopeless)
2.80 + end
2.81 | try_merge_steps _ _ _ = NONE
2.82
2.83 +val merge_slack_time = seconds 0.005
2.84 +val merge_slack_factor = 1.5
2.85 +
2.86 +fun adjust_merge_timeout max time =
2.87 + let val timeout = time_mult merge_slack_factor (Time.+ (merge_slack_time, time)) in
2.88 + if Time.< (max, timeout) then max else timeout
2.89 + end
2.90 +
2.91 val compress_degree = 2
2.92 -val merge_timeout_slack_time = seconds 0.005
2.93 -val merge_timeout_slack_factor = 1.5
2.94 -
2.95 -fun slackify_merge_timeout time =
2.96 - time_mult merge_timeout_slack_factor (Time.+ (merge_timeout_slack_time, time))
2.97
2.98 (* Precondition: The proof must be labeled canonically. *)
2.99 -fun compress_isar_proof ctxt compress_isar preplay_data proof =
2.100 +fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof =
2.101 if compress_isar <= 1.0 then
2.102 proof
2.103 else
2.104 @@ -180,7 +181,7 @@
2.105 val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'', comment)
2.106
2.107 (* check if the modified step can be preplayed fast enough *)
2.108 - val timeout = slackify_merge_timeout (Time.+ (time, time'))
2.109 + val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, time'))
2.110 val (_, Played time'') :: meths_outcomes =
2.111 preplay_isar_step ctxt timeout hopeless step''
2.112 in
2.113 @@ -190,7 +191,8 @@
2.114 nontriv_subs
2.115 end
2.116 handle Bind =>
2.117 - elim_one_subproof time [] qs fix l t lfs gfs meths comment subs (sub :: nontriv_subs))
2.118 + elim_one_subproof time [] qs fix l t lfs gfs meths comment subs
2.119 + (sub :: nontriv_subs))
2.120 | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
2.121
2.122 fun elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)) =
2.123 @@ -232,18 +234,20 @@
2.124
2.125 val succs = collect_successors steps' labels
2.126
2.127 - (* only touch steps that can be preplayed successfully; FIXME: more generous *)
2.128 - val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l
2.129 + val time =
2.130 + (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of
2.131 + Played time => time
2.132 + | _ => preplay_timeout)
2.133
2.134 val (succs', hopelesses) =
2.135 map (try_merge_steps (!preplay_data) cand #> the) succs
2.136 |> split_list
2.137
2.138 - (* FIXME: more generous *)
2.139 val times0 = map ((fn Played time => time) o
2.140 forced_intermediate_preplay_outcome_of_isar_step (!preplay_data)) labels
2.141 val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
2.142 - val timeouts = map (curry Time.+ time_slice #> slackify_merge_timeout) times0
2.143 + val timeouts =
2.144 + map (curry Time.+ time_slice #> adjust_merge_timeout preplay_timeout) times0
2.145 (* FIXME: "preplay_timeout" should be an ultimate maximum *)
2.146
2.147 val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
2.148 @@ -294,12 +298,12 @@
2.149 (* bottom-up: compress innermost proofs first *)
2.150 steps |> map (fn step => step |> compress_further () ? compress_sub_levels)
2.151 |> compress_further () ? compress_top_level
2.152 - and compress_sub_levels (step as Let _) = step
2.153 - | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
2.154 + and compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) =
2.155 (* compress subproofs *)
2.156 Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment)
2.157 (* eliminate trivial subproofs *)
2.158 |> compress_further () ? elim_subproofs
2.159 + | compress_sub_levels step = step
2.160 in
2.161 compress_proof proof
2.162 end
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Tue Feb 04 23:11:18 2014 +0100
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Tue Feb 04 23:11:18 2014 +0100
3.3 @@ -133,8 +133,8 @@
3.4
3.5 val play_outcome = take_time timeout prove ()
3.6 in
3.7 - (if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
3.8 - play_outcome)
3.9 + if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
3.10 + play_outcome
3.11 end
3.12
3.13 fun preplay_isar_step_for_method ctxt timeout meth =
3.14 @@ -200,7 +200,8 @@
3.15 end
3.16
3.17 fun preplay_outcome_of_isar_step_for_method preplay_data l =
3.18 - the o AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
3.19 + AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
3.20 + #> the_default (Lazy.value Not_Played)
3.21
3.22 fun fastest_method_of_isar_step preplay_data =
3.23 the o Canonical_Label_Tab.lookup preplay_data