# HG changeset patch # User bulwahn # Date 1271844652 -7200 # Node ID d1d9dee7a4bf20a0152bb43c933ceaa78731d8c2 # Parent f8b3381e14378fe6904dba99458684c8ae2d7f97 adopting quickcheck diff -r f8b3381e1437 -r d1d9dee7a4bf src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Apr 21 12:10:52 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Apr 21 12:10:52 2010 +0200 @@ -68,6 +68,8 @@ skip_proof = false, compilation = Random, inductify = true, + specialise = true, + detect_switches = false, function_flattening = true, fail_safe_function_flattening = false, no_higher_order_predicate = [], @@ -88,6 +90,8 @@ skip_proof = false, compilation = Random, inductify = true, + specialise = true, + detect_switches = false, function_flattening = true, fail_safe_function_flattening = false, no_higher_order_predicate = [], @@ -99,13 +103,13 @@ (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, - compilation = c, inductify = i, function_flattening = f_f, + compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, no_topmost_reordering = re}) = (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, - compilation = c, inductify = i, function_flattening = b, + compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b, fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, no_topmost_reordering = re}) @@ -113,13 +117,13 @@ (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, - compilation = c, inductify = i, function_flattening = f_f, + compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, no_topmost_reordering = re}) = (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, - compilation = c, inductify = i, function_flattening = f_f, + compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, fail_safe_function_flattening = b, no_higher_order_predicate = no_ho, no_topmost_reordering = re}) @@ -127,13 +131,13 @@ (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, - compilation = c, inductify = i, function_flattening = f_f, + compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, no_topmost_reordering = re}) = (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p, - compilation = c, inductify = i, function_flattening = f_f, + compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re}) @@ -198,7 +202,7 @@ val tac = fn _ => Skip_Proof.cheat_tac thy1 val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 - val (thy3, preproc_time) = cpu_time "predicate preprocessing" + val (thy3, preproc_time) = cpu_time "predicate preprocessing" (fn () => Predicate_Compile.preprocess options const thy2) val (thy4, core_comp_time) = cpu_time "random_dseq core compilation" (fn () => @@ -209,7 +213,9 @@ Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3 (*| Depth_Limited_Random => Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*)) - val _ = Predicate_Compile_Core.print_all_modes compilation thy4 + (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*) + val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time)) + val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time)) val modes = Predicate_Compile_Core.modes_of compilation thy4 full_constname val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool val prog = @@ -228,7 +234,6 @@ Const (name, T) end else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes)) - val qc_term = case compilation of Pos_Random_DSeq => mk_bind (prog,