# HG changeset patch # User bulwahn # Date 1291362047 -3600 # Node ID 508c838273647e7e7feaea182cebb4de077bb978 # Parent e006d1e069207f5172a56a36b1b079a63a8901f7 removed dead test_term_small function in quickcheck diff -r e006d1e06920 -r 508c83827364 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Dec 03 08:40:47 2010 +0100 +++ b/src/Tools/quickcheck.ML Fri Dec 03 08:40:47 2010 +0100 @@ -173,35 +173,6 @@ val time = Time.toMilliseconds (#cpu (end_timing start)) in (Exn.release result, (description, time)) end -fun test_term_small ctxt t = - let - val (names, t') = prep_test_term t; - val current_size = Unsynchronized.ref 0 - fun excipit s = - "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size) - val (tester, comp_time) = cpu_time "compilation" - (fn () => the (AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) "small") ctxt t'); - val empty_report = Report { iterations = 0, raised_match_errors = 0, - satisfied_assms = [], positive_concl_tests = 0 } - fun with_size k timings = - if k > Config.get ctxt size then (NONE, timings) - else - let - val _ = if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k); - val _ = current_size := k - val (result, timing) = cpu_time ("size " ^ string_of_int k) - (fn () => (fst (tester k)) handle Match => (if Config.get ctxt quiet then () - else warning "Exception Match raised during quickcheck"; NONE)) - in - case result of - NONE => with_size (k + 1) (timing :: timings) - | SOME q => (SOME q, (timing :: timings)) - end; - val result = with_size 1 [comp_time] - in - apsnd (rpair NONE) (apfst (Option.map (curry (op ~~) names)) result) - end - (* we actually assume we know the generators and its behaviour *) fun is_iteratable "SML" = true | is_iteratable "random" = true