1.1 --- a/doc-src/Nitpick/nitpick.tex Wed Oct 28 11:55:48 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Wed Oct 28 17:43:43 2009 +0100
1.3 @@ -112,6 +112,13 @@
1.4 machine called \texttt{java}. The examples presented in this manual can be found
1.5 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
1.6
1.7 +Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
1.8 +Nitpick also provides an automatic mode that can be enabled using the
1.9 +``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
1.10 +mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
1.11 +The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
1.12 +the ``Auto Counterexample Time Limit'' option.
1.13 +
1.14 \newbox\boxA
1.15 \setbox\boxA=\hbox{\texttt{nospam}}
1.16
1.17 @@ -154,16 +161,6 @@
1.18 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
1.19 available to Nitpick.
1.20
1.21 -Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
1.22 -Nitpick also provides an automatic mode that can be enabled by specifying
1.23 -
1.24 -\prew
1.25 -\textbf{nitpick\_params} [\textit{auto}]
1.26 -\postw
1.27 -
1.28 -at the beginning of the theory file. In this mode, Nitpick is run for up to 5
1.29 -seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
1.30 -
1.31 \subsection{Propositional Logic}
1.32 \label{propositional-logic}
1.33
1.34 @@ -1595,6 +1592,17 @@
1.35 (\S\ref{authentication}), optimizations
1.36 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
1.37
1.38 +You can instruct Nitpick to run automatically on newly entered theorems by
1.39 +enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
1.40 +General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
1.41 +and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
1.42 +\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
1.43 +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
1.44 +disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
1.45 +\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
1.46 +Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
1.47 +concise.
1.48 +
1.49 The number of options can be overwhelming at first glance. Do not let that worry
1.50 you: Nitpick's defaults have been chosen so that it almost always does the right
1.51 thing, and the most important options have been covered in context in
1.52 @@ -1622,35 +1630,19 @@
1.53 \end{enum}
1.54
1.55 Default values are indicated in square brackets. Boolean options have a negated
1.56 -counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
1.57 -options, ``= \textit{true}'' may be omitted.
1.58 +counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
1.59 +Boolean options, ``= \textit{true}'' may be omitted.
1.60
1.61 \subsection{Mode of Operation}
1.62 \label{mode-of-operation}
1.63
1.64 \begin{enum}
1.65 -\opfalse{auto}{no\_auto}
1.66 -Specifies whether Nitpick should be run automatically on newly entered theorems.
1.67 -For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
1.68 -\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
1.69 -\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
1.70 -(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
1.71 -disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
1.72 -\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
1.73 -\textit{timeout} (\S\ref{timeouts}). The output is also more concise.
1.74 -
1.75 -\nopagebreak
1.76 -{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
1.77 -
1.78 \optrue{blocking}{non\_blocking}
1.79 Specifies whether the \textbf{nitpick} command should operate synchronously.
1.80 The asynchronous (non-blocking) mode lets the user start proving the putative
1.81 theorem while Nitpick looks for a counterexample, but it can also be more
1.82 confusing. For technical reasons, automatic runs currently always block.
1.83
1.84 -\nopagebreak
1.85 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.86 -
1.87 \optrue{falsify}{satisfy}
1.88 Specifies whether Nitpick should look for falsifying examples (countermodels) or
1.89 satisfying examples (models). This manual assumes throughout that
1.90 @@ -1670,16 +1662,15 @@
1.91 considered.
1.92
1.93 \nopagebreak
1.94 -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
1.95 -(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
1.96 +{\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
1.97 +(\S\ref{output-format}).}
1.98
1.99 \optrue{assms}{no\_assms}
1.100 Specifies whether the relevant assumptions in structured proof should be
1.101 considered. The option is implicitly enabled for automatic runs.
1.102
1.103 \nopagebreak
1.104 -{\small See also \textit{auto} (\S\ref{mode-of-operation})
1.105 -and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1.106 +{\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1.107
1.108 \opfalse{overlord}{no\_overlord}
1.109 Specifies whether Nitpick should put its temporary files in
1.110 @@ -1861,9 +1852,6 @@
1.111 option is useful to determine which scopes are tried or which SAT solver is
1.112 used. This option is implicitly disabled for automatic runs.
1.113
1.114 -\nopagebreak
1.115 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.116 -
1.117 \opfalse{debug}{no\_debug}
1.118 Specifies whether Nitpick should display additional debugging information beyond
1.119 what \textit{verbose} already displays. Enabling \textit{debug} also enables
1.120 @@ -1871,8 +1859,8 @@
1.121 option is implicitly disabled for automatic runs.
1.122
1.123 \nopagebreak
1.124 -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord}
1.125 -(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).}
1.126 +{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
1.127 +\textit{batch\_size} (\S\ref{optimizations}).}
1.128
1.129 \optrue{show\_skolems}{hide\_skolem}
1.130 Specifies whether the values of Skolem constants should be displayed as part of
1.131 @@ -1910,8 +1898,7 @@
1.132 enabled.
1.133
1.134 \nopagebreak
1.135 -{\small See also \textit{auto} (\S\ref{mode-of-operation}),
1.136 -\textit{check\_potential} (\S\ref{authentication}), and
1.137 +{\small See also \textit{check\_potential} (\S\ref{authentication}) and
1.138 \textit{sat\_solver} (\S\ref{optimizations}).}
1.139
1.140 \opt{max\_genuine}{int}{$\mathbf{1}$}
1.141 @@ -1968,8 +1955,7 @@
1.142 shown to be genuine, Nitpick displays a message to this effect and terminates.
1.143
1.144 \nopagebreak
1.145 -{\small See also \textit{max\_potential} (\S\ref{output-format}) and
1.146 -\textit{auto\_timeout} (\S\ref{timeouts}).}
1.147 +{\small See also \textit{max\_potential} (\S\ref{output-format}).}
1.148
1.149 \opfalse{check\_genuine}{trust\_genuine}
1.150 Specifies whether genuine and likely genuine counterexamples should be given to
1.151 @@ -1979,8 +1965,7 @@
1.152 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
1.153
1.154 \nopagebreak
1.155 -{\small See also \textit{max\_genuine} (\S\ref{output-format}) and
1.156 -\textit{auto\_timeout} (\S\ref{timeouts}).}
1.157 +{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
1.158
1.159 \ops{expect}{string}
1.160 Specifies the expected outcome, which must be one of the following:
1.161 @@ -2206,19 +2191,12 @@
1.162 Specifies the maximum amount of time that the \textbf{nitpick} command should
1.163 spend looking for a counterexample. Nitpick tries to honor this constraint as
1.164 well as it can but offers no guarantees. For automatic runs,
1.165 -\textit{auto\_timeout} is used instead.
1.166 +\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
1.167 +a time slot whose length is specified by the ``Auto Counterexample Time
1.168 +Limit'' option in Proof General.
1.169
1.170 \nopagebreak
1.171 -{\small See also \textit{auto} (\S\ref{mode-of-operation})
1.172 -and \textit{max\_threads} (\S\ref{optimizations}).}
1.173 -
1.174 -\opt{auto\_timeout}{time}{$\mathbf{5}$ s}
1.175 -Specifies the maximum amount of time that Nitpick should use to find a
1.176 -counterexample when running automatically. Nitpick tries to honor this
1.177 -constraint as well as it can but offers no guarantees.
1.178 -
1.179 -\nopagebreak
1.180 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.181 +{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
1.182
1.183 \opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
1.184 Specifies the maximum amount of time that the \textit{auto} tactic should use
2.1 --- a/src/HOL/IsaMakefile Wed Oct 28 11:55:48 2009 +0100
2.2 +++ b/src/HOL/IsaMakefile Wed Oct 28 17:43:43 2009 +0100
2.3 @@ -101,6 +101,7 @@
2.4 $(SRC)/Provers/hypsubst.ML \
2.5 $(SRC)/Provers/quantifier1.ML \
2.6 $(SRC)/Provers/splitter.ML \
2.7 + $(SRC)/Tools/Auto_Counterexample.thy \
2.8 $(SRC)/Tools/Code/code_haskell.ML \
2.9 $(SRC)/Tools/Code/code_ml.ML \
2.10 $(SRC)/Tools/Code/code_preproc.ML \
2.11 @@ -113,6 +114,7 @@
2.12 $(SRC)/Tools/IsaPlanner/rw_tools.ML \
2.13 $(SRC)/Tools/IsaPlanner/zipper.ML \
2.14 $(SRC)/Tools/atomize_elim.ML \
2.15 + $(SRC)/Tools/auto_counterexample.ML \
2.16 $(SRC)/Tools/auto_solve.ML \
2.17 $(SRC)/Tools/coherent.ML \
2.18 $(SRC)/Tools/cong_tac.ML \
3.1 --- a/src/HOL/Main.thy Wed Oct 28 11:55:48 2009 +0100
3.2 +++ b/src/HOL/Main.thy Wed Oct 28 17:43:43 2009 +0100
3.3 @@ -1,7 +1,7 @@
3.4 header {* Main HOL *}
3.5
3.6 theory Main
3.7 -imports Plain Nitpick Quickcheck Recdef
3.8 +imports Plain Nitpick
3.9 begin
3.10
3.11 text {*
4.1 --- a/src/HOL/Nitpick.thy Wed Oct 28 11:55:48 2009 +0100
4.2 +++ b/src/HOL/Nitpick.thy Wed Oct 28 17:43:43 2009 +0100
4.3 @@ -8,7 +8,7 @@
4.4 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
4.5
4.6 theory Nitpick
4.7 -imports Map SAT
4.8 +imports Map Quickcheck SAT
4.9 uses ("Tools/Nitpick/kodkod.ML")
4.10 ("Tools/Nitpick/kodkod_sat.ML")
4.11 ("Tools/Nitpick/nitpick_util.ML")
4.12 @@ -241,6 +241,8 @@
4.13 use "Tools/Nitpick/nitpick_tests.ML"
4.14 use "Tools/Nitpick/minipick.ML"
4.15
4.16 +setup {* Nitpick_Isar.setup *}
4.17 +
4.18 hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim
4.19 bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
4.20 fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
5.1 --- a/src/HOL/Quickcheck.thy Wed Oct 28 11:55:48 2009 +0100
5.2 +++ b/src/HOL/Quickcheck.thy Wed Oct 28 17:43:43 2009 +0100
5.3 @@ -126,6 +126,8 @@
5.4 shows "random_aux k = rhs k"
5.5 using assms by (rule code_numeral.induct)
5.6
5.7 +setup {* Quickcheck.setup *}
5.8 +
5.9 use "Tools/quickcheck_generators.ML"
5.10 setup {* Quickcheck_Generators.setup *}
5.11
6.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Oct 28 11:55:48 2009 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Oct 28 17:43:43 2009 +0100
6.3 @@ -187,7 +187,7 @@
6.4 val pprint =
6.5 if auto then
6.6 Unsynchronized.change state_ref o Proof.goal_message o K
6.7 - o curry Pretty.blk 0 o cons (Pretty.str "") o single
6.8 + o Pretty.chunks o cons (Pretty.str "") o single
6.9 o Pretty.mark Markup.hilite
6.10 else
6.11 priority o Pretty.string_of
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Oct 28 11:55:48 2009 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Oct 28 17:43:43 2009 +0100
7.3 @@ -10,7 +10,9 @@
7.4 sig
7.5 type params = Nitpick.params
7.6
7.7 + val auto: bool Unsynchronized.ref
7.8 val default_params : theory -> (string * string) list -> params
7.9 + val setup : theory -> theory
7.10 end
7.11
7.12 structure Nitpick_Isar : NITPICK_ISAR =
7.13 @@ -22,6 +24,14 @@
7.14 open Nitpick_Nut
7.15 open Nitpick
7.16
7.17 +val auto = Unsynchronized.ref false;
7.18 +
7.19 +val _ = ProofGeneralPgip.add_preference Preferences.category_tracing
7.20 + (setmp_CRITICAL auto false
7.21 + (fn () => Preferences.bool_pref auto
7.22 + "auto-nitpick"
7.23 + "Whether to run Nitpick automatically.") ())
7.24 +
7.25 type raw_param = string * string list
7.26
7.27 val default_default_params =
7.28 @@ -33,7 +43,6 @@
7.29 ("wf", ["smart"]),
7.30 ("sat_solver", ["smart"]),
7.31 ("batch_size", ["smart"]),
7.32 - ("auto", ["false"]),
7.33 ("blocking", ["true"]),
7.34 ("falsify", ["true"]),
7.35 ("user_axioms", ["smart"]),
7.36 @@ -47,7 +56,6 @@
7.37 ("fast_descrs", ["true"]),
7.38 ("peephole_optim", ["true"]),
7.39 ("timeout", ["30 s"]),
7.40 - ("auto_timeout", ["5 s"]),
7.41 ("tac_timeout", ["500 ms"]),
7.42 ("sym_break", ["20"]),
7.43 ("sharing_depth", ["3"]),
7.44 @@ -70,7 +78,6 @@
7.45 [("dont_box", "box"),
7.46 ("non_mono", "mono"),
7.47 ("non_wf", "wf"),
7.48 - ("no_auto", "auto"),
7.49 ("non_blocking", "blocking"),
7.50 ("satisfy", "falsify"),
7.51 ("no_user_axioms", "user_axioms"),
7.52 @@ -126,31 +133,22 @@
7.53 | NONE => (name, value)
7.54
7.55 structure TheoryData = TheoryDataFun(
7.56 - type T = {params: raw_param list, registered_auto: bool}
7.57 - val empty = {params = rev default_default_params, registered_auto = false}
7.58 + type T = {params: raw_param list}
7.59 + val empty = {params = rev default_default_params}
7.60 val copy = I
7.61 val extend = I
7.62 - fun merge _ ({params = ps1, registered_auto = a1},
7.63 - {params = ps2, registered_auto = a2}) =
7.64 - {params = AList.merge (op =) (op =) (ps1, ps2),
7.65 - registered_auto = a1 orelse a2})
7.66 + fun merge _ ({params = ps1}, {params = ps2}) =
7.67 + {params = AList.merge (op =) (op =) (ps1, ps2)})
7.68
7.69 (* raw_param -> theory -> theory *)
7.70 fun set_default_raw_param param thy =
7.71 - let val {params, registered_auto} = TheoryData.get thy in
7.72 + let val {params} = TheoryData.get thy in
7.73 TheoryData.put
7.74 - {params = AList.update (op =) (unnegate_raw_param param) params,
7.75 - registered_auto = registered_auto} thy
7.76 + {params = AList.update (op =) (unnegate_raw_param param) params} thy
7.77 end
7.78 (* theory -> raw_param list *)
7.79 val default_raw_params = #params o TheoryData.get
7.80
7.81 -(* theory -> theory *)
7.82 -fun set_registered_auto thy =
7.83 - TheoryData.put {params = default_raw_params thy, registered_auto = true} thy
7.84 -(* theory -> bool *)
7.85 -val is_registered_auto = #registered_auto o TheoryData.get
7.86 -
7.87 (* string -> bool *)
7.88 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
7.89
7.90 @@ -313,8 +311,7 @@
7.91 val uncurry = lookup_bool "uncurry"
7.92 val fast_descrs = lookup_bool "fast_descrs"
7.93 val peephole_optim = lookup_bool "peephole_optim"
7.94 - val timeout = if auto then lookup_time "auto_timeout"
7.95 - else lookup_time "timeout"
7.96 + val timeout = if auto then NONE else lookup_time "timeout"
7.97 val tac_timeout = lookup_time "tac_timeout"
7.98 val sym_break = Int.max (0, lookup_int "sym_break")
7.99 val sharing_depth = Int.max (1, lookup_int "sharing_depth")
7.100 @@ -326,8 +323,8 @@
7.101 val show_consts = show_all orelse lookup_bool "show_consts"
7.102 val formats = lookup_ints_assigns read_term_polymorphic "format" 0
7.103 val evals = lookup_term_list "eval"
7.104 - val max_potential = if auto then 0
7.105 - else Int.max (0, lookup_int "max_potential")
7.106 + val max_potential =
7.107 + if auto then 0 else Int.max (0, lookup_int "max_potential")
7.108 val max_genuine = Int.max (0, lookup_int "max_genuine")
7.109 val check_potential = lookup_bool "check_potential"
7.110 val check_genuine = lookup_bool "check_genuine"
7.111 @@ -412,79 +409,58 @@
7.112 | Refute.REFUTE (loc, details) =>
7.113 error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
7.114
7.115 -(* raw_param list -> bool -> int -> Proof.state -> Proof.state *)
7.116 +(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
7.117 fun pick_nits override_params auto subgoal state =
7.118 let
7.119 val thy = Proof.theory_of state
7.120 val ctxt = Proof.context_of state
7.121 - val thm = snd (snd (Proof.get_goal state))
7.122 + val thm = state |> Proof.get_goal |> snd |> snd
7.123 val _ = List.app check_raw_param override_params
7.124 val params as {blocking, debug, ...} =
7.125 extract_params ctxt auto (default_raw_params thy) override_params
7.126 - (* unit -> Proof.state *)
7.127 + (* unit -> bool * Proof.state *)
7.128 fun go () =
7.129 - (if auto then perhaps o try
7.130 - else if debug then fn f => fn x => f x
7.131 - else handle_exceptions ctxt)
7.132 - (fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
7.133 - state
7.134 + (false, state)
7.135 + |> (if auto then perhaps o try
7.136 + else if debug then fn f => fn x => f x
7.137 + else handle_exceptions ctxt)
7.138 + (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
7.139 + |>> equal "genuine")
7.140 in
7.141 - if auto orelse blocking then
7.142 - go ()
7.143 - else
7.144 - (SimpleThread.fork true (fn () => (go (); ()));
7.145 - state)
7.146 + if auto orelse blocking then go ()
7.147 + else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
7.148 end
7.149
7.150 (* (TableFun().key * string list) list option * int option
7.151 -> Toplevel.transition -> Toplevel.transition *)
7.152 fun nitpick_trans (opt_params, opt_subgoal) =
7.153 Toplevel.keep (K ()
7.154 - o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
7.155 + o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
7.156 o Toplevel.proof_of)
7.157
7.158 (* raw_param -> string *)
7.159 fun string_for_raw_param (name, value) =
7.160 name ^ " = " ^ stringify_raw_param_value value
7.161
7.162 -(* bool -> Proof.state -> Proof.state *)
7.163 -fun pick_nits_auto interactive state =
7.164 - let val thy = Proof.theory_of state in
7.165 - ((interactive andalso not (!Toplevel.quiet)
7.166 - andalso the (general_lookup_bool false (default_raw_params thy)
7.167 - (SOME false) "auto"))
7.168 - ? pick_nits [] true 0) state
7.169 - end
7.170 -
7.171 -(* theory -> theory *)
7.172 -fun register_auto thy =
7.173 - (not (is_registered_auto thy)
7.174 - ? (set_registered_auto
7.175 - #> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))
7.176 - thy
7.177 -
7.178 (* (TableFun().key * string) list option -> Toplevel.transition
7.179 -> Toplevel.transition *)
7.180 fun nitpick_params_trans opt_params =
7.181 Toplevel.theory
7.182 - (fn thy =>
7.183 - let val thy = fold set_default_raw_param (these opt_params) thy in
7.184 - writeln ("Default parameters for Nitpick:\n" ^
7.185 - (case rev (default_raw_params thy) of
7.186 - [] => "none"
7.187 - | params =>
7.188 - (map check_raw_param params;
7.189 - params |> map string_for_raw_param |> sort_strings
7.190 - |> cat_lines)));
7.191 - register_auto thy
7.192 - end)
7.193 + (fold set_default_raw_param (these opt_params)
7.194 + #> tap (fn thy =>
7.195 + writeln ("Default parameters for Nitpick:\n" ^
7.196 + (case rev (default_raw_params thy) of
7.197 + [] => "none"
7.198 + | params =>
7.199 + (map check_raw_param params;
7.200 + params |> map string_for_raw_param
7.201 + |> sort_strings |> cat_lines)))))
7.202
7.203 (* OuterParse.token list
7.204 -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
7.205 -fun scan_nitpick_command tokens =
7.206 - (scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
7.207 -fun scan_nitpick_params_command tokens =
7.208 - scan_params tokens |>> nitpick_params_trans
7.209 +val scan_nitpick_command =
7.210 + (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
7.211 +val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
7.212
7.213 val _ = OuterSyntax.improper_command "nitpick"
7.214 "try to find a counterexample for a given subgoal using Kodkod"
7.215 @@ -493,4 +469,10 @@
7.216 "set and display the default parameters for Nitpick"
7.217 OuterKeyword.thy_decl scan_nitpick_params_command
7.218
7.219 +(* Proof.state -> bool * Proof.state *)
7.220 +fun auto_nitpick state =
7.221 + if not (!auto) then (false, state) else pick_nits [] true 1 state
7.222 +
7.223 +val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
7.224 +
7.225 end;
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/Auto_Counterexample.thy Wed Oct 28 17:43:43 2009 +0100
8.3 @@ -0,0 +1,15 @@
8.4 +(* Title: Tools/Auto_Counterexample.thy
8.5 + Author: Jasmin Blanchette, TU Muenchen
8.6 +
8.7 +Counterexample Search Unit (do not abbreviate!).
8.8 +*)
8.9 +
8.10 +header {* Counterexample Search Unit *}
8.11 +
8.12 +theory Auto_Counterexample
8.13 +imports Pure
8.14 +uses
8.15 + "~~/src/Tools/auto_counterexample.ML"
8.16 +begin
8.17 +
8.18 +end
9.1 --- a/src/Tools/Code_Generator.thy Wed Oct 28 11:55:48 2009 +0100
9.2 +++ b/src/Tools/Code_Generator.thy Wed Oct 28 17:43:43 2009 +0100
9.3 @@ -5,7 +5,7 @@
9.4 header {* Loading the code generator modules *}
9.5
9.6 theory Code_Generator
9.7 -imports Pure
9.8 +imports Auto_Counterexample
9.9 uses
9.10 "~~/src/Tools/value.ML"
9.11 "~~/src/Tools/quickcheck.ML"
9.12 @@ -25,4 +25,4 @@
9.13 #> Nbe.setup
9.14 *}
9.15
9.16 -end
9.17 \ No newline at end of file
9.18 +end
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/Tools/auto_counterexample.ML Wed Oct 28 17:43:43 2009 +0100
10.3 @@ -0,0 +1,59 @@
10.4 +(* Title: Tools/auto_counterexample.ML
10.5 + Author: Jasmin Blanchette, TU Muenchen
10.6 +
10.7 +Counterexample Search Unit (do not abbreviate!).
10.8 +*)
10.9 +
10.10 +signature AUTO_COUNTEREXAMPLE =
10.11 +sig
10.12 + val time_limit: int Unsynchronized.ref
10.13 +
10.14 + val register_tool :
10.15 + string * (Proof.state -> bool * Proof.state) -> theory -> theory
10.16 +end;
10.17 +
10.18 +structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
10.19 +struct
10.20 +
10.21 +(* preferences *)
10.22 +
10.23 +val time_limit = Unsynchronized.ref 2500
10.24 +
10.25 +val _ =
10.26 + ProofGeneralPgip.add_preference Preferences.category_tracing
10.27 + (Preferences.nat_pref time_limit
10.28 + "auto-counterexample-time-limit"
10.29 + "Time limit for automatic counterexample search (in milliseconds).")
10.30 +
10.31 +
10.32 +(* configuration *)
10.33 +
10.34 +structure Data = TheoryDataFun(
10.35 + type T = (string * (Proof.state -> bool * Proof.state)) list
10.36 + val empty = []
10.37 + val copy = I
10.38 + val extend = I
10.39 + fun merge _ (tools1, tools2) = AList.merge (op =) (K true) (tools1, tools2)
10.40 +)
10.41 +
10.42 +val register_tool = Data.map o AList.update (op =)
10.43 +
10.44 +
10.45 +(* automatic testing *)
10.46 +
10.47 +val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
10.48 + case !time_limit of
10.49 + 0 => state
10.50 + | ms =>
10.51 + TimeLimit.timeLimit (Time.fromMilliseconds ms)
10.52 + (fn () =>
10.53 + if interact andalso not (!Toplevel.quiet) then
10.54 + fold_rev (fn (_, tool) => fn (true, state) => (true, state)
10.55 + | (false, state) => tool state)
10.56 + (Data.get (Proof.theory_of state)) (false, state) |> snd
10.57 + else
10.58 + state) ()
10.59 + handle TimeLimit.TimeOut =>
10.60 + (warning "Automatic counterexample search timed out."; state)))
10.61 +
10.62 +end;
11.1 --- a/src/Tools/quickcheck.ML Wed Oct 28 11:55:48 2009 +0100
11.2 +++ b/src/Tools/quickcheck.ML Wed Oct 28 17:43:43 2009 +0100
11.3 @@ -7,10 +7,10 @@
11.4 signature QUICKCHECK =
11.5 sig
11.6 val auto: bool Unsynchronized.ref
11.7 - val auto_time_limit: int Unsynchronized.ref
11.8 val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
11.9 (string * term) list option
11.10 val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
11.11 + val setup: theory -> theory
11.12 val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
11.13 end;
11.14
11.15 @@ -20,20 +20,13 @@
11.16 (* preferences *)
11.17
11.18 val auto = Unsynchronized.ref false;
11.19 -val auto_time_limit = Unsynchronized.ref 2500;
11.20
11.21 val _ =
11.22 ProofGeneralPgip.add_preference Preferences.category_tracing
11.23 (setmp_CRITICAL auto true (fn () =>
11.24 Preferences.bool_pref auto
11.25 "auto-quickcheck"
11.26 - "Whether to enable quickcheck automatically.") ());
11.27 -
11.28 -val _ =
11.29 - ProofGeneralPgip.add_preference Preferences.category_tracing
11.30 - (Preferences.nat_pref auto_time_limit
11.31 - "auto-quickcheck-time-limit"
11.32 - "Time limit for automatic quickcheck (in milliseconds).");
11.33 + "Whether to run Quickcheck automatically.") ());
11.34
11.35
11.36 (* quickcheck configuration -- default parameters, test generators *)
11.37 @@ -159,28 +152,26 @@
11.38
11.39 (* automatic testing *)
11.40
11.41 -val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
11.42 - let
11.43 - val ctxt = Proof.context_of state;
11.44 - val assms = map term_of (Assumption.all_assms_of ctxt);
11.45 - val Test_Params { size, iterations, default_type } =
11.46 - (snd o Data.get o Proof.theory_of) state;
11.47 - fun test () =
11.48 - let
11.49 - val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
11.50 - (try (test_goal true NONE size iterations default_type [] 1 assms)) state;
11.51 - in
11.52 - case res of
11.53 - NONE => state
11.54 - | SOME NONE => state
11.55 - | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
11.56 - Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
11.57 - end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
11.58 - in
11.59 - if int andalso !auto andalso not (!Toplevel.quiet)
11.60 - then test ()
11.61 - else state
11.62 - end));
11.63 +fun auto_quickcheck state =
11.64 + if not (!auto) then
11.65 + (false, state)
11.66 + else
11.67 + let
11.68 + val ctxt = Proof.context_of state;
11.69 + val assms = map term_of (Assumption.all_assms_of ctxt);
11.70 + val Test_Params { size, iterations, default_type } =
11.71 + (snd o Data.get o Proof.theory_of) state;
11.72 + val res =
11.73 + try (test_goal true NONE size iterations default_type [] 1 assms) state;
11.74 + in
11.75 + case res of
11.76 + NONE => (false, state)
11.77 + | SOME NONE => (false, state)
11.78 + | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
11.79 + Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
11.80 + end
11.81 +
11.82 +val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck)
11.83
11.84
11.85 (* Isar commands *)
11.86 @@ -251,4 +242,3 @@
11.87
11.88
11.89 val auto_quickcheck = Quickcheck.auto;
11.90 -val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;