changing the container for the quickcheck options to a generic data
authorbulwahn
Thu Sep 09 16:43:57 2010 +0200 (2010-09-09)
changeset 392528f176e575a49
parent 39250 548a3e5521ab
child 39253 0c47d615a69b
changing the container for the quickcheck options to a generic data
src/HOL/Library/Predicate_Compile_Quickcheck.thy
src/HOL/Library/SML_Quickcheck.thy
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/quickcheck_generators.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Thu Sep 09 14:38:14 2010 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Thu Sep 09 16:43:57 2010 +0200
     1.3 @@ -7,11 +7,11 @@
     1.4  uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
     1.5  begin
     1.6  
     1.7 -setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
     1.8 -  Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4) *}
     1.9 -setup {* Quickcheck.add_generator ("predicate_compile_ff_fs",
    1.10 -  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4) *}
    1.11 -setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs",
    1.12 -  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4) *}
    1.13 +setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
    1.14 +  Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4)) *}
    1.15 +setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_fs",
    1.16 +  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4)) *}
    1.17 +setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_nofs",
    1.18 +  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4)) *}
    1.19  
    1.20  end
    1.21 \ No newline at end of file
     2.1 --- a/src/HOL/Library/SML_Quickcheck.thy	Thu Sep 09 14:38:14 2010 +0200
     2.2 +++ b/src/HOL/Library/SML_Quickcheck.thy	Thu Sep 09 16:43:57 2010 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  setup {*
     2.6    Inductive_Codegen.quickcheck_setup #>
     2.7 -  Quickcheck.add_generator ("SML", Codegen.test_term)
     2.8 +  Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term))
     2.9  *}
    2.10  
    2.11  end
     3.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Sep 09 14:38:14 2010 +0200
     3.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Sep 09 16:43:57 2010 +0200
     3.3 @@ -853,6 +853,6 @@
     3.4    setup_depth_start #>
     3.5    setup_random_values #>
     3.6    setup_size_offset #>
     3.7 -  Quickcheck.add_generator ("SML_inductive", test_term);
     3.8 +  Context.theory_map (Quickcheck.add_generator ("SML_inductive", test_term));
     3.9  
    3.10  end;
     4.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 09 14:38:14 2010 +0200
     4.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 09 16:43:57 2010 +0200
     4.3 @@ -404,6 +404,7 @@
     4.4  val setup =
     4.5    Datatype.interpretation ensure_random_datatype
     4.6    #> Code_Target.extend_target (target, (Code_Eval.target, K I))
     4.7 -  #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of);
     4.8 +  #> Context.theory_map
     4.9 +    (Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of));
    4.10  
    4.11  end;
     5.1 --- a/src/Tools/quickcheck.ML	Thu Sep 09 14:38:14 2010 +0200
     5.2 +++ b/src/Tools/quickcheck.ML	Thu Sep 09 16:43:57 2010 +0200
     5.3 @@ -17,10 +17,10 @@
     5.4    datatype test_params = Test_Params of
     5.5    { size: int, iterations: int, default_type: typ list, no_assms: bool,
     5.6      expect : expectation, report: bool, quiet : bool};
     5.7 -  val test_params_of: theory -> test_params 
     5.8 +  val test_params_of: Proof.context -> test_params 
     5.9    val add_generator:
    5.10      string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
    5.11 -      -> theory -> theory
    5.12 +      -> Context.generic -> Context.generic
    5.13    (* testing terms and proof states *)
    5.14    val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term ->
    5.15      (string * term) list option * ((string * int) list * ((int * report list) list) option)
    5.16 @@ -99,7 +99,7 @@
    5.17      ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
    5.18      ((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2)));
    5.19  
    5.20 -structure Data = Theory_Data
    5.21 +structure Data = Generic_Data
    5.22  (
    5.23    type T =
    5.24      (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
    5.25 @@ -113,24 +113,24 @@
    5.26        merge_test_params (params1, params2));
    5.27  );
    5.28  
    5.29 -val test_params_of = snd o Data.get;
    5.30 +val test_params_of = snd o Data.get o Context.Proof;
    5.31  
    5.32  val add_generator = Data.map o apfst o AList.update (op =);
    5.33  
    5.34  (* generating tests *)
    5.35  
    5.36  fun mk_tester_select name ctxt =
    5.37 -  case AList.lookup (op =) ((fst o Data.get o ProofContext.theory_of) ctxt) name
    5.38 +  case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name
    5.39     of NONE => error ("No such quickcheck generator: " ^ name)
    5.40      | SOME generator => generator ctxt;
    5.41  
    5.42  fun mk_testers ctxt report t =
    5.43 -  (map snd o fst o Data.get o ProofContext.theory_of) ctxt
    5.44 +  (map snd o fst o Data.get o Context.Proof) ctxt
    5.45    |> map_filter (fn generator => try (generator ctxt report) t);
    5.46  
    5.47  fun mk_testers_strict ctxt report t =
    5.48    let
    5.49 -    val generators = ((map snd o fst o Data.get o ProofContext.theory_of) ctxt)
    5.50 +    val generators = ((map snd o fst o Data.get  o Context.Proof) ctxt)
    5.51      val testers = map (fn generator => Exn.capture (generator ctxt report) t) generators;
    5.52    in if forall (is_none o Exn.get_result) testers
    5.53      then [(Exn.release o snd o split_last) testers]
    5.54 @@ -296,7 +296,7 @@
    5.55      let
    5.56        val ctxt = Proof.context_of state;
    5.57        val Test_Params {size, iterations, default_type, no_assms, ...} =
    5.58 -        (snd o Data.get o Proof.theory_of) state;
    5.59 +        (snd o Data.get o Context.Proof) ctxt;
    5.60        val res =
    5.61          try (test_goal true false NONE size iterations default_type no_assms [] 1) state;
    5.62      in
    5.63 @@ -353,18 +353,17 @@
    5.64  
    5.65  fun quickcheck_params_cmd args thy =
    5.66    let
    5.67 -    val ctxt = ProofContext.init_global thy;
    5.68 +    val ctxt = ProofContext.init_global thy
    5.69      val f = fold (parse_test_param ctxt) args;
    5.70    in
    5.71      thy
    5.72 -    |> (Data.map o apsnd o map_test_params) f
    5.73 +    |> (Context.theory_map o Data.map o apsnd o map_test_params) f
    5.74    end;
    5.75  
    5.76  fun gen_quickcheck args i state =
    5.77    let
    5.78 -    val thy = Proof.theory_of state;
    5.79      val ctxt = Proof.context_of state;
    5.80 -    val default_params = (dest_test_params o snd o Data.get) thy;
    5.81 +    val default_params = (dest_test_params o snd o Data.get o Context.Proof) ctxt;
    5.82      val f = fold (parse_test_param_inst ctxt) args;
    5.83      val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) =
    5.84        f (default_params, (NONE, []));