1.1 --- a/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -31,13 +31,11 @@
     1.4      string * (Proof.context -> term -> int -> term list option * (bool list * bool))
     1.5        -> Context.generic -> Context.generic
     1.6    (* testing terms and proof states *)
     1.7 -  val test_term_small: Proof.context -> term ->
     1.8 -    (string * term) list option * ((string * int) list * ((int * report list) list) option)
     1.9 -  val test_term: Proof.context -> bool -> string option -> term ->
    1.10 -    (string * term) list option * ((string * int) list * ((int * report list) list) option)
    1.11 +  val test_term: Proof.context -> bool -> term ->
    1.12 +    (string * term) list option * ((string * int) list * ((int * report) list) option)
    1.13    val test_goal_terms:
    1.14 -    Proof.context -> bool -> string option * (string * typ) list -> term list
    1.15 -      -> (string * term) list option * ((string * int) list * ((int * report list) list) option) list
    1.16 +    Proof.context -> bool -> (string * typ) list -> term list
    1.17 +      -> (string * term) list option * ((string * int) list * ((int * report) list) option) list
    1.18    val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
    1.19  end;
    1.20  
    1.21 @@ -139,25 +137,23 @@
    1.22  
    1.23  (* generating tests *)
    1.24  
    1.25 -fun mk_tester_select name ctxt =
    1.26 -  case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name
    1.27 -   of NONE => error ("No such quickcheck generator: " ^ name)
    1.28 -    | SOME generator => generator ctxt;
    1.29 -
    1.30 -fun mk_testers ctxt t =
    1.31 -  (map snd o fst o Data.get o Context.Proof) ctxt
    1.32 -  |> map_filter (fn generator => try (generator ctxt) t);
    1.33 -
    1.34 -fun mk_testers_strict ctxt t =
    1.35 +fun mk_tester ctxt t =
    1.36    let
    1.37 -    val generators = ((map snd o fst o Data.get o Context.Proof) ctxt)
    1.38 -    val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators;
    1.39 +    val name = Config.get ctxt tester
    1.40 +    val tester = case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name
    1.41 +      of NONE => error ("No such quickcheck tester: " ^ name)
    1.42 +      | SOME tester => tester ctxt;
    1.43    in
    1.44 -    if forall (is_none o Exn.get_result) testers
    1.45 -    then [(Exn.release o snd o split_last) testers]
    1.46 -    else map_filter Exn.get_result testers
    1.47 -  end;
    1.48 -
    1.49 +    if Config.get ctxt quiet then
    1.50 +      try tester t
    1.51 +    else
    1.52 +      let
    1.53 +        val tester = Exn.interruptible_capture tester t
    1.54 +      in case Exn.get_result tester of
    1.55 +          NONE => SOME (Exn.release tester)
    1.56 +        | SOME tester => SOME tester
    1.57 +      end
    1.58 +  end
    1.59  
    1.60  (* testing propositions *)
    1.61  
    1.62 @@ -211,16 +207,13 @@
    1.63    | is_iteratable "random" = true
    1.64    | is_iteratable _ = false
    1.65    
    1.66 -fun test_term ctxt is_interactive generator_name t =
    1.67 +fun test_term ctxt is_interactive t =
    1.68    let
    1.69      val (names, t') = prep_test_term t;
    1.70      val current_size = Unsynchronized.ref 0
    1.71      fun excipit s =
    1.72        "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
    1.73 -    val (testers, comp_time) = cpu_time "quickcheck compilation"
    1.74 -      (fn () => (case generator_name
    1.75 -       of NONE => if Config.get ctxt quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
    1.76 -        | SOME name => [mk_tester_select name ctxt t']));
    1.77 +    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t');
    1.78      fun iterate f 0 report = (NONE, report)
    1.79        | iterate f j report =
    1.80          let
    1.81 @@ -233,38 +226,31 @@
    1.82          end
    1.83      val empty_report = Report { iterations = 0, raised_match_errors = 0,
    1.84        satisfied_assms = [], positive_concl_tests = 0 }
    1.85 -    fun with_testers k [] = (NONE, [])
    1.86 -      | with_testers k (tester :: testers) =
    1.87 -        let
    1.88 -          val niterations = case generator_name of
    1.89 -            SOME generator_name =>
    1.90 -              if is_iteratable generator_name then Config.get ctxt iterations else 1
    1.91 -          | NONE => Config.get ctxt iterations
    1.92 -          val (result, timing) = cpu_time ("size " ^ string_of_int k)
    1.93 -            (fn () => iterate (fn () => tester (k - 1)) niterations empty_report)
    1.94 -        in
    1.95 -          case result
    1.96 -           of (NONE, report) => apsnd (cons report) (with_testers k testers)
    1.97 -            | (SOME q, report) => (SOME q, [report])
    1.98 -        end
    1.99 -    fun with_size k reports =
   1.100 +    fun with_size test_fun k reports =
   1.101        if k > Config.get ctxt size then (NONE, reports)
   1.102        else
   1.103         (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
   1.104          let
   1.105            val _ = current_size := k
   1.106 -          val (result, new_report) = with_testers k testers
   1.107 +          val niterations =
   1.108 +            if is_iteratable (Config.get ctxt tester) then Config.get ctxt iterations else 1
   1.109 +          val ((result, new_report), timing) = cpu_time ("size " ^ string_of_int k)
   1.110 +            (fn () => iterate (fn () => test_fun (k - 1)) niterations empty_report)
   1.111            val reports = ((k, new_report) :: reports)
   1.112 -        in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
   1.113 -    val ((result, reports), exec_time) =
   1.114 -      TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => cpu_time "quickcheck execution"
   1.115 -      (fn () => apfst
   1.116 -         (fn result => case result of NONE => NONE
   1.117 -        | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
   1.118 -      handle TimeLimit.TimeOut =>
   1.119 -        if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut
   1.120 +        in case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports) end);
   1.121    in
   1.122 -    (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
   1.123 +    case test_fun of NONE => (NONE, ([comp_time], NONE)) 
   1.124 +      | SOME test_fun =>
   1.125 +        TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
   1.126 +          let
   1.127 +            val ((result, reports), exec_time) =
   1.128 +              cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
   1.129 +          in
   1.130 +            (case result of NONE => NONE | SOME ts => SOME (names ~~ ts),
   1.131 +              ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
   1.132 +          end) ()
   1.133 +        handle TimeLimit.TimeOut =>
   1.134 +          if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut
   1.135    end;
   1.136  
   1.137  fun get_finite_types ctxt =
   1.138 @@ -292,7 +278,7 @@
   1.139  
   1.140  datatype wellsorted_error = Wellsorted_Error of string | Term of term
   1.141  
   1.142 -fun test_goal_terms lthy is_interactive (generator_name, insts) check_goals =
   1.143 +fun test_goal_terms lthy is_interactive insts check_goals =
   1.144    let
   1.145      val thy = ProofContext.theory_of lthy 
   1.146      val inst_goals =
   1.147 @@ -315,9 +301,9 @@
   1.148          case f t of
   1.149            (SOME res, report) => (SOME res, rev (report :: reports))
   1.150          | (NONE, report) => collect_results f (report :: reports) ts
   1.151 -  in collect_results (test_term lthy is_interactive generator_name) [] correct_inst_goals end;
   1.152 +  in collect_results (test_term lthy is_interactive) [] correct_inst_goals end;
   1.153  
   1.154 -fun test_goal (generator_name, insts) i state =
   1.155 +fun test_goal insts i state =
   1.156    let
   1.157      val lthy = Proof.context_of state;
   1.158      val thy = Proof.theory_of state;
   1.159 @@ -338,7 +324,7 @@
   1.160        | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
   1.161          (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   1.162    in
   1.163 -    test_goal_terms lthy true (generator_name, insts) check_goals
   1.164 +    test_goal_terms lthy true insts check_goals
   1.165    end
   1.166  
   1.167  (* pretty printing *)
   1.168 @@ -363,16 +349,10 @@
   1.169       @ [pretty_stat "positive conclusion tests" positive_concl_tests])
   1.170    end
   1.171  
   1.172 -fun pretty_reports' [report] = [Pretty.chunks (pretty_report report)]
   1.173 -  | pretty_reports' reports =
   1.174 -  map_index (fn (i, report) =>
   1.175 -    Pretty.chunks (Pretty.str (string_of_int (i + 1) ^ ". generator:\n") :: pretty_report report))
   1.176 -    reports
   1.177 -
   1.178  fun pretty_reports ctxt (SOME reports) =
   1.179    Pretty.chunks (Pretty.str "Quickcheck report:" ::
   1.180 -    maps (fn (size, reports) =>
   1.181 -      Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_reports' reports @ [Pretty.brk 1])
   1.182 +    maps (fn (size, report) =>
   1.183 +      Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_report report @ [Pretty.brk 1])
   1.184        (rev reports))
   1.185    | pretty_reports ctxt NONE = Pretty.str ""
   1.186  
   1.187 @@ -391,7 +371,7 @@
   1.188        val res =
   1.189          state
   1.190          |> Proof.map_context (Config.put report false #> Config.put quiet true)
   1.191 -        |> try (test_goal (NONE, []) 1);
   1.192 +        |> try (test_goal [] 1);
   1.193      in
   1.194        case res of
   1.195          NONE => (false, state)
   1.196 @@ -424,7 +404,8 @@
   1.197    | read_expectation "counterexample" = Counterexample
   1.198    | read_expectation s = error ("Not an expectation value: " ^ s)  
   1.199  
   1.200 -fun parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
   1.201 +fun parse_test_param ("tester", [arg]) = Config.put_generic tester arg
   1.202 +  | parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
   1.203    | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
   1.204    | parse_test_param ("default_type", arg) = (fn gen_ctxt =>
   1.205      map_test_params ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)
   1.206 @@ -437,20 +418,18 @@
   1.207    | parse_test_param ("finite_type_size", [arg]) = Config.put_generic finite_type_size (read_nat arg)
   1.208    | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
   1.209  
   1.210 -fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =
   1.211 -      (apfst o apfst o K o SOME) arg ((generator, insts), ctxt)
   1.212 -  | parse_test_param_inst (name, arg) ((generator, insts), ctxt) =
   1.213 +fun parse_test_param_inst (name, arg) (insts, ctxt) =
   1.214        case try (ProofContext.read_typ ctxt) name
   1.215 -       of SOME (TFree (v, _)) => (apfst o apsnd o AList.update (op =))
   1.216 -              (v, ProofContext.read_typ ctxt (the_single arg)) ((generator, insts), ctxt)
   1.217 -        | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) ((generator, insts), ctxt);
   1.218 +       of SOME (TFree (v, _)) => (apfst o AList.update (op =))
   1.219 +              (v, ProofContext.read_typ ctxt (the_single arg)) (insts, ctxt)
   1.220 +        | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) (insts, ctxt);
   1.221  
   1.222  fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
   1.223    
   1.224  fun gen_quickcheck args i state =
   1.225    state
   1.226 -  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ((NONE, []), ctxt))
   1.227 -  |> (fn ((generator, insts), state') => test_goal (generator, insts) i state'
   1.228 +  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ([], ctxt))
   1.229 +  |> (fn (insts, state') => test_goal insts i state'
   1.230    |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
   1.231                 error ("quickcheck expected to find no counterexample but found one") else ()
   1.232             | (NONE, _) => if expect (Proof.context_of state') = Counterexample then