# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 2fef4f9429f79947870bd0f2c468d8050281e7f4 # Parent 5378e61add1a1fd4d0ebe4699c8bb1abdd47bbeb added option show_intermediate_results diff -r 5378e61add1a -r 2fef4f9429f7 src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200 @@ -112,7 +112,7 @@ (*check_modes : (string * int list list) list,*) show_steps : bool, show_mode_inference : bool, - + show_intermediate_results : bool, (* inductify_functions : bool, *) @@ -120,13 +120,16 @@ rpred : bool }; -fun is_show_steps (Options opt) = #show_steps opt +fun show_steps (Options opt) = #show_steps opt +fun show_intermediate_results (Options opt) = #show_intermediate_results opt + fun is_inductify (Options opt) = #inductify opt fun is_rpred (Options opt) = #rpred opt val default_options = Options { show_steps = false, + show_intermediate_results = false, show_mode_inference = false, inductify = false, rpred = false @@ -134,7 +137,7 @@ fun print_step options s = - if is_show_steps options then tracing s else () + if show_steps options then tracing s else () (* tuple processing *) diff -r 5378e61add1a -r 2fef4f9429f7 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 @@ -26,11 +26,13 @@ fun tracing s = () -fun print_intross thy msg intross = - tracing (msg ^ +fun print_intross options thy msg intross = + if show_intermediate_results options then + Output.tracing (msg ^ (space_implode "; " (map (fn intros => commas (map (Display.string_of_thm_global thy) intros)) intross))) - + else () + fun print_specs thy specs = map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs @@ -41,7 +43,7 @@ val specs = map (apsnd (map (fn th => if is_equationlike th then Pred_Compile_Data.normalize_equation thy' th else th))) specs val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy') - val _ = print_intross thy'' "Flattened introduction rules: " intross1 + val _ = print_intross options thy'' "Flattened introduction rules: " intross1 val _ = "Replacing functions in introrules..." val intross2 = if fail_safe_mode then @@ -49,7 +51,7 @@ SOME intross => intross | NONE => let val _ = warning "Function replacement failed!" in intross1 end else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 - val _ = print_intross thy'' "Introduction rules with replaced functions: " intross2 + val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2 val _ = print_step options "Introducing new constants for abstractions at higher-order argument positions..." val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'') val (new_intross, thy'''') = @@ -77,12 +79,12 @@ val _ = print_specs thy' fun_pred_specs val specs = (get_specs prednames) @ fun_pred_specs val (intross3, thy''') = process_specification options specs thy' - val _ = print_intross thy''' "Introduction rules with new constants: " intross3 + val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 val intross4 = map (maps remove_pointless_clauses) intross3 - val _ = print_intross thy''' "After removing pointless clauses: " intross4 + val _ = print_intross options thy''' "After removing pointless clauses: " intross4 val intross5 = map (map (AxClass.overload thy''')) intross4 val intross6 = burrow (map (expand_tuples thy''')) intross5 - val _ = print_intross thy''' "introduction rules before registering: " intross6 + val _ = print_intross options thy''' "introduction rules before registering: " intross6 val _ = print_step options "Registering introduction rules..." val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' in @@ -105,6 +107,7 @@ in Options { show_steps = chk "show_steps", + show_intermediate_results = chk "show_intermediate_results", show_mode_inference = chk "show_mode_inference", inductify = chk "inductify", rpred = chk "rpred" @@ -135,7 +138,7 @@ val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup -val bool_options = ["show_steps", "show_mode_inference", "inductify", "rpred"] +val bool_options = ["show_steps", "show_intermediate_results", "show_mode_inference", "inductify", "rpred"] val _ = List.app OuterKeyword.keyword ("mode" :: bool_options)