# HG changeset patch # User blanchet # Date 1391190196 -3600 # Node ID 9d833fe96c5180967d2017bee4ab6bfd91a090ab # Parent 6fe9fd75f9d79e990a0708ae8299f017362ab5a6 moved code around diff -r 6fe9fd75f9d7 -r 9d833fe96c51 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 18:43:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 18:43:16 2014 +0100 @@ -103,89 +103,6 @@ add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines) end -val add_labels_of_proof = - steps_of_proof - #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I)) - -fun kill_useless_labels_in_proof proof = - let - val used_ls = add_labels_of_proof proof [] - - fun kill_label l = if member (op =) used_ls l then l else no_label - fun kill_assms assms = map (apfst kill_label) assms - - fun kill_step (Prove (qs, xs, l, t, subproofs, by)) = - Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by) - | kill_step step = step - and kill_proof (Proof (fix, assms, steps)) = - Proof (fix, kill_assms assms, map kill_step steps) - in - kill_proof proof - end - -val assume_prefix = "a" -val have_prefix = "f" - -val relabel_proof = - let - fun fresh_label depth prefix (accum as (l, subst, next)) = - if l = no_label then - accum - else - let val l' = (replicate_string (depth + 1) prefix, next) in - (l', (l, l') :: subst, next + 1) - end - - fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst)) - - fun relabel_assm depth (l, t) (subst, next) = - let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in - ((l, t), (subst, next)) - end - - fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst - - fun relabel_steps _ _ _ [] = [] - | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) = - let - val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix - val sub = relabel_proofs subst depth sub - val by = apfst (relabel_facts subst) by - in - Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps - end - | relabel_steps subst depth next (step :: steps) = - step :: relabel_steps subst depth next steps - and relabel_proof subst depth (Proof (fix, assms, steps)) = - let val (assms, subst) = relabel_assms subst depth assms in - Proof (fix, assms, relabel_steps subst depth 1 steps) - end - and relabel_proofs subst depth = map (relabel_proof subst (depth + 1)) - in - relabel_proof [] 0 - end - -val chain_direct_proof = - let - fun chain_qs_lfs NONE lfs = ([], lfs) - | chain_qs_lfs (SOME l0) lfs = - if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs) - fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) = - let val (qs', lfs) = chain_qs_lfs lbl lfs in - Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss)) - end - | chain_step _ step = step - and chain_steps _ [] = [] - | chain_steps (prev as SOME _) (i :: is) = - chain_step prev i :: chain_steps (label_of_step i) is - | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is - and chain_proof (Proof (fix, assms, steps)) = - Proof (fix, assms, chain_steps (try (List.last #> fst) assms) steps) - and chain_proofs proofs = map (chain_proof) proofs - in - chain_proof - end - type isar_params = bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm @@ -378,7 +295,9 @@ (try0_isar ? minimize_isar_step_dependencies preplay_data) |> tap (trace_isar_proof "Minimized") |> `overall_preplay_outcome - ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof) + ||> chain_isar_proof + ||> kill_useless_labels_in_isar_proof + ||> relabel_isar_proof_finally in (case string_of_isar_proof false isar_proof of "" => diff -r 6fe9fd75f9d7 -r 9d833fe96c51 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 18:43:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 18:43:16 2014 +0100 @@ -42,7 +42,11 @@ structure Canonical_Label_Tab : TABLE val canonical_label_ord : (label * label) -> order + + val chain_isar_proof : isar_proof -> isar_proof + val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof val relabel_isar_proof_canonically : isar_proof -> isar_proof + val relabel_isar_proof_finally : isar_proof -> isar_proof val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> bool -> isar_proof -> string @@ -127,6 +131,38 @@ type key = label val ord = canonical_label_ord) +fun chain_qs_lfs NONE lfs = ([], lfs) + | chain_qs_lfs (SOME l0) lfs = + if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs) +fun chain_isar_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) = + let val (qs', lfs) = chain_qs_lfs lbl lfs in + Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, ((lfs, gfs), methss)) + end + | chain_isar_step _ step = step +and chain_isar_steps _ [] = [] + | chain_isar_steps (prev as SOME _) (i :: is) = + chain_isar_step prev i :: chain_isar_steps (label_of_step i) is + | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_step i) is +and chain_isar_proof (Proof (fix, assms, steps)) = + Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps) + +fun kill_useless_labels_in_isar_proof proof = + let + val used_ls = + fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I)) + (steps_of_proof proof) [] + + fun kill_label l = if member (op =) used_ls l then l else no_label + + fun kill_step (Prove (qs, xs, l, t, subproofs, by)) = + Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by) + | kill_step step = step + and kill_proof (Proof (fix, assms, steps)) = + Proof (fix, map (apfst kill_label) assms, map kill_step steps) + in + kill_proof proof + end + fun relabel_isar_proof_canonically proof = let fun next_label l (next, subst) = @@ -162,6 +198,48 @@ fst (do_proof proof (0, [])) end +val assume_prefix = "a" +val have_prefix = "f" + +val relabel_isar_proof_finally = + let + fun fresh_label depth prefix (accum as (l, subst, next)) = + if l = no_label then + accum + else + let val l' = (replicate_string (depth + 1) prefix, next) in + (l', (l, l') :: subst, next + 1) + end + + fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst)) + + fun relabel_assm depth (l, t) (subst, next) = + let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in + ((l, t), (subst, next)) + end + + fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst + + fun relabel_steps _ _ _ [] = [] + | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) = + let + val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix + val sub = relabel_proofs subst depth sub + val by = apfst (relabel_facts subst) by + in + Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps + end + | relabel_steps subst depth next (step :: steps) = + step :: relabel_steps subst depth next steps + and relabel_proof subst depth (Proof (fix, assms, steps)) = + let val (assms, subst) = relabel_assms subst depth assms in + Proof (fix, assms, relabel_steps subst depth 1 steps) + end + and relabel_proofs subst depth = map (relabel_proof subst (depth + 1)) + in + relabel_proof [] 0 + end + val indent_size = 2 fun string_of_isar_proof ctxt type_enc lam_trans i n all_methods proof =