changed old-style quickcheck configurations to new Config.T configurations
authorbulwahn
Mon Nov 22 10:42:07 2010 +0100 (2010-11-22)
changeset 406440850a2a16dce
parent 40643 3bba5e71a873
child 40645 03ce94672ee6
changed old-style quickcheck configurations to new Config.T configurations
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/smallvalue_generators.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Mon Nov 22 10:42:06 2010 +0100
     1.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Nov 22 10:42:07 2010 +0100
     1.3 @@ -391,7 +391,7 @@
     1.4    let
     1.5      val Ts = (map snd o fst o strip_abs) t;
     1.6      val thy = ProofContext.theory_of ctxt
     1.7 -  in if Quickcheck.report ctxt then
     1.8 +  in if Config.get ctxt Quickcheck.report then
     1.9      let
    1.10        val t' = mk_reporting_generator_expr thy t Ts;
    1.11        val compile = Code_Runtime.dynamic_value_strict
     2.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:06 2010 +0100
     2.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:07 2010 +0100
     2.3 @@ -206,7 +206,7 @@
     2.4    let
     2.5      val Ts = (map snd o fst o strip_abs) t;
     2.6      val thy = ProofContext.theory_of ctxt
     2.7 -  in if Quickcheck.report ctxt then
     2.8 +  in if Config.get ctxt Quickcheck.report then
     2.9      error "Compilation with reporting facility is not supported"
    2.10    else
    2.11      let
     3.1 --- a/src/Tools/quickcheck.ML	Mon Nov 22 10:42:06 2010 +0100
     3.2 +++ b/src/Tools/quickcheck.ML	Mon Nov 22 10:42:07 2010 +0100
     3.3 @@ -10,18 +10,19 @@
     3.4    (* configuration *)
     3.5    val auto: bool Unsynchronized.ref
     3.6    val timing : bool Unsynchronized.ref
     3.7 +  val size : int Config.T
     3.8 +  val iterations : int Config.T
     3.9 +  val no_assms : bool Config.T
    3.10 +  val report : bool Config.T
    3.11 +  val quiet : bool Config.T
    3.12 +  val timeout : real Config.T
    3.13    datatype report = Report of
    3.14      { iterations : int, raised_match_errors : int,
    3.15        satisfied_assms : int list, positive_concl_tests : int }
    3.16 -  datatype expectation = No_Expectation | No_Counterexample | Counterexample;
    3.17 -  datatype test_params = Test_Params of
    3.18 -  { size: int, iterations: int, default_type: typ list, no_assms: bool,
    3.19 -    expect : expectation, report: bool, quiet : bool, timeout : real};
    3.20 +  datatype expectation = No_Expectation | No_Counterexample | Counterexample;  
    3.21 +  datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
    3.22    val test_params_of : Proof.context -> test_params
    3.23 -  val report : Proof.context -> bool
    3.24 -  val map_test_params :
    3.25 -    ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real)))
    3.26 -      -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real))))
    3.27 +  val map_test_params : (typ list * expectation -> typ list * expectation)
    3.28      -> Context.generic -> Context.generic
    3.29    val add_generator:
    3.30      string * (Proof.context -> term -> int -> term list option * (bool list * bool))
    3.31 @@ -80,43 +81,36 @@
    3.32    if expect1 = expect2 then expect1 else No_Expectation
    3.33  
    3.34  (* quickcheck configuration -- default parameters, test generators *)
    3.35 -
    3.36 -datatype test_params = Test_Params of
    3.37 -  { size: int, iterations: int, default_type: typ list, no_assms: bool,
    3.38 -    expect : expectation, report: bool, quiet : bool, timeout : real};
    3.39 -
    3.40 -fun dest_test_params
    3.41 -    (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
    3.42 -  ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout))));
    3.43 +val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
    3.44 +val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
    3.45 +val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
    3.46 +val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
    3.47 +val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
    3.48 +val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
    3.49  
    3.50 -fun make_test_params
    3.51 -    ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))) =
    3.52 -  Test_Params { size = size, iterations = iterations, default_type = default_type,
    3.53 -    no_assms = no_assms, expect = expect, report = report, quiet = quiet, timeout = timeout };
    3.54 +val setup_config =
    3.55 +  setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
    3.56 +  
    3.57 +datatype test_params = Test_Params of
    3.58 +  {default_type: typ list, expect : expectation};
    3.59  
    3.60 -fun map_test_params' f
    3.61 -    (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
    3.62 -  make_test_params
    3.63 -    (f ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))));
    3.64 +fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect);
    3.65 +
    3.66 +fun make_test_params (default_type, expect) = Test_Params {default_type = default_type, expect = expect};
    3.67 +
    3.68 +fun map_test_params' f (Test_Params {default_type, expect}) = make_test_params (f (default_type, expect));
    3.69  
    3.70  fun merge_test_params
    3.71 - (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
    3.72 -    no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1, timeout = timeout1 },
    3.73 -  Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
    3.74 -    no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2, timeout = timeout2}) =
    3.75 -  make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    3.76 -    ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
    3.77 -    ((merge_expectation (expect1, expect2), report1 orelse report2),
    3.78 -    (quiet1 orelse quiet2, Real.min (timeout1, timeout2)))));
    3.79 + (Test_Params {default_type = default_type1, expect = expect1},
    3.80 +  Test_Params {default_type = default_type2, expect = expect2}) =
    3.81 +  make_test_params (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
    3.82  
    3.83  structure Data = Generic_Data
    3.84  (
    3.85    type T =
    3.86      (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
    3.87        * test_params;
    3.88 -  val empty = ([], Test_Params
    3.89 -    { size = 10, iterations = 100, default_type = [], no_assms = false,
    3.90 -      expect = No_Expectation, report = false, quiet = false, timeout = 30.0});
    3.91 +  val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
    3.92    val extend = I;
    3.93    fun merge ((generators1, params1), (generators2, params2)) : T =
    3.94      (AList.merge (op =) (K true) (generators1, generators2),
    3.95 @@ -125,35 +119,9 @@
    3.96  
    3.97  val test_params_of = snd o Data.get o Context.Proof;
    3.98  
    3.99 -val size = fst o fst o dest_test_params o test_params_of
   3.100 -
   3.101 -val iterations = snd o fst o dest_test_params o test_params_of
   3.102 -
   3.103 -val default_type = fst o fst o snd o dest_test_params o test_params_of
   3.104 -
   3.105 -val no_assms = snd o fst o snd o dest_test_params o test_params_of
   3.106 -
   3.107 -val expect = fst o fst o snd o snd o dest_test_params o test_params_of
   3.108 -
   3.109 -val report = snd o fst o snd o snd o dest_test_params o test_params_of
   3.110 -
   3.111 -val quiet = fst o snd o snd o snd o dest_test_params o test_params_of
   3.112 +val default_type = fst o dest_test_params o test_params_of
   3.113  
   3.114 -val timeout = snd o snd o snd o snd o dest_test_params o test_params_of
   3.115 -
   3.116 -fun map_report f
   3.117 -  (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
   3.118 -    make_test_params
   3.119 -      ((size, iterations), ((default_type, no_assms), ((expect, f report), (quiet, timeout))));
   3.120 -
   3.121 -fun map_quiet f
   3.122 -  (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
   3.123 -    make_test_params
   3.124 -      ((size, iterations), ((default_type, no_assms), ((expect, report), (f quiet, timeout))));
   3.125 -    
   3.126 -fun set_report report = Data.map (apsnd (map_report (K report)))
   3.127 -
   3.128 -fun set_quiet quiet = Data.map (apsnd (map_quiet (K quiet)))
   3.129 +val expect = snd o dest_test_params o test_params_of
   3.130  
   3.131  val map_test_params = Data.map o apsnd o map_test_params'
   3.132  
   3.133 @@ -210,12 +178,13 @@
   3.134      val empty_report = Report { iterations = 0, raised_match_errors = 0,
   3.135        satisfied_assms = [], positive_concl_tests = 0 }
   3.136      fun with_size k timings =
   3.137 -      if k > size ctxt then (NONE, timings)
   3.138 +      if k > Config.get ctxt size then (NONE, timings)
   3.139        else
   3.140           let
   3.141 -           val _ = if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
   3.142 +           val _ = if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
   3.143             val _ = current_size := k
   3.144 -           val (result, timing) = cpu_time ("size " ^ string_of_int k) (fn () => (fst (tester k)) handle Match => (if quiet ctxt then ()
   3.145 +           val (result, timing) = cpu_time ("size " ^ string_of_int k)
   3.146 +             (fn () => (fst (tester k)) handle Match => (if Config.get ctxt quiet then ()
   3.147               else warning "Exception Match raised during quickcheck"; NONE))
   3.148          in
   3.149            case result of
   3.150 @@ -235,12 +204,13 @@
   3.151        "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
   3.152      val (testers, comp_time) = cpu_time "quickcheck compilation"
   3.153        (fn () => (case generator_name
   3.154 -       of NONE => if quiet ctxt then mk_testers ctxt t' else mk_testers_strict ctxt t'
   3.155 +       of NONE => if Config.get ctxt quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
   3.156          | SOME name => [mk_tester_select name ctxt t']));
   3.157      fun iterate f 0 report = (NONE, report)
   3.158        | iterate f j report =
   3.159          let
   3.160 -          val (test_result, single_report) = apsnd Run (f ()) handle Match => (if quiet ctxt then ()
   3.161 +          val (test_result, single_report) = apsnd Run (f ()) handle Match => 
   3.162 +            (if Config.get ctxt quiet then ()
   3.163               else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
   3.164            val report = collect_single_report single_report report
   3.165          in
   3.166 @@ -250,20 +220,20 @@
   3.167        satisfied_assms = [], positive_concl_tests = 0 }
   3.168      fun with_testers k [] = (NONE, [])
   3.169        | with_testers k (tester :: testers) =
   3.170 -          case iterate (fn () => tester (k - 1)) (iterations ctxt) empty_report
   3.171 +          case iterate (fn () => tester (k - 1)) (Config.get ctxt iterations) empty_report
   3.172             of (NONE, report) => apsnd (cons report) (with_testers k testers)
   3.173              | (SOME q, report) => (SOME q, [report]);
   3.174      fun with_size k reports =
   3.175 -      if k > size ctxt then (NONE, reports)
   3.176 +      if k > Config.get ctxt size then (NONE, reports)
   3.177        else
   3.178 -       (if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
   3.179 +       (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
   3.180          let
   3.181            val _ = current_size := k  
   3.182            val (result, new_report) = with_testers k testers
   3.183            val reports = ((k, new_report) :: reports)
   3.184          in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
   3.185      val ((result, reports), exec_time) =
   3.186 -      TimeLimit.timeLimit (seconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution"
   3.187 +      TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => cpu_time "quickcheck execution"
   3.188        (fn () => apfst
   3.189           (fn result => case result of NONE => NONE
   3.190          | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
   3.191 @@ -271,7 +241,7 @@
   3.192          error (excipit "ran out of time")
   3.193       | Exn.Interrupt => error (excipit "was interrupted")  (* FIXME violates Isabelle/ML exception model *)
   3.194    in
   3.195 -    (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
   3.196 +    (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
   3.197    end;
   3.198  
   3.199  exception WELLSORTED of string
   3.200 @@ -294,7 +264,7 @@
   3.201  
   3.202  datatype wellsorted_error = Wellsorted_Error of string | Term of term
   3.203  
   3.204 -fun test_goal generator_name insts i state =
   3.205 +fun test_goal (generator_name, insts) i state =
   3.206    let
   3.207      val lthy = Proof.context_of state;
   3.208      val thy = Proof.theory_of state;
   3.209 @@ -306,7 +276,7 @@
   3.210       of NONE => NONE
   3.211        | SOME "" => NONE
   3.212        | SOME locale => SOME locale;
   3.213 -    val assms = if no_assms lthy then [] else case some_locale
   3.214 +    val assms = if Config.get lthy no_assms then [] else case some_locale
   3.215       of NONE => Assumption.all_assms_of lthy
   3.216        | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
   3.217      val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
   3.218 @@ -322,7 +292,7 @@
   3.219        case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
   3.220          [] => error error_msg
   3.221        | xs => xs
   3.222 -    val _ = if quiet lthy then () else warning error_msg
   3.223 +    val _ = if Config.get lthy quiet then () else warning error_msg
   3.224      fun collect_results f reports [] = (NONE, rev reports)
   3.225        | collect_results f reports (t :: ts) =
   3.226          case f t of
   3.227 @@ -379,8 +349,8 @@
   3.228        val ctxt = Proof.context_of state;
   3.229        val res =
   3.230          state
   3.231 -        |> Proof.map_context (Context.proof_map (set_report false #> set_quiet true))
   3.232 -        |> try (test_goal NONE [] 1);
   3.233 +        |> Proof.map_context (Config.put report false #> Config.put quiet true)
   3.234 +        |> try (test_goal (NONE, []) 1);
   3.235      in
   3.236        case res of
   3.237          NONE => (false, state)
   3.238 @@ -390,7 +360,7 @@
   3.239      end
   3.240  
   3.241  val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
   3.242 -
   3.243 +  #> setup_config
   3.244  
   3.245  (* Isar commands *)
   3.246  
   3.247 @@ -413,57 +383,35 @@
   3.248    | read_expectation "counterexample" = Counterexample
   3.249    | read_expectation s = error ("Not an expectation value: " ^ s)  
   3.250  
   3.251 -fun parse_test_param ctxt ("size", [arg]) =
   3.252 -      (apfst o apfst o K) (read_nat arg)
   3.253 -  | parse_test_param ctxt ("iterations", [arg]) =
   3.254 -      (apfst o apsnd o K) (read_nat arg)
   3.255 -  | parse_test_param ctxt ("default_type", arg) =
   3.256 -      (apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg)
   3.257 -  | parse_test_param ctxt ("no_assms", [arg]) =
   3.258 -      (apsnd o apfst o apsnd o K) (read_bool arg)
   3.259 -  | parse_test_param ctxt ("expect", [arg]) =
   3.260 -      (apsnd o apsnd o apfst o apfst o K) (read_expectation arg)
   3.261 -  | parse_test_param ctxt ("report", [arg]) =
   3.262 -      (apsnd o apsnd o apfst o apsnd o K) (read_bool arg)
   3.263 -  | parse_test_param ctxt ("quiet", [arg]) =
   3.264 -      (apsnd o apsnd o apsnd o apfst o K) (read_bool arg)
   3.265 -  | parse_test_param ctxt ("timeout", [arg]) =
   3.266 -      (apsnd o apsnd o apsnd o apsnd o K) (read_real arg)
   3.267 -  | parse_test_param ctxt (name, _) =
   3.268 -      error ("Unknown test parameter: " ^ name);
   3.269 +fun parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
   3.270 +  | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
   3.271 +  | parse_test_param ("default_type", arg) = (fn gen_ctxt =>
   3.272 +    map_test_params ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)
   3.273 +  | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg)
   3.274 +  | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg))
   3.275 +  | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg)
   3.276 +  | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
   3.277 +  | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
   3.278 +  | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
   3.279  
   3.280 -fun parse_test_param_inst ctxt ("generator", [arg]) =
   3.281 -      (apsnd o apfst o K o SOME) arg
   3.282 -  | parse_test_param_inst ctxt (name, arg) =
   3.283 +fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =
   3.284 +      (apfst o apfst o K o SOME) arg ((generator, insts), ctxt)
   3.285 +  | parse_test_param_inst (name, arg) ((generator, insts), ctxt) =
   3.286        case try (ProofContext.read_typ ctxt) name
   3.287 -       of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =))
   3.288 -              (v, ProofContext.read_typ ctxt (the_single arg))
   3.289 -        | _ => (apfst o parse_test_param ctxt) (name, arg);
   3.290 +       of SOME (TFree (v, _)) => (apfst o apsnd o AList.update (op =))
   3.291 +              (v, ProofContext.read_typ ctxt (the_single arg)) ((generator, insts), ctxt)
   3.292 +        | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) ((generator, insts), ctxt);
   3.293  
   3.294 -fun quickcheck_params_cmd args thy =
   3.295 -  let
   3.296 -    val ctxt = ProofContext.init_global thy
   3.297 -    val f = fold (parse_test_param ctxt) args;
   3.298 -  in
   3.299 -    thy
   3.300 -    |> (Context.theory_map o map_test_params) f
   3.301 -  end;
   3.302 -
   3.303 +fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
   3.304 +  
   3.305  fun gen_quickcheck args i state =
   3.306 -  let
   3.307 -    val ctxt = Proof.context_of state;
   3.308 -    val default_params = (dest_test_params o snd o Data.get o Context.Proof) ctxt;
   3.309 -    val f = fold (parse_test_param_inst ctxt) args;
   3.310 -    val (test_params, (generator_name, insts)) = f (default_params, (NONE, []));
   3.311 -  in
   3.312 -    state
   3.313 -    |> Proof.map_context (Context.proof_map (map_test_params (K test_params)))
   3.314 -    |> (fn state' => test_goal generator_name insts i state'
   3.315 -      |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
   3.316 -                 error ("quickcheck expected to find no counterexample but found one") else ()
   3.317 -             | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
   3.318 -                 error ("quickcheck expected to find a counterexample but did not find one") else ()))
   3.319 -  end;
   3.320 +  state
   3.321 +  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ((NONE, []), ctxt))
   3.322 +  |> (fn ((generator, insts), state') => test_goal (generator, insts) i state'
   3.323 +  |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
   3.324 +               error ("quickcheck expected to find no counterexample but found one") else ()
   3.325 +           | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
   3.326 +               error ("quickcheck expected to find a counterexample but did not find one") else ()))
   3.327  
   3.328  fun quickcheck args i state = fst (gen_quickcheck args i state);
   3.329