# HG changeset patch # User blanchet # Date 1391418858 -3600 # Node ID 4d63fffcde8d5daefc3a251eccdb498ca0f4cb0d # Parent 16724746ad89dd04b455f5f5e178470a0f83b618 tuned diff -r 16724746ad89 -r 4d63fffcde8d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 00:22:48 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 10:14:18 2014 +0100 @@ -289,13 +289,13 @@ val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty - fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) = + fun init_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) = set_preplay_outcomes_of_isar_step preplay_data l (map (fn meth => (meth, Lazy.lazy (fn () => preplay_isar_step preplay_ctxt preplay_timeout meth step))) meths) - | reset_preplay_outcomes _ = () + | init_preplay_outcomes _ = () - val _ = fold_isar_steps (K o reset_preplay_outcomes) + val _ = fold_isar_steps (K o init_preplay_outcomes) (steps_of_isar_proof canonical_isar_proof) () fun str_of_preplay_outcome outcome = diff -r 16724746ad89 -r 4d63fffcde8d src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 00:22:48 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:14:18 2014 +0100 @@ -28,21 +28,21 @@ (* 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 [] 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 + fun collect_steps _ ([], accu) = ([], accu) + | collect_steps [] accum = accum + | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum) + and collect_step (Let _) x = x + | collect_step (step as Prove (_, _, l, _, subproofs, _)) x = + (case collect_subproofs subproofs x of ([], accu) => ([], 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_isar_proof proof) x of + and collect_subproofs [] x = x + | collect_subproofs (proof :: subproofs) x = + (case collect_steps (steps_of_isar_proof proof) x of accum as ([], _) => accum - | accum => do_subproofs subproofs accum) + | accum => collect_subproofs subproofs accum) in - (case do_steps steps (lbls, []) of + (case collect_steps steps (lbls, []) of ([], succs) => rev succs | _ => raise Fail "Sledgehammer_Isar_Compress: collect_successors") end @@ -50,32 +50,32 @@ (* 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) - 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)) + fun update_steps [] updates = ([], updates) + | update_steps steps [] = (steps, []) + | update_steps (step :: steps) updates = update_step step (update_steps steps updates) + and update_step step (steps, []) = (step :: steps, []) + | update_step (step as Let _) (steps, updates) = (step :: steps, updates) + | update_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 + if l = l' then update_subproofs subproofs' updates' + else update_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_Isar_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) - and do_proof proof (proofs, []) = (proof :: proofs, []) - | do_proof (Proof (fix, assms, steps)) (proofs, updates) = - let val (steps, updates) = do_steps steps updates in + and update_subproofs [] updates = ([], updates) + | update_subproofs steps [] = (steps, []) + | update_subproofs (proof :: subproofs) updates = + update_proof proof (update_subproofs subproofs updates) + and update_proof proof (proofs, []) = (proof :: proofs, []) + | update_proof (Proof (fix, assms, steps)) (proofs, updates) = + let val (steps, updates) = update_steps steps updates in (Proof (fix, assms, steps) :: proofs, updates) end in - (case do_steps steps (rev updates) of + (case update_steps steps (rev updates) of (steps, []) => steps | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps") end @@ -182,7 +182,6 @@ Played time => elim_subproofs' time qs fix l t lfs gfs meths subproofs [] | _ => step) - (** top_level compression: eliminate steps by merging them into their successors **) fun compress_top_level steps = let (* (#successors, (size_of_term t, position)) *) @@ -278,7 +277,6 @@ |> remove (op =) dummy_isar_step end - (** recusion over the proof tree **) (* Proofs are compressed bottom-up, beginning with the innermost subproofs. @@ -289,20 +287,20 @@ 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 = + 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 = (* bottom-up: compress innermost proofs first *) - steps |> map (fn step => step |> compress_further () ? do_sub_levels) + steps |> map (fn step => step |> compress_further () ? compress_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)) = + and compress_sub_levels (step as Let _) = step + | compress_sub_levels (Prove (qs, xs, l, t, subproofs, by)) = (* compress subproofs *) - Prove (qs, xs, l, t, map do_proof subproofs, by) + Prove (qs, xs, l, t, map compress_proof subproofs, by) (* eliminate trivial subproofs *) |> compress_further () ? elim_subproofs in - do_proof proof + compress_proof proof end end; diff -r 16724746ad89 -r 4d63fffcde8d src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 00:22:48 2014 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 10:14:18 2014 +0100 @@ -33,7 +33,6 @@ Played time => let fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths)) - 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) = @@ -42,7 +41,7 @@ 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 (mk_step_gfs_lfs gfs) time [] lfs + 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 in set_preplay_outcomes_of_isar_step preplay_data l [(meth, Lazy.value (Played time))];