# HG changeset patch # User blanchet # Date 1391423868 -3600 # Node ID df41d34d1324c1d4446709733bca0a12830960b5 # Parent 73372494fd80b47812306674e0547e53f9286f7b tuned data structure diff -r 73372494fd80 -r df41d34d1324 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 11:30:53 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 11:37:48 2014 +0100 @@ -230,9 +230,9 @@ val skolem = is_skolemize_rule rule fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by) - fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs + fun steps_of_rest l step = isar_steps outer (SOME l) (step :: accum) infs - val deps = fold add_fact_of_dependencies gamma no_facts + val deps = fold add_fact_of_dependencies gamma ([], []) val meths = (if skolem then skolem_methods else if is_arith_rule rule then arith_methods @@ -246,13 +246,14 @@ [g] => if skolem andalso is_clause_tainted g then let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in - isar_steps outer (SOME l) [prove [subproof] (no_facts, meths)] infs + isar_steps outer (SOME l) [prove [subproof] (([], []), meths)] infs end else - do_rest l (prove [] by) - | _ => do_rest l (prove [] by)) + steps_of_rest l (prove [] by) + | _ => steps_of_rest l (prove [] by)) else - do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by) + steps_of_rest l + (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by) end | isar_steps outer predecessor accum (Cases cases :: infs) = let diff -r 73372494fd80 -r df41d34d1324 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 11:30:53 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 11:37:48 2014 +0100 @@ -169,7 +169,7 @@ outcome as Played _ => SOME (meth, outcome) | _ => NONE) - val meths = snd (byline_of_isar_step step) + val meths = proof_methods_of_isar_step step in the_list (Par_List.get_some try_method meths) end diff -r 73372494fd80 -r df41d34d1324 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 11:30:53 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 11:37:48 2014 +0100 @@ -33,7 +33,6 @@ (facts * proof_method list) val no_label : label - val no_facts : facts val label_ord : label * label -> order val string_of_label : label -> string @@ -43,7 +42,8 @@ val steps_of_isar_proof : isar_proof -> isar_step list val label_of_isar_step : isar_step -> label option - val byline_of_isar_step : isar_step -> facts * proof_method list + val facts_of_isar_step : isar_step -> facts + val proof_methods_of_isar_step : isar_step -> proof_method list val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof @@ -98,7 +98,6 @@ (facts * proof_method list) val no_label = ("", ~1) -val no_facts = ([],[]) val label_ord = pairself swap #> prod_ord int_ord fast_string_ord @@ -127,8 +126,11 @@ fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs | subproofs_of_isar_step _ = NONE -fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = byline - | byline_of_isar_step _ = (([], []), []) +fun facts_of_isar_step (Prove (_, _, _, _, _, (facts, _))) = facts + | facts_of_isar_step _ = ([], []) + +fun proof_methods_of_isar_step (Prove (_, _, _, _, _, (_, meths))) = meths + | proof_methods_of_isar_step _ = [] fun fold_isar_step f step = fold (steps_of_isar_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step @@ -169,8 +171,7 @@ fun kill_useless_labels_in_isar_proof proof = let val used_ls = - fold_isar_steps (byline_of_isar_step #> (fn ((ls, _), _) => union (op =) ls | _ => I)) - (steps_of_isar_proof proof) [] + fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) [] fun kill_label l = if member (op =) used_ls l then l else no_label @@ -188,34 +189,34 @@ fun next_label l (next, subst) = let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end - fun do_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by + fun relabel_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by handle Option.Option => raise Fail "Sledgehammer_Isar_Proof: relabel_isar_proof_canonically" - fun do_assm (l, t) state = + fun relabel_assm (l, t) state = let val (l, state) = next_label l state in ((l, t), state) end - fun do_proof (Proof (fix, assms, steps)) state = + fun relabel_proof (Proof (fix, assms, steps)) state = let - val (assms, state) = fold_map do_assm assms state - val (steps, state) = fold_map do_step steps state + val (assms, state) = fold_map relabel_assm assms state + val (steps, state) = fold_map relabel_step steps state in (Proof (fix, assms, steps), state) end - and do_step (step as Let _) state = (step, state) - | do_step (Prove (qs, fix, l, t, subproofs, by)) state= + and relabel_step (step as Let _) state = (step, state) + | relabel_step (Prove (qs, fix, l, t, subproofs, by)) state= let - val by = do_byline by state - val (subproofs, state) = fold_map do_proof subproofs state + val by = relabel_byline by state + val (subproofs, state) = fold_map relabel_proof subproofs state val (l, state) = next_label l state in (Prove (qs, fix, l, t, subproofs, by), state) end in - fst (do_proof proof (0, [])) + fst (relabel_proof proof (0, [])) end val assume_prefix = "a"