introduced Auto Nitpick in addition to Auto Quickcheck;
authorblanchet
Wed Oct 28 17:43:43 2009 +0100 (2009-10-28)
changeset 33561ab01b72715ef
parent 33560 b12ab081e5d1
child 33562 b1e2830ee31a
introduced Auto Nitpick in addition to Auto Quickcheck;
this required generalizing the theorem hook used by Quickcheck,
following a suggestion by Florian
doc-src/Nitpick/nitpick.tex
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/Nitpick.thy
src/HOL/Quickcheck.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/Tools/Auto_Counterexample.thy
src/Tools/Code_Generator.thy
src/Tools/auto_counterexample.ML
src/Tools/quickcheck.ML
     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;