1.1 --- a/doc-src/Nitpick/nitpick.tex Mon Dec 14 16:48:49 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Thu Dec 17 15:22:11 2009 +0100
1.3 @@ -436,12 +436,10 @@
1.4 \label{natural-numbers-and-integers}
1.5
1.6 Because of the axiom of infinity, the type \textit{nat} does not admit any
1.7 -finite models. To deal with this, Nitpick considers prefixes $\{0,\, 1,\,
1.8 -\ldots,\, K - 1\}$ of \textit{nat} (where $K = \textit{card}~\textit{nat}$) and
1.9 -maps all other numbers to the undefined value ($\unk$). The type \textit{int} is
1.10 -handled in a similar way: If $K = \textit{card}~\textit{int}$, the subset of
1.11 -\textit{int} known to Nitpick is $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor
1.12 -K/2 \rfloor\}$. Undefined values lead to a three-valued logic.
1.13 +finite models. To deal with this, Nitpick's approach is to consider finite
1.14 +subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined
1.15 +value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
1.16 +Internally, undefined values lead to a three-valued logic.
1.17
1.18 Here is an example involving \textit{int}:
1.19
1.20 @@ -456,15 +454,26 @@
1.21 \hbox{}\qquad\qquad $n = 0$
1.22 \postw
1.23
1.24 +Internally, Nitpick uses either a unary or a binary representation of numbers.
1.25 +The unary representation is more efficient but only suitable for numbers very
1.26 +close to zero. By default, Nitpick attempts to choose the more appropriate
1.27 +encoding by inspecting the formula at hand. This behavior can be overridden by
1.28 +passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For
1.29 +binary notation, the number of bits to use can be specified using
1.30 +the \textit{bits} option. For example:
1.31 +
1.32 +\prew
1.33 +\textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$]
1.34 +\postw
1.35 +
1.36 With infinite types, we don't always have the luxury of a genuine counterexample
1.37 and must often content ourselves with a potential one. The tedious task of
1.38 finding out whether the potential counterexample is in fact genuine can be
1.39 -outsourced to \textit{auto} by passing the option \textit{check\_potential}. For
1.40 -example:
1.41 +outsourced to \textit{auto} by passing \textit{check\_potential}. For example:
1.42
1.43 \prew
1.44 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
1.45 -\textbf{nitpick} [\textit{card~nat}~= 100,\, \textit{check\_potential}] \\[2\smallskipamount]
1.46 +\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
1.47 \slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
1.48 \hbox{}\qquad Free variable: \nopagebreak \\
1.49 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
1.50 @@ -482,7 +491,7 @@
1.51
1.52 Incidentally, if you distrust the so-called genuine counterexamples, you can
1.53 enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
1.54 -aware that \textit{auto} will often fail to prove that the counterexample is
1.55 +aware that \textit{auto} will usually fail to prove that the counterexample is
1.56 genuine or spurious.
1.57
1.58 Some conjectures involving elementary number theory make Nitpick look like a
1.59 @@ -495,10 +504,11 @@
1.60 Nitpick found no counterexample.
1.61 \postw
1.62
1.63 -For any cardinality $k$, \textit{Suc} is the partial function $\{0 \mapsto 1,\,
1.64 -1 \mapsto 2,\, \ldots,\, k - 1 \mapsto \unk\}$, which evaluates to $\unk$ when
1.65 -it is passed as argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$.
1.66 -The next example is similar:
1.67 +On any finite set $N$, \textit{Suc} is a partial function; for example, if $N =
1.68 +\{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\,
1.69 +\ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as
1.70 +argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next
1.71 +example is similar:
1.72
1.73 \prew
1.74 \textbf{lemma} ``$P~(\textit{op}~{+}\Colon
1.75 @@ -822,7 +832,7 @@
1.76
1.77 \prew
1.78 \textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
1.79 -\textbf{nitpick} [\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
1.80 +\textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
1.81 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.82 \hbox{}\qquad Free variable: \nopagebreak \\
1.83 \hbox{}\qquad\qquad $n = 1$ \\
1.84 @@ -989,7 +999,7 @@
1.85 \prew
1.86 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
1.87 \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1.88 -\textbf{nitpick} [\textit{bisim\_depth} = $-1$,\, \textit{show\_datatypes}] \\[2\smallskipamount]
1.89 +\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
1.90 \slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1.91 \hbox{}\qquad Free variables: \nopagebreak \\
1.92 \hbox{}\qquad\qquad $a = a_2$ \\
1.93 @@ -1687,9 +1697,38 @@
1.94
1.95 \begin{enum}
1.96 \opu{card}{type}{int\_seq}
1.97 -Specifies the sequence of cardinalities to use for a given type. For
1.98 -\textit{nat} and \textit{int}, the cardinality fully specifies the subset used
1.99 -to approximate the type. For example:
1.100 +Specifies the sequence of cardinalities to use for a given type.
1.101 +For free types, and often also for \textbf{typedecl}'d types, it usually makes
1.102 +sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1.103 +Although function and product types are normally mapped directly to the
1.104 +corresponding Kodkod concepts, setting
1.105 +the cardinality of such types is also allowed and implicitly enables ``boxing''
1.106 +for them, as explained in the description of the \textit{box}~\qty{type}
1.107 +and \textit{box} (\S\ref{scope-of-search}) options.
1.108 +
1.109 +\nopagebreak
1.110 +{\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.111 +
1.112 +\opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.113 +Specifies the default sequence of cardinalities to use. This can be overridden
1.114 +on a per-type basis using the \textit{card}~\qty{type} option described above.
1.115 +
1.116 +\opu{max}{const}{int\_seq}
1.117 +Specifies the sequence of maximum multiplicities to use for a given
1.118 +(co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1.119 +number of distinct values that it can construct. Nonsensical values (e.g.,
1.120 +\textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1.121 +datatypes equipped with several constructors.
1.122 +
1.123 +\ops{max}{int\_seq}
1.124 +Specifies the default sequence of maximum multiplicities to use for
1.125 +(co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1.126 +basis using the \textit{max}~\qty{const} option described above.
1.127 +
1.128 +\opsmart{binary\_ints}{unary\_ints}
1.129 +Specifies whether natural numbers and integers should be encoded using a unary
1.130 +or binary notation. In unary mode, the cardinality fully specifies the subset
1.131 +used to approximate the type. For example:
1.132 %
1.133 $$\hbox{\begin{tabular}{@{}rll@{}}%
1.134 \textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
1.135 @@ -1704,32 +1743,25 @@
1.136 \textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
1.137 \end{tabular}}$$
1.138 %
1.139 -For free types, and often also for \textbf{typedecl}'d types, it usually makes
1.140 -sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1.141 -Although function and product types are normally mapped directly to the
1.142 -corresponding Kodkod concepts, setting
1.143 -the cardinality of such types is also allowed and implicitly enables ``boxing''
1.144 -for them, as explained in the description of the \textit{box}~\qty{type}
1.145 -and \textit{box} (\S\ref{scope-of-search}) options.
1.146 -
1.147 -\nopagebreak
1.148 -{\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.149 -
1.150 -\opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.151 -Specifies the default sequence of cardinalities to use. This can be overridden
1.152 -on a per-type basis using the \textit{card}~\qty{type} option described above.
1.153 -
1.154 -\opu{max}{const}{int\_seq}
1.155 -Specifies the sequence of maximum multiplicities to use for a given
1.156 -(co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1.157 -number of distinct values that it can construct. Nonsensical values (e.g.,
1.158 -\textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1.159 -datatypes equipped with several constructors.
1.160 -
1.161 -\ops{max}{int\_seq}
1.162 -Specifies the default sequence of maximum multiplicities to use for
1.163 -(co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1.164 -basis using the \textit{max}~\qty{const} option described above.
1.165 +In binary mode, the cardinality specifies the number of distinct values that can
1.166 +be constructed. Each of these value is represented by a bit pattern whose length
1.167 +is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
1.168 +Nitpick attempts to choose the more appropriate encoding by inspecting the
1.169 +formula at hand, preferring the binary notation for problems involving
1.170 +multiplicative operators or large constants.
1.171 +
1.172 +\textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
1.173 +problems that refer to the types \textit{rat} or \textit{real} or the constants
1.174 +\textit{gcd} or \textit{lcm}.
1.175 +
1.176 +{\small See also \textit{bits} (\S\ref{scope-of-search}) and
1.177 +\textit{show\_datatypes} (\S\ref{output-format}).}
1.178 +
1.179 +\opt{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
1.180 +Specifies the number of bits to use to represent natural numbers and integers in
1.181 +binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
1.182 +
1.183 +{\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
1.184
1.185 \opusmart{wf}{const}{non\_wf}
1.186 Specifies whether the specified (co)in\-duc\-tively defined predicate is
2.1 --- a/src/HOL/Nitpick.thy Mon Dec 14 16:48:49 2009 +0100
2.2 +++ b/src/HOL/Nitpick.thy Thu Dec 17 15:22:11 2009 +0100
2.3 @@ -36,7 +36,12 @@
2.4 and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
2.5
2.6 datatype ('a, 'b) pair_box = PairBox 'a 'b
2.7 -datatype ('a, 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
2.8 +datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
2.9 +
2.10 +typedecl unsigned_bit
2.11 +typedecl signed_bit
2.12 +
2.13 +datatype 'a word = Word "('a set)"
2.14
2.15 text {*
2.16 Alternative definitions.
2.17 @@ -126,8 +131,6 @@
2.18
2.19 declare nat.cases [nitpick_simp del]
2.20
2.21 -lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
2.22 -
2.23 lemma list_size_simp [nitpick_simp]:
2.24 "list_size f xs = (if xs = [] then 0
2.25 else Suc (f (hd xs) + list_size f (tl xs)))"
2.26 @@ -244,11 +247,11 @@
2.27 setup {* Nitpick_Isar.setup *}
2.28
2.29 hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim
2.30 - bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
2.31 - fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
2.32 - one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
2.33 - number_of_frac inverse_frac less_eq_frac of_frac
2.34 -hide (open) type bisim_iterator pair_box fun_box
2.35 + bisim_iterator_max Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
2.36 + wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
2.37 + Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
2.38 + times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
2.39 +hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
2.40 hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
2.41 wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
2.42 The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
3.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Dec 14 16:48:49 2009 +0100
3.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Dec 17 15:22:11 2009 +0100
3.3 @@ -18,16 +18,16 @@
3.4 val def_table = Nitpick_HOL.const_def_table @{context} defs
3.5 val ext_ctxt : Nitpick_HOL.extended_context =
3.6 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
3.7 - user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false,
3.8 - specialize = false, skolemize = false, star_linear_preds = false,
3.9 - uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [],
3.10 - case_names = [], def_table = def_table, nondef_table = Symtab.empty,
3.11 - user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty,
3.12 - psimp_table = Symtab.empty, intro_table = Symtab.empty,
3.13 - ground_thm_table = Inttab.empty, ersatz_table = [],
3.14 - skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
3.15 - unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
3.16 - constr_cache = Unsynchronized.ref []}
3.17 + user_axioms = NONE, debug = false, wfs = [], binary_ints = SOME false,
3.18 + destroy_constrs = false, specialize = false, skolemize = false,
3.19 + star_linear_preds = false, uncurry = false, fast_descrs = false,
3.20 + tac_timeout = NONE, evals = [], case_names = [], def_table = def_table,
3.21 + nondef_table = Symtab.empty, user_nondefs = [],
3.22 + simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
3.23 + intro_table = Symtab.empty, ground_thm_table = Inttab.empty,
3.24 + ersatz_table = [], skolems = Unsynchronized.ref [],
3.25 + special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
3.26 + wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
3.27 (* term -> bool *)
3.28 val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] []
3.29 fun is_const t =
4.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Dec 14 16:48:49 2009 +0100
4.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Thu Dec 17 15:22:11 2009 +0100
4.3 @@ -135,7 +135,7 @@
4.4 lemma "\<forall>a. g a = a
4.5 \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
4.6 b\<^isub>1 < b\<^isub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x"
4.7 -nitpick [expect = potential]
4.8 +nitpick [expect = none]
4.9 nitpick [dont_specialize, expect = none]
4.10 nitpick [dont_box, expect = none]
4.11 nitpick [dont_box, dont_specialize, expect = none]
4.12 @@ -163,7 +163,7 @@
4.13 else
4.14 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
4.15 + h b\<^isub>9 + h b\<^isub>10) x"
4.16 -nitpick [card nat = 2, card 'a = 1, expect = none]
4.17 +nitpick [card nat = 2, card 'a = 1, expect = potential]
4.18 nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]
4.19 nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]
4.20 nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,
5.1 --- a/src/HOL/Tools/Nitpick/HISTORY Mon Dec 14 16:48:49 2009 +0100
5.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Thu Dec 17 15:22:11 2009 +0100
5.3 @@ -1,5 +1,6 @@
5.4 Version 2010
5.5
5.6 + * Added and implemented "binary_ints" and "bits" options
5.7 * Fixed soundness bug in "destroy_constrs" optimization
5.8
5.9 Version 2009-1
6.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Dec 14 16:48:49 2009 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Dec 17 15:22:11 2009 +0100
6.3 @@ -506,12 +506,13 @@
6.4 = filter (is_relevant_setting o fst) (#settings p2)
6.5
6.6 (* int -> string *)
6.7 -fun base_name j = if j < 0 then Int.toString (~j - 1) ^ "'" else Int.toString j
6.8 +fun base_name j =
6.9 + if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j
6.10
6.11 (* n_ary_index -> string -> string -> string -> string *)
6.12 fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j
6.13 | n_ary_name (2, j) _ prefix _ = prefix ^ base_name j
6.14 - | n_ary_name (n, j) _ _ prefix = prefix ^ Int.toString n ^ "_" ^ base_name j
6.15 + | n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j
6.16
6.17 (* int -> string *)
6.18 fun atom_name j = "A" ^ base_name j
6.19 @@ -574,7 +575,7 @@
6.20 sub ts1 prec ^ " - " ^ sub ts1 (prec + 1)
6.21 | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts1 prec
6.22 | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
6.23 - | TupleProject (ts, c) => sub ts prec ^ "[" ^ Int.toString c ^ "]"
6.24 + | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
6.25 | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
6.26 | TupleRange (t1, t2) =>
6.27 "{" ^ string_for_tuple t1 ^
6.28 @@ -602,7 +603,7 @@
6.29 (* int_bound -> string *)
6.30 fun int_string_for_bound (opt_n, tss) =
6.31 (case opt_n of
6.32 - SOME n => Int.toString n ^ ": "
6.33 + SOME n => signed_string_of_int n ^ ": "
6.34 | NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]"
6.35
6.36 val prec_All = 1
6.37 @@ -823,7 +824,7 @@
6.38 | Neg i => (out "-"; out_i i prec)
6.39 | Absolute i => (out "abs "; out_i i prec)
6.40 | Signum i => (out "sgn "; out_i i prec)
6.41 - | Num k => out (Int.toString k)
6.42 + | Num k => out (signed_string_of_int k)
6.43 | IntReg j => out (int_reg_name j));
6.44 (if need_parens then out ")" else ())
6.45 end
6.46 @@ -1048,12 +1049,12 @@
6.47 \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
6.48 \$LD_LIBRARY_PATH\" \
6.49 \\"$KODKODI\"/bin/kodkodi" ^
6.50 - (if ms >= 0 then " -max-msecs " ^ Int.toString ms
6.51 + (if ms >= 0 then " -max-msecs " ^ string_of_int ms
6.52 else "") ^
6.53 (if max_solutions > 1 then " -solve-all" else "") ^
6.54 - " -max-solutions " ^ Int.toString max_solutions ^
6.55 + " -max-solutions " ^ string_of_int max_solutions ^
6.56 (if max_threads > 0 then
6.57 - " -max-threads " ^ Int.toString max_threads
6.58 + " -max-threads " ^ string_of_int max_threads
6.59 else
6.60 "") ^
6.61 " < " ^ Path.implode in_path ^
7.1 --- a/src/HOL/Tools/Nitpick/minipick.ML Mon Dec 14 16:48:49 2009 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Thu Dec 17 15:22:11 2009 +0100
7.3 @@ -314,7 +314,8 @@
7.4 bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
7.5 in
7.6 case solve_any_problem overlord NONE 0 1 [problem] of
7.7 - Normal ([], _) => "none"
7.8 + NotInstalled => "unknown"
7.9 + | Normal ([], _) => "none"
7.10 | Normal _ => "genuine"
7.11 | TimedOut _ => "unknown"
7.12 | Interrupted _ => "unknown"
8.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 14 16:48:49 2009 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Dec 17 15:22:11 2009 +0100
8.3 @@ -12,6 +12,7 @@
8.4 cards_assigns: (typ option * int list) list,
8.5 maxes_assigns: (styp option * int list) list,
8.6 iters_assigns: (styp option * int list) list,
8.7 + bitss: int list,
8.8 bisim_depths: int list,
8.9 boxes: (typ option * bool option) list,
8.10 monos: (typ option * bool option) list,
8.11 @@ -25,6 +26,7 @@
8.12 user_axioms: bool option,
8.13 assms: bool,
8.14 merge_type_vars: bool,
8.15 + binary_ints: bool option,
8.16 destroy_constrs: bool,
8.17 specialize: bool,
8.18 skolemize: bool,
8.19 @@ -77,6 +79,7 @@
8.20 cards_assigns: (typ option * int list) list,
8.21 maxes_assigns: (styp option * int list) list,
8.22 iters_assigns: (styp option * int list) list,
8.23 + bitss: int list,
8.24 bisim_depths: int list,
8.25 boxes: (typ option * bool option) list,
8.26 monos: (typ option * bool option) list,
8.27 @@ -90,6 +93,7 @@
8.28 user_axioms: bool option,
8.29 assms: bool,
8.30 merge_type_vars: bool,
8.31 + binary_ints: bool option,
8.32 destroy_constrs: bool,
8.33 specialize: bool,
8.34 skolemize: bool,
8.35 @@ -186,20 +190,21 @@
8.36 val nitpick_thy = ThyInfo.get_theory "Nitpick"
8.37 val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy))
8.38 val thy = if nitpick_thy_missing then
8.39 - Theory.begin_theory "Nitpick_Internal" [nitpick_thy, user_thy]
8.40 + Theory.begin_theory "Nitpick_Internal_Name_Do_Not_Use_XYZZY"
8.41 + [nitpick_thy, user_thy]
8.42 |> Theory.checkpoint
8.43 else
8.44 user_thy
8.45 val ctxt = Proof.context_of state
8.46 |> nitpick_thy_missing ? Context.raw_transfer thy
8.47 - val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
8.48 - monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
8.49 - user_axioms, assms, merge_type_vars, destroy_constrs, specialize,
8.50 - skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim,
8.51 - tac_timeout, sym_break, sharing_depth, flatten_props, max_threads,
8.52 - show_skolems, show_datatypes, show_consts, evals, formats,
8.53 - max_potential, max_genuine, check_potential, check_genuine, batch_size,
8.54 - ...} =
8.55 + val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
8.56 + boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose,
8.57 + overlord, user_axioms, assms, merge_type_vars, binary_ints,
8.58 + destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
8.59 + fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
8.60 + flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
8.61 + evals, formats, max_potential, max_genuine, check_potential,
8.62 + check_genuine, batch_size, ...} =
8.63 params
8.64 val state_ref = Unsynchronized.ref state
8.65 (* Pretty.T -> unit *)
8.66 @@ -260,10 +265,11 @@
8.67 val (ext_ctxt as {wf_cache, ...}) =
8.68 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
8.69 user_axioms = user_axioms, debug = debug, wfs = wfs,
8.70 - destroy_constrs = destroy_constrs, specialize = specialize,
8.71 - skolemize = skolemize, star_linear_preds = star_linear_preds,
8.72 - uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout,
8.73 - evals = evals, case_names = case_names, def_table = def_table,
8.74 + binary_ints = binary_ints, destroy_constrs = destroy_constrs,
8.75 + specialize = specialize, skolemize = skolemize,
8.76 + star_linear_preds = star_linear_preds, uncurry = uncurry,
8.77 + fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
8.78 + case_names = case_names, def_table = def_table,
8.79 nondef_table = nondef_table, user_nondefs = user_nondefs,
8.80 simp_table = simp_table, psimp_table = psimp_table,
8.81 intro_table = intro_table, ground_thm_table = ground_thm_table,
8.82 @@ -321,19 +327,27 @@
8.83 unique_scope orelse
8.84 case triple_lookup (type_match thy) monos T of
8.85 SOME (SOME b) => b
8.86 - | _ => formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
8.87 + | _ => is_bit_type T
8.88 + orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
8.89 fun is_datatype_monotonic T =
8.90 unique_scope orelse
8.91 case triple_lookup (type_match thy) monos T of
8.92 SOME (SOME b) => b
8.93 - | _ =>
8.94 - not (is_pure_typedef thy T) orelse is_univ_typedef thy T
8.95 - orelse is_number_type thy T
8.96 - orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
8.97 - fun is_datatype_shallow T =
8.98 - not (exists (curry (op =) T o domain_type o type_of) sel_names)
8.99 + | _ => not (is_pure_typedef thy T) orelse is_univ_typedef thy T
8.100 + orelse is_number_type thy T
8.101 + orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
8.102 + fun is_datatype_deep T =
8.103 + is_word_type T
8.104 + orelse exists (curry (op =) T o domain_type o type_of) sel_names
8.105 val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
8.106 |> sort TermOrd.typ_ord
8.107 + val _ = if verbose andalso binary_ints = SOME true
8.108 + andalso exists (member (op =) [nat_T, int_T]) Ts then
8.109 + print_v (K "The option \"binary_ints\" will be ignored because \
8.110 + \of the presence of rationals, reals, \"gcd\", or \
8.111 + \\"lcm\" in the problem.")
8.112 + else
8.113 + ()
8.114 val (all_dataTs, all_free_Ts) =
8.115 List.partition (is_integer_type orf is_datatype thy) Ts
8.116 val (mono_dataTs, nonmono_dataTs) =
8.117 @@ -341,11 +355,13 @@
8.118 val (mono_free_Ts, nonmono_free_Ts) =
8.119 List.partition is_free_type_monotonic all_free_Ts
8.120
8.121 + val interesting_mono_free_Ts = filter_out is_bit_type mono_free_Ts
8.122 val _ =
8.123 - if not unique_scope andalso not (null mono_free_Ts) then
8.124 + if not unique_scope andalso not (null interesting_mono_free_Ts) then
8.125 print_v (fn () =>
8.126 let
8.127 - val ss = map (quote o string_for_type ctxt) mono_free_Ts
8.128 + val ss = map (quote o string_for_type ctxt)
8.129 + interesting_mono_free_Ts
8.130 in
8.131 "The type" ^ plural_s_for_list ss ^ " " ^
8.132 space_implode " " (serial_commas "and" ss) ^ " " ^
8.133 @@ -360,7 +376,7 @@
8.134 ()
8.135 val mono_Ts = mono_dataTs @ mono_free_Ts
8.136 val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
8.137 - val shallow_dataTs = filter is_datatype_shallow mono_dataTs
8.138 + val shallow_dataTs = filter_out is_datatype_deep mono_dataTs
8.139 (*
8.140 val _ = priority "Monotonic datatypes:"
8.141 val _ = List.app (priority o string_for_type ctxt) mono_dataTs
8.142 @@ -400,12 +416,12 @@
8.143
8.144 (* bool -> scope -> rich_problem option *)
8.145 fun problem_for_scope liberal
8.146 - (scope as {card_assigns, bisim_depth, datatypes, ofs, ...}) =
8.147 + (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
8.148 let
8.149 val _ = not (exists (fn other => scope_less_eq other scope)
8.150 (!too_big_scopes))
8.151 - orelse raise LIMIT ("Nitpick.pick_them_nits_in_term.\
8.152 - \problem_for_scope", "too big scope")
8.153 + orelse raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
8.154 + \problem_for_scope", "too large scope")
8.155 (*
8.156 val _ = priority "Offsets:"
8.157 val _ = List.app (fn (T, j0) =>
8.158 @@ -454,7 +470,7 @@
8.159 val def_us = map (rename_vars_in_nut pool rel_table) def_us
8.160 val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
8.161 (* nut -> Kodkod.formula *)
8.162 - val to_f = kodkod_formula_from_nut ofs liberal kk
8.163 + val to_f = kodkod_formula_from_nut bits ofs liberal kk
8.164 val core_f = to_f core_u
8.165 val def_fs = map to_f def_us
8.166 val nondef_fs = map to_f nondef_us
8.167 @@ -463,6 +479,7 @@
8.168 PrintMode.setmp [] multiline_string_for_scope scope
8.169 val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver
8.170 |> snd
8.171 + val bit_width = if bits = 0 then 16 else bits + 1
8.172 val delay = if liberal then
8.173 Option.map (fn time => Time.- (time, Time.now ()))
8.174 deadline
8.175 @@ -471,7 +488,7 @@
8.176 0
8.177 val settings = [("solver", commas (map quote kodkod_sat_solver)),
8.178 ("skolem_depth", "-1"),
8.179 - ("bit_width", "16"),
8.180 + ("bit_width", string_of_int bit_width),
8.181 ("symmetry_breaking", signed_string_of_int sym_break),
8.182 ("sharing", signed_string_of_int sharing_depth),
8.183 ("flatten", Bool.toString flatten_props),
8.184 @@ -480,7 +497,7 @@
8.185 val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
8.186 val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
8.187 val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
8.188 - val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt ofs kk
8.189 + val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk
8.190 rel_table datatypes
8.191 val declarative_axioms = plain_axioms @ dtype_axioms
8.192 val univ_card = univ_card nat_card int_card main_j0
8.193 @@ -492,35 +509,44 @@
8.194 val highest_arity =
8.195 fold Integer.max (map (fst o fst) (maps fst bounds)) 0
8.196 val formula = fold_rev s_and declarative_axioms formula
8.197 + val _ = if bits = 0 then () else check_bits bits formula
8.198 val _ = if formula = Kodkod.False then ()
8.199 else check_arity univ_card highest_arity
8.200 in
8.201 SOME ({comment = comment, settings = settings, univ_card = univ_card,
8.202 tuple_assigns = [], bounds = bounds,
8.203 - int_bounds = sequential_int_bounds univ_card,
8.204 + int_bounds =
8.205 + if bits = 0 then sequential_int_bounds univ_card
8.206 + else pow_of_two_int_bounds bits main_j0 univ_card,
8.207 expr_assigns = [], formula = formula},
8.208 {free_names = free_names, sel_names = sel_names,
8.209 nonsel_names = nonsel_names, rel_table = rel_table,
8.210 liberal = liberal, scope = scope, core = core_f,
8.211 defs = nondef_fs @ def_fs @ declarative_axioms})
8.212 end
8.213 - handle LIMIT (loc, msg) =>
8.214 + handle TOO_LARGE (loc, msg) =>
8.215 if loc = "Nitpick_Kodkod.check_arity"
8.216 andalso not (Typtab.is_empty ofs) then
8.217 problem_for_scope liberal
8.218 {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
8.219 - bisim_depth = bisim_depth, datatypes = datatypes,
8.220 - ofs = Typtab.empty}
8.221 + bits = bits, bisim_depth = bisim_depth,
8.222 + datatypes = datatypes, ofs = Typtab.empty}
8.223 else if loc = "Nitpick.pick_them_nits_in_term.\
8.224 \problem_for_scope" then
8.225 NONE
8.226 else
8.227 (Unsynchronized.change too_big_scopes (cons scope);
8.228 print_v (fn () => ("Limit reached: " ^ msg ^
8.229 - ". Dropping " ^ (if liberal then "potential"
8.230 + ". Skipping " ^ (if liberal then "potential"
8.231 else "genuine") ^
8.232 " component of scope."));
8.233 NONE)
8.234 + | TOO_SMALL (loc, msg) =>
8.235 + (print_v (fn () => ("Limit reached: " ^ msg ^
8.236 + ". Skipping " ^ (if liberal then "potential"
8.237 + else "genuine") ^
8.238 + " component of scope."));
8.239 + NONE)
8.240
8.241 (* int -> (''a * int list list) list -> ''a -> Kodkod.tuple_set *)
8.242 fun tuple_set_for_rel univ_card =
8.243 @@ -809,7 +835,7 @@
8.244 (* int -> int -> scope list -> int * int * int -> Kodkod.outcome *)
8.245 fun run_batches _ _ [] (max_potential, max_genuine, donno) =
8.246 if donno > 0 andalso max_genuine > 0 then
8.247 - (print_m (fn () => excipit "ran out of juice"); "unknown")
8.248 + (print_m (fn () => excipit "ran out of some resource"); "unknown")
8.249 else if max_genuine = original_max_genuine then
8.250 if max_potential = original_max_potential then
8.251 (print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")
8.252 @@ -827,9 +853,9 @@
8.253
8.254 val (skipped, the_scopes) =
8.255 all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
8.256 - bisim_depths mono_Ts nonmono_Ts shallow_dataTs
8.257 + bitss bisim_depths mono_Ts nonmono_Ts shallow_dataTs
8.258 val _ = if skipped > 0 then
8.259 - print_m (fn () => "Too many scopes. Dropping " ^
8.260 + print_m (fn () => "Too many scopes. Skipping " ^
8.261 string_of_int skipped ^ " scope" ^
8.262 plural_s skipped ^
8.263 ". (Consider using \"mono\" or \
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Dec 14 16:48:49 2009 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 17 15:22:11 2009 +0100
9.3 @@ -21,6 +21,7 @@
9.4 wfs: (styp option * bool option) list,
9.5 user_axioms: bool option,
9.6 debug: bool,
9.7 + binary_ints: bool option,
9.8 destroy_constrs: bool,
9.9 specialize: bool,
9.10 skolemize: bool,
9.11 @@ -49,7 +50,7 @@
9.12 val skolem_prefix : string
9.13 val eval_prefix : string
9.14 val original_name : string -> string
9.15 - val unbox_type : typ -> typ
9.16 + val unbit_and_unbox_type : typ -> typ
9.17 val string_for_type : Proof.context -> typ -> string
9.18 val prefix_name : string -> string -> string
9.19 val shortest_name : string -> string
9.20 @@ -68,6 +69,8 @@
9.21 val is_fp_iterator_type : typ -> bool
9.22 val is_boolean_type : typ -> bool
9.23 val is_integer_type : typ -> bool
9.24 + val is_bit_type : typ -> bool
9.25 + val is_word_type : typ -> bool
9.26 val is_record_type : typ -> bool
9.27 val is_number_type : theory -> typ -> bool
9.28 val const_for_iterator_type : typ -> styp
9.29 @@ -91,6 +94,7 @@
9.30 val is_constr : theory -> styp -> bool
9.31 val is_stale_constr : theory -> styp -> bool
9.32 val is_sel : string -> bool
9.33 + val is_sel_like_and_no_discr : string -> bool
9.34 val discr_for_constr : styp -> styp
9.35 val num_sels_for_constr_type : typ -> int
9.36 val nth_sel_name_for_constr_name : string -> int -> string
9.37 @@ -161,6 +165,7 @@
9.38 wfs: (styp option * bool option) list,
9.39 user_axioms: bool option,
9.40 debug: bool,
9.41 + binary_ints: bool option,
9.42 destroy_constrs: bool,
9.43 specialize: bool,
9.44 skolemize: bool,
9.45 @@ -307,7 +312,6 @@
9.46 (@{const_name minus_nat_inst.minus_nat}, 0),
9.47 (@{const_name times_nat_inst.times_nat}, 0),
9.48 (@{const_name div_nat_inst.div_nat}, 0),
9.49 - (@{const_name div_nat_inst.mod_nat}, 0),
9.50 (@{const_name ord_nat_inst.less_nat}, 2),
9.51 (@{const_name ord_nat_inst.less_eq_nat}, 2),
9.52 (@{const_name nat_gcd}, 0),
9.53 @@ -318,7 +322,6 @@
9.54 (@{const_name minus_int_inst.minus_int}, 0),
9.55 (@{const_name times_int_inst.times_int}, 0),
9.56 (@{const_name div_int_inst.div_int}, 0),
9.57 - (@{const_name div_int_inst.mod_int}, 0),
9.58 (@{const_name uminus_int_inst.uminus_int}, 0),
9.59 (@{const_name ord_int_inst.less_int}, 2),
9.60 (@{const_name ord_int_inst.less_eq_int}, 2),
9.61 @@ -329,7 +332,8 @@
9.62 [(@{const_name The}, 1),
9.63 (@{const_name Eps}, 1)]
9.64 val built_in_typed_consts =
9.65 - [((@{const_name of_nat}, nat_T --> int_T), 0)]
9.66 + [((@{const_name of_nat}, nat_T --> int_T), 0),
9.67 + ((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)]
9.68 val built_in_set_consts =
9.69 [(@{const_name lower_semilattice_fun_inst.inf_fun}, 2),
9.70 (@{const_name upper_semilattice_fun_inst.sup_fun}, 2),
9.71 @@ -337,14 +341,23 @@
9.72 (@{const_name ord_fun_inst.less_eq_fun}, 2)]
9.73
9.74 (* typ -> typ *)
9.75 -fun unbox_type (Type (@{type_name fun_box}, Ts)) =
9.76 - Type ("fun", map unbox_type Ts)
9.77 - | unbox_type (Type (@{type_name pair_box}, Ts)) =
9.78 - Type ("*", map unbox_type Ts)
9.79 - | unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts)
9.80 - | unbox_type T = T
9.81 +fun unbit_type @{typ "unsigned_bit word"} = nat_T
9.82 + | unbit_type @{typ "signed_bit word"} = int_T
9.83 + | unbit_type @{typ bisim_iterator} = nat_T
9.84 + | unbit_type (Type (s, Ts as _ :: _)) = Type (s, map unbit_type Ts)
9.85 + | unbit_type T = T
9.86 +fun unbit_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
9.87 + unbit_and_unbox_type (Type ("fun", Ts))
9.88 + | unbit_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
9.89 + Type ("*", map unbit_and_unbox_type Ts)
9.90 + | unbit_and_unbox_type @{typ "unsigned_bit word"} = nat_T
9.91 + | unbit_and_unbox_type @{typ "signed_bit word"} = int_T
9.92 + | unbit_and_unbox_type @{typ bisim_iterator} = nat_T
9.93 + | unbit_and_unbox_type (Type (s, Ts as _ :: _)) =
9.94 + Type (s, map unbit_and_unbox_type Ts)
9.95 + | unbit_and_unbox_type T = T
9.96 (* Proof.context -> typ -> string *)
9.97 -fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type
9.98 +fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type
9.99
9.100 (* string -> string -> string *)
9.101 val prefix_name = Long_Name.qualify o Long_Name.base_name
9.102 @@ -401,6 +414,9 @@
9.103 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
9.104 val is_integer_type =
9.105 member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
9.106 +fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
9.107 +fun is_word_type (Type (@{type_name word}, _)) = true
9.108 + | is_word_type _ = false
9.109 val is_record_type = not o null o Record.dest_recTs
9.110 (* theory -> typ -> bool *)
9.111 fun is_frac_type thy (Type (s, [])) =
9.112 @@ -454,17 +470,6 @@
9.113 | dest_n_tuple_type _ T =
9.114 raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
9.115
9.116 -(* (typ * typ) list -> typ -> typ *)
9.117 -fun typ_subst [] T = T
9.118 - | typ_subst ps T =
9.119 - let
9.120 - (* typ -> typ *)
9.121 - fun subst T =
9.122 - case AList.lookup (op =) ps T of
9.123 - SOME T' => T'
9.124 - | NONE => case T of Type (s, Ts) => Type (s, map subst Ts) | _ => T
9.125 - in subst T end
9.126 -
9.127 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
9.128 e.g., by adding a field to "Datatype_Aux.info". *)
9.129 (* string -> bool *)
9.130 @@ -622,7 +627,7 @@
9.131 handle TYPE ("dest_Type", _, _) => false
9.132 fun is_constr_like thy (s, T) =
9.133 s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
9.134 - let val (x as (s, T)) = (s, unbox_type T) in
9.135 + let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
9.136 Refute.is_IDT_constructor thy x orelse is_record_constr x
9.137 orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
9.138 orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep}
9.139 @@ -634,7 +639,7 @@
9.140 andalso not (is_coconstr thy x)
9.141 fun is_constr thy (x as (_, T)) =
9.142 is_constr_like thy x
9.143 - andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
9.144 + andalso not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T)))))
9.145 andalso not (is_stale_constr thy x)
9.146 (* string -> bool *)
9.147 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
9.148 @@ -886,7 +891,7 @@
9.149 val x' as (_, T') =
9.150 if is_pair_type T then
9.151 let val (T1, T2) = HOLogic.dest_prodT T in
9.152 - (@{const_name Pair}, [T1, T2] ---> T)
9.153 + (@{const_name Pair}, T1 --> T2 --> T)
9.154 end
9.155 else
9.156 datatype_constrs ext_ctxt T |> the_single
9.157 @@ -1215,7 +1220,7 @@
9.158
9.159 (* Proof.context -> term list -> const_table *)
9.160 fun const_def_table ctxt ts =
9.161 - table_for (map prop_of o Nitpick_Defs.get) ctxt
9.162 + table_for (rev o map prop_of o Nitpick_Defs.get) ctxt
9.163 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
9.164 (map pair_for_prop ts)
9.165 (* term list -> const_table *)
9.166 @@ -1324,7 +1329,7 @@
9.167 end
9.168 (* extended_context -> typ -> int * styp -> term -> term *)
9.169 fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
9.170 - Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
9.171 + Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
9.172 $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
9.173 $ res_t
9.174 (* extended_context -> typ -> typ -> term *)
9.175 @@ -1555,10 +1560,10 @@
9.176 else case def_of_const thy def_table x of
9.177 SOME def =>
9.178 if depth > unfold_max_depth then
9.179 - raise LIMIT ("Nitpick_HOL.unfold_defs_in_term",
9.180 - "too many nested definitions (" ^
9.181 - string_of_int depth ^ ") while expanding " ^
9.182 - quote s)
9.183 + raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
9.184 + "too many nested definitions (" ^
9.185 + string_of_int depth ^ ") while expanding " ^
9.186 + quote s)
9.187 else if s = @{const_name wfrec'} then
9.188 (do_term (depth + 1) Ts (betapplys (def, ts)), [])
9.189 else
9.190 @@ -1573,7 +1578,7 @@
9.191 val xs = datatype_constrs ext_ctxt T
9.192 val set_T = T --> bool_T
9.193 val iter_T = @{typ bisim_iterator}
9.194 - val bisim_const = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
9.195 + val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
9.196 val bisim_max = @{const bisim_iterator_max}
9.197 val n_var = Var (("n", 0), iter_T)
9.198 val n_var_minus_1 =
9.199 @@ -1603,7 +1608,7 @@
9.200 $ (betapplys (optimized_case_def ext_ctxt T bool_T,
9.201 map case_func xs @ [x_var]))),
9.202 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
9.203 - $ (Const (@{const_name insert}, [T, set_T] ---> set_T)
9.204 + $ (Const (@{const_name insert}, T --> set_T --> set_T)
9.205 $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
9.206 |> map HOLogic.mk_Trueprop
9.207 end
9.208 @@ -2064,7 +2069,7 @@
9.209 let val arg_Ts = binder_types T in
9.210 if length arg_Ts = length args
9.211 andalso (is_constr thy x orelse s = @{const_name Pair}
9.212 - orelse x = dest_Const @{const Suc})
9.213 + orelse x = (@{const_name Suc}, nat_T --> nat_T))
9.214 andalso (not careful orelse not (is_Var t1)
9.215 orelse String.isPrefix val_var_prefix
9.216 (fst (fst (dest_Var t1)))) then
9.217 @@ -2496,7 +2501,7 @@
9.218 map Bound (length trunk_arg_Ts - 1 downto 0))
9.219 in
9.220 List.foldr absdummy
9.221 - (Const (set_oper, [set_T, set_T] ---> set_T)
9.222 + (Const (set_oper, set_T --> set_T --> set_T)
9.223 $ app pos $ app neg) trunk_arg_Ts
9.224 end
9.225 else
9.226 @@ -2833,7 +2838,7 @@
9.227 val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
9.228 val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
9.229 in
9.230 - list_comb (Const (s0, [T, T] ---> body_type T0),
9.231 + list_comb (Const (s0, T --> T --> body_type T0),
9.232 map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
9.233 end
9.234 (* string -> typ -> term *)
9.235 @@ -3050,9 +3055,10 @@
9.236 else
9.237 let val accum as (xs, _) = (x :: xs, axs) in
9.238 if depth > axioms_max_depth then
9.239 - raise LIMIT ("Nitpick_HOL.axioms_for_term.add_axioms_for_term",
9.240 - "too many nested axioms (" ^ string_of_int depth ^
9.241 - ")")
9.242 + raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\
9.243 + \add_axioms_for_term",
9.244 + "too many nested axioms (" ^
9.245 + string_of_int depth ^ ")")
9.246 else if Refute.is_const_of_class thy x then
9.247 let
9.248 val class = Logic.class_of_const s
9.249 @@ -3195,7 +3201,7 @@
9.250 (* int list -> int list -> typ -> typ *)
9.251 fun format_type default_format format T =
9.252 let
9.253 - val T = unbox_type T
9.254 + val T = unbit_and_unbox_type T
9.255 val format = format |> filter (curry (op <) 0)
9.256 in
9.257 if forall (curry (op =) 1) format then
9.258 @@ -3234,7 +3240,8 @@
9.259 (* term -> term *)
9.260 val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
9.261 val (x' as (_, T'), js, ts) =
9.262 - AList.find (op =) (!special_funs) (s, unbox_type T) |> the_single
9.263 + AList.find (op =) (!special_funs) (s, unbit_and_unbox_type T)
9.264 + |> the_single
9.265 val max_j = List.last js
9.266 val Ts = List.take (binder_types T', max_j + 1)
9.267 val missing_js = filter_out (member (op =) js) (0 upto max_j)
9.268 @@ -3323,7 +3330,7 @@
9.269 let val t = Const (original_name s, T) in
9.270 (t, format_term_type thy def_table formats t)
9.271 end)
9.272 - |>> map_types (typ_subst [(@{typ bisim_iterator}, nat_T)] o unbox_type)
9.273 + |>> map_types unbit_and_unbox_type
9.274 |>> shorten_names_in_term |>> shorten_abs_vars
9.275 in do_const end
9.276
9.277 @@ -3338,10 +3345,45 @@
9.278 else
9.279 "="
9.280
9.281 +val binary_int_threshold = 4
9.282 +
9.283 +(* term -> bool *)
9.284 +fun may_use_binary_ints (t1 $ t2) =
9.285 + may_use_binary_ints t1 andalso may_use_binary_ints t2
9.286 + | may_use_binary_ints (Const (s, _)) =
9.287 + not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
9.288 + @{const_name Frac}, @{const_name norm_frac},
9.289 + @{const_name nat_gcd}, @{const_name nat_lcm}] s)
9.290 + | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
9.291 + | may_use_binary_ints _ = true
9.292 +
9.293 +fun should_use_binary_ints (t1 $ t2) =
9.294 + should_use_binary_ints t1 orelse should_use_binary_ints t2
9.295 + | should_use_binary_ints (Const (s, _)) =
9.296 + member (op =) [@{const_name times_nat_inst.times_nat},
9.297 + @{const_name div_nat_inst.div_nat},
9.298 + @{const_name times_int_inst.times_int},
9.299 + @{const_name div_int_inst.div_int}] s
9.300 + orelse (String.isPrefix numeral_prefix s andalso
9.301 + let val n = the (Int.fromString (unprefix numeral_prefix s)) in
9.302 + n <= ~ binary_int_threshold orelse n >= binary_int_threshold
9.303 + end)
9.304 + | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
9.305 + | should_use_binary_ints _ = false
9.306 +
9.307 +(* typ -> typ *)
9.308 +fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
9.309 + | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
9.310 + | binarize_nat_and_int_in_type (Type (s, Ts)) =
9.311 + Type (s, map binarize_nat_and_int_in_type Ts)
9.312 + | binarize_nat_and_int_in_type T = T
9.313 +(* term -> term *)
9.314 +val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
9.315 +
9.316 (* extended_context -> term
9.317 -> ((term list * term list) * (bool * bool)) * term *)
9.318 -fun preprocess_term (ext_ctxt as {thy, destroy_constrs, boxes, skolemize,
9.319 - uncurry, ...}) t =
9.320 +fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes,
9.321 + skolemize, uncurry, ...}) t =
9.322 let
9.323 val skolem_depth = if skolemize then 4 else ~1
9.324 val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
9.325 @@ -3350,14 +3392,22 @@
9.326 |> skolemize_term_and_more ext_ctxt skolem_depth
9.327 |> specialize_consts_in_term ext_ctxt 0
9.328 |> `(axioms_for_term ext_ctxt)
9.329 - val maybe_box = exists (not_equal (SOME false) o snd) boxes
9.330 + val binarize =
9.331 + case binary_ints of
9.332 + SOME false => false
9.333 + | _ =>
9.334 + forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
9.335 + (binary_ints = SOME true
9.336 + orelse exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
9.337 + val box = exists (not_equal (SOME false) o snd) boxes
9.338 val table =
9.339 Termtab.empty |> uncurry
9.340 ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
9.341 (* bool -> bool -> term -> term *)
9.342 fun do_rest def core =
9.343 - uncurry ? uncurry_term table
9.344 - #> maybe_box ? box_fun_and_pair_in_term ext_ctxt def
9.345 + binarize ? binarize_nat_and_int_in_term
9.346 + #> uncurry ? uncurry_term table
9.347 + #> box ? box_fun_and_pair_in_term ext_ctxt def
9.348 #> destroy_constrs ? (pull_out_universal_constrs thy def
9.349 #> pull_out_existential_constrs thy
9.350 #> destroy_pulled_out_constrs ext_ctxt def)
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Dec 14 16:48:49 2009 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Dec 17 15:22:11 2009 +0100
10.3 @@ -37,6 +37,7 @@
10.4 val default_default_params =
10.5 [("card", ["1\<midarrow>8"]),
10.6 ("iter", ["0,1,2,4,8,12,16,24"]),
10.7 + ("bits", ["1,2,3,4,6,8,10,12"]),
10.8 ("bisim_depth", ["7"]),
10.9 ("box", ["smart"]),
10.10 ("mono", ["smart"]),
10.11 @@ -48,6 +49,7 @@
10.12 ("user_axioms", ["smart"]),
10.13 ("assms", ["true"]),
10.14 ("merge_type_vars", ["false"]),
10.15 + ("binary_ints", ["smart"]),
10.16 ("destroy_constrs", ["true"]),
10.17 ("specialize", ["true"]),
10.18 ("skolemize", ["true"]),
10.19 @@ -83,6 +85,7 @@
10.20 ("no_user_axioms", "user_axioms"),
10.21 ("no_assms", "assms"),
10.22 ("dont_merge_type_vars", "merge_type_vars"),
10.23 + ("unary_ints", "binary_ints"),
10.24 ("dont_destroy_constrs", "destroy_constrs"),
10.25 ("dont_specialize", "specialize"),
10.26 ("dont_skolemize", "skolemize"),
10.27 @@ -283,6 +286,7 @@
10.28 val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
10.29 val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
10.30 val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
10.31 + val bitss = lookup_int_seq "bits" 1
10.32 val bisim_depths = lookup_int_seq "bisim_depth" ~1
10.33 val boxes =
10.34 lookup_bool_option_assigns read_type_polymorphic "box" @
10.35 @@ -303,6 +307,7 @@
10.36 val user_axioms = lookup_bool_option "user_axioms"
10.37 val assms = lookup_bool "assms"
10.38 val merge_type_vars = lookup_bool "merge_type_vars"
10.39 + val binary_ints = lookup_bool_option "binary_ints"
10.40 val destroy_constrs = lookup_bool "destroy_constrs"
10.41 val specialize = lookup_bool "specialize"
10.42 val skolemize = lookup_bool "skolemize"
10.43 @@ -333,15 +338,16 @@
10.44 val expect = lookup_string "expect"
10.45 in
10.46 {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
10.47 - iters_assigns = iters_assigns, bisim_depths = bisim_depths, boxes = boxes,
10.48 - monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
10.49 - falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
10.50 - user_axioms = user_axioms, assms = assms,
10.51 - merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs,
10.52 - specialize = specialize, skolemize = skolemize,
10.53 - star_linear_preds = star_linear_preds, uncurry = uncurry,
10.54 - fast_descrs = fast_descrs, peephole_optim = peephole_optim,
10.55 - timeout = timeout, tac_timeout = tac_timeout, sym_break = sym_break,
10.56 + iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
10.57 + boxes = boxes, monos = monos, wfs = wfs, sat_solver = sat_solver,
10.58 + blocking = blocking, falsify = falsify, debug = debug, verbose = verbose,
10.59 + overlord = overlord, user_axioms = user_axioms, assms = assms,
10.60 + merge_type_vars = merge_type_vars, binary_ints = binary_ints,
10.61 + destroy_constrs = destroy_constrs, specialize = specialize,
10.62 + skolemize = skolemize, star_linear_preds = star_linear_preds,
10.63 + uncurry = uncurry, fast_descrs = fast_descrs,
10.64 + peephole_optim = peephole_optim, timeout = timeout,
10.65 + tac_timeout = tac_timeout, sym_break = sym_break,
10.66 sharing_depth = sharing_depth, flatten_props = flatten_props,
10.67 max_threads = max_threads, show_skolems = show_skolems,
10.68 show_datatypes = show_datatypes, show_consts = show_consts,
10.69 @@ -379,8 +385,6 @@
10.70 error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
10.71 | BAD (loc, details) =>
10.72 error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
10.73 - | LIMIT (_, details) =>
10.74 - (warning ("Limit reached: " ^ details ^ "."); x)
10.75 | NOT_SUPPORTED details =>
10.76 (warning ("Unsupported case: " ^ details ^ "."); x)
10.77 | NUT (loc, us) =>
10.78 @@ -394,6 +398,10 @@
10.79 error ("Invalid term" ^ plural_s_for_list ts ^
10.80 " (" ^ quote loc ^ "): " ^
10.81 commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
10.82 + | TOO_LARGE (_, details) =>
10.83 + (warning ("Limit reached: " ^ details ^ "."); x)
10.84 + | TOO_SMALL (_, details) =>
10.85 + (warning ("Limit reached: " ^ details ^ "."); x)
10.86 | TYPE (loc, Ts, ts) =>
10.87 error ("Invalid type" ^ plural_s_for_list Ts ^
10.88 (if null ts then
11.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Dec 14 16:48:49 2009 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Dec 17 15:22:11 2009 +0100
11.3 @@ -19,10 +19,12 @@
11.4
11.5 val univ_card :
11.6 int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int
11.7 + val check_bits : int -> Kodkod.formula -> unit
11.8 val check_arity : int -> int -> unit
11.9 val kk_tuple : bool -> int -> int list -> Kodkod.tuple
11.10 val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
11.11 val sequential_int_bounds : int -> Kodkod.int_bound list
11.12 + val pow_of_two_int_bounds : int -> int -> int -> Kodkod.int_bound list
11.13 val bounds_for_built_in_rels_in_formula :
11.14 bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list
11.15 val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
11.16 @@ -31,10 +33,10 @@
11.17 val merge_bounds : Kodkod.bound list -> Kodkod.bound list
11.18 val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
11.19 val declarative_axioms_for_datatypes :
11.20 - extended_context -> int Typtab.table -> kodkod_constrs
11.21 + extended_context -> int -> int Typtab.table -> kodkod_constrs
11.22 -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
11.23 val kodkod_formula_from_nut :
11.24 - int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
11.25 + int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
11.26 end;
11.27
11.28 structure Nitpick_Kodkod : NITPICK_KODKOD =
11.29 @@ -80,18 +82,28 @@
11.30 |> Kodkod.fold_formula expr_F formula
11.31 in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end
11.32
11.33 -(* Proof.context -> bool -> string -> typ -> rep -> string *)
11.34 -fun bound_comment ctxt debug nick T R =
11.35 - short_name nick ^
11.36 - (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
11.37 - else "") ^ " : " ^ string_for_rep R
11.38 +(* int -> Kodkod.formula -> unit *)
11.39 +fun check_bits bits formula =
11.40 + let
11.41 + (* Kodkod.int_expr -> unit -> unit *)
11.42 + fun int_expr_func (Kodkod.Num k) () =
11.43 + if is_twos_complement_representable bits k then
11.44 + ()
11.45 + else
11.46 + raise TOO_SMALL ("Nitpick_Kodkod.check_bits",
11.47 + "\"bits\" value " ^ string_of_int bits ^
11.48 + " too small for problem")
11.49 + | int_expr_func _ () = ()
11.50 + val expr_F = {formula_func = K I, rel_expr_func = K I,
11.51 + int_expr_func = int_expr_func}
11.52 + in Kodkod.fold_formula expr_F formula () end
11.53
11.54 (* int -> int -> unit *)
11.55 fun check_arity univ_card n =
11.56 if n > Kodkod.max_arity univ_card then
11.57 - raise LIMIT ("Nitpick_Kodkod.check_arity",
11.58 - "arity " ^ string_of_int n ^ " too large for universe of \
11.59 - \cardinality " ^ string_of_int univ_card)
11.60 + raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
11.61 + "arity " ^ string_of_int n ^ " too large for universe of \
11.62 + \cardinality " ^ string_of_int univ_card)
11.63 else
11.64 ()
11.65
11.66 @@ -109,20 +121,34 @@
11.67 (* rep -> Kodkod.tuple_set *)
11.68 val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
11.69
11.70 +(* int -> Kodkod.tuple_set *)
11.71 +val single_atom = Kodkod.TupleSet o single o Kodkod.Tuple o single
11.72 (* int -> Kodkod.int_bound list *)
11.73 -fun sequential_int_bounds n =
11.74 - [(NONE, map (Kodkod.TupleSet o single o Kodkod.Tuple o single)
11.75 - (index_seq 0 n))]
11.76 +fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
11.77 +(* int -> int -> Kodkod.int_bound list *)
11.78 +fun pow_of_two_int_bounds bits j0 univ_card =
11.79 + let
11.80 + (* int -> int -> int -> Kodkod.int_bound list *)
11.81 + fun aux 0 _ _ = []
11.82 + | aux 1 pow_of_two j =
11.83 + if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else []
11.84 + | aux iter pow_of_two j =
11.85 + (SOME pow_of_two, [single_atom j]) ::
11.86 + aux (iter - 1) (2 * pow_of_two) (j + 1)
11.87 + in aux (bits + 1) 1 j0 end
11.88
11.89 (* Kodkod.formula -> Kodkod.n_ary_index list *)
11.90 fun built_in_rels_in_formula formula =
11.91 let
11.92 (* Kodkod.rel_expr -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list *)
11.93 - fun rel_expr_func (Kodkod.Rel (n, j)) rels =
11.94 - (case AList.lookup (op =) (#rels initial_pool) n of
11.95 - SOME k => (j < k ? insert (op =) (n, j)) rels
11.96 - | NONE => rels)
11.97 - | rel_expr_func _ rels = rels
11.98 + fun rel_expr_func (r as Kodkod.Rel (x as (n, j))) =
11.99 + if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
11.100 + I
11.101 + else
11.102 + (case AList.lookup (op =) (#rels initial_pool) n of
11.103 + SOME k => j < k ? insert (op =) x
11.104 + | NONE => I)
11.105 + | rel_expr_func _ = I
11.106 val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
11.107 int_expr_func = K I}
11.108 in Kodkod.fold_formula expr_F formula [] end
11.109 @@ -132,8 +158,8 @@
11.110 (* int -> unit *)
11.111 fun check_table_size k =
11.112 if k > max_table_size then
11.113 - raise LIMIT ("Nitpick_Kodkod.check_table_size",
11.114 - "precomputed table too large (" ^ string_of_int k ^ ")")
11.115 + raise TOO_LARGE ("Nitpick_Kodkod.check_table_size",
11.116 + "precomputed table too large (" ^ string_of_int k ^ ")")
11.117 else
11.118 ()
11.119
11.120 @@ -205,43 +231,39 @@
11.121 -> string * bool * Kodkod.tuple list *)
11.122 fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) =
11.123 (check_arity univ_card n;
11.124 - if Kodkod.Rel x = not3_rel then
11.125 + if x = not3_rel then
11.126 ("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
11.127 - else if Kodkod.Rel x = suc_rel then
11.128 + else if x = suc_rel then
11.129 ("suc", tabulate_func1 debug univ_card (univ_card - j0 - 1, j0)
11.130 (Integer.add 1))
11.131 - else if Kodkod.Rel x = nat_add_rel then
11.132 + else if x = nat_add_rel then
11.133 ("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +))
11.134 - else if Kodkod.Rel x = int_add_rel then
11.135 + else if x = int_add_rel then
11.136 ("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +))
11.137 - else if Kodkod.Rel x = nat_subtract_rel then
11.138 + else if x = nat_subtract_rel then
11.139 ("nat_subtract",
11.140 tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus))
11.141 - else if Kodkod.Rel x = int_subtract_rel then
11.142 + else if x = int_subtract_rel then
11.143 ("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op -))
11.144 - else if Kodkod.Rel x = nat_multiply_rel then
11.145 + else if x = nat_multiply_rel then
11.146 ("nat_multiply", tabulate_nat_op2 debug univ_card (nat_card, j0) (op * ))
11.147 - else if Kodkod.Rel x = int_multiply_rel then
11.148 + else if x = int_multiply_rel then
11.149 ("int_multiply", tabulate_int_op2 debug univ_card (int_card, j0) (op * ))
11.150 - else if Kodkod.Rel x = nat_divide_rel then
11.151 + else if x = nat_divide_rel then
11.152 ("nat_divide", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_div)
11.153 - else if Kodkod.Rel x = int_divide_rel then
11.154 + else if x = int_divide_rel then
11.155 ("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div)
11.156 - else if Kodkod.Rel x = nat_modulo_rel then
11.157 - ("nat_modulo", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_mod)
11.158 - else if Kodkod.Rel x = int_modulo_rel then
11.159 - ("int_modulo", tabulate_int_op2 debug univ_card (int_card, j0) isa_mod)
11.160 - else if Kodkod.Rel x = nat_less_rel then
11.161 + else if x = nat_less_rel then
11.162 ("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0)
11.163 (int_for_bool o op <))
11.164 - else if Kodkod.Rel x = int_less_rel then
11.165 + else if x = int_less_rel then
11.166 ("int_less", tabulate_int_op2 debug univ_card (int_card, j0)
11.167 (int_for_bool o op <))
11.168 - else if Kodkod.Rel x = gcd_rel then
11.169 + else if x = gcd_rel then
11.170 ("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd)
11.171 - else if Kodkod.Rel x = lcm_rel then
11.172 + else if x = lcm_rel then
11.173 ("lcm", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_lcm)
11.174 - else if Kodkod.Rel x = norm_frac_rel then
11.175 + else if x = norm_frac_rel then
11.176 ("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0)
11.177 isa_norm_frac)
11.178 else
11.179 @@ -260,12 +282,18 @@
11.180 map (bound_for_built_in_rel debug univ_card nat_card int_card j0)
11.181 o built_in_rels_in_formula
11.182
11.183 +(* Proof.context -> bool -> string -> typ -> rep -> string *)
11.184 +fun bound_comment ctxt debug nick T R =
11.185 + short_name nick ^
11.186 + (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
11.187 + else "") ^ " : " ^ string_for_rep R
11.188 +
11.189 (* Proof.context -> bool -> nut -> Kodkod.bound *)
11.190 fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
11.191 ([(x, bound_comment ctxt debug nick T R)],
11.192 if nick = @{const_name bisim_iterator_max} then
11.193 case R of
11.194 - Atom (k, j0) => [Kodkod.TupleSet [Kodkod.Tuple [k - 1 + j0]]]
11.195 + Atom (k, j0) => [single_atom (k - 1 + j0)]
11.196 | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
11.197 else
11.198 [Kodkod.TupleSet [], upper_bound_for_rep R])
11.199 @@ -369,17 +397,17 @@
11.200 else
11.201 Kodkod.True
11.202 end
11.203 -fun kk_n_ary_function kk R (r as Kodkod.Rel _) =
11.204 +fun kk_n_ary_function kk R (r as Kodkod.Rel x) =
11.205 if not (is_opt_rep R) then
11.206 - if r = suc_rel then
11.207 + if x = suc_rel then
11.208 Kodkod.False
11.209 - else if r = nat_add_rel then
11.210 + else if x = nat_add_rel then
11.211 formula_for_bool (card_of_rep (body_rep R) = 1)
11.212 - else if r = nat_multiply_rel then
11.213 + else if x = nat_multiply_rel then
11.214 formula_for_bool (card_of_rep (body_rep R) <= 2)
11.215 else
11.216 d_n_ary_function kk R r
11.217 - else if r = nat_subtract_rel then
11.218 + else if x = nat_subtract_rel then
11.219 Kodkod.True
11.220 else
11.221 d_n_ary_function kk R r
11.222 @@ -393,27 +421,27 @@
11.223
11.224 (* int -> kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr)
11.225 -> Kodkod.rel_expr -> Kodkod.rel_expr *)
11.226 -fun basic_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
11.227 +fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
11.228 if inline_rel_expr r then
11.229 f r
11.230 else
11.231 let val x = (Kodkod.arity_of_rel_expr r, j) in
11.232 kk_rel_let [Kodkod.AssignRelReg (x, r)] (f (Kodkod.RelReg x))
11.233 end
11.234 -
11.235 (* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr) -> Kodkod.rel_expr
11.236 -> Kodkod.rel_expr *)
11.237 -val single_rel_let = basic_rel_let 0
11.238 +val single_rel_rel_let = basic_rel_rel_let 0
11.239 (* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
11.240 -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
11.241 -fun double_rel_let kk f r1 r2 =
11.242 - single_rel_let kk (fn r1 => basic_rel_let 1 kk (f r1) r2) r1
11.243 +fun double_rel_rel_let kk f r1 r2 =
11.244 + single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
11.245 (* kodkod_constrs
11.246 -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
11.247 -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr
11.248 -> Kodkod.rel_expr *)
11.249 -fun triple_rel_let kk f r1 r2 r3 =
11.250 - double_rel_let kk (fn r1 => fn r2 => basic_rel_let 2 kk (f r1 r2) r3) r1 r2
11.251 +fun tripl_rel_rel_let kk f r1 r2 r3 =
11.252 + double_rel_rel_let kk
11.253 + (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
11.254
11.255 (* kodkod_constrs -> int -> Kodkod.formula -> Kodkod.rel_expr *)
11.256 fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
11.257 @@ -469,8 +497,8 @@
11.258 if is_lone_rep old_R andalso is_lone_rep new_R
11.259 andalso card = card_of_rep new_R then
11.260 if card >= lone_rep_fallback_max_card then
11.261 - raise LIMIT ("Nitpick_Kodkod.lone_rep_fallback",
11.262 - "too high cardinality (" ^ string_of_int card ^ ")")
11.263 + raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback",
11.264 + "too high cardinality (" ^ string_of_int card ^ ")")
11.265 else
11.266 kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)
11.267 (all_singletons_for_rep new_R)
11.268 @@ -672,6 +700,21 @@
11.269 (* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
11.270 and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2))
11.271
11.272 +(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.rel_expr *)
11.273 +fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r =
11.274 + kk_join r (Kodkod.Rel (if T = @{typ "unsigned_bit word"} then
11.275 + unsigned_bit_word_sel_rel
11.276 + else
11.277 + signed_bit_word_sel_rel))
11.278 +(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.int_expr *)
11.279 +val int_expr_from_atom = Kodkod.SetSum ooo bit_set_from_atom
11.280 +(* kodkod_constrs -> typ -> rep -> Kodkod.int_expr -> Kodkod.rel_expr *)
11.281 +fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
11.282 + : kodkod_constrs) T R i =
11.283 + kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
11.284 + (kk_rel_eq (bit_set_from_atom kk T (Kodkod.Var (1, ~1)))
11.285 + (Kodkod.Bits i))
11.286 +
11.287 (* kodkod_constrs -> nut -> Kodkod.formula *)
11.288 fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
11.289 kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
11.290 @@ -804,9 +847,9 @@
11.291 (kk_no r'))
11.292 end
11.293 end
11.294 -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
11.295 +(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
11.296 -> constr_spec -> Kodkod.formula list *)
11.297 -fun sel_axioms_for_constr ext_ctxt j0 kk rel_table
11.298 +fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
11.299 (constr as {const, delta, epsilon, explicit_max, ...}) =
11.300 let
11.301 val honors_explicit_max =
11.302 @@ -818,19 +861,25 @@
11.303 let
11.304 val ran_r = discr_rel_expr rel_table const
11.305 val max_axiom =
11.306 - if honors_explicit_max then Kodkod.True
11.307 - else Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max)
11.308 + if honors_explicit_max then
11.309 + Kodkod.True
11.310 + else if is_twos_complement_representable bits (epsilon - delta) then
11.311 + Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max)
11.312 + else
11.313 + raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
11.314 + "\"bits\" value " ^ string_of_int bits ^
11.315 + " too small for \"max\"")
11.316 in
11.317 max_axiom ::
11.318 map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr)
11.319 (index_seq 0 (num_sels_for_constr_type (snd const)))
11.320 end
11.321 end
11.322 -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
11.323 +(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
11.324 -> dtype_spec -> Kodkod.formula list *)
11.325 -fun sel_axioms_for_datatype ext_ctxt j0 kk rel_table
11.326 +fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
11.327 ({constrs, ...} : dtype_spec) =
11.328 - maps (sel_axioms_for_constr ext_ctxt j0 kk rel_table) constrs
11.329 + maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
11.330
11.331 (* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
11.332 -> Kodkod.formula list *)
11.333 @@ -881,24 +930,25 @@
11.334 kk_disjoint_sets kk rs]
11.335 end
11.336
11.337 -(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
11.338 - -> dtype_spec -> Kodkod.formula list *)
11.339 -fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
11.340 - | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
11.341 +(* extended_context -> int -> int Typtab.table -> kodkod_constrs
11.342 + -> nut NameTable.table -> dtype_spec -> Kodkod.formula list *)
11.343 +fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = []
11.344 + | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
11.345 + (dtype as {typ, ...}) =
11.346 let val j0 = offset_of_type ofs typ in
11.347 - sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
11.348 + sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @
11.349 uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
11.350 partition_axioms_for_datatype j0 kk rel_table dtype
11.351 end
11.352
11.353 -(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
11.354 - -> dtype_spec list -> Kodkod.formula list *)
11.355 -fun declarative_axioms_for_datatypes ext_ctxt ofs kk rel_table dtypes =
11.356 +(* extended_context -> int -> int Typtab.table -> kodkod_constrs
11.357 + -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list *)
11.358 +fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
11.359 acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
11.360 - maps (other_axioms_for_datatype ext_ctxt ofs kk rel_table) dtypes
11.361 + maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
11.362
11.363 -(* int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *)
11.364 -fun kodkod_formula_from_nut ofs liberal
11.365 +(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *)
11.366 +fun kodkod_formula_from_nut bits ofs liberal
11.367 (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
11.368 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
11.369 kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference,
11.370 @@ -924,12 +974,12 @@
11.371 fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2)
11.372 (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
11.373 val kk_or3 =
11.374 - double_rel_let kk
11.375 + double_rel_rel_let kk
11.376 (fn r1 => fn r2 =>
11.377 kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom
11.378 (kk_intersect r1 r2))
11.379 val kk_and3 =
11.380 - double_rel_let kk
11.381 + double_rel_rel_let kk
11.382 (fn r1 => fn r2 =>
11.383 kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom
11.384 (kk_intersect r1 r2))
11.385 @@ -1153,38 +1203,98 @@
11.386 | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => Kodkod.Atom j0
11.387 | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
11.388 to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
11.389 - | Cst (Num j, @{typ int}, R) =>
11.390 - (case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
11.391 + | Cst (Num j, T, R) =>
11.392 + if is_word_type T then
11.393 + atom_from_int_expr kk T R (Kodkod.Num j)
11.394 + else if T = int_T then
11.395 + case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
11.396 ~1 => if is_opt_rep R then Kodkod.None
11.397 else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
11.398 - | j' => Kodkod.Atom j')
11.399 - | Cst (Num j, T, R) =>
11.400 - if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
11.401 - else if is_opt_rep R then Kodkod.None
11.402 - else raise NUT ("Nitpick_Kodkod.to_r", [u])
11.403 + | j' => Kodkod.Atom j'
11.404 + else
11.405 + if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
11.406 + else if is_opt_rep R then Kodkod.None
11.407 + else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
11.408 | Cst (Unknown, _, R) => empty_rel_for_rep R
11.409 | Cst (Unrep, _, R) => empty_rel_for_rep R
11.410 | Cst (Suc, T, Func (Atom x, _)) =>
11.411 - if domain_type T <> nat_T then suc_rel
11.412 - else kk_intersect suc_rel (kk_product Kodkod.Univ (Kodkod.AtomSeq x))
11.413 - | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => nat_add_rel
11.414 - | Cst (Add, Type ("fun", [@{typ int}, _]), _) => int_add_rel
11.415 - | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) => nat_subtract_rel
11.416 - | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) => int_subtract_rel
11.417 - | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) => nat_multiply_rel
11.418 - | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) => int_multiply_rel
11.419 - | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => nat_divide_rel
11.420 - | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => int_divide_rel
11.421 - | Cst (Modulo, Type ("fun", [@{typ nat}, _]), _) => nat_modulo_rel
11.422 - | Cst (Modulo, Type ("fun", [@{typ int}, _]), _) => int_modulo_rel
11.423 - | Cst (Gcd, _, _) => gcd_rel
11.424 - | Cst (Lcm, _, _) => lcm_rel
11.425 + if domain_type T <> nat_T then
11.426 + Kodkod.Rel suc_rel
11.427 + else
11.428 + kk_intersect (Kodkod.Rel suc_rel)
11.429 + (kk_product Kodkod.Univ (Kodkod.AtomSeq x))
11.430 + | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => Kodkod.Rel nat_add_rel
11.431 + | Cst (Add, Type ("fun", [@{typ int}, _]), _) => Kodkod.Rel int_add_rel
11.432 + | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
11.433 + to_bit_word_binary_op T R NONE (SOME (curry Kodkod.Add))
11.434 + | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
11.435 + to_bit_word_binary_op T R
11.436 + (SOME (fn i1 => fn i2 => fn i3 =>
11.437 + kk_implies (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i1, i2)))
11.438 + (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i2, i3)))))
11.439 + (SOME (curry Kodkod.Add))
11.440 + | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) =>
11.441 + Kodkod.Rel nat_subtract_rel
11.442 + | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) =>
11.443 + Kodkod.Rel int_subtract_rel
11.444 + | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
11.445 + to_bit_word_binary_op T R NONE
11.446 + (SOME (fn i1 => fn i2 =>
11.447 + Kodkod.IntIf (Kodkod.LE (i1, i2), Kodkod.Num 0,
11.448 + Kodkod.Sub (i1, i2))))
11.449 + | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
11.450 + to_bit_word_binary_op T R
11.451 + (SOME (fn i1 => fn i2 => fn i3 =>
11.452 + kk_implies (Kodkod.LT (Kodkod.BitXor (i1, i2), Kodkod.Num 0))
11.453 + (Kodkod.LT (Kodkod.BitXor (i2, i3), Kodkod.Num 0))))
11.454 + (SOME (curry Kodkod.Sub))
11.455 + | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) =>
11.456 + Kodkod.Rel nat_multiply_rel
11.457 + | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) =>
11.458 + Kodkod.Rel int_multiply_rel
11.459 + | Cst (Multiply,
11.460 + T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) =>
11.461 + to_bit_word_binary_op T R
11.462 + (SOME (fn i1 => fn i2 => fn i3 =>
11.463 + kk_or (Kodkod.IntEq (i2, Kodkod.Num 0))
11.464 + (Kodkod.IntEq (Kodkod.Div (i3, i2), i1)
11.465 + |> bit_T = @{typ signed_bit}
11.466 + ? kk_and (Kodkod.LE (Kodkod.Num 0,
11.467 + foldl1 Kodkod.BitAnd [i1, i2, i3])))))
11.468 + (SOME (curry Kodkod.Mult))
11.469 + | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) =>
11.470 + Kodkod.Rel nat_divide_rel
11.471 + | Cst (Divide, Type ("fun", [@{typ int}, _]), _) =>
11.472 + Kodkod.Rel int_divide_rel
11.473 + | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
11.474 + to_bit_word_binary_op T R NONE
11.475 + (SOME (fn i1 => fn i2 =>
11.476 + Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
11.477 + Kodkod.Num 0, Kodkod.Div (i1, i2))))
11.478 + | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
11.479 + to_bit_word_binary_op T R
11.480 + (SOME (fn i1 => fn i2 => fn i3 =>
11.481 + Kodkod.LE (Kodkod.Num 0, foldl1 Kodkod.BitAnd [i1, i2, i3])))
11.482 + (SOME (fn i1 => fn i2 =>
11.483 + Kodkod.IntIf (kk_and (Kodkod.LT (i1, Kodkod.Num 0))
11.484 + (Kodkod.LT (Kodkod.Num 0, i2)),
11.485 + Kodkod.Sub (Kodkod.Div (Kodkod.Add (i1, Kodkod.Num 1), i2),
11.486 + Kodkod.Num 1),
11.487 + Kodkod.IntIf (kk_and (Kodkod.LT (Kodkod.Num 0, i1))
11.488 + (Kodkod.LT (i2, Kodkod.Num 0)),
11.489 + Kodkod.Sub (Kodkod.Div (Kodkod.Sub (i1, Kodkod.Num 1),
11.490 + i2), Kodkod.Num 1),
11.491 + Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
11.492 + Kodkod.Num 0, Kodkod.Div (i1, i2))))))
11.493 + | Cst (Gcd, _, _) => Kodkod.Rel gcd_rel
11.494 + | Cst (Lcm, _, _) => Kodkod.Rel lcm_rel
11.495 | Cst (Fracs, _, Func (Atom (1, _), _)) => Kodkod.None
11.496 | Cst (Fracs, _, Func (Struct _, _)) =>
11.497 - kk_project_seq norm_frac_rel 2 2
11.498 - | Cst (NormFrac, _, _) => norm_frac_rel
11.499 - | Cst (NatToInt, _, Func (Atom _, Atom _)) => Kodkod.Iden
11.500 - | Cst (NatToInt, _,
11.501 + kk_project_seq (Kodkod.Rel norm_frac_rel) 2 2
11.502 + | Cst (NormFrac, _, _) => Kodkod.Rel norm_frac_rel
11.503 + | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
11.504 + Kodkod.Iden
11.505 + | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
11.506 Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) =>
11.507 if nat_j0 = int_j0 then
11.508 kk_intersect Kodkod.Iden
11.509 @@ -1192,7 +1302,10 @@
11.510 Kodkod.Univ)
11.511 else
11.512 raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
11.513 - | Cst (IntToNat, _, Func (Atom (int_k, int_j0), nat_R)) =>
11.514 + | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
11.515 + to_bit_word_unary_op T R I
11.516 + | Cst (IntToNat, Type ("fun", [@{typ int}, _]),
11.517 + Func (Atom (int_k, int_j0), nat_R)) =>
11.518 let
11.519 val abs_card = max_int_for_card int_k + 1
11.520 val (nat_k, nat_j0) = the_single (atom_schema_of_rep nat_R)
11.521 @@ -1208,6 +1321,10 @@
11.522 else
11.523 raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
11.524 end
11.525 + | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
11.526 + to_bit_word_unary_op T R
11.527 + (fn i => Kodkod.IntIf (Kodkod.LE (i, Kodkod.Num 0),
11.528 + Kodkod.Num 0, i))
11.529 | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
11.530 | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None
11.531 | Op1 (Converse, T, R, u1) =>
11.532 @@ -1241,7 +1358,7 @@
11.533 val R' = rep_to_binary_rel_rep ofs T1 (unopt_rep (rep_of u1))
11.534 val R'' = opt_rep ofs T1 R'
11.535 in
11.536 - single_rel_let kk
11.537 + single_rel_rel_let kk
11.538 (fn r =>
11.539 let
11.540 val true_r = kk_closure (kk_join r true_atom)
11.541 @@ -1266,7 +1383,7 @@
11.542 Func (R1, Formula Neut) => to_rep R1 u1
11.543 | Func (Unit, Opt R) => to_guard [u1] R true_atom
11.544 | Func (R1, R2 as Opt _) =>
11.545 - single_rel_let kk
11.546 + single_rel_rel_let kk
11.547 (fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)
11.548 (rel_expr_to_func kk R1 bool_atom_R
11.549 (Func (R1, Formula Neut)) r))
11.550 @@ -1309,12 +1426,22 @@
11.551 if is_opt_rep (rep_of u1) then kk_rel_if (to_f u2) (to_r u1) false_atom
11.552 else kk_rel_if (to_f u1) (to_r u2) false_atom
11.553 | Op2 (Less, _, _, u1, u2) =>
11.554 - if type_of u1 = nat_T then
11.555 - if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom
11.556 - else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom
11.557 - else kk_nat_less (to_integer u1) (to_integer u2)
11.558 - else
11.559 - kk_int_less (to_integer u1) (to_integer u2)
11.560 + (case type_of u1 of
11.561 + @{typ nat} =>
11.562 + if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom
11.563 + else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom
11.564 + else kk_nat_less (to_integer u1) (to_integer u2)
11.565 + | @{typ int} => kk_int_less (to_integer u1) (to_integer u2)
11.566 + | _ => double_rel_rel_let kk
11.567 + (fn r1 => fn r2 =>
11.568 + kk_rel_if
11.569 + (fold kk_and (map_filter (fn (u, r) =>
11.570 + if is_opt_rep (rep_of u) then SOME (kk_some r)
11.571 + else NONE) [(u1, r1), (u2, r2)]) Kodkod.True)
11.572 + (atom_from_formula kk bool_j0 (Kodkod.LT (pairself
11.573 + (int_expr_from_atom kk (type_of u1)) (r1, r2))))
11.574 + Kodkod.None)
11.575 + (to_r u1) (to_r u2))
11.576 | Op2 (The, T, R, u1, u2) =>
11.577 if is_opt_rep R then
11.578 let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in
11.579 @@ -1468,7 +1595,7 @@
11.580 if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
11.581 Kodkod.Atom (offset_of_type ofs nat_T)
11.582 else
11.583 - fold kk_join [to_integer u1, to_integer u2] nat_subtract_rel
11.584 + fold kk_join (map to_integer [u1, u2]) (Kodkod.Rel nat_subtract_rel)
11.585 | Op2 (Apply, _, R, u1, u2) =>
11.586 if is_Cst Unrep u2 andalso is_set_type (type_of u1)
11.587 andalso is_FreeName u1 then
11.588 @@ -1494,7 +1621,7 @@
11.589 kk_rel_let [to_expr_assign u1 u2] (to_rep R u3)
11.590 | Op3 (If, _, R, u1, u2, u3) =>
11.591 if is_opt_rep (rep_of u1) then
11.592 - triple_rel_let kk
11.593 + tripl_rel_rel_let kk
11.594 (fn r1 => fn r2 => fn r3 =>
11.595 let val empty_r = empty_rel_for_rep R in
11.596 fold1 kk_union
11.597 @@ -1686,7 +1813,7 @@
11.598 | Func (_, Formula Neut) => set_oper r1 r2
11.599 | Func (Unit, _) => connective3 r1 r2
11.600 | Func (R1, _) =>
11.601 - double_rel_let kk
11.602 + double_rel_rel_let kk
11.603 (fn r1 => fn r2 =>
11.604 kk_union
11.605 (kk_product
11.606 @@ -1702,6 +1829,43 @@
11.607 r1 r2
11.608 | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
11.609 end
11.610 + (* typ -> rep -> (Kodkod.int_expr -> Kodkod.int_expr) -> Kodkod.rel_expr *)
11.611 + and to_bit_word_unary_op T R oper =
11.612 + let
11.613 + val Ts = strip_type T ||> single |> op @
11.614 + (* int -> Kodkod.int_expr *)
11.615 + fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
11.616 + in
11.617 + kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
11.618 + (Kodkod.FormulaLet
11.619 + (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 1),
11.620 + Kodkod.IntEq (Kodkod.IntReg 1, oper (Kodkod.IntReg 0))))
11.621 + end
11.622 + (* typ -> rep
11.623 + -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr -> bool) option
11.624 + -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr) option
11.625 + -> Kodkod.rel_expr *)
11.626 + and to_bit_word_binary_op T R opt_guard opt_oper =
11.627 + let
11.628 + val Ts = strip_type T ||> single |> op @
11.629 + (* int -> Kodkod.int_expr *)
11.630 + fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
11.631 + in
11.632 + kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
11.633 + (Kodkod.FormulaLet
11.634 + (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 2),
11.635 + fold1 kk_and
11.636 + ((case opt_guard of
11.637 + NONE => []
11.638 + | SOME guard =>
11.639 + [guard (Kodkod.IntReg 0) (Kodkod.IntReg 1)
11.640 + (Kodkod.IntReg 2)]) @
11.641 + (case opt_oper of
11.642 + NONE => []
11.643 + | SOME oper =>
11.644 + [Kodkod.IntEq (Kodkod.IntReg 2,
11.645 + oper (Kodkod.IntReg 0) (Kodkod.IntReg 1))]))))
11.646 + end
11.647 (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *)
11.648 and to_apply res_R func_u arg_u =
11.649 case unopt_rep (rep_of func_u) of
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Dec 14 16:48:49 2009 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Dec 17 15:22:11 2009 +0100
12.3 @@ -71,24 +71,40 @@
12.4 else
12.5 Const (atom_name "" T j, T)
12.6
12.7 +(* term * term -> order *)
12.8 +fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
12.9 + | nice_term_ord (t1, t2) =
12.10 + int_ord (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
12.11 + handle TERM ("dest_number", _) =>
12.12 + case (t1, t2) of
12.13 + (t11 $ t12, t21 $ t22) =>
12.14 + (case nice_term_ord (t11, t21) of
12.15 + EQUAL => nice_term_ord (t12, t22)
12.16 + | ord => ord)
12.17 + | _ => TermOrd.term_ord (t1, t2)
12.18 +
12.19 (* nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list *)
12.20 fun tuple_list_for_name rel_table bounds name =
12.21 the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
12.22
12.23 (* term -> term *)
12.24 -fun unbox_term (Const (@{const_name FunBox}, _) $ t1) = unbox_term t1
12.25 - | unbox_term (Const (@{const_name PairBox},
12.26 - Type ("fun", [T1, Type ("fun", [T2, T3])])) $ t1 $ t2) =
12.27 - let val Ts = map unbox_type [T1, T2] in
12.28 +fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
12.29 + unbit_and_unbox_term t1
12.30 + | unbit_and_unbox_term (Const (@{const_name PairBox},
12.31 + Type ("fun", [T1, Type ("fun", [T2, T3])]))
12.32 + $ t1 $ t2) =
12.33 + let val Ts = map unbit_and_unbox_type [T1, T2] in
12.34 Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
12.35 - $ unbox_term t1 $ unbox_term t2
12.36 + $ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
12.37 end
12.38 - | unbox_term (Const (s, T)) = Const (s, unbox_type T)
12.39 - | unbox_term (t1 $ t2) = unbox_term t1 $ unbox_term t2
12.40 - | unbox_term (Free (s, T)) = Free (s, unbox_type T)
12.41 - | unbox_term (Var (x, T)) = Var (x, unbox_type T)
12.42 - | unbox_term (Bound j) = Bound j
12.43 - | unbox_term (Abs (s, T, t')) = Abs (s, unbox_type T, unbox_term t')
12.44 + | unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T)
12.45 + | unbit_and_unbox_term (t1 $ t2) =
12.46 + unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
12.47 + | unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T)
12.48 + | unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T)
12.49 + | unbit_and_unbox_term (Bound j) = Bound j
12.50 + | unbit_and_unbox_term (Abs (s, T, t')) =
12.51 + Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t')
12.52
12.53 (* typ -> typ -> (typ * typ) * (typ * typ) *)
12.54 fun factor_out_types (T1 as Type ("*", [T11, T12]))
12.55 @@ -121,7 +137,7 @@
12.56 Const (if maybe_opt orelse T2 <> bool_T then @{const_name undefined}
12.57 else non_opt_name, T1 --> T2)
12.58 | aux T1 T2 ((t1, t2) :: ps) =
12.59 - Const (@{const_name fun_upd}, [T1 --> T2, T1, T2] ---> T1 --> T2)
12.60 + Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
12.61 $ aux T1 T2 ps $ t1 $ t2
12.62 in aux T1 T2 o rev end
12.63 (* term -> bool *)
12.64 @@ -186,7 +202,7 @@
12.65 | do_arrow T1' T2' T1 T2
12.66 (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
12.67 Const (@{const_name fun_upd},
12.68 - [T1' --> T2', T1', T2'] ---> T1' --> T2')
12.69 + (T1' --> T2') --> T1' --> T2' --> T1' --> T2')
12.70 $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
12.71 | do_arrow _ _ _ _ t =
12.72 raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t])
12.73 @@ -221,21 +237,31 @@
12.74 HOLogic.mk_prod (mk_tuple T1 ts,
12.75 mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
12.76 | mk_tuple _ (t :: _) = t
12.77 + | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
12.78
12.79 (* string * string * string * string -> scope -> nut list -> nut list
12.80 -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> typ -> typ
12.81 -> rep -> int list list -> term *)
12.82 fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
12.83 - ({ext_ctxt as {thy, ctxt, ...}, card_assigns, datatypes, ofs, ...}
12.84 + ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
12.85 : scope) sel_names rel_table bounds =
12.86 let
12.87 val for_auto = (maybe_name = "")
12.88 + (* int list list -> int *)
12.89 + fun value_of_bits jss =
12.90 + let
12.91 + val j0 = offset_of_type ofs @{typ unsigned_bit}
12.92 + val js = map (Integer.add (~ j0) o the_single) jss
12.93 + in
12.94 + fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~))
12.95 + js 0
12.96 + end
12.97 (* bool -> typ -> typ -> (term * term) list -> term *)
12.98 fun make_set maybe_opt T1 T2 =
12.99 let
12.100 val empty_const = Const (@{const_name Set.empty}, T1 --> T2)
12.101 val insert_const = Const (@{const_name insert},
12.102 - [T1, T1 --> T2] ---> T1 --> T2)
12.103 + T1 --> (T1 --> T2) --> T1 --> T2)
12.104 (* (term * term) list -> term *)
12.105 fun aux [] =
12.106 if maybe_opt andalso not (is_complete_type datatypes T1) then
12.107 @@ -254,7 +280,7 @@
12.108 fun make_map T1 T2 T2' =
12.109 let
12.110 val update_const = Const (@{const_name fun_upd},
12.111 - [T1 --> T2, T1, T2] ---> T1 --> T2)
12.112 + (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
12.113 (* (term * term) list -> term *)
12.114 fun aux' [] = Const (@{const_name Map.empty}, T1 --> T2)
12.115 | aux' ((t1, t2) :: ps) =
12.116 @@ -300,8 +326,10 @@
12.117 fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
12.118 ts1 ~~ ts2 |> T1 = @{typ bisim_iterator} ? rev
12.119 |> make_plain_fun (maybe_opt andalso not for_auto) T1 T2
12.120 - |> unbox_term
12.121 - |> typecast_fun (unbox_type T') (unbox_type T1) (unbox_type T2)
12.122 + |> unbit_and_unbox_term
12.123 + |> typecast_fun (unbit_and_unbox_type T')
12.124 + (unbit_and_unbox_type T1)
12.125 + (unbit_and_unbox_type T2)
12.126 (* (typ * int) list -> typ -> typ -> int -> term *)
12.127 fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j =
12.128 let
12.129 @@ -373,6 +401,10 @@
12.130 in
12.131 if co andalso member (op =) seen (T, j) then
12.132 Var (var ())
12.133 + else if constr_s = @{const_name Word} then
12.134 + HOLogic.mk_number
12.135 + (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
12.136 + (value_of_bits (the_single arg_jsss))
12.137 else
12.138 let
12.139 val seen = seen |> co ? cons (T, j)
12.140 @@ -398,7 +430,7 @@
12.141 | n1 => case HOLogic.dest_number t2 |> snd of
12.142 1 => mk_num n1
12.143 | n2 => Const (@{const_name HOL.divide},
12.144 - [num_T, num_T] ---> num_T)
12.145 + num_T --> num_T --> num_T)
12.146 $ mk_num n1 $ mk_num n2)
12.147 | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
12.148 \for_atom (Abs_Frac)", ts)
12.149 @@ -413,7 +445,7 @@
12.150 if exists_subterm (curry (op =) (Var var)) t then
12.151 Const (@{const_name The}, (T --> bool_T) --> T)
12.152 $ Abs ("\<omega>", T,
12.153 - Const (@{const_name "op ="}, [T, T] ---> bool_T)
12.154 + Const (@{const_name "op ="}, T --> T --> bool_T)
12.155 $ Bound 0 $ abstract_over (Var var, t))
12.156 else
12.157 t
12.158 @@ -470,7 +502,8 @@
12.159 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
12.160 string_of_int (length jss))
12.161 in
12.162 - (not for_auto ? setify_mapify_funs []) o unbox_term oooo term_for_rep []
12.163 + (not for_auto ? setify_mapify_funs []) o unbit_and_unbox_term
12.164 + oooo term_for_rep []
12.165 end
12.166
12.167 (* scope -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> nut
12.168 @@ -533,25 +566,26 @@
12.169 -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
12.170 -> Pretty.T * bool *)
12.171 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
12.172 - ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, user_axioms, debug,
12.173 - wfs, destroy_constrs, specialize, skolemize,
12.174 - star_linear_preds, uncurry, fast_descrs, tac_timeout,
12.175 - evals, case_names, def_table, nondef_table, user_nondefs,
12.176 - simp_table, psimp_table, intro_table, ground_thm_table,
12.177 - ersatz_table, skolems, special_funs, unrolled_preds,
12.178 - wf_cache, constr_cache},
12.179 - card_assigns, bisim_depth, datatypes, ofs} : scope) formats all_frees
12.180 - free_names sel_names nonsel_names rel_table bounds =
12.181 + ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
12.182 + debug, binary_ints, destroy_constrs, specialize,
12.183 + skolemize, star_linear_preds, uncurry, fast_descrs,
12.184 + tac_timeout, evals, case_names, def_table, nondef_table,
12.185 + user_nondefs, simp_table, psimp_table, intro_table,
12.186 + ground_thm_table, ersatz_table, skolems, special_funs,
12.187 + unrolled_preds, wf_cache, constr_cache},
12.188 + card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
12.189 + formats all_frees free_names sel_names nonsel_names rel_table bounds =
12.190 let
12.191 val (wacky_names as (_, base_name, step_name, _), ctxt) =
12.192 add_wacky_syntax ctxt
12.193 val ext_ctxt =
12.194 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
12.195 wfs = wfs, user_axioms = user_axioms, debug = debug,
12.196 - destroy_constrs = destroy_constrs, specialize = specialize,
12.197 - skolemize = skolemize, star_linear_preds = star_linear_preds,
12.198 - uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout,
12.199 - evals = evals, case_names = case_names, def_table = def_table,
12.200 + binary_ints = binary_ints, destroy_constrs = destroy_constrs,
12.201 + specialize = specialize, skolemize = skolemize,
12.202 + star_linear_preds = star_linear_preds, uncurry = uncurry,
12.203 + fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
12.204 + case_names = case_names, def_table = def_table,
12.205 nondef_table = nondef_table, user_nondefs = user_nondefs,
12.206 simp_table = simp_table, psimp_table = psimp_table,
12.207 intro_table = intro_table, ground_thm_table = ground_thm_table,
12.208 @@ -559,17 +593,21 @@
12.209 special_funs = special_funs, unrolled_preds = unrolled_preds,
12.210 wf_cache = wf_cache, constr_cache = constr_cache}
12.211 val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
12.212 - bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
12.213 + bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
12.214 + ofs = ofs}
12.215 (* typ -> typ -> rep -> int list list -> term *)
12.216 val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table
12.217 bounds
12.218 - (* typ -> typ -> typ *)
12.219 - fun nth_value_of_type T card n = term_for_rep T T (Atom (card, 0)) [[n]]
12.220 + (* nat -> typ -> nat -> typ *)
12.221 + fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]]
12.222 + (* nat -> typ -> typ list *)
12.223 + fun all_values_of_type card T =
12.224 + index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
12.225 (* dtype_spec list -> dtype_spec -> bool *)
12.226 fun is_codatatype_wellformed (cos : dtype_spec list)
12.227 ({typ, card, ...} : dtype_spec) =
12.228 let
12.229 - val ts = map (nth_value_of_type typ card) (index_seq 0 card)
12.230 + val ts = all_values_of_type card typ
12.231 val max_depth = Integer.sum (map #card cos)
12.232 in
12.233 forall (not o bisimilar_values (map #typ cos) max_depth)
12.234 @@ -581,7 +619,7 @@
12.235 val (oper, (t1, T'), T) =
12.236 case name of
12.237 FreeName (s, T, _) =>
12.238 - let val t = Free (s, unbox_type T) in
12.239 + let val t = Free (s, unbit_and_unbox_type T) in
12.240 ("=", (t, format_term_type thy def_table formats t), T)
12.241 end
12.242 | ConstName (s, T, _) =>
12.243 @@ -603,11 +641,10 @@
12.244 (* dtype_spec -> Pretty.T *)
12.245 fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
12.246 Pretty.block (Pretty.breaks
12.247 - [Syntax.pretty_typ ctxt (unbox_type typ), Pretty.str "=",
12.248 + [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
12.249 Pretty.enum "," "{" "}"
12.250 - (map (Syntax.pretty_term ctxt o nth_value_of_type typ card)
12.251 - (index_seq 0 card) @
12.252 - (if complete then [] else [Pretty.str unrep]))])
12.253 + (map (Syntax.pretty_term ctxt) (all_values_of_type card typ)
12.254 + @ (if complete then [] else [Pretty.str unrep]))])
12.255 (* typ -> dtype_spec list *)
12.256 fun integer_datatype T =
12.257 [{typ = T, card = card_of_type card_assigns T, co = false,
12.258 @@ -647,7 +684,7 @@
12.259 val free_names =
12.260 map (fn x as (s, T) =>
12.261 case filter (curry (op =) x
12.262 - o pairf nickname_of (unbox_type o type_of))
12.263 + o pairf nickname_of (unbit_and_unbox_type o type_of))
12.264 free_names of
12.265 [name] => name
12.266 | [] => FreeName (s, T, Any)
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Dec 14 16:48:49 2009 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Dec 17 15:22:11 2009 +0100
13.3 @@ -26,7 +26,6 @@
13.4 Subtract |
13.5 Multiply |
13.6 Divide |
13.7 - Modulo |
13.8 Gcd |
13.9 Lcm |
13.10 Fracs |
13.11 @@ -144,7 +143,6 @@
13.12 Subtract |
13.13 Multiply |
13.14 Divide |
13.15 - Modulo |
13.16 Gcd |
13.17 Lcm |
13.18 Fracs |
13.19 @@ -218,7 +216,6 @@
13.20 | string_for_cst Subtract = "Subtract"
13.21 | string_for_cst Multiply = "Multiply"
13.22 | string_for_cst Divide = "Divide"
13.23 - | string_for_cst Modulo = "Modulo"
13.24 | string_for_cst Gcd = "Gcd"
13.25 | string_for_cst Lcm = "Lcm"
13.26 | string_for_cst Fracs = "Fracs"
13.27 @@ -614,8 +611,6 @@
13.28 Cst (Multiply, T, Any)
13.29 | (Const (@{const_name div_nat_inst.div_nat}, T), []) =>
13.30 Cst (Divide, T, Any)
13.31 - | (Const (@{const_name div_nat_inst.mod_nat}, T), []) =>
13.32 - Cst (Modulo, T, Any)
13.33 | (Const (@{const_name ord_nat_inst.less_nat}, T), [t1, t2]) =>
13.34 Op2 (Less, bool_T, Any, sub t1, sub t2)
13.35 | (Const (@{const_name ord_nat_inst.less_eq_nat}, T), [t1, t2]) =>
13.36 @@ -634,12 +629,12 @@
13.37 Cst (Multiply, T, Any)
13.38 | (Const (@{const_name div_int_inst.div_int}, T), []) =>
13.39 Cst (Divide, T, Any)
13.40 - | (Const (@{const_name div_int_inst.mod_int}, T), []) =>
13.41 - Cst (Modulo, T, Any)
13.42 | (Const (@{const_name uminus_int_inst.uminus_int}, T), []) =>
13.43 - Op2 (Apply, int_T --> int_T, Any,
13.44 - Cst (Subtract, [int_T, int_T] ---> int_T, Any),
13.45 - Cst (Num 0, int_T, Any))
13.46 + let val num_T = domain_type T in
13.47 + Op2 (Apply, num_T --> num_T, Any,
13.48 + Cst (Subtract, num_T --> num_T --> num_T, Any),
13.49 + Cst (Num 0, num_T, Any))
13.50 + end
13.51 | (Const (@{const_name ord_int_inst.less_int}, T), [t1, t2]) =>
13.52 Op2 (Less, bool_T, Any, sub t1, sub t2)
13.53 | (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) =>
13.54 @@ -650,6 +645,9 @@
13.55 | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
13.56 | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
13.57 Cst (NatToInt, T, Any)
13.58 + | (Const (@{const_name of_nat},
13.59 + T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
13.60 + Cst (NatToInt, T, Any)
13.61 | (Const (@{const_name lower_semilattice_fun_inst.inf_fun}, T),
13.62 [t1, t2]) =>
13.63 Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2)
13.64 @@ -742,12 +740,14 @@
13.65
13.66 (* scope -> styp -> int -> nut list * rep NameTable.table
13.67 -> nut list * rep NameTable.table *)
13.68 -fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) x n
13.69 +fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n
13.70 (vs, table) =
13.71 let
13.72 val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
13.73 - val R' = if n = ~1 then best_non_opt_set_rep_for_type scope T'
13.74 - else best_opt_set_rep_for_type scope T' |> unopt_rep
13.75 + val R' = if n = ~1 orelse is_word_type (body_type T) then
13.76 + best_non_opt_set_rep_for_type scope T'
13.77 + else
13.78 + best_opt_set_rep_for_type scope T' |> unopt_rep
13.79 val v = ConstName (s', T', R')
13.80 in (v :: vs, NameTable.update (v, R') table) end
13.81 (* scope -> styp -> nut list * rep NameTable.table
13.82 @@ -780,7 +780,8 @@
13.83 (not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse
13.84 case u of
13.85 Cst (Num _, _, _) => true
13.86 - | Cst (cst, T, _) => cst = Suc orelse (body_type T = nat_T andalso cst = Add)
13.87 + | Cst (cst, T, _) =>
13.88 + cst = Suc orelse (body_type T = nat_T andalso cst = Add)
13.89 | Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2]
13.90 | Op3 (If, _, _, u1, u2, u3) =>
13.91 not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3]
13.92 @@ -883,7 +884,8 @@
13.93
13.94 (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
13.95 fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns,
13.96 - datatypes, ofs, ...}) liberal table def =
13.97 + bits, datatypes, ofs, ...})
13.98 + liberal table def =
13.99 let
13.100 val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
13.101 (* polarity -> bool -> rep *)
13.102 @@ -912,17 +914,23 @@
13.103 Cst (False, T, _) => Cst (False, T, Formula Neut)
13.104 | Cst (True, T, _) => Cst (True, T, Formula Neut)
13.105 | Cst (Num j, T, _) =>
13.106 - (case spec_of_type scope T of
13.107 - (1, j0) => if j = 0 then Cst (Unity, T, Unit)
13.108 - else Cst (Unrep, T, Opt (Atom (1, j0)))
13.109 - | (k, j0) =>
13.110 - let
13.111 - val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
13.112 - else j < k)
13.113 - in
13.114 - if ok then Cst (Num j, T, Atom (k, j0))
13.115 - else Cst (Unrep, T, Opt (Atom (k, j0)))
13.116 - end)
13.117 + if is_word_type T then
13.118 + if is_twos_complement_representable bits j then
13.119 + Cst (Num j, T, best_non_opt_set_rep_for_type scope T)
13.120 + else
13.121 + Cst (Unrep, T, best_opt_set_rep_for_type scope T)
13.122 + else
13.123 + (case spec_of_type scope T of
13.124 + (1, j0) => if j = 0 then Cst (Unity, T, Unit)
13.125 + else Cst (Unrep, T, Opt (Atom (1, j0)))
13.126 + | (k, j0) =>
13.127 + let
13.128 + val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
13.129 + else j < k)
13.130 + in
13.131 + if ok then Cst (Num j, T, Atom (k, j0))
13.132 + else Cst (Unrep, T, Opt (Atom (k, j0)))
13.133 + end)
13.134 | Cst (Suc, T as Type ("fun", [T1, _]), _) =>
13.135 let val R = Atom (spec_of_type scope T1) in
13.136 Cst (Suc, T, Func (R, Opt R))
13.137 @@ -939,31 +947,27 @@
13.138 (true, Pos) => Cst (False, T, Formula Pos)
13.139 | (true, Neg) => Cst (True, T, Formula Neg)
13.140 | _ => Cst (cst, T, best_opt_set_rep_for_type scope T)
13.141 - else if member (op =) [Add, Subtract, Multiply, Divide, Modulo, Gcd,
13.142 - Lcm] cst then
13.143 + else if member (op =) [Add, Subtract, Multiply, Divide, Gcd, Lcm]
13.144 + cst then
13.145 let
13.146 val T1 = domain_type T
13.147 val R1 = Atom (spec_of_type scope T1)
13.148 - val total =
13.149 - T1 = nat_T andalso (cst = Subtract orelse cst = Divide
13.150 - orelse cst = Modulo orelse cst = Gcd)
13.151 + val total = T1 = nat_T
13.152 + andalso (cst = Subtract orelse cst = Divide
13.153 + orelse cst = Gcd)
13.154 in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
13.155 else if cst = NatToInt orelse cst = IntToNat then
13.156 let
13.157 - val (nat_card, nat_j0) = spec_of_type scope nat_T
13.158 - val (int_card, int_j0) = spec_of_type scope int_T
13.159 + val (dom_card, dom_j0) = spec_of_type scope (domain_type T)
13.160 + val (ran_card, ran_j0) = spec_of_type scope (range_type T)
13.161 + val total = not (is_word_type (domain_type T))
13.162 + andalso (if cst = NatToInt then
13.163 + max_int_for_card ran_card >= dom_card + 1
13.164 + else
13.165 + max_int_for_card dom_card < ran_card)
13.166 in
13.167 - if cst = NatToInt then
13.168 - let val total = (max_int_for_card int_card >= nat_card + 1) in
13.169 - Cst (cst, T,
13.170 - Func (Atom (nat_card, nat_j0),
13.171 - (not total ? Opt) (Atom (int_card, int_j0))))
13.172 - end
13.173 - else
13.174 - let val total = (max_int_for_card int_card < nat_card) in
13.175 - Cst (cst, T, Func (Atom (int_card, int_j0),
13.176 - Atom (nat_card, nat_j0)) |> not total ? Opt)
13.177 - end
13.178 + Cst (cst, T, Func (Atom (dom_card, dom_j0),
13.179 + Atom (ran_card, ran_j0) |> not total ? Opt))
13.180 end
13.181 else
13.182 Cst (cst, T, best_set_rep_for_type scope T)
13.183 @@ -1313,7 +1317,18 @@
13.184 in (ws' @ ws, pool, NameTable.update (v, shape_tuple T R ws') table) end
13.185 else
13.186 let
13.187 - val (j, pool) = fresh arity pool
13.188 + val (j, pool) =
13.189 + case v of
13.190 + ConstName _ =>
13.191 + if is_sel_like_and_no_discr nick then
13.192 + case domain_type T of
13.193 + @{typ "unsigned_bit word"} =>
13.194 + (snd unsigned_bit_word_sel_rel, pool)
13.195 + | @{typ "signed_bit word"} => (snd signed_bit_word_sel_rel, pool)
13.196 + | _ => fresh arity pool
13.197 + else
13.198 + fresh arity pool
13.199 + | _ => fresh arity pool
13.200 val w = constr ((arity, j), T, R, nick)
13.201 in (w :: ws, pool, NameTable.update (v, w) table) end
13.202 end
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Dec 14 16:48:49 2009 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Thu Dec 17 15:22:11 2009 +0100
14.3 @@ -7,6 +7,7 @@
14.4
14.5 signature NITPICK_PEEPHOLE =
14.6 sig
14.7 + type n_ary_index = Kodkod.n_ary_index
14.8 type formula = Kodkod.formula
14.9 type int_expr = Kodkod.int_expr
14.10 type rel_expr = Kodkod.rel_expr
14.11 @@ -14,29 +15,29 @@
14.12 type expr_assign = Kodkod.expr_assign
14.13
14.14 type name_pool = {
14.15 - rels: Kodkod.n_ary_index list,
14.16 - vars: Kodkod.n_ary_index list,
14.17 + rels: n_ary_index list,
14.18 + vars: n_ary_index list,
14.19 formula_reg: int,
14.20 rel_reg: int}
14.21
14.22 val initial_pool : name_pool
14.23 - val not3_rel : rel_expr
14.24 - val suc_rel : rel_expr
14.25 - val nat_add_rel : rel_expr
14.26 - val int_add_rel : rel_expr
14.27 - val nat_subtract_rel : rel_expr
14.28 - val int_subtract_rel : rel_expr
14.29 - val nat_multiply_rel : rel_expr
14.30 - val int_multiply_rel : rel_expr
14.31 - val nat_divide_rel : rel_expr
14.32 - val int_divide_rel : rel_expr
14.33 - val nat_modulo_rel : rel_expr
14.34 - val int_modulo_rel : rel_expr
14.35 - val nat_less_rel : rel_expr
14.36 - val int_less_rel : rel_expr
14.37 - val gcd_rel : rel_expr
14.38 - val lcm_rel : rel_expr
14.39 - val norm_frac_rel : rel_expr
14.40 + val not3_rel : n_ary_index
14.41 + val suc_rel : n_ary_index
14.42 + val unsigned_bit_word_sel_rel : n_ary_index
14.43 + val signed_bit_word_sel_rel : n_ary_index
14.44 + val nat_add_rel : n_ary_index
14.45 + val int_add_rel : n_ary_index
14.46 + val nat_subtract_rel : n_ary_index
14.47 + val int_subtract_rel : n_ary_index
14.48 + val nat_multiply_rel : n_ary_index
14.49 + val int_multiply_rel : n_ary_index
14.50 + val nat_divide_rel : n_ary_index
14.51 + val int_divide_rel : n_ary_index
14.52 + val nat_less_rel : n_ary_index
14.53 + val int_less_rel : n_ary_index
14.54 + val gcd_rel : n_ary_index
14.55 + val lcm_rel : n_ary_index
14.56 + val norm_frac_rel : n_ary_index
14.57 val atom_for_bool : int -> bool -> rel_expr
14.58 val formula_for_bool : bool -> formula
14.59 val atom_for_nat : int * int -> int -> int
14.60 @@ -44,6 +45,7 @@
14.61 val max_int_for_card : int -> int
14.62 val int_for_atom : int * int -> int -> int
14.63 val atom_for_int : int * int -> int -> int
14.64 + val is_twos_complement_representable : int -> int -> bool
14.65 val inline_rel_expr : rel_expr -> bool
14.66 val empty_n_ary_rel : int -> rel_expr
14.67 val num_seq : int -> int -> int_expr list
14.68 @@ -105,23 +107,23 @@
14.69 {rels = [(2, 10), (3, 20), (4, 10)], vars = [], formula_reg = 10,
14.70 rel_reg = 10}
14.71
14.72 -val not3_rel = Rel (2, 0)
14.73 -val suc_rel = Rel (2, 1)
14.74 -val nat_add_rel = Rel (3, 0)
14.75 -val int_add_rel = Rel (3, 1)
14.76 -val nat_subtract_rel = Rel (3, 2)
14.77 -val int_subtract_rel = Rel (3, 3)
14.78 -val nat_multiply_rel = Rel (3, 4)
14.79 -val int_multiply_rel = Rel (3, 5)
14.80 -val nat_divide_rel = Rel (3, 6)
14.81 -val int_divide_rel = Rel (3, 7)
14.82 -val nat_modulo_rel = Rel (3, 8)
14.83 -val int_modulo_rel = Rel (3, 9)
14.84 -val nat_less_rel = Rel (3, 10)
14.85 -val int_less_rel = Rel (3, 11)
14.86 -val gcd_rel = Rel (3, 12)
14.87 -val lcm_rel = Rel (3, 13)
14.88 -val norm_frac_rel = Rel (4, 0)
14.89 +val not3_rel = (2, 0)
14.90 +val suc_rel = (2, 1)
14.91 +val unsigned_bit_word_sel_rel = (2, 2)
14.92 +val signed_bit_word_sel_rel = (2, 3)
14.93 +val nat_add_rel = (3, 0)
14.94 +val int_add_rel = (3, 1)
14.95 +val nat_subtract_rel = (3, 2)
14.96 +val int_subtract_rel = (3, 3)
14.97 +val nat_multiply_rel = (3, 4)
14.98 +val int_multiply_rel = (3, 5)
14.99 +val nat_divide_rel = (3, 6)
14.100 +val int_divide_rel = (3, 7)
14.101 +val nat_less_rel = (3, 8)
14.102 +val int_less_rel = (3, 9)
14.103 +val gcd_rel = (3, 10)
14.104 +val lcm_rel = (3, 11)
14.105 +val norm_frac_rel = (4, 0)
14.106
14.107 (* int -> bool -> rel_expr *)
14.108 fun atom_for_bool j0 = Atom o Integer.add j0 o int_for_bool
14.109 @@ -140,6 +142,9 @@
14.110 if n < min_int_for_card k orelse n > max_int_for_card k then ~1
14.111 else if n < 0 then n + k + j0
14.112 else n + j0
14.113 +(* int -> int -> bool *)
14.114 +fun is_twos_complement_representable bits n =
14.115 + let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
14.116
14.117 (* rel_expr -> bool *)
14.118 fun is_none_product (Product (r1, r2)) =
14.119 @@ -365,16 +370,28 @@
14.120 (* rel_expr -> rel_expr *)
14.121 fun s_not3 (Atom j) = Atom (if j = main_j0 then j + 1 else j - 1)
14.122 | s_not3 (r as Join (r1, r2)) =
14.123 - if r2 = not3_rel then r1 else Join (r, not3_rel)
14.124 - | s_not3 r = Join (r, not3_rel)
14.125 + if r2 = Rel not3_rel then r1 else Join (r, Rel not3_rel)
14.126 + | s_not3 r = Join (r, Rel not3_rel)
14.127
14.128 (* rel_expr -> rel_expr -> formula *)
14.129 fun s_rel_eq r1 r2 =
14.130 (case (r1, r2) of
14.131 - (Join (r11, r12), _) =>
14.132 - if r12 = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME ()
14.133 - | (_, Join (r21, r22)) =>
14.134 - if r22 = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME ()
14.135 + (Join (r11, Rel x), _) =>
14.136 + if x = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME ()
14.137 + | (_, Join (r21, Rel x)) =>
14.138 + if x = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME ()
14.139 + | (RelIf (f, r11, r12), _) =>
14.140 + if inline_rel_expr r2 then
14.141 + s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)
14.142 + else
14.143 + raise SAME ()
14.144 + | (_, RelIf (f, r21, r22)) =>
14.145 + if inline_rel_expr r1 then
14.146 + s_formula_if f (s_rel_eq r1 r21) (s_rel_eq r1 r22)
14.147 + else
14.148 + raise SAME ()
14.149 + | (RelLet (bs, r1'), Atom _) => s_formula_let bs (s_rel_eq r1' r2)
14.150 + | (Atom _, RelLet (bs, r2')) => s_formula_let bs (s_rel_eq r1 r2')
14.151 | _ => raise SAME ())
14.152 handle SAME () =>
14.153 case rel_expr_equal r1 r2 of
14.154 @@ -499,8 +516,8 @@
14.155 | s_join (r1 as RelIf (f, r11, r12)) r2 =
14.156 if inline_rel_expr r2 then s_rel_if f (s_join r11 r2) (s_join r12 r2)
14.157 else Join (r1, r2)
14.158 - | s_join (r1 as Atom j1) (r2 as Rel (2, j2)) =
14.159 - if r2 = suc_rel then
14.160 + | s_join (r1 as Atom j1) (r2 as Rel (x as (2, j2))) =
14.161 + if x = suc_rel then
14.162 let val n = to_nat j1 + 1 in
14.163 if n < nat_card then from_nat n else None
14.164 end
14.165 @@ -511,8 +528,8 @@
14.166 s_project (s_join r21 r1) is
14.167 else
14.168 Join (r1, r2)
14.169 - | s_join r1 (Join (r21, r22 as Rel (3, j22))) =
14.170 - ((if r22 = nat_add_rel then
14.171 + | s_join r1 (Join (r21, r22 as Rel (x as (3, j22)))) =
14.172 + ((if x = nat_add_rel then
14.173 case (r21, r1) of
14.174 (Atom j1, Atom j2) =>
14.175 let val n = to_nat j1 + to_nat j2 in
14.176 @@ -521,19 +538,19 @@
14.177 | (Atom j, r) =>
14.178 (case to_nat j of
14.179 0 => r
14.180 - | 1 => s_join r suc_rel
14.181 + | 1 => s_join r (Rel suc_rel)
14.182 | _ => raise SAME ())
14.183 | (r, Atom j) =>
14.184 (case to_nat j of
14.185 0 => r
14.186 - | 1 => s_join r suc_rel
14.187 + | 1 => s_join r (Rel suc_rel)
14.188 | _ => raise SAME ())
14.189 | _ => raise SAME ()
14.190 - else if r22 = nat_subtract_rel then
14.191 + else if x = nat_subtract_rel then
14.192 case (r21, r1) of
14.193 (Atom j1, Atom j2) => from_nat (nat_minus (to_nat j1) (to_nat j2))
14.194 | _ => raise SAME ()
14.195 - else if r22 = nat_multiply_rel then
14.196 + else if x = nat_multiply_rel then
14.197 case (r21, r1) of
14.198 (Atom j1, Atom j2) =>
14.199 let val n = to_nat j1 * to_nat j2 in
14.200 @@ -596,20 +613,20 @@
14.201 in aux (arity_of_rel_expr r) r end
14.202
14.203 (* rel_expr -> rel_expr -> rel_expr *)
14.204 - fun s_nat_subtract r1 r2 = fold s_join [r1, r2] nat_subtract_rel
14.205 + fun s_nat_subtract r1 r2 = fold s_join [r1, r2] (Rel nat_subtract_rel)
14.206 fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2)
14.207 - | s_nat_less r1 r2 = fold s_join [r1, r2] nat_less_rel
14.208 + | s_nat_less r1 r2 = fold s_join [r1, r2] (Rel nat_less_rel)
14.209 fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2)
14.210 - | s_int_less r1 r2 = fold s_join [r1, r2] int_less_rel
14.211 + | s_int_less r1 r2 = fold s_join [r1, r2] (Rel int_less_rel)
14.212
14.213 (* rel_expr -> int -> int -> rel_expr *)
14.214 fun d_project_seq r j0 n = Project (r, num_seq j0 n)
14.215 (* rel_expr -> rel_expr *)
14.216 - fun d_not3 r = Join (r, not3_rel)
14.217 + fun d_not3 r = Join (r, Rel not3_rel)
14.218 (* rel_expr -> rel_expr -> rel_expr *)
14.219 - fun d_nat_subtract r1 r2 = List.foldl Join nat_subtract_rel [r1, r2]
14.220 - fun d_nat_less r1 r2 = List.foldl Join nat_less_rel [r1, r2]
14.221 - fun d_int_less r1 r2 = List.foldl Join int_less_rel [r1, r2]
14.222 + fun d_nat_subtract r1 r2 = List.foldl Join (Rel nat_subtract_rel) [r1, r2]
14.223 + fun d_nat_less r1 r2 = List.foldl Join (Rel nat_less_rel) [r1, r2]
14.224 + fun d_int_less r1 r2 = List.foldl Join (Rel int_less_rel) [r1, r2]
14.225 in
14.226 if optim then
14.227 {kk_all = s_all, kk_exist = s_exist, kk_formula_let = s_formula_let,
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Dec 14 16:48:49 2009 +0100
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Dec 17 15:22:11 2009 +0100
15.3 @@ -30,6 +30,7 @@
15.4 type scope = {
15.5 ext_ctxt: extended_context,
15.6 card_assigns: (typ * int) list,
15.7 + bits: int,
15.8 bisim_depth: int,
15.9 datatypes: dtype_spec list,
15.10 ofs: int Typtab.table}
15.11 @@ -48,7 +49,8 @@
15.12 val all_scopes :
15.13 extended_context -> int -> (typ option * int list) list
15.14 -> (styp option * int list) list -> (styp option * int list) list
15.15 - -> int list -> typ list -> typ list -> typ list -> int * scope list
15.16 + -> int list -> int list -> typ list -> typ list -> typ list
15.17 + -> int * scope list
15.18 end;
15.19
15.20 structure Nitpick_Scope : NITPICK_SCOPE =
15.21 @@ -77,6 +79,7 @@
15.22 type scope = {
15.23 ext_ctxt: extended_context,
15.24 card_assigns: (typ * int) list,
15.25 + bits: int,
15.26 bisim_depth: int,
15.27 datatypes: dtype_spec list,
15.28 ofs: int Typtab.table}
15.29 @@ -104,7 +107,8 @@
15.30 | is_complete_type dtypes (Type ("*", Ts)) =
15.31 forall (is_complete_type dtypes) Ts
15.32 | is_complete_type dtypes T =
15.33 - not (is_integer_type T) andalso #complete (the (datatype_spec dtypes T))
15.34 + not (is_integer_type T) andalso not (is_bit_type T)
15.35 + andalso #complete (the (datatype_spec dtypes T))
15.36 handle Option.Option => true
15.37 and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
15.38 is_complete_type dtypes T1 andalso is_concrete_type dtypes T2
15.39 @@ -128,13 +132,16 @@
15.40 (* (string -> string) -> scope
15.41 -> string list * string list * string list * string list * string list *)
15.42 fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
15.43 - bisim_depth, datatypes, ...} : scope) =
15.44 + bits, bisim_depth, datatypes, ...} : scope) =
15.45 let
15.46 + val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
15.47 + @{typ bisim_iterator}]
15.48 val (iter_assigns, card_assigns) =
15.49 - card_assigns |> filter_out (curry (op =) @{typ bisim_iterator} o fst)
15.50 + card_assigns |> filter_out (member (op =) boring_Ts o fst)
15.51 |> List.partition (is_fp_iterator_type o fst)
15.52 - val (unimportant_card_assigns, important_card_assigns) =
15.53 - card_assigns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
15.54 + val (secondary_card_assigns, primary_card_assigns) =
15.55 + card_assigns |> List.partition ((is_integer_type orf is_datatype thy)
15.56 + o fst)
15.57 val cards =
15.58 map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
15.59 string_of_int k)
15.60 @@ -152,23 +159,24 @@
15.61 quote (Syntax.string_of_term ctxt
15.62 (Const (const_for_iterator_type T))) ^ " = " ^
15.63 string_of_int (k - 1)) iter_assigns
15.64 - fun bisims () =
15.65 - if bisim_depth < 0 andalso forall (not o #co) datatypes then []
15.66 - else ["bisim_depth = " ^ string_of_int bisim_depth]
15.67 + fun miscs () =
15.68 + (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
15.69 + (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
15.70 + else ["bisim_depth = " ^ string_of_int bisim_depth])
15.71 in
15.72 setmp_show_all_types
15.73 - (fn () => (cards important_card_assigns, cards unimportant_card_assigns,
15.74 - maxes (), iters (), bisims ())) ()
15.75 + (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
15.76 + maxes (), iters (), miscs ())) ()
15.77 end
15.78
15.79 (* scope -> bool -> Pretty.T list *)
15.80 fun pretties_for_scope scope verbose =
15.81 let
15.82 - val (important_cards, unimportant_cards, maxes, iters, bisim_depths) =
15.83 + val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
15.84 quintuple_for_scope maybe_quote scope
15.85 - val ss = map (prefix "card ") important_cards @
15.86 + val ss = map (prefix "card ") primary_cards @
15.87 (if verbose then
15.88 - map (prefix "card ") unimportant_cards @
15.89 + map (prefix "card ") secondary_cards @
15.90 map (prefix "max ") maxes @
15.91 map (prefix "iter ") iters @
15.92 bisim_depths
15.93 @@ -182,9 +190,9 @@
15.94 (* scope -> string *)
15.95 fun multiline_string_for_scope scope =
15.96 let
15.97 - val (important_cards, unimportant_cards, maxes, iters, bisim_depths) =
15.98 + val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
15.99 quintuple_for_scope I scope
15.100 - val cards = important_cards @ unimportant_cards
15.101 + val cards = primary_cards @ secondary_cards
15.102 in
15.103 case (if null cards then [] else ["card: " ^ commas cards]) @
15.104 (if null maxes then [] else ["max: " ^ commas maxes]) @
15.105 @@ -230,15 +238,21 @@
15.106 SOME (Max constr, lookup_const_ints_assign thy maxes_assigns constr)
15.107 handle TERM ("lookup_const_ints_assign", _) => NONE
15.108
15.109 +val max_bits = 31 (* Kodkod limit *)
15.110 +
15.111 (* extended_context -> (typ option * int list) list
15.112 -> (styp option * int list) list -> (styp option * int list) list -> int list
15.113 - -> typ -> block *)
15.114 + -> int list -> typ -> block *)
15.115 fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns
15.116 - iters_assigns bisim_depths T =
15.117 - if T = @{typ bisim_iterator} then
15.118 - [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)]
15.119 + iters_assigns bitss bisim_depths T =
15.120 + if T = @{typ unsigned_bit} then
15.121 + [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
15.122 + else if T = @{typ signed_bit} then
15.123 + [(Card T, map (Integer.add 1 o Integer.min max_bits o Integer.max 1) bitss)]
15.124 + else if T = @{typ bisim_iterator} then
15.125 + [(Card T, map (Integer.add 1 o Integer.max 0) bisim_depths)]
15.126 else if is_fp_iterator_type T then
15.127 - [(Card T, map (fn k => Int.max (0, k) + 1)
15.128 + [(Card T, map (Integer.add 1 o Integer.max 0)
15.129 (lookup_const_ints_assign thy iters_assigns
15.130 (const_for_iterator_type T)))]
15.131 else
15.132 @@ -249,13 +263,13 @@
15.133
15.134 (* extended_context -> (typ option * int list) list
15.135 -> (styp option * int list) list -> (styp option * int list) list -> int list
15.136 - -> typ list -> typ list -> block list *)
15.137 -fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns
15.138 + -> int list -> typ list -> typ list -> block list *)
15.139 +fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns bitss
15.140 bisim_depths mono_Ts nonmono_Ts =
15.141 let
15.142 (* typ -> block *)
15.143 val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns
15.144 - iters_assigns bisim_depths
15.145 + iters_assigns bitss bisim_depths
15.146 val mono_block = maps block_for mono_Ts
15.147 val nonmono_blocks = map block_for nonmono_Ts
15.148 in mono_block :: nonmono_blocks end
15.149 @@ -388,7 +402,7 @@
15.150 -> int Typtab.table *)
15.151 fun aux next _ [] = Typtab.update_new (dummyT, next)
15.152 | aux next reusable ((T, k) :: assigns) =
15.153 - if k = 1 orelse is_integer_type T then
15.154 + if k = 1 orelse is_integer_type T orelse is_bit_type T then
15.155 aux next reusable assigns
15.156 else if length (these (Option.map #constrs (datatype_spec dtypes T)))
15.157 > 1 then
15.158 @@ -472,6 +486,14 @@
15.159 shallow = shallow, constrs = constrs}
15.160 end
15.161
15.162 +(* int -> int *)
15.163 +fun min_bits_for_nat_value n = if n <= 0 then 0 else IntInf.log2 n + 1
15.164 +(* scope_desc -> int *)
15.165 +fun min_bits_for_max_assigns (_, []) = 0
15.166 + | min_bits_for_max_assigns (card_assigns, max_assigns) =
15.167 + min_bits_for_nat_value (fold Integer.max
15.168 + (map snd card_assigns @ map snd max_assigns) 0)
15.169 +
15.170 (* extended_context -> int -> typ list -> scope_desc -> scope *)
15.171 fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
15.172 (desc as (card_assigns, _)) =
15.173 @@ -479,25 +501,29 @@
15.174 val datatypes =
15.175 map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
15.176 (filter (is_datatype thy o fst) card_assigns)
15.177 + val bits = card_of_type card_assigns @{typ signed_bit} - 1
15.178 + handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
15.179 + card_of_type card_assigns @{typ unsigned_bit}
15.180 + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
15.181 val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
15.182 in
15.183 {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes,
15.184 - bisim_depth = bisim_depth,
15.185 + bits = bits, bisim_depth = bisim_depth,
15.186 ofs = if sym_break <= 0 then Typtab.empty
15.187 else offset_table_for_card_assigns thy card_assigns datatypes}
15.188 end
15.189
15.190 (* theory -> typ list -> (typ option * int list) list
15.191 -> (typ option * int list) list *)
15.192 -fun fix_cards_assigns_wrt_boxing _ _ [] = []
15.193 - | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
15.194 +fun repair_cards_assigns_wrt_boxing _ _ [] = []
15.195 + | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
15.196 (if is_fun_type T orelse is_pair_type T then
15.197 - Ts |> filter (curry (type_match thy o swap) T o unbox_type)
15.198 + Ts |> filter (curry (type_match thy o swap) T o unbit_and_unbox_type)
15.199 |> map (rpair ks o SOME)
15.200 else
15.201 - [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_assigns
15.202 - | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) =
15.203 - (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_assigns
15.204 + [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
15.205 + | repair_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) =
15.206 + (NONE, ks) :: repair_cards_assigns_wrt_boxing thy Ts cards_assigns
15.207
15.208 val max_scopes = 4096
15.209 val distinct_threshold = 512
15.210 @@ -506,11 +532,14 @@
15.211 -> (styp option * int list) list -> (styp option * int list) list -> int list
15.212 -> typ list -> typ list -> typ list -> int * scope list *)
15.213 fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
15.214 - iters_assigns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
15.215 + iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
15.216 + shallow_dataTs =
15.217 let
15.218 - val cards_assigns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_assigns
15.219 + val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
15.220 + cards_assigns
15.221 val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns
15.222 - iters_assigns bisim_depths mono_Ts nonmono_Ts
15.223 + iters_assigns bitss bisim_depths mono_Ts
15.224 + nonmono_Ts
15.225 val ranks = map rank_of_block blocks
15.226 val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
15.227 val head = take max_scopes all
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Dec 14 16:48:49 2009 +0100
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Dec 17 15:22:11 2009 +0100
16.3 @@ -300,6 +300,7 @@
16.4 val peephole_optim = true
16.5 val nat_card = 4
16.6 val int_card = 9
16.7 + val bits = 8
16.8 val j0 = 0
16.9 val constrs = kodkod_constrs peephole_optim nat_card int_card j0
16.10 val (free_rels, pool, table) =
16.11 @@ -307,7 +308,7 @@
16.12 NameTable.empty
16.13 val u = Op1 (Not, type_of u, rep_of u, u)
16.14 |> rename_vars_in_nut pool table
16.15 - val formula = kodkod_formula_from_nut Typtab.empty false constrs u
16.16 + val formula = kodkod_formula_from_nut bits Typtab.empty false constrs u
16.17 val bounds = map (bound_for_plain_rel ctxt debug) free_rels
16.18 val univ_card = univ_card nat_card int_card j0 bounds formula
16.19 val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)
17.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Dec 14 16:48:49 2009 +0100
17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Dec 17 15:22:11 2009 +0100
17.3 @@ -12,7 +12,8 @@
17.4
17.5 exception ARG of string * string
17.6 exception BAD of string * string
17.7 - exception LIMIT of string * string
17.8 + exception TOO_SMALL of string * string
17.9 + exception TOO_LARGE of string * string
17.10 exception NOT_SUPPORTED of string
17.11 exception SAME of unit
17.12
17.13 @@ -51,7 +52,6 @@
17.14 val bool_T : typ
17.15 val nat_T : typ
17.16 val int_T : typ
17.17 - val subscript : string -> string
17.18 val nat_subscript : int -> string
17.19 val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
17.20 val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
17.21 @@ -71,7 +71,8 @@
17.22
17.23 exception ARG of string * string
17.24 exception BAD of string * string
17.25 -exception LIMIT of string * string
17.26 +exception TOO_SMALL of string * string
17.27 +exception TOO_LARGE of string * string
17.28 exception NOT_SUPPORTED of string
17.29 exception SAME of unit
17.30
17.31 @@ -96,14 +97,16 @@
17.32 | reasonable_power 0 _ = 0
17.33 | reasonable_power 1 _ = 1
17.34 | reasonable_power a b =
17.35 - if b < 0 orelse b > max_exponent then
17.36 - raise LIMIT ("Nitpick_Util.reasonable_power",
17.37 - "too large exponent (" ^ signed_string_of_int b ^ ")")
17.38 + if b < 0 then
17.39 + raise ARG ("Nitpick_Util.reasonable_power",
17.40 + "negative exponent (" ^ signed_string_of_int b ^ ")")
17.41 + else if b > max_exponent then
17.42 + raise TOO_LARGE ("Nitpick_Util.reasonable_power",
17.43 + "too large exponent (" ^ signed_string_of_int b ^ ")")
17.44 else
17.45 - let
17.46 - val c = reasonable_power a (b div 2) in
17.47 - c * c * reasonable_power a (b mod 2)
17.48 - end
17.49 + let val c = reasonable_power a (b div 2) in
17.50 + c * c * reasonable_power a (b mod 2)
17.51 + end
17.52
17.53 (* int -> int -> int *)
17.54 fun exact_log m n =
17.55 @@ -247,7 +250,11 @@
17.56 (* string -> string *)
17.57 val subscript = implode o map (prefix "\<^isub>") o explode
17.58 (* int -> string *)
17.59 -val nat_subscript = subscript o signed_string_of_int
17.60 +fun nat_subscript n =
17.61 + (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
17.62 + numbers *)
17.63 + if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>"
17.64 + else subscript (string_of_int n)
17.65
17.66 (* Time.time option -> ('a -> 'b) -> 'a -> 'b *)
17.67 fun time_limit NONE = I