1.1 --- a/doc-src/Nitpick/nitpick.tex Wed Nov 04 17:17:30 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Thu Nov 05 11:58:36 2009 +0100
1.3 @@ -2,7 +2,7 @@
1.4 \usepackage[T1]{fontenc}
1.5 \usepackage{amsmath}
1.6 \usepackage{amssymb}
1.7 -\usepackage[french,english]{babel}
1.8 +\usepackage[english,french]{babel}
1.9 \usepackage{color}
1.10 \usepackage{graphicx}
1.11 %\usepackage{mathpazo}
1.12 @@ -40,6 +40,8 @@
1.13
1.14 \begin{document}
1.15
1.16 +\selectlanguage{english}
1.17 +
1.18 \title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
1.19 Picking Nits \\[\smallskipamount]
1.20 \Large A User's Guide to Nitpick for Isabelle/HOL 2010}
1.21 @@ -112,6 +114,13 @@
1.22 machine called \texttt{java}. The examples presented in this manual can be found
1.23 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
1.24
1.25 +Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
1.26 +Nitpick also provides an automatic mode that can be enabled using the
1.27 +``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
1.28 +mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
1.29 +The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
1.30 +the ``Auto Counterexample Time Limit'' option.
1.31 +
1.32 \newbox\boxA
1.33 \setbox\boxA=\hbox{\texttt{nospam}}
1.34
1.35 @@ -154,16 +163,6 @@
1.36 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
1.37 available to Nitpick.
1.38
1.39 -Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
1.40 -Nitpick also provides an automatic mode that can be enabled by specifying
1.41 -
1.42 -\prew
1.43 -\textbf{nitpick\_params} [\textit{auto}]
1.44 -\postw
1.45 -
1.46 -at the beginning of the theory file. In this mode, Nitpick is run for up to 5
1.47 -seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
1.48 -
1.49 \subsection{Propositional Logic}
1.50 \label{propositional-logic}
1.51
1.52 @@ -1595,6 +1594,17 @@
1.53 (\S\ref{authentication}), optimizations
1.54 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
1.55
1.56 +You can instruct Nitpick to run automatically on newly entered theorems by
1.57 +enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
1.58 +General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
1.59 +and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
1.60 +\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
1.61 +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
1.62 +disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
1.63 +\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
1.64 +Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
1.65 +concise.
1.66 +
1.67 The number of options can be overwhelming at first glance. Do not let that worry
1.68 you: Nitpick's defaults have been chosen so that it almost always does the right
1.69 thing, and the most important options have been covered in context in
1.70 @@ -1622,35 +1632,19 @@
1.71 \end{enum}
1.72
1.73 Default values are indicated in square brackets. Boolean options have a negated
1.74 -counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
1.75 -options, ``= \textit{true}'' may be omitted.
1.76 +counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
1.77 +Boolean options, ``= \textit{true}'' may be omitted.
1.78
1.79 \subsection{Mode of Operation}
1.80 \label{mode-of-operation}
1.81
1.82 \begin{enum}
1.83 -\opfalse{auto}{no\_auto}
1.84 -Specifies whether Nitpick should be run automatically on newly entered theorems.
1.85 -For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
1.86 -\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
1.87 -\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
1.88 -(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
1.89 -disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
1.90 -\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
1.91 -\textit{timeout} (\S\ref{timeouts}). The output is also more concise.
1.92 -
1.93 -\nopagebreak
1.94 -{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
1.95 -
1.96 \optrue{blocking}{non\_blocking}
1.97 Specifies whether the \textbf{nitpick} command should operate synchronously.
1.98 The asynchronous (non-blocking) mode lets the user start proving the putative
1.99 theorem while Nitpick looks for a counterexample, but it can also be more
1.100 confusing. For technical reasons, automatic runs currently always block.
1.101
1.102 -\nopagebreak
1.103 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.104 -
1.105 \optrue{falsify}{satisfy}
1.106 Specifies whether Nitpick should look for falsifying examples (countermodels) or
1.107 satisfying examples (models). This manual assumes throughout that
1.108 @@ -1670,16 +1664,15 @@
1.109 considered.
1.110
1.111 \nopagebreak
1.112 -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
1.113 -(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
1.114 +{\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
1.115 +(\S\ref{output-format}).}
1.116
1.117 \optrue{assms}{no\_assms}
1.118 Specifies whether the relevant assumptions in structured proof should be
1.119 considered. The option is implicitly enabled for automatic runs.
1.120
1.121 \nopagebreak
1.122 -{\small See also \textit{auto} (\S\ref{mode-of-operation})
1.123 -and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1.124 +{\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1.125
1.126 \opfalse{overlord}{no\_overlord}
1.127 Specifies whether Nitpick should put its temporary files in
1.128 @@ -1836,14 +1829,14 @@
1.129
1.130 \nopagebreak
1.131 {\small See also \textit{card} (\S\ref{scope-of-search}),
1.132 -\textit{coalesce\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
1.133 +\textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
1.134 (\S\ref{output-format}).}
1.135
1.136 \opsmart{mono}{non\_box}
1.137 Specifies the default monotonicity setting to use. This can be overridden on a
1.138 per-type basis using the \textit{mono}~\qty{type} option described above.
1.139
1.140 -\opfalse{coalesce\_type\_vars}{dont\_coalesce\_type\_vars}
1.141 +\opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
1.142 Specifies whether type variables with the same sort constraints should be
1.143 merged. Setting this option to \textit{true} can reduce the number of scopes
1.144 tried and the size of the generated Kodkod formulas, but it also diminishes the
1.145 @@ -1861,9 +1854,6 @@
1.146 option is useful to determine which scopes are tried or which SAT solver is
1.147 used. This option is implicitly disabled for automatic runs.
1.148
1.149 -\nopagebreak
1.150 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.151 -
1.152 \opfalse{debug}{no\_debug}
1.153 Specifies whether Nitpick should display additional debugging information beyond
1.154 what \textit{verbose} already displays. Enabling \textit{debug} also enables
1.155 @@ -1871,8 +1861,8 @@
1.156 option is implicitly disabled for automatic runs.
1.157
1.158 \nopagebreak
1.159 -{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord}
1.160 -(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).}
1.161 +{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
1.162 +\textit{batch\_size} (\S\ref{optimizations}).}
1.163
1.164 \optrue{show\_skolems}{hide\_skolem}
1.165 Specifies whether the values of Skolem constants should be displayed as part of
1.166 @@ -1910,8 +1900,7 @@
1.167 enabled.
1.168
1.169 \nopagebreak
1.170 -{\small See also \textit{auto} (\S\ref{mode-of-operation}),
1.171 -\textit{check\_potential} (\S\ref{authentication}), and
1.172 +{\small See also \textit{check\_potential} (\S\ref{authentication}) and
1.173 \textit{sat\_solver} (\S\ref{optimizations}).}
1.174
1.175 \opt{max\_genuine}{int}{$\mathbf{1}$}
1.176 @@ -1968,8 +1957,7 @@
1.177 shown to be genuine, Nitpick displays a message to this effect and terminates.
1.178
1.179 \nopagebreak
1.180 -{\small See also \textit{max\_potential} (\S\ref{output-format}) and
1.181 -\textit{auto\_timeout} (\S\ref{timeouts}).}
1.182 +{\small See also \textit{max\_potential} (\S\ref{output-format}).}
1.183
1.184 \opfalse{check\_genuine}{trust\_genuine}
1.185 Specifies whether genuine and likely genuine counterexamples should be given to
1.186 @@ -1979,8 +1967,7 @@
1.187 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
1.188
1.189 \nopagebreak
1.190 -{\small See also \textit{max\_genuine} (\S\ref{output-format}) and
1.191 -\textit{auto\_timeout} (\S\ref{timeouts}).}
1.192 +{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
1.193
1.194 \ops{expect}{string}
1.195 Specifies the expected outcome, which must be one of the following:
1.196 @@ -2206,21 +2193,14 @@
1.197 Specifies the maximum amount of time that the \textbf{nitpick} command should
1.198 spend looking for a counterexample. Nitpick tries to honor this constraint as
1.199 well as it can but offers no guarantees. For automatic runs,
1.200 -\textit{auto\_timeout} is used instead.
1.201 +\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
1.202 +a time slot whose length is specified by the ``Auto Counterexample Time
1.203 +Limit'' option in Proof General.
1.204
1.205 \nopagebreak
1.206 -{\small See also \textit{auto} (\S\ref{mode-of-operation})
1.207 -and \textit{max\_threads} (\S\ref{optimizations}).}
1.208 -
1.209 -\opt{auto\_timeout}{time}{$\mathbf{5}$ s}
1.210 -Specifies the maximum amount of time that Nitpick should use to find a
1.211 -counterexample when running automatically. Nitpick tries to honor this
1.212 -constraint as well as it can but offers no guarantees.
1.213 -
1.214 -\nopagebreak
1.215 -{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.216 -
1.217 -\opt{tac\_timeout}{time}{$\mathbf{500}$ ms}
1.218 +{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
1.219 +
1.220 +\opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
1.221 Specifies the maximum amount of time that the \textit{auto} tactic should use
1.222 when checking a counterexample, and similarly that \textit{lexicographic\_order}
1.223 and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
1.224 @@ -2398,11 +2378,11 @@
1.225 & \textit{subgoal}\end{aligned}$
1.226 \postw
1.227
1.228 +\let\antiq=\textrm
1.229 +
1.230 \subsection{Registration of Coinductive Datatypes}
1.231 \label{registration-of-coinductive-datatypes}
1.232
1.233 -\let\antiq=\textrm
1.234 -
1.235 If you have defined a custom coinductive datatype, you can tell Nitpick about
1.236 it, so that it can use an efficient Kodkod axiomatization similar to the one it
1.237 uses for lazy lists. The interface for registering and unregistering coinductive
1.238 @@ -2467,6 +2447,12 @@
1.239 representation of functions synthesized by Isabelle, which is an implementation
1.240 detail.
1.241
1.242 +\item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
1.243 +which can become invalid if you change the definition of an inductive predicate
1.244 +that is registered in the cache. To clear the cache,
1.245 +run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
1.246 +501$\,\textit{ms}$).
1.247 +
1.248 \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
1.249 \textbf{guess} command in a structured proof.
1.250
2.1 Binary file doc-src/gfx/isabelle_nitpick.pdf has changed
3.1 --- a/src/HOL/IsaMakefile Wed Nov 04 17:17:30 2009 +0100
3.2 +++ b/src/HOL/IsaMakefile Thu Nov 05 11:58:36 2009 +0100
3.3 @@ -104,6 +104,7 @@
3.4 $(SRC)/Provers/hypsubst.ML \
3.5 $(SRC)/Provers/quantifier1.ML \
3.6 $(SRC)/Provers/splitter.ML \
3.7 + $(SRC)/Tools/Auto_Counterexample.thy \
3.8 $(SRC)/Tools/Code/code_haskell.ML \
3.9 $(SRC)/Tools/Code/code_ml.ML \
3.10 $(SRC)/Tools/Code/code_preproc.ML \
3.11 @@ -116,6 +117,7 @@
3.12 $(SRC)/Tools/IsaPlanner/rw_tools.ML \
3.13 $(SRC)/Tools/IsaPlanner/zipper.ML \
3.14 $(SRC)/Tools/atomize_elim.ML \
3.15 + $(SRC)/Tools/auto_counterexample.ML \
3.16 $(SRC)/Tools/auto_solve.ML \
3.17 $(SRC)/Tools/coherent.ML \
3.18 $(SRC)/Tools/cong_tac.ML \
4.1 --- a/src/HOL/Main.thy Wed Nov 04 17:17:30 2009 +0100
4.2 +++ b/src/HOL/Main.thy Thu Nov 05 11:58:36 2009 +0100
4.3 @@ -1,7 +1,7 @@
4.4 header {* Main HOL *}
4.5
4.6 theory Main
4.7 -imports Plain Nitpick Predicate_Compile Recdef
4.8 +imports Plain Nitpick Predicate_Compile
4.9 begin
4.10
4.11 text {*
5.1 --- a/src/HOL/Nitpick.thy Wed Nov 04 17:17:30 2009 +0100
5.2 +++ b/src/HOL/Nitpick.thy Thu Nov 05 11:58:36 2009 +0100
5.3 @@ -8,7 +8,7 @@
5.4 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
5.5
5.6 theory Nitpick
5.7 -imports Map SAT
5.8 +imports Map Quickcheck SAT
5.9 uses ("Tools/Nitpick/kodkod.ML")
5.10 ("Tools/Nitpick/kodkod_sat.ML")
5.11 ("Tools/Nitpick/nitpick_util.ML")
5.12 @@ -117,12 +117,16 @@
5.13 apply (simp only: unit.cases)
5.14 by simp
5.15
5.16 +declare unit.cases [nitpick_simp del]
5.17 +
5.18 lemma nat_case_def [nitpick_def]:
5.19 "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
5.20 apply (rule eq_reflection)
5.21 by (case_tac n) auto
5.22
5.23 -lemmas dvd_def = dvd_eq_mod_eq_0 [THEN eq_reflection, nitpick_def]
5.24 +declare nat.cases [nitpick_simp del]
5.25 +
5.26 +lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
5.27
5.28 lemma list_size_simp [nitpick_simp]:
5.29 "list_size f xs = (if xs = [] then 0
5.30 @@ -206,6 +210,21 @@
5.31 definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
5.32 "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
5.33
5.34 +(* While Nitpick normally avoids to unfold definitions for locales, it
5.35 + unfortunately needs to unfold them when dealing with the following built-in
5.36 + constants. A cleaner approach would be to change "Nitpick_HOL" and
5.37 + "Nitpick_Nits" so that they handle the unexpanded overloaded constants
5.38 + directly, but this is slightly more tricky to implement. *)
5.39 +lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
5.40 + div_nat_inst.div_nat div_nat_inst.mod_nat lower_semilattice_fun_inst.inf_fun
5.41 + minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
5.42 + one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
5.43 + ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
5.44 + ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
5.45 + times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
5.46 + upper_semilattice_fun_inst.sup_fun zero_int_inst.zero_int
5.47 + zero_nat_inst.zero_nat
5.48 +
5.49 use "Tools/Nitpick/kodkod.ML"
5.50 use "Tools/Nitpick/kodkod_sat.ML"
5.51 use "Tools/Nitpick/nitpick_util.ML"
5.52 @@ -222,6 +241,8 @@
5.53 use "Tools/Nitpick/nitpick_tests.ML"
5.54 use "Tools/Nitpick/minipick.ML"
5.55
5.56 +setup {* Nitpick_Isar.setup *}
5.57 +
5.58 hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim
5.59 bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
5.60 fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
5.61 @@ -230,10 +251,10 @@
5.62 hide (open) type bisim_iterator pair_box fun_box
5.63 hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
5.64 wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
5.65 - The_psimp Eps_psimp unit_case_def nat_case_def dvd_def list_size_simp
5.66 - nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def
5.67 - one_frac_def num_def denom_def norm_frac_def frac_def plus_frac_def
5.68 - times_frac_def uminus_frac_def number_of_frac_def inverse_frac_def
5.69 - less_eq_frac_def of_frac_def
5.70 + The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
5.71 + nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
5.72 + num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
5.73 + uminus_frac_def number_of_frac_def inverse_frac_def less_eq_frac_def
5.74 + of_frac_def
5.75
5.76 end
6.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Nov 04 17:17:30 2009 +0100
6.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Nov 05 11:58:36 2009 +0100
6.3 @@ -28,7 +28,7 @@
6.4 skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
6.5 unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
6.6 (* term -> bool *)
6.7 -val is_mono = NitpickMono.formulas_monotonic ext_ctxt @{typ 'a} [] []
6.8 +val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] []
6.9 fun is_const t =
6.10 let val T = fastype_of t in
6.11 is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
7.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 04 17:17:30 2009 +0100
7.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Nov 05 11:58:36 2009 +0100
7.3 @@ -173,15 +173,15 @@
7.4 Ycoord :: int
7.5
7.6 lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
7.7 -nitpick [expect = unknown]
7.8 +nitpick [expect = none]
7.9 by (rule Rep_point_ext_type_inverse)
7.10
7.11 lemma "Fract a b = of_int a / of_int b"
7.12 -nitpick [card = 1\<midarrow>2, expect = unknown]
7.13 +nitpick [card = 1\<midarrow>2, expect = none]
7.14 by (rule Fract_of_int_quotient)
7.15
7.16 lemma "Abs_Rat (Rep_Rat a) = a"
7.17 -nitpick [card = 1\<midarrow>2, expect = unknown]
7.18 +nitpick [card = 1\<midarrow>2, expect = none]
7.19 by (rule Rep_Rat_inverse)
7.20
7.21 end
8.1 --- a/src/HOL/Quickcheck.thy Wed Nov 04 17:17:30 2009 +0100
8.2 +++ b/src/HOL/Quickcheck.thy Thu Nov 05 11:58:36 2009 +0100
8.3 @@ -126,6 +126,8 @@
8.4 shows "random_aux k = rhs k"
8.5 using assms by (rule code_numeral.induct)
8.6
8.7 +setup {* Quickcheck.setup *}
8.8 +
8.9 subsection {* the Random-Predicate Monad *}
8.10
8.11 types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
9.1 --- a/src/HOL/Tools/Nitpick/HISTORY Wed Nov 04 17:17:30 2009 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Thu Nov 05 11:58:36 2009 +0100
9.3 @@ -6,7 +6,11 @@
9.4 "nitpick_ind_intro" to "nitpick_intro"
9.5 * Replaced "special_depth" and "skolemize_depth" options by "specialize"
9.6 and "skolemize"
9.7 + * Renamed "coalesce_type_vars" to "merge_type_vars"
9.8 + * Optimized Kodkod encoding of datatypes whose constructors don't appear in
9.9 + the formula to falsify
9.10 * Fixed monotonicity check
9.11 + * Fixed error in display of uncurried constants
9.12
9.13 Version 1.2.2 (16 Oct 2009)
9.14
10.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Nov 04 17:17:30 2009 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Nov 05 11:58:36 2009 +0100
10.3 @@ -1027,12 +1027,10 @@
10.4 val err_path = path_for "kodkodi" "err"
10.5 val _ = write_problem_file out (map snd indexed_problems)
10.6 val _ = File.write_buffer in_path (!in_buf)
10.7 - (* (int list -> outcome) -> outcome *)
10.8 - fun stopped constr =
10.9 - let val nontriv_js = map reindex (snd (read_output_file out_path)) in
10.10 - constr (triv_js @ nontriv_js)
10.11 - handle Exn.Interrupt => Interrupted NONE
10.12 - end
10.13 + (* unit -> unit *)
10.14 + fun remove_temporary_files () =
10.15 + if overlord then ()
10.16 + else List.app File.rm [in_path, out_path, err_path]
10.17 in
10.18 let
10.19 val ms =
10.20 @@ -1085,12 +1083,16 @@
10.21 else
10.22 Normal (ps, js)
10.23 end
10.24 - in
10.25 - if overlord then ()
10.26 - else List.app File.rm [in_path, out_path, err_path];
10.27 - outcome
10.28 - end
10.29 - handle Exn.Interrupt => stopped (Interrupted o SOME)
10.30 + in remove_temporary_files (); outcome end
10.31 + handle Exn.Interrupt =>
10.32 + let
10.33 + val nontriv_js = map reindex (snd (read_output_file out_path))
10.34 + in
10.35 + (remove_temporary_files ();
10.36 + Interrupted (SOME (triv_js @ nontriv_js)))
10.37 + handle Exn.Interrupt =>
10.38 + (remove_temporary_files (); Interrupted NONE)
10.39 + end
10.40 end
10.41 end
10.42
11.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Nov 04 17:17:30 2009 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 05 11:58:36 2009 +0100
11.3 @@ -23,7 +23,7 @@
11.4 overlord: bool,
11.5 user_axioms: bool option,
11.6 assms: bool,
11.7 - coalesce_type_vars: bool,
11.8 + merge_type_vars: bool,
11.9 destroy_constrs: bool,
11.10 specialize: bool,
11.11 skolemize: bool,
11.12 @@ -88,7 +88,7 @@
11.13 overlord: bool,
11.14 user_axioms: bool option,
11.15 assms: bool,
11.16 - coalesce_type_vars: bool,
11.17 + merge_type_vars: bool,
11.18 destroy_constrs: bool,
11.19 specialize: bool,
11.20 skolemize: bool,
11.21 @@ -137,6 +137,15 @@
11.22 Pretty.str (if j = 1 then "." else ";")])
11.23 (length ts downto 1) ts))]
11.24
11.25 +(* unit -> string *)
11.26 +fun install_kodkodi_message () =
11.27 + "Nitpick requires the external Java program Kodkodi. To install it, download \
11.28 + \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
11.29 + \directory's full path to \"" ^
11.30 + Path.implode (Path.expand (Path.appends
11.31 + (Path.variable "ISABELLE_HOME_USER" ::
11.32 + map Path.basic ["etc", "components"]))) ^ "\"."
11.33 +
11.34 val max_liberal_delay_ms = 200
11.35 val max_liberal_delay_percent = 2
11.36
11.37 @@ -166,6 +175,9 @@
11.38 val has_weaselly_sorts =
11.39 exists_type o exists_subtype o is_tfree_with_weaselly_sort
11.40
11.41 +(* (unit -> string) -> Pretty.T *)
11.42 +fun plazy f = Pretty.blk (0, pstrs (f ()))
11.43 +
11.44 (* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *)
11.45 fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts
11.46 orig_t =
11.47 @@ -175,7 +187,7 @@
11.48 val ctxt = Proof.context_of state
11.49 val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
11.50 monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
11.51 - user_axioms, assms, coalesce_type_vars, destroy_constrs, specialize,
11.52 + user_axioms, assms, merge_type_vars, destroy_constrs, specialize,
11.53 skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim,
11.54 tac_timeout, sym_break, sharing_depth, flatten_props, max_threads,
11.55 show_skolems, show_datatypes, show_consts, evals, formats,
11.56 @@ -187,7 +199,7 @@
11.57 val pprint =
11.58 if auto then
11.59 Unsynchronized.change state_ref o Proof.goal_message o K
11.60 - o curry Pretty.blk 0 o cons (Pretty.str "") o single
11.61 + o Pretty.chunks o cons (Pretty.str "") o single
11.62 o Pretty.mark Markup.hilite
11.63 else
11.64 priority o Pretty.string_of
11.65 @@ -198,9 +210,9 @@
11.66 (* string -> unit *)
11.67 val print = pprint o curry Pretty.blk 0 o pstrs
11.68 (* (unit -> string) -> unit *)
11.69 - fun print_m f = pprint_m (curry Pretty.blk 0 o pstrs o f)
11.70 - fun print_v f = pprint_v (curry Pretty.blk 0 o pstrs o f)
11.71 - fun print_d f = pprint_d (curry Pretty.blk 0 o pstrs o f)
11.72 + val print_m = pprint_m o K o plazy
11.73 + val print_v = pprint_v o K o plazy
11.74 + val print_d = pprint_d o K o plazy
11.75
11.76 (* unit -> unit *)
11.77 fun check_deadline () =
11.78 @@ -220,7 +232,7 @@
11.79 neg_t
11.80 val (assms_t, evals) =
11.81 assms_t :: evals
11.82 - |> coalesce_type_vars ? coalesce_type_vars_in_terms
11.83 + |> merge_type_vars ? merge_type_vars_in_terms
11.84 |> hd pairf tl
11.85 val original_max_potential = max_potential
11.86 val original_max_genuine = max_genuine
11.87 @@ -283,6 +295,21 @@
11.88 handle TYPE (_, Ts, ts) =>
11.89 raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
11.90
11.91 + val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
11.92 + val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
11.93 + def_ts
11.94 + val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
11.95 + nondef_ts
11.96 + val (free_names, const_names) =
11.97 + fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
11.98 + val (sel_names, nonsel_names) =
11.99 + List.partition (is_sel o nickname_of) const_names
11.100 + val would_be_genuine = got_all_user_axioms andalso none_true wfs
11.101 +(*
11.102 + val _ = List.app (priority o string_for_nut ctxt)
11.103 + (core_u :: def_us @ nondef_us)
11.104 +*)
11.105 +
11.106 val unique_scope = forall (equal 1 o length o snd) cards_assigns
11.107 (* typ -> bool *)
11.108 fun is_free_type_monotonic T =
11.109 @@ -298,6 +325,8 @@
11.110 not (is_pure_typedef thy T) orelse is_univ_typedef thy T
11.111 orelse is_number_type thy T
11.112 orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
11.113 + fun is_datatype_shallow T =
11.114 + not (exists (equal T o domain_type o type_of) sel_names)
11.115 val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
11.116 |> sort TermOrd.typ_ord
11.117 val (all_dataTs, all_free_Ts) =
11.118 @@ -326,7 +355,7 @@
11.119 ()
11.120 val mono_Ts = mono_dataTs @ mono_free_Ts
11.121 val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
11.122 -
11.123 + val shallow_dataTs = filter is_datatype_shallow mono_dataTs
11.124 (*
11.125 val _ = priority "Monotonic datatypes:"
11.126 val _ = List.app (priority o string_for_type ctxt) mono_dataTs
11.127 @@ -338,19 +367,6 @@
11.128 val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts
11.129 *)
11.130
11.131 - val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
11.132 - val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
11.133 - def_ts
11.134 - val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
11.135 - nondef_ts
11.136 - val (free_names, const_names) =
11.137 - fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
11.138 - val nonsel_names = filter_out (is_sel o nickname_of) const_names
11.139 - val would_be_genuine = got_all_user_axioms andalso none_true wfs
11.140 -(*
11.141 - val _ = List.app (priority o string_for_nut ctxt)
11.142 - (core_u :: def_us @ nondef_us)
11.143 -*)
11.144 val need_incremental = Int.max (max_potential, max_genuine) >= 2
11.145 val effective_sat_solver =
11.146 if sat_solver <> "smart" then
11.147 @@ -627,15 +643,7 @@
11.148 case Kodkod.solve_any_problem overlord deadline max_threads
11.149 max_solutions (map fst problems) of
11.150 Kodkod.NotInstalled =>
11.151 - (print_m (fn () =>
11.152 - "Nitpick requires the external Java program Kodkodi. \
11.153 - \To install it, download the package from Isabelle's \
11.154 - \web page and add the \"kodkodi-x.y.z\" directory's \
11.155 - \full path to \"" ^
11.156 - Path.implode (Path.expand (Path.appends
11.157 - (Path.variable "ISABELLE_HOME" ::
11.158 - (map Path.basic ["etc", "components"])))) ^
11.159 - "\".");
11.160 + (print_m install_kodkodi_message;
11.161 (max_potential, max_genuine, donno + 1))
11.162 | Kodkod.Normal ([], unsat_js) =>
11.163 (update_checked_problems problems unsat_js;
11.164 @@ -778,11 +786,9 @@
11.165 case scope_count (do_filter (!generated_problems)) scope of
11.166 0 => I
11.167 | n =>
11.168 - if scope_count (do_filter (these (!checked_problems)))
11.169 - scope = n then
11.170 - Integer.add 1
11.171 - else
11.172 - I) (!generated_scopes) 0
11.173 + scope_count (do_filter (these (!checked_problems)))
11.174 + scope = n
11.175 + ? Integer.add 1) (!generated_scopes) 0
11.176 in
11.177 "Nitpick " ^ did_so_and_so ^
11.178 (if is_some (!checked_problems) andalso total > 0 then
11.179 @@ -814,6 +820,7 @@
11.180
11.181 val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns
11.182 iters_assigns bisim_depths mono_Ts nonmono_Ts
11.183 + shallow_dataTs
11.184 val batches = batch_list batch_size (!scopes)
11.185 val outcome_code =
11.186 (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)
11.187 @@ -839,16 +846,21 @@
11.188 (* Proof.state -> params -> bool -> term -> string * Proof.state *)
11.189 fun pick_nits_in_term state (params as {debug, timeout, expect, ...})
11.190 auto orig_assm_ts orig_t =
11.191 - let
11.192 - val deadline = Option.map (curry Time.+ (Time.now ())) timeout
11.193 - val outcome as (outcome_code, _) =
11.194 - time_limit (if debug then NONE else timeout)
11.195 - (pick_them_nits_in_term deadline state params auto orig_assm_ts)
11.196 - orig_t
11.197 - in
11.198 - if expect = "" orelse outcome_code = expect then outcome
11.199 - else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
11.200 - end
11.201 + if getenv "KODKODI" = "" then
11.202 + (if auto then ()
11.203 + else warning (Pretty.string_of (plazy install_kodkodi_message));
11.204 + ("unknown", state))
11.205 + else
11.206 + let
11.207 + val deadline = Option.map (curry Time.+ (Time.now ())) timeout
11.208 + val outcome as (outcome_code, _) =
11.209 + time_limit (if debug then NONE else timeout)
11.210 + (pick_them_nits_in_term deadline state params auto orig_assm_ts)
11.211 + orig_t
11.212 + in
11.213 + if expect = "" orelse outcome_code = expect then outcome
11.214 + else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
11.215 + end
11.216
11.217 (* Proof.state -> params -> thm -> int -> string * Proof.state *)
11.218 fun pick_nits_in_subgoal state params auto subgoal =
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Nov 04 17:17:30 2009 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Nov 05 11:58:36 2009 +0100
12.3 @@ -125,7 +125,7 @@
12.4 val is_inductive_pred : extended_context -> styp -> bool
12.5 val is_constr_pattern_lhs : theory -> term -> bool
12.6 val is_constr_pattern_formula : theory -> term -> bool
12.7 - val coalesce_type_vars_in_terms : term list -> term list
12.8 + val merge_type_vars_in_terms : term list -> term list
12.9 val ground_types_in_type : extended_context -> typ -> typ list
12.10 val ground_types_in_terms : extended_context -> term list -> typ list
12.11 val format_type : int list -> int list -> typ -> typ
12.12 @@ -313,7 +313,7 @@
12.13 (@{const_name times_int_inst.times_int}, 0),
12.14 (@{const_name div_int_inst.div_int}, 0),
12.15 (@{const_name div_int_inst.mod_int}, 0),
12.16 - (@{const_name uminus_int_inst.uminus_int}, 0), (* FIXME: needed? *)
12.17 + (@{const_name uminus_int_inst.uminus_int}, 0),
12.18 (@{const_name ord_int_inst.less_int}, 2),
12.19 (@{const_name ord_int_inst.less_eq_int}, 2),
12.20 (@{const_name Tha}, 1),
12.21 @@ -966,6 +966,14 @@
12.22 (* indexname * typ -> term -> term *)
12.23 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
12.24
12.25 +(* theory -> string -> bool *)
12.26 +fun is_funky_typedef_name thy s =
12.27 + s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
12.28 + @{type_name int}]
12.29 + orelse is_frac_type thy (Type (s, []))
12.30 +(* theory -> term -> bool *)
12.31 +fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
12.32 + | is_funky_typedef _ _ = false
12.33 (* term -> bool *)
12.34 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
12.35 $ Const (@{const_name TYPE}, _)) = true
12.36 @@ -976,9 +984,7 @@
12.37 | is_typedef_axiom thy boring
12.38 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
12.39 $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
12.40 - boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
12.41 - orelse is_frac_type thy (Type (s, [])))
12.42 - andalso is_typedef thy s
12.43 + boring <> is_funky_typedef_name thy s andalso is_typedef thy s
12.44 | is_typedef_axiom _ _ _ = false
12.45
12.46 (* Distinguishes between (1) constant definition axioms, (2) type arity and
12.47 @@ -1016,24 +1022,6 @@
12.48 | do_eq _ = false
12.49 in do_eq end
12.50
12.51 -(* This table is not pretty. A better approach would be to avoid expanding the
12.52 - operators to their low-level definitions, but this would require dealing with
12.53 - overloading. *)
12.54 -val built_in_built_in_defs =
12.55 - [@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},
12.56 - @{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},
12.57 - @{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},
12.58 - @{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},
12.59 - @{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},
12.60 - @{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},
12.61 - @{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},
12.62 - @{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},
12.63 - @{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},
12.64 - @{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},
12.65 - @{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},
12.66 - @{thm zero_nat_inst.zero_nat}]
12.67 - |> map prop_of
12.68 -
12.69 (* theory -> term list * term list * term list *)
12.70 fun all_axioms_of thy =
12.71 let
12.72 @@ -1054,8 +1042,7 @@
12.73 val (built_in_nondefs, user_nondefs) =
12.74 List.partition (is_typedef_axiom thy false) user_nondefs
12.75 |>> append built_in_nondefs
12.76 - val defs = built_in_built_in_defs @
12.77 - (thy |> PureThy.all_thms_of
12.78 + val defs = (thy |> PureThy.all_thms_of
12.79 |> filter (equal Thm.definitionK o Thm.get_kind o snd)
12.80 |> map (prop_of o snd) |> filter is_plain_definition) @
12.81 user_defs @ built_in_defs
12.82 @@ -1309,10 +1296,6 @@
12.83 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
12.84 end
12.85
12.86 -val redefined_in_Nitpick_thy =
12.87 - [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
12.88 - @{const_name list_size}]
12.89 -
12.90 (* theory -> string -> typ -> typ -> term -> term *)
12.91 fun optimized_record_get thy s rec_T res_T t =
12.92 let val constr_x = the_single (datatype_constrs thy rec_T) in
12.93 @@ -1382,7 +1365,6 @@
12.94 (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
12.95 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
12.96 andf (not o has_trivial_definition thy def_table)
12.97 - andf (not o member (op =) redefined_in_Nitpick_thy o fst)
12.98
12.99 (* term * term -> term *)
12.100 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
12.101 @@ -1630,6 +1612,7 @@
12.102 (tac ctxt (auto_tac (clasimpset_of ctxt))))
12.103 #> the #> Goal.finish ctxt) goal
12.104
12.105 +val max_cached_wfs = 100
12.106 val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
12.107 val cached_wf_props : (term * bool) list Unsynchronized.ref =
12.108 Unsynchronized.ref []
12.109 @@ -1663,8 +1646,11 @@
12.110 else
12.111 ()
12.112 in
12.113 - if tac_timeout = (!cached_timeout) then ()
12.114 - else (cached_wf_props := []; cached_timeout := tac_timeout);
12.115 + if tac_timeout = (!cached_timeout)
12.116 + andalso length (!cached_wf_props) < max_cached_wfs then
12.117 + ()
12.118 + else
12.119 + (cached_wf_props := []; cached_timeout := tac_timeout);
12.120 case AList.lookup (op =) (!cached_wf_props) prop of
12.121 SOME wf => wf
12.122 | NONE =>
12.123 @@ -1879,9 +1865,7 @@
12.124 (* extended_context -> styp -> term list *)
12.125 fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
12.126 psimp_table, ...}) (x as (s, _)) =
12.127 - if s mem redefined_in_Nitpick_thy then
12.128 - []
12.129 - else case def_props_for_const thy fast_descrs (!simp_table) x of
12.130 + case def_props_for_const thy fast_descrs (!simp_table) x of
12.131 [] => (case def_props_for_const thy fast_descrs psimp_table x of
12.132 [] => [inductive_pred_axiom ext_ctxt x]
12.133 | psimps => psimps)
12.134 @@ -1890,7 +1874,7 @@
12.135 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
12.136
12.137 (* term list -> term list *)
12.138 -fun coalesce_type_vars_in_terms ts =
12.139 +fun merge_type_vars_in_terms ts =
12.140 let
12.141 (* typ -> (sort * string) list -> (sort * string) list *)
12.142 fun add_type (TFree (s, S)) table =
12.143 @@ -2565,7 +2549,6 @@
12.144 t
12.145 else
12.146 let
12.147 - (* FIXME: strong enough in the face of user-defined axioms? *)
12.148 val blacklist = if depth = 0 then []
12.149 else case term_under_def t of Const x => [x] | _ => []
12.150 (* term list -> typ list -> term -> term *)
12.151 @@ -3031,14 +3014,16 @@
12.152 else if is_abs_fun thy x then
12.153 accum |> fold (add_nondef_axiom depth)
12.154 (nondef_props_for_const thy false nondef_table x)
12.155 - |> fold (add_def_axiom depth)
12.156 - (nondef_props_for_const thy true
12.157 + |> is_funky_typedef thy (range_type T)
12.158 + ? fold (add_def_axiom depth)
12.159 + (nondef_props_for_const thy true
12.160 (extra_table def_table s) x)
12.161 else if is_rep_fun thy x then
12.162 accum |> fold (add_nondef_axiom depth)
12.163 (nondef_props_for_const thy false nondef_table x)
12.164 - |> fold (add_def_axiom depth)
12.165 - (nondef_props_for_const thy true
12.166 + |> is_funky_typedef thy (range_type T)
12.167 + ? fold (add_def_axiom depth)
12.168 + (nondef_props_for_const thy true
12.169 (extra_table def_table s) x)
12.170 |> add_axioms_for_term depth
12.171 (Const (mate_of_rep_fun thy x))
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Nov 04 17:17:30 2009 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Nov 05 11:58:36 2009 +0100
13.3 @@ -10,7 +10,9 @@
13.4 sig
13.5 type params = Nitpick.params
13.6
13.7 + val auto: bool Unsynchronized.ref
13.8 val default_params : theory -> (string * string) list -> params
13.9 + val setup : theory -> theory
13.10 end
13.11
13.12 structure Nitpick_Isar : NITPICK_ISAR =
13.13 @@ -22,6 +24,14 @@
13.14 open Nitpick_Nut
13.15 open Nitpick
13.16
13.17 +val auto = Unsynchronized.ref false;
13.18 +
13.19 +val _ = ProofGeneralPgip.add_preference Preferences.category_tracing
13.20 + (setmp_CRITICAL auto false
13.21 + (fn () => Preferences.bool_pref auto
13.22 + "auto-nitpick"
13.23 + "Whether to run Nitpick automatically.") ())
13.24 +
13.25 type raw_param = string * string list
13.26
13.27 val default_default_params =
13.28 @@ -33,12 +43,11 @@
13.29 ("wf", ["smart"]),
13.30 ("sat_solver", ["smart"]),
13.31 ("batch_size", ["smart"]),
13.32 - ("auto", ["false"]),
13.33 ("blocking", ["true"]),
13.34 ("falsify", ["true"]),
13.35 ("user_axioms", ["smart"]),
13.36 ("assms", ["true"]),
13.37 - ("coalesce_type_vars", ["false"]),
13.38 + ("merge_type_vars", ["false"]),
13.39 ("destroy_constrs", ["true"]),
13.40 ("specialize", ["true"]),
13.41 ("skolemize", ["true"]),
13.42 @@ -47,7 +56,6 @@
13.43 ("fast_descrs", ["true"]),
13.44 ("peephole_optim", ["true"]),
13.45 ("timeout", ["30 s"]),
13.46 - ("auto_timeout", ["5 s"]),
13.47 ("tac_timeout", ["500 ms"]),
13.48 ("sym_break", ["20"]),
13.49 ("sharing_depth", ["3"]),
13.50 @@ -70,12 +78,11 @@
13.51 [("dont_box", "box"),
13.52 ("non_mono", "mono"),
13.53 ("non_wf", "wf"),
13.54 - ("no_auto", "auto"),
13.55 ("non_blocking", "blocking"),
13.56 ("satisfy", "falsify"),
13.57 ("no_user_axioms", "user_axioms"),
13.58 ("no_assms", "assms"),
13.59 - ("dont_coalesce_type_vars", "coalesce_type_vars"),
13.60 + ("dont_merge_type_vars", "merge_type_vars"),
13.61 ("dont_destroy_constrs", "destroy_constrs"),
13.62 ("dont_specialize", "specialize"),
13.63 ("dont_skolemize", "skolemize"),
13.64 @@ -126,31 +133,22 @@
13.65 | NONE => (name, value)
13.66
13.67 structure TheoryData = TheoryDataFun(
13.68 - type T = {params: raw_param list, registered_auto: bool}
13.69 - val empty = {params = rev default_default_params, registered_auto = false}
13.70 + type T = {params: raw_param list}
13.71 + val empty = {params = rev default_default_params}
13.72 val copy = I
13.73 val extend = I
13.74 - fun merge _ ({params = ps1, registered_auto = a1},
13.75 - {params = ps2, registered_auto = a2}) =
13.76 - {params = AList.merge (op =) (op =) (ps1, ps2),
13.77 - registered_auto = a1 orelse a2})
13.78 + fun merge _ ({params = ps1}, {params = ps2}) =
13.79 + {params = AList.merge (op =) (op =) (ps1, ps2)})
13.80
13.81 (* raw_param -> theory -> theory *)
13.82 fun set_default_raw_param param thy =
13.83 - let val {params, registered_auto} = TheoryData.get thy in
13.84 + let val {params} = TheoryData.get thy in
13.85 TheoryData.put
13.86 - {params = AList.update (op =) (unnegate_raw_param param) params,
13.87 - registered_auto = registered_auto} thy
13.88 + {params = AList.update (op =) (unnegate_raw_param param) params} thy
13.89 end
13.90 (* theory -> raw_param list *)
13.91 val default_raw_params = #params o TheoryData.get
13.92
13.93 -(* theory -> theory *)
13.94 -fun set_registered_auto thy =
13.95 - TheoryData.put {params = default_raw_params thy, registered_auto = true} thy
13.96 -(* theory -> bool *)
13.97 -val is_registered_auto = #registered_auto o TheoryData.get
13.98 -
13.99 (* string -> bool *)
13.100 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
13.101
13.102 @@ -305,7 +303,7 @@
13.103 val overlord = lookup_bool "overlord"
13.104 val user_axioms = lookup_bool_option "user_axioms"
13.105 val assms = lookup_bool "assms"
13.106 - val coalesce_type_vars = lookup_bool "coalesce_type_vars"
13.107 + val merge_type_vars = lookup_bool "merge_type_vars"
13.108 val destroy_constrs = lookup_bool "destroy_constrs"
13.109 val specialize = lookup_bool "specialize"
13.110 val skolemize = lookup_bool "skolemize"
13.111 @@ -313,8 +311,7 @@
13.112 val uncurry = lookup_bool "uncurry"
13.113 val fast_descrs = lookup_bool "fast_descrs"
13.114 val peephole_optim = lookup_bool "peephole_optim"
13.115 - val timeout = if auto then lookup_time "auto_timeout"
13.116 - else lookup_time "timeout"
13.117 + val timeout = if auto then NONE else lookup_time "timeout"
13.118 val tac_timeout = lookup_time "tac_timeout"
13.119 val sym_break = Int.max (0, lookup_int "sym_break")
13.120 val sharing_depth = Int.max (1, lookup_int "sharing_depth")
13.121 @@ -326,8 +323,8 @@
13.122 val show_consts = show_all orelse lookup_bool "show_consts"
13.123 val formats = lookup_ints_assigns read_term_polymorphic "format" 0
13.124 val evals = lookup_term_list "eval"
13.125 - val max_potential = if auto then 0
13.126 - else Int.max (0, lookup_int "max_potential")
13.127 + val max_potential =
13.128 + if auto then 0 else Int.max (0, lookup_int "max_potential")
13.129 val max_genuine = Int.max (0, lookup_int "max_genuine")
13.130 val check_potential = lookup_bool "check_potential"
13.131 val check_genuine = lookup_bool "check_genuine"
13.132 @@ -341,7 +338,7 @@
13.133 monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
13.134 falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
13.135 user_axioms = user_axioms, assms = assms,
13.136 - coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs,
13.137 + merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs,
13.138 specialize = specialize, skolemize = skolemize,
13.139 star_linear_preds = star_linear_preds, uncurry = uncurry,
13.140 fast_descrs = fast_descrs, peephole_optim = peephole_optim,
13.141 @@ -412,7 +409,7 @@
13.142 | Refute.REFUTE (loc, details) =>
13.143 error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
13.144
13.145 -(* raw_param list -> bool -> int -> Proof.state -> Proof.state *)
13.146 +(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
13.147 fun pick_nits override_params auto subgoal state =
13.148 let
13.149 val thy = Proof.theory_of state
13.150 @@ -421,70 +418,49 @@
13.151 val _ = List.app check_raw_param override_params
13.152 val params as {blocking, debug, ...} =
13.153 extract_params ctxt auto (default_raw_params thy) override_params
13.154 - (* unit -> Proof.state *)
13.155 + (* unit -> bool * Proof.state *)
13.156 fun go () =
13.157 - (if auto then perhaps o try
13.158 - else if debug then fn f => fn x => f x
13.159 - else handle_exceptions ctxt)
13.160 - (fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
13.161 - state
13.162 + (false, state)
13.163 + |> (if auto then perhaps o try
13.164 + else if debug then fn f => fn x => f x
13.165 + else handle_exceptions ctxt)
13.166 + (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
13.167 + |>> equal "genuine")
13.168 in
13.169 - if auto orelse blocking then
13.170 - go ()
13.171 - else
13.172 - (SimpleThread.fork true (fn () => (go (); ()));
13.173 - state)
13.174 + if auto orelse blocking then go ()
13.175 + else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
13.176 end
13.177
13.178 (* (TableFun().key * string list) list option * int option
13.179 -> Toplevel.transition -> Toplevel.transition *)
13.180 fun nitpick_trans (opt_params, opt_subgoal) =
13.181 Toplevel.keep (K ()
13.182 - o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
13.183 + o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
13.184 o Toplevel.proof_of)
13.185
13.186 (* raw_param -> string *)
13.187 fun string_for_raw_param (name, value) =
13.188 name ^ " = " ^ stringify_raw_param_value value
13.189
13.190 -(* bool -> Proof.state -> Proof.state *)
13.191 -fun pick_nits_auto interactive state =
13.192 - let val thy = Proof.theory_of state in
13.193 - ((interactive andalso not (!Toplevel.quiet)
13.194 - andalso the (general_lookup_bool false (default_raw_params thy)
13.195 - (SOME false) "auto"))
13.196 - ? pick_nits [] true 0) state
13.197 - end
13.198 -
13.199 -(* theory -> theory *)
13.200 -fun register_auto thy =
13.201 - (not (is_registered_auto thy)
13.202 - ? (set_registered_auto
13.203 - #> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))
13.204 - thy
13.205 -
13.206 (* (TableFun().key * string) list option -> Toplevel.transition
13.207 -> Toplevel.transition *)
13.208 fun nitpick_params_trans opt_params =
13.209 Toplevel.theory
13.210 - (fn thy =>
13.211 - let val thy = fold set_default_raw_param (these opt_params) thy in
13.212 - writeln ("Default parameters for Nitpick:\n" ^
13.213 - (case rev (default_raw_params thy) of
13.214 - [] => "none"
13.215 - | params =>
13.216 - (map check_raw_param params;
13.217 - params |> map string_for_raw_param |> sort_strings
13.218 - |> cat_lines)));
13.219 - register_auto thy
13.220 - end)
13.221 + (fold set_default_raw_param (these opt_params)
13.222 + #> tap (fn thy =>
13.223 + writeln ("Default parameters for Nitpick:\n" ^
13.224 + (case rev (default_raw_params thy) of
13.225 + [] => "none"
13.226 + | params =>
13.227 + (map check_raw_param params;
13.228 + params |> map string_for_raw_param
13.229 + |> sort_strings |> cat_lines)))))
13.230
13.231 (* OuterParse.token list
13.232 -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
13.233 -fun scan_nitpick_command tokens =
13.234 - (scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
13.235 -fun scan_nitpick_params_command tokens =
13.236 - scan_params tokens |>> nitpick_params_trans
13.237 +val scan_nitpick_command =
13.238 + (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
13.239 +val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
13.240
13.241 val _ = OuterSyntax.improper_command "nitpick"
13.242 "try to find a counterexample for a given subgoal using Kodkod"
13.243 @@ -493,4 +469,10 @@
13.244 "set and display the default parameters for Nitpick"
13.245 OuterKeyword.thy_decl scan_nitpick_params_command
13.246
13.247 +(* Proof.state -> bool * Proof.state *)
13.248 +fun auto_nitpick state =
13.249 + if not (!auto) then (false, state) else pick_nits [] true 1 state
13.250 +
13.251 +val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
13.252 +
13.253 end;
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Nov 04 17:17:30 2009 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Nov 05 11:58:36 2009 +0100
14.3 @@ -343,7 +343,6 @@
14.4
14.5 (* The type constraint below is a workaround for a Poly/ML bug. *)
14.6
14.7 -(* FIXME: clean up *)
14.8 (* kodkod_constrs -> rep -> Kodkod.rel_expr -> Kodkod.formula *)
14.9 fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
14.10 R r =
14.11 @@ -371,7 +370,6 @@
14.12 Kodkod.True
14.13 end
14.14 fun kk_n_ary_function kk R (r as Kodkod.Rel _) =
14.15 - (* FIXME: weird test *)
14.16 if not (is_opt_rep R) then
14.17 if r = suc_rel then
14.18 Kodkod.False
14.19 @@ -716,8 +714,8 @@
14.20 (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
14.21 -> dtype_spec -> nfa_entry option *)
14.22 fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
14.23 - | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes
14.24 - ({typ, constrs, ...} : dtype_spec) =
14.25 + | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE
14.26 + | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
14.27 SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
14.28 o #const) constrs)
14.29
14.30 @@ -884,12 +882,13 @@
14.31
14.32 (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
14.33 -> dtype_spec -> Kodkod.formula list *)
14.34 -fun other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
14.35 - let val j0 = offset_of_type ofs typ in
14.36 - sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
14.37 - uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
14.38 - partition_axioms_for_datatype j0 kk rel_table dtype
14.39 - end
14.40 +fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
14.41 + | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
14.42 + let val j0 = offset_of_type ofs typ in
14.43 + sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
14.44 + uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
14.45 + partition_axioms_for_datatype j0 kk rel_table dtype
14.46 + end
14.47
14.48 (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
14.49 -> dtype_spec list -> Kodkod.formula list *)
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Nov 04 17:17:30 2009 +0100
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Nov 05 11:58:36 2009 +0100
15.3 @@ -133,12 +133,14 @@
15.4 | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
15.5 in apsnd (pairself rev) o aux end
15.6
15.7 -(* typ -> term -> term list * term *)
15.8 -fun break_in_two (Type ("*", [T1, T2]))
15.9 - (Const (@{const_name Pair}, _) $ t1 $ t2) =
15.10 - break_in_two T2 t2 |>> cons t1
15.11 - | break_in_two _ (Const (@{const_name Pair}, _) $ t1 $ t2) = ([t1], t2)
15.12 - | break_in_two _ t = raise TERM ("Nitpick_Model.break_in_two", [t])
15.13 +(* typ -> typ -> typ -> term -> term * term *)
15.14 +fun break_in_two T T1 T2 t =
15.15 + let
15.16 + val ps = HOLogic.flat_tupleT_paths T
15.17 + val cut = length (HOLogic.strip_tupleT T1)
15.18 + val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
15.19 + val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
15.20 + in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
15.21 (* typ -> term -> term -> term *)
15.22 fun pair_up (Type ("*", [T1', T2']))
15.23 (t1 as Const (@{const_name Pair},
15.24 @@ -153,12 +155,12 @@
15.25 (* typ -> typ -> typ -> term -> term *)
15.26 fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
15.27 let
15.28 - (* typ -> typ -> typ -> term -> term *)
15.29 - fun do_curry T1a T1b T2 t =
15.30 + (* typ -> typ -> typ -> typ -> term -> term *)
15.31 + fun do_curry T1 T1a T1b T2 t =
15.32 let
15.33 val (maybe_opt, ps) = dest_plain_fun t
15.34 val ps =
15.35 - ps |>> map (break_in_two T1a #>> mk_flat_tuple T1a)
15.36 + ps |>> map (break_in_two T1 T1a T1b)
15.37 |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
15.38 |> AList.coalesce (op =)
15.39 |> map (apsnd (make_plain_fun maybe_opt T1b T2))
15.40 @@ -185,7 +187,7 @@
15.41 case factor_out_types T1' T1 of
15.42 ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
15.43 | ((_, NONE), (T1a, SOME T1b)) =>
15.44 - t |> do_curry T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
15.45 + t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
15.46 | ((T1a', SOME T1b'), (_, NONE)) =>
15.47 t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
15.48 | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
15.49 @@ -329,7 +331,8 @@
15.50 HOLogic.mk_number nat_T j
15.51 else case datatype_spec datatypes T of
15.52 NONE => atom for_auto T j
15.53 - | SOME {constrs, co, ...} =>
15.54 + | SOME {shallow = true, ...} => atom for_auto T j
15.55 + | SOME {co, constrs, ...} =>
15.56 let
15.57 (* styp -> int list *)
15.58 fun tuples_for_const (s, T) =
15.59 @@ -585,8 +588,7 @@
15.60 |> term_for_rep T T' (rep_of name)
15.61 in
15.62 Pretty.block (Pretty.breaks
15.63 - [(setmp_CRITICAL show_question_marks false o setmp_show_all_types)
15.64 - (Syntax.pretty_term ctxt) t1,
15.65 + [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
15.66 Pretty.str oper, Syntax.pretty_term ctxt t2])
15.67 end
15.68 (* dtype_spec -> Pretty.T *)
15.69 @@ -600,11 +602,12 @@
15.70 (* typ -> dtype_spec list *)
15.71 fun integer_datatype T =
15.72 [{typ = T, card = card_of_type card_assigns T, co = false,
15.73 - precise = false, constrs = []}]
15.74 + precise = false, shallow = false, constrs = []}]
15.75 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
15.76 val (codatatypes, datatypes) =
15.77 - List.partition #co datatypes
15.78 - ||> append (integer_datatype nat_T @ integer_datatype int_T)
15.79 + datatypes |> filter_out #shallow
15.80 + |> List.partition #co
15.81 + ||> append (integer_datatype nat_T @ integer_datatype int_T)
15.82 val block_of_datatypes =
15.83 if show_datatypes andalso not (null datatypes) then
15.84 [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Nov 04 17:17:30 2009 +0100
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Nov 05 11:58:36 2009 +0100
16.3 @@ -505,7 +505,7 @@
16.4 map prop_for_comp comps @
16.5 map prop_for_sign_expr sexps)
16.6 in
16.7 - case silence (SatSolver.invoke_solver "dpll") prop of
16.8 + case SatSolver.invoke_solver "dpll" prop of
16.9 SatSolver.SATISFIABLE asgns =>
16.10 SOME (literals_from_assignments max_var asgns lits
16.11 |> tap print_solution)
16.12 @@ -708,7 +708,7 @@
16.13 (CFun (left_set_C, S Neg,
16.14 CFun (right_set_C, S Neg, left_set_C)),
16.15 (gamma, cset |> add_ctype_is_right_unique right_set_C
16.16 - (* FIXME: |> add_is_sub_ctype right_set_C left_set_C *)))
16.17 + |> add_is_sub_ctype right_set_C left_set_C))
16.18 end
16.19 | @{const_name ord_fun_inst.less_eq_fun} =>
16.20 do_fragile_set_operation T accum
16.21 @@ -784,10 +784,8 @@
16.22 let
16.23 (* typ -> ctype *)
16.24 val ctype_for = fresh_ctype_for_type cdata
16.25 - (* term -> accumulator -> ctype * accumulator *)
16.26 - val do_term = consider_term cdata
16.27 (* term -> accumulator -> accumulator *)
16.28 - val do_boolean_term = snd oo do_term
16.29 + val do_term = snd oo consider_term cdata
16.30 (* sign -> term -> accumulator -> accumulator *)
16.31 fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
16.32 | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
16.33 @@ -812,11 +810,8 @@
16.34 (* term -> term -> accumulator *)
16.35 fun do_equals t1 t2 =
16.36 case sn of
16.37 - Pos => do_boolean_term t accum
16.38 - | Neg => let
16.39 - val (C1, accum) = do_term t1 accum
16.40 - val (C2, accum) = do_term t2 accum
16.41 - in accum (* FIXME: ||> add_ctypes_equal C1 C2 *) end
16.42 + Pos => do_term t accum
16.43 + | Neg => fold do_term [t1, t2] accum
16.44 in
16.45 case t of
16.46 Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
16.47 @@ -844,10 +839,10 @@
16.48 | @{const "op -->"} $ t1 $ t2 =>
16.49 accum |> do_contra_formula t1 |> do_co_formula t2
16.50 | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
16.51 - accum |> do_boolean_term t1 |> do_co_formula t2 |> do_co_formula t3
16.52 + accum |> do_term t1 |> fold do_co_formula [t2, t3]
16.53 | Const (@{const_name Let}, _) $ t1 $ t2 =>
16.54 do_co_formula (betapply (t2, t1)) accum
16.55 - | _ => do_boolean_term t accum
16.56 + | _ => do_term t accum
16.57 end
16.58 |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
16.59 Syntax.string_of_term ctxt t ^
17.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Nov 04 17:17:30 2009 +0100
17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Nov 05 11:58:36 2009 +0100
17.3 @@ -749,8 +749,9 @@
17.4 (~1 upto num_sels_for_constr_type T - 1)
17.5 (* scope -> dtype_spec -> nut list * rep NameTable.table
17.6 -> nut list * rep NameTable.table *)
17.7 -fun choose_rep_for_sels_of_datatype scope ({constrs, ...} : dtype_spec) =
17.8 - fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
17.9 +fun choose_rep_for_sels_of_datatype _ ({shallow = true, ...} : dtype_spec) = I
17.10 + | choose_rep_for_sels_of_datatype scope {constrs, ...} =
17.11 + fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
17.12 (* scope -> rep NameTable.table -> nut list * rep NameTable.table *)
17.13 fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
17.14 fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
17.15 @@ -1058,11 +1059,12 @@
17.16 Op2 (And, bool_T, Any,
17.17 case u2 of
17.18 Op2 (Lambda, _, _, u21, u22) =>
17.19 - if num_occs_in_nut u21 u22 = 0 then (* FIXME: move to s_op2 *)
17.20 + if num_occs_in_nut u21 u22 = 0 then
17.21 u22
17.22 else
17.23 Op2 (Apply, bool_T, Any, u2, x_u)
17.24 | _ => Op2 (Apply, bool_T, Any, u2, x_u),
17.25 +
17.26 Op2 (Eq, bool_T, Any, y_u,
17.27 Op2 (Apply, ran_T, Any, u1, x_u)))))
17.28 |> sub
18.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Nov 04 17:17:30 2009 +0100
18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Nov 05 11:58:36 2009 +0100
18.3 @@ -22,6 +22,7 @@
18.4 card: int,
18.5 co: bool,
18.6 precise: bool,
18.7 + shallow: bool,
18.8 constrs: constr_spec list}
18.9
18.10 type scope = {
18.11 @@ -44,7 +45,7 @@
18.12 val all_scopes :
18.13 extended_context -> int -> (typ option * int list) list
18.14 -> (styp option * int list) list -> (styp option * int list) list
18.15 - -> int list -> typ list -> typ list -> scope list
18.16 + -> int list -> typ list -> typ list -> typ list -> scope list
18.17 end;
18.18
18.19 structure Nitpick_Scope : NITPICK_SCOPE =
18.20 @@ -66,6 +67,7 @@
18.21 card: int,
18.22 co: bool,
18.23 precise: bool,
18.24 + shallow: bool,
18.25 constrs: constr_spec list}
18.26
18.27 type scope = {
18.28 @@ -126,7 +128,7 @@
18.29 card_assigns |> filter_out (equal @{typ bisim_iterator} o fst)
18.30 |> List.partition (is_fp_iterator_type o fst)
18.31 val (unimportant_card_asgns, important_card_asgns) =
18.32 - card_asgns |> List.partition ((is_datatype thy orf is_integer_type) o fst)
18.33 + card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
18.34 val cards =
18.35 map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
18.36 string_of_int k)
18.37 @@ -431,10 +433,11 @@
18.38 explicit_max = max, total = total} :: constrs
18.39 end
18.40
18.41 -(* extended_context -> scope_desc -> typ * int -> dtype_spec *)
18.42 -fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...})
18.43 +(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
18.44 +fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
18.45 (desc as (card_asgns, _)) (T, card) =
18.46 let
18.47 + val shallow = T mem shallow_dataTs
18.48 val co = is_codatatype thy T
18.49 val xs = boxed_datatype_constrs ext_ctxt T
18.50 val self_recs = map (is_self_recursive_constr_type o snd) xs
18.51 @@ -448,14 +451,18 @@
18.52 val constrs =
18.53 fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
18.54 num_non_self_recs) (self_recs ~~ xs) []
18.55 - in {typ = T, card = card, co = co, precise = precise, constrs = constrs} end
18.56 + in
18.57 + {typ = T, card = card, co = co, precise = precise, shallow = shallow,
18.58 + constrs = constrs}
18.59 + end
18.60
18.61 -(* extended_context -> int -> scope_desc -> scope *)
18.62 -fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break
18.63 +(* extended_context -> int -> typ list -> scope_desc -> scope *)
18.64 +fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
18.65 (desc as (card_asgns, _)) =
18.66 let
18.67 - val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt desc)
18.68 - (filter (is_datatype thy o fst) card_asgns)
18.69 + val datatypes =
18.70 + map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
18.71 + (filter (is_datatype thy o fst) card_asgns)
18.72 val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1
18.73 in
18.74 {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes,
18.75 @@ -480,9 +487,9 @@
18.76
18.77 (* extended_context -> int -> (typ option * int list) list
18.78 -> (styp option * int list) list -> (styp option * int list) list -> int list
18.79 - -> typ list -> typ list -> scope list *)
18.80 + -> typ list -> typ list -> typ list -> scope list *)
18.81 fun all_scopes (ext_ctxt as {thy, ctxt, ...}) sym_break cards_asgns maxes_asgns
18.82 - iters_asgns bisim_depths mono_Ts nonmono_Ts =
18.83 + iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
18.84 let
18.85 val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns
18.86 val blocks = blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns
18.87 @@ -492,7 +499,7 @@
18.88 |> map_filter (scope_descriptor_from_combination thy blocks)
18.89 in
18.90 descs |> length descs <= distinct_threshold ? distinct (op =)
18.91 - |> map (scope_from_descriptor ext_ctxt sym_break)
18.92 + |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs)
18.93 end
18.94
18.95 end;
19.1 --- a/src/HOL/Tools/inductive.ML Wed Nov 04 17:17:30 2009 +0100
19.2 +++ b/src/HOL/Tools/inductive.ML Thu Nov 05 11:58:36 2009 +0100
19.3 @@ -655,7 +655,8 @@
19.4 |> LocalTheory.conceal
19.5 |> LocalTheory.define Thm.internalK
19.6 ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
19.7 - (Attrib.empty_binding, fold_rev lambda params
19.8 + ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
19.9 + fold_rev lambda params
19.10 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
19.11 ||> LocalTheory.restore_naming ctxt;
19.12 val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
20.1 --- a/src/HOL/Tools/sat_solver.ML Wed Nov 04 17:17:30 2009 +0100
20.2 +++ b/src/HOL/Tools/sat_solver.ML Thu Nov 05 11:58:36 2009 +0100
20.3 @@ -546,7 +546,7 @@
20.4 (if name="dpll" orelse name="enumerate" then
20.5 warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
20.6 else
20.7 - tracing ("Using SAT solver " ^ quote name ^ "."));
20.8 + ());
20.9 (* apply 'solver' to 'fm' *)
20.10 solver fm
20.11 handle SatSolver.NOT_CONFIGURED => loop solvers
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/Tools/Auto_Counterexample.thy Thu Nov 05 11:58:36 2009 +0100
21.3 @@ -0,0 +1,15 @@
21.4 +(* Title: Tools/Auto_Counterexample.thy
21.5 + Author: Jasmin Blanchette, TU Muenchen
21.6 +
21.7 +Counterexample Search Unit (do not abbreviate!).
21.8 +*)
21.9 +
21.10 +header {* Counterexample Search Unit *}
21.11 +
21.12 +theory Auto_Counterexample
21.13 +imports Pure
21.14 +uses
21.15 + "~~/src/Tools/auto_counterexample.ML"
21.16 +begin
21.17 +
21.18 +end
22.1 --- a/src/Tools/Code_Generator.thy Wed Nov 04 17:17:30 2009 +0100
22.2 +++ b/src/Tools/Code_Generator.thy Thu Nov 05 11:58:36 2009 +0100
22.3 @@ -5,7 +5,7 @@
22.4 header {* Loading the code generator modules *}
22.5
22.6 theory Code_Generator
22.7 -imports Pure
22.8 +imports Auto_Counterexample
22.9 uses
22.10 "~~/src/Tools/value.ML"
22.11 "~~/src/Tools/quickcheck.ML"
22.12 @@ -25,4 +25,4 @@
22.13 #> Nbe.setup
22.14 *}
22.15
22.16 -end
22.17 \ No newline at end of file
22.18 +end
23.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
23.2 +++ b/src/Tools/auto_counterexample.ML Thu Nov 05 11:58:36 2009 +0100
23.3 @@ -0,0 +1,59 @@
23.4 +(* Title: Tools/auto_counterexample.ML
23.5 + Author: Jasmin Blanchette, TU Muenchen
23.6 +
23.7 +Counterexample Search Unit (do not abbreviate!).
23.8 +*)
23.9 +
23.10 +signature AUTO_COUNTEREXAMPLE =
23.11 +sig
23.12 + val time_limit: int Unsynchronized.ref
23.13 +
23.14 + val register_tool :
23.15 + string * (Proof.state -> bool * Proof.state) -> theory -> theory
23.16 +end;
23.17 +
23.18 +structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
23.19 +struct
23.20 +
23.21 +(* preferences *)
23.22 +
23.23 +val time_limit = Unsynchronized.ref 2500
23.24 +
23.25 +val _ =
23.26 + ProofGeneralPgip.add_preference Preferences.category_tracing
23.27 + (Preferences.nat_pref time_limit
23.28 + "auto-counterexample-time-limit"
23.29 + "Time limit for automatic counterexample search (in milliseconds).")
23.30 +
23.31 +
23.32 +(* configuration *)
23.33 +
23.34 +structure Data = TheoryDataFun(
23.35 + type T = (string * (Proof.state -> bool * Proof.state)) list
23.36 + val empty = []
23.37 + val copy = I
23.38 + val extend = I
23.39 + fun merge _ (tools1, tools2) = AList.merge (op =) (K true) (tools1, tools2)
23.40 +)
23.41 +
23.42 +val register_tool = Data.map o AList.update (op =)
23.43 +
23.44 +
23.45 +(* automatic testing *)
23.46 +
23.47 +val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
23.48 + case !time_limit of
23.49 + 0 => state
23.50 + | ms =>
23.51 + TimeLimit.timeLimit (Time.fromMilliseconds ms)
23.52 + (fn () =>
23.53 + if interact andalso not (!Toplevel.quiet) then
23.54 + fold_rev (fn (_, tool) => fn (true, state) => (true, state)
23.55 + | (false, state) => tool state)
23.56 + (Data.get (Proof.theory_of state)) (false, state) |> snd
23.57 + else
23.58 + state) ()
23.59 + handle TimeLimit.TimeOut =>
23.60 + (warning "Automatic counterexample search timed out."; state)))
23.61 +
23.62 +end;
24.1 --- a/src/Tools/quickcheck.ML Wed Nov 04 17:17:30 2009 +0100
24.2 +++ b/src/Tools/quickcheck.ML Thu Nov 05 11:58:36 2009 +0100
24.3 @@ -7,10 +7,10 @@
24.4 signature QUICKCHECK =
24.5 sig
24.6 val auto: bool Unsynchronized.ref
24.7 - val auto_time_limit: int Unsynchronized.ref
24.8 val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
24.9 (string * term) list option
24.10 val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
24.11 + val setup: theory -> theory
24.12 val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
24.13 end;
24.14
24.15 @@ -20,20 +20,13 @@
24.16 (* preferences *)
24.17
24.18 val auto = Unsynchronized.ref false;
24.19 -val auto_time_limit = Unsynchronized.ref 2500;
24.20
24.21 val _ =
24.22 ProofGeneralPgip.add_preference Preferences.category_tracing
24.23 (setmp_CRITICAL auto true (fn () =>
24.24 Preferences.bool_pref auto
24.25 "auto-quickcheck"
24.26 - "Whether to enable quickcheck automatically.") ());
24.27 -
24.28 -val _ =
24.29 - ProofGeneralPgip.add_preference Preferences.category_tracing
24.30 - (Preferences.nat_pref auto_time_limit
24.31 - "auto-quickcheck-time-limit"
24.32 - "Time limit for automatic quickcheck (in milliseconds).");
24.33 + "Whether to run Quickcheck automatically.") ());
24.34
24.35
24.36 (* quickcheck configuration -- default parameters, test generators *)
24.37 @@ -159,28 +152,26 @@
24.38
24.39 (* automatic testing *)
24.40
24.41 -val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
24.42 - let
24.43 - val ctxt = Proof.context_of state;
24.44 - val assms = map term_of (Assumption.all_assms_of ctxt);
24.45 - val Test_Params { size, iterations, default_type } =
24.46 - (snd o Data.get o Proof.theory_of) state;
24.47 - fun test () =
24.48 - let
24.49 - val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
24.50 - (try (test_goal true NONE size iterations default_type [] 1 assms)) state;
24.51 - in
24.52 - case res of
24.53 - NONE => state
24.54 - | SOME NONE => state
24.55 - | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
24.56 - Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
24.57 - end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
24.58 - in
24.59 - if int andalso !auto andalso not (!Toplevel.quiet)
24.60 - then test ()
24.61 - else state
24.62 - end));
24.63 +fun auto_quickcheck state =
24.64 + if not (!auto) then
24.65 + (false, state)
24.66 + else
24.67 + let
24.68 + val ctxt = Proof.context_of state;
24.69 + val assms = map term_of (Assumption.all_assms_of ctxt);
24.70 + val Test_Params { size, iterations, default_type } =
24.71 + (snd o Data.get o Proof.theory_of) state;
24.72 + val res =
24.73 + try (test_goal true NONE size iterations default_type [] 1 assms) state;
24.74 + in
24.75 + case res of
24.76 + NONE => (false, state)
24.77 + | SOME NONE => (false, state)
24.78 + | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
24.79 + Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
24.80 + end
24.81 +
24.82 +val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck)
24.83
24.84
24.85 (* Isar commands *)
24.86 @@ -251,4 +242,3 @@
24.87
24.88
24.89 val auto_quickcheck = Quickcheck.auto;
24.90 -val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;