1.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Sun Oct 16 21:49:47 2011 +0200
     1.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Oct 17 10:19:01 2011 +0200
     1.3 @@ -496,7 +496,7 @@
     1.4      val ctxt' = Proof_Context.init_global thy
     1.5        |> Config.put Quickcheck.size 1
     1.6        |> Config.put Quickcheck.iterations 1
     1.7 -    val test = Quickcheck.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false)
     1.8 +    val test = Quickcheck_Common.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false)
     1.9    in  
    1.10      case try test (preprocess thy insts (prop_of th), []) of
    1.11        SOME _ => (Output.urgent_message "executable"; true)

     2.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Oct 16 21:49:47 2011 +0200
     2.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Oct 17 10:19:01 2011 +0200
     2.3 @@ -122,8 +122,11 @@
     2.4    TimeLimit.timeLimit (seconds (!Try.auto_time_limit))
     2.5        (fn _ =>
     2.6            let
     2.7 -            val SOME [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy))
     2.8 -              (false, false) [] [(t, [])]
     2.9 +            val ctxt' = change_options (Proof_Context.init_global thy)
    2.10 +            val [result] = case Quickcheck.active_testers ctxt' of
    2.11 +              [] => error "No active testers for quickcheck"
    2.12 +            | [tester] => tester ctxt' (false, false) [] [(t, [])]
    2.13 +            | _ => error "Multiple active testers for quickcheck"
    2.14            in
    2.15              case Quickcheck.counterexample_of result of 
    2.16                NONE => (NoCex, Quickcheck.timings_of result)
    2.17 @@ -317,11 +320,12 @@
    2.18      val ctxt = Proof_Context.init_global thy
    2.19    in
    2.20      can (TimeLimit.timeLimit (seconds 2.0)
    2.21 -      (Quickcheck.test_goal_terms
    2.22 +      (Quickcheck.test_terms
    2.23          ((Config.put Quickcheck.finite_types true #>
    2.24            Config.put Quickcheck.finite_type_size 1 #>
    2.25            Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
    2.26 -        (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
    2.27 +        (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy)
    2.28 +        (fst (Variable.import_terms true [t] ctxt)))
    2.29    end
    2.30  
    2.31  fun is_executable_thm thy th = is_executable_term thy (prop_of th)

     3.1 --- a/src/HOL/Quickcheck.thy	Sun Oct 16 21:49:47 2011 +0200
     3.2 +++ b/src/HOL/Quickcheck.thy	Mon Oct 17 10:19:01 2011 +0200
     3.3 @@ -144,6 +144,12 @@
     3.4  no_notation fcomp (infixl "\<circ>>" 60)
     3.5  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
     3.6  
     3.7 +subsection {* Tester SML-inductive based on the SML code generator *}
     3.8 +
     3.9 +setup {*
    3.10 +  Context.theory_map (Quickcheck.add_tester ("SML_inductive",
    3.11 +    (Inductive_Codegen.active, Quickcheck_Common.generator_test_goal_terms Inductive_Codegen.test_term)));
    3.12 +*}
    3.13  
    3.14  subsection {* The Random-Predicate Monad *} 
    3.15  

     4.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sun Oct 16 21:49:47 2011 +0200
     4.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Oct 17 10:19:01 2011 +0200
     4.3 @@ -488,7 +488,7 @@
     4.4        thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
     4.5    end;
     4.6  
     4.7 -val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr;
     4.8 +val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr;
     4.9    
    4.10  (* setup *)
    4.11  

     5.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Oct 16 21:49:47 2011 +0200
     5.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Oct 17 10:19:01 2011 +0200
     5.3 @@ -462,9 +462,9 @@
     5.4  fun test_goals ctxt (limit_time, is_interactive) insts goals =
     5.5    if (not (getenv "ISABELLE_GHC" = "")) then
     5.6      let
     5.7 -      val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
     5.8 +      val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
     5.9      in
    5.10 -      Quickcheck.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
    5.11 +      Quickcheck_Common.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
    5.12      end
    5.13    else
    5.14      (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message

     6.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Oct 16 21:49:47 2011 +0200
     6.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Oct 17 10:19:01 2011 +0200
     6.3 @@ -11,6 +11,13 @@
     6.4      -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context 
     6.5    val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
     6.6      -> (string * sort -> string * sort) option
     6.7 +  val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     6.8 +    -> (typ option * (term * term list)) list list
     6.9 +  val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
    6.10 +  type compile_generator =
    6.11 +    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
    6.12 +  val generator_test_goal_terms : compile_generator -> Proof.context -> bool * bool
    6.13 +    -> (string * typ) list -> (term * term list) list -> Quickcheck.result list
    6.14    val ensure_sort_datatype:
    6.15      ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list
    6.16        -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory)
    6.17 @@ -20,6 +27,7 @@
    6.18       -> Proof.context -> (term * term list) list -> term
    6.19    val mk_fun_upd : typ -> typ -> term * term -> term -> term
    6.20    val post_process_term : term -> term
    6.21 +  val test_term : compile_generator -> Proof.context -> bool * bool -> term * term list -> Quickcheck.result
    6.22  end;
    6.23  
    6.24  structure Quickcheck_Common : QUICKCHECK_COMMON =
    6.25 @@ -35,7 +43,222 @@
    6.26    | strip_imp A = ([], A)
    6.27  
    6.28  fun mk_undefined T = Const(@{const_name undefined}, T)
    6.29 +
    6.30 +(* testing functions: testing with increasing sizes (and cardinalities) *)
    6.31 +
    6.32 +type compile_generator =
    6.33 +  Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
    6.34 +
    6.35 +fun check_test_term t =
    6.36 +  let
    6.37 +    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    6.38 +      error "Term to be tested contains type variables";
    6.39 +    val _ = null (Term.add_vars t []) orelse
    6.40 +      error "Term to be tested contains schematic variables";
    6.41 +  in () end
    6.42 +
    6.43 +fun cpu_time description e =
    6.44 +  let val ({cpu, ...}, result) = Timing.timing e ()
    6.45 +  in (result, (description, Time.toMilliseconds cpu)) end
    6.46 +
    6.47 +fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) =
    6.48 +  let
    6.49 +    val _ = check_test_term t
    6.50 +    val names = Term.add_free_names t []
    6.51 +    val current_size = Unsynchronized.ref 0
    6.52 +    val current_result = Unsynchronized.ref Quickcheck.empty_result 
    6.53 +    fun excipit () =
    6.54 +      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
    6.55 +    fun with_size test_fun k =
    6.56 +      if k > Config.get ctxt Quickcheck.size then
    6.57 +        NONE
    6.58 +      else
    6.59 +        let
    6.60 +          val _ = Quickcheck.message ctxt ("Test data size: " ^ string_of_int k)
    6.61 +          val _ = current_size := k
    6.62 +          val ((result, report), timing) =
    6.63 +            cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
    6.64 +          val _ = Quickcheck.add_timing timing current_result
    6.65 +          val _ = Quickcheck.add_report k report current_result
    6.66 +        in
    6.67 +          case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
    6.68 +        end;
    6.69 +  in
    6.70 +    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
    6.71 +      let
    6.72 +        val (test_fun, comp_time) = cpu_time "quickcheck compilation"
    6.73 +          (fn () => compile ctxt [(t, eval_terms)]);
    6.74 +        val _ = Quickcheck.add_timing comp_time current_result
    6.75 +        val (response, exec_time) =
    6.76 +          cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
    6.77 +        val _ = Quickcheck.add_response names eval_terms response current_result
    6.78 +        val _ = Quickcheck.add_timing exec_time current_result
    6.79 +      in !current_result end)
    6.80 +(*    (fn () => (message (excipit ()); !current_result)) ()*)
    6.81 +  end;
    6.82 +
    6.83 +fun validate_terms ctxt ts =
    6.84 +  let
    6.85 +    val _ = map check_test_term ts
    6.86 +    val size = Config.get ctxt Quickcheck.size
    6.87 +    val (test_funs, comp_time) = cpu_time "quickcheck batch compilation"
    6.88 +      (fn () => Quickcheck.mk_batch_validator ctxt ts) 
    6.89 +    fun with_size tester k =
    6.90 +      if k > size then true
    6.91 +      else if tester k then with_size tester (k + 1) else false
    6.92 +    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
    6.93 +        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
    6.94 +              (fn () => with_size test_fun 1) ()
    6.95 +             handle TimeLimit.TimeOut => true)) test_funs)
    6.96 +  in
    6.97 +    (results, [comp_time, exec_time])
    6.98 +  end
    6.99    
   6.100 +fun test_terms ctxt ts =
   6.101 +  let
   6.102 +    val _ = map check_test_term ts
   6.103 +    val size = Config.get ctxt Quickcheck.size
   6.104 +    val namess = map (fn t => Term.add_free_names t []) ts
   6.105 +    val (test_funs, comp_time) =
   6.106 +      cpu_time "quickcheck batch compilation" (fn () => Quickcheck.mk_batch_tester ctxt ts) 
   6.107 +    fun with_size tester k =
   6.108 +      if k > size then NONE
   6.109 +      else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
   6.110 +    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
   6.111 +        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
   6.112 +              (fn () => with_size test_fun 1) ()
   6.113 +             handle TimeLimit.TimeOut => NONE)) test_funs)
   6.114 +  in
   6.115 +    (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results,
   6.116 +      [comp_time, exec_time])
   6.117 +  end
   6.118 +
   6.119 +
   6.120 +fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts =
   6.121 +  let
   6.122 +    val thy = Proof_Context.theory_of ctxt
   6.123 +    val (ts', eval_terms) = split_list ts
   6.124 +    val _ = map check_test_term ts'
   6.125 +    val names = Term.add_free_names (hd ts') []
   6.126 +    val Ts = map snd (Term.add_frees (hd ts') [])
   6.127 +    val current_result = Unsynchronized.ref Quickcheck.empty_result
   6.128 +    fun test_card_size test_fun (card, size) =
   6.129 +      (* FIXME: why decrement size by one? *)
   6.130 +      let
   6.131 +        val (ts, timing) =
   6.132 +          cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
   6.133 +            (fn () => fst (test_fun [card, size - 1]))
   6.134 +        val _ = Quickcheck.add_timing timing current_result
   6.135 +      in
   6.136 +        Option.map (pair card) ts
   6.137 +      end
   6.138 +    val enumeration_card_size =
   6.139 +      if forall (fn T => Sign.of_sort thy (T,  ["Enum.enum"])) Ts then
   6.140 +        (* size does not matter *)
   6.141 +        map (rpair 0) (1 upto (length ts))
   6.142 +      else
   6.143 +        (* size does matter *)
   6.144 +        map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size))
   6.145 +        |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
   6.146 +  in
   6.147 +    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
   6.148 +      let
   6.149 +        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts)
   6.150 +        val _ = Quickcheck.add_timing comp_time current_result     
   6.151 +        val _ = case get_first (test_card_size test_fun) enumeration_card_size of
   6.152 +          SOME (card, ts) => Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
   6.153 +        | NONE => ()
   6.154 +      in !current_result end)
   6.155 +      (*(fn () => (message "Quickcheck ran out of time"; !current_result)) ()*)
   6.156 +  end
   6.157 +
   6.158 +fun get_finite_types ctxt =
   6.159 +  fst (chop (Config.get ctxt Quickcheck.finite_type_size)
   6.160 +    (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
   6.161 +     "Enum.finite_4", "Enum.finite_5"]))
   6.162 +
   6.163 +exception WELLSORTED of string
   6.164 +
   6.165 +fun monomorphic_term thy insts default_T =
   6.166 +  let
   6.167 +    fun subst (T as TFree (v, S)) =
   6.168 +      let
   6.169 +        val T' = AList.lookup (op =) insts v
   6.170 +          |> the_default default_T
   6.171 +      in if Sign.of_sort thy (T', S) then T'
   6.172 +        else raise (WELLSORTED ("For instantiation with default_type " ^
   6.173 +          Syntax.string_of_typ_global thy default_T ^
   6.174 +          ":\n" ^ Syntax.string_of_typ_global thy T' ^
   6.175 +          " to be substituted for variable " ^
   6.176 +          Syntax.string_of_typ_global thy T ^ " does not have sort " ^
   6.177 +          Syntax.string_of_sort_global thy S))
   6.178 +      end
   6.179 +      | subst T = T;
   6.180 +  in (map_types o map_atyps) subst end;
   6.181 +
   6.182 +datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
   6.183 +
   6.184 +fun instantiate_goals lthy insts goals =
   6.185 +  let
   6.186 +    fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
   6.187 +    val thy = Proof_Context.theory_of lthy
   6.188 +    val default_insts =
   6.189 +      if Config.get lthy Quickcheck.finite_types then (get_finite_types lthy) else (Quickcheck.default_type lthy)
   6.190 +    val inst_goals =
   6.191 +      map (fn (check_goal, eval_terms) =>
   6.192 +        if not (null (Term.add_tfree_names check_goal [])) then
   6.193 +          map (fn T =>
   6.194 +            (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy))
   6.195 +              (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
   6.196 +              handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
   6.197 +        else
   6.198 +          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals
   6.199 +    val error_msg =
   6.200 +      cat_lines
   6.201 +        (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
   6.202 +    fun is_wellsorted_term (T, Term t) = SOME (T, t)
   6.203 +      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
   6.204 +    val correct_inst_goals =
   6.205 +      case map (map_filter is_wellsorted_term) inst_goals of
   6.206 +        [[]] => error error_msg
   6.207 +      | xs => xs
   6.208 +    val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg
   6.209 +  in
   6.210 +    correct_inst_goals
   6.211 +  end
   6.212 +
   6.213 +fun collect_results f [] results = results
   6.214 +  | collect_results f (t :: ts) results =
   6.215 +    let
   6.216 +      val result = f t
   6.217 +    in
   6.218 +      if Quickcheck.found_counterexample result then
   6.219 +        (result :: results)
   6.220 +      else
   6.221 +        collect_results f ts (result :: results)
   6.222 +    end  
   6.223 +
   6.224 +fun add_equation_eval_terms (t, eval_terms) =
   6.225 +  case try HOLogic.dest_eq (snd (strip_imp t)) of
   6.226 +    SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs])
   6.227 +  | NONE => (t, eval_terms)
   6.228 +
   6.229 +fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals =
   6.230 +  let
   6.231 +    fun test_term' goal =
   6.232 +      case goal of
   6.233 +        [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t
   6.234 +      | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts)
   6.235 +    val goals' = instantiate_goals ctxt insts goals
   6.236 +      |> map (map (apsnd add_equation_eval_terms))
   6.237 +  in
   6.238 +    if Config.get ctxt Quickcheck.finite_types then
   6.239 +      collect_results test_term' goals' []
   6.240 +    else
   6.241 +      collect_results (test_term compile ctxt (limit_time, is_interactive))
   6.242 +        (maps (map snd) goals') []
   6.243 +  end;
   6.244 +
   6.245  (* defining functions *)
   6.246  
   6.247  fun pat_completeness_auto ctxt =

     7.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Oct 16 21:49:47 2011 +0200
     7.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Oct 17 10:19:01 2011 +0200
     7.3 @@ -438,7 +438,7 @@
     7.4        end
     7.5    end;
     7.6  
     7.7 -val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr;
     7.8 +val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr;
     7.9    
    7.10  (** setup **)
    7.11  

     8.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun Oct 16 21:49:47 2011 +0200
     8.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Oct 17 10:19:01 2011 +0200
     8.3 @@ -10,8 +10,8 @@
     8.4    val poke_test_fn: (int * int * int -> term list option) -> unit
     8.5    val test_term: Proof.context -> (term * term list) list -> int list ->
     8.6      term list option * Quickcheck.report option
     8.7 +  val active : bool Config.T
     8.8    val setup: theory -> theory
     8.9 -  val quickcheck_setup: theory -> theory
    8.10  end;
    8.11  
    8.12  structure Inductive_Codegen : INDUCTIVE_CODEGEN =
    8.13 @@ -862,12 +862,12 @@
    8.14        NONE => deepen bound f (i + 1)
    8.15      | SOME x => SOME x);
    8.16  
    8.17 -val active = Attrib.setup_config_bool @{binding quickcheck_inductive_SML_active} (K false);
    8.18 +val active = Attrib.setup_config_bool @{binding quickcheck_SML_inductive_active} (K false);
    8.19      
    8.20 -val depth_bound = Attrib.setup_config_int @{binding ind_quickcheck_depth} (K 10);
    8.21 -val depth_start = Attrib.setup_config_int @{binding ind_quickcheck_depth_start} (K 1);
    8.22 -val random_values = Attrib.setup_config_int @{binding ind_quickcheck_random} (K 5);
    8.23 -val size_offset = Attrib.setup_config_int @{binding ind_quickcheck_size_offset} (K 0);
    8.24 +val depth_bound = Attrib.setup_config_int @{binding quickcheck_ind_depth} (K 10);
    8.25 +val depth_start = Attrib.setup_config_int @{binding quickcheck_ind_depth_start} (K 1);
    8.26 +val random_values = Attrib.setup_config_int @{binding quickcheck_ind_random} (K 5);
    8.27 +val size_offset = Attrib.setup_config_int @{binding quickcheck_ind_size_offset} (K 0);
    8.28  
    8.29  fun test_term ctxt [(t, [])] =
    8.30        let
    8.31 @@ -926,9 +926,4 @@
    8.32    | test_term ctxt _ =
    8.33        error "Compilation of multiple instances is not supported by tester SML_inductive";
    8.34  
    8.35 -val test_goal = Quickcheck.generator_test_goal_terms test_term;
    8.36 -
    8.37 -val quickcheck_setup =
    8.38 -  Context.theory_map (Quickcheck.add_tester ("SML_inductive", (active, test_goal)));
    8.39 -
    8.40  end;

     9.1 --- a/src/Tools/quickcheck.ML	Sun Oct 16 21:49:47 2011 +0200
     9.2 +++ b/src/Tools/quickcheck.ML	Mon Oct 17 10:19:01 2011 +0200
     9.3 @@ -29,6 +29,7 @@
     9.4    val test_params_of : Proof.context -> test_params
     9.5    val map_test_params : (typ list * expectation -> typ list * expectation)
     9.6      -> Context.generic -> Context.generic
     9.7 +  val default_type : Proof.context -> typ list
     9.8    datatype report = Report of
     9.9      { iterations : int, raised_match_errors : int,
    9.10        satisfied_assms : int list, positive_concl_tests : int }
    9.11 @@ -40,7 +41,10 @@
    9.12        timings : (string * int) list,
    9.13        reports : (int * report) list}
    9.14    val empty_result : result
    9.15 +  val found_counterexample : result -> bool
    9.16    val add_timing : (string * int) -> result Unsynchronized.ref -> unit
    9.17 +  val add_response : string list -> term list -> term list option -> result Unsynchronized.ref -> unit
    9.18 +  val add_report : int -> report option -> result Unsynchronized.ref -> unit
    9.19    val counterexample_of : result -> (string * term) list option
    9.20    val timings_of : result -> (string * int) list
    9.21    (* registering testers & generators *) 
    9.22 @@ -54,23 +58,15 @@
    9.23      string * (Proof.context -> term list -> (int -> bool) list)
    9.24        -> Context.generic -> Context.generic
    9.25    (* basic operations *)
    9.26 -  type compile_generator =
    9.27 -    Proof.context -> (term * term list) list -> int list -> term list option * report option
    9.28 -  val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a  
    9.29 -  val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
    9.30 -    -> (typ option * (term * term list)) list list
    9.31 -  val collect_results : ('a -> result) -> 'a list -> result list -> result list
    9.32 -  val generator_test_goal_terms : compile_generator ->
    9.33 -    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
    9.34 +  val message : Proof.context -> string -> unit
    9.35 +  val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a
    9.36    (* testing terms and proof states *)
    9.37 -  val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result
    9.38 -  val test_goal_terms :
    9.39 +  val mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
    9.40 +  val mk_batch_tester : Proof.context -> term list -> (int -> term list option) list option
    9.41 +  val active_testers : Proof.context -> tester list
    9.42 +  val test_terms :
    9.43      Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option
    9.44    val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
    9.45 -  (* testing a batch of terms *)
    9.46 -  val test_terms:
    9.47 -    Proof.context -> term list -> (string * term) list option list option * (string * int) list
    9.48 -  val validate_terms: Proof.context -> term list -> bool list option * (string * int) list
    9.49  end;
    9.50  
    9.51  structure Quickcheck : QUICKCHECK =
    9.52 @@ -119,14 +115,15 @@
    9.53  
    9.54  fun timings_of (Result r) = #timings r
    9.55  
    9.56 -fun set_reponse names eval_terms (SOME ts) (Result r) =
    9.57 +fun set_response names eval_terms (SOME ts) (Result r) =
    9.58    let
    9.59      val (ts1, ts2) = chop (length names) ts
    9.60 +    val (eval_terms', _) = chop (length ts2) eval_terms
    9.61    in
    9.62 -    Result {counterexample = SOME (names ~~ ts1), evaluation_terms = SOME (eval_terms ~~ ts2),
    9.63 +    Result {counterexample = SOME (names ~~ ts1), evaluation_terms = SOME (eval_terms' ~~ ts2),
    9.64        timings = #timings r, reports = #reports r}
    9.65    end
    9.66 -  | set_reponse _ _ NONE result = result
    9.67 +  | set_response _ _ NONE result = result
    9.68  
    9.69  
    9.70  fun set_counterexample counterexample (Result r) =
    9.71 @@ -153,7 +150,7 @@
    9.72    Unsynchronized.change result_ref (cons_report size report)
    9.73  
    9.74  fun add_response names eval_terms response result_ref =
    9.75 -  Unsynchronized.change result_ref (set_reponse names eval_terms response)
    9.76 +  Unsynchronized.change result_ref (set_response names eval_terms response)
    9.77  
    9.78  (* expectation *)
    9.79  
    9.80 @@ -275,18 +272,6 @@
    9.81  type compile_generator =
    9.82    Proof.context -> (term * term list) list -> int list -> term list option * report option
    9.83  
    9.84 -fun check_test_term t =
    9.85 -  let
    9.86 -    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    9.87 -      error "Term to be tested contains type variables";
    9.88 -    val _ = null (Term.add_vars t []) orelse
    9.89 -      error "Term to be tested contains schematic variables";
    9.90 -  in () end
    9.91 -
    9.92 -fun cpu_time description e =
    9.93 -  let val ({cpu, ...}, result) = Timing.timing e ()
    9.94 -  in (result, (description, Time.toMilliseconds cpu)) end
    9.95 -
    9.96  fun limit timeout (limit_time, is_interactive) f exc () =
    9.97    if limit_time then
    9.98        TimeLimit.timeLimit timeout f ()
    9.99 @@ -295,205 +280,9 @@
   9.100    else
   9.101      f ()
   9.102  
   9.103 -fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) =
   9.104 -  let
   9.105 -    fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
   9.106 -    val _ = check_test_term t
   9.107 -    val names = Term.add_free_names t []
   9.108 -    val current_size = Unsynchronized.ref 0
   9.109 -    val current_result = Unsynchronized.ref empty_result 
   9.110 -    fun excipit () =
   9.111 -      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
   9.112 -    fun with_size test_fun k =
   9.113 -      if k > Config.get ctxt size then
   9.114 -        NONE
   9.115 -      else
   9.116 -        let
   9.117 -          val _ = message ("Test data size: " ^ string_of_int k)
   9.118 -          val _ = current_size := k
   9.119 -          val ((result, report), timing) =
   9.120 -            cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
   9.121 -          val _ = add_timing timing current_result
   9.122 -          val _ = add_report k report current_result
   9.123 -        in
   9.124 -          case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
   9.125 -        end;
   9.126 -  in
   9.127 -    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
   9.128 -      let
   9.129 -        val (test_fun, comp_time) = cpu_time "quickcheck compilation"
   9.130 -          (fn () => compile ctxt [(t, eval_terms)]);
   9.131 -        val _ = add_timing comp_time current_result
   9.132 -        val (response, exec_time) =
   9.133 -          cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
   9.134 -        val _ = add_response names eval_terms response current_result
   9.135 -        val _ = add_timing exec_time current_result
   9.136 -      in !current_result end)
   9.137 -(*    (fn () => (message (excipit ()); !current_result)) ()*)
   9.138 -  end;
   9.139 -
   9.140 -fun validate_terms ctxt ts =
   9.141 -  let
   9.142 -    val _ = map check_test_term ts
   9.143 -    val size = Config.get ctxt size
   9.144 -    val (test_funs, comp_time) = cpu_time "quickcheck batch compilation"
   9.145 -      (fn () => mk_batch_validator ctxt ts) 
   9.146 -    fun with_size tester k =
   9.147 -      if k > size then true
   9.148 -      else if tester k then with_size tester (k + 1) else false
   9.149 -    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
   9.150 -        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout))
   9.151 -              (fn () => with_size test_fun 1) ()
   9.152 -             handle TimeLimit.TimeOut => true)) test_funs)
   9.153 -  in
   9.154 -    (results, [comp_time, exec_time])
   9.155 -  end
   9.156 -  
   9.157 -fun test_terms ctxt ts =
   9.158 -  let
   9.159 -    val _ = map check_test_term ts
   9.160 -    val size = Config.get ctxt size
   9.161 -    val namess = map (fn t => Term.add_free_names t []) ts
   9.162 -    val (test_funs, comp_time) =
   9.163 -      cpu_time "quickcheck batch compilation" (fn () => mk_batch_tester ctxt ts) 
   9.164 -    fun with_size tester k =
   9.165 -      if k > size then NONE
   9.166 -      else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
   9.167 -    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
   9.168 -        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout))
   9.169 -              (fn () => with_size test_fun 1) ()
   9.170 -             handle TimeLimit.TimeOut => NONE)) test_funs)
   9.171 -  in
   9.172 -    (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results,
   9.173 -      [comp_time, exec_time])
   9.174 -  end
   9.175 -
   9.176 -(* FIXME: this function shows that many assumptions are made upon the generation *)
   9.177 -(* In the end there is probably no generic quickcheck interface left... *)
   9.178 -
   9.179 -fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts =
   9.180 -  let
   9.181 -    val thy = Proof_Context.theory_of ctxt
   9.182 -    fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
   9.183 -    val (ts', eval_terms) = split_list ts
   9.184 -    val _ = map check_test_term ts'
   9.185 -    val names = Term.add_free_names (hd ts') []
   9.186 -    val Ts = map snd (Term.add_frees (hd ts') [])
   9.187 -    val current_result = Unsynchronized.ref empty_result
   9.188 -    fun test_card_size test_fun (card, size) =
   9.189 -      (* FIXME: why decrement size by one? *)
   9.190 -      let
   9.191 -        val (ts, timing) =
   9.192 -          cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
   9.193 -            (fn () => fst (test_fun [card, size - 1]))
   9.194 -        val _ = add_timing timing current_result
   9.195 -      in
   9.196 -        Option.map (pair card) ts
   9.197 -      end
   9.198 -    val enumeration_card_size =
   9.199 -      if forall (fn T => Sign.of_sort thy (T,  ["Enum.enum"])) Ts then
   9.200 -        (* size does not matter *)
   9.201 -        map (rpair 0) (1 upto (length ts))
   9.202 -      else
   9.203 -        (* size does matter *)
   9.204 -        map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
   9.205 -        |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
   9.206 -  in
   9.207 -    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
   9.208 -      let
   9.209 -        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts)
   9.210 -        val _ = add_timing comp_time current_result     
   9.211 -        val _ = case get_first (test_card_size test_fun) enumeration_card_size of
   9.212 -          SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
   9.213 -        | NONE => ()
   9.214 -      in !current_result end)
   9.215 -      (*(fn () => (message "Quickcheck ran out of time"; !current_result)) ()*)
   9.216 -  end
   9.217 -
   9.218 -fun get_finite_types ctxt =
   9.219 -  fst (chop (Config.get ctxt finite_type_size)
   9.220 -    (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
   9.221 -     "Enum.finite_4", "Enum.finite_5"]))
   9.222 -
   9.223 -exception WELLSORTED of string
   9.224 -
   9.225 -fun monomorphic_term thy insts default_T =
   9.226 -  let
   9.227 -    fun subst (T as TFree (v, S)) =
   9.228 -      let
   9.229 -        val T' = AList.lookup (op =) insts v
   9.230 -          |> the_default default_T
   9.231 -      in if Sign.of_sort thy (T', S) then T'
   9.232 -        else raise (WELLSORTED ("For instantiation with default_type " ^
   9.233 -          Syntax.string_of_typ_global thy default_T ^
   9.234 -          ":\n" ^ Syntax.string_of_typ_global thy T' ^
   9.235 -          " to be substituted for variable " ^
   9.236 -          Syntax.string_of_typ_global thy T ^ " does not have sort " ^
   9.237 -          Syntax.string_of_sort_global thy S))
   9.238 -      end
   9.239 -      | subst T = T;
   9.240 -  in (map_types o map_atyps) subst end;
   9.241 -
   9.242 -datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
   9.243 -
   9.244 -fun instantiate_goals lthy insts goals =
   9.245 -  let
   9.246 -    fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
   9.247 -    val thy = Proof_Context.theory_of lthy
   9.248 -    val default_insts =
   9.249 -      if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy)
   9.250 -    val inst_goals =
   9.251 -      map (fn (check_goal, eval_terms) =>
   9.252 -        if not (null (Term.add_tfree_names check_goal [])) then
   9.253 -          map (fn T =>
   9.254 -            (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy))
   9.255 -              (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
   9.256 -              handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
   9.257 -        else
   9.258 -          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals
   9.259 -    val error_msg =
   9.260 -      cat_lines
   9.261 -        (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
   9.262 -    fun is_wellsorted_term (T, Term t) = SOME (T, t)
   9.263 -      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
   9.264 -    val correct_inst_goals =
   9.265 -      case map (map_filter is_wellsorted_term) inst_goals of
   9.266 -        [[]] => error error_msg
   9.267 -      | xs => xs
   9.268 -    val _ = if Config.get lthy quiet then () else warning error_msg
   9.269 -  in
   9.270 -    correct_inst_goals
   9.271 -  end
   9.272 -
   9.273 -fun collect_results f [] results = results
   9.274 -  | collect_results f (t :: ts) results =
   9.275 -    let
   9.276 -      val result = f t
   9.277 -    in
   9.278 -      if found_counterexample result then
   9.279 -        (result :: results)
   9.280 -      else
   9.281 -        collect_results f ts (result :: results)
   9.282 -    end  
   9.283 -
   9.284 -fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals =
   9.285 -  let
   9.286 -    fun test_term' goal =
   9.287 -      case goal of
   9.288 -        [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t
   9.289 -      | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts)
   9.290 -    val correct_inst_goals = instantiate_goals ctxt insts goals
   9.291 -  in
   9.292 -    if Config.get ctxt finite_types then
   9.293 -      collect_results test_term' correct_inst_goals []
   9.294 -    else
   9.295 -      collect_results (test_term compile ctxt (limit_time, is_interactive))
   9.296 -        (maps (map snd) correct_inst_goals) []
   9.297 -  end;
   9.298 -
   9.299  fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s
   9.300    
   9.301 -fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
   9.302 +fun test_terms ctxt (limit_time, is_interactive) insts goals =
   9.303    case active_testers ctxt of
   9.304      [] => error "No active testers for quickcheck"
   9.305    | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
   9.306 @@ -524,7 +313,7 @@
   9.307          map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
   9.308            (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   9.309    in
   9.310 -    test_goal_terms lthy (time_limit, is_interactive) insts goals
   9.311 +    test_terms lthy (time_limit, is_interactive) insts goals
   9.312    end
   9.313  
   9.314  (* pretty printing *)
   9.315 @@ -537,7 +326,7 @@
   9.316          map (fn (s, t) =>
   9.317            Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex))
   9.318          @ (if null eval_terms then []
   9.319 -           else (Pretty.str ("Evaluated terms:\n") ::
   9.320 +           else (Pretty.fbrk :: Pretty.str ("Evaluated terms:") ::
   9.321               map (fn (t, u) =>
   9.322                 Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
   9.323                   Syntax.pretty_term ctxt u]) (rev eval_terms))));