1.1 --- a/src/HOL/Library/SML_Quickcheck.thy	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/Library/SML_Quickcheck.thy	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -6,9 +6,8 @@
     1.4  begin
     1.5  
     1.6  setup {*
     1.7 -  Inductive_Codegen.quickcheck_setup #>
     1.8 -  Context.theory_map (Quickcheck.add_generator ("SML",
     1.9 -    fn ctxt => fn [(t, eval_terms)] =>
    1.10 +  let
    1.11 +    fun compile_generator_expr ctxt [(t, eval_terms)] =
    1.12        let
    1.13          val prop = list_abs_free (Term.add_frees t [], t)
    1.14          val test_fun = Codegen.test_term ctxt prop
    1.15 @@ -22,8 +21,13 @@
    1.16                in
    1.17                  case result of NONE => iterate size (j - 1) | SOME q => SOME q
    1.18                end
    1.19 -     in fn [_, size] => (iterate size iterations, NONE) end))
    1.20 -  #> Context.theory_map (Quickcheck.add_tester ("SML", Quickcheck.generator_test_goal_terms))  
    1.21 +      in fn [_, size] => (iterate size iterations, NONE) end))
    1.22 +    val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr
    1.23 +  in
    1.24 +    Inductive_Codegen.quickcheck_setup
    1.25 +    #> Context.theory_map (Quickcheck.add_generator ("SML", compile_generator_expr))
    1.26 +    #> Context.theory_map (Quickcheck.add_tester ("SML", test_goals))
    1.27 +  end
    1.28  *}
    1.29  
    1.30  end

     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 18 10:34:21 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 18 10:34:21 2011 +0200
     2.3 @@ -488,7 +488,7 @@
     2.4        thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
     2.5    end;
     2.6  
     2.7 -val test_goals = Quickcheck.generator_test_goal_terms;
     2.8 +val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr;
     2.9    
    2.10  (* setup *)
    2.11  

     3.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 18 10:34:21 2011 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 18 10:34:21 2011 +0200
     3.3 @@ -438,7 +438,7 @@
     3.4        end
     3.5    end;
     3.6  
     3.7 -val test_goals = Quickcheck.generator_test_goal_terms;
     3.8 +val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr;
     3.9    
    3.10  (** setup **)
    3.11  

     4.1 --- a/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
     4.2 +++ b/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
     4.3 @@ -56,17 +56,18 @@
     4.4      string * (Proof.context -> term list -> (int -> bool) list)
     4.5        -> Context.generic -> Context.generic
     4.6    (* basic operations *)
     4.7 +  type compile_generator =
     4.8 +    Proof.context -> (term * term list) list -> int list -> term list option * report option
     4.9    val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a  
    4.10    val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
    4.11      -> (typ option * (term * term list)) list list
    4.12    val collect_results: ('a -> result) -> 'a list -> result list -> result list
    4.13 -  val generator_test_goal_terms: Proof.context -> bool * bool -> (string * typ) list ->
    4.14 -    (term * term list) list -> result list
    4.15 +  val generator_test_goal_terms: compile_generator ->
    4.16 +    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
    4.17    (* testing terms and proof states *)
    4.18 -  val test_term: Proof.context -> bool * bool -> term * term list -> result
    4.19 +  val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result
    4.20    val test_goal_terms:
    4.21 -    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list  
    4.22 -      -> result list
    4.23 +    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
    4.24    val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
    4.25    (* testing a batch of terms *)
    4.26    val test_terms:
    4.27 @@ -246,9 +247,10 @@
    4.28          | SOME tester => SOME tester
    4.29        end
    4.30    end
    4.31 -
    4.32 +(*
    4.33  val mk_tester =
    4.34    gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o fst o Data.get o Context.Proof) ctxt))
    4.35 +*)
    4.36  val mk_batch_tester =
    4.37    gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
    4.38  val mk_batch_validator =
    4.39 @@ -259,6 +261,9 @@
    4.40  
    4.41  (* testing propositions *)
    4.42  
    4.43 +type compile_generator =
    4.44 +  Proof.context -> (term * term list) list -> int list -> term list option * report option
    4.45 +
    4.46  fun check_test_term t =
    4.47    let
    4.48      val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    4.49 @@ -279,7 +284,7 @@
    4.50    else
    4.51      f ()
    4.52  
    4.53 -fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
    4.54 +fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) =
    4.55    let
    4.56      fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
    4.57      val _ = check_test_term t
    4.58 @@ -306,21 +311,14 @@
    4.59      limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
    4.60        let
    4.61          val (test_fun, comp_time) = cpu_time "quickcheck compilation"
    4.62 -          (fn () => mk_tester ctxt [(t, eval_terms)]);
    4.63 +          (fn () => compile ctxt [(t, eval_terms)]);
    4.64          val _ = add_timing comp_time current_result
    4.65 -      in
    4.66 -        case test_fun of NONE => !current_result
    4.67 -          | SOME test_fun =>
    4.68 -            let
    4.69 -              val (response, exec_time) =
    4.70 -                cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
    4.71 -              val _ = add_response names eval_terms response current_result
    4.72 -              val _ = add_timing exec_time current_result
    4.73 -            in
    4.74 -              !current_result
    4.75 -            end
    4.76 -       end)
    4.77 -     (fn () => (message (excipit ()); !current_result)) ()
    4.78 +        val (response, exec_time) =
    4.79 +          cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
    4.80 +        val _ = add_response names eval_terms response current_result
    4.81 +        val _ = add_timing exec_time current_result
    4.82 +      in !current_result end)
    4.83 +    (fn () => (message (excipit ()); !current_result)) ()
    4.84    end;
    4.85  
    4.86  fun validate_terms ctxt ts =
    4.87 @@ -361,7 +359,7 @@
    4.88  (* FIXME: this function shows that many assumptions are made upon the generation *)
    4.89  (* In the end there is probably no generic quickcheck interface left... *)
    4.90  
    4.91 -fun test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) ts =
    4.92 +fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts =
    4.93    let
    4.94      val thy = Proof_Context.theory_of ctxt
    4.95      fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
    4.96 @@ -390,18 +388,12 @@
    4.97    in
    4.98      limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
    4.99        let
   4.100 -        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt ts)
   4.101 -        val _ = add_timing comp_time current_result
   4.102 -      in
   4.103 -        case test_fun of
   4.104 -          NONE => !current_result
   4.105 -        | SOME test_fun =>
   4.106 -          let
   4.107 -            val _ = case get_first (test_card_size test_fun) enumeration_card_size of
   4.108 -              SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
   4.109 -            | NONE => ()
   4.110 -          in !current_result end
   4.111 -      end)
   4.112 +        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts)
   4.113 +        val _ = add_timing comp_time current_result     
   4.114 +        val _ = case get_first (test_card_size test_fun) enumeration_card_size of
   4.115 +          SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
   4.116 +        | NONE => ()
   4.117 +      in !current_result end)
   4.118        (fn () => (message "Quickcheck ran out of time"; !current_result)) ()
   4.119    end
   4.120  
   4.121 @@ -471,18 +463,18 @@
   4.122          collect_results f ts (result :: results)
   4.123      end  
   4.124  
   4.125 -fun generator_test_goal_terms ctxt (limit_time, is_interactive) insts goals =
   4.126 +fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals =
   4.127    let
   4.128      fun test_term' goal =
   4.129        case goal of
   4.130 -        [(NONE, t)] => test_term ctxt (limit_time, is_interactive) t
   4.131 -      | ts => test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) (map snd ts)
   4.132 +        [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t
   4.133 +      | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts)
   4.134      val correct_inst_goals = instantiate_goals ctxt insts goals
   4.135    in
   4.136      if Config.get ctxt finite_types then
   4.137        collect_results test_term' correct_inst_goals []
   4.138      else
   4.139 -      collect_results (test_term ctxt (limit_time, is_interactive))
   4.140 +      collect_results (test_term compile ctxt (limit_time, is_interactive))
   4.141          (maps (map snd) correct_inst_goals) []
   4.142    end;
   4.143