# HG changeset patch # User bulwahn # Date 1318839541 -7200 # Node ID 3f1d1ce024cb17072501209173993f53ef2b06ae # Parent efc2e2d80218cb2f0595a867a8f457dc06a60cbe moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms diff -r efc2e2d80218 -r 3f1d1ce024cb src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Sun Oct 16 21:49:47 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle.ML Mon Oct 17 10:19:01 2011 +0200 @@ -496,7 +496,7 @@ val ctxt' = Proof_Context.init_global thy |> Config.put Quickcheck.size 1 |> Config.put Quickcheck.iterations 1 - val test = Quickcheck.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false) + val test = Quickcheck_Common.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false) in case try test (preprocess thy insts (prop_of th), []) of SOME _ => (Output.urgent_message "executable"; true) diff -r efc2e2d80218 -r 3f1d1ce024cb src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Sun Oct 16 21:49:47 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Oct 17 10:19:01 2011 +0200 @@ -122,8 +122,11 @@ TimeLimit.timeLimit (seconds (!Try.auto_time_limit)) (fn _ => let - val SOME [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy)) - (false, false) [] [(t, [])] + val ctxt' = change_options (Proof_Context.init_global thy) + val [result] = case Quickcheck.active_testers ctxt' of + [] => error "No active testers for quickcheck" + | [tester] => tester ctxt' (false, false) [] [(t, [])] + | _ => error "Multiple active testers for quickcheck" in case Quickcheck.counterexample_of result of NONE => (NoCex, Quickcheck.timings_of result) @@ -317,11 +320,12 @@ val ctxt = Proof_Context.init_global thy in can (TimeLimit.timeLimit (seconds 2.0) - (Quickcheck.test_goal_terms + (Quickcheck.test_terms ((Config.put Quickcheck.finite_types true #> Config.put Quickcheck.finite_type_size 1 #> Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt) - (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt))) + (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy) + (fst (Variable.import_terms true [t] ctxt))) end fun is_executable_thm thy th = is_executable_term thy (prop_of th) diff -r efc2e2d80218 -r 3f1d1ce024cb src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Sun Oct 16 21:49:47 2011 +0200 +++ b/src/HOL/Quickcheck.thy Mon Oct 17 10:19:01 2011 +0200 @@ -144,6 +144,12 @@ no_notation fcomp (infixl "\>" 60) no_notation scomp (infixl "\\" 60) +subsection {* Tester SML-inductive based on the SML code generator *} + +setup {* + Context.theory_map (Quickcheck.add_tester ("SML_inductive", + (Inductive_Codegen.active, Quickcheck_Common.generator_test_goal_terms Inductive_Codegen.test_term))); +*} subsection {* The Random-Predicate Monad *} diff -r efc2e2d80218 -r 3f1d1ce024cb src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sun Oct 16 21:49:47 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Oct 17 10:19:01 2011 +0200 @@ -488,7 +488,7 @@ thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') [] end; -val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr; +val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr; (* setup *) diff -r efc2e2d80218 -r 3f1d1ce024cb src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Oct 16 21:49:47 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Oct 17 10:19:01 2011 +0200 @@ -462,9 +462,9 @@ fun test_goals ctxt (limit_time, is_interactive) insts goals = if (not (getenv "ISABELLE_GHC" = "")) then let - val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals + val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals in - Quickcheck.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) [] + Quickcheck_Common.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) [] end else (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message diff -r efc2e2d80218 -r 3f1d1ce024cb src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sun Oct 16 21:49:47 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Oct 17 10:19:01 2011 +0200 @@ -11,6 +11,13 @@ -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list -> (string * sort -> string * sort) option + val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list + -> (typ option * (term * term list)) list list + val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list + type compile_generator = + Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option + val generator_test_goal_terms : compile_generator -> Proof.context -> bool * bool + -> (string * typ) list -> (term * term list) list -> Quickcheck.result list val ensure_sort_datatype: ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory) @@ -20,6 +27,7 @@ -> Proof.context -> (term * term list) list -> term val mk_fun_upd : typ -> typ -> term * term -> term -> term val post_process_term : term -> term + val test_term : compile_generator -> Proof.context -> bool * bool -> term * term list -> Quickcheck.result end; structure Quickcheck_Common : QUICKCHECK_COMMON = @@ -35,7 +43,222 @@ | strip_imp A = ([], A) fun mk_undefined T = Const(@{const_name undefined}, T) + +(* testing functions: testing with increasing sizes (and cardinalities) *) + +type compile_generator = + Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option + +fun check_test_term t = + let + val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse + error "Term to be tested contains type variables"; + val _ = null (Term.add_vars t []) orelse + error "Term to be tested contains schematic variables"; + in () end + +fun cpu_time description e = + let val ({cpu, ...}, result) = Timing.timing e () + in (result, (description, Time.toMilliseconds cpu)) end + +fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) = + let + val _ = check_test_term t + val names = Term.add_free_names t [] + val current_size = Unsynchronized.ref 0 + val current_result = Unsynchronized.ref Quickcheck.empty_result + fun excipit () = + "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size) + fun with_size test_fun k = + if k > Config.get ctxt Quickcheck.size then + NONE + else + let + val _ = Quickcheck.message ctxt ("Test data size: " ^ string_of_int k) + val _ = current_size := k + val ((result, report), timing) = + cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1]) + val _ = Quickcheck.add_timing timing current_result + val _ = Quickcheck.add_report k report current_result + in + case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q + end; + in + (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( + let + val (test_fun, comp_time) = cpu_time "quickcheck compilation" + (fn () => compile ctxt [(t, eval_terms)]); + val _ = Quickcheck.add_timing comp_time current_result + val (response, exec_time) = + cpu_time "quickcheck execution" (fn () => with_size test_fun 1) + val _ = Quickcheck.add_response names eval_terms response current_result + val _ = Quickcheck.add_timing exec_time current_result + in !current_result end) +(* (fn () => (message (excipit ()); !current_result)) ()*) + end; + +fun validate_terms ctxt ts = + let + val _ = map check_test_term ts + val size = Config.get ctxt Quickcheck.size + val (test_funs, comp_time) = cpu_time "quickcheck batch compilation" + (fn () => Quickcheck.mk_batch_validator ctxt ts) + fun with_size tester k = + if k > size then true + else if tester k then with_size tester (k + 1) else false + val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => + Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) + (fn () => with_size test_fun 1) () + handle TimeLimit.TimeOut => true)) test_funs) + in + (results, [comp_time, exec_time]) + end +fun test_terms ctxt ts = + let + val _ = map check_test_term ts + val size = Config.get ctxt Quickcheck.size + val namess = map (fn t => Term.add_free_names t []) ts + val (test_funs, comp_time) = + cpu_time "quickcheck batch compilation" (fn () => Quickcheck.mk_batch_tester ctxt ts) + fun with_size tester k = + if k > size then NONE + else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1) + val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => + Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) + (fn () => with_size test_fun 1) () + handle TimeLimit.TimeOut => NONE)) test_funs) + in + (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results, + [comp_time, exec_time]) + end + + +fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts = + let + val thy = Proof_Context.theory_of ctxt + val (ts', eval_terms) = split_list ts + val _ = map check_test_term ts' + val names = Term.add_free_names (hd ts') [] + val Ts = map snd (Term.add_frees (hd ts') []) + val current_result = Unsynchronized.ref Quickcheck.empty_result + fun test_card_size test_fun (card, size) = + (* FIXME: why decrement size by one? *) + let + val (ts, timing) = + cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card) + (fn () => fst (test_fun [card, size - 1])) + val _ = Quickcheck.add_timing timing current_result + in + Option.map (pair card) ts + end + val enumeration_card_size = + if forall (fn T => Sign.of_sort thy (T, ["Enum.enum"])) Ts then + (* size does not matter *) + map (rpair 0) (1 upto (length ts)) + else + (* size does matter *) + map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size)) + |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) + in + (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( + let + val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts) + val _ = Quickcheck.add_timing comp_time current_result + val _ = case get_first (test_card_size test_fun) enumeration_card_size of + SOME (card, ts) => Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME ts) current_result + | NONE => () + in !current_result end) + (*(fn () => (message "Quickcheck ran out of time"; !current_result)) ()*) + end + +fun get_finite_types ctxt = + fst (chop (Config.get ctxt Quickcheck.finite_type_size) + (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3", + "Enum.finite_4", "Enum.finite_5"])) + +exception WELLSORTED of string + +fun monomorphic_term thy insts default_T = + let + fun subst (T as TFree (v, S)) = + let + val T' = AList.lookup (op =) insts v + |> the_default default_T + in if Sign.of_sort thy (T', S) then T' + else raise (WELLSORTED ("For instantiation with default_type " ^ + Syntax.string_of_typ_global thy default_T ^ + ":\n" ^ Syntax.string_of_typ_global thy T' ^ + " to be substituted for variable " ^ + Syntax.string_of_typ_global thy T ^ " does not have sort " ^ + Syntax.string_of_sort_global thy S)) + end + | subst T = T; + in (map_types o map_atyps) subst end; + +datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list + +fun instantiate_goals lthy insts goals = + let + fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) + val thy = Proof_Context.theory_of lthy + val default_insts = + if Config.get lthy Quickcheck.finite_types then (get_finite_types lthy) else (Quickcheck.default_type lthy) + val inst_goals = + map (fn (check_goal, eval_terms) => + if not (null (Term.add_tfree_names check_goal [])) then + map (fn T => + (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy)) + (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms)) + handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts + else + [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals + val error_msg = + cat_lines + (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) + fun is_wellsorted_term (T, Term t) = SOME (T, t) + | is_wellsorted_term (_, Wellsorted_Error s) = NONE + val correct_inst_goals = + case map (map_filter is_wellsorted_term) inst_goals of + [[]] => error error_msg + | xs => xs + val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg + in + correct_inst_goals + end + +fun collect_results f [] results = results + | collect_results f (t :: ts) results = + let + val result = f t + in + if Quickcheck.found_counterexample result then + (result :: results) + else + collect_results f ts (result :: results) + end + +fun add_equation_eval_terms (t, eval_terms) = + case try HOLogic.dest_eq (snd (strip_imp t)) of + SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs]) + | NONE => (t, eval_terms) + +fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals = + let + fun test_term' goal = + case goal of + [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t + | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts) + val goals' = instantiate_goals ctxt insts goals + |> map (map (apsnd add_equation_eval_terms)) + in + if Config.get ctxt Quickcheck.finite_types then + collect_results test_term' goals' [] + else + collect_results (test_term compile ctxt (limit_time, is_interactive)) + (maps (map snd) goals') [] + end; + (* defining functions *) fun pat_completeness_auto ctxt = diff -r efc2e2d80218 -r 3f1d1ce024cb src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Sun Oct 16 21:49:47 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Oct 17 10:19:01 2011 +0200 @@ -438,7 +438,7 @@ end end; -val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr; +val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr; (** setup **) diff -r efc2e2d80218 -r 3f1d1ce024cb src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Sun Oct 16 21:49:47 2011 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Mon Oct 17 10:19:01 2011 +0200 @@ -10,8 +10,8 @@ val poke_test_fn: (int * int * int -> term list option) -> unit val test_term: Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option + val active : bool Config.T val setup: theory -> theory - val quickcheck_setup: theory -> theory end; structure Inductive_Codegen : INDUCTIVE_CODEGEN = @@ -862,12 +862,12 @@ NONE => deepen bound f (i + 1) | SOME x => SOME x); -val active = Attrib.setup_config_bool @{binding quickcheck_inductive_SML_active} (K false); +val active = Attrib.setup_config_bool @{binding quickcheck_SML_inductive_active} (K false); -val depth_bound = Attrib.setup_config_int @{binding ind_quickcheck_depth} (K 10); -val depth_start = Attrib.setup_config_int @{binding ind_quickcheck_depth_start} (K 1); -val random_values = Attrib.setup_config_int @{binding ind_quickcheck_random} (K 5); -val size_offset = Attrib.setup_config_int @{binding ind_quickcheck_size_offset} (K 0); +val depth_bound = Attrib.setup_config_int @{binding quickcheck_ind_depth} (K 10); +val depth_start = Attrib.setup_config_int @{binding quickcheck_ind_depth_start} (K 1); +val random_values = Attrib.setup_config_int @{binding quickcheck_ind_random} (K 5); +val size_offset = Attrib.setup_config_int @{binding quickcheck_ind_size_offset} (K 0); fun test_term ctxt [(t, [])] = let @@ -926,9 +926,4 @@ | test_term ctxt _ = error "Compilation of multiple instances is not supported by tester SML_inductive"; -val test_goal = Quickcheck.generator_test_goal_terms test_term; - -val quickcheck_setup = - Context.theory_map (Quickcheck.add_tester ("SML_inductive", (active, test_goal))); - end; diff -r efc2e2d80218 -r 3f1d1ce024cb src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Sun Oct 16 21:49:47 2011 +0200 +++ b/src/Tools/quickcheck.ML Mon Oct 17 10:19:01 2011 +0200 @@ -29,6 +29,7 @@ val test_params_of : Proof.context -> test_params val map_test_params : (typ list * expectation -> typ list * expectation) -> Context.generic -> Context.generic + val default_type : Proof.context -> typ list datatype report = Report of { iterations : int, raised_match_errors : int, satisfied_assms : int list, positive_concl_tests : int } @@ -40,7 +41,10 @@ timings : (string * int) list, reports : (int * report) list} val empty_result : result + val found_counterexample : result -> bool val add_timing : (string * int) -> result Unsynchronized.ref -> unit + val add_response : string list -> term list -> term list option -> result Unsynchronized.ref -> unit + val add_report : int -> report option -> result Unsynchronized.ref -> unit val counterexample_of : result -> (string * term) list option val timings_of : result -> (string * int) list (* registering testers & generators *) @@ -54,23 +58,15 @@ string * (Proof.context -> term list -> (int -> bool) list) -> Context.generic -> Context.generic (* basic operations *) - type compile_generator = - Proof.context -> (term * term list) list -> int list -> term list option * report option - val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a - val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list - -> (typ option * (term * term list)) list list - val collect_results : ('a -> result) -> 'a list -> result list -> result list - val generator_test_goal_terms : compile_generator -> - Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list + val message : Proof.context -> string -> unit + val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a (* testing terms and proof states *) - val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result - val test_goal_terms : + val mk_batch_validator : Proof.context -> term list -> (int -> bool) list option + val mk_batch_tester : Proof.context -> term list -> (int -> term list option) list option + val active_testers : Proof.context -> tester list + val test_terms : Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option - (* testing a batch of terms *) - val test_terms: - Proof.context -> term list -> (string * term) list option list option * (string * int) list - val validate_terms: Proof.context -> term list -> bool list option * (string * int) list end; structure Quickcheck : QUICKCHECK = @@ -119,14 +115,15 @@ fun timings_of (Result r) = #timings r -fun set_reponse names eval_terms (SOME ts) (Result r) = +fun set_response names eval_terms (SOME ts) (Result r) = let val (ts1, ts2) = chop (length names) ts + val (eval_terms', _) = chop (length ts2) eval_terms in - Result {counterexample = SOME (names ~~ ts1), evaluation_terms = SOME (eval_terms ~~ ts2), + Result {counterexample = SOME (names ~~ ts1), evaluation_terms = SOME (eval_terms' ~~ ts2), timings = #timings r, reports = #reports r} end - | set_reponse _ _ NONE result = result + | set_response _ _ NONE result = result fun set_counterexample counterexample (Result r) = @@ -153,7 +150,7 @@ Unsynchronized.change result_ref (cons_report size report) fun add_response names eval_terms response result_ref = - Unsynchronized.change result_ref (set_reponse names eval_terms response) + Unsynchronized.change result_ref (set_response names eval_terms response) (* expectation *) @@ -275,18 +272,6 @@ type compile_generator = Proof.context -> (term * term list) list -> int list -> term list option * report option -fun check_test_term t = - let - val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse - error "Term to be tested contains type variables"; - val _ = null (Term.add_vars t []) orelse - error "Term to be tested contains schematic variables"; - in () end - -fun cpu_time description e = - let val ({cpu, ...}, result) = Timing.timing e () - in (result, (description, Time.toMilliseconds cpu)) end - fun limit timeout (limit_time, is_interactive) f exc () = if limit_time then TimeLimit.timeLimit timeout f () @@ -295,205 +280,9 @@ else f () -fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) = - let - fun message s = if Config.get ctxt quiet then () else Output.urgent_message s - val _ = check_test_term t - val names = Term.add_free_names t [] - val current_size = Unsynchronized.ref 0 - val current_result = Unsynchronized.ref empty_result - fun excipit () = - "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size) - fun with_size test_fun k = - if k > Config.get ctxt size then - NONE - else - let - val _ = message ("Test data size: " ^ string_of_int k) - val _ = current_size := k - val ((result, report), timing) = - cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1]) - val _ = add_timing timing current_result - val _ = add_report k report current_result - in - case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q - end; - in - (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( - let - val (test_fun, comp_time) = cpu_time "quickcheck compilation" - (fn () => compile ctxt [(t, eval_terms)]); - val _ = add_timing comp_time current_result - val (response, exec_time) = - cpu_time "quickcheck execution" (fn () => with_size test_fun 1) - val _ = add_response names eval_terms response current_result - val _ = add_timing exec_time current_result - in !current_result end) -(* (fn () => (message (excipit ()); !current_result)) ()*) - end; - -fun validate_terms ctxt ts = - let - val _ = map check_test_term ts - val size = Config.get ctxt size - val (test_funs, comp_time) = cpu_time "quickcheck batch compilation" - (fn () => mk_batch_validator ctxt ts) - fun with_size tester k = - if k > size then true - else if tester k then with_size tester (k + 1) else false - val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => - Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) - (fn () => with_size test_fun 1) () - handle TimeLimit.TimeOut => true)) test_funs) - in - (results, [comp_time, exec_time]) - end - -fun test_terms ctxt ts = - let - val _ = map check_test_term ts - val size = Config.get ctxt size - val namess = map (fn t => Term.add_free_names t []) ts - val (test_funs, comp_time) = - cpu_time "quickcheck batch compilation" (fn () => mk_batch_tester ctxt ts) - fun with_size tester k = - if k > size then NONE - else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1) - val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => - Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) - (fn () => with_size test_fun 1) () - handle TimeLimit.TimeOut => NONE)) test_funs) - in - (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results, - [comp_time, exec_time]) - end - -(* FIXME: this function shows that many assumptions are made upon the generation *) -(* In the end there is probably no generic quickcheck interface left... *) - -fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts = - let - val thy = Proof_Context.theory_of ctxt - fun message s = if Config.get ctxt quiet then () else Output.urgent_message s - val (ts', eval_terms) = split_list ts - val _ = map check_test_term ts' - val names = Term.add_free_names (hd ts') [] - val Ts = map snd (Term.add_frees (hd ts') []) - val current_result = Unsynchronized.ref empty_result - fun test_card_size test_fun (card, size) = - (* FIXME: why decrement size by one? *) - let - val (ts, timing) = - cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card) - (fn () => fst (test_fun [card, size - 1])) - val _ = add_timing timing current_result - in - Option.map (pair card) ts - end - val enumeration_card_size = - if forall (fn T => Sign.of_sort thy (T, ["Enum.enum"])) Ts then - (* size does not matter *) - map (rpair 0) (1 upto (length ts)) - else - (* size does matter *) - map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size)) - |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) - in - (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( - let - val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts) - val _ = add_timing comp_time current_result - val _ = case get_first (test_card_size test_fun) enumeration_card_size of - SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result - | NONE => () - in !current_result end) - (*(fn () => (message "Quickcheck ran out of time"; !current_result)) ()*) - end - -fun get_finite_types ctxt = - fst (chop (Config.get ctxt finite_type_size) - (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3", - "Enum.finite_4", "Enum.finite_5"])) - -exception WELLSORTED of string - -fun monomorphic_term thy insts default_T = - let - fun subst (T as TFree (v, S)) = - let - val T' = AList.lookup (op =) insts v - |> the_default default_T - in if Sign.of_sort thy (T', S) then T' - else raise (WELLSORTED ("For instantiation with default_type " ^ - Syntax.string_of_typ_global thy default_T ^ - ":\n" ^ Syntax.string_of_typ_global thy T' ^ - " to be substituted for variable " ^ - Syntax.string_of_typ_global thy T ^ " does not have sort " ^ - Syntax.string_of_sort_global thy S)) - end - | subst T = T; - in (map_types o map_atyps) subst end; - -datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list - -fun instantiate_goals lthy insts goals = - let - fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) - val thy = Proof_Context.theory_of lthy - val default_insts = - if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy) - val inst_goals = - map (fn (check_goal, eval_terms) => - if not (null (Term.add_tfree_names check_goal [])) then - map (fn T => - (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy)) - (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms)) - handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts - else - [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals - val error_msg = - cat_lines - (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) - fun is_wellsorted_term (T, Term t) = SOME (T, t) - | is_wellsorted_term (_, Wellsorted_Error s) = NONE - val correct_inst_goals = - case map (map_filter is_wellsorted_term) inst_goals of - [[]] => error error_msg - | xs => xs - val _ = if Config.get lthy quiet then () else warning error_msg - in - correct_inst_goals - end - -fun collect_results f [] results = results - | collect_results f (t :: ts) results = - let - val result = f t - in - if found_counterexample result then - (result :: results) - else - collect_results f ts (result :: results) - end - -fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals = - let - fun test_term' goal = - case goal of - [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t - | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts) - val correct_inst_goals = instantiate_goals ctxt insts goals - in - if Config.get ctxt finite_types then - collect_results test_term' correct_inst_goals [] - else - collect_results (test_term compile ctxt (limit_time, is_interactive)) - (maps (map snd) correct_inst_goals) [] - end; - fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s -fun test_goal_terms ctxt (limit_time, is_interactive) insts goals = +fun test_terms ctxt (limit_time, is_interactive) insts goals = case active_testers ctxt of [] => error "No active testers for quickcheck" | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) @@ -524,7 +313,7 @@ map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms)) (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); in - test_goal_terms lthy (time_limit, is_interactive) insts goals + test_terms lthy (time_limit, is_interactive) insts goals end (* pretty printing *) @@ -537,7 +326,7 @@ map (fn (s, t) => Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex)) @ (if null eval_terms then [] - else (Pretty.str ("Evaluated terms:\n") :: + else (Pretty.fbrk :: Pretty.str ("Evaluated terms:") :: map (fn (t, u) => Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u]) (rev eval_terms))));