# HG changeset patch # User blanchet # Date 1261134044 -3600 # Node ID 85257fa296f6e98ed83d6147226e7563bcbe36d9 # Parent b1cabadf68811842cff7287d1ae30585bea636a6# Parent 8a2c5d7aff51f7938bd06a1cfb1647a41f81237e merged diff -r b1cabadf6881 -r 85257fa296f6 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Fri Dec 18 11:28:24 2009 +0100 +++ b/doc-src/Nitpick/nitpick.tex Fri Dec 18 12:00:44 2009 +0100 @@ -436,12 +436,10 @@ \label{natural-numbers-and-integers} Because of the axiom of infinity, the type \textit{nat} does not admit any -finite models. To deal with this, Nitpick considers prefixes $\{0,\, 1,\, -\ldots,\, K - 1\}$ of \textit{nat} (where $K = \textit{card}~\textit{nat}$) and -maps all other numbers to the undefined value ($\unk$). The type \textit{int} is -handled in a similar way: If $K = \textit{card}~\textit{int}$, the subset of -\textit{int} known to Nitpick is $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor -K/2 \rfloor\}$. Undefined values lead to a three-valued logic. +finite models. To deal with this, Nitpick's approach is to consider finite +subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined +value (displayed as `$\unk$'). The type \textit{int} is handled similarly. +Internally, undefined values lead to a three-valued logic. Here is an example involving \textit{int}: @@ -456,15 +454,26 @@ \hbox{}\qquad\qquad $n = 0$ \postw +Internally, Nitpick uses either a unary or a binary representation of numbers. +The unary representation is more efficient but only suitable for numbers very +close to zero. By default, Nitpick attempts to choose the more appropriate +encoding by inspecting the formula at hand. This behavior can be overridden by +passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For +binary notation, the number of bits to use can be specified using +the \textit{bits} option. For example: + +\prew +\textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$] +\postw + With infinite types, we don't always have the luxury of a genuine counterexample and must often content ourselves with a potential one. The tedious task of finding out whether the potential counterexample is in fact genuine can be -outsourced to \textit{auto} by passing the option \textit{check\_potential}. For -example: +outsourced to \textit{auto} by passing \textit{check\_potential}. For example: \prew \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ -\textbf{nitpick} [\textit{card~nat}~= 100,\, \textit{check\_potential}] \\[2\smallskipamount] +\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount] \slshape Nitpick found a potential counterexample: \\[2\smallskipamount] \hbox{}\qquad Free variable: \nopagebreak \\ \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount] @@ -482,7 +491,7 @@ Incidentally, if you distrust the so-called genuine counterexamples, you can enable \textit{check\_\allowbreak genuine} to verify them as well. However, be -aware that \textit{auto} will often fail to prove that the counterexample is +aware that \textit{auto} will usually fail to prove that the counterexample is genuine or spurious. Some conjectures involving elementary number theory make Nitpick look like a @@ -495,10 +504,11 @@ Nitpick found no counterexample. \postw -For any cardinality $k$, \textit{Suc} is the partial function $\{0 \mapsto 1,\, -1 \mapsto 2,\, \ldots,\, k - 1 \mapsto \unk\}$, which evaluates to $\unk$ when -it is passed as argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. -The next example is similar: +On any finite set $N$, \textit{Suc} is a partial function; for example, if $N = +\{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\, +\ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as +argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next +example is similar: \prew \textbf{lemma} ``$P~(\textit{op}~{+}\Colon @@ -730,7 +740,7 @@ \prew \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ -\textbf{nitpick}~[\textit{card nat}~= 100,\, \textit{verbose}] \\[2\smallskipamount] +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount] \slshape The inductive predicate ``\textit{even}'' was proved well-founded. Nitpick can compute it efficiently. \\[2\smallskipamount] Trying 1 scope: \\ @@ -748,7 +758,7 @@ \prew \textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ -\textbf{nitpick}~[\textit{card nat}~= 100] \\[2\smallskipamount] +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount] \slshape Nitpick found a counterexample: \\[2\smallskipamount] \hbox{}\qquad Empty assignment \postw @@ -822,7 +832,7 @@ \prew \textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\ -\textbf{nitpick} [\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount] +\textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount] \slshape Nitpick found a counterexample: \\[2\smallskipamount] \hbox{}\qquad Free variable: \nopagebreak \\ \hbox{}\qquad\qquad $n = 1$ \\ @@ -989,7 +999,7 @@ \prew \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\ -\textbf{nitpick} [\textit{bisim\_depth} = $-1$,\, \textit{show\_datatypes}] \\[2\smallskipamount] +\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount] \slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount] \hbox{}\qquad Free variables: \nopagebreak \\ \hbox{}\qquad\qquad $a = a_2$ \\ @@ -1687,23 +1697,7 @@ \begin{enum} \opu{card}{type}{int\_seq} -Specifies the sequence of cardinalities to use for a given type. For -\textit{nat} and \textit{int}, the cardinality fully specifies the subset used -to approximate the type. For example: -% -$$\hbox{\begin{tabular}{@{}rll@{}}% -\textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\ -\textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\ -\textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$% -\end{tabular}}$$ -% -In general: -% -$$\hbox{\begin{tabular}{@{}rll@{}}% -\textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\ -\textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$% -\end{tabular}}$$ -% +Specifies the sequence of cardinalities to use for a given type. For free types, and often also for \textbf{typedecl}'d types, it usually makes sense to specify cardinalities as a range of the form \textit{$1$--$n$}. Although function and product types are normally mapped directly to the @@ -1731,6 +1725,44 @@ (co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor basis using the \textit{max}~\qty{const} option described above. +\opsmart{binary\_ints}{unary\_ints} +Specifies whether natural numbers and integers should be encoded using a unary +or binary notation. In unary mode, the cardinality fully specifies the subset +used to approximate the type. For example: +% +$$\hbox{\begin{tabular}{@{}rll@{}}% +\textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\ +\textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\ +\textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$% +\end{tabular}}$$ +% +In general: +% +$$\hbox{\begin{tabular}{@{}rll@{}}% +\textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\ +\textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$% +\end{tabular}}$$ +% +In binary mode, the cardinality specifies the number of distinct values that can +be constructed. Each of these value is represented by a bit pattern whose length +is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default, +Nitpick attempts to choose the more appropriate encoding by inspecting the +formula at hand, preferring the binary notation for problems involving +multiplicative operators or large constants. + +\textbf{Warning:} For technical reasons, Nitpick always reverts to unary for +problems that refer to the types \textit{rat} or \textit{real} or the constants +\textit{Suc}, \textit{gcd}, or \textit{lcm}. + +{\small See also \textit{bits} (\S\ref{scope-of-search}) and +\textit{show\_datatypes} (\S\ref{output-format}).} + +\opt{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$} +Specifies the number of bits to use to represent natural numbers and integers in +binary, excluding the sign bit. The minimum is 1 and the maximum is 31. + +{\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).} + \opusmart{wf}{const}{non\_wf} Specifies whether the specified (co)in\-duc\-tively defined predicate is well-founded. The option can take the following values: diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Divides.thy Fri Dec 18 12:00:44 2009 +0100 @@ -2443,6 +2443,17 @@ declare dvd_eq_mod_eq_0_number_of [simp] +subsubsection {* Nitpick *} + +lemma zmod_zdiv_equality': +"(m\int) mod n = m - (m div n) * n" +by (rule_tac P="%x. m mod n = x - (m div n) * n" + in subst [OF mod_div_equality [of _ n]]) + arith + +lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection] + zmod_zdiv_equality' [THEN eq_reflection] + subsubsection {* Code generation *} definition pdivmod :: "int \ int \ int \ int" where diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/IsaMakefile Fri Dec 18 12:00:44 2009 +0100 @@ -610,13 +610,13 @@ HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz -$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ - Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \ - Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \ - Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \ - Nitpick_Examples/Nitpick_Examples.thy \ - Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \ - Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \ +$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ + Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \ + Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Integer_Nits.thy \ + Nitpick_Examples/Manual_Nits.thy Nitpick_Examples/Mini_Nits.thy \ + Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \ + Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \ + Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \ Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Nitpick.thy Fri Dec 18 12:00:44 2009 +0100 @@ -36,7 +36,12 @@ and Tha :: "('a \ bool) \ 'a" datatype ('a, 'b) pair_box = PairBox 'a 'b -datatype ('a, 'b) fun_box = FunBox "'a \ 'b" +datatype ('a, 'b) fun_box = FunBox "('a \ 'b)" + +typedecl unsigned_bit +typedecl signed_bit + +datatype 'a word = Word "('a set)" text {* Alternative definitions. @@ -126,8 +131,6 @@ declare nat.cases [nitpick_simp del] -lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection] - lemma list_size_simp [nitpick_simp]: "list_size f xs = (if xs = [] then 0 else Suc (f (hd xs) + list_size f (tl xs)))" @@ -244,11 +247,11 @@ setup {* Nitpick_Isar.setup *} hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim - bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum' - fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac - one_frac num denom norm_frac frac plus_frac times_frac uminus_frac - number_of_frac inverse_frac less_eq_frac of_frac -hide (open) type bisim_iterator pair_box fun_box + bisim_iterator_max Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec' + wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac + Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac + times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac +hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Dec 18 12:00:44 2009 +0100 @@ -876,7 +876,7 @@ by auto lemma "I = (\x\'a set. x) \ uminus = (\x. uminus (I x))" -nitpick [expect = none] +nitpick [card = 1\7, expect = none] by auto lemma "A \ - A = UNIV" @@ -892,7 +892,7 @@ oops lemma "I = (\x. x) \ finite = (\x. finite (I x))" -nitpick [expect = none] +nitpick [card = 1\7, expect = none] oops lemma "finite A" diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Nitpick_Examples/Datatype_Nits.thy --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Dec 18 12:00:44 2009 +0100 @@ -14,21 +14,11 @@ nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s] primrec rot where -"rot Nibble0 = Nibble1" | -"rot Nibble1 = Nibble2" | -"rot Nibble2 = Nibble3" | -"rot Nibble3 = Nibble4" | -"rot Nibble4 = Nibble5" | -"rot Nibble5 = Nibble6" | -"rot Nibble6 = Nibble7" | -"rot Nibble7 = Nibble8" | -"rot Nibble8 = Nibble9" | -"rot Nibble9 = NibbleA" | -"rot NibbleA = NibbleB" | -"rot NibbleB = NibbleC" | -"rot NibbleC = NibbleD" | -"rot NibbleD = NibbleE" | -"rot NibbleE = NibbleF" | +"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" | +"rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" | +"rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" | +"rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" | +"rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" | "rot NibbleF = Nibble0" lemma "rot n \ n" diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Nitpick_Examples/Integer_Nits.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Fri Dec 18 12:00:44 2009 +0100 @@ -0,0 +1,209 @@ +(* Title: HOL/Nitpick_Examples/Integer_Nits.thy + Author: Jasmin Blanchette, TU Muenchen + Copyright 2009 + +Examples featuring Nitpick applied to natural numbers and integers. +*) + +header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *} + +theory Integer_Nits +imports Nitpick +begin + +nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s, + card = 1\6, bits = 1,2,3,4,6,8] + +lemma "Suc x = x + 1" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x < Suc x" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x + y \ (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y \ 0 \ x + y > (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x + y = y + (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x > y \ x - y \ (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x \ y \ x - y = (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x - (0::nat) = x" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "0 * y = (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y * 0 = (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (y::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x * y div y = (x::nat)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "y \ 0 \ x * y div y = (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "5 * 55 < (260::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +nitpick [binary_ints, bits = 9, expect = genuine] +oops + +lemma "nat (of_nat n) = n" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x + y \ (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "\x \ 0; y \ 0\ \ x + y \ (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y \ 0 \ x + y \ (x::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x \ 0 \ x + y \ (y::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x \ 0 \ x + y \ (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "\x \ 0; y \ 0\ \ x + y \ (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y \ 0 \ x + y > (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "x + y = y + (x::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x > y \ x - y \ (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x \ y \ x - y = (0::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "x - (0::int) = x" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "0 * y = (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y * 0 = (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "\x \ 0; y \ 0\ \ x * y \ (y::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "x * y div y = (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "y \ 0 \ x * y div y = (x::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none, card = 1\5, bits = 1\5] +sorry + +lemma "(x * y < 0) \ (x > 0 \ y < 0) \ (x < 0 \ y > (0::int))" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "-5 * 55 > (-260::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +nitpick [binary_ints, bits = 9, expect = genuine] +oops + +lemma "nat (of_nat n) = n" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +end diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Dec 18 12:00:44 2009 +0100 @@ -59,7 +59,7 @@ nitpick oops -subsection {* 3.5. Numbers *} +subsection {* 3.5. Natural Numbers and Integers *} lemma "\i \ j; n \ (m\int)\ \ i * n + j * m \ i * m + j * n" nitpick @@ -121,11 +121,11 @@ "even n \ even (Suc (Suc n))" lemma "\n. even n \ even (Suc n)" -nitpick [card nat = 100, verbose] +nitpick [card nat = 100, unary_ints, verbose] oops lemma "\n \ 99. even n \ even (Suc n)" -nitpick [card nat = 100] +nitpick [card nat = 100, unary_ints, verbose] oops inductive even' where @@ -134,7 +134,7 @@ "\even' m; even' n\ \ even' (m + n)" lemma "\n \ {0, 2, 4, 6, 8}. \ even' n" -nitpick [card nat = 10, verbose, show_consts] +nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *) oops lemma "even' (n - 2) \ even' n" diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Dec 18 12:00:44 2009 +0100 @@ -18,16 +18,16 @@ val def_table = Nitpick_HOL.const_def_table @{context} defs val ext_ctxt : Nitpick_HOL.extended_context = {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], - user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false, - specialize = false, skolemize = false, star_linear_preds = false, - uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [], - case_names = [], def_table = def_table, nondef_table = Symtab.empty, - user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty, - psimp_table = Symtab.empty, intro_table = Symtab.empty, - ground_thm_table = Inttab.empty, ersatz_table = [], - skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], - unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], - constr_cache = Unsynchronized.ref []} + user_axioms = NONE, debug = false, wfs = [], binary_ints = SOME false, + destroy_constrs = false, specialize = false, skolemize = false, + star_linear_preds = false, uncurry = false, fast_descrs = false, + tac_timeout = NONE, evals = [], case_names = [], def_table = def_table, + nondef_table = Symtab.empty, user_nondefs = [], + simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty, + intro_table = Symtab.empty, ground_thm_table = Inttab.empty, + ersatz_table = [], skolems = Unsynchronized.ref [], + special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [], + wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} (* term -> bool *) val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] [] fun is_const t = diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Nitpick_Examples/Nitpick_Examples.thy --- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Fri Dec 18 12:00:44 2009 +0100 @@ -6,9 +6,8 @@ *) theory Nitpick_Examples -imports Core_Nits Datatype_Nits Induct_Nits Manual_Nits Mini_Nits Mono_Nits - Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits +imports Core_Nits Datatype_Nits Induct_Nits Integer_Nits Manual_Nits Mini_Nits + Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits Typedef_Nits begin - end diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Nitpick_Examples/Special_Nits.thy --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Fri Dec 18 12:00:44 2009 +0100 @@ -163,7 +163,7 @@ else h b\<^isub>2 + h b\<^isub>3 + h b\<^isub>4 + h b\<^isub>5 + h b\<^isub>6 + h b\<^isub>7 + h b\<^isub>8 + h b\<^isub>9 + h b\<^isub>10) x" -nitpick [card nat = 2, card 'a = 1, expect = none] +nitpick [card nat = 2, card 'a = 1, expect = potential] nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential] nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential] nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize, diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Dec 18 12:00:44 2009 +0100 @@ -11,7 +11,7 @@ imports Main Rational begin -nitpick_params [card = 1\4, timeout = 5 s] +nitpick_params [card = 1\4, timeout = 30 s] typedef three = "{0\nat, 1, 2}" by blast @@ -67,7 +67,7 @@ sorry lemma "x \ (y\(bool \ bool) bounded) \ z = x \ z = y" -nitpick [card = 1\5, timeout = 10 s, expect = genuine] +nitpick [card = 1\5, expect = genuine] oops lemma "True \ ((\x\bool. x) = (\x. x))" @@ -157,15 +157,15 @@ by (rule Rep_Nat_inverse) lemma "0 \ Abs_Integ (intrel `` {(0, 0)})" -nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none] +nitpick [card = 1, unary_ints, max_potential = 0, expect = none] by (rule Zero_int_def_raw) lemma "Abs_Integ (Rep_Integ a) = a" -nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none] +nitpick [card = 1, unary_ints, max_potential = 0, expect = none] by (rule Rep_Integ_inverse) lemma "Abs_list (Rep_list a) = a" -nitpick [card = 1\2, timeout = 60 s, expect = none] +nitpick [card = 1\2, expect = none] by (rule Rep_list_inverse) record point = diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Refute.thy --- a/src/HOL/Refute.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Refute.thy Fri Dec 18 12:00:44 2009 +0100 @@ -61,7 +61,8 @@ (* ------------------------------------------------------------------------- *) (* PARAMETERS *) (* *) -(* The following global parameters are currently supported (and required): *) +(* The following global parameters are currently supported (and required, *) +(* except for "expect"): *) (* *) (* Name Type Description *) (* *) @@ -75,6 +76,10 @@ (* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) (* This value is ignored under some ML compilers. *) (* "satsolver" string Name of the SAT solver to be used. *) +(* "no_assms" bool If "true", assumptions in structured proofs are *) +(* not considered. *) +(* "expect" string Expected result ("genuine", "potential", "none", or *) +(* "unknown"). *) (* *) (* See 'HOL/SAT.thy' for default values. *) (* *) diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/SAT.thy --- a/src/HOL/SAT.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/SAT.thy Fri Dec 18 12:00:44 2009 +0100 @@ -23,7 +23,8 @@ maxsize=8, maxvars=10000, maxtime=60, - satsolver="auto"] + satsolver="auto", + no_assms="false"] ML {* structure sat = SATFunc(cnf) *} diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Fri Dec 18 12:00:44 2009 +0100 @@ -1,5 +1,6 @@ Version 2010 + * Added and implemented "binary_ints" and "bits" options * Fixed soundness bug in "destroy_constrs" optimization Version 2009-1 diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Fri Dec 18 12:00:44 2009 +0100 @@ -506,12 +506,13 @@ = filter (is_relevant_setting o fst) (#settings p2) (* int -> string *) -fun base_name j = if j < 0 then Int.toString (~j - 1) ^ "'" else Int.toString j +fun base_name j = + if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j (* n_ary_index -> string -> string -> string -> string *) fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j | n_ary_name (2, j) _ prefix _ = prefix ^ base_name j - | n_ary_name (n, j) _ _ prefix = prefix ^ Int.toString n ^ "_" ^ base_name j + | n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j (* int -> string *) fun atom_name j = "A" ^ base_name j @@ -574,7 +575,7 @@ sub ts1 prec ^ " - " ^ sub ts1 (prec + 1) | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts1 prec | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec - | TupleProject (ts, c) => sub ts prec ^ "[" ^ Int.toString c ^ "]" + | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]" | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}" | TupleRange (t1, t2) => "{" ^ string_for_tuple t1 ^ @@ -602,7 +603,7 @@ (* int_bound -> string *) fun int_string_for_bound (opt_n, tss) = (case opt_n of - SOME n => Int.toString n ^ ": " + SOME n => signed_string_of_int n ^ ": " | NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]" val prec_All = 1 @@ -823,7 +824,7 @@ | Neg i => (out "-"; out_i i prec) | Absolute i => (out "abs "; out_i i prec) | Signum i => (out "sgn "; out_i i prec) - | Num k => out (Int.toString k) + | Num k => out (signed_string_of_int k) | IntReg j => out (int_reg_name j)); (if need_parens then out ")" else ()) end @@ -996,7 +997,7 @@ (* bool -> Time.time option -> int -> int -> problem list -> outcome *) fun solve_any_problem overlord deadline max_threads max_solutions problems = let - val j = find_index (equal True o #formula) problems + val j = find_index (curry (op =) True o #formula) problems val indexed_problems = if j >= 0 then [(j, nth problems j)] else @@ -1048,12 +1049,12 @@ \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ \$LD_LIBRARY_PATH\" \ \\"$KODKODI\"/bin/kodkodi" ^ - (if ms >= 0 then " -max-msecs " ^ Int.toString ms + (if ms >= 0 then " -max-msecs " ^ string_of_int ms else "") ^ (if max_solutions > 1 then " -solve-all" else "") ^ - " -max-solutions " ^ Int.toString max_solutions ^ + " -max-solutions " ^ string_of_int max_solutions ^ (if max_threads > 0 then - " -max-threads " ^ Int.toString max_threads + " -max-threads " ^ string_of_int max_threads else "") ^ " < " ^ Path.implode in_path ^ diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/minipick.ML Fri Dec 18 12:00:44 2009 +0100 @@ -232,7 +232,7 @@ | Const (@{const_name snd}, _) => raise SAME () | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t) | Free (x as (_, T)) => - Rel (arity_of RRep card T, find_index (equal x) frees) + Rel (arity_of RRep card T, find_index (curry (op =) x) frees) | Term.Var _ => raise NOT_SUPPORTED "schematic variables" | Bound j => raise SAME () | Abs (_, T, t') => @@ -314,7 +314,8 @@ bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula} in case solve_any_problem overlord NONE 0 1 [problem] of - Normal ([], _) => "none" + NotInstalled => "unknown" + | Normal ([], _) => "none" | Normal _ => "genuine" | TimedOut _ => "unknown" | Interrupted _ => "unknown" diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Dec 18 12:00:44 2009 +0100 @@ -12,6 +12,7 @@ cards_assigns: (typ option * int list) list, maxes_assigns: (styp option * int list) list, iters_assigns: (styp option * int list) list, + bitss: int list, bisim_depths: int list, boxes: (typ option * bool option) list, monos: (typ option * bool option) list, @@ -25,6 +26,7 @@ user_axioms: bool option, assms: bool, merge_type_vars: bool, + binary_ints: bool option, destroy_constrs: bool, specialize: bool, skolemize: bool, @@ -73,10 +75,13 @@ open Nitpick_Kodkod open Nitpick_Model +structure KK = Kodkod + type params = { cards_assigns: (typ option * int list) list, maxes_assigns: (styp option * int list) list, iters_assigns: (styp option * int list) list, + bitss: int list, bisim_depths: int list, boxes: (typ option * bool option) list, monos: (typ option * bool option) list, @@ -90,6 +95,7 @@ user_axioms: bool option, assms: bool, merge_type_vars: bool, + binary_ints: bool option, destroy_constrs: bool, specialize: bool, skolemize: bool, @@ -122,10 +128,10 @@ rel_table: nut NameTable.table, liberal: bool, scope: scope, - core: Kodkod.formula, - defs: Kodkod.formula list} + core: KK.formula, + defs: KK.formula list} -type rich_problem = Kodkod.problem * problem_extension +type rich_problem = KK.problem * problem_extension (* Proof.context -> string -> term list -> Pretty.T list *) fun pretties_for_formulas _ _ [] = [] @@ -133,7 +139,7 @@ [Pretty.str (s ^ plural_s_for_list ts ^ ":"), Pretty.indent indent_size (Pretty.chunks (map2 (fn j => fn t => - Pretty.block [t |> shorten_const_names_in_term + Pretty.block [t |> shorten_names_in_term |> Syntax.pretty_term ctxt, Pretty.str (if j = 1 then "." else ";")]) (length ts downto 1) ts))] @@ -162,7 +168,7 @@ | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS (* ('a * bool option) list -> bool *) -fun none_true asgns = forall (not_equal (SOME true) o snd) asgns +fun none_true assigns = forall (not_equal (SOME true) o snd) assigns val syntactic_sorts = @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @ @@ -186,20 +192,21 @@ val nitpick_thy = ThyInfo.get_theory "Nitpick" val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy)) val thy = if nitpick_thy_missing then - Theory.begin_theory "Nitpick_Internal" [nitpick_thy, user_thy] + Theory.begin_theory "Nitpick_Internal_Name_Do_Not_Use_XYZZY" + [nitpick_thy, user_thy] |> Theory.checkpoint else user_thy val ctxt = Proof.context_of state |> nitpick_thy_missing ? Context.raw_transfer thy - val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes, - monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord, - user_axioms, assms, merge_type_vars, destroy_constrs, specialize, - skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim, - tac_timeout, sym_break, sharing_depth, flatten_props, max_threads, - show_skolems, show_datatypes, show_consts, evals, formats, - max_potential, max_genuine, check_potential, check_genuine, batch_size, - ...} = + val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, + boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose, + overlord, user_axioms, assms, merge_type_vars, binary_ints, + destroy_constrs, specialize, skolemize, star_linear_preds, uncurry, + fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth, + flatten_props, max_threads, show_skolems, show_datatypes, show_consts, + evals, formats, max_potential, max_genuine, check_potential, + check_genuine, batch_size, ...} = params val state_ref = Unsynchronized.ref state (* Pretty.T -> unit *) @@ -260,10 +267,11 @@ val (ext_ctxt as {wf_cache, ...}) = {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, user_axioms = user_axioms, debug = debug, wfs = wfs, - destroy_constrs = destroy_constrs, specialize = specialize, - skolemize = skolemize, star_linear_preds = star_linear_preds, - uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout, - evals = evals, case_names = case_names, def_table = def_table, + binary_ints = binary_ints, destroy_constrs = destroy_constrs, + specialize = specialize, skolemize = skolemize, + star_linear_preds = star_linear_preds, uncurry = uncurry, + fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, + case_names = case_names, def_table = def_table, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_table, intro_table = intro_table, ground_thm_table = ground_thm_table, @@ -315,25 +323,33 @@ (core_u :: def_us @ nondef_us) *) - val unique_scope = forall (equal 1 o length o snd) cards_assigns + val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns (* typ -> bool *) fun is_free_type_monotonic T = unique_scope orelse case triple_lookup (type_match thy) monos T of SOME (SOME b) => b - | _ => formulas_monotonic ext_ctxt T def_ts nondef_ts core_t + | _ => is_bit_type T + orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t fun is_datatype_monotonic T = unique_scope orelse case triple_lookup (type_match thy) monos T of SOME (SOME b) => b - | _ => - not (is_pure_typedef thy T) orelse is_univ_typedef thy T - orelse is_number_type thy T - orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t - fun is_datatype_shallow T = - not (exists (equal T o domain_type o type_of) sel_names) + | _ => not (is_pure_typedef thy T) orelse is_univ_typedef thy T + orelse is_number_type thy T + orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t + fun is_datatype_deep T = + is_word_type T + orelse exists (curry (op =) T o domain_type o type_of) sel_names val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts) |> sort TermOrd.typ_ord + val _ = if verbose andalso binary_ints = SOME true + andalso exists (member (op =) [nat_T, int_T]) Ts then + print_v (K "The option \"binary_ints\" will be ignored because \ + \of the presence of rationals, reals, \"Suc\", \ + \\"gcd\", or \"lcm\" in the problem.") + else + () val (all_dataTs, all_free_Ts) = List.partition (is_integer_type orf is_datatype thy) Ts val (mono_dataTs, nonmono_dataTs) = @@ -341,11 +357,13 @@ val (mono_free_Ts, nonmono_free_Ts) = List.partition is_free_type_monotonic all_free_Ts + val interesting_mono_free_Ts = filter_out is_bit_type mono_free_Ts val _ = - if not unique_scope andalso not (null mono_free_Ts) then + if not unique_scope andalso not (null interesting_mono_free_Ts) then print_v (fn () => let - val ss = map (quote o string_for_type ctxt) mono_free_Ts + val ss = map (quote o string_for_type ctxt) + interesting_mono_free_Ts in "The type" ^ plural_s_for_list ss ^ " " ^ space_implode " " (serial_commas "and" ss) ^ " " ^ @@ -360,7 +378,7 @@ () val mono_Ts = mono_dataTs @ mono_free_Ts val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts - val shallow_dataTs = filter is_datatype_shallow mono_dataTs + val shallow_dataTs = filter_out is_datatype_deep mono_dataTs (* val _ = priority "Monotonic datatypes:" val _ = List.app (priority o string_for_type ctxt) mono_dataTs @@ -375,8 +393,9 @@ val need_incremental = Int.max (max_potential, max_genuine) >= 2 val effective_sat_solver = if sat_solver <> "smart" then - if need_incremental andalso - not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then + if need_incremental + andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true) + sat_solver) then (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ \be used instead of " ^ quote sat_solver ^ ".")); "SAT4J") @@ -399,12 +418,12 @@ (* bool -> scope -> rich_problem option *) fun problem_for_scope liberal - (scope as {card_assigns, bisim_depth, datatypes, ofs, ...}) = + (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) = let val _ = not (exists (fn other => scope_less_eq other scope) (!too_big_scopes)) - orelse raise LIMIT ("Nitpick.pick_them_nits_in_term.\ - \problem_for_scope", "too big scope") + orelse raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\ + \problem_for_scope", "too large scope") (* val _ = priority "Offsets:" val _ = List.app (fn (T, j0) => @@ -412,13 +431,13 @@ string_of_int j0)) (Typtab.dest ofs) *) - val all_precise = forall (is_precise_type datatypes) Ts + val all_exact = forall (is_exact_type datatypes) Ts (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *) - val repify_consts = choose_reps_for_consts scope all_precise + val repify_consts = choose_reps_for_consts scope all_exact val main_j0 = offset_of_type ofs bool_T val (nat_card, nat_j0) = spec_of_type scope nat_T val (int_card, int_j0) = spec_of_type scope int_T - val _ = forall (equal main_j0) [nat_j0, int_j0] + val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse raise BAD ("Nitpick.pick_them_nits_in_term.\ \problem_for_scope", "bad offsets") val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 @@ -430,7 +449,7 @@ NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1 val min_univ_card = NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table - (univ_card nat_card int_card main_j0 [] Kodkod.True) + (univ_card nat_card int_card main_j0 [] KK.True) val _ = check_arity min_univ_card min_highest_arity val core_u = choose_reps_in_nut scope liberal rep_table false core_u @@ -452,8 +471,8 @@ val core_u = rename_vars_in_nut pool rel_table core_u val def_us = map (rename_vars_in_nut pool rel_table) def_us val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us - (* nut -> Kodkod.formula *) - val to_f = kodkod_formula_from_nut ofs liberal kk + (* nut -> KK.formula *) + val to_f = kodkod_formula_from_nut bits ofs liberal kk val core_f = to_f core_u val def_fs = map to_f def_us val nondef_fs = map to_f nondef_us @@ -462,6 +481,7 @@ PrintMode.setmp [] multiline_string_for_scope scope val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd + val bit_width = if bits = 0 then 16 else bits + 1 val delay = if liberal then Option.map (fn time => Time.- (time, Time.now ())) deadline @@ -470,7 +490,7 @@ 0 val settings = [("solver", commas (map quote kodkod_sat_solver)), ("skolem_depth", "-1"), - ("bit_width", "16"), + ("bit_width", string_of_int bit_width), ("symmetry_breaking", signed_string_of_int sym_break), ("sharing", signed_string_of_int sharing_depth), ("flatten", Bool.toString flatten_props), @@ -479,7 +499,7 @@ val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels - val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt ofs kk + val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table datatypes val declarative_axioms = plain_axioms @ dtype_axioms val univ_card = univ_card nat_card int_card main_j0 @@ -491,40 +511,48 @@ val highest_arity = fold Integer.max (map (fst o fst) (maps fst bounds)) 0 val formula = fold_rev s_and declarative_axioms formula - val _ = if formula = Kodkod.False then () + val _ = if bits = 0 then () else check_bits bits formula + val _ = if formula = KK.False then () else check_arity univ_card highest_arity in SOME ({comment = comment, settings = settings, univ_card = univ_card, tuple_assigns = [], bounds = bounds, - int_bounds = sequential_int_bounds univ_card, + int_bounds = + if bits = 0 then sequential_int_bounds univ_card + else pow_of_two_int_bounds bits main_j0 univ_card, expr_assigns = [], formula = formula}, {free_names = free_names, sel_names = sel_names, nonsel_names = nonsel_names, rel_table = rel_table, liberal = liberal, scope = scope, core = core_f, defs = nondef_fs @ def_fs @ declarative_axioms}) end - handle LIMIT (loc, msg) => - if loc = "Nitpick_Kodkod.check_arity" + handle TOO_LARGE (loc, msg) => + if loc = "Nitpick_KK.check_arity" andalso not (Typtab.is_empty ofs) then problem_for_scope liberal {ext_ctxt = ext_ctxt, card_assigns = card_assigns, - bisim_depth = bisim_depth, datatypes = datatypes, - ofs = Typtab.empty} + bits = bits, bisim_depth = bisim_depth, + datatypes = datatypes, ofs = Typtab.empty} else if loc = "Nitpick.pick_them_nits_in_term.\ \problem_for_scope" then NONE else (Unsynchronized.change too_big_scopes (cons scope); print_v (fn () => ("Limit reached: " ^ msg ^ - ". Dropping " ^ (if liberal then "potential" + ". Skipping " ^ (if liberal then "potential" else "genuine") ^ " component of scope.")); NONE) + | TOO_SMALL (loc, msg) => + (print_v (fn () => ("Limit reached: " ^ msg ^ + ". Skipping " ^ (if liberal then "potential" + else "genuine") ^ + " component of scope.")); + NONE) - (* int -> (''a * int list list) list -> ''a -> Kodkod.tuple_set *) + (* int -> (''a * int list list) list -> ''a -> KK.tuple_set *) fun tuple_set_for_rel univ_card = - Kodkod.TupleSet o map (kk_tuple debug univ_card) o the - oo AList.lookup (op =) + KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =) val word_model = if falsify then "counterexample" else "model" @@ -539,7 +567,7 @@ List.app (Unsynchronized.change checked_problems o Option.map o cons o nth problems) - (* bool -> Kodkod.raw_bound list -> problem_extension -> bool option *) + (* bool -> KK.raw_bound list -> problem_extension -> bool option *) fun print_and_check_model genuine bounds ({free_names, sel_names, nonsel_names, rel_table, scope, ...} : problem_extension) = @@ -636,7 +664,7 @@ let val max_potential = Int.max (0, max_potential) val max_genuine = Int.max (0, max_genuine) - (* bool -> int * Kodkod.raw_bound list -> bool option *) + (* bool -> int * KK.raw_bound list -> bool option *) fun print_and_check genuine (j, bounds) = print_and_check_model genuine bounds (snd (nth problems j)) val max_solutions = max_potential + max_genuine @@ -645,15 +673,15 @@ if max_solutions <= 0 then (0, 0, donno) else - case Kodkod.solve_any_problem overlord deadline max_threads - max_solutions (map fst problems) of - Kodkod.NotInstalled => + case KK.solve_any_problem overlord deadline max_threads max_solutions + (map fst problems) of + KK.NotInstalled => (print_m install_kodkodi_message; (max_potential, max_genuine, donno + 1)) - | Kodkod.Normal ([], unsat_js) => + | KK.Normal ([], unsat_js) => (update_checked_problems problems unsat_js; (max_potential, max_genuine, donno)) - | Kodkod.Normal (sat_ps, unsat_js) => + | KK.Normal (sat_ps, unsat_js) => let val (lib_ps, con_ps) = List.partition (#liberal o snd o nth problems o fst) sat_ps @@ -663,7 +691,8 @@ let val num_genuine = take max_potential lib_ps |> map (print_and_check false) - |> filter (equal (SOME true)) |> length + |> filter (curry (op =) (SOME true)) + |> length val max_genuine = max_genuine - num_genuine val max_potential = max_potential - (length lib_ps - num_genuine) @@ -711,13 +740,12 @@ in solve_any_problem 0 max_genuine donno false problems end end end - | Kodkod.TimedOut unsat_js => + | KK.TimedOut unsat_js => (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) - | Kodkod.Interrupted NONE => - (checked_problems := NONE; do_interrupted ()) - | Kodkod.Interrupted (SOME unsat_js) => + | KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ()) + | KK.Interrupted (SOME unsat_js) => (update_checked_problems problems unsat_js; do_interrupted ()) - | Kodkod.Error (s, unsat_js) => + | KK.Error (s, unsat_js) => (update_checked_problems problems unsat_js; print_v (K ("Kodkod error: " ^ s ^ ".")); (max_potential, max_genuine, donno + 1)) @@ -759,8 +787,8 @@ SOME problem => (problems |> (null problems orelse - not (Kodkod.problems_equivalent (fst problem) - (fst (hd problems)))) + not (KK.problems_equivalent (fst problem) + (fst (hd problems)))) ? cons problem, donno) | NONE => (problems, donno + 1)) val (problems, donno) = @@ -804,10 +832,10 @@ "") ^ "." end - (* int -> int -> scope list -> int * int * int -> Kodkod.outcome *) + (* int -> int -> scope list -> int * int * int -> KK.outcome *) fun run_batches _ _ [] (max_potential, max_genuine, donno) = if donno > 0 andalso max_genuine > 0 then - (print_m (fn () => excipit "ran out of juice"); "unknown") + (print_m (fn () => excipit "ran out of some resource"); "unknown") else if max_genuine = original_max_genuine then if max_potential = original_max_potential then (print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none") @@ -825,9 +853,9 @@ val (skipped, the_scopes) = all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns - bisim_depths mono_Ts nonmono_Ts shallow_dataTs + bitss bisim_depths mono_Ts nonmono_Ts shallow_dataTs val _ = if skipped > 0 then - print_m (fn () => "Too many scopes. Dropping " ^ + print_m (fn () => "Too many scopes. Skipping " ^ string_of_int skipped ^ " scope" ^ plural_s skipped ^ ". (Consider using \"mono\" or \ @@ -859,8 +887,8 @@ error "Nitpick was interrupted." (* Proof.state -> params -> bool -> term -> string * Proof.state *) -fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) - auto orig_assm_ts orig_t = +fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto + orig_assm_ts orig_t = if getenv "KODKODI" = "" then (if auto then () else warning (Pretty.string_of (plazy install_kodkodi_message)); @@ -878,7 +906,7 @@ end (* Proof.state -> params -> thm -> int -> string * Proof.state *) -fun pick_nits_in_subgoal state params auto subgoal = +fun pick_nits_in_subgoal state params auto i = let val ctxt = Proof.context_of state val t = state |> Proof.raw_goal |> #goal |> prop_of @@ -888,7 +916,7 @@ else let val assms = map term_of (Assumption.all_assms_of ctxt) - val (t, frees) = Logic.goal_params t subgoal + val (t, frees) = Logic.goal_params t i in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end end diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Dec 18 12:00:44 2009 +0100 @@ -21,6 +21,7 @@ wfs: (styp option * bool option) list, user_axioms: bool option, debug: bool, + binary_ints: bool option, destroy_constrs: bool, specialize: bool, skolemize: bool, @@ -49,12 +50,12 @@ val skolem_prefix : string val eval_prefix : string val original_name : string -> string - val unbox_type : typ -> typ + val unbit_and_unbox_type : typ -> typ val string_for_type : Proof.context -> typ -> string val prefix_name : string -> string -> string + val shortest_name : string -> string val short_name : string -> string - val short_const_name : string -> string - val shorten_const_names_in_term : term -> term + val shorten_names_in_term : term -> term val type_match : theory -> typ * typ -> bool val const_match : theory -> styp * styp -> bool val term_match : theory -> term * term -> bool @@ -68,6 +69,8 @@ val is_fp_iterator_type : typ -> bool val is_boolean_type : typ -> bool val is_integer_type : typ -> bool + val is_bit_type : typ -> bool + val is_word_type : typ -> bool val is_record_type : typ -> bool val is_number_type : theory -> typ -> bool val const_for_iterator_type : typ -> styp @@ -91,6 +94,7 @@ val is_constr : theory -> styp -> bool val is_stale_constr : theory -> styp -> bool val is_sel : string -> bool + val is_sel_like_and_no_discr : string -> bool val discr_for_constr : styp -> styp val num_sels_for_constr_type : typ -> int val nth_sel_name_for_constr_name : string -> int -> string @@ -111,7 +115,7 @@ val boxed_constr_for_sel : extended_context -> styp -> styp val card_of_type : (typ * int) list -> typ -> int val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int - val bounded_precise_card_of_type : + val bounded_exact_card_of_type : extended_context -> int -> int -> (typ * int) list -> typ -> int val is_finite_type : extended_context -> typ -> bool val all_axioms_of : theory -> term list * term list * term list @@ -161,6 +165,7 @@ wfs: (styp option * bool option) list, user_axioms: bool option, debug: bool, + binary_ints: bool option, destroy_constrs: bool, specialize: bool, skolemize: bool, @@ -197,12 +202,14 @@ (* term * term -> term *) fun s_conj (t1, @{const True}) = t1 | s_conj (@{const True}, t2) = t2 - | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False} - else HOLogic.mk_conj (t1, t2) + | s_conj (t1, t2) = + if t1 = @{const False} orelse t2 = @{const False} then @{const False} + else HOLogic.mk_conj (t1, t2) fun s_disj (t1, @{const False}) = t1 | s_disj (@{const False}, t2) = t2 - | s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True} - else HOLogic.mk_disj (t1, t2) + | s_disj (t1, t2) = + if t1 = @{const True} orelse t2 = @{const True} then @{const True} + else HOLogic.mk_disj (t1, t2) (* term -> term -> term *) fun mk_exists v t = HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t) @@ -213,7 +220,7 @@ | strip_connective _ t = [t] (* term -> term list * term *) fun strip_any_connective (t as (t0 $ t1 $ t2)) = - if t0 mem [@{const "op &"}, @{const "op |"}] then + if t0 = @{const "op &"} orelse t0 = @{const "op |"} then (strip_connective t0 t, t0) else ([t], @{const Not}) @@ -305,7 +312,6 @@ (@{const_name minus_nat_inst.minus_nat}, 0), (@{const_name times_nat_inst.times_nat}, 0), (@{const_name div_nat_inst.div_nat}, 0), - (@{const_name div_nat_inst.mod_nat}, 0), (@{const_name ord_nat_inst.less_nat}, 2), (@{const_name ord_nat_inst.less_eq_nat}, 2), (@{const_name nat_gcd}, 0), @@ -316,7 +322,6 @@ (@{const_name minus_int_inst.minus_int}, 0), (@{const_name times_int_inst.times_int}, 0), (@{const_name div_int_inst.div_int}, 0), - (@{const_name div_int_inst.mod_int}, 0), (@{const_name uminus_int_inst.uminus_int}, 0), (@{const_name ord_int_inst.less_int}, 2), (@{const_name ord_int_inst.less_eq_int}, 2), @@ -327,7 +332,8 @@ [(@{const_name The}, 1), (@{const_name Eps}, 1)] val built_in_typed_consts = - [((@{const_name of_nat}, nat_T --> int_T), 0)] + [((@{const_name of_nat}, nat_T --> int_T), 0), + ((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)] val built_in_set_consts = [(@{const_name lower_semilattice_fun_inst.inf_fun}, 2), (@{const_name upper_semilattice_fun_inst.sup_fun}, 2), @@ -335,31 +341,45 @@ (@{const_name ord_fun_inst.less_eq_fun}, 2)] (* typ -> typ *) -fun unbox_type (Type (@{type_name fun_box}, Ts)) = - Type ("fun", map unbox_type Ts) - | unbox_type (Type (@{type_name pair_box}, Ts)) = - Type ("*", map unbox_type Ts) - | unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts) - | unbox_type T = T +fun unbit_type @{typ "unsigned_bit word"} = nat_T + | unbit_type @{typ "signed_bit word"} = int_T + | unbit_type @{typ bisim_iterator} = nat_T + | unbit_type (Type (s, Ts as _ :: _)) = Type (s, map unbit_type Ts) + | unbit_type T = T +fun unbit_and_unbox_type (Type (@{type_name fun_box}, Ts)) = + unbit_and_unbox_type (Type ("fun", Ts)) + | unbit_and_unbox_type (Type (@{type_name pair_box}, Ts)) = + Type ("*", map unbit_and_unbox_type Ts) + | unbit_and_unbox_type @{typ "unsigned_bit word"} = nat_T + | unbit_and_unbox_type @{typ "signed_bit word"} = int_T + | unbit_and_unbox_type @{typ bisim_iterator} = nat_T + | unbit_and_unbox_type (Type (s, Ts as _ :: _)) = + Type (s, map unbit_and_unbox_type Ts) + | unbit_and_unbox_type T = T (* Proof.context -> typ -> string *) -fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type +fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type (* string -> string -> string *) val prefix_name = Long_Name.qualify o Long_Name.base_name (* string -> string *) -fun short_name s = List.last (space_explode "." s) handle List.Empty => "" +fun shortest_name s = List.last (space_explode "." s) handle List.Empty => "" (* string -> term -> term *) val prefix_abs_vars = Term.map_abs_vars o prefix_name (* term -> term *) -val shorten_abs_vars = Term.map_abs_vars short_name +val shorten_abs_vars = Term.map_abs_vars shortest_name (* string -> string *) -fun short_const_name s = +fun short_name s = case space_explode name_sep s of [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix - | ss => map short_name ss |> space_implode "_" + | ss => map shortest_name ss |> space_implode "_" +(* typ -> typ *) +fun shorten_names_in_type (Type (s, Ts)) = + Type (short_name s, map shorten_names_in_type Ts) + | shorten_names_in_type T = T (* term -> term *) -val shorten_const_names_in_term = - map_aterms (fn Const (s, T) => Const (short_const_name s, T) | t => t) +val shorten_names_in_term = + map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t) + #> map_types shorten_names_in_type (* theory -> typ * typ -> bool *) fun type_match thy (T1, T2) = @@ -371,7 +391,7 @@ (* theory -> term * term -> bool *) fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2) | term_match thy (Free (s1, T1), Free (s2, T2)) = - const_match thy ((short_name s1, T1), (short_name s2, T2)) + const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) | term_match thy (t1, t2) = t1 aconv t2 (* typ -> bool *) @@ -391,9 +411,12 @@ fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s | is_gfp_iterator_type _ = false val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type -val is_boolean_type = equal prop_T orf equal bool_T +fun is_boolean_type T = (T = prop_T orelse T = bool_T) val is_integer_type = member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type +fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit}) +fun is_word_type (Type (@{type_name word}, _)) = true + | is_word_type _ = false val is_record_type = not o null o Record.dest_recTs (* theory -> typ -> bool *) fun is_frac_type thy (Type (s, [])) = @@ -447,16 +470,13 @@ | dest_n_tuple_type _ T = raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) -(* (typ * typ) list -> typ -> typ *) -fun typ_subst [] T = T - | typ_subst ps T = - let - (* typ -> typ *) - fun subst T = - case AList.lookup (op =) ps T of - SOME T' => T' - | NONE => case T of Type (s, Ts) => Type (s, map subst Ts) | _ => T - in subst T end +(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype", + e.g., by adding a field to "Datatype_Aux.info". *) +(* string -> bool *) +val is_basic_datatype = + member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit}, + @{type_name nat}, @{type_name int}, + "Code_Numeral.code_numeral"] (* theory -> typ -> typ -> typ -> typ *) fun instantiate_type thy T1 T1' T2 = @@ -486,8 +506,11 @@ val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs val (co_s, co_Ts) = dest_Type co_T val _ = - if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then () - else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) + if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) + andalso co_s <> "fun" andalso not (is_basic_datatype co_s) then + () + else + raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) codatatypes in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end @@ -516,12 +539,6 @@ Rep_inverse = SOME Rep_inverse} | NONE => NONE -(* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype", - e.g., by adding a field to "Datatype_Aux.info". *) -(* string -> bool *) -fun is_basic_datatype s = - s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit}, - @{type_name nat}, @{type_name int}, "Code_Numeral.code_numeral"] (* theory -> string -> bool *) val is_typedef = is_some oo typedef_info val is_real_datatype = is_some oo Datatype.get_info @@ -568,14 +585,15 @@ val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields (* theory -> string -> typ -> int *) fun no_of_record_field thy s T1 = - find_index (equal s o fst) (Record.get_extT_fields thy T1 ||> single |> op @) + find_index (curry (op =) s o fst) + (Record.get_extT_fields thy T1 ||> single |> op @) (* theory -> styp -> bool *) fun is_record_get thy (s, Type ("fun", [T1, _])) = - exists (equal s o fst) (all_record_fields thy T1) + exists (curry (op =) s o fst) (all_record_fields thy T1) | is_record_get _ _ = false fun is_record_update thy (s, T) = String.isSuffix Record.updateN s andalso - exists (equal (unsuffix Record.updateN s) o fst) + exists (curry (op =) (unsuffix Record.updateN s) o fst) (all_record_fields thy (body_type T)) handle TYPE _ => false fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) = @@ -608,11 +626,11 @@ end handle TYPE ("dest_Type", _, _) => false fun is_constr_like thy (s, T) = - s mem [@{const_name FunBox}, @{const_name PairBox}] orelse - let val (x as (s, T)) = (s, unbox_type T) in + s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse + let val (x as (s, T)) = (s, unbit_and_unbox_type T) in Refute.is_IDT_constructor thy x orelse is_record_constr x orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) - orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}] + orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse is_coconstr thy x end @@ -621,7 +639,7 @@ andalso not (is_coconstr thy x) fun is_constr thy (x as (_, T)) = is_constr_like thy x - andalso not (is_basic_datatype (fst (dest_Type (body_type T)))) + andalso not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso not (is_stale_constr thy x) (* string -> bool *) val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix @@ -644,10 +662,11 @@ fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = case T of Type ("fun", _) => - boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T)) + (boxy = InPair orelse boxy = InFunLHS) + andalso not (is_boolean_type (body_type T)) | Type ("*", Ts) => - boxy mem [InPair, InFunRHS1, InFunRHS2] - orelse (boxy mem [InExpr, InFunLHS] + boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 + orelse ((boxy = InExpr orelse boxy = InFunLHS) andalso exists (is_boxing_worth_it ext_ctxt InPair) (map (box_type ext_ctxt InPair) Ts)) | _ => false @@ -660,7 +679,7 @@ and box_type ext_ctxt boxy T = case T of Type (z as ("fun", [T1, T2])) => - if not (boxy mem [InConstr, InSel]) + if boxy <> InConstr andalso boxy <> InSel andalso should_box_type ext_ctxt boxy z then Type (@{type_name fun_box}, [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2]) @@ -672,8 +691,8 @@ Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts) else Type ("*", map (box_type ext_ctxt - (if boxy mem [InConstr, InSel] then boxy - else InPair)) Ts) + (if boxy = InConstr orelse boxy = InSel then boxy + else InPair)) Ts) | _ => T (* styp -> styp *) @@ -872,7 +891,7 @@ val x' as (_, T') = if is_pair_type T then let val (T1, T2) = HOLogic.dest_prodT T in - (@{const_name Pair}, [T1, T2] ---> T) + (@{const_name Pair}, T1 --> T2 --> T) end else datatype_constrs ext_ctxt T |> the_single @@ -883,46 +902,46 @@ end (* (typ * int) list -> typ -> int *) -fun card_of_type asgns (Type ("fun", [T1, T2])) = - reasonable_power (card_of_type asgns T2) (card_of_type asgns T1) - | card_of_type asgns (Type ("*", [T1, T2])) = - card_of_type asgns T1 * card_of_type asgns T2 +fun card_of_type assigns (Type ("fun", [T1, T2])) = + reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) + | card_of_type assigns (Type ("*", [T1, T2])) = + card_of_type assigns T1 * card_of_type assigns T2 | card_of_type _ (Type (@{type_name itself}, _)) = 1 | card_of_type _ @{typ prop} = 2 | card_of_type _ @{typ bool} = 2 | card_of_type _ @{typ unit} = 1 - | card_of_type asgns T = - case AList.lookup (op =) asgns T of + | card_of_type assigns T = + case AList.lookup (op =) assigns T of SOME k => k | NONE => if T = @{typ bisim_iterator} then 0 else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) (* int -> (typ * int) list -> typ -> int *) -fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) = +fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) = let - val k1 = bounded_card_of_type max default_card asgns T1 - val k2 = bounded_card_of_type max default_card asgns T2 + val k1 = bounded_card_of_type max default_card assigns T1 + val k2 = bounded_card_of_type max default_card assigns T2 in if k1 = max orelse k2 = max then max else Int.min (max, reasonable_power k2 k1) end - | bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) = + | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) = let - val k1 = bounded_card_of_type max default_card asgns T1 - val k2 = bounded_card_of_type max default_card asgns T2 + val k1 = bounded_card_of_type max default_card assigns T1 + val k2 = bounded_card_of_type max default_card assigns T2 in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end - | bounded_card_of_type max default_card asgns T = + | bounded_card_of_type max default_card assigns T = Int.min (max, if default_card = ~1 then - card_of_type asgns T + card_of_type assigns T else - card_of_type asgns T + card_of_type assigns T handle TYPE ("Nitpick_HOL.card_of_type", _, _) => default_card) (* extended_context -> int -> (typ * int) list -> typ -> int *) -fun bounded_precise_card_of_type ext_ctxt max default_card asgns T = +fun bounded_exact_card_of_type ext_ctxt max default_card assigns T = let (* typ list -> typ -> int *) fun aux avoid T = - (if T mem avoid then + (if member (op =) avoid T then 0 else case T of Type ("fun", [T1, T2]) => @@ -949,7 +968,8 @@ | @{typ unit} => 1 | Type _ => (case datatype_constrs ext_ctxt T of - [] => if is_integer_type T then 0 else raise SAME () + [] => if is_integer_type T orelse is_bit_type T then 0 + else raise SAME () | constrs => let val constr_cards = @@ -957,16 +977,17 @@ |> map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd) in - if exists (equal 0) constr_cards then 0 + if exists (curry (op =) 0) constr_cards then 0 else Integer.sum constr_cards end) | _ => raise SAME ()) - handle SAME () => AList.lookup (op =) asgns T |> the_default default_card + handle SAME () => + AList.lookup (op =) assigns T |> the_default default_card in Int.min (max, aux [] T) end (* extended_context -> typ -> bool *) fun is_finite_type ext_ctxt = - not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 [] + not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 [] (* term -> bool *) fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 @@ -989,8 +1010,8 @@ (* theory -> string -> bool *) fun is_funky_typedef_name thy s = - s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, - @{type_name int}] + member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, + @{type_name int}] s orelse is_frac_type thy (Type (s, [])) (* theory -> term -> bool *) fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s @@ -1063,10 +1084,11 @@ val (built_in_nondefs, user_nondefs) = List.partition (is_typedef_axiom thy false) user_nondefs |>> append built_in_nondefs - val defs = (thy |> PureThy.all_thms_of - |> filter (equal Thm.definitionK o Thm.get_kind o snd) - |> map (prop_of o snd) |> filter is_plain_definition) @ - user_defs @ built_in_defs + val defs = + (thy |> PureThy.all_thms_of + |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd) + |> map (prop_of o snd) |> filter is_plain_definition) @ + user_defs @ built_in_defs in (defs, built_in_nondefs, user_nondefs) end (* bool -> styp -> int option *) @@ -1111,7 +1133,7 @@ else these (Symtab.lookup table s) |> map_filter (try (Refute.specialize_type thy x)) - |> filter (equal (Const x) o term_under_def) + |> filter (curry (op =) (Const x) o term_under_def) (* theory -> term -> term option *) fun normalized_rhs_of thy t = @@ -1152,7 +1174,8 @@ (* term -> bool *) fun is_good_arg (Bound _) = true | is_good_arg (Const (s, _)) = - s mem [@{const_name True}, @{const_name False}, @{const_name undefined}] + s = @{const_name True} orelse s = @{const_name False} + orelse s = @{const_name undefined} | is_good_arg _ = false in case t |> strip_abs_body |> strip_comb of @@ -1307,7 +1330,7 @@ end (* extended_context -> typ -> int * styp -> term -> term *) fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t = - Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T) + Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T) $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x) $ res_t (* extended_context -> typ -> typ -> term *) @@ -1538,10 +1561,10 @@ else case def_of_const thy def_table x of SOME def => if depth > unfold_max_depth then - raise LIMIT ("Nitpick_HOL.unfold_defs_in_term", - "too many nested definitions (" ^ - string_of_int depth ^ ") while expanding " ^ - quote s) + raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term", + "too many nested definitions (" ^ + string_of_int depth ^ ") while expanding " ^ + quote s) else if s = @{const_name wfrec'} then (do_term (depth + 1) Ts (betapplys (def, ts)), []) else @@ -1556,7 +1579,7 @@ val xs = datatype_constrs ext_ctxt T val set_T = T --> bool_T val iter_T = @{typ bisim_iterator} - val bisim_const = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T) + val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T) val bisim_max = @{const bisim_iterator_max} val n_var = Var (("n", 0), iter_T) val n_var_minus_1 = @@ -1586,7 +1609,7 @@ $ (betapplys (optimized_case_def ext_ctxt T bool_T, map case_func xs @ [x_var]))), HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var) - $ (Const (@{const_name insert}, [T, set_T] ---> set_T) + $ (Const (@{const_name insert}, T --> set_T --> set_T) $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))] |> map HOLogic.mk_Trueprop end @@ -1598,9 +1621,9 @@ let val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy) val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy - val (main, side) = List.partition (exists_Const (equal x)) prems + val (main, side) = List.partition (exists_Const (curry (op =) x)) prems (* term -> bool *) - val is_good_head = equal (Const x) o head_of + val is_good_head = curry (op =) (Const x) o head_of in if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE () end @@ -1693,7 +1716,7 @@ (x as (s, _)) = case triple_lookup (const_match thy) wfs x of SOME (SOME b) => b - | _ => s mem [@{const_name Nats}, @{const_name fold_graph'}] + | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse case AList.lookup (op =) (!wf_cache) x of SOME (_, wf) => wf | NONE => @@ -1730,7 +1753,7 @@ | do_disjunct j t = case num_occs_of_bound_in_term j t of 0 => true - | 1 => exists (equal (Bound j) o head_of) (conjuncts t) + | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t) | _ => false (* term -> bool *) fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) = @@ -1774,7 +1797,7 @@ t end val (nonrecs, recs) = - List.partition (equal 0 o num_occs_of_bound_in_term j) + List.partition (curry (op =) 0 o num_occs_of_bound_in_term j) (disjuncts body) val base_body = nonrecs |> List.foldl s_disj @{const False} val step_body = recs |> map (repair_rec j) @@ -1923,7 +1946,7 @@ | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum | Type (_, Ts) => - if T mem @{typ prop} :: @{typ bool} :: @{typ unit} :: accum then + if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then accum else T :: accum @@ -1962,7 +1985,7 @@ andalso has_heavy_bounds_or_vars Ts level t_comb andalso not (loose_bvar (t_comb, level)) then let - val (j, seen) = case find_index (equal t_comb) seen of + val (j, seen) = case find_index (curry (op =) t_comb) seen of ~1 => (0, t_comb :: seen) | j => (j, seen) in (fresh_value_var Ts k (length seen) j t_comb, seen) end @@ -2046,8 +2069,8 @@ (Const (x as (s, T)), args) => let val arg_Ts = binder_types T in if length arg_Ts = length args - andalso (is_constr thy x orelse s mem [@{const_name Pair}] - orelse x = dest_Const @{const Suc}) + andalso (is_constr thy x orelse s = @{const_name Pair} + orelse x = (@{const_name Suc}, nat_T --> nat_T)) andalso (not careful orelse not (is_Var t1) orelse String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then @@ -2141,7 +2164,8 @@ (* term list -> (indexname * typ) list -> indexname * typ -> term -> term -> term -> term *) and aux_eq prems zs z t' t1 t2 = - if not (z mem zs) andalso not (exists_subterm (equal (Var z)) t') then + if not (member (op =) zs z) + andalso not (exists_subterm (curry (op =) (Var z)) t') then aux prems zs (subst_free [(Var z, t')] t2) else aux (t1 :: prems) (Term.add_vars t1 zs) t2 @@ -2299,8 +2323,8 @@ (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) => if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then aux s0 (s1 :: ss) (T1 :: Ts) t1 - else if quant_s = "" - andalso s0 mem [@{const_name All}, @{const_name Ex}] then + else if quant_s = "" andalso (s0 = @{const_name All} + orelse s0 = @{const_name Ex}) then aux s0 [s1] [T1] t1 else raise SAME () @@ -2330,7 +2354,8 @@ | cost boundss_cum_costs (j :: js) = let val (yeas, nays) = - List.partition (fn (bounds, _) => j mem bounds) + List.partition (fn (bounds, _) => + member (op =) bounds j) boundss_cum_costs val yeas_bounds = big_union fst yeas val yeas_cost = Integer.sum (map snd yeas) @@ -2339,7 +2364,7 @@ val js = all_permutations (index_seq 0 num_Ts) |> map (`(cost (t_boundss ~~ t_costs))) |> sort (int_ord o pairself fst) |> hd |> snd - val back_js = map (fn j => find_index (equal j) js) + val back_js = map (fn j => find_index (curry (op =) j) js) (index_seq 0 num_Ts) val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip)) ts @@ -2355,7 +2380,8 @@ | build ts_cum_bounds (j :: js) = let val (yeas, nays) = - List.partition (fn (_, bounds) => j mem bounds) + List.partition (fn (_, bounds) => + member (op =) bounds j) ts_cum_bounds ||> map (apfst (incr_boundvars ~1)) in @@ -2476,7 +2502,7 @@ map Bound (length trunk_arg_Ts - 1 downto 0)) in List.foldr absdummy - (Const (set_oper, [set_T, set_T] ---> set_T) + (Const (set_oper, set_T --> set_T --> set_T) $ app pos $ app neg) trunk_arg_Ts end else @@ -2548,7 +2574,7 @@ if t = Const x then list_comb (Const x', extra_args @ filter_out_indices fixed_js args) else - let val j = find_index (equal t) fixed_params in + let val j = find_index (curry (op =) t) fixed_params in list_comb (if j >= 0 then nth fixed_args j else t, args) end in aux [] t end @@ -2582,7 +2608,7 @@ else case term_under_def t of Const x => [x] | _ => [] (* term list -> typ list -> term -> term *) fun aux args Ts (Const (x as (s, T))) = - ((if not (x mem blacklist) andalso not (null args) + ((if not (member (op =) blacklist x) andalso not (null args) andalso not (String.isPrefix special_prefix s) andalso is_equational_fun ext_ctxt x then let @@ -2607,7 +2633,8 @@ (* int -> term *) fun var_for_bound_no j = Var ((bound_var_prefix ^ - nat_subscript (find_index (equal j) bound_js + 1), k), + nat_subscript (find_index (curry (op =) j) bound_js + + 1), k), nth Ts j) val fixed_args_in_axiom = map (curry subst_bounds @@ -2739,7 +2766,8 @@ \coerce_term", [t'])) | (Type (new_s, new_Ts as [new_T1, new_T2]), Type (old_s, old_Ts as [old_T1, old_T2])) => - if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then + if old_s = @{type_name fun_box} orelse old_s = @{type_name pair_box} + orelse old_s = "*" then case constr_expand ext_ctxt old_T t of Const (@{const_name FunBox}, _) $ t1 => if new_s = "fun" then @@ -2770,13 +2798,13 @@ fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)] | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\ \add_boxed_types_for_var", [T'], [])) - | _ => exists_subterm (equal (Var z)) t' ? insert (op =) T + | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T (* typ list -> typ list -> term -> indexname * typ -> typ *) fun box_var_in_def new_Ts old_Ts t (z as (_, T)) = case t of @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z | Const (s0, _) $ t1 $ _ => - if s0 mem [@{const_name "=="}, @{const_name "op ="}] then + if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then let val (t', args) = strip_comb t1 val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t') @@ -2811,7 +2839,7 @@ val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last in - list_comb (Const (s0, [T, T] ---> body_type T0), + list_comb (Const (s0, T --> T --> body_type T0), map2 (coerce_term new_Ts T) [T1, T2] [t1, t2]) end (* string -> typ -> term *) @@ -2855,7 +2883,8 @@ | Const (s as @{const_name Eps}, T) => do_description_operator s T | Const (s as @{const_name Tha}, T) => do_description_operator s T | Const (x as (s, T)) => - Const (s, if s mem [@{const_name converse}, @{const_name trancl}] then + Const (s, if s = @{const_name converse} + orelse s = @{const_name trancl} then box_relational_operator_type T else if is_built_in_const fast_descrs x orelse s = @{const_name Sigma} then @@ -2954,7 +2983,7 @@ |> map (fn ((x, js, ts), x') => (x, (js, ts, x'))) |> AList.group (op =) |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst) - |> map (fn (x, zs) => (x, zs |> (x mem xs) ? cons ([], [], x))) + |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x))) (* special -> int *) fun generality (js, _, _) = ~(length js) (* special -> special -> bool *) @@ -3022,14 +3051,15 @@ case t of t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2] | Const (x as (s, T)) => - (if x mem xs orelse is_built_in_const fast_descrs x then + (if member (op =) xs x orelse is_built_in_const fast_descrs x then accum else let val accum as (xs, _) = (x :: xs, axs) in if depth > axioms_max_depth then - raise LIMIT ("Nitpick_HOL.axioms_for_term.add_axioms_for_term", - "too many nested axioms (" ^ string_of_int depth ^ - ")") + raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\ + \add_axioms_for_term", + "too many nested axioms (" ^ + string_of_int depth ^ ")") else if Refute.is_const_of_class thy x then let val class = Logic.class_of_const s @@ -3172,10 +3202,10 @@ (* int list -> int list -> typ -> typ *) fun format_type default_format format T = let - val T = unbox_type T + val T = unbit_and_unbox_type T val format = format |> filter (curry (op <) 0) in - if forall (equal 1) format then + if forall (curry (op =) 1) format then T else let @@ -3211,7 +3241,8 @@ (* term -> term *) val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t') val (x' as (_, T'), js, ts) = - AList.find (op =) (!special_funs) (s, unbox_type T) |> the_single + AList.find (op =) (!special_funs) (s, unbit_and_unbox_type T) + |> the_single val max_j = List.last js val Ts = List.take (binder_types T', max_j + 1) val missing_js = filter_out (member (op =) js) (0 upto max_j) @@ -3226,7 +3257,8 @@ SOME t => do_term t | NONE => Var (nth missing_vars - (find_index (equal j) missing_js))) + (find_index (curry (op =) j) + missing_js))) Ts (0 upto max_j) val t = do_const x' |> fst val format = @@ -3299,8 +3331,8 @@ let val t = Const (original_name s, T) in (t, format_term_type thy def_table formats t) end) - |>> map_types (typ_subst [(@{typ bisim_iterator}, nat_T)] o unbox_type) - |>> shorten_const_names_in_term |>> shorten_abs_vars + |>> map_types unbit_and_unbox_type + |>> shorten_names_in_term |>> shorten_abs_vars in do_const end (* styp -> string *) @@ -3314,10 +3346,45 @@ else "=" +val binary_int_threshold = 4 + +(* term -> bool *) +fun may_use_binary_ints (t1 $ t2) = + may_use_binary_ints t1 andalso may_use_binary_ints t2 + | may_use_binary_ints (t as Const (s, _)) = + t <> @{const Suc} andalso + not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, + @{const_name nat_gcd}, @{const_name nat_lcm}, + @{const_name Frac}, @{const_name norm_frac}] s) + | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t' + | may_use_binary_ints _ = true +fun should_use_binary_ints (t1 $ t2) = + should_use_binary_ints t1 orelse should_use_binary_ints t2 + | should_use_binary_ints (Const (s, _)) = + member (op =) [@{const_name times_nat_inst.times_nat}, + @{const_name div_nat_inst.div_nat}, + @{const_name times_int_inst.times_int}, + @{const_name div_int_inst.div_int}] s + orelse (String.isPrefix numeral_prefix s andalso + let val n = the (Int.fromString (unprefix numeral_prefix s)) in + n <= ~ binary_int_threshold orelse n >= binary_int_threshold + end) + | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t' + | should_use_binary_ints _ = false + +(* typ -> typ *) +fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"} + | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"} + | binarize_nat_and_int_in_type (Type (s, Ts)) = + Type (s, map binarize_nat_and_int_in_type Ts) + | binarize_nat_and_int_in_type T = T +(* term -> term *) +val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type + (* extended_context -> term -> ((term list * term list) * (bool * bool)) * term *) -fun preprocess_term (ext_ctxt as {thy, destroy_constrs, boxes, skolemize, - uncurry, ...}) t = +fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes, + skolemize, uncurry, ...}) t = let val skolem_depth = if skolemize then 4 else ~1 val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), @@ -3326,14 +3393,22 @@ |> skolemize_term_and_more ext_ctxt skolem_depth |> specialize_consts_in_term ext_ctxt 0 |> `(axioms_for_term ext_ctxt) - val maybe_box = exists (not_equal (SOME false) o snd) boxes + val binarize = + case binary_ints of + SOME false => false + | _ => + forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso + (binary_ints = SOME true + orelse exists should_use_binary_ints (core_t :: def_ts @ nondef_ts)) + val box = exists (not_equal (SOME false) o snd) boxes val table = Termtab.empty |> uncurry ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts) (* bool -> bool -> term -> term *) fun do_rest def core = - uncurry ? uncurry_term table - #> maybe_box ? box_fun_and_pair_in_term ext_ctxt def + binarize ? binarize_nat_and_int_in_term + #> uncurry ? uncurry_term table + #> box ? box_fun_and_pair_in_term ext_ctxt def #> destroy_constrs ? (pull_out_universal_constrs thy def #> pull_out_existential_constrs thy #> destroy_pulled_out_constrs ext_ctxt def) diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Dec 18 12:00:44 2009 +0100 @@ -37,6 +37,7 @@ val default_default_params = [("card", ["1\8"]), ("iter", ["0,1,2,4,8,12,16,24"]), + ("bits", ["1,2,3,4,6,8,10,12"]), ("bisim_depth", ["7"]), ("box", ["smart"]), ("mono", ["smart"]), @@ -48,6 +49,7 @@ ("user_axioms", ["smart"]), ("assms", ["true"]), ("merge_type_vars", ["false"]), + ("binary_ints", ["smart"]), ("destroy_constrs", ["true"]), ("specialize", ["true"]), ("skolemize", ["true"]), @@ -83,6 +85,7 @@ ("no_user_axioms", "user_axioms"), ("no_assms", "assms"), ("dont_merge_type_vars", "merge_type_vars"), + ("unary_ints", "binary_ints"), ("dont_destroy_constrs", "destroy_constrs"), ("dont_specialize", "specialize"), ("dont_skolemize", "skolemize"), @@ -105,7 +108,7 @@ fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) negated_params s - orelse s mem ["max", "eval", "expect"] + orelse s = "max" orelse s = "eval" orelse s = "expect" orelse exists (fn p => String.isPrefix (p ^ " ") s) ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "wf", "non_wf", "format"] @@ -283,6 +286,7 @@ val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1 val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1 val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0 + val bitss = lookup_int_seq "bits" 1 val bisim_depths = lookup_int_seq "bisim_depth" ~1 val boxes = lookup_bool_option_assigns read_type_polymorphic "box" @ @@ -303,6 +307,7 @@ val user_axioms = lookup_bool_option "user_axioms" val assms = lookup_bool "assms" val merge_type_vars = lookup_bool "merge_type_vars" + val binary_ints = lookup_bool_option "binary_ints" val destroy_constrs = lookup_bool "destroy_constrs" val specialize = lookup_bool "specialize" val skolemize = lookup_bool "skolemize" @@ -333,15 +338,16 @@ val expect = lookup_string "expect" in {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, - iters_assigns = iters_assigns, bisim_depths = bisim_depths, boxes = boxes, - monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking, - falsify = falsify, debug = debug, verbose = verbose, overlord = overlord, - user_axioms = user_axioms, assms = assms, - merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs, - specialize = specialize, skolemize = skolemize, - star_linear_preds = star_linear_preds, uncurry = uncurry, - fast_descrs = fast_descrs, peephole_optim = peephole_optim, - timeout = timeout, tac_timeout = tac_timeout, sym_break = sym_break, + iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths, + boxes = boxes, monos = monos, wfs = wfs, sat_solver = sat_solver, + blocking = blocking, falsify = falsify, debug = debug, verbose = verbose, + overlord = overlord, user_axioms = user_axioms, assms = assms, + merge_type_vars = merge_type_vars, binary_ints = binary_ints, + destroy_constrs = destroy_constrs, specialize = specialize, + skolemize = skolemize, star_linear_preds = star_linear_preds, + uncurry = uncurry, fast_descrs = fast_descrs, + peephole_optim = peephole_optim, timeout = timeout, + tac_timeout = tac_timeout, sym_break = sym_break, sharing_depth = sharing_depth, flatten_props = flatten_props, max_threads = max_threads, show_skolems = show_skolems, show_datatypes = show_datatypes, show_consts = show_consts, @@ -379,8 +385,6 @@ error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".") | BAD (loc, details) => error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".") - | LIMIT (_, details) => - (warning ("Limit reached: " ^ details ^ "."); x) | NOT_SUPPORTED details => (warning ("Unsupported case: " ^ details ^ "."); x) | NUT (loc, us) => @@ -394,6 +398,10 @@ error ("Invalid term" ^ plural_s_for_list ts ^ " (" ^ quote loc ^ "): " ^ commas (map (Syntax.string_of_term ctxt) ts) ^ ".") + | TOO_LARGE (_, details) => + (warning ("Limit reached: " ^ details ^ "."); x) + | TOO_SMALL (_, details) => + (warning ("Limit reached: " ^ details ^ "."); x) | TYPE (loc, Ts, ts) => error ("Invalid type" ^ plural_s_for_list Ts ^ (if null ts then @@ -409,7 +417,7 @@ error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".") (* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *) -fun pick_nits override_params auto subgoal state = +fun pick_nits override_params auto i state = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -423,26 +431,25 @@ |> (if auto then perhaps o try else if debug then fn f => fn x => f x else handle_exceptions ctxt) - (fn (_, state) => pick_nits_in_subgoal state params auto subgoal - |>> equal "genuine") + (fn (_, state) => pick_nits_in_subgoal state params auto i + |>> curry (op =) "genuine") in if auto orelse blocking then go () else (Toplevel.thread true (fn () => (go (); ())); (false, state)) end -(* (TableFun().key * string list) list option * int option - -> Toplevel.transition -> Toplevel.transition *) -fun nitpick_trans (opt_params, opt_subgoal) = +(* raw_param list option * int option -> Toplevel.transition + -> Toplevel.transition *) +fun nitpick_trans (opt_params, opt_i) = Toplevel.keep (K () - o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal) + o snd o pick_nits (these opt_params) false (the_default 1 opt_i) o Toplevel.proof_of) (* raw_param -> string *) fun string_for_raw_param (name, value) = name ^ " = " ^ stringify_raw_param_value value -(* (TableFun().key * string) list option -> Toplevel.transition - -> Toplevel.transition *) +(* raw_param list option -> Toplevel.transition -> Toplevel.transition *) fun nitpick_params_trans opt_params = Toplevel.theory (fold set_default_raw_param (these opt_params) diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Dec 18 12:00:44 2009 +0100 @@ -19,10 +19,12 @@ val univ_card : int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int + val check_bits : int -> Kodkod.formula -> unit val check_arity : int -> int -> unit val kk_tuple : bool -> int -> int list -> Kodkod.tuple val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set val sequential_int_bounds : int -> Kodkod.int_bound list + val pow_of_two_int_bounds : int -> int -> int -> Kodkod.int_bound list val bounds_for_built_in_rels_in_formula : bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound @@ -31,10 +33,10 @@ val merge_bounds : Kodkod.bound list -> Kodkod.bound list val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula val declarative_axioms_for_datatypes : - extended_context -> int Typtab.table -> kodkod_constrs + extended_context -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list val kodkod_formula_from_nut : - int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula + int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula end; structure Nitpick_Kodkod : NITPICK_KODKOD = @@ -47,97 +49,122 @@ open Nitpick_Rep open Nitpick_Nut -type nfa_transition = Kodkod.rel_expr * typ +structure KK = Kodkod + +type nfa_transition = KK.rel_expr * typ type nfa_entry = typ * nfa_transition list type nfa_table = nfa_entry list structure NfaGraph = Graph(type key = typ val ord = TermOrd.typ_ord) -(* int -> Kodkod.int_expr list *) -fun flip_nums n = index_seq 1 n @ [0] |> map Kodkod.Num +(* int -> KK.int_expr list *) +fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num -(* int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int *) +(* int -> int -> int -> KK.bound list -> KK.formula -> int *) fun univ_card nat_card int_card main_j0 bounds formula = let - (* Kodkod.rel_expr -> int -> int *) + (* KK.rel_expr -> int -> int *) fun rel_expr_func r k = Int.max (k, case r of - Kodkod.Atom j => j + 1 - | Kodkod.AtomSeq (k', j0) => j0 + k' + KK.Atom j => j + 1 + | KK.AtomSeq (k', j0) => j0 + k' | _ => 0) - (* Kodkod.tuple -> int -> int *) + (* KK.tuple -> int -> int *) fun tuple_func t k = case t of - Kodkod.Tuple js => fold Integer.max (map (Integer.add 1) js) k + KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k | _ => k - (* Kodkod.tuple_set -> int -> int *) + (* KK.tuple_set -> int -> int *) fun tuple_set_func ts k = - Int.max (k, case ts of Kodkod.TupleAtomSeq (k', j0) => j0 + k' | _ => 0) + Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k' | _ => 0) val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, int_expr_func = K I} val tuple_F = {tuple_func = tuple_func, tuple_set_func = tuple_set_func} - val card = fold (Kodkod.fold_bound expr_F tuple_F) bounds 1 - |> Kodkod.fold_formula expr_F formula + val card = fold (KK.fold_bound expr_F tuple_F) bounds 1 + |> KK.fold_formula expr_F formula in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end -(* Proof.context -> bool -> string -> typ -> rep -> string *) -fun bound_comment ctxt debug nick T R = - short_const_name nick ^ - (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T) - else "") ^ " : " ^ string_for_rep R +(* int -> KK.formula -> unit *) +fun check_bits bits formula = + let + (* KK.int_expr -> unit -> unit *) + fun int_expr_func (KK.Num k) () = + if is_twos_complement_representable bits k then + () + else + raise TOO_SMALL ("Nitpick_Kodkod.check_bits", + "\"bits\" value " ^ string_of_int bits ^ + " too small for problem") + | int_expr_func _ () = () + val expr_F = {formula_func = K I, rel_expr_func = K I, + int_expr_func = int_expr_func} + in KK.fold_formula expr_F formula () end (* int -> int -> unit *) fun check_arity univ_card n = - if n > Kodkod.max_arity univ_card then - raise LIMIT ("Nitpick_Kodkod.check_arity", - "arity " ^ string_of_int n ^ " too large for universe of \ - \cardinality " ^ string_of_int univ_card) + if n > KK.max_arity univ_card then + raise TOO_LARGE ("Nitpick_Kodkod.check_arity", + "arity " ^ string_of_int n ^ " too large for universe of \ + \cardinality " ^ string_of_int univ_card) else () -(* bool -> int -> int list -> Kodkod.tuple *) +(* bool -> int -> int list -> KK.tuple *) fun kk_tuple debug univ_card js = if debug then - Kodkod.Tuple js + KK.Tuple js else - Kodkod.TupleIndex (length js, - fold (fn j => fn accum => accum * univ_card + j) js 0) + KK.TupleIndex (length js, + fold (fn j => fn accum => accum * univ_card + j) js 0) -(* (int * int) list -> Kodkod.tuple_set *) -val tuple_set_from_atom_schema = - foldl1 Kodkod.TupleProduct o map Kodkod.TupleAtomSeq -(* rep -> Kodkod.tuple_set *) +(* (int * int) list -> KK.tuple_set *) +val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq +(* rep -> KK.tuple_set *) val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep -(* int -> Kodkod.int_bound list *) -fun sequential_int_bounds n = - [(NONE, map (Kodkod.TupleSet o single o Kodkod.Tuple o single) - (index_seq 0 n))] +(* int -> KK.tuple_set *) +val single_atom = KK.TupleSet o single o KK.Tuple o single +(* int -> KK.int_bound list *) +fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))] +(* int -> int -> KK.int_bound list *) +fun pow_of_two_int_bounds bits j0 univ_card = + let + (* int -> int -> int -> KK.int_bound list *) + fun aux 0 _ _ = [] + | aux 1 pow_of_two j = + if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else [] + | aux iter pow_of_two j = + (SOME pow_of_two, [single_atom j]) :: + aux (iter - 1) (2 * pow_of_two) (j + 1) + in aux (bits + 1) 1 j0 end -(* Kodkod.formula -> Kodkod.n_ary_index list *) +(* KK.formula -> KK.n_ary_index list *) fun built_in_rels_in_formula formula = let - (* Kodkod.rel_expr -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list *) - fun rel_expr_func (Kodkod.Rel (n, j)) rels = - (case AList.lookup (op =) (#rels initial_pool) n of - SOME k => (j < k ? insert (op =) (n, j)) rels - | NONE => rels) - | rel_expr_func _ rels = rels + (* KK.rel_expr -> KK.n_ary_index list -> KK.n_ary_index list *) + fun rel_expr_func (r as KK.Rel (x as (n, j))) = + if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then + I + else + (case AList.lookup (op =) (#rels initial_pool) n of + SOME k => j < k ? insert (op =) x + | NONE => I) + | rel_expr_func _ = I val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, int_expr_func = K I} - in Kodkod.fold_formula expr_F formula [] end + in KK.fold_formula expr_F formula [] end val max_table_size = 65536 (* int -> unit *) fun check_table_size k = if k > max_table_size then - raise LIMIT ("Nitpick_Kodkod.check_table_size", - "precomputed table too large (" ^ string_of_int k ^ ")") + raise TOO_LARGE ("Nitpick_Kodkod.check_table_size", + "precomputed table too large (" ^ string_of_int k ^ ")") else () -(* bool -> int -> int * int -> (int -> int) -> Kodkod.tuple list *) +(* bool -> int -> int * int -> (int -> int) -> KK.tuple list *) fun tabulate_func1 debug univ_card (k, j0) f = (check_table_size k; map_filter (fn j1 => let val j2 = f j1 in @@ -146,7 +173,7 @@ else NONE end) (index_seq 0 k)) -(* bool -> int -> int * int -> int -> (int * int -> int) -> Kodkod.tuple list *) +(* bool -> int -> int * int -> int -> (int * int -> int) -> KK.tuple list *) fun tabulate_op2 debug univ_card (k, j0) res_j0 f = (check_table_size (k * k); map_filter (fn j => let @@ -161,7 +188,7 @@ NONE end) (index_seq 0 (k * k))) (* bool -> int -> int * int -> int -> (int * int -> int * int) - -> Kodkod.tuple list *) + -> KK.tuple list *) fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f = (check_table_size (k * k); map_filter (fn j => let @@ -176,13 +203,13 @@ else NONE end) (index_seq 0 (k * k))) -(* bool -> int -> int * int -> (int * int -> int) -> Kodkod.tuple list *) +(* bool -> int -> int * int -> (int * int -> int) -> KK.tuple list *) fun tabulate_nat_op2 debug univ_card (k, j0) f = tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f) fun tabulate_int_op2 debug univ_card (k, j0) f = tabulate_op2 debug univ_card (k, j0) j0 (atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0))) -(* bool -> int -> int * int -> (int * int -> int * int) -> Kodkod.tuple list *) +(* bool -> int -> int * int -> (int * int -> int * int) -> KK.tuple list *) fun tabulate_int_op2_2 debug univ_card (k, j0) f = tabulate_op2_2 debug univ_card (k, j0) j0 (pairself (atom_for_int (k, 0)) o f @@ -202,77 +229,78 @@ else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end (* bool -> int -> int -> int -> int -> int * int - -> string * bool * Kodkod.tuple list *) + -> string * bool * KK.tuple list *) fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) = (check_arity univ_card n; - if Kodkod.Rel x = not3_rel then + if x = not3_rel then ("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1)) - else if Kodkod.Rel x = suc_rel then + else if x = suc_rel then ("suc", tabulate_func1 debug univ_card (univ_card - j0 - 1, j0) (Integer.add 1)) - else if Kodkod.Rel x = nat_add_rel then + else if x = nat_add_rel then ("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +)) - else if Kodkod.Rel x = int_add_rel then + else if x = int_add_rel then ("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +)) - else if Kodkod.Rel x = nat_subtract_rel then + else if x = nat_subtract_rel then ("nat_subtract", tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus)) - else if Kodkod.Rel x = int_subtract_rel then + else if x = int_subtract_rel then ("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op -)) - else if Kodkod.Rel x = nat_multiply_rel then + else if x = nat_multiply_rel then ("nat_multiply", tabulate_nat_op2 debug univ_card (nat_card, j0) (op * )) - else if Kodkod.Rel x = int_multiply_rel then + else if x = int_multiply_rel then ("int_multiply", tabulate_int_op2 debug univ_card (int_card, j0) (op * )) - else if Kodkod.Rel x = nat_divide_rel then + else if x = nat_divide_rel then ("nat_divide", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_div) - else if Kodkod.Rel x = int_divide_rel then + else if x = int_divide_rel then ("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div) - else if Kodkod.Rel x = nat_modulo_rel then - ("nat_modulo", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_mod) - else if Kodkod.Rel x = int_modulo_rel then - ("int_modulo", tabulate_int_op2 debug univ_card (int_card, j0) isa_mod) - else if Kodkod.Rel x = nat_less_rel then + else if x = nat_less_rel then ("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0) (int_for_bool o op <)) - else if Kodkod.Rel x = int_less_rel then + else if x = int_less_rel then ("int_less", tabulate_int_op2 debug univ_card (int_card, j0) (int_for_bool o op <)) - else if Kodkod.Rel x = gcd_rel then + else if x = gcd_rel then ("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd) - else if Kodkod.Rel x = lcm_rel then + else if x = lcm_rel then ("lcm", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_lcm) - else if Kodkod.Rel x = norm_frac_rel then + else if x = norm_frac_rel then ("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0) isa_norm_frac) else raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation")) -(* bool -> int -> int -> int -> int -> int * int -> Kodkod.rel_expr - -> Kodkod.bound *) +(* bool -> int -> int -> int -> int -> int * int -> KK.rel_expr -> KK.bound *) fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x = let val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card j0 x - in ([(x, nick)], [Kodkod.TupleSet ts]) end + in ([(x, nick)], [KK.TupleSet ts]) end -(* bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list *) +(* bool -> int -> int -> int -> int -> KK.formula -> KK.bound list *) fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 = map (bound_for_built_in_rel debug univ_card nat_card int_card j0) o built_in_rels_in_formula -(* Proof.context -> bool -> nut -> Kodkod.bound *) +(* Proof.context -> bool -> string -> typ -> rep -> string *) +fun bound_comment ctxt debug nick T R = + short_name nick ^ + (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T) + else "") ^ " : " ^ string_for_rep R + +(* Proof.context -> bool -> nut -> KK.bound *) fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) = ([(x, bound_comment ctxt debug nick T R)], if nick = @{const_name bisim_iterator_max} then case R of - Atom (k, j0) => [Kodkod.TupleSet [Kodkod.Tuple [k - 1 + j0]]] + Atom (k, j0) => [single_atom (k - 1 + j0)] | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) else - [Kodkod.TupleSet [], upper_bound_for_rep R]) + [KK.TupleSet [], upper_bound_for_rep R]) | bound_for_plain_rel _ _ u = raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) -(* Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound *) +(* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *) fun bound_for_sel_rel ctxt debug dtypes (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2), nick)) = @@ -282,26 +310,24 @@ in ([(x, bound_comment ctxt debug nick T R)], if explicit_max = 0 then - [Kodkod.TupleSet []] + [KK.TupleSet []] else - let val ts = Kodkod.TupleAtomSeq (epsilon - delta, delta + j0) in + let val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) in if R2 = Formula Neut then - [ts] |> not exclusive ? cons (Kodkod.TupleSet []) + [ts] |> not exclusive ? cons (KK.TupleSet []) else - [Kodkod.TupleSet [], - Kodkod.TupleProduct (ts, upper_bound_for_rep R2)] + [KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)] end) end | bound_for_sel_rel _ _ _ u = raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u]) -(* Kodkod.bound list -> Kodkod.bound list *) +(* KK.bound list -> KK.bound list *) fun merge_bounds bs = let - (* Kodkod.bound -> int *) + (* KK.bound -> int *) fun arity (zs, _) = fst (fst (hd zs)) - (* Kodkod.bound list -> Kodkod.bound -> Kodkod.bound list - -> Kodkod.bound list *) + (* KK.bound list -> KK.bound -> KK.bound list -> KK.bound list *) fun add_bound ds b [] = List.revAppend (ds, [b]) | add_bound ds b (c :: cs) = if arity b = arity c andalso snd b = snd c then @@ -310,40 +336,40 @@ add_bound (c :: ds) b cs in fold (add_bound []) bs [] end -(* int -> int -> Kodkod.rel_expr list *) -fun unary_var_seq j0 n = map (curry Kodkod.Var 1) (index_seq j0 n) +(* int -> int -> KK.rel_expr list *) +fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n) -(* int list -> Kodkod.rel_expr *) -val singleton_from_combination = foldl1 Kodkod.Product o map Kodkod.Atom -(* rep -> Kodkod.rel_expr list *) +(* int list -> KK.rel_expr *) +val singleton_from_combination = foldl1 KK.Product o map KK.Atom +(* rep -> KK.rel_expr list *) fun all_singletons_for_rep R = if is_lone_rep R then all_combinations_for_rep R |> map singleton_from_combination else raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R]) -(* Kodkod.rel_expr -> Kodkod.rel_expr list *) -fun unpack_products (Kodkod.Product (r1, r2)) = +(* KK.rel_expr -> KK.rel_expr list *) +fun unpack_products (KK.Product (r1, r2)) = unpack_products r1 @ unpack_products r2 | unpack_products r = [r] -fun unpack_joins (Kodkod.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2 +fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2 | unpack_joins r = [r] -(* rep -> Kodkod.rel_expr *) +(* rep -> KK.rel_expr *) val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep fun full_rel_for_rep R = case atom_schema_of_rep R of [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R]) - | schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema) + | schema => foldl1 KK.Product (map KK.AtomSeq schema) -(* int -> int list -> Kodkod.decl list *) +(* int -> int list -> KK.decl list *) fun decls_for_atom_schema j0 schema = - map2 (fn j => fn x => Kodkod.DeclOne ((1, j), Kodkod.AtomSeq x)) + map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x)) (index_seq j0 (length schema)) schema (* The type constraint below is a workaround for a Poly/ML bug. *) -(* kodkod_constrs -> rep -> Kodkod.rel_expr -> Kodkod.formula *) +(* kodkod_constrs -> rep -> KK.rel_expr -> KK.formula *) fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs) R r = let val body_R = body_rep R in @@ -352,13 +378,13 @@ val binder_schema = atom_schema_of_reps (binder_reps R) val body_schema = atom_schema_of_rep body_R val one = is_one_rep body_R - val opt_x = case r of Kodkod.Rel x => SOME x | _ => NONE + val opt_x = case r of KK.Rel x => SOME x | _ => NONE in if opt_x <> NONE andalso length binder_schema = 1 andalso length body_schema = 1 then - (if one then Kodkod.Function else Kodkod.Functional) - (the opt_x, Kodkod.AtomSeq (hd binder_schema), - Kodkod.AtomSeq (hd body_schema)) + (if one then KK.Function else KK.Functional) + (the opt_x, KK.AtomSeq (hd binder_schema), + KK.AtomSeq (hd body_schema)) else let val decls = decls_for_atom_schema ~1 binder_schema @@ -367,71 +393,69 @@ in kk_all decls (kk_xone (fold kk_join vars r)) end end else - Kodkod.True + KK.True end -fun kk_n_ary_function kk R (r as Kodkod.Rel _) = +fun kk_n_ary_function kk R (r as KK.Rel x) = if not (is_opt_rep R) then - if r = suc_rel then - Kodkod.False - else if r = nat_add_rel then + if x = suc_rel then + KK.False + else if x = nat_add_rel then formula_for_bool (card_of_rep (body_rep R) = 1) - else if r = nat_multiply_rel then + else if x = nat_multiply_rel then formula_for_bool (card_of_rep (body_rep R) <= 2) else d_n_ary_function kk R r - else if r = nat_subtract_rel then - Kodkod.True + else if x = nat_subtract_rel then + KK.True else d_n_ary_function kk R r | kk_n_ary_function kk R r = d_n_ary_function kk R r -(* kodkod_constrs -> Kodkod.rel_expr list -> Kodkod.formula *) -fun kk_disjoint_sets _ [] = Kodkod.True +(* kodkod_constrs -> KK.rel_expr list -> KK.formula *) +fun kk_disjoint_sets _ [] = KK.True | kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs) (r :: rs) = fold (kk_and o kk_no o kk_intersect r) rs (kk_disjoint_sets kk rs) -(* int -> kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr) - -> Kodkod.rel_expr -> Kodkod.rel_expr *) -fun basic_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r = +(* int -> kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr + -> KK.rel_expr *) +fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r = if inline_rel_expr r then f r else - let val x = (Kodkod.arity_of_rel_expr r, j) in - kk_rel_let [Kodkod.AssignRelReg (x, r)] (f (Kodkod.RelReg x)) + let val x = (KK.arity_of_rel_expr r, j) in + kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x)) end +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr + -> KK.rel_expr *) +val single_rel_rel_let = basic_rel_rel_let 0 +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr) -> KK.rel_expr + -> KK.rel_expr -> KK.rel_expr *) +fun double_rel_rel_let kk f r1 r2 = + single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1 +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr) + -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *) +fun tripl_rel_rel_let kk f r1 r2 r3 = + double_rel_rel_let kk + (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2 -(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr) -> Kodkod.rel_expr - -> Kodkod.rel_expr *) -val single_rel_let = basic_rel_let 0 -(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr) - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *) -fun double_rel_let kk f r1 r2 = - single_rel_let kk (fn r1 => basic_rel_let 1 kk (f r1) r2) r1 -(* kodkod_constrs - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr) - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr - -> Kodkod.rel_expr *) -fun triple_rel_let kk f r1 r2 r3 = - double_rel_let kk (fn r1 => fn r2 => basic_rel_let 2 kk (f r1 r2) r3) r1 r2 - -(* kodkod_constrs -> int -> Kodkod.formula -> Kodkod.rel_expr *) +(* kodkod_constrs -> int -> KK.formula -> KK.rel_expr *) fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f = - kk_rel_if f (Kodkod.Atom (j0 + 1)) (Kodkod.Atom j0) -(* kodkod_constrs -> rep -> Kodkod.formula -> Kodkod.rel_expr *) + kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0) +(* kodkod_constrs -> rep -> KK.formula -> KK.rel_expr *) fun rel_expr_from_formula kk R f = case unopt_rep R of Atom (2, j0) => atom_from_formula kk j0 f | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R]) -(* kodkod_cotrs -> int -> int -> Kodkod.rel_expr -> Kodkod.rel_expr list *) +(* kodkod_cotrs -> int -> int -> KK.rel_expr -> KK.rel_expr list *) fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity num_chunks r = List.tabulate (num_chunks, fn j => kk_project_seq r (j * chunk_arity) chunk_arity) -(* kodkod_constrs -> bool -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr - -> Kodkod.rel_expr *) +(* kodkod_constrs -> bool -> rep -> rep -> KK.rel_expr -> KK.rel_expr + -> KK.rel_expr *) fun kk_n_fold_join (kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1 res_R r1 r2 = @@ -451,8 +475,8 @@ arity1 (arity_of_rep res_R) end -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr list - -> Kodkod.rel_expr list -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr list + -> KK.rel_expr list -> KK.rel_expr *) fun kk_case_switch (kk as {kk_union, kk_product, ...}) R1 R2 r rs1 rs2 = if rs1 = rs2 then r else kk_n_fold_join kk true R1 R2 r (fold1 kk_union (map2 kk_product rs1 rs2)) @@ -460,7 +484,7 @@ val lone_rep_fallback_max_card = 4096 val some_j0 = 0 -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) fun lone_rep_fallback kk new_R old_R r = if old_R = new_R then r @@ -469,15 +493,15 @@ if is_lone_rep old_R andalso is_lone_rep new_R andalso card = card_of_rep new_R then if card >= lone_rep_fallback_max_card then - raise LIMIT ("Nitpick_Kodkod.lone_rep_fallback", - "too high cardinality (" ^ string_of_int card ^ ")") + raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback", + "too high cardinality (" ^ string_of_int card ^ ")") else kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R) (all_singletons_for_rep new_R) else raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R]) end -(* kodkod_constrs -> int * int -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> int * int -> rep -> KK.rel_expr -> KK.rel_expr *) and atom_from_rel_expr kk (x as (k, j0)) old_R r = case old_R of Func (R1, R2) => @@ -490,7 +514,7 @@ end | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R]) | _ => lone_rep_fallback kk (Atom x) old_R r -(* kodkod_constrs -> rep list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep list -> rep -> KK.rel_expr -> KK.rel_expr *) and struct_from_rel_expr kk Rs old_R r = case old_R of Atom _ => lone_rep_fallback kk (Struct Rs) old_R r @@ -514,7 +538,7 @@ lone_rep_fallback kk (Struct Rs) old_R r end | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R]) -(* kodkod_constrs -> int -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> int -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) and vect_from_rel_expr kk k R old_R r = case old_R of Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r @@ -537,7 +561,7 @@ (kk_n_fold_join kk true R1 R2 arg_r r)) (all_singletons_for_rep R1)) | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) -(* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r = let val dom_card = card_of_rep R1 @@ -566,9 +590,9 @@ let val args_rs = all_singletons_for_rep R1 val vals_rs = unpack_vect_in_chunks kk 1 k r - (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *) + (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *) fun empty_or_singleton_set_for arg_r val_r = - #kk_join kk val_r (#kk_product kk (Kodkod.Atom (j0 + 1)) arg_r) + #kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r) in fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs) end @@ -585,11 +609,11 @@ #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) end | Func (Unit, (Atom (2, j0))) => - #kk_rel_if kk (#kk_rel_eq kk r (Kodkod.Atom (j0 + 1))) + #kk_rel_if kk (#kk_rel_eq kk r (KK.Atom (j0 + 1))) (full_rel_for_rep R1) (empty_rel_for_rep R1) | Func (R1', Atom (2, j0)) => func_from_no_opt_rel_expr kk R1 (Formula Neut) - (Func (R1', Formula Neut)) (#kk_join kk r (Kodkod.Atom (j0 + 1))) + (Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1))) | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (R1, Formula Neut)])) | func_from_no_opt_rel_expr kk R1 R2 old_R r = @@ -605,14 +629,14 @@ Atom (x as (2, j0)) => let val schema = atom_schema_of_rep R1 in if length schema = 1 then - #kk_override kk (#kk_product kk (Kodkod.AtomSeq (hd schema)) - (Kodkod.Atom j0)) - (#kk_product kk r (Kodkod.Atom (j0 + 1))) + #kk_override kk (#kk_product kk (KK.AtomSeq (hd schema)) + (KK.Atom j0)) + (#kk_product kk r (KK.Atom (j0 + 1))) else let val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema)) |> rel_expr_from_rel_expr kk R1' R1 - val r2 = Kodkod.Var (1, ~(length schema) - 1) + val r2 = KK.Var (1, ~(length schema) - 1) val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r) in #kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x])) @@ -624,7 +648,7 @@ | Func (Unit, R2') => let val j0 = some_j0 in func_from_no_opt_rel_expr kk R1 R2 (Func (Atom (1, j0), R2')) - (#kk_product kk (Kodkod.Atom j0) r) + (#kk_product kk (KK.Atom j0) r) end | Func (R1', R2') => if R1 = R1' andalso R2 = R2' then @@ -649,7 +673,7 @@ end | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (R1, R2)]) -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) and rel_expr_from_rel_expr kk new_R old_R r = let val unopt_old_R = unopt_rep old_R @@ -669,28 +693,43 @@ [old_R, new_R])) unopt_old_R r end -(* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2)) -(* kodkod_constrs -> nut -> Kodkod.formula *) +(* kodkod_constrs -> typ -> KK.rel_expr -> KK.rel_expr *) +fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r = + kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then + unsigned_bit_word_sel_rel + else + signed_bit_word_sel_rel)) +(* kodkod_constrs -> typ -> KK.rel_expr -> KK.int_expr *) +val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom +(* kodkod_constrs -> typ -> rep -> KK.int_expr -> KK.rel_expr *) +fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...} + : kodkod_constrs) T R i = + kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R)) + (kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1))) + (KK.Bits i)) + +(* kodkod_constrs -> nut -> KK.formula *) fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) = kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep) - (Kodkod.Rel x) + (KK.Rel x) | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs) (FreeRel (x, _, R, _)) = - if is_one_rep R then kk_one (Kodkod.Rel x) - else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (Kodkod.Rel x) - else Kodkod.True + if is_one_rep R then kk_one (KK.Rel x) + else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x) + else KK.True | declarative_axiom_for_plain_rel _ u = raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u]) -(* nut NameTable.table -> styp -> Kodkod.rel_expr * rep * int *) +(* nut NameTable.table -> styp -> KK.rel_expr * rep * int *) fun const_triple rel_table (x as (s, T)) = case the_name rel_table (ConstName (s, T, Any)) of - FreeRel ((n, j), _, R, _) => (Kodkod.Rel (n, j), R, n) + FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n) | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x]) -(* nut NameTable.table -> styp -> Kodkod.rel_expr *) +(* nut NameTable.table -> styp -> KK.rel_expr *) fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list @@ -704,7 +743,7 @@ in map_filter (fn (j, T) => if forall (not_equal T o #typ) dtypes then NONE - else SOME (kk_project r (map Kodkod.Num [0, j]), T)) + else SOME (kk_project r (map KK.Num [0, j]), T)) (index_seq 1 (arity - 1) ~~ tl type_schema) end (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list @@ -720,28 +759,28 @@ SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes o #const) constrs) -val empty_rel = Kodkod.Product (Kodkod.None, Kodkod.None) +val empty_rel = KK.Product (KK.None, KK.None) -(* nfa_table -> typ -> typ -> Kodkod.rel_expr list *) +(* nfa_table -> typ -> typ -> KK.rel_expr list *) fun direct_path_rel_exprs nfa start final = case AList.lookup (op =) nfa final of - SOME trans => map fst (filter (equal start o snd) trans) + SOME trans => map fst (filter (curry (op =) start o snd) trans) | NONE => [] -(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> Kodkod.rel_expr *) +(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *) and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final = fold kk_union (direct_path_rel_exprs nfa start final) - (if start = final then Kodkod.Iden else empty_rel) + (if start = final then KK.Iden else empty_rel) | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final = kk_union (any_path_rel_expr kk nfa qs start final) (knot_path_rel_expr kk nfa qs start q final) (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ - -> Kodkod.rel_expr *) + -> KK.rel_expr *) and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start knot final = kk_join (kk_join (any_path_rel_expr kk nfa qs knot final) (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot))) (any_path_rel_expr kk nfa qs start knot) -(* kodkod_constrs -> nfa_table -> typ list -> typ -> Kodkod.rel_expr *) +(* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *) and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start = fold kk_union (direct_path_rel_exprs nfa start start) empty_rel | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start = @@ -769,12 +808,12 @@ nfa |> graph_for_nfa |> NfaGraph.strong_conn |> map (fn keys => filter (member (op =) keys o fst) nfa) -(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> Kodkod.formula *) +(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *) fun acyclicity_axiom_for_datatype dtypes kk nfa start = #kk_no kk (#kk_intersect kk - (loop_path_rel_expr kk nfa (map fst nfa) start) Kodkod.Iden) + (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden) (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list - -> Kodkod.formula list *) + -> KK.formula list *) fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes = map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes |> strongly_connected_sub_nfas @@ -782,7 +821,7 @@ nfa) (* extended_context -> int -> kodkod_constrs -> nut NameTable.table - -> Kodkod.rel_expr -> constr_spec -> int -> Kodkod.formula *) + -> KK.rel_expr -> constr_spec -> int -> KK.formula *) fun sel_axiom_for_sel ext_ctxt j0 (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no, kk_join, ...}) rel_table dom_r @@ -797,16 +836,15 @@ if exclusive then kk_n_ary_function kk (Func (Atom z, R2)) r else - let val r' = kk_join (Kodkod.Var (1, 0)) r in - kk_all [Kodkod.DeclOne ((1, 0), Kodkod.AtomSeq z)] - (kk_formula_if (kk_subset (Kodkod.Var (1, 0)) dom_r) - (kk_n_ary_function kk R2 r') - (kk_no r')) + let val r' = kk_join (KK.Var (1, 0)) r in + kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)] + (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r) + (kk_n_ary_function kk R2 r') (kk_no r')) end end -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table - -> constr_spec -> Kodkod.formula list *) -fun sel_axioms_for_constr ext_ctxt j0 kk rel_table +(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table + -> constr_spec -> KK.formula list *) +fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table (constr as {const, delta, epsilon, explicit_max, ...}) = let val honors_explicit_max = @@ -818,30 +856,35 @@ let val ran_r = discr_rel_expr rel_table const val max_axiom = - if honors_explicit_max then Kodkod.True - else Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max) + if honors_explicit_max then + KK.True + else if is_twos_complement_representable bits (epsilon - delta) then + KK.LE (KK.Cardinality ran_r, KK.Num explicit_max) + else + raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr", + "\"bits\" value " ^ string_of_int bits ^ + " too small for \"max\"") in max_axiom :: map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr) (index_seq 0 (num_sels_for_constr_type (snd const))) end end -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table - -> dtype_spec -> Kodkod.formula list *) -fun sel_axioms_for_datatype ext_ctxt j0 kk rel_table +(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table + -> dtype_spec -> KK.formula list *) +fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table ({constrs, ...} : dtype_spec) = - maps (sel_axioms_for_constr ext_ctxt j0 kk rel_table) constrs + maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs (* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec - -> Kodkod.formula list *) + -> KK.formula list *) fun uniqueness_axiom_for_constr ext_ctxt ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} : kodkod_constrs) rel_table ({const, ...} : constr_spec) = let - (* Kodkod.rel_expr -> Kodkod.formula *) + (* KK.rel_expr -> KK.formula *) fun conjunct_for_sel r = - kk_rel_eq (kk_join (Kodkod.Var (1, 0)) r) - (kk_join (Kodkod.Var (1, 1)) r) + kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r) val num_sels = num_sels_for_constr_type (snd const) val triples = map (const_triple rel_table o boxed_nth_sel_for_constr ext_ctxt const) @@ -855,13 +898,13 @@ if num_sels = 0 then kk_lone set_r else - kk_all (map (Kodkod.DeclOne o rpair set_r o pair 1) [0, 1]) + kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1]) (kk_implies (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples))) - (kk_rel_eq (Kodkod.Var (1, 0)) (Kodkod.Var (1, 1)))) + (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1)))) end (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec - -> Kodkod.formula list *) + -> KK.formula list *) fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table ({constrs, ...} : dtype_spec) = map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs @@ -869,7 +912,7 @@ (* constr_spec -> int *) fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta (* int -> kodkod_constrs -> nut NameTable.table -> dtype_spec - -> Kodkod.formula list *) + -> KK.formula list *) fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...}) rel_table ({card, constrs, ...} : dtype_spec) = @@ -877,28 +920,29 @@ [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool] else let val rs = map (discr_rel_expr rel_table o #const) constrs in - [kk_rel_eq (fold1 kk_union rs) (Kodkod.AtomSeq (card, j0)), + [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)), kk_disjoint_sets kk rs] end -(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table - -> dtype_spec -> Kodkod.formula list *) -fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = [] - | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) = +(* extended_context -> int -> int Typtab.table -> kodkod_constrs + -> nut NameTable.table -> dtype_spec -> KK.formula list *) +fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = [] + | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table + (dtype as {typ, ...}) = let val j0 = offset_of_type ofs typ in - sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @ + sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @ uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @ partition_axioms_for_datatype j0 kk rel_table dtype end -(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table - -> dtype_spec list -> Kodkod.formula list *) -fun declarative_axioms_for_datatypes ext_ctxt ofs kk rel_table dtypes = +(* extended_context -> int -> int Typtab.table -> kodkod_constrs + -> nut NameTable.table -> dtype_spec list -> KK.formula list *) +fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes = acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @ - maps (other_axioms_for_datatype ext_ctxt ofs kk rel_table) dtypes + maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes -(* int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *) -fun kodkod_formula_from_nut ofs liberal +(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *) +fun kodkod_formula_from_nut bits ofs liberal (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not, kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference, @@ -909,53 +953,53 @@ val main_j0 = offset_of_type ofs bool_T val bool_j0 = main_j0 val bool_atom_R = Atom (2, main_j0) - val false_atom = Kodkod.Atom bool_j0 - val true_atom = Kodkod.Atom (bool_j0 + 1) + val false_atom = KK.Atom bool_j0 + val true_atom = KK.Atom (bool_j0 + 1) - (* polarity -> int -> Kodkod.rel_expr -> Kodkod.formula *) + (* polarity -> int -> KK.rel_expr -> KK.formula *) fun formula_from_opt_atom polar j0 r = case polar of - Neg => kk_not (kk_rel_eq r (Kodkod.Atom j0)) - | _ => kk_rel_eq r (Kodkod.Atom (j0 + 1)) - (* int -> Kodkod.rel_expr -> Kodkod.formula *) + Neg => kk_not (kk_rel_eq r (KK.Atom j0)) + | _ => kk_rel_eq r (KK.Atom (j0 + 1)) + (* int -> KK.rel_expr -> KK.formula *) val formula_from_atom = formula_from_opt_atom Pos - (* Kodkod.formula -> Kodkod.formula -> Kodkod.formula *) + (* KK.formula -> KK.formula -> KK.formula *) fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2) - (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *) + (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *) val kk_or3 = - double_rel_let kk + double_rel_rel_let kk (fn r1 => fn r2 => kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom (kk_intersect r1 r2)) val kk_and3 = - double_rel_let kk + double_rel_rel_let kk (fn r1 => fn r2 => kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom (kk_intersect r1 r2)) fun kk_notimplies3 r1 r2 = kk_and3 r1 (kk_not3 r2) - (* int -> Kodkod.rel_expr -> Kodkod.formula list *) + (* int -> KK.rel_expr -> KK.formula list *) val unpack_formulas = map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1 - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) -> int - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *) + (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr + -> KK.rel_expr -> KK.rel_expr *) fun kk_vect_set_op connective k r1 r2 = fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective) (unpack_formulas k r1) (unpack_formulas k r2)) - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) -> int - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula *) + (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr + -> KK.rel_expr -> KK.formula *) fun kk_vect_set_bool_op connective k r1 r2 = fold1 kk_and (map2 connective (unpack_formulas k r1) (unpack_formulas k r2)) - (* nut -> Kodkod.formula *) + (* nut -> KK.formula *) fun to_f u = case rep_of u of Formula polar => (case u of - Cst (False, _, _) => Kodkod.False - | Cst (True, _, _) => Kodkod.True + Cst (False, _, _) => KK.False + | Cst (True, _, _) => KK.True | Op1 (Not, _, _, u1) => kk_not (to_f_with_polarity (flip_polarity polar) u1) | Op1 (Finite, _, _, u1) => @@ -964,9 +1008,9 @@ Neut => if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) else - Kodkod.True + KK.True | Pos => formula_for_bool (not opt1) - | Neg => Kodkod.True + | Neg => KK.True end | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1 | Op2 (All, _, _, u1, u2) => @@ -1002,7 +1046,7 @@ else let (* FIXME: merge with similar code below *) - (* bool -> nut -> Kodkod.rel_expr *) + (* bool -> nut -> KK.rel_expr *) fun set_to_r widen u = if widen then kk_difference (full_rel_for_rep dom_R) @@ -1015,7 +1059,7 @@ end | Op2 (DefEq, _, _, u1, u2) => (case min_rep (rep_of u1) (rep_of u2) of - Unit => Kodkod.True + Unit => KK.True | Formula polar => kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) | min_R => @@ -1031,11 +1075,11 @@ fold (kk_or o (kk_no o to_r)) opt_arg_us (kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)) else - kk_no (kk_difference (to_rep min_R u1) (to_rep min_R u2)) + kk_subset (to_rep min_R u1) (to_rep min_R u2) end) | Op2 (Eq, T, R, u1, u2) => (case min_rep (rep_of u1) (rep_of u2) of - Unit => Kodkod.True + Unit => KK.True | Formula polar => kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) | min_R => @@ -1064,10 +1108,10 @@ else if is_lone_rep min_R then if arity_of_rep min_R = 1 then - kk_subset (kk_product r1 r2) Kodkod.Iden + kk_subset (kk_product r1 r2) KK.Iden else if not both_opt then (r1, r2) |> is_opt_rep (rep_of u2) ? swap - |> uncurry kk_difference |> kk_no + |-> kk_subset else raise SAME () else @@ -1089,8 +1133,8 @@ val rs2 = unpack_products r2 in if length rs1 = length rs2 - andalso map Kodkod.arity_of_rel_expr rs1 - = map Kodkod.arity_of_rel_expr rs2 then + andalso map KK.arity_of_rel_expr rs1 + = map KK.arity_of_rel_expr rs2 then fold1 kk_and (map2 kk_subset rs1 rs2) else kk_subset r1 r2 @@ -1115,26 +1159,25 @@ | Op3 (If, _, _, u1, u2, u3) => kk_formula_if (to_f u1) (to_f_with_polarity polar u2) (to_f_with_polarity polar u3) - | FormulaReg (j, _, _) => Kodkod.FormulaReg j + | FormulaReg (j, _, _) => KK.FormulaReg j | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])) | Atom (2, j0) => formula_from_atom j0 (to_r u) | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]) - (* polarity -> nut -> Kodkod.formula *) + (* polarity -> nut -> KK.formula *) and to_f_with_polarity polar u = case rep_of u of Formula _ => to_f u | Atom (2, j0) => formula_from_atom j0 (to_r u) | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u) | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u]) - (* nut -> Kodkod.rel_expr *) + (* nut -> KK.rel_expr *) and to_r u = case u of Cst (False, _, Atom _) => false_atom | Cst (True, _, Atom _) => true_atom | Cst (Iden, T, Func (Struct [R1, R2], Formula Neut)) => if R1 = R2 andalso arity_of_rep R1 = 1 then - kk_intersect Kodkod.Iden (kk_product (full_rel_for_rep R1) - Kodkod.Univ) + kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ) else let val schema1 = atom_schema_of_rep R1 @@ -1150,66 +1193,125 @@ (kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1) (rel_expr_from_rel_expr kk min_R R2 r2)) end - | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => Kodkod.Atom j0 + | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0 | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) => to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut))) - | Cst (Num j, @{typ int}, R) => - (case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of - ~1 => if is_opt_rep R then Kodkod.None + | Cst (Num j, T, R) => + if is_word_type T then + atom_from_int_expr kk T R (KK.Num j) + else if T = int_T then + case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of + ~1 => if is_opt_rep R then KK.None else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) - | j' => Kodkod.Atom j') - | Cst (Num j, T, R) => - if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T) - else if is_opt_rep R then Kodkod.None - else raise NUT ("Nitpick_Kodkod.to_r", [u]) + | j' => KK.Atom j' + else + if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T) + else if is_opt_rep R then KK.None + else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) | Cst (Unknown, _, R) => empty_rel_for_rep R | Cst (Unrep, _, R) => empty_rel_for_rep R - | Cst (Suc, T, Func (Atom x, _)) => - if domain_type T <> nat_T then suc_rel - else kk_intersect suc_rel (kk_product Kodkod.Univ (Kodkod.AtomSeq x)) - | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => nat_add_rel - | Cst (Add, Type ("fun", [@{typ int}, _]), _) => int_add_rel - | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) => nat_subtract_rel - | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) => int_subtract_rel - | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) => nat_multiply_rel - | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) => int_multiply_rel - | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => nat_divide_rel - | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => int_divide_rel - | Cst (Modulo, Type ("fun", [@{typ nat}, _]), _) => nat_modulo_rel - | Cst (Modulo, Type ("fun", [@{typ int}, _]), _) => int_modulo_rel - | Cst (Gcd, _, _) => gcd_rel - | Cst (Lcm, _, _) => lcm_rel - | Cst (Fracs, _, Func (Atom (1, _), _)) => Kodkod.None + | Cst (Suc, T as @{typ "unsigned_bit word => unsigned_bit word"}, R) => + to_bit_word_unary_op T R (curry KK.Add (KK.Num 1)) + | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) => + kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x)) + | Cst (Suc, _, Func (Atom x, _)) => KK.Rel suc_rel + | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel + | Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel + | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => + to_bit_word_binary_op T R NONE (SOME (curry KK.Add)) + | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => + to_bit_word_binary_op T R + (SOME (fn i1 => fn i2 => fn i3 => + kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2))) + (KK.LE (KK.Num 0, KK.BitXor (i2, i3))))) + (SOME (curry KK.Add)) + | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) => + KK.Rel nat_subtract_rel + | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) => + KK.Rel int_subtract_rel + | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => + to_bit_word_binary_op T R NONE + (SOME (fn i1 => fn i2 => + KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2)))) + | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => + to_bit_word_binary_op T R + (SOME (fn i1 => fn i2 => fn i3 => + kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0)) + (KK.LT (KK.BitXor (i2, i3), KK.Num 0)))) + (SOME (curry KK.Sub)) + | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) => + KK.Rel nat_multiply_rel + | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) => + KK.Rel int_multiply_rel + | Cst (Multiply, + T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) => + to_bit_word_binary_op T R + (SOME (fn i1 => fn i2 => fn i3 => + kk_or (KK.IntEq (i2, KK.Num 0)) + (KK.IntEq (KK.Div (i3, i2), i1) + |> bit_T = @{typ signed_bit} + ? kk_and (KK.LE (KK.Num 0, + foldl1 KK.BitAnd [i1, i2, i3]))))) + (SOME (curry KK.Mult)) + | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_divide_rel + | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_divide_rel + | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => + to_bit_word_binary_op T R NONE + (SOME (fn i1 => fn i2 => + KK.IntIf (KK.IntEq (i2, KK.Num 0), + KK.Num 0, KK.Div (i1, i2)))) + | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => + to_bit_word_binary_op T R + (SOME (fn i1 => fn i2 => fn i3 => + KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3]))) + (SOME (fn i1 => fn i2 => + KK.IntIf (kk_and (KK.LT (i1, KK.Num 0)) + (KK.LT (KK.Num 0, i2)), + KK.Sub (KK.Div (KK.Add (i1, KK.Num 1), i2), KK.Num 1), + KK.IntIf (kk_and (KK.LT (KK.Num 0, i1)) + (KK.LT (i2, KK.Num 0)), + KK.Sub (KK.Div (KK.Sub (i1, KK.Num 1), i2), KK.Num 1), + KK.IntIf (KK.IntEq (i2, KK.Num 0), + KK.Num 0, KK.Div (i1, i2)))))) + | Cst (Gcd, _, _) => KK.Rel gcd_rel + | Cst (Lcm, _, _) => KK.Rel lcm_rel + | Cst (Fracs, _, Func (Atom (1, _), _)) => KK.None | Cst (Fracs, _, Func (Struct _, _)) => - kk_project_seq norm_frac_rel 2 2 - | Cst (NormFrac, _, _) => norm_frac_rel - | Cst (NatToInt, _, Func (Atom _, Atom _)) => Kodkod.Iden - | Cst (NatToInt, _, + kk_project_seq (KK.Rel norm_frac_rel) 2 2 + | Cst (NormFrac, _, _) => KK.Rel norm_frac_rel + | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) => + KK.Iden + | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) => if nat_j0 = int_j0 then - kk_intersect Kodkod.Iden - (kk_product (Kodkod.AtomSeq (max_int_for_card int_k + 1, nat_j0)) - Kodkod.Univ) + kk_intersect KK.Iden + (kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0)) + KK.Univ) else raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"") - | Cst (IntToNat, _, Func (Atom (int_k, int_j0), nat_R)) => + | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => + to_bit_word_unary_op T R I + | Cst (IntToNat, Type ("fun", [@{typ int}, _]), + Func (Atom (int_k, int_j0), nat_R)) => let val abs_card = max_int_for_card int_k + 1 val (nat_k, nat_j0) = the_single (atom_schema_of_rep nat_R) val overlap = Int.min (nat_k, abs_card) in if nat_j0 = int_j0 then - kk_union (kk_product (Kodkod.AtomSeq (int_k - abs_card, - int_j0 + abs_card)) - (Kodkod.Atom nat_j0)) - (kk_intersect Kodkod.Iden - (kk_product (Kodkod.AtomSeq (overlap, int_j0)) - Kodkod.Univ)) + kk_union (kk_product (KK.AtomSeq (int_k - abs_card, + int_j0 + abs_card)) + (KK.Atom nat_j0)) + (kk_intersect KK.Iden + (kk_product (KK.AtomSeq (overlap, int_j0)) KK.Univ)) else raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"") end + | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => + to_bit_word_unary_op T R + (fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i)) | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1) - | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None + | Op1 (Finite, _, Opt (Atom _), _) => KK.None | Op1 (Converse, T, R, u1) => let val (b_T, a_T) = HOLogic.dest_prodT (domain_type T) @@ -1229,9 +1331,9 @@ val body_arity = arity_of_rep body_R in kk_project (to_rep (Func (Struct [a_R, b_R], body_R)) u1) - (map Kodkod.Num (index_seq a_arity b_arity @ - index_seq 0 a_arity @ - index_seq ab_arity body_arity)) + (map KK.Num (index_seq a_arity b_arity @ + index_seq 0 a_arity @ + index_seq ab_arity body_arity)) |> rel_expr_from_rel_expr kk R (Func (Struct [b_R, a_R], body_R)) end | Op1 (Closure, _, R, u1) => @@ -1241,7 +1343,7 @@ val R' = rep_to_binary_rel_rep ofs T1 (unopt_rep (rep_of u1)) val R'' = opt_rep ofs T1 R' in - single_rel_let kk + single_rel_rel_let kk (fn r => let val true_r = kk_closure (kk_join r true_atom) @@ -1266,7 +1368,7 @@ Func (R1, Formula Neut) => to_rep R1 u1 | Func (Unit, Opt R) => to_guard [u1] R true_atom | Func (R1, R2 as Opt _) => - single_rel_let kk + single_rel_rel_let kk (fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R) (rel_expr_to_func kk R1 bool_atom_R (Func (R1, Formula Neut)) r)) @@ -1293,13 +1395,13 @@ | Op2 (Exist, T, Opt _, u1, u2) => let val rs1 = untuple to_decl u1 in if not (is_opt_rep (rep_of u2)) then - kk_rel_if (kk_exist rs1 (to_f u2)) true_atom Kodkod.None + kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None else let val r2 = to_r u2 in kk_union (kk_rel_if (kk_exist rs1 (kk_rel_eq r2 true_atom)) - true_atom Kodkod.None) + true_atom KK.None) (kk_rel_if (kk_all rs1 (kk_rel_eq r2 false_atom)) - false_atom Kodkod.None) + false_atom KK.None) end end | Op2 (Or, _, _, u1, u2) => @@ -1309,12 +1411,22 @@ if is_opt_rep (rep_of u1) then kk_rel_if (to_f u2) (to_r u1) false_atom else kk_rel_if (to_f u1) (to_r u2) false_atom | Op2 (Less, _, _, u1, u2) => - if type_of u1 = nat_T then - if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom - else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom - else kk_nat_less (to_integer u1) (to_integer u2) - else - kk_int_less (to_integer u1) (to_integer u2) + (case type_of u1 of + @{typ nat} => + if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom + else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom + else kk_nat_less (to_integer u1) (to_integer u2) + | @{typ int} => kk_int_less (to_integer u1) (to_integer u2) + | _ => double_rel_rel_let kk + (fn r1 => fn r2 => + kk_rel_if + (fold kk_and (map_filter (fn (u, r) => + if is_opt_rep (rep_of u) then SOME (kk_some r) + else NONE) [(u1, r1), (u2, r2)]) KK.True) + (atom_from_formula kk bool_j0 (KK.LT (pairself + (int_expr_from_atom kk (type_of u1)) (r1, r2)))) + KK.None) + (to_r u1) (to_r u2)) | Op2 (The, T, R, u1, u2) => if is_opt_rep R then let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in @@ -1358,8 +1470,8 @@ if f1 = f2 then atom_from_formula kk j0 f1 else - kk_union (kk_rel_if f1 true_atom Kodkod.None) - (kk_rel_if f2 Kodkod.None false_atom) + kk_union (kk_rel_if f1 true_atom KK.None) + (kk_rel_if f2 KK.None false_atom) end | Op2 (Union, _, R, u1, u2) => to_set_op kk_or kk_or3 kk_union kk_union kk_intersect false R u1 u2 @@ -1391,7 +1503,7 @@ | Opt (Atom (2, _)) => let (* FIXME: merge with similar code above *) - (* rep -> rep -> nut -> Kodkod.rel_expr *) + (* rep -> rep -> nut -> KK.rel_expr *) fun must R1 R2 u = kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom fun may R1 R2 u = @@ -1426,9 +1538,9 @@ (to_rep (Func (b_R, Formula Neut)) u2) | Opt (Atom (2, _)) => let - (* Kodkod.rel_expr -> rep -> nut -> Kodkod.rel_expr *) + (* KK.rel_expr -> rep -> nut -> KK.rel_expr *) fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r - (* Kodkod.rel_expr -> Kodkod.rel_expr *) + (* KK.rel_expr -> KK.rel_expr *) fun do_term r = kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r in kk_union (do_term true_atom) (do_term false_atom) end @@ -1440,7 +1552,7 @@ (Func (R11, R12), Func (R21, Formula Neut)) => if R21 = R11 andalso is_lone_rep R12 then let - (* Kodkod.rel_expr -> Kodkod.rel_expr *) + (* KK.rel_expr -> KK.rel_expr *) fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1) val core_r = big_join (to_r u2) val core_R = Func (R12, Formula Neut) @@ -1466,9 +1578,9 @@ | Op2 (Apply, @{typ nat}, _, Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) => if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then - Kodkod.Atom (offset_of_type ofs nat_T) + KK.Atom (offset_of_type ofs nat_T) else - fold kk_join [to_integer u1, to_integer u2] nat_subtract_rel + fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel) | Op2 (Apply, _, R, u1, u2) => if is_Cst Unrep u2 andalso is_set_type (type_of u1) andalso is_FreeName u1 then @@ -1476,7 +1588,7 @@ else to_apply R u1 u2 | Op2 (Lambda, T, R as Opt (Atom (1, j0)), u1, u2) => - to_guard [u1, u2] R (Kodkod.Atom j0) + to_guard [u1, u2] R (KK.Atom j0) | Op2 (Lambda, T, Func (_, Formula Neut), u1, u2) => kk_comprehension (untuple to_decl u1) (to_f u2) | Op2 (Lambda, T, Func (_, R2), u1, u2) => @@ -1494,7 +1606,7 @@ kk_rel_let [to_expr_assign u1 u2] (to_rep R u3) | Op3 (If, _, R, u1, u2, u3) => if is_opt_rep (rep_of u1) then - triple_rel_let kk + tripl_rel_rel_let kk (fn r1 => fn r2 => fn r3 => let val empty_r = empty_rel_for_rep R in fold1 kk_union @@ -1512,10 +1624,9 @@ | Vect (k, R) => to_product (replicate k R) us | Atom (1, j0) => (case filter (not_equal Unit o rep_of) us of - [] => Kodkod.Atom j0 - | us' => - kk_rel_if (kk_some (fold1 kk_product (map to_r us'))) - (Kodkod.Atom j0) Kodkod.None) + [] => KK.Atom j0 + | us' => kk_rel_if (kk_some (fold1 kk_product (map to_r us'))) + (KK.Atom j0) KK.None) | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u])) | Construct ([u'], _, _, []) => to_r u' | Construct (_ :: sel_us, T, R, arg_us) => @@ -1533,47 +1644,46 @@ else kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R1)) - (kk_rel_eq (kk_join (Kodkod.Var (1, ~1)) sel_r) - arg_r) + (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r) end) sel_us arg_us in fold1 kk_intersect set_rs end - | BoundRel (x, _, _, _) => Kodkod.Var x - | FreeRel (x, _, _, _) => Kodkod.Rel x - | RelReg (j, _, R) => Kodkod.RelReg (arity_of_rep R, j) + | BoundRel (x, _, _, _) => KK.Var x + | FreeRel (x, _, _, _) => KK.Rel x + | RelReg (j, _, R) => KK.RelReg (arity_of_rep R, j) | u => raise NUT ("Nitpick_Kodkod.to_r", [u]) - (* nut -> Kodkod.decl *) + (* nut -> KK.decl *) and to_decl (BoundRel (x, _, R, _)) = - Kodkod.DeclOne (x, Kodkod.AtomSeq (the_single (atom_schema_of_rep R))) + KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R))) | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u]) - (* nut -> Kodkod.expr_assign *) + (* nut -> KK.expr_assign *) and to_expr_assign (FormulaReg (j, _, R)) u = - Kodkod.AssignFormulaReg (j, to_f u) + KK.AssignFormulaReg (j, to_f u) | to_expr_assign (RelReg (j, _, R)) u = - Kodkod.AssignRelReg ((arity_of_rep R, j), to_r u) + KK.AssignRelReg ((arity_of_rep R, j), to_r u) | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1]) - (* int * int -> nut -> Kodkod.rel_expr *) + (* int * int -> nut -> KK.rel_expr *) and to_atom (x as (k, j0)) u = case rep_of u of Formula _ => atom_from_formula kk j0 (to_f u) - | Unit => if k = 1 then Kodkod.Atom j0 + | Unit => if k = 1 then KK.Atom j0 else raise NUT ("Nitpick_Kodkod.to_atom", [u]) | R => atom_from_rel_expr kk x R (to_r u) - (* rep list -> nut -> Kodkod.rel_expr *) + (* rep list -> nut -> KK.rel_expr *) and to_struct Rs u = case rep_of u of Unit => full_rel_for_rep (Struct Rs) | R' => struct_from_rel_expr kk Rs R' (to_r u) - (* int -> rep -> nut -> Kodkod.rel_expr *) + (* int -> rep -> nut -> KK.rel_expr *) and to_vect k R u = case rep_of u of Unit => full_rel_for_rep (Vect (k, R)) | R' => vect_from_rel_expr kk k R R' (to_r u) - (* rep -> rep -> nut -> Kodkod.rel_expr *) + (* rep -> rep -> nut -> KK.rel_expr *) and to_func R1 R2 u = case rep_of u of Unit => full_rel_for_rep (Func (R1, R2)) | R' => rel_expr_to_func kk R1 R2 R' (to_r u) - (* rep -> nut -> Kodkod.rel_expr *) + (* rep -> nut -> KK.rel_expr *) and to_opt R u = let val old_R = rep_of u in if is_opt_rep old_R then @@ -1581,16 +1691,16 @@ else to_rep R u end - (* rep -> nut -> Kodkod.rel_expr *) + (* rep -> nut -> KK.rel_expr *) and to_rep (Atom x) u = to_atom x u | to_rep (Struct Rs) u = to_struct Rs u | to_rep (Vect (k, R)) u = to_vect k R u | to_rep (Func (R1, R2)) u = to_func R1 R2 u | to_rep (Opt R) u = to_opt R u | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R]) - (* nut -> Kodkod.rel_expr *) + (* nut -> KK.rel_expr *) and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u - (* nut list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) + (* nut list -> rep -> KK.rel_expr -> KK.rel_expr *) and to_guard guard_us R r = let val unpacked_rs = unpack_joins r @@ -1610,16 +1720,16 @@ else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r end - (* rep -> rep -> Kodkod.rel_expr -> int -> Kodkod.rel_expr *) + (* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *) and to_project new_R old_R r j0 = rel_expr_from_rel_expr kk new_R old_R (kk_project_seq r j0 (arity_of_rep old_R)) - (* rep list -> nut list -> Kodkod.rel_expr *) + (* rep list -> nut list -> KK.rel_expr *) and to_product Rs us = case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of [] => raise REP ("Nitpick_Kodkod.to_product", Rs) | rs => fold1 kk_product rs - (* int -> typ -> rep -> nut -> Kodkod.rel_expr *) + (* int -> typ -> rep -> nut -> KK.rel_expr *) and to_nth_pair_sel n res_T res_R u = case u of Tuple (_, _, us) => to_rep res_R (nth us n) @@ -1647,9 +1757,9 @@ (to_rep res_R (Cst (Unity, res_T, Unit))) | arity => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0 end - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) -> nut -> nut - -> Kodkod.formula *) + (* (KK.formula -> KK.formula -> KK.formula) + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> nut -> nut + -> KK.formula *) and to_set_bool_op connective set_oper u1 u2 = let val min_R = min_rep (rep_of u1) (rep_of u2) @@ -1665,12 +1775,12 @@ (kk_join r2 true_atom) | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R]) end - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) -> bool -> rep - -> nut -> nut -> Kodkod.rel_expr *) + (* (KK.formula -> KK.formula -> KK.formula) + -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr) + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> bool -> rep -> nut + -> nut -> KK.rel_expr *) and to_set_op connective connective3 set_oper true_set_oper false_set_oper neg_second R u1 u2 = let @@ -1686,7 +1796,7 @@ | Func (_, Formula Neut) => set_oper r1 r2 | Func (Unit, _) => connective3 r1 r2 | Func (R1, _) => - double_rel_let kk + double_rel_rel_let kk (fn r1 => fn r2 => kk_union (kk_product @@ -1702,14 +1812,47 @@ r1 r2 | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R])) end - (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *) + (* typ -> rep -> (KK.int_expr -> KK.int_expr) -> KK.rel_expr *) + and to_bit_word_unary_op T R oper = + let + val Ts = strip_type T ||> single |> op @ + (* int -> KK.int_expr *) + fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j)) + in + kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R)) + (KK.FormulaLet + (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 1), + KK.IntEq (KK.IntReg 1, oper (KK.IntReg 0)))) + end + (* typ -> rep -> (KK.int_expr -> KK.int_expr -> KK.int_expr -> bool) option + -> (KK.int_expr -> KK.int_expr -> KK.int_expr) option -> KK.rel_expr *) + and to_bit_word_binary_op T R opt_guard opt_oper = + let + val Ts = strip_type T ||> single |> op @ + (* int -> KK.int_expr *) + fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j)) + in + kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R)) + (KK.FormulaLet + (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 2), + fold1 kk_and + ((case opt_guard of + NONE => [] + | SOME guard => + [guard (KK.IntReg 0) (KK.IntReg 1) (KK.IntReg 2)]) @ + (case opt_oper of + NONE => [] + | SOME oper => + [KK.IntEq (KK.IntReg 2, + oper (KK.IntReg 0) (KK.IntReg 1))])))) + end + (* rep -> rep -> KK.rel_expr -> nut -> KK.rel_expr *) and to_apply res_R func_u arg_u = case unopt_rep (rep_of func_u) of Unit => let val j0 = offset_of_type ofs (type_of func_u) in to_guard [arg_u] res_R - (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) - (Kodkod.Atom j0)) + (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0)) end | Atom (1, j0) => to_guard [arg_u] res_R @@ -1738,7 +1881,7 @@ (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u)) |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u]) - (* int -> rep -> rep -> Kodkod.rel_expr -> nut *) + (* int -> rep -> rep -> KK.rel_expr -> nut *) and to_apply_vect k R' res_R func_r arg_u = let val arg_R = one_rep ofs (type_of arg_u) (unopt_rep (rep_of arg_u)) @@ -1748,11 +1891,10 @@ kk_case_switch kk arg_R res_R (to_opt arg_R arg_u) (all_singletons_for_rep arg_R) vect_rs end - (* bool -> nut -> Kodkod.formula *) + (* bool -> nut -> KK.formula *) and to_could_be_unrep neg u = - if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u) - else Kodkod.False - (* nut -> Kodkod.rel_expr -> Kodkod.rel_expr *) + if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u) else KK.False + (* nut -> KK.rel_expr -> KK.rel_expr *) and to_compare_with_unrep u r = if is_opt_rep (rep_of u) then kk_rel_if (kk_some (to_r u)) r (empty_rel_for_rep (rep_of u)) diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Dec 18 12:00:44 2009 +0100 @@ -40,6 +40,8 @@ open Nitpick_Rep open Nitpick_Nut +structure KK = Kodkod + type params = { show_skolems: bool, show_datatypes: bool, @@ -60,7 +62,7 @@ ? prefix "\<^isub>," (* string -> typ -> int -> string *) fun atom_name prefix (T as Type (s, _)) j = - prefix ^ substring (short_name s, 0, 1) ^ atom_suffix s j + prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j | atom_name prefix (T as TFree (s, _)) j = prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], []) @@ -71,24 +73,43 @@ else Const (atom_name "" T j, T) -(* nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list *) +(* term -> real *) +fun extract_real_number (Const (@{const_name HOL.divide}, _) $ t1 $ t2) = + real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2)) + | extract_real_number t = real (snd (HOLogic.dest_number t)) +(* term * term -> order *) +fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2) + | nice_term_ord tp = Real.compare (pairself extract_real_number tp) + handle TERM ("dest_number", _) => + case tp of + (t11 $ t12, t21 $ t22) => + (case nice_term_ord (t11, t21) of + EQUAL => nice_term_ord (t12, t22) + | ord => ord) + | _ => TermOrd.fast_term_ord tp + +(* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *) fun tuple_list_for_name rel_table bounds name = the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] (* term -> term *) -fun unbox_term (Const (@{const_name FunBox}, _) $ t1) = unbox_term t1 - | unbox_term (Const (@{const_name PairBox}, - Type ("fun", [T1, Type ("fun", [T2, T3])])) $ t1 $ t2) = - let val Ts = map unbox_type [T1, T2] in +fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) = + unbit_and_unbox_term t1 + | unbit_and_unbox_term (Const (@{const_name PairBox}, + Type ("fun", [T1, Type ("fun", [T2, T3])])) + $ t1 $ t2) = + let val Ts = map unbit_and_unbox_type [T1, T2] in Const (@{const_name Pair}, Ts ---> Type ("*", Ts)) - $ unbox_term t1 $ unbox_term t2 + $ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2 end - | unbox_term (Const (s, T)) = Const (s, unbox_type T) - | unbox_term (t1 $ t2) = unbox_term t1 $ unbox_term t2 - | unbox_term (Free (s, T)) = Free (s, unbox_type T) - | unbox_term (Var (x, T)) = Var (x, unbox_type T) - | unbox_term (Bound j) = Bound j - | unbox_term (Abs (s, T, t')) = Abs (s, unbox_type T, unbox_term t') + | unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T) + | unbit_and_unbox_term (t1 $ t2) = + unbit_and_unbox_term t1 $ unbit_and_unbox_term t2 + | unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T) + | unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T) + | unbit_and_unbox_term (Bound j) = Bound j + | unbit_and_unbox_term (Abs (s, T, t')) = + Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t') (* typ -> typ -> (typ * typ) * (typ * typ) *) fun factor_out_types (T1 as Type ("*", [T11, T12])) @@ -121,11 +142,12 @@ Const (if maybe_opt orelse T2 <> bool_T then @{const_name undefined} else non_opt_name, T1 --> T2) | aux T1 T2 ((t1, t2) :: ps) = - Const (@{const_name fun_upd}, [T1 --> T2, T1, T2] ---> T1 --> T2) + Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ aux T1 T2 ps $ t1 $ t2 in aux T1 T2 o rev end (* term -> bool *) -fun is_plain_fun (Const (s, _)) = s mem [@{const_name undefined}, non_opt_name] +fun is_plain_fun (Const (s, _)) = + (s = @{const_name undefined} orelse s = non_opt_name) | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) = is_plain_fun t0 | is_plain_fun _ = false @@ -185,7 +207,7 @@ | do_arrow T1' T2' T1 T2 (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = Const (@{const_name fun_upd}, - [T1' --> T2', T1', T2'] ---> T1' --> T2') + (T1' --> T2') --> T1' --> T2' --> T1' --> T2') $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2 | do_arrow _ _ _ _ t = raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t]) @@ -220,24 +242,34 @@ HOLogic.mk_prod (mk_tuple T1 ts, mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1)))) | mk_tuple _ (t :: _) = t + | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], []) (* string * string * string * string -> scope -> nut list -> nut list - -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> typ -> typ - -> rep -> int list list -> term *) + -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep + -> int list list -> term *) fun reconstruct_term (maybe_name, base_name, step_name, abs_name) - ({ext_ctxt as {thy, ctxt, ...}, card_assigns, datatypes, ofs, ...} + ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...} : scope) sel_names rel_table bounds = let val for_auto = (maybe_name = "") + (* int list list -> int *) + fun value_of_bits jss = + let + val j0 = offset_of_type ofs @{typ unsigned_bit} + val js = map (Integer.add (~ j0) o the_single) jss + in + fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~)) + js 0 + end (* bool -> typ -> typ -> (term * term) list -> term *) fun make_set maybe_opt T1 T2 = let val empty_const = Const (@{const_name Set.empty}, T1 --> T2) val insert_const = Const (@{const_name insert}, - [T1, T1 --> T2] ---> T1 --> T2) + T1 --> (T1 --> T2) --> T1 --> T2) (* (term * term) list -> term *) fun aux [] = - if maybe_opt andalso not (is_precise_type datatypes T1) then + if maybe_opt andalso not (is_complete_type datatypes T1) then insert_const $ Const (unrep, T1) $ empty_const else empty_const @@ -253,7 +285,7 @@ fun make_map T1 T2 T2' = let val update_const = Const (@{const_name fun_upd}, - [T1 --> T2, T1, T2] ---> T1 --> T2) + (T1 --> T2) --> T1 --> T2 --> T1 --> T2) (* (term * term) list -> term *) fun aux' [] = Const (@{const_name Map.empty}, T1 --> T2) | aux' ((t1, t2) :: ps) = @@ -261,7 +293,7 @@ Const (@{const_name None}, _) => aux' ps | _ => update_const $ aux' ps $ t1 $ t2) fun aux ps = - if not (is_precise_type datatypes T1) then + if not (is_complete_type datatypes T1) then update_const $ aux' ps $ Const (unrep, T1) $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2')) else @@ -297,10 +329,12 @@ | _ => t (* bool -> typ -> typ -> typ -> term list -> term list -> term *) fun make_fun maybe_opt T1 T2 T' ts1 ts2 = - ts1 ~~ ts2 |> T1 = @{typ bisim_iterator} ? rev + ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst) |> make_plain_fun (maybe_opt andalso not for_auto) T1 T2 - |> unbox_term - |> typecast_fun (unbox_type T') (unbox_type T1) (unbox_type T2) + |> unbit_and_unbox_term + |> typecast_fun (unbit_and_unbox_type T') + (unbit_and_unbox_type T1) + (unbit_and_unbox_type T2) (* (typ * int) list -> typ -> typ -> int -> term *) fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j = let @@ -350,7 +384,8 @@ val real_j = j + offset_of_type ofs T val constr_x as (constr_s, constr_T) = get_first (fn (jss, {const, ...}) => - if [real_j] mem jss then SOME const else NONE) + if member (op =) jss [real_j] then SOME const + else NONE) (discr_jsss ~~ constrs) |> the val arg_Ts = curried_binder_types constr_T val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x) @@ -369,8 +404,12 @@ else NONE)) sel_jsss val uncur_arg_Ts = binder_types constr_T in - if co andalso (T, j) mem seen then + if co andalso member (op =) seen (T, j) then Var (var ()) + else if constr_s = @{const_name Word} then + HOLogic.mk_number + (if T = @{typ "unsigned_bit word"} then nat_T else int_T) + (value_of_bits (the_single arg_jsss)) else let val seen = seen |> co ? cons (T, j) @@ -396,7 +435,7 @@ | n1 => case HOLogic.dest_number t2 |> snd of 1 => mk_num n1 | n2 => Const (@{const_name HOL.divide}, - [num_T, num_T] ---> num_T) + num_T --> num_T --> num_T) $ mk_num n1 $ mk_num n2) | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\ \for_atom (Abs_Frac)", ts) @@ -408,10 +447,10 @@ in if co then let val var = var () in - if exists_subterm (equal (Var var)) t then + if exists_subterm (curry (op =) (Var var)) t then Const (@{const_name The}, (T --> bool_T) --> T) $ Abs ("\", T, - Const (@{const_name "op ="}, [T, T] ---> bool_T) + Const (@{const_name "op ="}, T --> T --> bool_T) $ Bound 0 $ abstract_over (Var var, t)) else t @@ -449,7 +488,8 @@ val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1 val ts2 = map (fn js => term_for_rep seen T2 T2 (Atom (2, 0)) - [[int_for_bool (js mem jss)]]) jss1 + [[int_for_bool (member (op =) jss js)]]) + jss1 in make_fun false T1 T2 T' ts1 ts2 end | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss = let @@ -467,10 +507,11 @@ Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^ string_of_int (length jss)) in - (not for_auto ? setify_mapify_funs []) o unbox_term oooo term_for_rep [] + (not for_auto ? setify_mapify_funs []) o unbit_and_unbox_term + oooo term_for_rep [] end -(* scope -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> nut +(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut -> term *) fun term_for_name scope sel_names rel_table bounds name = let val T = type_of name in @@ -517,7 +558,7 @@ let val ((head1, args1), (head2, args2)) = pairself (strip_comb o unfold_outer_the_binders) (t1, t2) - val max_depth = max_depth - (if T mem coTs then 1 else 0) + val max_depth = max_depth - (if member (op =) coTs T then 1 else 0) in head1 = head2 andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2) @@ -527,28 +568,29 @@ end (* params -> scope -> (term option * int list) list -> styp list -> nut list - -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list + -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> Pretty.T * bool *) fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts} - ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, user_axioms, debug, - wfs, destroy_constrs, specialize, skolemize, - star_linear_preds, uncurry, fast_descrs, tac_timeout, - evals, case_names, def_table, nondef_table, user_nondefs, - simp_table, psimp_table, intro_table, ground_thm_table, - ersatz_table, skolems, special_funs, unrolled_preds, - wf_cache, constr_cache}, - card_assigns, bisim_depth, datatypes, ofs} : scope) formats all_frees - free_names sel_names nonsel_names rel_table bounds = + ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms, + debug, binary_ints, destroy_constrs, specialize, + skolemize, star_linear_preds, uncurry, fast_descrs, + tac_timeout, evals, case_names, def_table, nondef_table, + user_nondefs, simp_table, psimp_table, intro_table, + ground_thm_table, ersatz_table, skolems, special_funs, + unrolled_preds, wf_cache, constr_cache}, + card_assigns, bits, bisim_depth, datatypes, ofs} : scope) + formats all_frees free_names sel_names nonsel_names rel_table bounds = let val (wacky_names as (_, base_name, step_name, _), ctxt) = add_wacky_syntax ctxt val ext_ctxt = {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, wfs = wfs, user_axioms = user_axioms, debug = debug, - destroy_constrs = destroy_constrs, specialize = specialize, - skolemize = skolemize, star_linear_preds = star_linear_preds, - uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout, - evals = evals, case_names = case_names, def_table = def_table, + binary_ints = binary_ints, destroy_constrs = destroy_constrs, + specialize = specialize, skolemize = skolemize, + star_linear_preds = star_linear_preds, uncurry = uncurry, + fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, + case_names = case_names, def_table = def_table, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_table, intro_table = intro_table, ground_thm_table = ground_thm_table, @@ -556,17 +598,21 @@ special_funs = special_funs, unrolled_preds = unrolled_preds, wf_cache = wf_cache, constr_cache = constr_cache} val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns, - bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs} + bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, + ofs = ofs} (* typ -> typ -> rep -> int list list -> term *) val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table bounds - (* typ -> typ -> typ *) - fun nth_value_of_type T card n = term_for_rep T T (Atom (card, 0)) [[n]] + (* nat -> typ -> nat -> typ *) + fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]] + (* nat -> typ -> typ list *) + fun all_values_of_type card T = + index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord (* dtype_spec list -> dtype_spec -> bool *) fun is_codatatype_wellformed (cos : dtype_spec list) ({typ, card, ...} : dtype_spec) = let - val ts = map (nth_value_of_type typ card) (index_seq 0 card) + val ts = all_values_of_type card typ val max_depth = Integer.sum (map #card cos) in forall (not o bisimilar_values (map #typ cos) max_depth) @@ -578,7 +624,7 @@ val (oper, (t1, T'), T) = case name of FreeName (s, T, _) => - let val t = Free (s, unbox_type T) in + let val t = Free (s, unbit_and_unbox_type T) in ("=", (t, format_term_type thy def_table formats t), T) end | ConstName (s, T, _) => @@ -598,17 +644,16 @@ Pretty.str oper, Syntax.pretty_term ctxt t2]) end (* dtype_spec -> Pretty.T *) - fun pretty_for_datatype ({typ, card, precise, ...} : dtype_spec) = + fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) = Pretty.block (Pretty.breaks - [Syntax.pretty_typ ctxt (unbox_type typ), Pretty.str "=", + [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=", Pretty.enum "," "{" "}" - (map (Syntax.pretty_term ctxt o nth_value_of_type typ card) - (index_seq 0 card) @ - (if precise then [] else [Pretty.str unrep]))]) + (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) + @ (if complete then [] else [Pretty.str unrep]))]) (* typ -> dtype_spec list *) fun integer_datatype T = [{typ = T, card = card_of_type card_assigns T, co = false, - precise = false, shallow = false, constrs = []}] + complete = false, concrete = true, shallow = false, constrs = []}] handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] val (codatatypes, datatypes) = datatypes |> filter_out #shallow @@ -639,10 +684,12 @@ val (eval_names, noneval_nonskolem_nonsel_names) = List.partition (String.isPrefix eval_prefix o nickname_of) nonskolem_nonsel_names - ||> filter_out (equal @{const_name bisim_iterator_max} o nickname_of) + ||> filter_out (curry (op =) @{const_name bisim_iterator_max} + o nickname_of) val free_names = map (fn x as (s, T) => - case filter (equal x o pairf nickname_of (unbox_type o type_of)) + case filter (curry (op =) x + o pairf nickname_of (unbit_and_unbox_type o type_of)) free_names of [name] => name | [] => FreeName (s, T, Any) @@ -662,7 +709,7 @@ end (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table - -> Kodkod.raw_bound list -> term -> bool option *) + -> KK.raw_bound list -> term -> bool option *) fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, ...}) auto_timeout free_names sel_names rel_table bounds prop = let diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Dec 18 12:00:44 2009 +0100 @@ -101,7 +101,7 @@ string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2 | CPair (C1, C2) => aux (prec + 1) C1 ^ " \ " ^ aux prec C2 | CType (s, []) => - if s mem [@{type_name prop}, @{type_name bool}] then "o" else s + if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s | CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s | CRec (s, _) => "[" ^ s ^ "]") ^ (if need_parens then ")" else "") @@ -125,9 +125,10 @@ andalso exists (could_exist_alpha_subtype alpha_T) Ts) | could_exist_alpha_subtype alpha_T T = (T = alpha_T) (* theory -> typ -> typ -> bool *) -fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) = - could_exist_alpha_subtype alpha_T - | could_exist_alpha_sub_ctype thy alpha_T = equal alpha_T orf is_datatype thy +fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T = + could_exist_alpha_subtype alpha_T T + | could_exist_alpha_sub_ctype thy alpha_T T = + (T = alpha_T orelse is_datatype thy T) (* ctype -> bool *) fun exists_alpha_sub_ctype CAlpha = true @@ -164,7 +165,7 @@ | repair_ctype cache seen (CRec (z as (s, _))) = case AList.lookup (op =) cache z |> the of CRec _ => CType (s, []) - | C => if C mem seen then CType (s, []) + | C => if member (op =) seen C then CType (s, []) else repair_ctype cache (C :: seen) C (* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *) @@ -465,11 +466,11 @@ PropLogic.SOr (prop_for_exists_eq xs Neg, prop_for_comp (a1, a2, cmp, [])) (* var -> (int -> bool option) -> literal list -> literal list *) -fun literals_from_assignments max_var asgns lits = +fun literals_from_assignments max_var assigns lits = fold (fn x => fn accum => if AList.defined (op =) lits x then accum - else case asgns x of + else case assigns x of SOME b => (x, sign_from_bool b) :: accum | NONE => accum) (max_var downto 1) lits @@ -490,7 +491,7 @@ (* literal list -> unit *) fun print_solution lits = - let val (pos, neg) = List.partition (equal Pos o snd) lits in + let val (pos, neg) = List.partition (curry (op =) Pos o snd) lits in print_g ("*** Solution:\n" ^ "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^ "-: " ^ commas (map (string_for_var o fst) neg)) @@ -504,10 +505,13 @@ val prop = PropLogic.all (map prop_for_literal lits @ map prop_for_comp comps @ map prop_for_sign_expr sexps) + (* use the first ML solver (to avoid startup overhead) *) + val solvers = !SatSolver.solvers + |> filter (member (op =) ["dptsat", "dpll"] o fst) in - case SatSolver.invoke_solver "dpll" prop of - SatSolver.SATISFIABLE asgns => - SOME (literals_from_assignments max_var asgns lits + case snd (hd solvers) prop of + SatSolver.SATISFIABLE assigns => + SOME (literals_from_assignments max_var assigns lits |> tap print_solution) | _ => NONE end diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Dec 18 12:00:44 2009 +0100 @@ -26,7 +26,6 @@ Subtract | Multiply | Divide | - Modulo | Gcd | Lcm | Fracs | @@ -131,6 +130,8 @@ open Nitpick_Peephole open Nitpick_Rep +structure KK = Kodkod + datatype cst = Unity | False | @@ -144,7 +145,6 @@ Subtract | Multiply | Divide | - Modulo | Gcd | Lcm | Fracs | @@ -198,8 +198,8 @@ BoundName of int * typ * rep * string | FreeName of string * typ * rep | ConstName of string * typ * rep | - BoundRel of Kodkod.n_ary_index * typ * rep * string | - FreeRel of Kodkod.n_ary_index * typ * rep * string | + BoundRel of KK.n_ary_index * typ * rep * string | + FreeRel of KK.n_ary_index * typ * rep * string | RelReg of int * typ * rep | FormulaReg of int * typ * rep @@ -218,7 +218,6 @@ | string_for_cst Subtract = "Subtract" | string_for_cst Multiply = "Multiply" | string_for_cst Divide = "Divide" - | string_for_cst Modulo = "Modulo" | string_for_cst Gcd = "Gcd" | string_for_cst Lcm = "Lcm" | string_for_cst Fracs = "Fracs" @@ -442,7 +441,7 @@ case NameTable.lookup table name of SOME u => u | NONE => raise NUT ("Nitpick_Nut.the_name", [name]) -(* nut NameTable.table -> nut -> Kodkod.n_ary_index *) +(* nut NameTable.table -> nut -> KK.n_ary_index *) fun the_rel table name = case the_name table name of FreeRel (x, _, _, _) => x @@ -614,8 +613,6 @@ Cst (Multiply, T, Any) | (Const (@{const_name div_nat_inst.div_nat}, T), []) => Cst (Divide, T, Any) - | (Const (@{const_name div_nat_inst.mod_nat}, T), []) => - Cst (Modulo, T, Any) | (Const (@{const_name ord_nat_inst.less_nat}, T), [t1, t2]) => Op2 (Less, bool_T, Any, sub t1, sub t2) | (Const (@{const_name ord_nat_inst.less_eq_nat}, T), [t1, t2]) => @@ -634,12 +631,12 @@ Cst (Multiply, T, Any) | (Const (@{const_name div_int_inst.div_int}, T), []) => Cst (Divide, T, Any) - | (Const (@{const_name div_int_inst.mod_int}, T), []) => - Cst (Modulo, T, Any) | (Const (@{const_name uminus_int_inst.uminus_int}, T), []) => - Op2 (Apply, int_T --> int_T, Any, - Cst (Subtract, [int_T, int_T] ---> int_T, Any), - Cst (Num 0, int_T, Any)) + let val num_T = domain_type T in + Op2 (Apply, num_T --> num_T, Any, + Cst (Subtract, num_T --> num_T --> num_T, Any), + Cst (Num 0, num_T, Any)) + end | (Const (@{const_name ord_int_inst.less_int}, T), [t1, t2]) => Op2 (Less, bool_T, Any, sub t1, sub t2) | (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) => @@ -650,6 +647,9 @@ | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any) | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) => Cst (NatToInt, T, Any) + | (Const (@{const_name of_nat}, + T as @{typ "unsigned_bit word => signed_bit word"}), []) => + Cst (NatToInt, T, Any) | (Const (@{const_name lower_semilattice_fun_inst.inf_fun}, T), [t1, t2]) => Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2) @@ -708,24 +708,24 @@ (* scope -> bool -> nut -> nut list * rep NameTable.table -> nut list * rep NameTable.table *) fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes, - ofs, ...}) all_precise v (vs, table) = + ofs, ...}) all_exact v (vs, table) = let val x as (s, T) = (nickname_of v, type_of v) val R = (if is_abs_fun thy x then rep_for_abs_fun else if is_rep_fun thy x then Func oo best_non_opt_symmetric_reps_for_fun_type - else if all_precise orelse is_skolem_name v - orelse original_name s - mem [@{const_name undefined_fast_The}, - @{const_name undefined_fast_Eps}, - @{const_name bisim}, - @{const_name bisim_iterator_max}] then + else if all_exact orelse is_skolem_name v + orelse member (op =) [@{const_name undefined_fast_The}, + @{const_name undefined_fast_Eps}, + @{const_name bisim}, + @{const_name bisim_iterator_max}] + (original_name s) then best_non_opt_set_rep_for_type - else if original_name s - mem [@{const_name set}, @{const_name distinct}, - @{const_name ord_class.less}, - @{const_name ord_class.less_eq}] then + else if member (op =) [@{const_name set}, @{const_name distinct}, + @{const_name ord_class.less}, + @{const_name ord_class.less_eq}] + (original_name s) then best_set_rep_for_type else best_opt_set_rep_for_type) scope T @@ -737,17 +737,19 @@ fold (choose_rep_for_free_var scope) vs ([], table) (* scope -> bool -> nut list -> rep NameTable.table -> nut list * rep NameTable.table *) -fun choose_reps_for_consts scope all_precise vs table = - fold (choose_rep_for_const scope all_precise) vs ([], table) +fun choose_reps_for_consts scope all_exact vs table = + fold (choose_rep_for_const scope all_exact) vs ([], table) (* scope -> styp -> int -> nut list * rep NameTable.table -> nut list * rep NameTable.table *) -fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) x n +fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n (vs, table) = let val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n - val R' = if n = ~1 then best_non_opt_set_rep_for_type scope T' - else best_opt_set_rep_for_type scope T' |> unopt_rep + val R' = if n = ~1 orelse is_word_type (body_type T) then + best_non_opt_set_rep_for_type scope T' + else + best_opt_set_rep_for_type scope T' |> unopt_rep val v = ConstName (s', T', R') in (v :: vs, NameTable.update (v, R') table) end (* scope -> styp -> nut list * rep NameTable.table @@ -780,7 +782,8 @@ (not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse case u of Cst (Num _, _, _) => true - | Cst (cst, T, _) => cst = Suc orelse (body_type T = nat_T andalso cst = Add) + | Cst (cst, T, _) => + cst = Suc orelse (body_type T = nat_T andalso cst = Add) | Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2] | Op3 (If, _, _, u1, u2, u3) => not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3] @@ -883,7 +886,8 @@ (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *) fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, - datatypes, ofs, ...}) liberal table def = + bits, datatypes, ofs, ...}) + liberal table def = let val bool_atom_R = Atom (2, offset_of_type ofs bool_T) (* polarity -> bool -> rep *) @@ -912,17 +916,21 @@ Cst (False, T, _) => Cst (False, T, Formula Neut) | Cst (True, T, _) => Cst (True, T, Formula Neut) | Cst (Num j, T, _) => - (case spec_of_type scope T of - (1, j0) => if j = 0 then Cst (Unity, T, Unit) - else Cst (Unrep, T, Opt (Atom (1, j0))) - | (k, j0) => - let - val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1 - else j < k) - in - if ok then Cst (Num j, T, Atom (k, j0)) - else Cst (Unrep, T, Opt (Atom (k, j0))) - end) + if is_word_type T then + Cst (if is_twos_complement_representable bits j then Num j + else Unrep, T, best_opt_set_rep_for_type scope T) + else + (case spec_of_type scope T of + (1, j0) => if j = 0 then Cst (Unity, T, Unit) + else Cst (Unrep, T, Opt (Atom (1, j0))) + | (k, j0) => + let + val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1 + else j < k) + in + if ok then Cst (Num j, T, Atom (k, j0)) + else Cst (Unrep, T, Opt (Atom (k, j0))) + end) | Cst (Suc, T as Type ("fun", [T1, _]), _) => let val R = Atom (spec_of_type scope T1) in Cst (Suc, T, Func (R, Opt R)) @@ -934,35 +942,32 @@ Cst (NormFrac, T, Func (R1, Func (R1, Opt (Struct [R1, R1])))) end | Cst (cst, T, _) => - if cst mem [Unknown, Unrep] then + if cst = Unknown orelse cst = Unrep then case (is_boolean_type T, polar) of (true, Pos) => Cst (False, T, Formula Pos) | (true, Neg) => Cst (True, T, Formula Neg) | _ => Cst (cst, T, best_opt_set_rep_for_type scope T) - else if cst mem [Add, Subtract, Multiply, Divide, Modulo, Gcd, - Lcm] then + else if member (op =) [Add, Subtract, Multiply, Divide, Gcd, Lcm] + cst then let val T1 = domain_type T val R1 = Atom (spec_of_type scope T1) - val total = - T1 = nat_T andalso cst mem [Subtract, Divide, Modulo, Gcd] + val total = T1 = nat_T + andalso (cst = Subtract orelse cst = Divide + orelse cst = Gcd) in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end - else if cst mem [NatToInt, IntToNat] then + else if cst = NatToInt orelse cst = IntToNat then let - val (nat_card, nat_j0) = spec_of_type scope nat_T - val (int_card, int_j0) = spec_of_type scope int_T + val (dom_card, dom_j0) = spec_of_type scope (domain_type T) + val (ran_card, ran_j0) = spec_of_type scope (range_type T) + val total = not (is_word_type (domain_type T)) + andalso (if cst = NatToInt then + max_int_for_card ran_card >= dom_card + 1 + else + max_int_for_card dom_card < ran_card) in - if cst = NatToInt then - let val total = (max_int_for_card int_card >= nat_card + 1) in - Cst (cst, T, - Func (Atom (nat_card, nat_j0), - (not total ? Opt) (Atom (int_card, int_j0)))) - end - else - let val total = (max_int_for_card int_card < nat_card) in - Cst (cst, T, Func (Atom (int_card, int_j0), - Atom (nat_card, nat_j0)) |> not total ? Opt) - end + Cst (cst, T, Func (Atom (dom_card, dom_j0), + Atom (ran_card, ran_j0) |> not total ? Opt)) end else Cst (cst, T, best_set_rep_for_type scope T) @@ -997,7 +1002,7 @@ if is_opt_rep R then triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2) else if opt andalso polar = Pos andalso - not (is_fully_comparable_type datatypes (type_of u1)) then + not (is_concrete_type datatypes (type_of u1)) then Cst (False, T, Formula Pos) else s_op2 Subset T R u1 u2 @@ -1023,7 +1028,7 @@ else opt_opt_case () in if liberal orelse polar = Neg - orelse is_fully_comparable_type datatypes (type_of u1) then + orelse is_concrete_type datatypes (type_of u1) then case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of (true, true) => opt_opt_case () | (true, false) => hybrid_case u1' @@ -1113,7 +1118,7 @@ in s_op2 Lambda T R u1' u2' end | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u])) | Op2 (oper, T, _, u1, u2) => - if oper mem [All, Exist] then + if oper = All orelse oper = Exist then let val table' = fold (choose_rep_for_bound_var scope) (untuple I u1) table @@ -1126,7 +1131,7 @@ let val quant_u = s_op2 oper T (Formula polar) u1' u2' in if def orelse (liberal andalso (polar = Pos) = (oper = All)) - orelse is_precise_type datatypes (type_of u1) then + orelse is_complete_type datatypes (type_of u1) then quant_u else let @@ -1140,7 +1145,7 @@ end end end - else if oper mem [Or, And] then + else if oper = Or orelse oper = And then let val u1' = gsub def polar u1 val u2' = gsub def polar u2 @@ -1159,7 +1164,7 @@ raise SAME ()) handle SAME () => s_op2 oper T (Formula polar) u1' u2' end - else if oper mem [The, Eps] then + else if oper = The orelse oper = Eps then let val u1' = sub u1 val opt1 = is_opt_rep (rep_of u1') @@ -1169,7 +1174,7 @@ else unopt_R |> opt ? opt_rep ofs T val u = Op2 (oper, T, R, u1', sub u2) in - if is_precise_type datatypes T orelse not opt1 then + if is_complete_type datatypes T orelse not opt1 then u else let @@ -1210,7 +1215,7 @@ let val Rs = map (best_one_rep_for_type scope o type_of) us val us = map sub us - val R = if forall (equal Unit) Rs then Unit else Struct Rs + val R = if forall (curry (op =) Unit) Rs then Unit else Struct Rs val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R in s_tuple T R' us end | Construct (us', T, _, us) => @@ -1234,8 +1239,8 @@ |> optimize_unit in aux table def Pos end -(* int -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list - -> int * Kodkod.n_ary_index list *) +(* int -> KK.n_ary_index list -> KK.n_ary_index list + -> int * KK.n_ary_index list *) fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys) | fresh_n_ary_index n ((m, j) :: xs) ys = if m = n then (j, ys @ ((m, j + 1) :: xs)) @@ -1312,7 +1317,18 @@ in (ws' @ ws, pool, NameTable.update (v, shape_tuple T R ws') table) end else let - val (j, pool) = fresh arity pool + val (j, pool) = + case v of + ConstName _ => + if is_sel_like_and_no_discr nick then + case domain_type T of + @{typ "unsigned_bit word"} => + (snd unsigned_bit_word_sel_rel, pool) + | @{typ "signed_bit word"} => (snd signed_bit_word_sel_rel, pool) + | _ => fresh arity pool + else + fresh arity pool + | _ => fresh arity pool val w = constr ((arity, j), T, R, nick) in (w :: ws, pool, NameTable.update (v, w) table) end end @@ -1331,7 +1347,7 @@ Cst _ => u | Op1 (oper, T, R, u1) => Op1 (oper, T, R, rename_vars_in_nut pool table u1) | Op2 (oper, T, R, u1, u2) => - if oper mem [All, Exist, Lambda] then + if oper = All orelse oper = Exist orelse oper = Lambda then let val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1) ([], pool, table) diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_peephole.ML --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Dec 18 12:00:44 2009 +0100 @@ -7,6 +7,7 @@ signature NITPICK_PEEPHOLE = sig + type n_ary_index = Kodkod.n_ary_index type formula = Kodkod.formula type int_expr = Kodkod.int_expr type rel_expr = Kodkod.rel_expr @@ -14,29 +15,29 @@ type expr_assign = Kodkod.expr_assign type name_pool = { - rels: Kodkod.n_ary_index list, - vars: Kodkod.n_ary_index list, + rels: n_ary_index list, + vars: n_ary_index list, formula_reg: int, rel_reg: int} val initial_pool : name_pool - val not3_rel : rel_expr - val suc_rel : rel_expr - val nat_add_rel : rel_expr - val int_add_rel : rel_expr - val nat_subtract_rel : rel_expr - val int_subtract_rel : rel_expr - val nat_multiply_rel : rel_expr - val int_multiply_rel : rel_expr - val nat_divide_rel : rel_expr - val int_divide_rel : rel_expr - val nat_modulo_rel : rel_expr - val int_modulo_rel : rel_expr - val nat_less_rel : rel_expr - val int_less_rel : rel_expr - val gcd_rel : rel_expr - val lcm_rel : rel_expr - val norm_frac_rel : rel_expr + val not3_rel : n_ary_index + val suc_rel : n_ary_index + val unsigned_bit_word_sel_rel : n_ary_index + val signed_bit_word_sel_rel : n_ary_index + val nat_add_rel : n_ary_index + val int_add_rel : n_ary_index + val nat_subtract_rel : n_ary_index + val int_subtract_rel : n_ary_index + val nat_multiply_rel : n_ary_index + val int_multiply_rel : n_ary_index + val nat_divide_rel : n_ary_index + val int_divide_rel : n_ary_index + val nat_less_rel : n_ary_index + val int_less_rel : n_ary_index + val gcd_rel : n_ary_index + val lcm_rel : n_ary_index + val norm_frac_rel : n_ary_index val atom_for_bool : int -> bool -> rel_expr val formula_for_bool : bool -> formula val atom_for_nat : int * int -> int -> int @@ -44,6 +45,7 @@ val max_int_for_card : int -> int val int_for_atom : int * int -> int -> int val atom_for_int : int * int -> int -> int + val is_twos_complement_representable : int -> int -> bool val inline_rel_expr : rel_expr -> bool val empty_n_ary_rel : int -> rel_expr val num_seq : int -> int -> int_expr list @@ -105,23 +107,23 @@ {rels = [(2, 10), (3, 20), (4, 10)], vars = [], formula_reg = 10, rel_reg = 10} -val not3_rel = Rel (2, 0) -val suc_rel = Rel (2, 1) -val nat_add_rel = Rel (3, 0) -val int_add_rel = Rel (3, 1) -val nat_subtract_rel = Rel (3, 2) -val int_subtract_rel = Rel (3, 3) -val nat_multiply_rel = Rel (3, 4) -val int_multiply_rel = Rel (3, 5) -val nat_divide_rel = Rel (3, 6) -val int_divide_rel = Rel (3, 7) -val nat_modulo_rel = Rel (3, 8) -val int_modulo_rel = Rel (3, 9) -val nat_less_rel = Rel (3, 10) -val int_less_rel = Rel (3, 11) -val gcd_rel = Rel (3, 12) -val lcm_rel = Rel (3, 13) -val norm_frac_rel = Rel (4, 0) +val not3_rel = (2, 0) +val suc_rel = (2, 1) +val unsigned_bit_word_sel_rel = (2, 2) +val signed_bit_word_sel_rel = (2, 3) +val nat_add_rel = (3, 0) +val int_add_rel = (3, 1) +val nat_subtract_rel = (3, 2) +val int_subtract_rel = (3, 3) +val nat_multiply_rel = (3, 4) +val int_multiply_rel = (3, 5) +val nat_divide_rel = (3, 6) +val int_divide_rel = (3, 7) +val nat_less_rel = (3, 8) +val int_less_rel = (3, 9) +val gcd_rel = (3, 10) +val lcm_rel = (3, 11) +val norm_frac_rel = (4, 0) (* int -> bool -> rel_expr *) fun atom_for_bool j0 = Atom o Integer.add j0 o int_for_bool @@ -140,6 +142,9 @@ if n < min_int_for_card k orelse n > max_int_for_card k then ~1 else if n < 0 then n + k + j0 else n + j0 +(* int -> int -> bool *) +fun is_twos_complement_representable bits n = + let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end (* rel_expr -> bool *) fun is_none_product (Product (r1, r2)) = @@ -261,7 +266,7 @@ (* bool -> int *) val from_bool = atom_for_bool main_j0 - (* int -> Kodkod.rel_expr *) + (* int -> rel_expr *) fun from_nat n = Atom (n + main_j0) val from_int = Atom o atom_for_int (int_card, main_j0) (* int -> int *) @@ -342,7 +347,7 @@ (* rel_expr -> formula *) fun s_no None = True | s_no (Product (r1, r2)) = s_or (s_no r1) (s_no r2) - | s_no (Intersect (Closure (Kodkod.Rel x), Kodkod.Iden)) = Acyclic x + | s_no (Intersect (Closure (Rel x), Iden)) = Acyclic x | s_no r = if is_one_rel_expr r then False else No r fun s_lone None = True | s_lone r = if is_one_rel_expr r then True else Lone r @@ -365,16 +370,28 @@ (* rel_expr -> rel_expr *) fun s_not3 (Atom j) = Atom (if j = main_j0 then j + 1 else j - 1) | s_not3 (r as Join (r1, r2)) = - if r2 = not3_rel then r1 else Join (r, not3_rel) - | s_not3 r = Join (r, not3_rel) + if r2 = Rel not3_rel then r1 else Join (r, Rel not3_rel) + | s_not3 r = Join (r, Rel not3_rel) (* rel_expr -> rel_expr -> formula *) fun s_rel_eq r1 r2 = (case (r1, r2) of - (Join (r11, r12), _) => - if r12 = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME () - | (_, Join (r21, r22)) => - if r22 = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME () + (Join (r11, Rel x), _) => + if x = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME () + | (_, Join (r21, Rel x)) => + if x = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME () + | (RelIf (f, r11, r12), _) => + if inline_rel_expr r2 then + s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2) + else + raise SAME () + | (_, RelIf (f, r21, r22)) => + if inline_rel_expr r1 then + s_formula_if f (s_rel_eq r1 r21) (s_rel_eq r1 r22) + else + raise SAME () + | (RelLet (bs, r1'), Atom _) => s_formula_let bs (s_rel_eq r1' r2) + | (Atom _, RelLet (bs, r2')) => s_formula_let bs (s_rel_eq r1 r2') | _ => raise SAME ()) handle SAME () => case rel_expr_equal r1 r2 of @@ -392,8 +409,8 @@ s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2) else RelEq (r1, r2) - | (_, Kodkod.None) => s_no r1 - | (Kodkod.None, _) => s_no r2 + | (_, None) => s_no r1 + | (None, _) => s_no r2 | _ => RelEq (r1, r2) fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2) | s_subset (Atom j) (AtomSeq (k, j0)) = @@ -499,8 +516,8 @@ | s_join (r1 as RelIf (f, r11, r12)) r2 = if inline_rel_expr r2 then s_rel_if f (s_join r11 r2) (s_join r12 r2) else Join (r1, r2) - | s_join (r1 as Atom j1) (r2 as Rel (2, j2)) = - if r2 = suc_rel then + | s_join (r1 as Atom j1) (r2 as Rel (x as (2, j2))) = + if x = suc_rel then let val n = to_nat j1 + 1 in if n < nat_card then from_nat n else None end @@ -511,8 +528,8 @@ s_project (s_join r21 r1) is else Join (r1, r2) - | s_join r1 (Join (r21, r22 as Rel (3, j22))) = - ((if r22 = nat_add_rel then + | s_join r1 (Join (r21, r22 as Rel (x as (3, j22)))) = + ((if x = nat_add_rel then case (r21, r1) of (Atom j1, Atom j2) => let val n = to_nat j1 + to_nat j2 in @@ -521,19 +538,19 @@ | (Atom j, r) => (case to_nat j of 0 => r - | 1 => s_join r suc_rel + | 1 => s_join r (Rel suc_rel) | _ => raise SAME ()) | (r, Atom j) => (case to_nat j of 0 => r - | 1 => s_join r suc_rel + | 1 => s_join r (Rel suc_rel) | _ => raise SAME ()) | _ => raise SAME () - else if r22 = nat_subtract_rel then + else if x = nat_subtract_rel then case (r21, r1) of (Atom j1, Atom j2) => from_nat (nat_minus (to_nat j1) (to_nat j2)) | _ => raise SAME () - else if r22 = nat_multiply_rel then + else if x = nat_multiply_rel then case (r21, r1) of (Atom j1, Atom j2) => let val n = to_nat j1 * to_nat j2 in @@ -596,20 +613,20 @@ in aux (arity_of_rel_expr r) r end (* rel_expr -> rel_expr -> rel_expr *) - fun s_nat_subtract r1 r2 = fold s_join [r1, r2] nat_subtract_rel + fun s_nat_subtract r1 r2 = fold s_join [r1, r2] (Rel nat_subtract_rel) fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2) - | s_nat_less r1 r2 = fold s_join [r1, r2] nat_less_rel + | s_nat_less r1 r2 = fold s_join [r1, r2] (Rel nat_less_rel) fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2) - | s_int_less r1 r2 = fold s_join [r1, r2] int_less_rel + | s_int_less r1 r2 = fold s_join [r1, r2] (Rel int_less_rel) (* rel_expr -> int -> int -> rel_expr *) fun d_project_seq r j0 n = Project (r, num_seq j0 n) (* rel_expr -> rel_expr *) - fun d_not3 r = Join (r, not3_rel) + fun d_not3 r = Join (r, Rel not3_rel) (* rel_expr -> rel_expr -> rel_expr *) - fun d_nat_subtract r1 r2 = List.foldl Join nat_subtract_rel [r1, r2] - fun d_nat_less r1 r2 = List.foldl Join nat_less_rel [r1, r2] - fun d_int_less r1 r2 = List.foldl Join int_less_rel [r1, r2] + fun d_nat_subtract r1 r2 = List.foldl Join (Rel nat_subtract_rel) [r1, r2] + fun d_nat_less r1 r2 = List.foldl Join (Rel nat_less_rel) [r1, r2] + fun d_int_less r1 r2 = List.foldl Join (Rel int_less_rel) [r1, r2] in if optim then {kk_all = s_all, kk_exist = s_exist, kk_formula_let = s_formula_let, diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Fri Dec 18 12:00:44 2009 +0100 @@ -299,7 +299,7 @@ | z => Func z) | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T fun best_set_rep_for_type (scope as {datatypes, ...}) T = - (if is_precise_type datatypes T then best_non_opt_set_rep_for_type + (if is_exact_type datatypes T then best_non_opt_set_rep_for_type else best_opt_set_rep_for_type) scope T fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...}) (Type ("fun", [T1, T2])) = diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Dec 18 12:00:44 2009 +0100 @@ -22,21 +22,24 @@ typ: typ, card: int, co: bool, - precise: bool, + complete: bool, + concrete: bool, shallow: bool, constrs: constr_spec list} type scope = { ext_ctxt: extended_context, card_assigns: (typ * int) list, + bits: int, bisim_depth: int, datatypes: dtype_spec list, ofs: int Typtab.table} val datatype_spec : dtype_spec list -> typ -> dtype_spec option val constr_spec : dtype_spec list -> styp -> constr_spec - val is_precise_type : dtype_spec list -> typ -> bool - val is_fully_comparable_type : dtype_spec list -> typ -> bool + val is_complete_type : dtype_spec list -> typ -> bool + val is_concrete_type : dtype_spec list -> typ -> bool + val is_exact_type : dtype_spec list -> typ -> bool val offset_of_type : int Typtab.table -> typ -> int val spec_of_type : scope -> typ -> int * int val pretties_for_scope : scope -> bool -> Pretty.T list @@ -46,7 +49,8 @@ val all_scopes : extended_context -> int -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list - -> int list -> typ list -> typ list -> typ list -> int * scope list + -> int list -> int list -> typ list -> typ list -> typ list + -> int * scope list end; structure Nitpick_Scope : NITPICK_SCOPE = @@ -67,13 +71,15 @@ typ: typ, card: int, co: bool, - precise: bool, + complete: bool, + concrete: bool, shallow: bool, constrs: constr_spec list} type scope = { ext_ctxt: extended_context, card_assigns: (typ * int) list, + bits: int, bisim_depth: int, datatypes: dtype_spec list, ofs: int Typtab.table} @@ -85,28 +91,32 @@ (* dtype_spec list -> typ -> dtype_spec option *) fun datatype_spec (dtypes : dtype_spec list) T = - List.find (equal T o #typ) dtypes + List.find (curry (op =) T o #typ) dtypes (* dtype_spec list -> styp -> constr_spec *) fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x]) | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) = - case List.find (equal (s, body_type T) o (apsnd body_type o #const)) + case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const)) constrs of SOME c => c | NONE => constr_spec dtypes x (* dtype_spec list -> typ -> bool *) -fun is_precise_type dtypes (Type ("fun", Ts)) = - forall (is_precise_type dtypes) Ts - | is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts - | is_precise_type dtypes T = - not (is_integer_type T) andalso #precise (the (datatype_spec dtypes T)) +fun is_complete_type dtypes (Type ("fun", [T1, T2])) = + is_concrete_type dtypes T1 andalso is_complete_type dtypes T2 + | is_complete_type dtypes (Type ("*", Ts)) = + forall (is_complete_type dtypes) Ts + | is_complete_type dtypes T = + not (is_integer_type T) andalso not (is_bit_type T) + andalso #complete (the (datatype_spec dtypes T)) handle Option.Option => true -fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) = - is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2 - | is_fully_comparable_type dtypes (Type ("*", Ts)) = - forall (is_fully_comparable_type dtypes) Ts - | is_fully_comparable_type _ _ = true +and is_concrete_type dtypes (Type ("fun", [T1, T2])) = + is_complete_type dtypes T1 andalso is_concrete_type dtypes T2 + | is_concrete_type dtypes (Type ("*", Ts)) = + forall (is_concrete_type dtypes) Ts + | is_concrete_type dtypes T = + #concrete (the (datatype_spec dtypes T)) handle Option.Option => true +fun is_exact_type dtypes = is_complete_type dtypes andf is_concrete_type dtypes (* int Typtab.table -> typ -> int *) fun offset_of_type ofs T = @@ -122,13 +132,16 @@ (* (string -> string) -> scope -> string list * string list * string list * string list * string list *) fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns, - bisim_depth, datatypes, ...} : scope) = + bits, bisim_depth, datatypes, ...} : scope) = let - val (iter_asgns, card_asgns) = - card_assigns |> filter_out (equal @{typ bisim_iterator} o fst) + val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, + @{typ bisim_iterator}] + val (iter_assigns, card_assigns) = + card_assigns |> filter_out (member (op =) boring_Ts o fst) |> List.partition (is_fp_iterator_type o fst) - val (unimportant_card_asgns, important_card_asgns) = - card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst) + val (secondary_card_assigns, primary_card_assigns) = + card_assigns |> List.partition ((is_integer_type orf is_datatype thy) + o fst) val cards = map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^ string_of_int k) @@ -145,24 +158,25 @@ map (fn (T, k) => quote (Syntax.string_of_term ctxt (Const (const_for_iterator_type T))) ^ " = " ^ - string_of_int (k - 1)) iter_asgns - fun bisims () = - if bisim_depth < 0 andalso forall (not o #co) datatypes then [] - else ["bisim_depth = " ^ string_of_int bisim_depth] + string_of_int (k - 1)) iter_assigns + fun miscs () = + (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @ + (if bisim_depth < 0 andalso forall (not o #co) datatypes then [] + else ["bisim_depth = " ^ string_of_int bisim_depth]) in setmp_show_all_types - (fn () => (cards important_card_asgns, cards unimportant_card_asgns, - maxes (), iters (), bisims ())) () + (fn () => (cards primary_card_assigns, cards secondary_card_assigns, + maxes (), iters (), miscs ())) () end (* scope -> bool -> Pretty.T list *) fun pretties_for_scope scope verbose = let - val (important_cards, unimportant_cards, maxes, iters, bisim_depths) = + val (primary_cards, secondary_cards, maxes, iters, bisim_depths) = quintuple_for_scope maybe_quote scope - val ss = map (prefix "card ") important_cards @ + val ss = map (prefix "card ") primary_cards @ (if verbose then - map (prefix "card ") unimportant_cards @ + map (prefix "card ") secondary_cards @ map (prefix "max ") maxes @ map (prefix "iter ") iters @ bisim_depths @@ -176,9 +190,9 @@ (* scope -> string *) fun multiline_string_for_scope scope = let - val (important_cards, unimportant_cards, maxes, iters, bisim_depths) = + val (primary_cards, secondary_cards, maxes, iters, bisim_depths) = quintuple_for_scope I scope - val cards = important_cards @ unimportant_cards + val cards = primary_cards @ secondary_cards in case (if null cards then [] else ["card: " ^ commas cards]) @ (if null maxes then [] else ["max: " ^ commas maxes]) @ @@ -204,52 +218,62 @@ fun project_block (column, block) = map (project_row column) block (* (''a * ''a -> bool) -> (''a option * int list) list -> ''a -> int list *) -fun lookup_ints_assign eq asgns key = - case triple_lookup eq asgns key of +fun lookup_ints_assign eq assigns key = + case triple_lookup eq assigns key of SOME ks => ks | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "") (* theory -> (typ option * int list) list -> typ -> int list *) -fun lookup_type_ints_assign thy asgns T = - map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T) +fun lookup_type_ints_assign thy assigns T = + map (curry Int.max 1) (lookup_ints_assign (type_match thy) assigns T) handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], []) (* theory -> (styp option * int list) list -> styp -> int list *) -fun lookup_const_ints_assign thy asgns x = - lookup_ints_assign (const_match thy) asgns x +fun lookup_const_ints_assign thy assigns x = + lookup_ints_assign (const_match thy) assigns x handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x]) (* theory -> (styp option * int list) list -> styp -> row option *) -fun row_for_constr thy maxes_asgns constr = - SOME (Max constr, lookup_const_ints_assign thy maxes_asgns constr) +fun row_for_constr thy maxes_assigns constr = + SOME (Max constr, lookup_const_ints_assign thy maxes_assigns constr) handle TERM ("lookup_const_ints_assign", _) => NONE +val max_bits = 31 (* Kodkod limit *) + (* extended_context -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list -> int list - -> typ -> block *) -fun block_for_type (ext_ctxt as {thy, ...}) cards_asgns maxes_asgns iters_asgns - bisim_depths T = - if T = @{typ bisim_iterator} then - [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)] + -> int list -> typ -> block *) +fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns + iters_assigns bitss bisim_depths T = + if T = @{typ unsigned_bit} then + [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)] + else if T = @{typ signed_bit} then + [(Card T, map (Integer.add 1 o Integer.min max_bits o Integer.max 1) bitss)] + else if T = @{typ "unsigned_bit word"} then + [(Card T, lookup_type_ints_assign thy cards_assigns nat_T)] + else if T = @{typ "signed_bit word"} then + [(Card T, lookup_type_ints_assign thy cards_assigns int_T)] + else if T = @{typ bisim_iterator} then + [(Card T, map (Integer.add 1 o Integer.max 0) bisim_depths)] else if is_fp_iterator_type T then - [(Card T, map (fn k => Int.max (0, k) + 1) - (lookup_const_ints_assign thy iters_asgns + [(Card T, map (Integer.add 1 o Integer.max 0) + (lookup_const_ints_assign thy iters_assigns (const_for_iterator_type T)))] else - (Card T, lookup_type_ints_assign thy cards_asgns T) :: + (Card T, lookup_type_ints_assign thy cards_assigns T) :: (case datatype_constrs ext_ctxt T of [_] => [] - | constrs => map_filter (row_for_constr thy maxes_asgns) constrs) + | constrs => map_filter (row_for_constr thy maxes_assigns) constrs) (* extended_context -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list -> int list - -> typ list -> typ list -> block list *) -fun blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns bisim_depths - mono_Ts nonmono_Ts = + -> int list -> typ list -> typ list -> block list *) +fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns bitss + bisim_depths mono_Ts nonmono_Ts = let (* typ -> block *) - val block_for = block_for_type ext_ctxt cards_asgns maxes_asgns iters_asgns - bisim_depths + val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns + iters_assigns bitss bisim_depths val mono_block = maps block_for mono_Ts val nonmono_blocks = map block_for nonmono_Ts in mono_block :: nonmono_blocks end @@ -262,14 +286,14 @@ (* int list -> int *) fun cost_with_monos [] = 0 | cost_with_monos (k :: ks) = - if k < sync_threshold andalso forall (equal k) ks then + if k < sync_threshold andalso forall (curry (op =) k) ks then k - sync_threshold else k * (k + 1) div 2 + Integer.sum ks fun cost_without_monos [] = 0 | cost_without_monos [k] = k | cost_without_monos (_ :: k :: ks) = - if k < sync_threshold andalso forall (equal k) ks then + if k < sync_threshold andalso forall (curry (op =) k) ks then k - sync_threshold else Integer.sum (k :: ks) @@ -282,7 +306,7 @@ (* typ -> bool *) fun is_self_recursive_constr_type T = - exists (exists_subtype (equal (body_type T))) (binder_types T) + exists (exists_subtype (curry (op =) (body_type T))) (binder_types T) (* (styp * int) list -> styp -> int *) fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x) @@ -290,117 +314,109 @@ type scope_desc = (typ * int) list * (styp * int) list (* extended_context -> scope_desc -> typ * int -> bool *) -fun is_surely_inconsistent_card_assign ext_ctxt (card_asgns, max_asgns) (T, k) = +fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns) + (T, k) = case datatype_constrs ext_ctxt T of [] => false | xs => let - val precise_cards = - map (Integer.prod - o map (bounded_precise_card_of_type ext_ctxt k 0 card_asgns) + val dom_cards = + map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns) o binder_types o snd) xs - val maxes = map (constr_max max_asgns) xs + val maxes = map (constr_max max_assigns) xs (* int -> int -> int *) - fun effective_max 0 ~1 = k - | effective_max 0 max = max - | effective_max card ~1 = card + fun effective_max card ~1 = card | effective_max card max = Int.min (card, max) - val max = map2 effective_max precise_cards maxes |> Integer.sum - (* unit -> int *) - fun doms_card () = - xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_asgns) - o binder_types o snd) - |> Integer.sum - in - max < k - orelse (forall (not_equal 0) precise_cards andalso doms_card () < k) - end - handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false - -(* extended_context -> scope_desc -> bool *) -fun is_surely_inconsistent_scope_description ext_ctxt - (desc as (card_asgns, _)) = - exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_asgns + val max = map2 effective_max dom_cards maxes |> Integer.sum + in max < k end +(* extended_context -> (typ * int) list -> (typ * int) list + -> (styp * int) list -> bool *) +fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns = + exists (is_surely_inconsistent_card_assign ext_ctxt + (seen @ rest, max_assigns)) seen (* extended_context -> scope_desc -> (typ * int) list option *) -fun repair_card_assigns ext_ctxt (card_asgns, max_asgns) = +fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) = let (* (typ * int) list -> (typ * int) list -> (typ * int) list option *) fun aux seen [] = SOME seen | aux seen ((T, 0) :: _) = NONE - | aux seen ((T, k) :: asgns) = - (if is_surely_inconsistent_scope_description ext_ctxt - ((T, k) :: seen, max_asgns) then + | aux seen ((T, k) :: rest) = + (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen) + rest max_assigns then raise SAME () else - case aux ((T, k) :: seen) asgns of - SOME asgns => SOME asgns + case aux ((T, k) :: seen) rest of + SOME assigns => SOME assigns | NONE => raise SAME ()) - handle SAME () => aux seen ((T, k - 1) :: asgns) - in aux [] (rev card_asgns) end + handle SAME () => aux seen ((T, k - 1) :: rest) + in aux [] (rev card_assigns) end (* theory -> (typ * int) list -> typ * int -> typ * int *) -fun repair_iterator_assign thy asgns (T as Type (s, Ts), k) = +fun repair_iterator_assign thy assigns (T as Type (s, Ts), k) = (T, if T = @{typ bisim_iterator} then - let val co_cards = map snd (filter (is_codatatype thy o fst) asgns) in - Int.min (k, Integer.sum co_cards) - end + let + val co_cards = map snd (filter (is_codatatype thy o fst) assigns) + in Int.min (k, Integer.sum co_cards) end else if is_fp_iterator_type T then case Ts of [] => 1 - | _ => bounded_card_of_type k ~1 asgns (foldr1 HOLogic.mk_prodT Ts) + | _ => bounded_card_of_type k ~1 assigns (foldr1 HOLogic.mk_prodT Ts) else k) - | repair_iterator_assign _ _ asgn = asgn + | repair_iterator_assign _ _ assign = assign (* row -> scope_desc -> scope_desc *) -fun add_row_to_scope_descriptor (kind, ks) (card_asgns, max_asgns) = +fun add_row_to_scope_descriptor (kind, ks) (card_assigns, max_assigns) = case kind of - Card T => ((T, the_single ks) :: card_asgns, max_asgns) - | Max x => (card_asgns, (x, the_single ks) :: max_asgns) + Card T => ((T, the_single ks) :: card_assigns, max_assigns) + | Max x => (card_assigns, (x, the_single ks) :: max_assigns) (* block -> scope_desc *) fun scope_descriptor_from_block block = fold_rev add_row_to_scope_descriptor block ([], []) (* extended_context -> block list -> int list -> scope_desc option *) fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns = let - val (card_asgns, max_asgns) = + val (card_assigns, max_assigns) = maps project_block (columns ~~ blocks) |> scope_descriptor_from_block - val card_asgns = repair_card_assigns ext_ctxt (card_asgns, max_asgns) |> the + val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns) + |> the in - SOME (map (repair_iterator_assign thy card_asgns) card_asgns, max_asgns) + SOME (map (repair_iterator_assign thy card_assigns) card_assigns, + max_assigns) end handle Option.Option => NONE (* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *) -fun offset_table_for_card_assigns thy asgns dtypes = +fun offset_table_for_card_assigns thy assigns dtypes = let (* int -> (int * int) list -> (typ * int) list -> int Typtab.table -> int Typtab.table *) fun aux next _ [] = Typtab.update_new (dummyT, next) - | aux next reusable ((T, k) :: asgns) = - if k = 1 orelse is_integer_type T then - aux next reusable asgns + | aux next reusable ((T, k) :: assigns) = + if k = 1 orelse is_integer_type T orelse is_bit_type T then + aux next reusable assigns else if length (these (Option.map #constrs (datatype_spec dtypes T))) > 1 then - Typtab.update_new (T, next) #> aux (next + k) reusable asgns + Typtab.update_new (T, next) #> aux (next + k) reusable assigns else case AList.lookup (op =) reusable k of - SOME j0 => Typtab.update_new (T, j0) #> aux next reusable asgns + SOME j0 => Typtab.update_new (T, j0) #> aux next reusable assigns | NONE => Typtab.update_new (T, next) - #> aux (next + k) ((k, next) :: reusable) asgns - in aux 0 [] asgns Typtab.empty end + #> aux (next + k) ((k, next) :: reusable) assigns + in aux 0 [] assigns Typtab.empty end (* int -> (typ * int) list -> typ -> int *) -fun domain_card max card_asgns = - Integer.prod o map (bounded_card_of_type max max card_asgns) o binder_types +fun domain_card max card_assigns = + Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types (* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp -> constr_spec list -> constr_spec list *) -fun add_constr_spec (card_asgns, max_asgns) co card sum_dom_cards num_self_recs - num_non_self_recs (self_rec, x as (s, T)) constrs = +fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards + num_self_recs num_non_self_recs (self_rec, x as (s, T)) + constrs = let - val max = constr_max max_asgns x + val max = constr_max max_assigns x (* int -> int *) fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k) (* unit -> int *) @@ -412,7 +428,7 @@ end else if not co andalso num_self_recs > 0 then if not self_rec andalso num_non_self_recs = 1 - andalso domain_card 2 card_asgns T = 1 then + andalso domain_card 2 card_assigns T = 1 then {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}), total = true} else if s = @{const_name Cons} then @@ -421,7 +437,7 @@ {delta = 0, epsilon = card, exclusive = false, total = false} else if card = sum_dom_cards (card + 1) then let val delta = next_delta () in - {delta = delta, epsilon = delta + domain_card card card_asgns T, + {delta = delta, epsilon = delta + domain_card card card_assigns T, exclusive = true, total = true} end else @@ -432,55 +448,74 @@ explicit_max = max, total = total} :: constrs end +(* extended_context -> (typ * int) list -> typ -> bool *) +fun has_exact_card ext_ctxt card_assigns T = + let val card = card_of_type card_assigns T in + card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T + end + (* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *) fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs - (desc as (card_asgns, _)) (T, card) = + (desc as (card_assigns, _)) (T, card) = let - val shallow = T mem shallow_dataTs + val shallow = member (op =) shallow_dataTs T val co = is_codatatype thy T val xs = boxed_datatype_constrs ext_ctxt T val self_recs = map (is_self_recursive_constr_type o snd) xs val (num_self_recs, num_non_self_recs) = - List.partition (equal true) self_recs |> pairself length - val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0 - card_asgns T) + List.partition I self_recs |> pairself length + val complete = has_exact_card ext_ctxt card_assigns T + val concrete = xs |> maps (binder_types o snd) |> maps binder_types + |> forall (has_exact_card ext_ctxt card_assigns) (* int -> int *) fun sum_dom_cards max = - map (domain_card max card_asgns o snd) xs |> Integer.sum + map (domain_card max card_assigns o snd) xs |> Integer.sum val constrs = fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs num_non_self_recs) (self_recs ~~ xs) [] in - {typ = T, card = card, co = co, precise = precise, shallow = shallow, - constrs = constrs} + {typ = T, card = card, co = co, complete = complete, concrete = concrete, + shallow = shallow, constrs = constrs} end +(* int -> int *) +fun min_bits_for_nat_value n = if n <= 0 then 0 else IntInf.log2 n + 1 +(* scope_desc -> int *) +fun min_bits_for_max_assigns (_, []) = 0 + | min_bits_for_max_assigns (card_assigns, max_assigns) = + min_bits_for_nat_value (fold Integer.max + (map snd card_assigns @ map snd max_assigns) 0) + (* extended_context -> int -> typ list -> scope_desc -> scope *) fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs - (desc as (card_asgns, _)) = + (desc as (card_assigns, _)) = let val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc) - (filter (is_datatype thy o fst) card_asgns) - val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1 + (filter (is_datatype thy o fst) card_assigns) + val bits = card_of_type card_assigns @{typ signed_bit} - 1 + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => + card_of_type card_assigns @{typ unsigned_bit} + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0 + val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1 in - {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes, - bisim_depth = bisim_depth, + {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes, + bits = bits, bisim_depth = bisim_depth, ofs = if sym_break <= 0 then Typtab.empty - else offset_table_for_card_assigns thy card_asgns datatypes} + else offset_table_for_card_assigns thy card_assigns datatypes} end (* theory -> typ list -> (typ option * int list) list -> (typ option * int list) list *) -fun fix_cards_assigns_wrt_boxing _ _ [] = [] - | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_asgns) = +fun repair_cards_assigns_wrt_boxing _ _ [] = [] + | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) = (if is_fun_type T orelse is_pair_type T then - Ts |> filter (curry (type_match thy o swap) T o unbox_type) + Ts |> filter (curry (type_match thy o swap) T o unbit_and_unbox_type) |> map (rpair ks o SOME) else - [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_asgns - | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_asgns) = - (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_asgns + [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns + | repair_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) = + (NONE, ks) :: repair_cards_assigns_wrt_boxing thy Ts cards_assigns val max_scopes = 4096 val distinct_threshold = 512 @@ -488,12 +523,15 @@ (* extended_context -> int -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list -> int list -> typ list -> typ list -> typ list -> int * scope list *) -fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_asgns maxes_asgns - iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs = +fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns + iters_assigns bitss bisim_depths mono_Ts nonmono_Ts + shallow_dataTs = let - val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns - val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns - bisim_depths mono_Ts nonmono_Ts + val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts + cards_assigns + val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns + iters_assigns bitss bisim_depths mono_Ts + nonmono_Ts val ranks = map rank_of_block blocks val all = all_combinations_ordered_smartly (map (rpair 0) ranks) val head = take max_scopes all diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Dec 18 12:00:44 2009 +0100 @@ -300,6 +300,7 @@ val peephole_optim = true val nat_card = 4 val int_card = 9 + val bits = 8 val j0 = 0 val constrs = kodkod_constrs peephole_optim nat_card int_card j0 val (free_rels, pool, table) = @@ -307,7 +308,7 @@ NameTable.empty val u = Op1 (Not, type_of u, rep_of u, u) |> rename_vars_in_nut pool table - val formula = kodkod_formula_from_nut Typtab.empty false constrs u + val formula = kodkod_formula_from_nut bits Typtab.empty false constrs u val bounds = map (bound_for_plain_rel ctxt debug) free_rels val univ_card = univ_card nat_card int_card j0 bounds formula val declarative_axioms = map (declarative_axiom_for_plain_rel constrs) diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Dec 18 12:00:44 2009 +0100 @@ -12,7 +12,8 @@ exception ARG of string * string exception BAD of string * string - exception LIMIT of string * string + exception TOO_SMALL of string * string + exception TOO_LARGE of string * string exception NOT_SUPPORTED of string exception SAME of unit @@ -51,7 +52,6 @@ val bool_T : typ val nat_T : typ val int_T : typ - val subscript : string -> string val nat_subscript : int -> string val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b val DETERM_TIMEOUT : Time.time option -> tactic -> tactic @@ -71,7 +71,8 @@ exception ARG of string * string exception BAD of string * string -exception LIMIT of string * string +exception TOO_SMALL of string * string +exception TOO_LARGE of string * string exception NOT_SUPPORTED of string exception SAME of unit @@ -96,14 +97,16 @@ | reasonable_power 0 _ = 0 | reasonable_power 1 _ = 1 | reasonable_power a b = - if b < 0 orelse b > max_exponent then - raise LIMIT ("Nitpick_Util.reasonable_power", - "too large exponent (" ^ signed_string_of_int b ^ ")") + if b < 0 then + raise ARG ("Nitpick_Util.reasonable_power", + "negative exponent (" ^ signed_string_of_int b ^ ")") + else if b > max_exponent then + raise TOO_LARGE ("Nitpick_Util.reasonable_power", + "too large exponent (" ^ signed_string_of_int b ^ ")") else - let - val c = reasonable_power a (b div 2) in - c * c * reasonable_power a (b mod 2) - end + let val c = reasonable_power a (b div 2) in + c * c * reasonable_power a (b mod 2) + end (* int -> int -> int *) fun exact_log m n = @@ -247,7 +250,11 @@ (* string -> string *) val subscript = implode o map (prefix "\<^isub>") o explode (* int -> string *) -val nat_subscript = subscript o signed_string_of_int +fun nat_subscript n = + (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit + numbers *) + if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>" + else subscript (string_of_int n) (* Time.time option -> ('a -> 'b) -> 'a -> 'b *) fun time_limit NONE = I diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/refute.ML Fri Dec 18 12:00:44 2009 +0100 @@ -45,13 +45,16 @@ val get_default_params : theory -> (string * string) list val actual_params : theory -> (string * string) list -> params - val find_model : theory -> params -> term -> bool -> unit + val find_model : theory -> params -> term list -> term -> bool -> unit (* tries to find a model for a formula: *) - val satisfy_term : theory -> (string * string) list -> term -> unit + val satisfy_term : + theory -> (string * string) list -> term list -> term -> unit (* tries to find a model that refutes a formula: *) - val refute_term : theory -> (string * string) list -> term -> unit - val refute_goal : theory -> (string * string) list -> thm -> int -> unit + val refute_term : + theory -> (string * string) list -> term list -> term -> unit + val refute_goal : + Proof.context -> (string * string) list -> thm -> int -> unit val setup : theory -> theory @@ -153,8 +156,10 @@ (* formula. *) (* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) (* "satsolver" string SAT solver to be used. *) +(* "no_assms" bool If "true", assumptions in structured proofs are *) +(* not considered. *) (* "expect" string Expected result ("genuine", "potential", "none", or *) -(* "unknown") *) +(* "unknown"). *) (* ------------------------------------------------------------------------- *) type params = @@ -165,6 +170,7 @@ maxvars : int, maxtime : int, satsolver: string, + no_assms : bool, expect : string }; @@ -360,6 +366,15 @@ fun actual_params thy override = let + (* (string * string) list * string -> bool *) + fun read_bool (parms, name) = + case AList.lookup (op =) parms name of + SOME "true" => true + | SOME "false" => false + | SOME s => error ("parameter " ^ quote name ^ + " (value is " ^ quote s ^ ") must be \"true\" or \"false\"") + | NONE => error ("parameter " ^ quote name ^ + " must be assigned a value") (* (string * string) list * string -> int *) fun read_int (parms, name) = case AList.lookup (op =) parms name of @@ -385,6 +400,7 @@ val maxtime = read_int (allparams, "maxtime") (* string *) val satsolver = read_string (allparams, "satsolver") + val no_assms = read_bool (allparams, "no_assms") val expect = the_default "" (AList.lookup (op =) allparams "expect") (* all remaining parameters of the form "string=int" are collected in *) (* 'sizes' *) @@ -395,10 +411,10 @@ (fn (name, value) => Option.map (pair name) (Int.fromString value)) (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" - andalso name<>"satsolver") allparams) + andalso name<>"satsolver" andalso name<>"no_assms") allparams) in {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, - maxtime=maxtime, satsolver=satsolver, expect=expect} + maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect} end; @@ -1118,6 +1134,7 @@ (* the model to the user by calling 'print_model' *) (* thy : the current theory *) (* {...} : parameters that control the translation/model generation *) +(* assm_ts : assumptions to be considered unless "no_assms" is specified *) (* t : term to be translated into a propositional formula *) (* negate : if true, find a model that makes 't' false (rather than true) *) (* ------------------------------------------------------------------------- *) @@ -1125,7 +1142,7 @@ (* theory -> params -> Term.term -> bool -> unit *) fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver, - expect} t negate = + no_assms, expect} assm_ts t negate = let (* string -> unit *) fun check_expect outcome_code = @@ -1135,6 +1152,9 @@ fun wrapper () = let val timer = Timer.startRealTimer () + val t = if no_assms then t + else if negate then Logic.list_implies (assm_ts, t) + else Logic.mk_conjunction_list (t :: assm_ts) val u = unfold_defs thy t val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u) val axioms = collect_axioms thy u @@ -1270,10 +1290,10 @@ (* parameters *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list -> Term.term -> unit *) + (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *) - fun satisfy_term thy params t = - find_model thy (actual_params thy params) t false; + fun satisfy_term thy params assm_ts t = + find_model thy (actual_params thy params) assm_ts t false; (* ------------------------------------------------------------------------- *) (* refute_term: calls 'find_model' to find a model that refutes 't' *) @@ -1281,9 +1301,9 @@ (* parameters *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * string) list -> Term.term -> unit *) + (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *) - fun refute_term thy params t = + fun refute_term thy params assm_ts t = let (* disallow schematic type variables, since we cannot properly negate *) (* terms containing them (their logical meaning is that there EXISTS a *) @@ -1332,15 +1352,29 @@ val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure) val subst_t = Term.subst_bounds (map Free frees, strip_t) in - find_model thy (actual_params thy params) subst_t true + find_model thy (actual_params thy params) assm_ts subst_t true + handle REFUTE (s, s') => error ("REFUTE " ^ s ^ " " ^ s') (* ### *) end; (* ------------------------------------------------------------------------- *) (* refute_goal *) (* ------------------------------------------------------------------------- *) - fun refute_goal thy params st i = - refute_term thy params (Logic.get_goal (Thm.prop_of st) i); + fun refute_goal ctxt params th i = + let + val t = th |> prop_of + in + if Logic.count_prems t = 0 then + priority "No subgoal!" + else + let + val assms = map term_of (Assumption.all_assms_of ctxt) + val (t, frees) = Logic.goal_params t i + in + refute_term (ProofContext.theory_of ctxt) params assms + (subst_bounds (frees, t)) + end + end (* ------------------------------------------------------------------------- *) diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/Tools/refute_isar.ML --- a/src/HOL/Tools/refute_isar.ML Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/Tools/refute_isar.ML Fri Dec 18 12:00:44 2009 +0100 @@ -12,8 +12,9 @@ (*optional list of arguments of the form [name1=value1, name2=value2, ...]*) -val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name); - +val scan_parm = + OuterParse.name + -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true") val scan_parms = Scan.optional (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") []; @@ -27,9 +28,9 @@ (fn (parms, i) => Toplevel.keep (fn state => let - val thy = Toplevel.theory_of state; + val ctxt = Toplevel.context_of state; val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state); - in Refute.refute_goal thy parms st i end))); + in Refute.refute_goal ctxt parms st i end))); (* 'refute_params' command *) diff -r b1cabadf6881 -r 85257fa296f6 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Fri Dec 18 11:28:24 2009 +0100 +++ b/src/HOL/ex/Refute_Examples.thy Fri Dec 18 12:00:44 2009 +0100 @@ -1516,6 +1516,17 @@ refute oops +text {* Structured proofs *} + +lemma "x = y" +proof cases + assume "x = y" + show ?thesis + refute + refute [no_assms] + refute [no_assms = false] +oops + refute_params [satsolver="auto"] end