# HG changeset patch
# User bulwahn
# Date 1290418927 -3600
# Node ID 0850a2a16dce67fe12f504918fd7a2279193fea5
# Parent  3bba5e71a8731e76c26f4e052fb77d56616b697b
changed old-style quickcheck configurations to new Config.T configurations

diff -r 3bba5e71a873 -r 0850a2a16dce src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Mon Nov 22 10:42:06 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Nov 22 10:42:07 2010 +0100
@@ -391,7 +391,7 @@
   let
     val Ts = (map snd o fst o strip_abs) t;
     val thy = ProofContext.theory_of ctxt
-  in if Quickcheck.report ctxt then
+  in if Config.get ctxt Quickcheck.report then
     let
       val t' = mk_reporting_generator_expr thy t Ts;
       val compile = Code_Runtime.dynamic_value_strict
diff -r 3bba5e71a873 -r 0850a2a16dce src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:06 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:07 2010 +0100
@@ -206,7 +206,7 @@
   let
     val Ts = (map snd o fst o strip_abs) t;
     val thy = ProofContext.theory_of ctxt
-  in if Quickcheck.report ctxt then
+  in if Config.get ctxt Quickcheck.report then
     error "Compilation with reporting facility is not supported"
   else
     let
diff -r 3bba5e71a873 -r 0850a2a16dce src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Nov 22 10:42:06 2010 +0100
+++ b/src/Tools/quickcheck.ML	Mon Nov 22 10:42:07 2010 +0100
@@ -10,18 +10,19 @@
   (* configuration *)
   val auto: bool Unsynchronized.ref
   val timing : bool Unsynchronized.ref
+  val size : int Config.T
+  val iterations : int Config.T
+  val no_assms : bool Config.T
+  val report : bool Config.T
+  val quiet : bool Config.T
+  val timeout : real Config.T
   datatype report = Report of
     { iterations : int, raised_match_errors : int,
       satisfied_assms : int list, positive_concl_tests : int }
-  datatype expectation = No_Expectation | No_Counterexample | Counterexample;
-  datatype test_params = Test_Params of
-  { size: int, iterations: int, default_type: typ list, no_assms: bool,
-    expect : expectation, report: bool, quiet : bool, timeout : real};
+  datatype expectation = No_Expectation | No_Counterexample | Counterexample;  
+  datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
   val test_params_of : Proof.context -> test_params
-  val report : Proof.context -> bool
-  val map_test_params :
-    ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real)))
-      -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real))))
+  val map_test_params : (typ list * expectation -> typ list * expectation)
     -> Context.generic -> Context.generic
   val add_generator:
     string * (Proof.context -> term -> int -> term list option * (bool list * bool))
@@ -80,43 +81,36 @@
   if expect1 = expect2 then expect1 else No_Expectation
 
 (* quickcheck configuration -- default parameters, test generators *)
-
-datatype test_params = Test_Params of
-  { size: int, iterations: int, default_type: typ list, no_assms: bool,
-    expect : expectation, report: bool, quiet : bool, timeout : real};
-
-fun dest_test_params
-    (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
-  ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout))));
+val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
+val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
+val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
+val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
+val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
+val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
 
-fun make_test_params
-    ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))) =
-  Test_Params { size = size, iterations = iterations, default_type = default_type,
-    no_assms = no_assms, expect = expect, report = report, quiet = quiet, timeout = timeout };
+val setup_config =
+  setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
+  
+datatype test_params = Test_Params of
+  {default_type: typ list, expect : expectation};
 
-fun map_test_params' f
-    (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
-  make_test_params
-    (f ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))));
+fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect);
+
+fun make_test_params (default_type, expect) = Test_Params {default_type = default_type, expect = expect};
+
+fun map_test_params' f (Test_Params {default_type, expect}) = make_test_params (f (default_type, expect));
 
 fun merge_test_params
