# HG changeset patch # User nipkow # Date 1319100240 -7200 # Node ID c4fab1099cd0b10ef8426436c93cd5bfad4205d0 # Parent 1b2132017774b9d7bb382f4110cc87c0aac60191# Parent a51a706875174bb4696276530aa1621c2b631b7d merged diff -r a51a70687517 -r c4fab1099cd0 src/HOL/Lazy_Sequence.thy --- a/src/HOL/Lazy_Sequence.thy Thu Oct 20 10:43:47 2011 +0200 +++ b/src/HOL/Lazy_Sequence.thy Thu Oct 20 10:44:00 2011 +0200 @@ -153,7 +153,7 @@ subsubsection {* Small lazy typeclasses *} class small_lazy = - fixes small_lazy :: "int \ 'a Lazy_Sequence.lazy_sequence" + fixes small_lazy :: "code_numeral \ 'a Lazy_Sequence.lazy_sequence" instantiation unit :: small_lazy begin @@ -178,7 +178,7 @@ termination by (relation "measure (%(d, i). nat (d + 1 - i))") auto -definition "small_lazy d = small_lazy' d (- d)" +definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))" instance .. @@ -197,7 +197,7 @@ instantiation list :: (small_lazy) small_lazy begin -fun small_lazy_list :: "int => 'a list Lazy_Sequence.lazy_sequence" +fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence" where "small_lazy_list d = Lazy_Sequence.append (Lazy_Sequence.single []) (if d > 0 then Lazy_Sequence.bind (product (small_lazy (d - 1)) (small_lazy (d - 1))) (%(x, xs). Lazy_Sequence.single (x # xs)) else Lazy_Sequence.empty)" diff -r a51a70687517 -r c4fab1099cd0 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 20 10:43:47 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 20 10:44:00 2011 +0200 @@ -519,14 +519,8 @@ compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns, mk_random = (fn T => fn additional_arguments => - let - val small_lazy = - Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"}, - @{typ "Int.int"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T])) - in - absdummy @{typ code_numeral} (small_lazy $ HOLogic.mk_number @{typ int} 3) - end - ), + Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"}, + @{typ "Code_Numeral.code_numeral"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))), modify_funT = I, additional_arguments = K [], wrap_compilation = K (K (K (K (K I)))) diff -r a51a70687517 -r c4fab1099cd0 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Oct 20 10:43:47 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Oct 20 10:44:00 2011 +0200 @@ -18,10 +18,7 @@ Proof.context -> Proof.context; val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) -> Proof.context -> Proof.context - - val tracing : bool Unsynchronized.ref; - val quiet : bool Unsynchronized.ref; - val test_goals : (Predicate_Compile_Aux.compilation * bool * bool * int) -> + val test_goals : (Predicate_Compile_Aux.compilation * bool * bool) -> Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> Quickcheck.result list val nrandom : int Unsynchronized.ref; @@ -70,10 +67,6 @@ ); val put_new_dseq_result = New_Dseq_Result.put; -val tracing = Unsynchronized.ref false; - -val quiet = Unsynchronized.ref true; - val target = "Quickcheck" val nrandom = Unsynchronized.ref 3; @@ -331,16 +324,22 @@ prog end -fun try_upto quiet f i = +fun try_upto_depth ctxt f = let - fun try' j = - if j <= i then + val max_depth = Config.get ctxt Quickcheck.depth + fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s + fun try' i = + if i <= max_depth then let - val _ = if quiet then () else Output.urgent_message ("Executing depth " ^ string_of_int j) + val _ = message ("Depth: " ^ string_of_int i) + val (result, time) = + cpu_time ("Depth " ^ string_of_int i) (fn () => + f i handle Match => (if Config.get ctxt Quickcheck.quiet then () + else warning "Exception Match raised during quickcheck"; NONE)) + val _ = if Config.get ctxt Quickcheck.timing then + message (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else () in - case f j handle Match => (if quiet then () - else warning "Exception Match raised during quickcheck"; NONE) - of NONE => try' (j + 1) | SOME q => SOME q + case result of NONE => try' (i + 1) | SOME q => SOME q end else NONE @@ -350,35 +349,35 @@ (* quickcheck interface functions *) -fun compile_term' compilation options depth ctxt (t, eval_terms) = +fun compile_term' compilation options ctxt (t, eval_terms) = let val size = Config.get ctxt Quickcheck.size val c = compile_term compilation options ctxt t - val counterexample = try_upto (!quiet) (c size (!nrandom)) depth + val counterexample = try_upto_depth ctxt (c size (!nrandom)) in Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample, evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []} end -fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth = +fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening = let val options = set_fail_safe_function_flattening fail_safe_function_flattening (set_function_flattening function_flattening (get_options ())) in - compile_term' compilation options depth + compile_term' compilation options end fun test_goals options ctxt (limit_time, is_interactive) insts goals = let - val (compilation, function_flattening, fail_safe_function_flattening, depth) = options - val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals + val (compilation, function_flattening, fail_safe_function_flattening) = options + val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals val test_term = - quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth + quickcheck_compile_term compilation function_flattening fail_safe_function_flattening in - Quickcheck.collect_results (test_term ctxt) + Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) [] end @@ -388,11 +387,11 @@ val setup = Context.theory_map (Quickcheck.add_tester ("predicate_compile_wo_ff", - (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, false, true, 4)))) + (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, false, true)))) #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_fs", - (ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true, 4)))) + (ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true)))) #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_nofs", - (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true, 4)))) + (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true)))) end; diff -r a51a70687517 -r c4fab1099cd0 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu Oct 20 10:43:47 2011 +0200 +++ b/src/Tools/quickcheck.ML Thu Oct 20 10:44:00 2011 +0200 @@ -16,6 +16,7 @@ val batch_tester : string Config.T val size : int Config.T val iterations : int Config.T + val depth : int Config.T val no_assms : bool Config.T val report : bool Config.T val timing : bool Config.T @@ -163,6 +164,8 @@ val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "") val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10) val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100) +val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10) + val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false) val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true) val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false) @@ -397,6 +400,7 @@ fun parse_test_param ("tester", args) = fold parse_tester args | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg)) | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg)) + | parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg)) | parse_test_param ("default_type", arg) = (fn (testers, gen_ctxt) => (testers, map_test_params ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))