merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
1.1 --- a/doc-src/Nitpick/nitpick.tex Tue Nov 10 13:17:50 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Nov 10 13:54:00 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 @@ -2440,6 +2420,11 @@
1.239 \kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
1.240 \postw
1.241
1.242 +Inductive datatypes can be registered as coinductive datatypes, given
1.243 +appropriate coinductive constructors. However, doing so precludes
1.244 +the use of the inductive constructors---Nitpick will generate an error if they
1.245 +are needed.
1.246 +
1.247 \section{Known Bugs and Limitations}
1.248 \label{known-bugs-and-limitations}
1.249
1.250 @@ -2467,12 +2452,21 @@
1.251 representation of functions synthesized by Isabelle, which is an implementation
1.252 detail.
1.253
1.254 +\item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
1.255 +which can become invalid if you change the definition of an inductive predicate
1.256 +that is registered in the cache. To clear the cache,
1.257 +run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
1.258 +501$\,\textit{ms}$).
1.259 +
1.260 \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
1.261 \textbf{guess} command in a structured proof.
1.262
1.263 \item[$\bullet$] The \textit{nitpick\_} attributes and the
1.264 \textit{Nitpick.register\_} functions can cause havoc if used improperly.
1.265
1.266 +\item[$\bullet$] Although this has never been observed, arbitrary theorem
1.267 +morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
1.268 +
1.269 \item[$\bullet$] Local definitions are not supported and result in an error.
1.270
1.271 \item[$\bullet$] All constants and types whose names start with
2.1 Binary file doc-src/gfx/isabelle_nitpick.pdf has changed
3.1 --- a/src/HOL/IsaMakefile Tue Nov 10 13:17:50 2009 +0100
3.2 +++ b/src/HOL/IsaMakefile Tue Nov 10 13:54:00 2009 +0100
3.3 @@ -103,6 +103,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 @@ -115,6 +116,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 Tue Nov 10 13:17:50 2009 +0100
4.2 +++ b/src/HOL/Main.thy Tue Nov 10 13:54:00 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 Tue Nov 10 13:17:50 2009 +0100
5.2 +++ b/src/HOL/Nitpick.thy Tue Nov 10 13:54:00 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 Tue Nov 10 13:17:50 2009 +0100
6.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Nov 10 13:54:00 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 Tue Nov 10 13:17:50 2009 +0100
7.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Nov 10 13:54:00 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 Tue Nov 10 13:17:50 2009 +0100
8.2 +++ b/src/HOL/Quickcheck.thy Tue Nov 10 13:54:00 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 Tue Nov 10 13:17:50 2009 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Tue Nov 10 13:54:00 2009 +0100
9.3 @@ -6,7 +6,14 @@
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 + * Added support for codatatype view of datatypes
9.11 + * Fixed soundness bug related to sets of sets
9.12 * Fixed monotonicity check
9.13 + * Fixed error in display of uncurried constants
9.14 + * Speeded up scope enumeration
9.15
9.16 Version 1.2.2 (16 Oct 2009)
9.17
10.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Nov 10 13:17:50 2009 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Nov 10 13:54:00 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 Tue Nov 10 13:17:50 2009 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Nov 10 13:54:00 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 @@ -251,7 +263,8 @@
11.88 intro_table = intro_table, ground_thm_table = ground_thm_table,
11.89 ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
11.90 special_funs = Unsynchronized.ref [],
11.91 - unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
11.92 + unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
11.93 + constr_cache = Unsynchronized.ref []}
11.94 val frees = Term.add_frees assms_t []
11.95 val _ = null (Term.add_tvars assms_t [])
11.96 orelse raise NOT_SUPPORTED "schematic type variables"
11.97 @@ -283,6 +296,21 @@
11.98 handle TYPE (_, Ts, ts) =>
11.99 raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
11.100
11.101 + val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
11.102 + val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
11.103 + def_ts
11.104 + val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
11.105 + nondef_ts
11.106 + val (free_names, const_names) =
11.107 + fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
11.108 + val (sel_names, nonsel_names) =
11.109 + List.partition (is_sel o nickname_of) const_names
11.110 + val would_be_genuine = got_all_user_axioms andalso none_true wfs
11.111 +(*
11.112 + val _ = List.app (priority o string_for_nut ctxt)
11.113 + (core_u :: def_us @ nondef_us)
11.114 +*)
11.115 +
11.116 val unique_scope = forall (equal 1 o length o snd) cards_assigns
11.117 (* typ -> bool *)
11.118 fun is_free_type_monotonic T =
11.119 @@ -298,6 +326,8 @@
11.120 not (is_pure_typedef thy T) orelse is_univ_typedef thy T
11.121 orelse is_number_type thy T
11.122 orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
11.123 + fun is_datatype_shallow T =
11.124 + not (exists (equal T o domain_type o type_of) sel_names)
11.125 val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
11.126 |> sort TermOrd.typ_ord
11.127 val (all_dataTs, all_free_Ts) =
11.128 @@ -326,7 +356,7 @@
11.129 ()
11.130 val mono_Ts = mono_dataTs @ mono_free_Ts
11.131 val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
11.132 -
11.133 + val shallow_dataTs = filter is_datatype_shallow mono_dataTs
11.134 (*
11.135 val _ = priority "Monotonic datatypes:"
11.136 val _ = List.app (priority o string_for_type ctxt) mono_dataTs
11.137 @@ -338,19 +368,6 @@
11.138 val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts
11.139 *)
11.140
11.141 - val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
11.142 - val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
11.143 - def_ts
11.144 - val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
11.145 - nondef_ts
11.146 - val (free_names, const_names) =
11.147 - fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
11.148 - val nonsel_names = filter_out (is_sel o nickname_of) const_names
11.149 - val would_be_genuine = got_all_user_axioms andalso none_true wfs
11.150 -(*
11.151 - val _ = List.app (priority o string_for_nut ctxt)
11.152 - (core_u :: def_us @ nondef_us)
11.153 -*)
11.154 val need_incremental = Int.max (max_potential, max_genuine) >= 2
11.155 val effective_sat_solver =
11.156 if sat_solver <> "smart" then
11.157 @@ -627,15 +644,7 @@
11.158 case Kodkod.solve_any_problem overlord deadline max_threads
11.159 max_solutions (map fst problems) of
11.160 Kodkod.NotInstalled =>
11.161 - (print_m (fn () =>
11.162 - "Nitpick requires the external Java program Kodkodi. \
11.163 - \To install it, download the package from Isabelle's \
11.164 - \web page and add the \"kodkodi-x.y.z\" directory's \
11.165 - \full path to \"" ^
11.166 - Path.implode (Path.expand (Path.appends
11.167 - (Path.variable "ISABELLE_HOME" ::
11.168 - (map Path.basic ["etc", "components"])))) ^
11.169 - "\".");
11.170 + (print_m install_kodkodi_message;
11.171 (max_potential, max_genuine, donno + 1))
11.172 | Kodkod.Normal ([], unsat_js) =>
11.173 (update_checked_problems problems unsat_js;
11.174 @@ -778,11 +787,9 @@
11.175 case scope_count (do_filter (!generated_problems)) scope of
11.176 0 => I
11.177 | n =>
11.178 - if scope_count (do_filter (these (!checked_problems)))
11.179 - scope = n then
11.180 - Integer.add 1
11.181 - else
11.182 - I) (!generated_scopes) 0
11.183 + scope_count (do_filter (these (!checked_problems)))
11.184 + scope = n
11.185 + ? Integer.add 1) (!generated_scopes) 0
11.186 in
11.187 "Nitpick " ^ did_so_and_so ^
11.188 (if is_some (!checked_problems) andalso total > 0 then
11.189 @@ -812,8 +819,19 @@
11.190 run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
11.191 end
11.192
11.193 - val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns
11.194 - iters_assigns bisim_depths mono_Ts nonmono_Ts
11.195 + val (skipped, the_scopes) =
11.196 + all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
11.197 + bisim_depths mono_Ts nonmono_Ts shallow_dataTs
11.198 + val _ = if skipped > 0 then
11.199 + print_m (fn () => "Too many scopes. Dropping " ^
11.200 + string_of_int skipped ^ " scope" ^
11.201 + plural_s skipped ^
11.202 + ". (Consider using \"mono\" or \
11.203 + \\"merge_type_vars\" to prevent this.)")
11.204 + else
11.205 + ()
11.206 + val _ = scopes := the_scopes
11.207 +
11.208 val batches = batch_list batch_size (!scopes)
11.209 val outcome_code =
11.210 (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)
11.211 @@ -839,16 +857,21 @@
11.212 (* Proof.state -> params -> bool -> term -> string * Proof.state *)
11.213 fun pick_nits_in_term state (params as {debug, timeout, expect, ...})
11.214 auto orig_assm_ts orig_t =
11.215 - let
11.216 - val deadline = Option.map (curry Time.+ (Time.now ())) timeout
11.217 - val outcome as (outcome_code, _) =
11.218 - time_limit (if debug then NONE else timeout)
11.219 - (pick_them_nits_in_term deadline state params auto orig_assm_ts)
11.220 - orig_t
11.221 - in
11.222 - if expect = "" orelse outcome_code = expect then outcome
11.223 - else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
11.224 - end
11.225 + if getenv "KODKODI" = "" then
11.226 + (if auto then ()
11.227 + else warning (Pretty.string_of (plazy install_kodkodi_message));
11.228 + ("unknown", state))
11.229 + else
11.230 + let
11.231 + val deadline = Option.map (curry Time.+ (Time.now ())) timeout
11.232 + val outcome as (outcome_code, _) =
11.233 + time_limit (if debug then NONE else timeout)
11.234 + (pick_them_nits_in_term deadline state params auto orig_assm_ts)
11.235 + orig_t
11.236 + in
11.237 + if expect = "" orelse outcome_code = expect then outcome
11.238 + else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
11.239 + end
11.240
11.241 (* Proof.state -> params -> thm -> int -> string * Proof.state *)
11.242 fun pick_nits_in_subgoal state params auto subgoal =
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 10 13:17:50 2009 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 10 13:54:00 2009 +0100
12.3 @@ -40,7 +40,8 @@
12.4 skolems: (string * string list) list Unsynchronized.ref,
12.5 special_funs: special_fun list Unsynchronized.ref,
12.6 unrolled_preds: unrolled list Unsynchronized.ref,
12.7 - wf_cache: wf_cache Unsynchronized.ref}
12.8 + wf_cache: wf_cache Unsynchronized.ref,
12.9 + constr_cache: (typ * styp list) list Unsynchronized.ref}
12.10
12.11 val name_sep : string
12.12 val numeral_prefix : string
12.13 @@ -86,6 +87,7 @@
12.14 val is_abs_fun : theory -> styp -> bool
12.15 val is_rep_fun : theory -> styp -> bool
12.16 val is_constr : theory -> styp -> bool
12.17 + val is_stale_constr : theory -> styp -> bool
12.18 val is_sel : string -> bool
12.19 val discr_for_constr : styp -> styp
12.20 val num_sels_for_constr_type : typ -> int
12.21 @@ -100,16 +102,16 @@
12.22 val unregister_frac_type : string -> theory -> theory
12.23 val register_codatatype : typ -> string -> styp list -> theory -> theory
12.24 val unregister_codatatype : typ -> theory -> theory
12.25 - val datatype_constrs : theory -> typ -> styp list
12.26 + val datatype_constrs : extended_context -> typ -> styp list
12.27 val boxed_datatype_constrs : extended_context -> typ -> styp list
12.28 - val num_datatype_constrs : theory -> typ -> int
12.29 + val num_datatype_constrs : extended_context -> typ -> int
12.30 val constr_name_for_sel_like : string -> string
12.31 val boxed_constr_for_sel : extended_context -> styp -> styp
12.32 val card_of_type : (typ * int) list -> typ -> int
12.33 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
12.34 val bounded_precise_card_of_type :
12.35 - theory -> int -> int -> (typ * int) list -> typ -> int
12.36 - val is_finite_type : theory -> typ -> bool
12.37 + extended_context -> int -> int -> (typ * int) list -> typ -> int
12.38 + val is_finite_type : extended_context -> typ -> bool
12.39 val all_axioms_of : theory -> term list * term list * term list
12.40 val arity_of_built_in_const : bool -> styp -> int option
12.41 val is_built_in_const : bool -> styp -> bool
12.42 @@ -125,7 +127,7 @@
12.43 val is_inductive_pred : extended_context -> styp -> bool
12.44 val is_constr_pattern_lhs : theory -> term -> bool
12.45 val is_constr_pattern_formula : theory -> term -> bool
12.46 - val coalesce_type_vars_in_terms : term list -> term list
12.47 + val merge_type_vars_in_terms : term list -> term list
12.48 val ground_types_in_type : extended_context -> typ -> typ list
12.49 val ground_types_in_terms : extended_context -> term list -> typ list
12.50 val format_type : int list -> int list -> typ -> typ
12.51 @@ -177,9 +179,10 @@
12.52 skolems: (string * string list) list Unsynchronized.ref,
12.53 special_funs: special_fun list Unsynchronized.ref,
12.54 unrolled_preds: unrolled list Unsynchronized.ref,
12.55 - wf_cache: wf_cache Unsynchronized.ref}
12.56 + wf_cache: wf_cache Unsynchronized.ref,
12.57 + constr_cache: (typ * styp list) list Unsynchronized.ref}
12.58
12.59 -structure TheoryData = Theory_Data(
12.60 +structure Data = Theory_Data(
12.61 type T = {frac_types: (string * (string * string) list) list,
12.62 codatatypes: (string * (string * styp list)) list}
12.63 val empty = {frac_types = [], codatatypes = []}
12.64 @@ -312,7 +315,7 @@
12.65 (@{const_name times_int_inst.times_int}, 0),
12.66 (@{const_name div_int_inst.div_int}, 0),
12.67 (@{const_name div_int_inst.mod_int}, 0),
12.68 - (@{const_name uminus_int_inst.uminus_int}, 0), (* FIXME: needed? *)
12.69 + (@{const_name uminus_int_inst.uminus_int}, 0),
12.70 (@{const_name ord_int_inst.less_int}, 2),
12.71 (@{const_name ord_int_inst.less_eq_int}, 2),
12.72 (@{const_name Tha}, 1),
12.73 @@ -392,8 +395,7 @@
12.74 val is_record_type = not o null o Record.dest_recTs
12.75 (* theory -> typ -> bool *)
12.76 fun is_frac_type thy (Type (s, [])) =
12.77 - not (null (these (AList.lookup (op =) (#frac_types (TheoryData.get thy))
12.78 - s)))
12.79 + not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
12.80 | is_frac_type _ _ = false
12.81 fun is_number_type thy = is_integer_type orf is_frac_type thy
12.82
12.83 @@ -469,16 +471,16 @@
12.84 (* string -> (string * string) list -> theory -> theory *)
12.85 fun register_frac_type frac_s ersaetze thy =
12.86 let
12.87 - val {frac_types, codatatypes} = TheoryData.get thy
12.88 + val {frac_types, codatatypes} = Data.get thy
12.89 val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
12.90 - in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
12.91 + in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
12.92 (* string -> theory -> theory *)
12.93 fun unregister_frac_type frac_s = register_frac_type frac_s []
12.94
12.95 (* typ -> string -> styp list -> theory -> theory *)
12.96 fun register_codatatype co_T case_name constr_xs thy =
12.97 let
12.98 - val {frac_types, codatatypes} = TheoryData.get thy
12.99 + val {frac_types, codatatypes} = Data.get thy
12.100 val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
12.101 val (co_s, co_Ts) = dest_Type co_T
12.102 val _ =
12.103 @@ -486,7 +488,7 @@
12.104 else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
12.105 val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
12.106 codatatypes
12.107 - in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
12.108 + in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
12.109 (* typ -> theory -> theory *)
12.110 fun unregister_codatatype co_T = register_codatatype co_T "" []
12.111
12.112 @@ -520,7 +522,7 @@
12.113 val is_real_datatype = is_some oo Datatype.get_info
12.114 (* theory -> typ -> bool *)
12.115 fun is_codatatype thy (T as Type (s, _)) =
12.116 - not (null (AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s
12.117 + not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
12.118 |> Option.map snd |> these))
12.119 | is_codatatype _ _ = false
12.120 fun is_pure_typedef thy (T as Type (s, _)) =
12.121 @@ -592,7 +594,7 @@
12.122 (* theory -> styp -> bool *)
12.123 fun is_coconstr thy (s, T) =
12.124 let
12.125 - val {codatatypes, ...} = TheoryData.get thy
12.126 + val {codatatypes, ...} = Data.get thy
12.127 val co_T = body_type T
12.128 val co_s = dest_Type co_T |> fst
12.129 in
12.130 @@ -609,9 +611,13 @@
12.131 orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
12.132 orelse is_coconstr thy x
12.133 end
12.134 +fun is_stale_constr thy (x as (_, T)) =
12.135 + is_codatatype thy (body_type T) andalso is_constr_like thy x
12.136 + andalso not (is_coconstr thy x)
12.137 fun is_constr thy (x as (_, T)) =
12.138 is_constr_like thy x
12.139 andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
12.140 + andalso not (is_stale_constr thy x)
12.141 (* string -> bool *)
12.142 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
12.143 val is_sel_like_and_no_discr =
12.144 @@ -726,41 +732,51 @@
12.145 fun suc_const T = Const (@{const_name Suc}, T --> T)
12.146
12.147 (* theory -> typ -> styp list *)
12.148 -fun datatype_constrs thy (T as Type (s, Ts)) =
12.149 - if is_datatype thy T then
12.150 - case Datatype.get_info thy s of
12.151 - SOME {index, descr, ...} =>
12.152 - let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
12.153 - map (fn (s', Us) =>
12.154 - (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
12.155 - constrs
12.156 - end
12.157 - | NONE =>
12.158 - case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of
12.159 - SOME (_, xs' as (_ :: _)) =>
12.160 - map (apsnd (repair_constr_type thy T)) xs'
12.161 - | _ =>
12.162 - if is_record_type T then
12.163 - let
12.164 - val s' = unsuffix Record.ext_typeN s ^ Record.extN
12.165 - val T' = (Record.get_extT_fields thy T
12.166 - |> apsnd single |> uncurry append |> map snd) ---> T
12.167 - in [(s', T')] end
12.168 - else case typedef_info thy s of
12.169 - SOME {abs_type, rep_type, Abs_name, ...} =>
12.170 - [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
12.171 - | NONE =>
12.172 - if T = @{typ ind} then
12.173 - [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
12.174 - else
12.175 - []
12.176 - else
12.177 - []
12.178 - | datatype_constrs _ _ = []
12.179 +fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
12.180 + (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
12.181 + SOME (_, xs' as (_ :: _)) =>
12.182 + map (apsnd (repair_constr_type thy T)) xs'
12.183 + | _ =>
12.184 + if is_datatype thy T then
12.185 + case Datatype.get_info thy s of
12.186 + SOME {index, descr, ...} =>
12.187 + let
12.188 + val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
12.189 + in
12.190 + map (fn (s', Us) =>
12.191 + (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
12.192 + ---> T)) constrs
12.193 + end
12.194 + | NONE =>
12.195 + if is_record_type T then
12.196 + let
12.197 + val s' = unsuffix Record.ext_typeN s ^ Record.extN
12.198 + val T' = (Record.get_extT_fields thy T
12.199 + |> apsnd single |> uncurry append |> map snd) ---> T
12.200 + in [(s', T')] end
12.201 + else case typedef_info thy s of
12.202 + SOME {abs_type, rep_type, Abs_name, ...} =>
12.203 + [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
12.204 + | NONE =>
12.205 + if T = @{typ ind} then
12.206 + [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
12.207 + else
12.208 + []
12.209 + else
12.210 + [])
12.211 + | uncached_datatype_constrs _ _ = []
12.212 (* extended_context -> typ -> styp list *)
12.213 -fun boxed_datatype_constrs (ext_ctxt as {thy, ...}) =
12.214 - map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs thy
12.215 -(* theory -> typ -> int *)
12.216 +fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
12.217 + T =
12.218 + case AList.lookup (op =) (!constr_cache) T of
12.219 + SOME xs => xs
12.220 + | NONE =>
12.221 + let val xs = uncached_datatype_constrs thy T in
12.222 + (Unsynchronized.change constr_cache (cons (T, xs)); xs)
12.223 + end
12.224 +fun boxed_datatype_constrs ext_ctxt =
12.225 + map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
12.226 +(* extended_context -> typ -> int *)
12.227 val num_datatype_constrs = length oo datatype_constrs
12.228
12.229 (* string -> string *)
12.230 @@ -773,26 +789,26 @@
12.231 AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
12.232 |> the |> pair s
12.233 end
12.234 -(* theory -> styp -> term *)
12.235 -fun discr_term_for_constr thy (x as (s, T)) =
12.236 +(* extended_context -> styp -> term *)
12.237 +fun discr_term_for_constr ext_ctxt (x as (s, T)) =
12.238 let val dataT = body_type T in
12.239 if s = @{const_name Suc} then
12.240 Abs (Name.uu, dataT,
12.241 @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
12.242 - else if num_datatype_constrs thy dataT >= 2 then
12.243 + else if num_datatype_constrs ext_ctxt dataT >= 2 then
12.244 Const (discr_for_constr x)
12.245 else
12.246 Abs (Name.uu, dataT, @{const True})
12.247 end
12.248
12.249 -(* theory -> styp -> term -> term *)
12.250 -fun discriminate_value thy (x as (_, T)) t =
12.251 +(* extended_context -> styp -> term -> term *)
12.252 +fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
12.253 case strip_comb t of
12.254 (Const x', args) =>
12.255 if x = x' then @{const True}
12.256 else if is_constr_like thy x' then @{const False}
12.257 - else betapply (discr_term_for_constr thy x, t)
12.258 - | _ => betapply (discr_term_for_constr thy x, t)
12.259 + else betapply (discr_term_for_constr ext_ctxt x, t)
12.260 + | _ => betapply (discr_term_for_constr ext_ctxt x, t)
12.261
12.262 (* styp -> term -> term *)
12.263 fun nth_arg_sel_term_for_constr (x as (s, T)) n =
12.264 @@ -841,8 +857,8 @@
12.265 | _ => list_comb (Const x, args)
12.266 end
12.267
12.268 -(* theory -> typ -> term -> term *)
12.269 -fun constr_expand thy T t =
12.270 +(* extended_context -> typ -> term -> term *)
12.271 +fun constr_expand (ext_ctxt as {thy, ...}) T t =
12.272 (case head_of t of
12.273 Const x => if is_constr_like thy x then t else raise SAME ()
12.274 | _ => raise SAME ())
12.275 @@ -854,7 +870,7 @@
12.276 (@{const_name Pair}, [T1, T2] ---> T)
12.277 end
12.278 else
12.279 - datatype_constrs thy T |> the_single
12.280 + datatype_constrs ext_ctxt T |> the_single
12.281 val arg_Ts = binder_types T'
12.282 in
12.283 list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
12.284 @@ -896,8 +912,8 @@
12.285 card_of_type asgns T
12.286 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
12.287 default_card)
12.288 -(* theory -> int -> (typ * int) list -> typ -> int *)
12.289 -fun bounded_precise_card_of_type thy max default_card asgns T =
12.290 +(* extended_context -> int -> (typ * int) list -> typ -> int *)
12.291 +fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
12.292 let
12.293 (* typ list -> typ -> int *)
12.294 fun aux avoid T =
12.295 @@ -927,12 +943,12 @@
12.296 | @{typ bool} => 2
12.297 | @{typ unit} => 1
12.298 | Type _ =>
12.299 - (case datatype_constrs thy T of
12.300 + (case datatype_constrs ext_ctxt T of
12.301 [] => if is_integer_type T then 0 else raise SAME ()
12.302 | constrs =>
12.303 let
12.304 val constr_cards =
12.305 - datatype_constrs thy T
12.306 + datatype_constrs ext_ctxt T
12.307 |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
12.308 o snd)
12.309 in
12.310 @@ -943,8 +959,9 @@
12.311 handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
12.312 in Int.min (max, aux [] T) end
12.313
12.314 -(* theory -> typ -> bool *)
12.315 -fun is_finite_type thy = not_equal 0 o bounded_precise_card_of_type thy 1 2 []
12.316 +(* extended_context -> typ -> bool *)
12.317 +fun is_finite_type ext_ctxt =
12.318 + not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []
12.319
12.320 (* term -> bool *)
12.321 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
12.322 @@ -965,6 +982,14 @@
12.323 (* indexname * typ -> term -> term *)
12.324 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
12.325
12.326 +(* theory -> string -> bool *)
12.327 +fun is_funky_typedef_name thy s =
12.328 + s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
12.329 + @{type_name int}]
12.330 + orelse is_frac_type thy (Type (s, []))
12.331 +(* theory -> term -> bool *)
12.332 +fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
12.333 + | is_funky_typedef _ _ = false
12.334 (* term -> bool *)
12.335 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
12.336 $ Const (@{const_name TYPE}, _)) = true
12.337 @@ -975,9 +1000,7 @@
12.338 | is_typedef_axiom thy boring
12.339 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
12.340 $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
12.341 - boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
12.342 - orelse is_frac_type thy (Type (s, [])))
12.343 - andalso is_typedef thy s
12.344 + boring <> is_funky_typedef_name thy s andalso is_typedef thy s
12.345 | is_typedef_axiom _ _ _ = false
12.346
12.347 (* Distinguishes between (1) constant definition axioms, (2) type arity and
12.348 @@ -1015,24 +1038,6 @@
12.349 | do_eq _ = false
12.350 in do_eq end
12.351
12.352 -(* This table is not pretty. A better approach would be to avoid expanding the
12.353 - operators to their low-level definitions, but this would require dealing with
12.354 - overloading. *)
12.355 -val built_in_built_in_defs =
12.356 - [@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},
12.357 - @{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},
12.358 - @{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},
12.359 - @{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},
12.360 - @{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},
12.361 - @{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},
12.362 - @{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},
12.363 - @{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},
12.364 - @{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},
12.365 - @{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},
12.366 - @{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},
12.367 - @{thm zero_nat_inst.zero_nat}]
12.368 - |> map prop_of
12.369 -
12.370 (* theory -> term list * term list * term list *)
12.371 fun all_axioms_of thy =
12.372 let
12.373 @@ -1053,8 +1058,7 @@
12.374 val (built_in_nondefs, user_nondefs) =
12.375 List.partition (is_typedef_axiom thy false) user_nondefs
12.376 |>> append built_in_nondefs
12.377 - val defs = built_in_built_in_defs @
12.378 - (thy |> PureThy.all_thms_of
12.379 + val defs = (thy |> PureThy.all_thms_of
12.380 |> filter (equal Thm.definitionK o Thm.get_kind o snd)
12.381 |> map (prop_of o snd) |> filter is_plain_definition) @
12.382 user_defs @ built_in_defs
12.383 @@ -1185,7 +1189,7 @@
12.384 cons (case_name, AList.lookup (op =) descr index
12.385 |> the |> #3 |> length))
12.386 (Datatype.get_all thy) [] @
12.387 - map (apsnd length o snd) (#codatatypes (TheoryData.get thy))
12.388 + map (apsnd length o snd) (#codatatypes (Data.get thy))
12.389
12.390 (* Proof.context -> term list -> const_table *)
12.391 fun const_def_table ctxt ts =
12.392 @@ -1221,7 +1225,7 @@
12.393
12.394 (* theory -> (string * string) list *)
12.395 fun ersatz_table thy =
12.396 - fold (append o snd) (#frac_types (TheoryData.get thy)) basic_ersatz_table
12.397 + fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
12.398
12.399 (* const_table Unsynchronized.ref -> string -> term list -> unit *)
12.400 fun add_simps simp_table s eqs =
12.401 @@ -1238,7 +1242,7 @@
12.402 if s = s' then
12.403 ys |> (if AList.defined (op =) ys T' then
12.404 I
12.405 - else
12.406 + else
12.407 cons (T', Refute.monomorphic_term
12.408 (Sign.typ_match thy (T', T) Vartab.empty) t)
12.409 handle Type.TYPE_MATCH => I
12.410 @@ -1292,29 +1296,26 @@
12.411 list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
12.412 (index_seq 0 (length arg_Ts)) arg_Ts)
12.413 end
12.414 -(* theory -> typ -> int * styp -> term -> term *)
12.415 -fun add_constr_case thy res_T (j, x) res_t =
12.416 +(* extended_context -> typ -> int * styp -> term -> term *)
12.417 +fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
12.418 Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
12.419 - $ discriminate_value thy x (Bound 0) $ constr_case_body thy (j, x) $ res_t
12.420 -(* theory -> typ -> typ -> term *)
12.421 -fun optimized_case_def thy dataT res_T =
12.422 + $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
12.423 + $ res_t
12.424 +(* extended_context -> typ -> typ -> term *)
12.425 +fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
12.426 let
12.427 - val xs = datatype_constrs thy dataT
12.428 + val xs = datatype_constrs ext_ctxt dataT
12.429 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
12.430 val (xs', x) = split_last xs
12.431 in
12.432 constr_case_body thy (1, x)
12.433 - |> fold_rev (add_constr_case thy res_T) (length xs downto 2 ~~ xs')
12.434 + |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
12.435 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
12.436 end
12.437
12.438 -val redefined_in_Nitpick_thy =
12.439 - [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
12.440 - @{const_name list_size}]
12.441 -
12.442 -(* theory -> string -> typ -> typ -> term -> term *)
12.443 -fun optimized_record_get thy s rec_T res_T t =
12.444 - let val constr_x = the_single (datatype_constrs thy rec_T) in
12.445 +(* extended_context -> string -> typ -> typ -> term -> term *)
12.446 +fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
12.447 + let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
12.448 case no_of_record_field thy s rec_T of
12.449 ~1 => (case rec_T of
12.450 Type (_, Ts as _ :: _) =>
12.451 @@ -1323,16 +1324,16 @@
12.452 val j = num_record_fields thy rec_T - 1
12.453 in
12.454 select_nth_constr_arg thy constr_x t j res_T
12.455 - |> optimized_record_get thy s rec_T' res_T
12.456 + |> optimized_record_get ext_ctxt s rec_T' res_T
12.457 end
12.458 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
12.459 []))
12.460 | j => select_nth_constr_arg thy constr_x t j res_T
12.461 end
12.462 -(* theory -> string -> typ -> term -> term -> term *)
12.463 -fun optimized_record_update thy s rec_T fun_t rec_t =
12.464 +(* extended_context -> string -> typ -> term -> term -> term *)
12.465 +fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
12.466 let
12.467 - val constr_x as (_, constr_T) = the_single (datatype_constrs thy rec_T)
12.468 + val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
12.469 val Ts = binder_types constr_T
12.470 val n = length Ts
12.471 val special_j = no_of_record_field thy s rec_T
12.472 @@ -1343,7 +1344,7 @@
12.473 if j = special_j then
12.474 betapply (fun_t, t)
12.475 else if j = n - 1 andalso special_j = ~1 then
12.476 - optimized_record_update thy s
12.477 + optimized_record_update ext_ctxt s
12.478 (rec_T |> dest_Type |> snd |> List.last) fun_t t
12.479 else
12.480 t
12.481 @@ -1381,7 +1382,6 @@
12.482 (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
12.483 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
12.484 andf (not o has_trivial_definition thy def_table)
12.485 - andf (not o member (op =) redefined_in_Nitpick_thy o fst)
12.486
12.487 (* term * term -> term *)
12.488 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
12.489 @@ -1488,7 +1488,7 @@
12.490 val (const, ts) =
12.491 if is_built_in_const fast_descrs x then
12.492 if s = @{const_name finite} then
12.493 - if is_finite_type thy (domain_type T) then
12.494 + if is_finite_type ext_ctxt (domain_type T) then
12.495 (Abs ("A", domain_type T, @{const True}), ts)
12.496 else case ts of
12.497 [Const (@{const_name UNIV}, _)] => (@{const False}, [])
12.498 @@ -1501,24 +1501,26 @@
12.499 val (dataT, res_T) = nth_range_type n T
12.500 |> domain_type pairf range_type
12.501 in
12.502 - (optimized_case_def thy dataT res_T
12.503 + (optimized_case_def ext_ctxt dataT res_T
12.504 |> do_term (depth + 1) Ts, ts)
12.505 end
12.506 | _ =>
12.507 if is_constr thy x then
12.508 (Const x, ts)
12.509 + else if is_stale_constr thy x then
12.510 + raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
12.511 + \(\"" ^ s ^ "\")")
12.512 else if is_record_get thy x then
12.513 case length ts of
12.514 0 => (do_term depth Ts (eta_expand Ts t 1), [])
12.515 - | _ => (optimized_record_get thy s (domain_type T)
12.516 + | _ => (optimized_record_get ext_ctxt s (domain_type T)
12.517 (range_type T) (hd ts), tl ts)
12.518 else if is_record_update thy x then
12.519 case length ts of
12.520 - 2 => (optimized_record_update thy (unsuffix Record.updateN s)
12.521 - (nth_range_type 2 T)
12.522 - (do_term depth Ts (hd ts))
12.523 - (do_term depth Ts (nth ts 1)),
12.524 - [])
12.525 + 2 => (optimized_record_update ext_ctxt
12.526 + (unsuffix Record.updateN s) (nth_range_type 2 T)
12.527 + (do_term depth Ts (hd ts))
12.528 + (do_term depth Ts (nth ts 1)), [])
12.529 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
12.530 else if is_rep_fun thy x then
12.531 let val x' = mate_of_rep_fun thy x in
12.532 @@ -1545,10 +1547,10 @@
12.533 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
12.534 in do_term 0 [] end
12.535
12.536 -(* theory -> typ -> term list *)
12.537 -fun codatatype_bisim_axioms thy T =
12.538 +(* extended_context -> typ -> term list *)
12.539 +fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
12.540 let
12.541 - val xs = datatype_constrs thy T
12.542 + val xs = datatype_constrs ext_ctxt T
12.543 val set_T = T --> bool_T
12.544 val iter_T = @{typ bisim_iterator}
12.545 val bisim_const = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
12.546 @@ -1571,14 +1573,14 @@
12.547 let
12.548 val arg_Ts = binder_types T
12.549 val core_t =
12.550 - discriminate_value thy x y_var ::
12.551 + discriminate_value ext_ctxt x y_var ::
12.552 map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
12.553 |> foldr1 s_conj
12.554 in List.foldr absdummy core_t arg_Ts end
12.555 in
12.556 [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
12.557 $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
12.558 - $ (betapplys (optimized_case_def thy T bool_T,
12.559 + $ (betapplys (optimized_case_def ext_ctxt T bool_T,
12.560 map case_func xs @ [x_var]))),
12.561 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
12.562 $ (Const (@{const_name insert}, [T, set_T] ---> set_T)
12.563 @@ -1629,6 +1631,7 @@
12.564 (tac ctxt (auto_tac (clasimpset_of ctxt))))
12.565 #> the #> Goal.finish ctxt) goal
12.566
12.567 +val max_cached_wfs = 100
12.568 val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
12.569 val cached_wf_props : (term * bool) list Unsynchronized.ref =
12.570 Unsynchronized.ref []
12.571 @@ -1637,11 +1640,11 @@
12.572 ScnpReconstruct.sizechange_tac]
12.573
12.574 (* extended_context -> const_table -> styp -> bool *)
12.575 -fun is_is_well_founded_inductive_pred
12.576 +fun uncached_is_well_founded_inductive_pred
12.577 ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
12.578 : extended_context) (x as (_, T)) =
12.579 case def_props_for_const thy fast_descrs intro_table x of
12.580 - [] => raise TERM ("Nitpick_HOL.is_is_well_founded_inductive_pred",
12.581 + [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
12.582 [Const x])
12.583 | intro_ts =>
12.584 (case map (triple_for_intro_rule thy x) intro_ts
12.585 @@ -1662,8 +1665,11 @@
12.586 else
12.587 ()
12.588 in
12.589 - if tac_timeout = (!cached_timeout) then ()
12.590 - else (cached_wf_props := []; cached_timeout := tac_timeout);
12.591 + if tac_timeout = (!cached_timeout)
12.592 + andalso length (!cached_wf_props) < max_cached_wfs then
12.593 + ()
12.594 + else
12.595 + (cached_wf_props := []; cached_timeout := tac_timeout);
12.596 case AList.lookup (op =) (!cached_wf_props) prop of
12.597 SOME wf => wf
12.598 | NONE =>
12.599 @@ -1690,7 +1696,7 @@
12.600 | NONE =>
12.601 let
12.602 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
12.603 - val wf = is_is_well_founded_inductive_pred ext_ctxt x
12.604 + val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
12.605 in
12.606 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
12.607 end
12.608 @@ -1878,9 +1884,7 @@
12.609 (* extended_context -> styp -> term list *)
12.610 fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
12.611 psimp_table, ...}) (x as (s, _)) =
12.612 - if s mem redefined_in_Nitpick_thy then
12.613 - []
12.614 - else case def_props_for_const thy fast_descrs (!simp_table) x of
12.615 + case def_props_for_const thy fast_descrs (!simp_table) x of
12.616 [] => (case def_props_for_const thy fast_descrs psimp_table x of
12.617 [] => [inductive_pred_axiom ext_ctxt x]
12.618 | psimps => psimps)
12.619 @@ -1889,7 +1893,7 @@
12.620 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
12.621
12.622 (* term list -> term list *)
12.623 -fun coalesce_type_vars_in_terms ts =
12.624 +fun merge_type_vars_in_terms ts =
12.625 let
12.626 (* typ -> (sort * string) list -> (sort * string) list *)
12.627 fun add_type (TFree (s, S)) table =
12.628 @@ -2002,8 +2006,8 @@
12.629 seen, concl)
12.630 end
12.631
12.632 -(* theory -> bool -> term -> term *)
12.633 -fun destroy_pulled_out_constrs thy axiom t =
12.634 +(* extended_context -> bool -> term -> term *)
12.635 +fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
12.636 let
12.637 (* styp -> int *)
12.638 val num_occs_of_var =
12.639 @@ -2037,7 +2041,7 @@
12.640 andalso (not careful orelse not (is_Var t1)
12.641 orelse String.isPrefix val_var_prefix
12.642 (fst (fst (dest_Var t1)))) then
12.643 - discriminate_value thy x t1 ::
12.644 + discriminate_value ext_ctxt x t1 ::
12.645 map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
12.646 |> foldr1 s_conj
12.647 |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
12.648 @@ -2564,7 +2568,6 @@
12.649 t
12.650 else
12.651 let
12.652 - (* FIXME: strong enough in the face of user-defined axioms? *)
12.653 val blacklist = if depth = 0 then []
12.654 else case term_under_def t of Const x => [x] | _ => []
12.655 (* term list -> typ list -> term -> term *)
12.656 @@ -2727,7 +2730,7 @@
12.657 | (Type (new_s, new_Ts as [new_T1, new_T2]),
12.658 Type (old_s, old_Ts as [old_T1, old_T2])) =>
12.659 if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
12.660 - case constr_expand thy old_T t of
12.661 + case constr_expand ext_ctxt old_T t of
12.662 Const (@{const_name FunBox}, _) $ t1 =>
12.663 if new_s = "fun" then
12.664 coerce_term Ts new_T (Type ("fun", old_Ts)) t1
12.665 @@ -3030,14 +3033,16 @@
12.666 else if is_abs_fun thy x then
12.667 accum |> fold (add_nondef_axiom depth)
12.668 (nondef_props_for_const thy false nondef_table x)
12.669 - |> fold (add_def_axiom depth)
12.670 - (nondef_props_for_const thy true
12.671 + |> is_funky_typedef thy (range_type T)
12.672 + ? fold (add_def_axiom depth)
12.673 + (nondef_props_for_const thy true
12.674 (extra_table def_table s) x)
12.675 else if is_rep_fun thy x then
12.676 accum |> fold (add_nondef_axiom depth)
12.677 (nondef_props_for_const thy false nondef_table x)
12.678 - |> fold (add_def_axiom depth)
12.679 - (nondef_props_for_const thy true
12.680 + |> is_funky_typedef thy (range_type T)
12.681 + ? fold (add_def_axiom depth)
12.682 + (nondef_props_for_const thy true
12.683 (extra_table def_table s) x)
12.684 |> add_axioms_for_term depth
12.685 (Const (mate_of_rep_fun thy x))
12.686 @@ -3068,7 +3073,7 @@
12.687 #> (if is_pure_typedef thy T then
12.688 fold (add_def_axiom depth) (optimized_typedef_axioms thy z)
12.689 else if max_bisim_depth >= 0 andalso is_codatatype thy T then
12.690 - fold (add_def_axiom depth) (codatatype_bisim_axioms thy T)
12.691 + fold (add_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T)
12.692 else
12.693 I)
12.694 (* int -> typ -> sort -> accumulator -> accumulator *)
12.695 @@ -3312,7 +3317,7 @@
12.696 #> maybe_box ? box_fun_and_pair_in_term ext_ctxt def
12.697 #> destroy_constrs ? (pull_out_universal_constrs thy def
12.698 #> pull_out_existential_constrs thy
12.699 - #> destroy_pulled_out_constrs thy def)
12.700 + #> destroy_pulled_out_constrs ext_ctxt def)
12.701 #> curry_assms
12.702 #> destroy_universal_equalities
12.703 #> destroy_existential_equalities thy
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Nov 10 13:17:50 2009 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Nov 10 13:54:00 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 @@ -125,30 +132,22 @@
13.65 | _ => value)
13.66 | NONE => (name, value)
13.67
13.68 -structure TheoryData = Theory_Data(
13.69 - type T = {params: raw_param list, registered_auto: bool}
13.70 - val empty = {params = rev default_default_params, registered_auto = false}
13.71 +structure Data = Theory_Data(
13.72 + type T = {params: raw_param list}
13.73 + val empty = {params = rev default_default_params}
13.74 + val copy = I
13.75 val extend = I
13.76 - fun merge ({params = ps1, registered_auto = a1},
13.77 - {params = ps2, registered_auto = a2}) : T =
13.78 - {params = AList.merge (op =) (op =) (ps1, ps2),
13.79 - registered_auto = a1 orelse a2})
13.80 + fun merge _ ({params = ps1}, {params = ps2}) =
13.81 + {params = AList.merge (op =) (op =) (ps1, ps2)})
13.82
13.83 (* raw_param -> theory -> theory *)
13.84 fun set_default_raw_param param thy =
13.85 - let val {params, registered_auto} = TheoryData.get thy in
13.86 - TheoryData.put
13.87 - {params = AList.update (op =) (unnegate_raw_param param) params,
13.88 - registered_auto = registered_auto} thy
13.89 + let val {params} = Data.get thy in
13.90 + Data.put {params = AList.update (op =) (unnegate_raw_param param) params}
13.91 + thy
13.92 end
13.93 (* theory -> raw_param list *)
13.94 -val default_raw_params = #params o TheoryData.get
13.95 -
13.96 -(* theory -> theory *)
13.97 -fun set_registered_auto thy =
13.98 - TheoryData.put {params = default_raw_params thy, registered_auto = true} thy
13.99 -(* theory -> bool *)
13.100 -val is_registered_auto = #registered_auto o TheoryData.get
13.101 +val default_raw_params = #params o Data.get
13.102
13.103 (* string -> bool *)
13.104 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
13.105 @@ -304,7 +303,7 @@
13.106 val overlord = lookup_bool "overlord"
13.107 val user_axioms = lookup_bool_option "user_axioms"
13.108 val assms = lookup_bool "assms"
13.109 - val coalesce_type_vars = lookup_bool "coalesce_type_vars"
13.110 + val merge_type_vars = lookup_bool "merge_type_vars"
13.111 val destroy_constrs = lookup_bool "destroy_constrs"
13.112 val specialize = lookup_bool "specialize"
13.113 val skolemize = lookup_bool "skolemize"
13.114 @@ -312,8 +311,7 @@
13.115 val uncurry = lookup_bool "uncurry"
13.116 val fast_descrs = lookup_bool "fast_descrs"
13.117 val peephole_optim = lookup_bool "peephole_optim"
13.118 - val timeout = if auto then lookup_time "auto_timeout"
13.119 - else lookup_time "timeout"
13.120 + val timeout = if auto then NONE else lookup_time "timeout"
13.121 val tac_timeout = lookup_time "tac_timeout"
13.122 val sym_break = Int.max (0, lookup_int "sym_break")
13.123 val sharing_depth = Int.max (1, lookup_int "sharing_depth")
13.124 @@ -325,8 +323,8 @@
13.125 val show_consts = show_all orelse lookup_bool "show_consts"
13.126 val formats = lookup_ints_assigns read_term_polymorphic "format" 0
13.127 val evals = lookup_term_list "eval"
13.128 - val max_potential = if auto then 0
13.129 - else Int.max (0, lookup_int "max_potential")
13.130 + val max_potential =
13.131 + if auto then 0 else Int.max (0, lookup_int "max_potential")
13.132 val max_genuine = Int.max (0, lookup_int "max_genuine")
13.133 val check_potential = lookup_bool "check_potential"
13.134 val check_genuine = lookup_bool "check_genuine"
13.135 @@ -340,7 +338,7 @@
13.136 monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
13.137 falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
13.138 user_axioms = user_axioms, assms = assms,
13.139 - coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs,
13.140 + merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs,
13.141 specialize = specialize, skolemize = skolemize,
13.142 star_linear_preds = star_linear_preds, uncurry = uncurry,
13.143 fast_descrs = fast_descrs, peephole_optim = peephole_optim,
13.144 @@ -411,7 +409,7 @@
13.145 | Refute.REFUTE (loc, details) =>
13.146 error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
13.147
13.148 -(* raw_param list -> bool -> int -> Proof.state -> Proof.state *)
13.149 +(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
13.150 fun pick_nits override_params auto subgoal state =
13.151 let
13.152 val thy = Proof.theory_of state
13.153 @@ -420,70 +418,49 @@
13.154 val _ = List.app check_raw_param override_params
13.155 val params as {blocking, debug, ...} =
13.156 extract_params ctxt auto (default_raw_params thy) override_params
13.157 - (* unit -> Proof.state *)
13.158 + (* unit -> bool * Proof.state *)
13.159 fun go () =
13.160 - (if auto then perhaps o try
13.161 - else if debug then fn f => fn x => f x
13.162 - else handle_exceptions ctxt)
13.163 - (fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
13.164 - state
13.165 + (false, state)
13.166 + |> (if auto then perhaps o try
13.167 + else if debug then fn f => fn x => f x
13.168 + else handle_exceptions ctxt)
13.169 + (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
13.170 + |>> equal "genuine")
13.171 in
13.172 - if auto orelse blocking then
13.173 - go ()
13.174 - else
13.175 - (SimpleThread.fork true (fn () => (go (); ()));
13.176 - state)
13.177 + if auto orelse blocking then go ()
13.178 + else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
13.179 end
13.180
13.181 (* (TableFun().key * string list) list option * int option
13.182 -> Toplevel.transition -> Toplevel.transition *)
13.183 fun nitpick_trans (opt_params, opt_subgoal) =
13.184 Toplevel.keep (K ()
13.185 - o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
13.186 + o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
13.187 o Toplevel.proof_of)
13.188
13.189 (* raw_param -> string *)
13.190 fun string_for_raw_param (name, value) =
13.191 name ^ " = " ^ stringify_raw_param_value value
13.192
13.193 -(* bool -> Proof.state -> Proof.state *)
13.194 -fun pick_nits_auto interactive state =
13.195 - let val thy = Proof.theory_of state in
13.196 - ((interactive andalso not (!Toplevel.quiet)
13.197 - andalso the (general_lookup_bool false (default_raw_params thy)
13.198 - (SOME false) "auto"))
13.199 - ? pick_nits [] true 0) state
13.200 - end
13.201 -
13.202 -(* theory -> theory *)
13.203 -fun register_auto thy =
13.204 - (not (is_registered_auto thy)
13.205 - ? (set_registered_auto
13.206 - #> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))
13.207 - thy
13.208 -
13.209 (* (TableFun().key * string) list option -> Toplevel.transition
13.210 -> Toplevel.transition *)
13.211 fun nitpick_params_trans opt_params =
13.212 Toplevel.theory
13.213 - (fn thy =>
13.214 - let val thy = fold set_default_raw_param (these opt_params) thy in
13.215 - writeln ("Default parameters for Nitpick:\n" ^
13.216 - (case rev (default_raw_params thy) of
13.217 - [] => "none"
13.218 - | params =>
13.219 - (map check_raw_param params;
13.220 - params |> map string_for_raw_param |> sort_strings
13.221 - |> cat_lines)));
13.222 - register_auto thy
13.223 - end)
13.224 + (fold set_default_raw_param (these opt_params)
13.225 + #> tap (fn thy =>
13.226 + writeln ("Default parameters for Nitpick:\n" ^
13.227 + (case rev (default_raw_params thy) of
13.228 + [] => "none"
13.229 + | params =>
13.230 + (map check_raw_param params;
13.231 + params |> map string_for_raw_param
13.232 + |> sort_strings |> cat_lines)))))
13.233
13.234 (* OuterParse.token list
13.235 -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
13.236 -fun scan_nitpick_command tokens =
13.237 - (scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
13.238 -fun scan_nitpick_params_command tokens =
13.239 - scan_params tokens |>> nitpick_params_trans
13.240 +val scan_nitpick_command =
13.241 + (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
13.242 +val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
13.243
13.244 val _ = OuterSyntax.improper_command "nitpick"
13.245 "try to find a counterexample for a given subgoal using Kodkod"
13.246 @@ -492,4 +469,10 @@
13.247 "set and display the default parameters for Nitpick"
13.248 OuterKeyword.thy_decl scan_nitpick_params_command
13.249
13.250 +(* Proof.state -> bool * Proof.state *)
13.251 +fun auto_nitpick state =
13.252 + if not (!auto) then (false, state) else pick_nits [] true 1 state
13.253 +
13.254 +val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
13.255 +
13.256 end;
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Nov 10 13:17:50 2009 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Nov 10 13:54:00 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 @@ -582,9 +580,9 @@
14.20 val schema = atom_schema_of_rep R1
14.21 val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema))
14.22 |> rel_expr_from_rel_expr kk R1' R1
14.23 + val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk
14.24 in
14.25 - #kk_comprehension kk (decls_for_atom_schema ~1 schema)
14.26 - (#kk_subset kk r1 r)
14.27 + #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)
14.28 end
14.29 | Func (Unit, (Atom (2, j0))) =>
14.30 #kk_rel_if kk (#kk_rel_eq kk r (Kodkod.Atom (j0 + 1)))
14.31 @@ -618,7 +616,7 @@
14.32 val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r)
14.33 in
14.34 #kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x]))
14.35 - (#kk_rel_eq kk r2 r3)
14.36 + (#kk_subset kk r2 r3)
14.37 end
14.38 end
14.39 | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
14.40 @@ -643,10 +641,11 @@
14.41 (length ran_schema))
14.42 |> rel_expr_from_rel_expr kk R2' R2
14.43 val app = kk_n_fold_join kk true R1' R2' dom_prod r
14.44 + val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk
14.45 in
14.46 #kk_comprehension kk (decls_for_atom_schema ~1
14.47 (dom_schema @ ran_schema))
14.48 - (#kk_subset kk ran_prod app)
14.49 + (kk_xeq ran_prod app)
14.50 end
14.51 | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
14.52 [old_R, Func (R1, R2)])
14.53 @@ -716,8 +715,8 @@
14.54 (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
14.55 -> dtype_spec -> nfa_entry option *)
14.56 fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
14.57 - | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes
14.58 - ({typ, constrs, ...} : dtype_spec) =
14.59 + | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE
14.60 + | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
14.61 SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
14.62 o #const) constrs)
14.63
14.64 @@ -884,12 +883,13 @@
14.65
14.66 (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
14.67 -> dtype_spec -> Kodkod.formula list *)
14.68 -fun other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
14.69 - let val j0 = offset_of_type ofs typ in
14.70 - sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
14.71 - uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
14.72 - partition_axioms_for_datatype j0 kk rel_table dtype
14.73 - end
14.74 +fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
14.75 + | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
14.76 + let val j0 = offset_of_type ofs typ in
14.77 + sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
14.78 + uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
14.79 + partition_axioms_for_datatype j0 kk rel_table dtype
14.80 + end
14.81
14.82 (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
14.83 -> dtype_spec list -> Kodkod.formula list *)
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Nov 10 13:17:50 2009 +0100
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Nov 10 13:54:00 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 @@ -527,7 +530,7 @@
15.60 evals, case_names, def_table, nondef_table, user_nondefs,
15.61 simp_table, psimp_table, intro_table, ground_thm_table,
15.62 ersatz_table, skolems, special_funs, unrolled_preds,
15.63 - wf_cache},
15.64 + wf_cache, constr_cache},
15.65 card_assigns, bisim_depth, datatypes, ofs} : scope) formats all_frees
15.66 free_names sel_names nonsel_names rel_table bounds =
15.67 let
15.68 @@ -545,7 +548,7 @@
15.69 intro_table = intro_table, ground_thm_table = ground_thm_table,
15.70 ersatz_table = ersatz_table, skolems = skolems,
15.71 special_funs = special_funs, unrolled_preds = unrolled_preds,
15.72 - wf_cache = wf_cache}
15.73 + wf_cache = wf_cache, constr_cache = constr_cache}
15.74 val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
15.75 bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
15.76 (* typ -> typ -> rep -> int list list -> term *)
15.77 @@ -585,8 +588,7 @@
15.78 |> term_for_rep T T' (rep_of name)
15.79 in
15.80 Pretty.block (Pretty.breaks
15.81 - [(setmp_CRITICAL show_question_marks false o setmp_show_all_types)
15.82 - (Syntax.pretty_term ctxt) t1,
15.83 + [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
15.84 Pretty.str oper, Syntax.pretty_term ctxt t2])
15.85 end
15.86 (* dtype_spec -> Pretty.T *)
15.87 @@ -600,11 +602,12 @@
15.88 (* typ -> dtype_spec list *)
15.89 fun integer_datatype T =
15.90 [{typ = T, card = card_of_type card_assigns T, co = false,
15.91 - precise = false, constrs = []}]
15.92 + precise = false, shallow = false, constrs = []}]
15.93 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
15.94 val (codatatypes, datatypes) =
15.95 - List.partition #co datatypes
15.96 - ||> append (integer_datatype nat_T @ integer_datatype int_T)
15.97 + datatypes |> filter_out #shallow
15.98 + |> List.partition #co
15.99 + ||> append (integer_datatype nat_T @ integer_datatype int_T)
15.100 val block_of_datatypes =
15.101 if show_datatypes andalso not (null datatypes) then
15.102 [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Nov 10 13:17:50 2009 +0100
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Nov 10 13:54:00 2009 +0100
16.3 @@ -215,7 +215,7 @@
16.4 | NONE =>
16.5 let
16.6 val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
16.7 - val xs = datatype_constrs thy T
16.8 + val xs = datatype_constrs ext_ctxt T
16.9 val (all_Cs, constr_Cs) =
16.10 fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
16.11 let
16.12 @@ -505,7 +505,7 @@
16.13 map prop_for_comp comps @
16.14 map prop_for_sign_expr sexps)
16.15 in
16.16 - case silence (SatSolver.invoke_solver "dpll") prop of
16.17 + case SatSolver.invoke_solver "dpll" prop of
16.18 SatSolver.SATISFIABLE asgns =>
16.19 SOME (literals_from_assignments max_var asgns lits
16.20 |> tap print_solution)
16.21 @@ -708,7 +708,7 @@
16.22 (CFun (left_set_C, S Neg,
16.23 CFun (right_set_C, S Neg, left_set_C)),
16.24 (gamma, cset |> add_ctype_is_right_unique right_set_C
16.25 - (* FIXME: |> add_is_sub_ctype right_set_C left_set_C *)))
16.26 + |> add_is_sub_ctype right_set_C left_set_C))
16.27 end
16.28 | @{const_name ord_fun_inst.less_eq_fun} =>
16.29 do_fragile_set_operation T accum
16.30 @@ -784,10 +784,8 @@
16.31 let
16.32 (* typ -> ctype *)
16.33 val ctype_for = fresh_ctype_for_type cdata
16.34 - (* term -> accumulator -> ctype * accumulator *)
16.35 - val do_term = consider_term cdata
16.36 (* term -> accumulator -> accumulator *)
16.37 - val do_boolean_term = snd oo do_term
16.38 + val do_term = snd oo consider_term cdata
16.39 (* sign -> term -> accumulator -> accumulator *)
16.40 fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
16.41 | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
16.42 @@ -812,11 +810,8 @@
16.43 (* term -> term -> accumulator *)
16.44 fun do_equals t1 t2 =
16.45 case sn of
16.46 - Pos => do_boolean_term t accum
16.47 - | Neg => let
16.48 - val (C1, accum) = do_term t1 accum
16.49 - val (C2, accum) = do_term t2 accum
16.50 - in accum (* FIXME: ||> add_ctypes_equal C1 C2 *) end
16.51 + Pos => do_term t accum
16.52 + | Neg => fold do_term [t1, t2] accum
16.53 in
16.54 case t of
16.55 Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
16.56 @@ -844,10 +839,10 @@
16.57 | @{const "op -->"} $ t1 $ t2 =>
16.58 accum |> do_contra_formula t1 |> do_co_formula t2
16.59 | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
16.60 - accum |> do_boolean_term t1 |> do_co_formula t2 |> do_co_formula t3
16.61 + accum |> do_term t1 |> fold do_co_formula [t2, t3]
16.62 | Const (@{const_name Let}, _) $ t1 $ t2 =>
16.63 do_co_formula (betapply (t2, t1)) accum
16.64 - | _ => do_boolean_term t accum
16.65 + | _ => do_term t accum
16.66 end
16.67 |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
16.68 Syntax.string_of_term ctxt t ^
17.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Nov 10 13:17:50 2009 +0100
17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Nov 10 13:54:00 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 Tue Nov 10 13:17:50 2009 +0100
18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Nov 10 13:54:00 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 -> int * 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 @@ -222,33 +224,31 @@
18.38 SOME (Max constr, lookup_const_ints_assign thy maxes_asgns constr)
18.39 handle TERM ("lookup_const_ints_assign", _) => NONE
18.40
18.41 -(* Proof.context -> (typ option * int list) list
18.42 +(* extended_context -> (typ option * int list) list
18.43 -> (styp option * int list) list -> (styp option * int list) list -> int list
18.44 -> typ -> block *)
18.45 -fun block_for_type ctxt cards_asgns maxes_asgns iters_asgns bisim_depths T =
18.46 - let val thy = ProofContext.theory_of ctxt in
18.47 - if T = @{typ bisim_iterator} then
18.48 - [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)]
18.49 - else if is_fp_iterator_type T then
18.50 - [(Card T, map (fn k => Int.max (0, k) + 1)
18.51 - (lookup_const_ints_assign thy iters_asgns
18.52 - (const_for_iterator_type T)))]
18.53 - else
18.54 - (Card T, lookup_type_ints_assign thy cards_asgns T) ::
18.55 - (case datatype_constrs thy T of
18.56 - [_] => []
18.57 - | constrs => map_filter (row_for_constr thy maxes_asgns) constrs)
18.58 - end
18.59 +fun block_for_type (ext_ctxt as {thy, ...}) cards_asgns maxes_asgns iters_asgns
18.60 + bisim_depths T =
18.61 + if T = @{typ bisim_iterator} then
18.62 + [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)]
18.63 + else if is_fp_iterator_type T then
18.64 + [(Card T, map (fn k => Int.max (0, k) + 1)
18.65 + (lookup_const_ints_assign thy iters_asgns
18.66 + (const_for_iterator_type T)))]
18.67 + else
18.68 + (Card T, lookup_type_ints_assign thy cards_asgns T) ::
18.69 + (case datatype_constrs ext_ctxt T of
18.70 + [_] => []
18.71 + | constrs => map_filter (row_for_constr thy maxes_asgns) constrs)
18.72
18.73 -(* Proof.context -> (typ option * int list) list
18.74 +(* extended_context -> (typ option * int list) list
18.75 -> (styp option * int list) list -> (styp option * int list) list -> int list
18.76 -> typ list -> typ list -> block list *)
18.77 -fun blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns bisim_depths
18.78 +fun blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns bisim_depths
18.79 mono_Ts nonmono_Ts =
18.80 let
18.81 - val thy = ProofContext.theory_of ctxt
18.82 (* typ -> block *)
18.83 - val block_for = block_for_type ctxt cards_asgns maxes_asgns iters_asgns
18.84 + val block_for = block_for_type ext_ctxt cards_asgns maxes_asgns iters_asgns
18.85 bisim_depths
18.86 val mono_block = maps block_for mono_Ts
18.87 val nonmono_blocks = map block_for nonmono_Ts
18.88 @@ -289,15 +289,15 @@
18.89
18.90 type scope_desc = (typ * int) list * (styp * int) list
18.91
18.92 -(* theory -> scope_desc -> typ * int -> bool *)
18.93 -fun is_surely_inconsistent_card_assign thy (card_asgns, max_asgns) (T, k) =
18.94 - case datatype_constrs thy T of
18.95 +(* extended_context -> scope_desc -> typ * int -> bool *)
18.96 +fun is_surely_inconsistent_card_assign ext_ctxt (card_asgns, max_asgns) (T, k) =
18.97 + case datatype_constrs ext_ctxt T of
18.98 [] => false
18.99 | xs =>
18.100 let
18.101 val precise_cards =
18.102 map (Integer.prod
18.103 - o map (bounded_precise_card_of_type thy k 0 card_asgns)
18.104 + o map (bounded_precise_card_of_type ext_ctxt k 0 card_asgns)
18.105 o binder_types o snd) xs
18.106 val maxes = map (constr_max max_asgns) xs
18.107 (* int -> int -> int *)
18.108 @@ -317,18 +317,19 @@
18.109 end
18.110 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
18.111
18.112 -(* theory -> scope_desc -> bool *)
18.113 -fun is_surely_inconsistent_scope_description thy (desc as (card_asgns, _)) =
18.114 - exists (is_surely_inconsistent_card_assign thy desc) card_asgns
18.115 +(* extended_context -> scope_desc -> bool *)
18.116 +fun is_surely_inconsistent_scope_description ext_ctxt
18.117 + (desc as (card_asgns, _)) =
18.118 + exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_asgns
18.119
18.120 -(* theory -> scope_desc -> (typ * int) list option *)
18.121 -fun repair_card_assigns thy (card_asgns, max_asgns) =
18.122 +(* extended_context -> scope_desc -> (typ * int) list option *)
18.123 +fun repair_card_assigns ext_ctxt (card_asgns, max_asgns) =
18.124 let
18.125 (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
18.126 fun aux seen [] = SOME seen
18.127 | aux seen ((T, 0) :: _) = NONE
18.128 | aux seen ((T, k) :: asgns) =
18.129 - (if is_surely_inconsistent_scope_description thy
18.130 + (if is_surely_inconsistent_scope_description ext_ctxt
18.131 ((T, k) :: seen, max_asgns) then
18.132 raise SAME ()
18.133 else
18.134 @@ -360,12 +361,12 @@
18.135 (* block -> scope_desc *)
18.136 fun scope_descriptor_from_block block =
18.137 fold_rev add_row_to_scope_descriptor block ([], [])
18.138 -(* theory -> block list -> int list -> scope_desc option *)
18.139 -fun scope_descriptor_from_combination thy blocks columns =
18.140 +(* extended_context -> block list -> int list -> scope_desc option *)
18.141 +fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
18.142 let
18.143 val (card_asgns, max_asgns) =
18.144 maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
18.145 - val card_asgns = repair_card_assigns thy (card_asgns, max_asgns) |> the
18.146 + val card_asgns = repair_card_assigns ext_ctxt (card_asgns, max_asgns) |> the
18.147 in
18.148 SOME (map (repair_iterator_assign thy card_asgns) card_asgns, max_asgns)
18.149 end
18.150 @@ -431,16 +432,17 @@
18.151 explicit_max = max, total = total} :: constrs
18.152 end
18.153
18.154 -(* extended_context -> scope_desc -> typ * int -> dtype_spec *)
18.155 -fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...})
18.156 +(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
18.157 +fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
18.158 (desc as (card_asgns, _)) (T, card) =
18.159 let
18.160 + val shallow = T mem shallow_dataTs
18.161 val co = is_codatatype thy T
18.162 val xs = boxed_datatype_constrs ext_ctxt T
18.163 val self_recs = map (is_self_recursive_constr_type o snd) xs
18.164 val (num_self_recs, num_non_self_recs) =
18.165 List.partition (equal true) self_recs |> pairself length
18.166 - val precise = (card = bounded_precise_card_of_type thy (card + 1) 0
18.167 + val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0
18.168 card_asgns T)
18.169 (* int -> int *)
18.170 fun sum_dom_cards max =
18.171 @@ -448,14 +450,18 @@
18.172 val constrs =
18.173 fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
18.174 num_non_self_recs) (self_recs ~~ xs) []
18.175 - in {typ = T, card = card, co = co, precise = precise, constrs = constrs} end
18.176 + in
18.177 + {typ = T, card = card, co = co, precise = precise, shallow = shallow,
18.178 + constrs = constrs}
18.179 + end
18.180
18.181 -(* extended_context -> int -> scope_desc -> scope *)
18.182 -fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break
18.183 +(* extended_context -> int -> typ list -> scope_desc -> scope *)
18.184 +fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
18.185 (desc as (card_asgns, _)) =
18.186 let
18.187 - val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt desc)
18.188 - (filter (is_datatype thy o fst) card_asgns)
18.189 + val datatypes =
18.190 + map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
18.191 + (filter (is_datatype thy o fst) card_asgns)
18.192 val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1
18.193 in
18.194 {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes,
18.195 @@ -476,23 +482,27 @@
18.196 | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_asgns) =
18.197 (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_asgns
18.198
18.199 +val max_scopes = 4096
18.200 val distinct_threshold = 512
18.201
18.202 (* extended_context -> int -> (typ option * int list) list
18.203 -> (styp option * int list) list -> (styp option * int list) list -> int list
18.204 - -> typ list -> typ list -> scope list *)
18.205 -fun all_scopes (ext_ctxt as {thy, ctxt, ...}) sym_break cards_asgns maxes_asgns
18.206 - iters_asgns bisim_depths mono_Ts nonmono_Ts =
18.207 + -> typ list -> typ list -> typ list -> int * scope list *)
18.208 +fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_asgns maxes_asgns
18.209 + iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
18.210 let
18.211 val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns
18.212 - val blocks = blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns
18.213 + val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns
18.214 bisim_depths mono_Ts nonmono_Ts
18.215 val ranks = map rank_of_block blocks
18.216 - val descs = all_combinations_ordered_smartly (map (rpair 0) ranks)
18.217 - |> map_filter (scope_descriptor_from_combination thy blocks)
18.218 + val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
18.219 + val head = Library.take (max_scopes, all)
18.220 + val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
18.221 + head
18.222 in
18.223 - descs |> length descs <= distinct_threshold ? distinct (op =)
18.224 - |> map (scope_from_descriptor ext_ctxt sym_break)
18.225 + (length all - length head,
18.226 + descs |> length descs <= distinct_threshold ? distinct (op =)
18.227 + |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs))
18.228 end
18.229
18.230 end;
19.1 --- a/src/HOL/Tools/inductive.ML Tue Nov 10 13:17:50 2009 +0100
19.2 +++ b/src/HOL/Tools/inductive.ML Tue Nov 10 13:54:00 2009 +0100
19.3 @@ -665,7 +665,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 lthy;
19.12 val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
20.1 --- a/src/HOL/Tools/sat_solver.ML Tue Nov 10 13:17:50 2009 +0100
20.2 +++ b/src/HOL/Tools/sat_solver.ML Tue Nov 10 13:54:00 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 Tue Nov 10 13:54:00 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 Tue Nov 10 13:17:50 2009 +0100
22.2 +++ b/src/Tools/Code_Generator.thy Tue Nov 10 13:54:00 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 Tue Nov 10 13:54:00 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 Tue Nov 10 13:17:50 2009 +0100
24.2 +++ b/src/Tools/quickcheck.ML Tue Nov 10 13:54:00 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;