- (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
-    no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1, timeout = timeout1 },
-  Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
-    no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2, timeout = timeout2}) =
-  make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
-    ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
-    ((merge_expectation (expect1, expect2), report1 orelse report2),
-    (quiet1 orelse quiet2, Real.min (timeout1, timeout2)))));
+ (Test_Params {default_type = default_type1, expect = expect1},
+  Test_Params {default_type = default_type2, expect = expect2}) =
+  make_test_params (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
 
 structure Data = Generic_Data
 (
   type T =
     (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
       * test_params;
-  val empty = ([], Test_Params
-    { size = 10, iterations = 100, default_type = [], no_assms = false,
-      expect = No_Expectation, report = false, quiet = false, timeout = 30.0});
+  val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
   val extend = I;
   fun merge ((generators1, params1), (generators2, params2)) : T =
     (AList.merge (op =) (K true) (generators1, generators2),
@@ -125,35 +119,9 @@
 
 val test_params_of = snd o Data.get o Context.Proof;
 
-val size = fst o fst o dest_test_params o test_params_of
-
-val iterations = snd o fst o dest_test_params o test_params_of
-
-val default_type = fst o fst o snd o dest_test_params o test_params_of
-
-val no_assms = snd o fst o snd o dest_test_params o test_params_of
-
-val expect = fst o fst o snd o snd o dest_test_params o test_params_of
-
-val report = snd o fst o snd o snd o dest_test_params o test_params_of
-
-val quiet = fst o snd o snd o snd o dest_test_params o test_params_of
+val default_type = fst o dest_test_params o test_params_of
 
-val timeout = snd o snd o snd o snd o dest_test_params o test_params_of
-
-fun map_report f
-  (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
-    make_test_params
-      ((size, iterations), ((default_type, no_assms), ((expect, f report), (quiet, timeout))));
-
-fun map_quiet f
-  (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
-    make_test_params
-      ((size, iterations), ((default_type, no_assms), ((expect, report), (f quiet, timeout))));
-    
-fun set_report report = Data.map (apsnd (map_report (K report)))
-
-fun set_quiet quiet = Data.map (apsnd (map_quiet (K quiet)))
+val expect = snd o dest_test_params o test_params_of
 
 val map_test_params = Data.map o apsnd o map_test_params'
 
@@ -210,12 +178,13 @@
     val empty_report = Report { iterations = 0, raised_match_errors = 0,
       satisfied_assms = [], positive_concl_tests = 0 }
     fun with_size k timings =
-      if k > size ctxt then (NONE, timings)
+      if k > Config.get ctxt size then (NONE, timings)
       else
          let
-           val _ = if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
+           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 quiet ctxt then ()
+           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
@@ -235,12 +204,13 @@
       "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
     val (testers, comp_time) = cpu_time "quickcheck compilation"
       (fn () => (case generator_name
-       of NONE => if quiet ctxt then mk_testers ctxt t' else mk_testers_strict ctxt t'
+       of NONE => if Config.get ctxt quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
         | SOME name => [mk_tester_select name ctxt t']));
     fun iterate f 0 report = (NONE, report)
       | iterate f j report =
         let
-          val (test_result, single_report) = apsnd Run (f ()) handle Match => (if quiet ctxt then ()
+          val (test_result, single_report) = apsnd Run (f ()) handle Match => 
+            (if Config.get ctxt quiet then ()
              else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
           val report = collect_single_report single_report report
         in
@@ -250,20 +220,20 @@
       satisfied_assms = [], positive_concl_tests = 0 }
     fun with_testers k [] = (NONE, [])
       | with_testers k (tester :: testers) =
-          case iterate (fn () => tester (k - 1)) (iterations ctxt) empty_report
+          case iterate (fn () => tester (k - 1)) (Config.get ctxt iterations) empty_report
            of (NONE, report) => apsnd (cons report) (with_testers k testers)
             | (SOME q, report) => (SOME q, [report]);
     fun with_size k reports =
-      if k > size ctxt then (NONE, reports)
+      if k > Config.get ctxt size then (NONE, reports)
       else
-       (if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
+       (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
         let
           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);
     val ((result, reports), exec_time) =
-      TimeLimit.timeLimit (seconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution"
+      TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => cpu_time "quickcheck execution"
       (fn () => apfst
          (fn result => case result of NONE => NONE
         | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
@@ -271,7 +241,7 @@
         error (excipit "ran out of time")
      | Exn.Interrupt => error (excipit "was interrupted")  (* FIXME violates Isabelle/ML exception model *)
   in
-    (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
+    (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
   end;
 
 exception WELLSORTED of string
@@ -294,7 +264,7 @@
 
 datatype wellsorted_error = Wellsorted_Error of string | Term of term
 
-fun test_goal generator_name insts i state =
+fun test_goal (generator_name, insts) i state =
   let
     val lthy = Proof.context_of state;
     val thy = Proof.theory_of state;
@@ -306,7 +276,7 @@
      of NONE => NONE
       | SOME "" => NONE
       | SOME locale => SOME locale;
-    val assms = if no_assms lthy then [] else case 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));
@@ -322,7 +292,7 @@
       case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
         [] => error error_msg
       | xs => xs
-    val _ = if quiet lthy then () else warning error_msg
+    val _ = if Config.get lthy quiet then () else warning error_msg
     fun collect_results f reports [] = (NONE, rev reports)
       | collect_results f reports (t :: ts) =
         case f t of
@@ -379,8 +349,8 @@
       val ctxt = Proof.context_of state;
       val res =
         state
-        |> Proof.map_context (Context.proof_map (set_report false #> set_quiet true))
-        |> try (test_goal NONE [] 1);
+        |> Proof.map_context (Config.put report false #> Config.put quiet true)
+        |> try (test_goal (NONE, []) 1);
     in
       case res of
         NONE => (false, state)
@@ -390,7 +360,7 @@
     end
 
 val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
-
+  #> setup_config
 
 (* Isar commands *)
 
@@ -413,57 +383,35 @@
   | read_expectation "counterexample" = Counterexample
   | read_expectation s = error ("Not an expectation value: " ^ s)  
 
-fun parse_test_param ctxt ("size", [arg]) =
-      (apfst o apfst o K) (read_nat arg)
-  | parse_test_param ctxt ("iterations", [arg]) =
-      (apfst o apsnd o K) (read_nat arg)
-  | parse_test_param ctxt ("default_type", arg) =
-      (apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg)
-  | parse_test_param ctxt ("no_assms", [arg]) =
-      (apsnd o apfst o apsnd o K) (read_bool arg)
-  | parse_test_param ctxt ("expect", [arg]) =
-      (apsnd o apsnd o apfst o apfst o K) (read_expectation arg)
-  | parse_test_param ctxt ("report", [arg]) =
-      (apsnd o apsnd o apfst o apsnd o K) (read_bool arg)
-  | parse_test_param ctxt ("quiet", [arg]) =
-      (apsnd o apsnd o apsnd o apfst o K) (read_bool arg)
-  | parse_test_param ctxt ("timeout", [arg]) =
-      (apsnd o apsnd o apsnd o apsnd o K) (read_real arg)
-  | parse_test_param ctxt (name, _) =
-      error ("Unknown test parameter: " ^ name);
+fun parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
+  | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
+  | parse_test_param ("default_type", arg) = (fn gen_ctxt =>
+    map_test_params ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)
+  | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg)
+  | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg))
+  | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg)
+  | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
+  | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
+  | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
 
-fun parse_test_param_inst ctxt ("generator", [arg]) =
-      (apsnd o apfst o K o SOME) arg
-  | parse_test_param_inst ctxt (name, arg) =
+fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =
+      (apfst o apfst o K o SOME) arg ((generator, insts), ctxt)
+  | parse_test_param_inst (name, arg) ((generator, insts), ctxt) =
       case try (ProofContext.read_typ ctxt) name
-       of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =))
-              (v, ProofContext.read_typ ctxt (the_single arg))
-        | _ => (apfst o parse_test_param ctxt) (name, arg);
+       of SOME (TFree (v, _)) => (apfst o apsnd o AList.update (op =))
+              (v, ProofContext.read_typ ctxt (the_single arg)) ((generator, insts), ctxt)
+        | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) ((generator, insts), ctxt);
 
-fun quickcheck_params_cmd args thy =
-  let
-    val ctxt = ProofContext.init_global thy
-    val f = fold (parse_test_param ctxt) args;
-  in
-    thy
-    |> (Context.theory_map o map_test_params) f
-  end;
-
+fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
+  
 fun gen_quickcheck args i state =
-  let
-    val ctxt = Proof.context_of state;
-    val default_params = (dest_test_params o snd o Data.get o Context.Proof) ctxt;
-    val f = fold (parse_test_param_inst ctxt) args;
-    val (test_params, (generator_name, insts)) = f (default_params, (NONE, []));
-  in
-    state
-    |> Proof.map_context (Context.proof_map (map_test_params (K test_params)))
-    |> (fn state' => test_goal generator_name insts i state'
-      |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
-                 error ("quickcheck expected to find no counterexample but found one") else ()
-             | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
-                 error ("quickcheck expected to find a counterexample but did not find one") else ()))
-  end;
+  state
+  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ((NONE, []), ctxt))
+  |> (fn ((generator, insts), state') => test_goal (generator, insts) i state'
+  |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
+               error ("quickcheck expected to find no counterexample but found one") else ()
+           | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
+               error ("quickcheck expected to find a counterexample but did not find one") else ()))
 
 fun quickcheck args i state = fst (gen_quickcheck args i state);