# HG changeset patch # User bulwahn # Date 1290422094 -3600 # Node ID 1598ec648b0d5117e9e9ee34669e934b9504ae46 # Parent 6e92ca8e981b653c9c70f40e5d04896b484a869f splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck diff -r 6e92ca8e981b -r 1598ec648b0d src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Mon Nov 22 11:34:53 2010 +0100 +++ b/src/Tools/quickcheck.ML Mon Nov 22 11:34:54 2010 +0100 @@ -16,6 +16,8 @@ val report : bool Config.T val quiet : bool Config.T val timeout : real Config.T + val finite_types : bool Config.T + val finite_type_size : int Config.T datatype report = Report of { iterations : int, raised_match_errors : int, satisfied_assms : int list, positive_concl_tests : int } @@ -32,6 +34,9 @@ (string * term) list option * ((string * int) list * ((int * report list) list) option) val test_term: Proof.context -> string option -> term -> (string * term) list option * ((string * int) list * ((int * report list) list) option) + val test_goal_terms: + Proof.context -> string option * (string * typ) list -> term list + -> (string * term) list option * ((string * int) list * ((int * report list) list) option) list val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option end; @@ -199,6 +204,10 @@ apsnd (rpair NONE) (apfst (Option.map (curry (op ~~) names)) result) end +(* we actually assume we know the generators and its behaviour *) +fun is_iteratable "small" = false + | is_iteratable "random" = true + fun test_term ctxt generator_name t = let val (names, t') = prep_test_term t; @@ -223,15 +232,24 @@ satisfied_assms = [], positive_concl_tests = 0 } fun with_testers k [] = (NONE, []) | with_testers k (tester :: testers) = - case iterate (fn () => tester (k - 1)) (Config.get ctxt iterations) empty_report + let + val niterations = case generator_name of + SOME generator_name => + if is_iteratable generator_name then Config.get ctxt iterations else 1 + | NONE => Config.get ctxt iterations + val (result, timing) = cpu_time ("size " ^ string_of_int k) + (fn () => iterate (fn () => tester (k - 1)) niterations empty_report) + in + case result of (NONE, report) => apsnd (cons report) (with_testers k testers) - | (SOME q, report) => (SOME q, [report]); + | (SOME q, report) => (SOME q, [report]) + end fun with_size k reports = if k > Config.get ctxt size then (NONE, reports) else (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k); let - val _ = current_size := k + val _ = current_size := k val (result, new_report) = with_testers k testers val reports = ((k, new_report) :: reports) in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end); @@ -272,26 +290,9 @@ datatype wellsorted_error = Wellsorted_Error of string | Term of term -fun test_goal (generator_name, insts) i state = +fun test_goal_terms lthy (generator_name, insts) check_goals = let - val lthy = Proof.context_of state; - val thy = Proof.theory_of state; - fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t - | strip t = t; - val {goal = st, ...} = Proof.raw_goal state; - val (gi, frees) = Logic.goal_params (prop_of st) i; - val some_locale = case (Option.map #target o Named_Target.peek) lthy - of NONE => NONE - | SOME "" => NONE - | SOME locale => SOME locale; - val assms = if Config.get lthy no_assms then [] else case some_locale - of NONE => Assumption.all_assms_of lthy - | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy); - val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi)); - val check_goals = case some_locale - of NONE => [proto_goal] - | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) - (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); + val thy = ProofContext.theory_of lthy val inst_goals = if Config.get lthy finite_types then maps (fn check_goal => map (fn T => @@ -314,6 +315,30 @@ | (NONE, report) => collect_results f (report :: reports) ts in collect_results (test_term lthy generator_name) [] correct_inst_goals end; +fun test_goal (generator_name, insts) i state = + let + val lthy = Proof.context_of state; + val thy = Proof.theory_of state; + fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t + | strip t = t; + val {goal = st, ...} = Proof.raw_goal state; + val (gi, frees) = Logic.goal_params (prop_of st) i; + val some_locale = case (Option.map #target o Named_Target.peek) lthy + of NONE => NONE + | SOME "" => NONE + | SOME locale => SOME locale; + val assms = if Config.get lthy no_assms then [] else case some_locale + of NONE => Assumption.all_assms_of lthy + | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy); + val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi)); + val check_goals = case some_locale + of NONE => [proto_goal] + | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) + (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); + in + test_goal_terms lthy (generator_name, insts) check_goals + end + (* pretty printing *) fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck"