# HG changeset patch # User blanchet # Date 1391182003 -3600 # Node ID dcb36a2540bc13f0182fb2faf9942c52504beec0 # Parent 5832470d956ed96fb81020c5067f2e180059b952 tuned ML function names diff -r 5832470d956e -r dcb36a2540bc src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 16:10:39 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 16:26:43 2014 +0100 @@ -352,35 +352,35 @@ |> tap (tracing o prefix "Direct proof: " o string_of_direct_proof) *) |> isar_proof true params assms lems - |> postprocess_remove_unreferenced_steps I - |> relabel_proof_canonically - |> `(proof_preplay_data debug ctxt metis_type_enc metis_lam_trans do_preplay - preplay_timeout) + |> postprocess_isar_proof_remove_unreferenced_steps I + |> relabel_isar_proof_canonically + |> `(preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay + preplay_timeout) val (play_outcome, isar_proof) = isar_proof - |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0) preplay_data + |> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0) + preplay_data |> try0_isar ? try0_isar_proof preplay_timeout preplay_data - |> postprocess_remove_unreferenced_steps (try0_isar ? minimal_deps_of_step preplay_data) + |> postprocess_isar_proof_remove_unreferenced_steps + (try0_isar ? minimize_isar_step_dependencies preplay_data) |> `overall_preplay_outcome ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof) val isar_text = - string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof + string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof in (case isar_text of "" => - if isar_proofs = SOME true then - "\nNo structured proof available (proof too simple)." - else - "" + if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)." + else "" | _ => let val msg = (if verbose then - let val num_steps = add_isar_steps (steps_of_proof isar_proof) 0 in - [string_of_int num_steps ^ " step" ^ plural_s num_steps] - end + let val num_steps = add_isar_steps (steps_of_proof isar_proof) 0 in + [string_of_int num_steps ^ " step" ^ plural_s num_steps] + end else []) @ (if do_preplay then [string_of_play_outcome play_outcome] else []) diff -r 5832470d956e -r dcb36a2540bc src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Jan 31 16:10:39 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Jan 31 16:26:43 2014 +0100 @@ -9,12 +9,12 @@ When configuring the pretty printer appropriately, the constraints will show up as type annotations when printing the term. This allows the term to be printed and reparsed without a change of types. -NOTE: Terms should be unchecked before calling annotate_types to avoid awkward syntax. +Note: Terms should be unchecked before calling "annotate_types_in_term" to avoid awkward syntax. *) signature SLEDGEHAMMER_ISAR_ANNOTATE = sig - val annotate_types : Proof.context -> term -> term + val annotate_types_in_term : Proof.context -> term -> term end; structure Sledgehammer_Isar_Annotate : SLEDGEHAMMER_ISAR_ANNOTATE = @@ -197,7 +197,7 @@ end (* (7) Annotate *) -fun annotate_types ctxt t = +fun annotate_types_in_term ctxt t = let val t' = generalize_types ctxt t val subst = match_types ctxt t' t diff -r 5832470d956e -r dcb36a2540bc src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 16:10:39 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 16:26:43 2014 +0100 @@ -9,9 +9,9 @@ signature SLEDGEHAMMER_ISAR_COMPRESS = sig type isar_proof = Sledgehammer_Isar_Proof.isar_proof - type preplay_data = Sledgehammer_Isar_Preplay.preplay_data + type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data - val compress_proof : real -> preplay_data -> isar_proof -> isar_proof + val compress_isar_proof : real -> isar_preplay_data -> isar_proof -> isar_proof end; structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS = @@ -95,8 +95,8 @@ (* Precondition: The proof must be labeled canonically (cf. "Slegehammer_Proof.relabel_proof_canonically"). *) -fun compress_proof compress_isar - ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data) proof = +fun compress_isar_proof compress_isar + ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof = if compress_isar <= 1.0 then proof else diff -r 5832470d956e -r dcb36a2540bc src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 16:10:39 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 16:26:43 2014 +0100 @@ -7,12 +7,13 @@ signature SLEDGEHAMMER_ISAR_MINIMIZE = sig - type preplay_data = Sledgehammer_Isar_Preplay.preplay_data type isar_step = Sledgehammer_Isar_Proof.isar_step type isar_proof = Sledgehammer_Isar_Proof.isar_proof + type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data - val minimal_deps_of_step : preplay_data -> isar_step -> isar_step - val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof + val minimize_isar_step_dependencies : isar_preplay_data -> isar_step -> isar_step + val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> + isar_proof end; structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = @@ -24,8 +25,8 @@ val slack = seconds 0.1 -fun minimal_deps_of_step (_ : preplay_data) (step as Let _) = step - | minimal_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} +fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step + | minimize_isar_step_dependencies {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) = (case get_preplay_outcome l of Played time => @@ -46,7 +47,7 @@ end | _ => step (* don't touch steps that time out or fail *)) -fun postprocess_remove_unreferenced_steps postproc_step = +fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = let val add_lfs = fold (Ord_List.insert label_ord) diff -r 5832470d956e -r dcb36a2540bc src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 16:10:39 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 16:26:43 2014 +0100 @@ -14,14 +14,14 @@ val trace : bool Config.T - type preplay_data = + type isar_preplay_data = {get_preplay_outcome: label -> play_outcome, set_preplay_outcome: label -> play_outcome -> unit, preplay_quietly: Time.time -> isar_step -> play_outcome, overall_preplay_outcome: isar_proof -> play_outcome} - val proof_preplay_data : bool -> Proof.context -> string -> string -> bool -> Time.time -> - isar_proof -> preplay_data + val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time -> + isar_proof -> isar_preplay_data end; structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY = @@ -147,7 +147,7 @@ (*** proof preplay interface ***) -type preplay_data = +type isar_preplay_data = {get_preplay_outcome: label -> play_outcome, set_preplay_outcome: label -> play_outcome -> unit, preplay_quietly: Time.time -> isar_step -> play_outcome, @@ -184,14 +184,14 @@ calculation. Precondition: The proof must be labeled canonically; cf. - "Slegehammer_Proof.relabel_proof_canonically". *) -fun proof_preplay_data debug ctxt type_enc lam_trans do_preplay preplay_timeout proof = + "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *) +fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof = if not do_preplay then (* the "dont_preplay" option pretends that everything works just fine *) {get_preplay_outcome = K (Played Time.zeroTime), set_preplay_outcome = K (K ()), preplay_quietly = K (K (Played Time.zeroTime)), - overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_data + overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data else let val ctxt = enrich_context_with_local_facts proof ctxt diff -r 5832470d956e -r dcb36a2540bc src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 16:10:39 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 16:26:43 2014 +0100 @@ -40,11 +40,10 @@ structure Canonical_Label_Tab : TABLE - (** canonical proof labels: 1, 2, 3, ... in postorder **) val canonical_label_ord : (label * label) -> order - val relabel_proof_canonically : isar_proof -> isar_proof + val relabel_isar_proof_canonically : isar_proof -> isar_proof - val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string + val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string end; structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF = @@ -112,14 +111,14 @@ type key = label val ord = canonical_label_ord) -fun relabel_proof_canonically proof = +fun relabel_isar_proof_canonically proof = let 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 handle Option.Option => - raise Fail "Sledgehammer_Isar_Proof: relabel_proof_canonically" + raise Fail "Sledgehammer_Isar_Proof: relabel_isar_proof_canonically" fun do_assm (l, t) state = let @@ -149,7 +148,7 @@ val indent_size = 2 -fun string_of_proof ctxt type_enc lam_trans i n proof = +fun string_of_isar_proof ctxt type_enc lam_trans i n proof = let (* Make sure only type constraints inserted by the type annotation code are printed. *) val ctxt = @@ -183,7 +182,7 @@ fun add_term term (s, ctxt) = (s ^ (term |> singleton (Syntax.uncheck_terms ctxt) - |> annotate_types ctxt + |> annotate_types_in_term ctxt |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of) |> simplify_spaces |> maybe_quote), diff -r 5832470d956e -r dcb36a2540bc src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 16:10:39 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 16:26:43 2014 +0100 @@ -9,9 +9,9 @@ signature SLEDGEHAMMER_ISAR_TRY0 = sig type isar_proof = Sledgehammer_Isar_Proof.isar_proof - type preplay_data = Sledgehammer_Isar_Preplay.preplay_data + type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data - val try0_isar_proof : Time.time -> preplay_data -> isar_proof -> isar_proof + val try0_isar_proof : Time.time -> isar_preplay_data -> isar_proof -> isar_proof end; structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 = @@ -30,7 +30,7 @@ fun try0_step _ _ (step as Let _) = step | try0_step preplay_timeout - ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data) + ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) (step as Prove (_, _, l, _, _, _)) = let val timeout =