src/Tools/quickcheck.ML
author haftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 58410 6d46ad54a2ab
parent 57195 ec0e10f11276
child 58842 22b87ab47d3b
permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
     1 (*  Title:      Tools/quickcheck.ML
     2     Author:     Stefan Berghofer, Florian Haftmann, Lukas Bulwahn, TU Muenchen
     3 
     4 Generic counterexample search engine.
     5 *)
     6 
     7 signature QUICKCHECK =
     8 sig
     9   val quickcheckN: string
    10   val genuineN: string
    11   val noneN: string
    12   val unknownN: string
    13   (*configuration*)
    14   val batch_tester : string Config.T
    15   val size : int Config.T
    16   val iterations : int Config.T
    17   val depth : int Config.T
    18   val no_assms : bool Config.T
    19   val report : bool Config.T
    20   val timeout : real Config.T
    21   val timing : bool Config.T
    22   val genuine_only : bool Config.T
    23   val abort_potential : bool Config.T
    24   val quiet : bool Config.T
    25   val verbose : bool Config.T
    26   val use_subtype : bool Config.T
    27   val allow_function_inversion : bool Config.T
    28   val finite_types : bool Config.T
    29   val finite_type_size : int Config.T
    30   val tag : string Config.T
    31   val locale : string Config.T
    32   val set_active_testers: string list -> Context.generic -> Context.generic
    33   datatype expectation = No_Expectation | No_Counterexample | Counterexample;
    34   datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
    35   val test_params_of : Proof.context -> test_params
    36   val map_test_params : (typ list * expectation -> typ list * expectation)
    37     -> Context.generic -> Context.generic
    38   val default_type : Proof.context -> typ list
    39   datatype report = Report of
    40     { iterations : int, raised_match_errors : int,
    41       satisfied_assms : int list, positive_concl_tests : int }
    42   (*quickcheck's result*)
    43   datatype result =
    44     Result of
    45      {counterexample : (bool * (string * term) list) option,
    46       evaluation_terms : (term * term) list option,
    47       timings : (string * int) list,
    48       reports : (int * report) list}
    49   val empty_result : result
    50   val found_counterexample : result -> bool
    51   val add_timing : (string * int) -> result Unsynchronized.ref -> unit
    52   val add_response : string list -> term list -> (bool * term list) option ->
    53     result Unsynchronized.ref -> unit
    54   val add_report : int -> report option -> result Unsynchronized.ref -> unit
    55   val counterexample_of : result -> (bool * (string * term) list) option
    56   val timings_of : result -> (string * int) list
    57   (*registering testers & generators*)
    58   type tester =
    59     Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list
    60   val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic
    61   val add_batch_generator :
    62     string * (Proof.context -> term list -> (int -> term list option) list)
    63       -> Context.generic -> Context.generic
    64   val add_batch_validator :
    65     string * (Proof.context -> term list -> (int -> bool) list)
    66       -> Context.generic -> Context.generic
    67   (*basic operations*)
    68   val message : Proof.context -> string -> unit
    69   val verbose_message : Proof.context -> string -> unit
    70   val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a
    71   val pretty_counterex : Proof.context -> bool ->
    72     ((bool * (string * term) list) * (term * term) list) option -> Pretty.T
    73   (*testing terms and proof states*)
    74   val mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
    75   val mk_batch_tester : Proof.context -> term list -> (int -> term list option) list option
    76   val active_testers : Proof.context -> tester list
    77   val test_terms : Proof.context -> bool * bool -> (string * typ) list ->
    78     (term * term list) list -> result list option
    79   val quickcheck: (string * string list) list -> int -> Proof.state ->
    80     (bool * (string * term) list) option
    81 end;
    82 
    83 structure Quickcheck : QUICKCHECK =
    84 struct
    85 
    86 val quickcheckN = "quickcheck";
    87 
    88 val genuineN = "genuine";
    89 val noneN = "none";
    90 val unknownN = "unknown";
    91 
    92 
    93 (* preferences *)
    94 
    95 val _ =
    96   ProofGeneral.preference_option ProofGeneral.category_tracing
    97     NONE
    98     @{system_option auto_quickcheck}
    99     "auto-quickcheck"
   100     "Run Quickcheck automatically";
   101 
   102 
   103 (* quickcheck report *)
   104 
   105 datatype report = Report of
   106  {iterations : int,
   107   raised_match_errors : int,
   108   satisfied_assms : int list,
   109   positive_concl_tests : int};
   110 
   111 
   112 (* Quickcheck Result *)
   113 
   114 datatype result = Result of
   115  {counterexample : (bool * (string * term) list) option,
   116   evaluation_terms : (term * term) list option,
   117   timings : (string * int) list,
   118   reports : (int * report) list};
   119 
   120 val empty_result =
   121   Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []};
   122 
   123 fun counterexample_of (Result r) = #counterexample r;
   124 
   125 fun found_counterexample (Result r) = is_some (#counterexample r);
   126 
   127 fun response_of (Result r) =
   128   (case (#counterexample r, #evaluation_terms r) of
   129     (SOME ts, SOME evals) => SOME (ts, evals)
   130   | (NONE, NONE) => NONE);
   131 
   132 fun timings_of (Result r) = #timings r;
   133 
   134 fun set_response names eval_terms (SOME (genuine, ts)) (Result r) =
   135       let
   136         val (ts1, ts2) = chop (length names) ts
   137         val (eval_terms', _) = chop (length ts2) eval_terms
   138       in
   139         Result {counterexample = SOME (genuine, (names ~~ ts1)),
   140           evaluation_terms = SOME (eval_terms' ~~ ts2),
   141           timings = #timings r, reports = #reports r}
   142       end
   143   | set_response _ _ NONE result = result;
   144 
   145 
   146 fun cons_timing timing (Result r) =
   147   Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
   148     timings = cons timing (#timings r), reports = #reports r};
   149 
   150 fun cons_report size (SOME report) (Result r) =
   151       Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
   152         timings = #timings r, reports = cons (size, report) (#reports r)}
   153   | cons_report _ NONE result = result;
   154 
   155 fun add_timing timing result_ref =
   156   Unsynchronized.change result_ref (cons_timing timing);
   157 
   158 fun add_report size report result_ref =
   159   Unsynchronized.change result_ref (cons_report size report);
   160 
   161 fun add_response names eval_terms response result_ref =
   162   Unsynchronized.change result_ref (set_response names eval_terms response);
   163 
   164 
   165 (* expectation *)
   166 
   167 datatype expectation = No_Expectation | No_Counterexample | Counterexample;
   168 
   169 fun merge_expectation (expect1, expect2) =
   170   if expect1 = expect2 then expect1 else No_Expectation;
   171 
   172 (*quickcheck configuration -- default parameters, test generators*)
   173 val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "");
   174 val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10);
   175 val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100);
   176 val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10);
   177 
   178 val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false);
   179 val locale = Attrib.setup_config_string @{binding quickcheck_locale} (K "interpret expand");
   180 val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true);
   181 val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false);
   182 val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0);
   183 
   184 val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false);
   185 val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false);
   186 
   187 val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false);
   188 val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false);
   189 val tag = Attrib.setup_config_string @{binding quickcheck_tag} (K "");
   190 
   191 val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false);
   192 
   193 val allow_function_inversion =
   194   Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false);
   195 val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true);
   196 val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3);
   197 
   198 datatype test_params = Test_Params of
   199   {default_type: typ list, expect : expectation};
   200 
   201 fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect);
   202 
   203 fun make_test_params (default_type, expect) =
   204   Test_Params {default_type = default_type, expect = expect};
   205 
   206 fun map_test_params' f (Test_Params {default_type, expect}) =
   207   make_test_params (f (default_type, expect));
   208 
   209 fun merge_test_params
   210   (Test_Params {default_type = default_type1, expect = expect1},
   211     Test_Params {default_type = default_type2, expect = expect2}) =
   212   make_test_params
   213     (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
   214 
   215 type tester =
   216   Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list;
   217 
   218 structure Data = Generic_Data
   219 (
   220   type T =
   221     ((string * (bool Config.T * tester)) list *
   222       ((string * (Proof.context -> term list -> (int -> term list option) list)) list *
   223       ((string * (Proof.context -> term list -> (int -> bool) list)) list))) *
   224       test_params;
   225   val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
   226   val extend = I;
   227   fun merge
   228    (((testers1, (batch_generators1, batch_validators1)), params1),
   229     ((testers2, (batch_generators2, batch_validators2)), params2)) : T =
   230     ((AList.merge (op =) (K true) (testers1, testers2),
   231       (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
   232        AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
   233       merge_test_params (params1, params2));
   234 );
   235 
   236 val test_params_of = snd o Data.get o Context.Proof;
   237 
   238 val default_type = fst o dest_test_params o test_params_of;
   239 
   240 val expect = snd o dest_test_params o test_params_of;
   241 
   242 val map_test_params = Data.map o apsnd o map_test_params';
   243 
   244 val add_tester = Data.map o apfst o apfst o AList.update (op =);
   245 
   246 val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =);
   247 
   248 val add_batch_validator = Data.map o apfst o apsnd o apsnd o AList.update (op =);
   249 
   250 fun active_testers ctxt =
   251   let
   252     val testers = map snd (fst (fst (Data.get (Context.Proof ctxt))));
   253   in
   254     map snd (filter (fn (active, _) => Config.get ctxt active) testers)
   255   end;
   256 
   257 fun set_active_testers [] context = context
   258   | set_active_testers testers context =
   259       let
   260         val registered_testers = fst (fst (Data.get context));
   261       in
   262         fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name))
   263           registered_testers context
   264       end;
   265 
   266 
   267 (* generating tests *)
   268 
   269 fun gen_mk_tester lookup ctxt v =
   270   let
   271     val name = Config.get ctxt batch_tester
   272     val tester =
   273       (case lookup ctxt name of
   274         NONE => error ("No such quickcheck batch-tester: " ^ name)
   275       | SOME tester => tester ctxt);
   276   in
   277     if Config.get ctxt quiet then
   278       try tester v
   279     else
   280       let (* FIXME !?!? *)
   281         val tester = Exn.interruptible_capture tester v
   282       in
   283         (case Exn.get_res tester of
   284           NONE => SOME (Exn.release tester)
   285         | SOME tester => SOME tester)
   286       end
   287   end;
   288 
   289 val mk_batch_tester =
   290   gen_mk_tester (AList.lookup (op =) o fst o snd o fst o Data.get o Context.Proof);
   291 val mk_batch_validator =
   292   gen_mk_tester (AList.lookup (op =) o snd o snd o fst o Data.get o Context.Proof);
   293 
   294 
   295 (* testing propositions *)
   296 
   297 type compile_generator =
   298   Proof.context -> (term * term list) list -> int list -> term list option * report option;
   299 
   300 fun limit timeout (limit_time, is_interactive) f exc () =
   301   if limit_time then
   302     TimeLimit.timeLimit timeout f ()
   303       handle TimeLimit.TimeOut =>
   304         if is_interactive then exc () else raise TimeLimit.TimeOut
   305   else f ();
   306 
   307 fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s;
   308 
   309 fun verbose_message ctxt s =
   310   if not (Config.get ctxt quiet) andalso Config.get ctxt verbose
   311   then Output.urgent_message s else ();
   312 
   313 fun test_terms ctxt (limit_time, is_interactive) insts goals =
   314   (case active_testers ctxt of
   315     [] => error "No active testers for quickcheck"
   316   | testers =>
   317       limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
   318         (fn () =>
   319           Par_List.get_some (fn tester =>
   320             tester ctxt (length testers > 1) insts goals |>
   321             (fn result => if exists found_counterexample result then SOME result else NONE))
   322           testers)
   323         (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ());
   324 
   325 fun all_axioms_of ctxt t =
   326   let
   327     val intros = Locale.get_intros ctxt;
   328     val unfolds = Locale.get_unfolds ctxt;
   329     fun retrieve_prems thms t =
   330        (case filter (fn th => Term.could_unify (Thm.concl_of th, t)) thms of
   331          [] => NONE
   332        | [th] =>
   333            let
   334              val (tyenv, tenv) =
   335                Pattern.match (Proof_Context.theory_of ctxt)
   336                 (Thm.concl_of th, t) (Vartab.empty, Vartab.empty)
   337            in SOME (map (Envir.subst_term (tyenv, tenv)) (Thm.prems_of th)) end);
   338     fun all t =
   339       (case retrieve_prems intros t of
   340         NONE => retrieve_prems unfolds t
   341       | SOME ts => SOME (maps (fn t => the_default [t] (all t)) ts));
   342   in
   343     all t
   344   end;
   345 
   346 fun locale_config_of s =
   347   let
   348     val cs = space_explode " " s;
   349   in
   350     if forall (fn c => c = "expand" orelse c = "interpret") cs then cs
   351     else
   352      (warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
   353       ["interpret", "expand"])
   354   end;
   355 
   356 fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
   357   let
   358     val lthy = Proof.context_of state;
   359     val thy = Proof.theory_of state;
   360     val _ = message lthy "Quickchecking..."
   361     fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t
   362       | strip t = t;
   363     val {goal = st, ...} = Proof.raw_goal state;
   364     val (gi, frees) = Logic.goal_params (prop_of st) i;
   365     val some_locale = Named_Target.bottom_locale_of lthy;
   366     val assms =
   367       if Config.get lthy no_assms then []
   368       else
   369         (case some_locale of
   370           NONE => Assumption.all_assms_of lthy
   371         | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy));
   372     val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
   373     fun axioms_of locale =
   374       (case fst (Locale.specification_of thy locale) of
   375         NONE => []
   376       | SOME t => the_default [] (all_axioms_of lthy t));
   377     val config = locale_config_of (Config.get lthy locale);
   378     val goals =
   379       (case some_locale of
   380         NONE => [(proto_goal, eval_terms)]
   381       | SOME locale =>
   382           fold (fn c =>
   383             if c = "expand" then
   384               cons (Logic.list_implies (axioms_of locale, proto_goal), eval_terms)
   385             else if c = "interpret" then
   386               append (map (fn (_, phi) =>
   387                   (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
   388                 (Locale.registrations_of (Context.Theory thy) (* FIXME !? *) locale))
   389             else I) config []);
   390     val _ =
   391       verbose_message lthy
   392         (Pretty.string_of
   393           (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term lthy o fst) goals)));
   394   in
   395     test_terms lthy (time_limit, is_interactive) insts goals
   396   end;
   397 
   398 
   399 (* pretty printing *)
   400 
   401 fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck";
   402 
   403 fun pretty_counterex ctxt auto NONE =
   404       Pretty.str (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
   405   | pretty_counterex ctxt auto (SOME ((genuine, cex), eval_terms)) =
   406       (Pretty.text_fold o Pretty.fbreaks)
   407        (Pretty.str (tool_name auto ^ " found a " ^
   408          (if genuine then "counterexample:"
   409           else "potentially spurious counterexample due to underspecified functions:") ^
   410         Config.get ctxt tag) ::
   411         Pretty.str "" ::
   412         map (fn (s, t) =>
   413           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex) @
   414         (if null eval_terms then []
   415          else
   416           Pretty.str "" :: Pretty.str "Evaluated terms:" ::
   417             map (fn (t, u) =>
   418               Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
   419                 Syntax.pretty_term ctxt u]) (rev eval_terms)));
   420 
   421 
   422 (* Isar commands *)
   423 
   424 fun read_nat s =
   425   (case Library.read_int (Symbol.explode s) of
   426     (k, []) =>
   427       if k >= 0 then k
   428       else error ("Not a natural number: " ^ s)
   429   | _ => error ("Not a natural number: " ^ s));
   430 
   431 fun read_bool "false" = false
   432   | read_bool "true" = true
   433   | read_bool s = error ("Not a Boolean value: " ^ s);
   434 
   435 fun read_real s =
   436   (case Real.fromString s of
   437     SOME s => s
   438   | NONE => error ("Not a real number: " ^ s));
   439 
   440 fun read_expectation "no_expectation" = No_Expectation
   441   | read_expectation "no_counterexample" = No_Counterexample
   442   | read_expectation "counterexample" = Counterexample
   443   | read_expectation s = error ("Not an expectation value: " ^ s);
   444 
   445 fun valid_tester_name genctxt name =
   446   AList.defined (op =) (fst (fst (Data.get genctxt))) name;
   447 
   448 fun parse_tester name (testers, genctxt) =
   449   if valid_tester_name genctxt name then
   450     (insert (op =) name testers, genctxt)
   451   else error ("Unknown tester: " ^ name);
   452 
   453 fun parse_test_param ("tester", args) = fold parse_tester args
   454   | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg))
   455   | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg))
   456   | parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg))
   457   | parse_test_param ("default_type", arg) =
   458       (fn (testers, context) =>
   459         (testers, map_test_params
   460           (apfst (K (map (Proof_Context.read_typ (Context.proof_of context)) arg))) context))
   461   | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
   462   | parse_test_param ("expect", [arg]) = apsnd (map_test_params (apsnd (K (read_expectation arg))))
   463   | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
   464   | parse_test_param ("genuine_only", [arg]) =
   465       apsnd (Config.put_generic genuine_only (read_bool arg))
   466   | parse_test_param ("abort_potential", [arg]) =
   467       apsnd (Config.put_generic abort_potential (read_bool arg))
   468   | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
   469   | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
   470   | parse_test_param ("tag", [arg]) = apsnd (Config.put_generic tag arg)
   471   | parse_test_param ("use_subtype", [arg]) =
   472       apsnd (Config.put_generic use_subtype (read_bool arg))
   473   | parse_test_param ("timeout", [arg]) =
   474       apsnd (Config.put_generic timeout (read_real arg))
   475   | parse_test_param ("finite_types", [arg]) =
   476       apsnd (Config.put_generic finite_types (read_bool arg))
   477   | parse_test_param ("allow_function_inversion", [arg]) =
   478       apsnd (Config.put_generic allow_function_inversion (read_bool arg))
   479   | parse_test_param ("finite_type_size", [arg]) =
   480       apsnd (Config.put_generic finite_type_size (read_nat arg))
   481   | parse_test_param (name, _) =
   482       (fn (testers, genctxt) =>
   483         if valid_tester_name genctxt name then
   484           (insert (op =) name testers, genctxt)
   485         else error ("Unknown tester or test parameter: " ^ name));
   486 
   487 fun parse_test_param_inst (name, arg) ((insts, eval_terms), (testers, ctxt)) =
   488   (case try (Proof_Context.read_typ ctxt) name of
   489     SOME (TFree (v, _)) =>
   490       ((AList.update (op =) (v, Proof_Context.read_typ ctxt (the_single arg)) insts, eval_terms),
   491         (testers, ctxt))
   492   | NONE =>
   493       (case name of
   494         "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), (testers, ctxt))
   495       | _ =>
   496         ((insts, eval_terms),
   497           let
   498             val (testers', Context.Proof ctxt') =
   499               parse_test_param (name, arg) (testers, Context.Proof ctxt);
   500           in (testers', ctxt') end)));
   501 
   502 fun quickcheck_params_cmd args =
   503   Context.theory_map
   504     (fn context => uncurry set_active_testers (fold parse_test_param args ([], context)));
   505 
   506 fun check_expectation state results =
   507   if is_some results andalso expect (Proof.context_of state) = No_Counterexample then
   508     error "quickcheck expected to find no counterexample but found one"
   509   else if is_none results andalso expect (Proof.context_of state) = Counterexample then
   510     error "quickcheck expected to find a counterexample but did not find one"
   511   else ();
   512 
   513 fun gen_quickcheck args i state =
   514   state
   515   |> Proof.map_context_result (fn ctxt =>
   516     apsnd (fn (testers, ctxt) => Context.proof_map (set_active_testers testers) ctxt)
   517       (fold parse_test_param_inst args (([], []), ([], ctxt))))
   518   |> (fn ((insts, eval_terms), state') =>
   519       test_goal (true, true) (insts, eval_terms) i state'
   520       |> tap (check_expectation state')
   521       |> rpair state');
   522 
   523 fun quickcheck args i state =
   524   Option.map (the o get_first counterexample_of) (fst (gen_quickcheck args i state));
   525 
   526 fun quickcheck_cmd args i state =
   527   gen_quickcheck args i (Toplevel.proof_of state)
   528   |> apfst (Option.map (the o get_first response_of))
   529   |> (fn (r, state) =>
   530       Output.urgent_message (Pretty.string_of
   531         (pretty_counterex (Proof.context_of state) false r)));
   532 
   533 val parse_arg =
   534   Parse.name --
   535     (Scan.optional (@{keyword "="} |--
   536       (((Parse.name || Parse.float_number) >> single) ||
   537         (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}))) ["true"]);
   538 
   539 val parse_args =
   540   @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
   541 
   542 val _ =
   543   Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing"
   544     (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
   545 
   546 val _ =
   547   Outer_Syntax.improper_command @{command_spec "quickcheck"}
   548     "try to find counterexample for subgoal"
   549     (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
   550       Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
   551 
   552 
   553 (* automatic testing *)
   554 
   555 fun try_quickcheck auto state =
   556   let
   557     val ctxt = Proof.context_of state;
   558     val i = 1;
   559     val res =
   560       state
   561       |> Proof.map_context (Config.put report false #> Config.put quiet true)
   562       |> try (test_goal (false, false) ([], []) i);
   563   in
   564     (case res of
   565       NONE => (unknownN, state)
   566     | SOME results =>
   567         let
   568           val msg = pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)
   569         in
   570           if is_some results then
   571             (genuineN,
   572              state
   573              |> (if auto then
   574                    Proof.goal_message (K (Pretty.mark Markup.information msg))
   575                  else
   576                    tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
   577           else
   578             (noneN, state)
   579         end)
   580   end
   581   |> `(fn (outcome_code, _) => outcome_code = genuineN);
   582 
   583 val _ = Try.tool_setup (quickcheckN, (20, @{system_option auto_quickcheck}, try_quickcheck));
   584 
   585 end;
   586