# HG changeset patch # User bulwahn # Date 1256630636 -3600 # Node ID 4b13ab778b7824ee8c381b70aa343fe609b46a7a # Parent 5c2af18a32371217027b3c285088d53dced34746 added option show_modes to predicate compiler diff -r 5c2af18a3237 -r 4b13ab778b78 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Oct 27 09:02:22 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Oct 27 09:03:56 2009 +0100 @@ -114,6 +114,7 @@ show_steps = chk "show_steps", show_intermediate_results = chk "show_intermediate_results", show_proof_trace = chk "show_proof_trace", + show_modes = chk "show_modes", show_mode_inference = chk "show_mode_inference", show_compilation = chk "show_compilation", skip_proof = chk "skip_proof", @@ -146,7 +147,7 @@ val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup -val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", +val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"] local structure P = OuterParse diff -r 5c2af18a3237 -r 4b13ab778b78 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Oct 27 09:02:22 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Oct 27 09:03:56 2009 +0100 @@ -135,9 +135,10 @@ datatype options = Options of { expected_modes : (string * int list list) option, show_steps : bool, - show_mode_inference : bool, show_proof_trace : bool, show_intermediate_results : bool, + show_mode_inference : bool, + show_modes : bool, show_compilation : bool, skip_proof : bool, @@ -148,9 +149,10 @@ fun expected_modes (Options opt) = #expected_modes opt fun show_steps (Options opt) = #show_steps opt -fun show_mode_inference (Options opt) = #show_mode_inference opt fun show_intermediate_results (Options opt) = #show_intermediate_results opt fun show_proof_trace (Options opt) = #show_proof_trace opt +fun show_modes (Options opt) = #show_modes opt +fun show_mode_inference (Options opt) = #show_mode_inference opt fun show_compilation (Options opt) = #show_compilation opt fun skip_proof (Options opt) = #skip_proof opt @@ -163,6 +165,7 @@ show_steps = false, show_intermediate_results = false, show_proof_trace = false, + show_modes = false, show_mode_inference = false, show_compilation = false, skip_proof = false, diff -r 5c2af18a3237 -r 4b13ab778b78 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 27 09:02:22 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 27 09:03:56 2009 +0100 @@ -332,10 +332,12 @@ (* diagnostic display functions *) -fun print_modes modes = - Output.tracing ("Inferred modes:\n" ^ - cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map - string_of_mode ms)) modes)); +fun print_modes options modes = + if show_modes options then + Output.tracing ("Inferred modes:\n" ^ + cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map + string_of_mode ms)) modes)) + else () fun print_pred_mode_table string_of_entry thy pred_mode_table = let @@ -2150,7 +2152,7 @@ val moded_clauses = #infer_modes steps options thy extra_modes all_modes param_vs clauses val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses val _ = check_expected_modes options modes - val _ = print_modes modes + val _ = print_modes options modes (*val _ = print_moded_clauses thy moded_clauses*) val _ = print_step options "Defining executable functions..." val thy' = fold (#create_definitions steps preds) modes thy