# HG changeset patch # User blanchet # Date 1256748223 -3600 # Node ID ab01b72715ef30505b2c409bcda8108401661f6e # Parent b12ab081e5d1cc7e16e290b1ded52ef944b1fdc5 introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian diff -r b12ab081e5d1 -r ab01b72715ef doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Wed Oct 28 11:55:48 2009 +0100 +++ b/doc-src/Nitpick/nitpick.tex Wed Oct 28 17:43:43 2009 +0100 @@ -112,6 +112,13 @@ machine called \texttt{java}. The examples presented in this manual can be found in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory. +Throughout this manual, we will explicitly invoke the \textbf{nitpick} command. +Nitpick also provides an automatic mode that can be enabled using the +``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this +mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck. +The collective time limit for Auto Nitpick and Auto Quickcheck can be set using +the ``Auto Counterexample Time Limit'' option. + \newbox\boxA \setbox\boxA=\hbox{\texttt{nospam}} @@ -154,16 +161,6 @@ configured SAT solvers in Isabelle (e.g., for Refute), these will also be available to Nitpick. -Throughout this manual, we will explicitly invoke the \textbf{nitpick} command. -Nitpick also provides an automatic mode that can be enabled by specifying - -\prew -\textbf{nitpick\_params} [\textit{auto}] -\postw - -at the beginning of the theory file. In this mode, Nitpick is run for up to 5 -seconds (by default) on every newly entered theorem, much like Auto Quickcheck. - \subsection{Propositional Logic} \label{propositional-logic} @@ -1595,6 +1592,17 @@ (\S\ref{authentication}), optimizations (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}). +You can instruct Nitpick to run automatically on newly entered theorems by +enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof +General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) +and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled, +\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose} +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are +disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and +\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample +Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more +concise. + The number of options can be overwhelming at first glance. Do not let that worry you: Nitpick's defaults have been chosen so that it almost always does the right thing, and the most important options have been covered in context in @@ -1622,35 +1630,19 @@ \end{enum} Default values are indicated in square brackets. Boolean options have a negated -counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean -options, ``= \textit{true}'' may be omitted. +counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting +Boolean options, ``= \textit{true}'' may be omitted. \subsection{Mode of Operation} \label{mode-of-operation} \begin{enum} -\opfalse{auto}{no\_auto} -Specifies whether Nitpick should be run automatically on newly entered theorems. -For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and -\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled, -\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose} -(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are -disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and -\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of -\textit{timeout} (\S\ref{timeouts}). The output is also more concise. - -\nopagebreak -{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).} - \optrue{blocking}{non\_blocking} Specifies whether the \textbf{nitpick} command should operate synchronously. The asynchronous (non-blocking) mode lets the user start proving the putative theorem while Nitpick looks for a counterexample, but it can also be more confusing. For technical reasons, automatic runs currently always block. -\nopagebreak -{\small See also \textit{auto} (\S\ref{mode-of-operation}).} - \optrue{falsify}{satisfy} Specifies whether Nitpick should look for falsifying examples (countermodels) or satisfying examples (models). This manual assumes throughout that @@ -1670,16 +1662,15 @@ considered. \nopagebreak -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms} -(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).} +{\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug} +(\S\ref{output-format}).} \optrue{assms}{no\_assms} Specifies whether the relevant assumptions in structured proof should be considered. The option is implicitly enabled for automatic runs. \nopagebreak -{\small See also \textit{auto} (\S\ref{mode-of-operation}) -and \textit{user\_axioms} (\S\ref{mode-of-operation}).} +{\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).} \opfalse{overlord}{no\_overlord} Specifies whether Nitpick should put its temporary files in @@ -1861,9 +1852,6 @@ option is useful to determine which scopes are tried or which SAT solver is used. This option is implicitly disabled for automatic runs. -\nopagebreak -{\small See also \textit{auto} (\S\ref{mode-of-operation}).} - \opfalse{debug}{no\_debug} Specifies whether Nitpick should display additional debugging information beyond what \textit{verbose} already displays. Enabling \textit{debug} also enables @@ -1871,8 +1859,8 @@ option is implicitly disabled for automatic runs. \nopagebreak -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord} -(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).} +{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and +\textit{batch\_size} (\S\ref{optimizations}).} \optrue{show\_skolems}{hide\_skolem} Specifies whether the values of Skolem constants should be displayed as part of @@ -1910,8 +1898,7 @@ enabled. \nopagebreak -{\small See also \textit{auto} (\S\ref{mode-of-operation}), -\textit{check\_potential} (\S\ref{authentication}), and +{\small See also \textit{check\_potential} (\S\ref{authentication}) and \textit{sat\_solver} (\S\ref{optimizations}).} \opt{max\_genuine}{int}{$\mathbf{1}$} @@ -1968,8 +1955,7 @@ shown to be genuine, Nitpick displays a message to this effect and terminates. \nopagebreak -{\small See also \textit{max\_potential} (\S\ref{output-format}) and -\textit{auto\_timeout} (\S\ref{timeouts}).} +{\small See also \textit{max\_potential} (\S\ref{output-format}).} \opfalse{check\_genuine}{trust\_genuine} Specifies whether genuine and likely genuine counterexamples should be given to @@ -1979,8 +1965,7 @@ \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}. \nopagebreak -{\small See also \textit{max\_genuine} (\S\ref{output-format}) and -\textit{auto\_timeout} (\S\ref{timeouts}).} +{\small See also \textit{max\_genuine} (\S\ref{output-format}).} \ops{expect}{string} Specifies the expected outcome, which must be one of the following: @@ -2206,19 +2191,12 @@ Specifies the maximum amount of time that the \textbf{nitpick} command should spend looking for a counterexample. Nitpick tries to honor this constraint as well as it can but offers no guarantees. For automatic runs, -\textit{auto\_timeout} is used instead. +\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share +a time slot whose length is specified by the ``Auto Counterexample Time +Limit'' option in Proof General. \nopagebreak -{\small See also \textit{auto} (\S\ref{mode-of-operation}) -and \textit{max\_threads} (\S\ref{optimizations}).} - -\opt{auto\_timeout}{time}{$\mathbf{5}$ s} -Specifies the maximum amount of time that Nitpick should use to find a -counterexample when running automatically. Nitpick tries to honor this -constraint as well as it can but offers no guarantees. - -\nopagebreak -{\small See also \textit{auto} (\S\ref{mode-of-operation}).} +{\small See also \textit{max\_threads} (\S\ref{optimizations}).} \opt{tac\_timeout}{time}{$\mathbf{500}$\,ms} Specifies the maximum amount of time that the \textit{auto} tactic should use diff -r b12ab081e5d1 -r ab01b72715ef src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Oct 28 11:55:48 2009 +0100 +++ b/src/HOL/IsaMakefile Wed Oct 28 17:43:43 2009 +0100 @@ -101,6 +101,7 @@ $(SRC)/Provers/hypsubst.ML \ $(SRC)/Provers/quantifier1.ML \ $(SRC)/Provers/splitter.ML \ + $(SRC)/Tools/Auto_Counterexample.thy \ $(SRC)/Tools/Code/code_haskell.ML \ $(SRC)/Tools/Code/code_ml.ML \ $(SRC)/Tools/Code/code_preproc.ML \ @@ -113,6 +114,7 @@ $(SRC)/Tools/IsaPlanner/rw_tools.ML \ $(SRC)/Tools/IsaPlanner/zipper.ML \ $(SRC)/Tools/atomize_elim.ML \ + $(SRC)/Tools/auto_counterexample.ML \ $(SRC)/Tools/auto_solve.ML \ $(SRC)/Tools/coherent.ML \ $(SRC)/Tools/cong_tac.ML \ diff -r b12ab081e5d1 -r ab01b72715ef src/HOL/Main.thy --- a/src/HOL/Main.thy Wed Oct 28 11:55:48 2009 +0100 +++ b/src/HOL/Main.thy Wed Oct 28 17:43:43 2009 +0100 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Plain Nitpick Quickcheck Recdef +imports Plain Nitpick begin text {* diff -r b12ab081e5d1 -r ab01b72715ef src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Wed Oct 28 11:55:48 2009 +0100 +++ b/src/HOL/Nitpick.thy Wed Oct 28 17:43:43 2009 +0100 @@ -8,7 +8,7 @@ header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *} theory Nitpick -imports Map SAT +imports Map Quickcheck SAT uses ("Tools/Nitpick/kodkod.ML") ("Tools/Nitpick/kodkod_sat.ML") ("Tools/Nitpick/nitpick_util.ML") @@ -241,6 +241,8 @@ use "Tools/Nitpick/nitpick_tests.ML" use "Tools/Nitpick/minipick.ML" +setup {* Nitpick_Isar.setup *} + hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac diff -r b12ab081e5d1 -r ab01b72715ef src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Wed Oct 28 11:55:48 2009 +0100 +++ b/src/HOL/Quickcheck.thy Wed Oct 28 17:43:43 2009 +0100 @@ -126,6 +126,8 @@ shows "random_aux k = rhs k" using assms by (rule code_numeral.induct) +setup {* Quickcheck.setup *} + use "Tools/quickcheck_generators.ML" setup {* Quickcheck_Generators.setup *} diff -r b12ab081e5d1 -r ab01b72715ef src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Oct 28 11:55:48 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Oct 28 17:43:43 2009 +0100 @@ -187,7 +187,7 @@ val pprint = if auto then Unsynchronized.change state_ref o Proof.goal_message o K - o curry Pretty.blk 0 o cons (Pretty.str "") o single + o Pretty.chunks o cons (Pretty.str "") o single o Pretty.mark Markup.hilite else priority o Pretty.string_of diff -r b12ab081e5d1 -r ab01b72715ef src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Oct 28 11:55:48 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Oct 28 17:43:43 2009 +0100 @@ -10,7 +10,9 @@ sig type params = Nitpick.params + val auto: bool Unsynchronized.ref val default_params : theory -> (string * string) list -> params + val setup : theory -> theory end structure Nitpick_Isar : NITPICK_ISAR = @@ -22,6 +24,14 @@ open Nitpick_Nut open Nitpick +val auto = Unsynchronized.ref false; + +val _ = ProofGeneralPgip.add_preference Preferences.category_tracing + (setmp_CRITICAL auto false + (fn () => Preferences.bool_pref auto + "auto-nitpick" + "Whether to run Nitpick automatically.") ()) + type raw_param = string * string list val default_default_params = @@ -33,7 +43,6 @@ ("wf", ["smart"]), ("sat_solver", ["smart"]), ("batch_size", ["smart"]), - ("auto", ["false"]), ("blocking", ["true"]), ("falsify", ["true"]), ("user_axioms", ["smart"]), @@ -47,7 +56,6 @@ ("fast_descrs", ["true"]), ("peephole_optim", ["true"]), ("timeout", ["30 s"]), - ("auto_timeout", ["5 s"]), ("tac_timeout", ["500 ms"]), ("sym_break", ["20"]), ("sharing_depth", ["3"]), @@ -70,7 +78,6 @@ [("dont_box", "box"), ("non_mono", "mono"), ("non_wf", "wf"), - ("no_auto", "auto"), ("non_blocking", "blocking"), ("satisfy", "falsify"), ("no_user_axioms", "user_axioms"), @@ -126,31 +133,22 @@ | NONE => (name, value) structure TheoryData = TheoryDataFun( - type T = {params: raw_param list, registered_auto: bool} - val empty = {params = rev default_default_params, registered_auto = false} + type T = {params: raw_param list} + val empty = {params = rev default_default_params} val copy = I val extend = I - fun merge _ ({params = ps1, registered_auto = a1}, - {params = ps2, registered_auto = a2}) = - {params = AList.merge (op =) (op =) (ps1, ps2), - registered_auto = a1 orelse a2}) + fun merge _ ({params = ps1}, {params = ps2}) = + {params = AList.merge (op =) (op =) (ps1, ps2)}) (* raw_param -> theory -> theory *) fun set_default_raw_param param thy = - let val {params, registered_auto} = TheoryData.get thy in + let val {params} = TheoryData.get thy in TheoryData.put - {params = AList.update (op =) (unnegate_raw_param param) params, - registered_auto = registered_auto} thy + {params = AList.update (op =) (unnegate_raw_param param) params} thy end (* theory -> raw_param list *) val default_raw_params = #params o TheoryData.get -(* theory -> theory *) -fun set_registered_auto thy = - TheoryData.put {params = default_raw_params thy, registered_auto = true} thy -(* theory -> bool *) -val is_registered_auto = #registered_auto o TheoryData.get - (* string -> bool *) fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\") @@ -313,8 +311,7 @@ val uncurry = lookup_bool "uncurry" val fast_descrs = lookup_bool "fast_descrs" val peephole_optim = lookup_bool "peephole_optim" - val timeout = if auto then lookup_time "auto_timeout" - else lookup_time "timeout" + val timeout = if auto then NONE else lookup_time "timeout" val tac_timeout = lookup_time "tac_timeout" val sym_break = Int.max (0, lookup_int "sym_break") val sharing_depth = Int.max (1, lookup_int "sharing_depth") @@ -326,8 +323,8 @@ val show_consts = show_all orelse lookup_bool "show_consts" val formats = lookup_ints_assigns read_term_polymorphic "format" 0 val evals = lookup_term_list "eval" - val max_potential = if auto then 0 - else Int.max (0, lookup_int "max_potential") + val max_potential = + if auto then 0 else Int.max (0, lookup_int "max_potential") val max_genuine = Int.max (0, lookup_int "max_genuine") val check_potential = lookup_bool "check_potential" val check_genuine = lookup_bool "check_genuine" @@ -412,79 +409,58 @@ | Refute.REFUTE (loc, details) => error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".") -(* raw_param list -> bool -> int -> Proof.state -> Proof.state *) +(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *) fun pick_nits override_params auto subgoal state = let val thy = Proof.theory_of state val ctxt = Proof.context_of state - val thm = snd (snd (Proof.get_goal state)) + val thm = state |> Proof.get_goal |> snd |> snd val _ = List.app check_raw_param override_params val params as {blocking, debug, ...} = extract_params ctxt auto (default_raw_params thy) override_params - (* unit -> Proof.state *) + (* unit -> bool * Proof.state *) fun go () = - (if auto then perhaps o try - else if debug then fn f => fn x => f x - else handle_exceptions ctxt) - (fn state => pick_nits_in_subgoal state params auto subgoal |> snd) - state + (false, state) + |> (if auto then perhaps o try + else if debug then fn f => fn x => f x + else handle_exceptions ctxt) + (fn (_, state) => pick_nits_in_subgoal state params auto subgoal + |>> equal "genuine") in - if auto orelse blocking then - go () - else - (SimpleThread.fork true (fn () => (go (); ())); - state) + if auto orelse blocking then go () + else (SimpleThread.fork true (fn () => (go (); ())); (false, state)) end (* (TableFun().key * string list) list option * int option -> Toplevel.transition -> Toplevel.transition *) fun nitpick_trans (opt_params, opt_subgoal) = Toplevel.keep (K () - o pick_nits (these opt_params) false (the_default 1 opt_subgoal) + o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal) o Toplevel.proof_of) (* raw_param -> string *) fun string_for_raw_param (name, value) = name ^ " = " ^ stringify_raw_param_value value -(* bool -> Proof.state -> Proof.state *) -fun pick_nits_auto interactive state = - let val thy = Proof.theory_of state in - ((interactive andalso not (!Toplevel.quiet) - andalso the (general_lookup_bool false (default_raw_params thy) - (SOME false) "auto")) - ? pick_nits [] true 0) state - end - -(* theory -> theory *) -fun register_auto thy = - (not (is_registered_auto thy) - ? (set_registered_auto - #> Context.theory_map (Specification.add_theorem_hook pick_nits_auto))) - thy - (* (TableFun().key * string) list option -> Toplevel.transition -> Toplevel.transition *) fun nitpick_params_trans opt_params = Toplevel.theory - (fn thy => - let val thy = fold set_default_raw_param (these opt_params) thy in - writeln ("Default parameters for Nitpick:\n" ^ - (case rev (default_raw_params thy) of - [] => "none" - | params => - (map check_raw_param params; - params |> map string_for_raw_param |> sort_strings - |> cat_lines))); - register_auto thy - end) + (fold set_default_raw_param (these opt_params) + #> tap (fn thy => + writeln ("Default parameters for Nitpick:\n" ^ + (case rev (default_raw_params thy) of + [] => "none" + | params => + (map check_raw_param params; + params |> map string_for_raw_param + |> sort_strings |> cat_lines))))) (* OuterParse.token list -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *) -fun scan_nitpick_command tokens = - (scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans -fun scan_nitpick_params_command tokens = - scan_params tokens |>> nitpick_params_trans +val scan_nitpick_command = + (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans +val scan_nitpick_params_command = scan_params #>> nitpick_params_trans val _ = OuterSyntax.improper_command "nitpick" "try to find a counterexample for a given subgoal using Kodkod" @@ -493,4 +469,10 @@ "set and display the default parameters for Nitpick" OuterKeyword.thy_decl scan_nitpick_params_command +(* Proof.state -> bool * Proof.state *) +fun auto_nitpick state = + if not (!auto) then (false, state) else pick_nits [] true 1 state + +val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick) + end; diff -r b12ab081e5d1 -r ab01b72715ef src/Tools/Auto_Counterexample.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Auto_Counterexample.thy Wed Oct 28 17:43:43 2009 +0100 @@ -0,0 +1,15 @@ +(* Title: Tools/Auto_Counterexample.thy + Author: Jasmin Blanchette, TU Muenchen + +Counterexample Search Unit (do not abbreviate!). +*) + +header {* Counterexample Search Unit *} + +theory Auto_Counterexample +imports Pure +uses + "~~/src/Tools/auto_counterexample.ML" +begin + +end diff -r b12ab081e5d1 -r ab01b72715ef src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Wed Oct 28 11:55:48 2009 +0100 +++ b/src/Tools/Code_Generator.thy Wed Oct 28 17:43:43 2009 +0100 @@ -5,7 +5,7 @@ header {* Loading the code generator modules *} theory Code_Generator -imports Pure +imports Auto_Counterexample uses "~~/src/Tools/value.ML" "~~/src/Tools/quickcheck.ML" @@ -25,4 +25,4 @@ #> Nbe.setup *} -end \ No newline at end of file +end diff -r b12ab081e5d1 -r ab01b72715ef src/Tools/auto_counterexample.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/auto_counterexample.ML Wed Oct 28 17:43:43 2009 +0100 @@ -0,0 +1,59 @@ +(* Title: Tools/auto_counterexample.ML + Author: Jasmin Blanchette, TU Muenchen + +Counterexample Search Unit (do not abbreviate!). +*) + +signature AUTO_COUNTEREXAMPLE = +sig + val time_limit: int Unsynchronized.ref + + val register_tool : + string * (Proof.state -> bool * Proof.state) -> theory -> theory +end; + +structure Auto_Counterexample : AUTO_COUNTEREXAMPLE = +struct + +(* preferences *) + +val time_limit = Unsynchronized.ref 2500 + +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing + (Preferences.nat_pref time_limit + "auto-counterexample-time-limit" + "Time limit for automatic counterexample search (in milliseconds).") + + +(* configuration *) + +structure Data = TheoryDataFun( + type T = (string * (Proof.state -> bool * Proof.state)) list + val empty = [] + val copy = I + val extend = I + fun merge _ (tools1, tools2) = AList.merge (op =) (K true) (tools1, tools2) +) + +val register_tool = Data.map o AList.update (op =) + + +(* automatic testing *) + +val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => + case !time_limit of + 0 => state + | ms => + TimeLimit.timeLimit (Time.fromMilliseconds ms) + (fn () => + if interact andalso not (!Toplevel.quiet) then + fold_rev (fn (_, tool) => fn (true, state) => (true, state) + | (false, state) => tool state) + (Data.get (Proof.theory_of state)) (false, state) |> snd + else + state) () + handle TimeLimit.TimeOut => + (warning "Automatic counterexample search timed out."; state))) + +end; diff -r b12ab081e5d1 -r ab01b72715ef src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Wed Oct 28 11:55:48 2009 +0100 +++ b/src/Tools/quickcheck.ML Wed Oct 28 17:43:43 2009 +0100 @@ -7,10 +7,10 @@ signature QUICKCHECK = sig val auto: bool Unsynchronized.ref - val auto_time_limit: int Unsynchronized.ref val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory + val setup: theory -> theory val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option end; @@ -20,20 +20,13 @@ (* preferences *) val auto = Unsynchronized.ref false; -val auto_time_limit = Unsynchronized.ref 2500; val _ = ProofGeneralPgip.add_preference Preferences.category_tracing (setmp_CRITICAL auto true (fn () => Preferences.bool_pref auto "auto-quickcheck" - "Whether to enable quickcheck automatically.") ()); - -val _ = - ProofGeneralPgip.add_preference Preferences.category_tracing - (Preferences.nat_pref auto_time_limit - "auto-quickcheck-time-limit" - "Time limit for automatic quickcheck (in milliseconds)."); + "Whether to run Quickcheck automatically.") ()); (* quickcheck configuration -- default parameters, test generators *) @@ -159,28 +152,26 @@ (* automatic testing *) -val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state => - let - val ctxt = Proof.context_of state; - val assms = map term_of (Assumption.all_assms_of ctxt); - val Test_Params { size, iterations, default_type } = - (snd o Data.get o Proof.theory_of) state; - fun test () = - let - val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit)) - (try (test_goal true NONE size iterations default_type [] 1 assms)) state; - in - case res of - NONE => state - | SOME NONE => state - | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "", - Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state - end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state); - in - if int andalso !auto andalso not (!Toplevel.quiet) - then test () - else state - end)); +fun auto_quickcheck state = + if not (!auto) then + (false, state) + else + let + val ctxt = Proof.context_of state; + val assms = map term_of (Assumption.all_assms_of ctxt); + val Test_Params { size, iterations, default_type } = + (snd o Data.get o Proof.theory_of) state; + val res = + try (test_goal true NONE size iterations default_type [] 1 assms) state; + in + case res of + NONE => (false, state) + | SOME NONE => (false, state) + | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "", + Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state) + end + +val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck) (* Isar commands *) @@ -251,4 +242,3 @@ val auto_quickcheck = Quickcheck.auto; -val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;