# HG changeset patch
# User bulwahn
# Date 1284043437 -7200
# Node ID 8f176e575a49ba46c22e54d55565ab53a902c56f
# Parent  548a3e5521ab5611473ea79576221dfac76757a5
changing the container for the quickcheck options to a generic data

diff -r 548a3e5521ab -r 8f176e575a49 src/HOL/Library/Predicate_Compile_Quickcheck.thy
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Thu Sep 09 14:38:14 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Thu Sep 09 16:43:57 2010 +0200
@@ -7,11 +7,11 @@
 uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
 begin
 
-setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
-  Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_fs",
-  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs",
-  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
+  Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4)) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_fs",
+  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4)) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_nofs",
+  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4)) *}
 
 end
\ No newline at end of file
diff -r 548a3e5521ab -r 8f176e575a49 src/HOL/Library/SML_Quickcheck.thy
--- a/src/HOL/Library/SML_Quickcheck.thy	Thu Sep 09 14:38:14 2010 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy	Thu Sep 09 16:43:57 2010 +0200
@@ -7,7 +7,7 @@
 
 setup {*
   Inductive_Codegen.quickcheck_setup #>
-  Quickcheck.add_generator ("SML", Codegen.test_term)
+  Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term))
 *}
 
 end
diff -r 548a3e5521ab -r 8f176e575a49 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Sep 09 14:38:14 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Sep 09 16:43:57 2010 +0200
@@ -853,6 +853,6 @@
   setup_depth_start #>
   setup_random_values #>
   setup_size_offset #>
-  Quickcheck.add_generator ("SML_inductive", test_term);
+  Context.theory_map (Quickcheck.add_generator ("SML_inductive", test_term));
 
 end;
diff -r 548a3e5521ab -r 8f176e575a49 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 09 14:38:14 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 09 16:43:57 2010 +0200
@@ -404,6 +404,7 @@
 val setup =
   Datatype.interpretation ensure_random_datatype
   #> Code_Target.extend_target (target, (Code_Eval.target, K I))
-  #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of);
+  #> Context.theory_map
+    (Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of));
 
 end;
diff -r 548a3e5521ab -r 8f176e575a49 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Sep 09 14:38:14 2010 +0200
+++ b/src/Tools/quickcheck.ML	Thu Sep 09 16:43:57 2010 +0200
@@ -17,10 +17,10 @@
   datatype test_params = Test_Params of
   { size: int, iterations: int, default_type: typ list, no_assms: bool,
     expect : expectation, report: bool, quiet : bool};
-  val test_params_of: theory -> test_params 
+  val test_params_of: Proof.context -> test_params 
   val add_generator:
     string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
-      -> theory -> theory
+      -> Context.generic -> Context.generic
   (* testing terms and proof states *)
   val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term ->
     (string * term) list option * ((string * int) list * ((int * report list) list) option)
@@ -99,7 +99,7 @@
     ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
     ((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2)));
 
-structure Data = Theory_Data
+structure Data = Generic_Data
 (
   type T =
     (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
@@ -113,24 +113,24 @@
       merge_test_params (params1, params2));
 );
 
-val test_params_of = snd o Data.get;
+val test_params_of = snd o Data.get o Context.Proof;
 
 val add_generator = Data.map o apfst o AList.update (op =);
 
 (* generating tests *)
 
 fun mk_tester_select name ctxt =
-  case AList.lookup (op =) ((fst o Data.get o ProofContext.theory_of) ctxt) name
+  case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name
    of NONE => error ("No such quickcheck generator: " ^ name)
     | SOME generator => generator ctxt;
 
 fun mk_testers ctxt report t =
-  (map snd o fst o Data.get o ProofContext.theory_of) ctxt
+  (map snd o fst o Data.get o Context.Proof) ctxt
   |> map_filter (fn generator => try (generator ctxt report) t);
 
 fun mk_testers_strict ctxt report t =
   let
-    val generators = ((map snd o fst o Data.get o ProofContext.theory_of) ctxt)
+    val generators = ((map snd o fst o Data.get  o Context.Proof) ctxt)
     val testers = map (fn generator => Exn.capture (generator ctxt report) t) generators;
   in if forall (is_none o Exn.get_result) testers
     then [(Exn.release o snd o split_last) testers]
@@ -296,7 +296,7 @@
     let
       val ctxt = Proof.context_of state;
       val Test_Params {size, iterations, default_type, no_assms, ...} =
-        (snd o Data.get o Proof.theory_of) state;
+        (snd o Data.get o Context.Proof) ctxt;
       val res =
         try (test_goal true false NONE size iterations default_type no_assms [] 1) state;
     in
@@ -353,18 +353,17 @@
 
 fun quickcheck_params_cmd args thy =
   let
-    val ctxt = ProofContext.init_global thy;
+    val ctxt = ProofContext.init_global thy
     val f = fold (parse_test_param ctxt) args;
   in
     thy
-    |> (Data.map o apsnd o map_test_params) f
+    |> (Context.theory_map o Data.map o apsnd o map_test_params) f
   end;
 
 fun gen_quickcheck args i state =
   let
-    val thy = Proof.theory_of state;
     val ctxt = Proof.context_of state;
-    val default_params = (dest_test_params o snd o Data.get) thy;
+    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 (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) =
       f (default_params, (NONE, []));