1.1 --- a/doc-src/Nitpick/nitpick.tex Thu Dec 17 15:22:27 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Fri Dec 18 12:00:29 2009 +0100
1.3 @@ -740,7 +740,7 @@
1.4
1.5 \prew
1.6 \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
1.7 -\textbf{nitpick}~[\textit{card nat}~= 100,\, \textit{verbose}] \\[2\smallskipamount]
1.8 +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
1.9 \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
1.10 Nitpick can compute it efficiently. \\[2\smallskipamount]
1.11 Trying 1 scope: \\
1.12 @@ -758,7 +758,7 @@
1.13
1.14 \prew
1.15 \textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
1.16 -\textbf{nitpick}~[\textit{card nat}~= 100] \\[2\smallskipamount]
1.17 +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount]
1.18 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.19 \hbox{}\qquad Empty assignment
1.20 \postw
1.21 @@ -1752,7 +1752,7 @@
1.22
1.23 \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
1.24 problems that refer to the types \textit{rat} or \textit{real} or the constants
1.25 -\textit{gcd} or \textit{lcm}.
1.26 +\textit{Suc}, \textit{gcd}, or \textit{lcm}.
1.27
1.28 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
1.29 \textit{show\_datatypes} (\S\ref{output-format}).}
2.1 --- a/src/HOL/Divides.thy Thu Dec 17 15:22:27 2009 +0100
2.2 +++ b/src/HOL/Divides.thy Fri Dec 18 12:00:29 2009 +0100
2.3 @@ -2443,6 +2443,17 @@
2.4 declare dvd_eq_mod_eq_0_number_of [simp]
2.5
2.6
2.7 +subsubsection {* Nitpick *}
2.8 +
2.9 +lemma zmod_zdiv_equality':
2.10 +"(m\<Colon>int) mod n = m - (m div n) * n"
2.11 +by (rule_tac P="%x. m mod n = x - (m div n) * n"
2.12 + in subst [OF mod_div_equality [of _ n]])
2.13 + arith
2.14 +
2.15 +lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection]
2.16 + zmod_zdiv_equality' [THEN eq_reflection]
2.17 +
2.18 subsubsection {* Code generation *}
2.19
2.20 definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
3.1 --- a/src/HOL/IsaMakefile Thu Dec 17 15:22:27 2009 +0100
3.2 +++ b/src/HOL/IsaMakefile Fri Dec 18 12:00:29 2009 +0100
3.3 @@ -610,13 +610,13 @@
3.4
3.5 HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
3.6
3.7 -$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
3.8 - Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
3.9 - Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \
3.10 - Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
3.11 - Nitpick_Examples/Nitpick_Examples.thy \
3.12 - Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
3.13 - Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
3.14 +$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
3.15 + Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
3.16 + Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Integer_Nits.thy \
3.17 + Nitpick_Examples/Manual_Nits.thy Nitpick_Examples/Mini_Nits.thy \
3.18 + Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
3.19 + Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
3.20 + Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
3.21 Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
3.22 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
3.23
4.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Thu Dec 17 15:22:27 2009 +0100
4.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Dec 18 12:00:29 2009 +0100
4.3 @@ -876,7 +876,7 @@
4.4 by auto
4.5
4.6 lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
4.7 -nitpick [expect = none]
4.8 +nitpick [card = 1\<midarrow>7, expect = none]
4.9 by auto
4.10
4.11 lemma "A \<union> - A = UNIV"
4.12 @@ -892,7 +892,7 @@
4.13 oops
4.14
4.15 lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
4.16 -nitpick [expect = none]
4.17 +nitpick [card = 1\<midarrow>7, expect = none]
4.18 oops
4.19
4.20 lemma "finite A"
5.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Thu Dec 17 15:22:27 2009 +0100
5.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Dec 18 12:00:29 2009 +0100
5.3 @@ -14,21 +14,11 @@
5.4 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
5.5
5.6 primrec rot where
5.7 -"rot Nibble0 = Nibble1" |
5.8 -"rot Nibble1 = Nibble2" |
5.9 -"rot Nibble2 = Nibble3" |
5.10 -"rot Nibble3 = Nibble4" |
5.11 -"rot Nibble4 = Nibble5" |
5.12 -"rot Nibble5 = Nibble6" |
5.13 -"rot Nibble6 = Nibble7" |
5.14 -"rot Nibble7 = Nibble8" |
5.15 -"rot Nibble8 = Nibble9" |
5.16 -"rot Nibble9 = NibbleA" |
5.17 -"rot NibbleA = NibbleB" |
5.18 -"rot NibbleB = NibbleC" |
5.19 -"rot NibbleC = NibbleD" |
5.20 -"rot NibbleD = NibbleE" |
5.21 -"rot NibbleE = NibbleF" |
5.22 +"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
5.23 +"rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
5.24 +"rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" |
5.25 +"rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" |
5.26 +"rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" |
5.27 "rot NibbleF = Nibble0"
5.28
5.29 lemma "rot n \<noteq> n"
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Fri Dec 18 12:00:29 2009 +0100
6.3 @@ -0,0 +1,209 @@
6.4 +(* Title: HOL/Nitpick_Examples/Integer_Nits.thy
6.5 + Author: Jasmin Blanchette, TU Muenchen
6.6 + Copyright 2009
6.7 +
6.8 +Examples featuring Nitpick applied to natural numbers and integers.
6.9 +*)
6.10 +
6.11 +header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *}
6.12 +
6.13 +theory Integer_Nits
6.14 +imports Nitpick
6.15 +begin
6.16 +
6.17 +nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
6.18 + card = 1\<midarrow>6, bits = 1,2,3,4,6,8]
6.19 +
6.20 +lemma "Suc x = x + 1"
6.21 +nitpick [unary_ints, expect = none]
6.22 +nitpick [binary_ints, expect = none]
6.23 +sorry
6.24 +
6.25 +lemma "x < Suc x"
6.26 +nitpick [unary_ints, expect = none]
6.27 +nitpick [binary_ints, expect = none]
6.28 +sorry
6.29 +
6.30 +lemma "x + y \<ge> (x::nat)"
6.31 +nitpick [unary_ints, expect = none]
6.32 +nitpick [binary_ints, expect = none]
6.33 +sorry
6.34 +
6.35 +lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::nat)"
6.36 +nitpick [unary_ints, expect = none]
6.37 +nitpick [binary_ints, expect = none]
6.38 +sorry
6.39 +
6.40 +lemma "x + y = y + (x::nat)"
6.41 +nitpick [unary_ints, expect = none]
6.42 +nitpick [binary_ints, expect = none]
6.43 +sorry
6.44 +
6.45 +lemma "x > y \<Longrightarrow> x - y \<noteq> (0::nat)"
6.46 +nitpick [unary_ints, expect = none]
6.47 +nitpick [binary_ints, expect = none]
6.48 +sorry
6.49 +
6.50 +lemma "x \<le> y \<Longrightarrow> x - y = (0::nat)"
6.51 +nitpick [unary_ints, expect = none]
6.52 +nitpick [binary_ints, expect = none]
6.53 +sorry
6.54 +
6.55 +lemma "x - (0::nat) = x"
6.56 +nitpick [unary_ints, expect = none]
6.57 +nitpick [binary_ints, expect = none]
6.58 +sorry
6.59 +
6.60 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::nat)"
6.61 +nitpick [unary_ints, expect = none]
6.62 +nitpick [binary_ints, expect = none]
6.63 +sorry
6.64 +
6.65 +lemma "0 * y = (0::nat)"
6.66 +nitpick [unary_ints, expect = none]
6.67 +nitpick [binary_ints, expect = none]
6.68 +sorry
6.69 +
6.70 +lemma "y * 0 = (0::nat)"
6.71 +nitpick [unary_ints, expect = none]
6.72 +nitpick [binary_ints, expect = none]
6.73 +sorry
6.74 +
6.75 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::nat)"
6.76 +nitpick [unary_ints, expect = none]
6.77 +nitpick [binary_ints, expect = none]
6.78 +sorry
6.79 +
6.80 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::nat)"
6.81 +nitpick [unary_ints, expect = none]
6.82 +nitpick [binary_ints, expect = none]
6.83 +sorry
6.84 +
6.85 +lemma "x * y div y = (x::nat)"
6.86 +nitpick [unary_ints, expect = genuine]
6.87 +nitpick [binary_ints, expect = genuine]
6.88 +oops
6.89 +
6.90 +lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::nat)"
6.91 +nitpick [unary_ints, expect = none]
6.92 +nitpick [binary_ints, expect = none]
6.93 +sorry
6.94 +
6.95 +lemma "5 * 55 < (260::nat)"
6.96 +nitpick [unary_ints, expect = none]
6.97 +nitpick [binary_ints, expect = none]
6.98 +nitpick [binary_ints, bits = 9, expect = genuine]
6.99 +oops
6.100 +
6.101 +lemma "nat (of_nat n) = n"
6.102 +nitpick [unary_ints, expect = none]
6.103 +nitpick [binary_ints, expect = none]
6.104 +sorry
6.105 +
6.106 +lemma "x + y \<ge> (x::int)"
6.107 +nitpick [unary_ints, expect = genuine]
6.108 +nitpick [binary_ints, expect = genuine]
6.109 +oops
6.110 +
6.111 +lemma "\<lbrakk>x \<ge> 0; y \<ge> 0\<rbrakk> \<Longrightarrow> x + y \<ge> (0::int)"
6.112 +nitpick [unary_ints, expect = none]
6.113 +nitpick [binary_ints, expect = none]
6.114 +sorry
6.115 +
6.116 +lemma "y \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
6.117 +nitpick [unary_ints, expect = none]
6.118 +nitpick [binary_ints, expect = none]
6.119 +sorry
6.120 +
6.121 +lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (y::int)"
6.122 +nitpick [unary_ints, expect = none]
6.123 +nitpick [binary_ints, expect = none]
6.124 +sorry
6.125 +
6.126 +lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)"
6.127 +nitpick [unary_ints, expect = genuine]
6.128 +nitpick [binary_ints, expect = genuine]
6.129 +oops
6.130 +
6.131 +lemma "\<lbrakk>x \<le> 0; y \<le> 0\<rbrakk> \<Longrightarrow> x + y \<le> (0::int)"
6.132 +nitpick [unary_ints, expect = none]
6.133 +nitpick [binary_ints, expect = none]
6.134 +sorry
6.135 +
6.136 +lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::int)"
6.137 +nitpick [unary_ints, expect = genuine]
6.138 +nitpick [binary_ints, expect = genuine]
6.139 +oops
6.140 +
6.141 +lemma "x + y = y + (x::int)"
6.142 +nitpick [unary_ints, expect = none]
6.143 +nitpick [binary_ints, expect = none]
6.144 +sorry
6.145 +
6.146 +lemma "x > y \<Longrightarrow> x - y \<noteq> (0::int)"
6.147 +nitpick [unary_ints, expect = none]
6.148 +nitpick [binary_ints, expect = none]
6.149 +sorry
6.150 +
6.151 +lemma "x \<le> y \<Longrightarrow> x - y = (0::int)"
6.152 +nitpick [unary_ints, expect = genuine]
6.153 +nitpick [binary_ints, expect = genuine]
6.154 +oops
6.155 +
6.156 +lemma "x - (0::int) = x"
6.157 +nitpick [unary_ints, expect = none]
6.158 +nitpick [binary_ints, expect = none]
6.159 +sorry
6.160 +
6.161 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::int)"
6.162 +nitpick [unary_ints, expect = none]
6.163 +nitpick [binary_ints, expect = none]
6.164 +sorry
6.165 +
6.166 +lemma "0 * y = (0::int)"
6.167 +nitpick [unary_ints, expect = none]
6.168 +nitpick [binary_ints, expect = none]
6.169 +sorry
6.170 +
6.171 +lemma "y * 0 = (0::int)"
6.172 +nitpick [unary_ints, expect = none]
6.173 +nitpick [binary_ints, expect = none]
6.174 +sorry
6.175 +
6.176 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::int)"
6.177 +nitpick [unary_ints, expect = genuine]
6.178 +nitpick [binary_ints, expect = genuine]
6.179 +oops
6.180 +
6.181 +lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::int)"
6.182 +nitpick [unary_ints, expect = genuine]
6.183 +nitpick [binary_ints, expect = genuine]
6.184 +oops
6.185 +
6.186 +lemma "x * y div y = (x::int)"
6.187 +nitpick [unary_ints, expect = genuine]
6.188 +nitpick [binary_ints, expect = genuine]
6.189 +oops
6.190 +
6.191 +lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
6.192 +nitpick [unary_ints, expect = none]
6.193 +nitpick [binary_ints, expect = none, card = 1\<midarrow>5, bits = 1\<midarrow>5]
6.194 +sorry
6.195 +
6.196 +lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"
6.197 +nitpick [unary_ints, expect = none]
6.198 +nitpick [binary_ints, expect = none]
6.199 +sorry
6.200 +
6.201 +lemma "-5 * 55 > (-260::int)"
6.202 +nitpick [unary_ints, expect = none]
6.203 +nitpick [binary_ints, expect = none]
6.204 +nitpick [binary_ints, bits = 9, expect = genuine]
6.205 +oops
6.206 +
6.207 +lemma "nat (of_nat n) = n"
6.208 +nitpick [unary_ints, expect = none]
6.209 +nitpick [binary_ints, expect = none]
6.210 +sorry
6.211 +
6.212 +end
7.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Dec 17 15:22:27 2009 +0100
7.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Dec 18 12:00:29 2009 +0100
7.3 @@ -59,7 +59,7 @@
7.4 nitpick
7.5 oops
7.6
7.7 -subsection {* 3.5. Numbers *}
7.8 +subsection {* 3.5. Natural Numbers and Integers *}
7.9
7.10 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
7.11 nitpick
7.12 @@ -121,11 +121,11 @@
7.13 "even n \<Longrightarrow> even (Suc (Suc n))"
7.14
7.15 lemma "\<exists>n. even n \<and> even (Suc n)"
7.16 -nitpick [card nat = 100, verbose]
7.17 +nitpick [card nat = 100, unary_ints, verbose]
7.18 oops
7.19
7.20 lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
7.21 -nitpick [card nat = 100]
7.22 +nitpick [card nat = 100, unary_ints, verbose]
7.23 oops
7.24
7.25 inductive even' where
7.26 @@ -134,7 +134,7 @@
7.27 "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
7.28
7.29 lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
7.30 -nitpick [card nat = 10, verbose, show_consts]
7.31 +nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
7.32 oops
7.33
7.34 lemma "even' (n - 2) \<Longrightarrow> even' n"
8.1 --- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Thu Dec 17 15:22:27 2009 +0100
8.2 +++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Fri Dec 18 12:00:29 2009 +0100
8.3 @@ -6,9 +6,8 @@
8.4 *)
8.5
8.6 theory Nitpick_Examples
8.7 -imports Core_Nits Datatype_Nits Induct_Nits Manual_Nits Mini_Nits Mono_Nits
8.8 - Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
8.9 +imports Core_Nits Datatype_Nits Induct_Nits Integer_Nits Manual_Nits Mini_Nits
8.10 + Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
8.11 Typedef_Nits
8.12 begin
8.13 -
8.14 end
9.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Thu Dec 17 15:22:27 2009 +0100
9.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Fri Dec 18 12:00:29 2009 +0100
9.3 @@ -135,7 +135,7 @@
9.4 lemma "\<forall>a. g a = a
9.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).
9.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"
9.7 -nitpick [expect = none]
9.8 +nitpick [expect = potential]
9.9 nitpick [dont_specialize, expect = none]
9.10 nitpick [dont_box, expect = none]
9.11 nitpick [dont_box, dont_specialize, expect = none]
10.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Dec 17 15:22:27 2009 +0100
10.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Dec 18 12:00:29 2009 +0100
10.3 @@ -11,7 +11,7 @@
10.4 imports Main Rational
10.5 begin
10.6
10.7 -nitpick_params [card = 1\<midarrow>4, timeout = 5 s]
10.8 +nitpick_params [card = 1\<midarrow>4, timeout = 30 s]
10.9
10.10 typedef three = "{0\<Colon>nat, 1, 2}"
10.11 by blast
10.12 @@ -67,7 +67,7 @@
10.13 sorry
10.14
10.15 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
10.16 -nitpick [card = 1\<midarrow>5, timeout = 10 s, expect = genuine]
10.17 +nitpick [card = 1\<midarrow>5, expect = genuine]
10.18 oops
10.19
10.20 lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))"
10.21 @@ -157,15 +157,15 @@
10.22 by (rule Rep_Nat_inverse)
10.23
10.24 lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
10.25 -nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none]
10.26 +nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
10.27 by (rule Zero_int_def_raw)
10.28
10.29 lemma "Abs_Integ (Rep_Integ a) = a"
10.30 -nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none]
10.31 +nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
10.32 by (rule Rep_Integ_inverse)
10.33
10.34 lemma "Abs_list (Rep_list a) = a"
10.35 -nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
10.36 +nitpick [card = 1\<midarrow>2, expect = none]
10.37 by (rule Rep_list_inverse)
10.38
10.39 record point =
11.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Dec 17 15:22:27 2009 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Dec 18 12:00:29 2009 +0100
11.3 @@ -75,6 +75,8 @@
11.4 open Nitpick_Kodkod
11.5 open Nitpick_Model
11.6
11.7 +structure KK = Kodkod
11.8 +
11.9 type params = {
11.10 cards_assigns: (typ option * int list) list,
11.11 maxes_assigns: (styp option * int list) list,
11.12 @@ -126,10 +128,10 @@
11.13 rel_table: nut NameTable.table,
11.14 liberal: bool,
11.15 scope: scope,
11.16 - core: Kodkod.formula,
11.17 - defs: Kodkod.formula list}
11.18 + core: KK.formula,
11.19 + defs: KK.formula list}
11.20
11.21 -type rich_problem = Kodkod.problem * problem_extension
11.22 +type rich_problem = KK.problem * problem_extension
11.23
11.24 (* Proof.context -> string -> term list -> Pretty.T list *)
11.25 fun pretties_for_formulas _ _ [] = []
11.26 @@ -344,8 +346,8 @@
11.27 val _ = if verbose andalso binary_ints = SOME true
11.28 andalso exists (member (op =) [nat_T, int_T]) Ts then
11.29 print_v (K "The option \"binary_ints\" will be ignored because \
11.30 - \of the presence of rationals, reals, \"gcd\", or \
11.31 - \\"lcm\" in the problem.")
11.32 + \of the presence of rationals, reals, \"Suc\", \
11.33 + \\"gcd\", or \"lcm\" in the problem.")
11.34 else
11.35 ()
11.36 val (all_dataTs, all_free_Ts) =
11.37 @@ -447,7 +449,7 @@
11.38 NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1
11.39 val min_univ_card =
11.40 NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table
11.41 - (univ_card nat_card int_card main_j0 [] Kodkod.True)
11.42 + (univ_card nat_card int_card main_j0 [] KK.True)
11.43 val _ = check_arity min_univ_card min_highest_arity
11.44
11.45 val core_u = choose_reps_in_nut scope liberal rep_table false core_u
11.46 @@ -469,7 +471,7 @@
11.47 val core_u = rename_vars_in_nut pool rel_table core_u
11.48 val def_us = map (rename_vars_in_nut pool rel_table) def_us
11.49 val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
11.50 - (* nut -> Kodkod.formula *)
11.51 + (* nut -> KK.formula *)
11.52 val to_f = kodkod_formula_from_nut bits ofs liberal kk
11.53 val core_f = to_f core_u
11.54 val def_fs = map to_f def_us
11.55 @@ -510,7 +512,7 @@
11.56 fold Integer.max (map (fst o fst) (maps fst bounds)) 0
11.57 val formula = fold_rev s_and declarative_axioms formula
11.58 val _ = if bits = 0 then () else check_bits bits formula
11.59 - val _ = if formula = Kodkod.False then ()
11.60 + val _ = if formula = KK.False then ()
11.61 else check_arity univ_card highest_arity
11.62 in
11.63 SOME ({comment = comment, settings = settings, univ_card = univ_card,
11.64 @@ -525,7 +527,7 @@
11.65 defs = nondef_fs @ def_fs @ declarative_axioms})
11.66 end
11.67 handle TOO_LARGE (loc, msg) =>
11.68 - if loc = "Nitpick_Kodkod.check_arity"
11.69 + if loc = "Nitpick_KK.check_arity"
11.70 andalso not (Typtab.is_empty ofs) then
11.71 problem_for_scope liberal
11.72 {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
11.73 @@ -548,10 +550,9 @@
11.74 " component of scope."));
11.75 NONE)
11.76
11.77 - (* int -> (''a * int list list) list -> ''a -> Kodkod.tuple_set *)
11.78 + (* int -> (''a * int list list) list -> ''a -> KK.tuple_set *)
11.79 fun tuple_set_for_rel univ_card =
11.80 - Kodkod.TupleSet o map (kk_tuple debug univ_card) o the
11.81 - oo AList.lookup (op =)
11.82 + KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =)
11.83
11.84 val word_model = if falsify then "counterexample" else "model"
11.85
11.86 @@ -566,7 +567,7 @@
11.87 List.app (Unsynchronized.change checked_problems o Option.map o cons
11.88 o nth problems)
11.89
11.90 - (* bool -> Kodkod.raw_bound list -> problem_extension -> bool option *)
11.91 + (* bool -> KK.raw_bound list -> problem_extension -> bool option *)
11.92 fun print_and_check_model genuine bounds
11.93 ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
11.94 : problem_extension) =
11.95 @@ -663,7 +664,7 @@
11.96 let
11.97 val max_potential = Int.max (0, max_potential)
11.98 val max_genuine = Int.max (0, max_genuine)
11.99 - (* bool -> int * Kodkod.raw_bound list -> bool option *)
11.100 + (* bool -> int * KK.raw_bound list -> bool option *)
11.101 fun print_and_check genuine (j, bounds) =
11.102 print_and_check_model genuine bounds (snd (nth problems j))
11.103 val max_solutions = max_potential + max_genuine
11.104 @@ -672,15 +673,15 @@
11.105 if max_solutions <= 0 then
11.106 (0, 0, donno)
11.107 else
11.108 - case Kodkod.solve_any_problem overlord deadline max_threads
11.109 - max_solutions (map fst problems) of
11.110 - Kodkod.NotInstalled =>
11.111 + case KK.solve_any_problem overlord deadline max_threads max_solutions
11.112 + (map fst problems) of
11.113 + KK.NotInstalled =>
11.114 (print_m install_kodkodi_message;
11.115 (max_potential, max_genuine, donno + 1))
11.116 - | Kodkod.Normal ([], unsat_js) =>
11.117 + | KK.Normal ([], unsat_js) =>
11.118 (update_checked_problems problems unsat_js;
11.119 (max_potential, max_genuine, donno))
11.120 - | Kodkod.Normal (sat_ps, unsat_js) =>
11.121 + | KK.Normal (sat_ps, unsat_js) =>
11.122 let
11.123 val (lib_ps, con_ps) =
11.124 List.partition (#liberal o snd o nth problems o fst) sat_ps
11.125 @@ -739,13 +740,12 @@
11.126 in solve_any_problem 0 max_genuine donno false problems end
11.127 end
11.128 end
11.129 - | Kodkod.TimedOut unsat_js =>
11.130 + | KK.TimedOut unsat_js =>
11.131 (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
11.132 - | Kodkod.Interrupted NONE =>
11.133 - (checked_problems := NONE; do_interrupted ())
11.134 - | Kodkod.Interrupted (SOME unsat_js) =>
11.135 + | KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ())
11.136 + | KK.Interrupted (SOME unsat_js) =>
11.137 (update_checked_problems problems unsat_js; do_interrupted ())
11.138 - | Kodkod.Error (s, unsat_js) =>
11.139 + | KK.Error (s, unsat_js) =>
11.140 (update_checked_problems problems unsat_js;
11.141 print_v (K ("Kodkod error: " ^ s ^ "."));
11.142 (max_potential, max_genuine, donno + 1))
11.143 @@ -787,8 +787,8 @@
11.144 SOME problem =>
11.145 (problems
11.146 |> (null problems orelse
11.147 - not (Kodkod.problems_equivalent (fst problem)
11.148 - (fst (hd problems))))
11.149 + not (KK.problems_equivalent (fst problem)
11.150 + (fst (hd problems))))
11.151 ? cons problem, donno)
11.152 | NONE => (problems, donno + 1))
11.153 val (problems, donno) =
11.154 @@ -832,7 +832,7 @@
11.155 "") ^ "."
11.156 end
11.157
11.158 - (* int -> int -> scope list -> int * int * int -> Kodkod.outcome *)
11.159 + (* int -> int -> scope list -> int * int * int -> KK.outcome *)
11.160 fun run_batches _ _ [] (max_potential, max_genuine, donno) =
11.161 if donno > 0 andalso max_genuine > 0 then
11.162 (print_m (fn () => excipit "ran out of some resource"); "unknown")
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 17 15:22:27 2009 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Dec 18 12:00:29 2009 +0100
12.3 @@ -968,7 +968,8 @@
12.4 | @{typ unit} => 1
12.5 | Type _ =>
12.6 (case datatype_constrs ext_ctxt T of
12.7 - [] => if is_integer_type T then 0 else raise SAME ()
12.8 + [] => if is_integer_type T orelse is_bit_type T then 0
12.9 + else raise SAME ()
12.10 | constrs =>
12.11 let
12.12 val constr_cards =
12.13 @@ -1220,7 +1221,7 @@
12.14
12.15 (* Proof.context -> term list -> const_table *)
12.16 fun const_def_table ctxt ts =
12.17 - table_for (rev o map prop_of o Nitpick_Defs.get) ctxt
12.18 + table_for (map prop_of o Nitpick_Defs.get) ctxt
12.19 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
12.20 (map pair_for_prop ts)
12.21 (* term list -> const_table *)
12.22 @@ -3350,13 +3351,13 @@
12.23 (* term -> bool *)
12.24 fun may_use_binary_ints (t1 $ t2) =
12.25 may_use_binary_ints t1 andalso may_use_binary_ints t2
12.26 - | may_use_binary_ints (Const (s, _)) =
12.27 + | may_use_binary_ints (t as Const (s, _)) =
12.28 + t <> @{const Suc} andalso
12.29 not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
12.30 - @{const_name Frac}, @{const_name norm_frac},
12.31 - @{const_name nat_gcd}, @{const_name nat_lcm}] s)
12.32 + @{const_name nat_gcd}, @{const_name nat_lcm},
12.33 + @{const_name Frac}, @{const_name norm_frac}] s)
12.34 | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
12.35 | may_use_binary_ints _ = true
12.36 -
12.37 fun should_use_binary_ints (t1 $ t2) =
12.38 should_use_binary_ints t1 orelse should_use_binary_ints t2
12.39 | should_use_binary_ints (Const (s, _)) =
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Dec 17 15:22:27 2009 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Dec 18 12:00:29 2009 +0100
13.3 @@ -49,44 +49,46 @@
13.4 open Nitpick_Rep
13.5 open Nitpick_Nut
13.6
13.7 -type nfa_transition = Kodkod.rel_expr * typ
13.8 +structure KK = Kodkod
13.9 +
13.10 +type nfa_transition = KK.rel_expr * typ
13.11 type nfa_entry = typ * nfa_transition list
13.12 type nfa_table = nfa_entry list
13.13
13.14 structure NfaGraph = Graph(type key = typ val ord = TermOrd.typ_ord)
13.15
13.16 -(* int -> Kodkod.int_expr list *)
13.17 -fun flip_nums n = index_seq 1 n @ [0] |> map Kodkod.Num
13.18 +(* int -> KK.int_expr list *)
13.19 +fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
13.20
13.21 -(* int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int *)
13.22 +(* int -> int -> int -> KK.bound list -> KK.formula -> int *)
13.23 fun univ_card nat_card int_card main_j0 bounds formula =
13.24 let
13.25 - (* Kodkod.rel_expr -> int -> int *)
13.26 + (* KK.rel_expr -> int -> int *)
13.27 fun rel_expr_func r k =
13.28 Int.max (k, case r of
13.29 - Kodkod.Atom j => j + 1
13.30 - | Kodkod.AtomSeq (k', j0) => j0 + k'
13.31 + KK.Atom j => j + 1
13.32 + | KK.AtomSeq (k', j0) => j0 + k'
13.33 | _ => 0)
13.34 - (* Kodkod.tuple -> int -> int *)
13.35 + (* KK.tuple -> int -> int *)
13.36 fun tuple_func t k =
13.37 case t of
13.38 - Kodkod.Tuple js => fold Integer.max (map (Integer.add 1) js) k
13.39 + KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k
13.40 | _ => k
13.41 - (* Kodkod.tuple_set -> int -> int *)
13.42 + (* KK.tuple_set -> int -> int *)
13.43 fun tuple_set_func ts k =
13.44 - Int.max (k, case ts of Kodkod.TupleAtomSeq (k', j0) => j0 + k' | _ => 0)
13.45 + Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k' | _ => 0)
13.46 val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
13.47 int_expr_func = K I}
13.48 val tuple_F = {tuple_func = tuple_func, tuple_set_func = tuple_set_func}
13.49 - val card = fold (Kodkod.fold_bound expr_F tuple_F) bounds 1
13.50 - |> Kodkod.fold_formula expr_F formula
13.51 + val card = fold (KK.fold_bound expr_F tuple_F) bounds 1
13.52 + |> KK.fold_formula expr_F formula
13.53 in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end
13.54
13.55 -(* int -> Kodkod.formula -> unit *)
13.56 +(* int -> KK.formula -> unit *)
13.57 fun check_bits bits formula =
13.58 let
13.59 - (* Kodkod.int_expr -> unit -> unit *)
13.60 - fun int_expr_func (Kodkod.Num k) () =
13.61 + (* KK.int_expr -> unit -> unit *)
13.62 + fun int_expr_func (KK.Num k) () =
13.63 if is_twos_complement_representable bits k then
13.64 ()
13.65 else
13.66 @@ -96,39 +98,38 @@
13.67 | int_expr_func _ () = ()
13.68 val expr_F = {formula_func = K I, rel_expr_func = K I,
13.69 int_expr_func = int_expr_func}
13.70 - in Kodkod.fold_formula expr_F formula () end
13.71 + in KK.fold_formula expr_F formula () end
13.72
13.73 (* int -> int -> unit *)
13.74 fun check_arity univ_card n =
13.75 - if n > Kodkod.max_arity univ_card then
13.76 + if n > KK.max_arity univ_card then
13.77 raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
13.78 "arity " ^ string_of_int n ^ " too large for universe of \
13.79 \cardinality " ^ string_of_int univ_card)
13.80 else
13.81 ()
13.82
13.83 -(* bool -> int -> int list -> Kodkod.tuple *)
13.84 +(* bool -> int -> int list -> KK.tuple *)
13.85 fun kk_tuple debug univ_card js =
13.86 if debug then
13.87 - Kodkod.Tuple js
13.88 + KK.Tuple js
13.89 else
13.90 - Kodkod.TupleIndex (length js,
13.91 - fold (fn j => fn accum => accum * univ_card + j) js 0)
13.92 + KK.TupleIndex (length js,
13.93 + fold (fn j => fn accum => accum * univ_card + j) js 0)
13.94
13.95 -(* (int * int) list -> Kodkod.tuple_set *)
13.96 -val tuple_set_from_atom_schema =
13.97 - foldl1 Kodkod.TupleProduct o map Kodkod.TupleAtomSeq
13.98 -(* rep -> Kodkod.tuple_set *)
13.99 +(* (int * int) list -> KK.tuple_set *)
13.100 +val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq
13.101 +(* rep -> KK.tuple_set *)
13.102 val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
13.103
13.104 -(* int -> Kodkod.tuple_set *)
13.105 -val single_atom = Kodkod.TupleSet o single o Kodkod.Tuple o single
13.106 -(* int -> Kodkod.int_bound list *)
13.107 +(* int -> KK.tuple_set *)
13.108 +val single_atom = KK.TupleSet o single o KK.Tuple o single
13.109 +(* int -> KK.int_bound list *)
13.110 fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
13.111 -(* int -> int -> Kodkod.int_bound list *)
13.112 +(* int -> int -> KK.int_bound list *)
13.113 fun pow_of_two_int_bounds bits j0 univ_card =
13.114 let
13.115 - (* int -> int -> int -> Kodkod.int_bound list *)
13.116 + (* int -> int -> int -> KK.int_bound list *)
13.117 fun aux 0 _ _ = []
13.118 | aux 1 pow_of_two j =
13.119 if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else []
13.120 @@ -137,11 +138,11 @@
13.121 aux (iter - 1) (2 * pow_of_two) (j + 1)
13.122 in aux (bits + 1) 1 j0 end
13.123
13.124 -(* Kodkod.formula -> Kodkod.n_ary_index list *)
13.125 +(* KK.formula -> KK.n_ary_index list *)
13.126 fun built_in_rels_in_formula formula =
13.127 let
13.128 - (* Kodkod.rel_expr -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list *)
13.129 - fun rel_expr_func (r as Kodkod.Rel (x as (n, j))) =
13.130 + (* KK.rel_expr -> KK.n_ary_index list -> KK.n_ary_index list *)
13.131 + fun rel_expr_func (r as KK.Rel (x as (n, j))) =
13.132 if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
13.133 I
13.134 else
13.135 @@ -151,7 +152,7 @@
13.136 | rel_expr_func _ = I
13.137 val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
13.138 int_expr_func = K I}
13.139 - in Kodkod.fold_formula expr_F formula [] end
13.140 + in KK.fold_formula expr_F formula [] end
13.141
13.142 val max_table_size = 65536
13.143
13.144 @@ -163,7 +164,7 @@
13.145 else
13.146 ()
13.147
13.148 -(* bool -> int -> int * int -> (int -> int) -> Kodkod.tuple list *)
13.149 +(* bool -> int -> int * int -> (int -> int) -> KK.tuple list *)
13.150 fun tabulate_func1 debug univ_card (k, j0) f =
13.151 (check_table_size k;
13.152 map_filter (fn j1 => let val j2 = f j1 in
13.153 @@ -172,7 +173,7 @@
13.154 else
13.155 NONE
13.156 end) (index_seq 0 k))
13.157 -(* bool -> int -> int * int -> int -> (int * int -> int) -> Kodkod.tuple list *)
13.158 +(* bool -> int -> int * int -> int -> (int * int -> int) -> KK.tuple list *)
13.159 fun tabulate_op2 debug univ_card (k, j0) res_j0 f =
13.160 (check_table_size (k * k);
13.161 map_filter (fn j => let
13.162 @@ -187,7 +188,7 @@
13.163 NONE
13.164 end) (index_seq 0 (k * k)))
13.165 (* bool -> int -> int * int -> int -> (int * int -> int * int)
13.166 - -> Kodkod.tuple list *)
13.167 + -> KK.tuple list *)
13.168 fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f =
13.169 (check_table_size (k * k);
13.170 map_filter (fn j => let
13.171 @@ -202,13 +203,13 @@
13.172 else
13.173 NONE
13.174 end) (index_seq 0 (k * k)))
13.175 -(* bool -> int -> int * int -> (int * int -> int) -> Kodkod.tuple list *)
13.176 +(* bool -> int -> int * int -> (int * int -> int) -> KK.tuple list *)
13.177 fun tabulate_nat_op2 debug univ_card (k, j0) f =
13.178 tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f)
13.179 fun tabulate_int_op2 debug univ_card (k, j0) f =
13.180 tabulate_op2 debug univ_card (k, j0) j0
13.181 (atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0)))
13.182 -(* bool -> int -> int * int -> (int * int -> int * int) -> Kodkod.tuple list *)
13.183 +(* bool -> int -> int * int -> (int * int -> int * int) -> KK.tuple list *)
13.184 fun tabulate_int_op2_2 debug univ_card (k, j0) f =
13.185 tabulate_op2_2 debug univ_card (k, j0) j0
13.186 (pairself (atom_for_int (k, 0)) o f
13.187 @@ -228,7 +229,7 @@
13.188 else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end
13.189
13.190 (* bool -> int -> int -> int -> int -> int * int
13.191 - -> string * bool * Kodkod.tuple list *)
13.192 + -> string * bool * KK.tuple list *)
13.193 fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) =
13.194 (check_arity univ_card n;
13.195 if x = not3_rel then
13.196 @@ -269,15 +270,14 @@
13.197 else
13.198 raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
13.199
13.200 -(* bool -> int -> int -> int -> int -> int * int -> Kodkod.rel_expr
13.201 - -> Kodkod.bound *)
13.202 +(* bool -> int -> int -> int -> int -> int * int -> KK.rel_expr -> KK.bound *)
13.203 fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x =
13.204 let
13.205 val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card
13.206 j0 x
13.207 - in ([(x, nick)], [Kodkod.TupleSet ts]) end
13.208 + in ([(x, nick)], [KK.TupleSet ts]) end
13.209
13.210 -(* bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list *)
13.211 +(* bool -> int -> int -> int -> int -> KK.formula -> KK.bound list *)
13.212 fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 =
13.213 map (bound_for_built_in_rel debug univ_card nat_card int_card j0)
13.214 o built_in_rels_in_formula
13.215 @@ -288,7 +288,7 @@
13.216 (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
13.217 else "") ^ " : " ^ string_for_rep R
13.218
13.219 -(* Proof.context -> bool -> nut -> Kodkod.bound *)
13.220 +(* Proof.context -> bool -> nut -> KK.bound *)
13.221 fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
13.222 ([(x, bound_comment ctxt debug nick T R)],
13.223 if nick = @{const_name bisim_iterator_max} then
13.224 @@ -296,11 +296,11 @@
13.225 Atom (k, j0) => [single_atom (k - 1 + j0)]
13.226 | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
13.227 else
13.228 - [Kodkod.TupleSet [], upper_bound_for_rep R])
13.229 + [KK.TupleSet [], upper_bound_for_rep R])
13.230 | bound_for_plain_rel _ _ u =
13.231 raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
13.232
13.233 -(* Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound *)
13.234 +(* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *)
13.235 fun bound_for_sel_rel ctxt debug dtypes
13.236 (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),
13.237 nick)) =
13.238 @@ -310,26 +310,24 @@
13.239 in
13.240 ([(x, bound_comment ctxt debug nick T R)],
13.241 if explicit_max = 0 then
13.242 - [Kodkod.TupleSet []]
13.243 + [KK.TupleSet []]
13.244 else
13.245 - let val ts = Kodkod.TupleAtomSeq (epsilon - delta, delta + j0) in
13.246 + let val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) in
13.247 if R2 = Formula Neut then
13.248 - [ts] |> not exclusive ? cons (Kodkod.TupleSet [])
13.249 + [ts] |> not exclusive ? cons (KK.TupleSet [])
13.250 else
13.251 - [Kodkod.TupleSet [],
13.252 - Kodkod.TupleProduct (ts, upper_bound_for_rep R2)]
13.253 + [KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)]
13.254 end)
13.255 end
13.256 | bound_for_sel_rel _ _ _ u =
13.257 raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
13.258
13.259 -(* Kodkod.bound list -> Kodkod.bound list *)
13.260 +(* KK.bound list -> KK.bound list *)
13.261 fun merge_bounds bs =
13.262 let
13.263 - (* Kodkod.bound -> int *)
13.264 + (* KK.bound -> int *)
13.265 fun arity (zs, _) = fst (fst (hd zs))
13.266 - (* Kodkod.bound list -> Kodkod.bound -> Kodkod.bound list
13.267 - -> Kodkod.bound list *)
13.268 + (* KK.bound list -> KK.bound -> KK.bound list -> KK.bound list *)
13.269 fun add_bound ds b [] = List.revAppend (ds, [b])
13.270 | add_bound ds b (c :: cs) =
13.271 if arity b = arity c andalso snd b = snd c then
13.272 @@ -338,40 +336,40 @@
13.273 add_bound (c :: ds) b cs
13.274 in fold (add_bound []) bs [] end
13.275
13.276 -(* int -> int -> Kodkod.rel_expr list *)
13.277 -fun unary_var_seq j0 n = map (curry Kodkod.Var 1) (index_seq j0 n)
13.278 +(* int -> int -> KK.rel_expr list *)
13.279 +fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n)
13.280
13.281 -(* int list -> Kodkod.rel_expr *)
13.282 -val singleton_from_combination = foldl1 Kodkod.Product o map Kodkod.Atom
13.283 -(* rep -> Kodkod.rel_expr list *)
13.284 +(* int list -> KK.rel_expr *)
13.285 +val singleton_from_combination = foldl1 KK.Product o map KK.Atom
13.286 +(* rep -> KK.rel_expr list *)
13.287 fun all_singletons_for_rep R =
13.288 if is_lone_rep R then
13.289 all_combinations_for_rep R |> map singleton_from_combination
13.290 else
13.291 raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R])
13.292
13.293 -(* Kodkod.rel_expr -> Kodkod.rel_expr list *)
13.294 -fun unpack_products (Kodkod.Product (r1, r2)) =
13.295 +(* KK.rel_expr -> KK.rel_expr list *)
13.296 +fun unpack_products (KK.Product (r1, r2)) =
13.297 unpack_products r1 @ unpack_products r2
13.298 | unpack_products r = [r]
13.299 -fun unpack_joins (Kodkod.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2
13.300 +fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2
13.301 | unpack_joins r = [r]
13.302
13.303 -(* rep -> Kodkod.rel_expr *)
13.304 +(* rep -> KK.rel_expr *)
13.305 val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
13.306 fun full_rel_for_rep R =
13.307 case atom_schema_of_rep R of
13.308 [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
13.309 - | schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema)
13.310 + | schema => foldl1 KK.Product (map KK.AtomSeq schema)
13.311
13.312 -(* int -> int list -> Kodkod.decl list *)
13.313 +(* int -> int list -> KK.decl list *)
13.314 fun decls_for_atom_schema j0 schema =
13.315 - map2 (fn j => fn x => Kodkod.DeclOne ((1, j), Kodkod.AtomSeq x))
13.316 + map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x))
13.317 (index_seq j0 (length schema)) schema
13.318
13.319 (* The type constraint below is a workaround for a Poly/ML bug. *)
13.320
13.321 -(* kodkod_constrs -> rep -> Kodkod.rel_expr -> Kodkod.formula *)
13.322 +(* kodkod_constrs -> rep -> KK.rel_expr -> KK.formula *)
13.323 fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
13.324 R r =
13.325 let val body_R = body_rep R in
13.326 @@ -380,13 +378,13 @@
13.327 val binder_schema = atom_schema_of_reps (binder_reps R)
13.328 val body_schema = atom_schema_of_rep body_R
13.329 val one = is_one_rep body_R
13.330 - val opt_x = case r of Kodkod.Rel x => SOME x | _ => NONE
13.331 + val opt_x = case r of KK.Rel x => SOME x | _ => NONE
13.332 in
13.333 if opt_x <> NONE andalso length binder_schema = 1
13.334 andalso length body_schema = 1 then
13.335 - (if one then Kodkod.Function else Kodkod.Functional)
13.336 - (the opt_x, Kodkod.AtomSeq (hd binder_schema),
13.337 - Kodkod.AtomSeq (hd body_schema))
13.338 + (if one then KK.Function else KK.Functional)
13.339 + (the opt_x, KK.AtomSeq (hd binder_schema),
13.340 + KK.AtomSeq (hd body_schema))
13.341 else
13.342 let
13.343 val decls = decls_for_atom_schema ~1 binder_schema
13.344 @@ -395,12 +393,12 @@
13.345 in kk_all decls (kk_xone (fold kk_join vars r)) end
13.346 end
13.347 else
13.348 - Kodkod.True
13.349 + KK.True
13.350 end
13.351 -fun kk_n_ary_function kk R (r as Kodkod.Rel x) =
13.352 +fun kk_n_ary_function kk R (r as KK.Rel x) =
13.353 if not (is_opt_rep R) then
13.354 if x = suc_rel then
13.355 - Kodkod.False
13.356 + KK.False
13.357 else if x = nat_add_rel then
13.358 formula_for_bool (card_of_rep (body_rep R) = 1)
13.359 else if x = nat_multiply_rel then
13.360 @@ -408,58 +406,56 @@
13.361 else
13.362 d_n_ary_function kk R r
13.363 else if x = nat_subtract_rel then
13.364 - Kodkod.True
13.365 + KK.True
13.366 else
13.367 d_n_ary_function kk R r
13.368 | kk_n_ary_function kk R r = d_n_ary_function kk R r
13.369
13.370 -(* kodkod_constrs -> Kodkod.rel_expr list -> Kodkod.formula *)
13.371 -fun kk_disjoint_sets _ [] = Kodkod.True
13.372 +(* kodkod_constrs -> KK.rel_expr list -> KK.formula *)
13.373 +fun kk_disjoint_sets _ [] = KK.True
13.374 | kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs)
13.375 (r :: rs) =
13.376 fold (kk_and o kk_no o kk_intersect r) rs (kk_disjoint_sets kk rs)
13.377
13.378 -(* int -> kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr)
13.379 - -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.380 +(* int -> kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr
13.381 + -> KK.rel_expr *)
13.382 fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
13.383 if inline_rel_expr r then
13.384 f r
13.385 else
13.386 - let val x = (Kodkod.arity_of_rel_expr r, j) in
13.387 - kk_rel_let [Kodkod.AssignRelReg (x, r)] (f (Kodkod.RelReg x))
13.388 + let val x = (KK.arity_of_rel_expr r, j) in
13.389 + kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x))
13.390 end
13.391 -(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr) -> Kodkod.rel_expr
13.392 - -> Kodkod.rel_expr *)
13.393 +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr
13.394 + -> KK.rel_expr *)
13.395 val single_rel_rel_let = basic_rel_rel_let 0
13.396 -(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
13.397 - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.398 +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr) -> KK.rel_expr
13.399 + -> KK.rel_expr -> KK.rel_expr *)
13.400 fun double_rel_rel_let kk f r1 r2 =
13.401 single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
13.402 -(* kodkod_constrs
13.403 - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
13.404 - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr
13.405 - -> Kodkod.rel_expr *)
13.406 +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr)
13.407 + -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
13.408 fun tripl_rel_rel_let kk f r1 r2 r3 =
13.409 double_rel_rel_let kk
13.410 (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
13.411
13.412 -(* kodkod_constrs -> int -> Kodkod.formula -> Kodkod.rel_expr *)
13.413 +(* kodkod_constrs -> int -> KK.formula -> KK.rel_expr *)
13.414 fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
13.415 - kk_rel_if f (Kodkod.Atom (j0 + 1)) (Kodkod.Atom j0)
13.416 -(* kodkod_constrs -> rep -> Kodkod.formula -> Kodkod.rel_expr *)
13.417 + kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0)
13.418 +(* kodkod_constrs -> rep -> KK.formula -> KK.rel_expr *)
13.419 fun rel_expr_from_formula kk R f =
13.420 case unopt_rep R of
13.421 Atom (2, j0) => atom_from_formula kk j0 f
13.422 | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R])
13.423
13.424 -(* kodkod_cotrs -> int -> int -> Kodkod.rel_expr -> Kodkod.rel_expr list *)
13.425 +(* kodkod_cotrs -> int -> int -> KK.rel_expr -> KK.rel_expr list *)
13.426 fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity
13.427 num_chunks r =
13.428 List.tabulate (num_chunks, fn j => kk_project_seq r (j * chunk_arity)
13.429 chunk_arity)
13.430
13.431 -(* kodkod_constrs -> bool -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr
13.432 - -> Kodkod.rel_expr *)
13.433 +(* kodkod_constrs -> bool -> rep -> rep -> KK.rel_expr -> KK.rel_expr
13.434 + -> KK.rel_expr *)
13.435 fun kk_n_fold_join
13.436 (kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1
13.437 res_R r1 r2 =
13.438 @@ -479,8 +475,8 @@
13.439 arity1 (arity_of_rep res_R)
13.440 end
13.441
13.442 -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr list
13.443 - -> Kodkod.rel_expr list -> Kodkod.rel_expr *)
13.444 +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr list
13.445 + -> KK.rel_expr list -> KK.rel_expr *)
13.446 fun kk_case_switch (kk as {kk_union, kk_product, ...}) R1 R2 r rs1 rs2 =
13.447 if rs1 = rs2 then r
13.448 else kk_n_fold_join kk true R1 R2 r (fold1 kk_union (map2 kk_product rs1 rs2))
13.449 @@ -488,7 +484,7 @@
13.450 val lone_rep_fallback_max_card = 4096
13.451 val some_j0 = 0
13.452
13.453 -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.454 +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
13.455 fun lone_rep_fallback kk new_R old_R r =
13.456 if old_R = new_R then
13.457 r
13.458 @@ -505,7 +501,7 @@
13.459 else
13.460 raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
13.461 end
13.462 -(* kodkod_constrs -> int * int -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.463 +(* kodkod_constrs -> int * int -> rep -> KK.rel_expr -> KK.rel_expr *)
13.464 and atom_from_rel_expr kk (x as (k, j0)) old_R r =
13.465 case old_R of
13.466 Func (R1, R2) =>
13.467 @@ -518,7 +514,7 @@
13.468 end
13.469 | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R])
13.470 | _ => lone_rep_fallback kk (Atom x) old_R r
13.471 -(* kodkod_constrs -> rep list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.472 +(* kodkod_constrs -> rep list -> rep -> KK.rel_expr -> KK.rel_expr *)
13.473 and struct_from_rel_expr kk Rs old_R r =
13.474 case old_R of
13.475 Atom _ => lone_rep_fallback kk (Struct Rs) old_R r
13.476 @@ -542,7 +538,7 @@
13.477 lone_rep_fallback kk (Struct Rs) old_R r
13.478 end
13.479 | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
13.480 -(* kodkod_constrs -> int -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.481 +(* kodkod_constrs -> int -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
13.482 and vect_from_rel_expr kk k R old_R r =
13.483 case old_R of
13.484 Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r
13.485 @@ -565,7 +561,7 @@
13.486 (kk_n_fold_join kk true R1 R2 arg_r r))
13.487 (all_singletons_for_rep R1))
13.488 | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
13.489 -(* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.490 +(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
13.491 and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r =
13.492 let
13.493 val dom_card = card_of_rep R1
13.494 @@ -594,9 +590,9 @@
13.495 let
13.496 val args_rs = all_singletons_for_rep R1
13.497 val vals_rs = unpack_vect_in_chunks kk 1 k r
13.498 - (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.499 + (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
13.500 fun empty_or_singleton_set_for arg_r val_r =
13.501 - #kk_join kk val_r (#kk_product kk (Kodkod.Atom (j0 + 1)) arg_r)
13.502 + #kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r)
13.503 in
13.504 fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs)
13.505 end
13.506 @@ -613,11 +609,11 @@
13.507 #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)
13.508 end
13.509 | Func (Unit, (Atom (2, j0))) =>
13.510 - #kk_rel_if kk (#kk_rel_eq kk r (Kodkod.Atom (j0 + 1)))
13.511 + #kk_rel_if kk (#kk_rel_eq kk r (KK.Atom (j0 + 1)))
13.512 (full_rel_for_rep R1) (empty_rel_for_rep R1)
13.513 | Func (R1', Atom (2, j0)) =>
13.514 func_from_no_opt_rel_expr kk R1 (Formula Neut)
13.515 - (Func (R1', Formula Neut)) (#kk_join kk r (Kodkod.Atom (j0 + 1)))
13.516 + (Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1)))
13.517 | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
13.518 [old_R, Func (R1, Formula Neut)]))
13.519 | func_from_no_opt_rel_expr kk R1 R2 old_R r =
13.520 @@ -633,14 +629,14 @@
13.521 Atom (x as (2, j0)) =>
13.522 let val schema = atom_schema_of_rep R1 in
13.523 if length schema = 1 then
13.524 - #kk_override kk (#kk_product kk (Kodkod.AtomSeq (hd schema))
13.525 - (Kodkod.Atom j0))
13.526 - (#kk_product kk r (Kodkod.Atom (j0 + 1)))
13.527 + #kk_override kk (#kk_product kk (KK.AtomSeq (hd schema))
13.528 + (KK.Atom j0))
13.529 + (#kk_product kk r (KK.Atom (j0 + 1)))
13.530 else
13.531 let
13.532 val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema))
13.533 |> rel_expr_from_rel_expr kk R1' R1
13.534 - val r2 = Kodkod.Var (1, ~(length schema) - 1)
13.535 + val r2 = KK.Var (1, ~(length schema) - 1)
13.536 val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r)
13.537 in
13.538 #kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x]))
13.539 @@ -652,7 +648,7 @@
13.540 | Func (Unit, R2') =>
13.541 let val j0 = some_j0 in
13.542 func_from_no_opt_rel_expr kk R1 R2 (Func (Atom (1, j0), R2'))
13.543 - (#kk_product kk (Kodkod.Atom j0) r)
13.544 + (#kk_product kk (KK.Atom j0) r)
13.545 end
13.546 | Func (R1', R2') =>
13.547 if R1 = R1' andalso R2 = R2' then
13.548 @@ -677,7 +673,7 @@
13.549 end
13.550 | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
13.551 [old_R, Func (R1, R2)])
13.552 -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.553 +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
13.554 and rel_expr_from_rel_expr kk new_R old_R r =
13.555 let
13.556 val unopt_old_R = unopt_rep old_R
13.557 @@ -697,43 +693,43 @@
13.558 [old_R, new_R]))
13.559 unopt_old_R r
13.560 end
13.561 -(* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.562 +(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
13.563 and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2))
13.564
13.565 -(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.566 +(* kodkod_constrs -> typ -> KK.rel_expr -> KK.rel_expr *)
13.567 fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r =
13.568 - kk_join r (Kodkod.Rel (if T = @{typ "unsigned_bit word"} then
13.569 - unsigned_bit_word_sel_rel
13.570 - else
13.571 - signed_bit_word_sel_rel))
13.572 -(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.int_expr *)
13.573 -val int_expr_from_atom = Kodkod.SetSum ooo bit_set_from_atom
13.574 -(* kodkod_constrs -> typ -> rep -> Kodkod.int_expr -> Kodkod.rel_expr *)
13.575 + kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then
13.576 + unsigned_bit_word_sel_rel
13.577 + else
13.578 + signed_bit_word_sel_rel))
13.579 +(* kodkod_constrs -> typ -> KK.rel_expr -> KK.int_expr *)
13.580 +val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom
13.581 +(* kodkod_constrs -> typ -> rep -> KK.int_expr -> KK.rel_expr *)
13.582 fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
13.583 : kodkod_constrs) T R i =
13.584 kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
13.585 - (kk_rel_eq (bit_set_from_atom kk T (Kodkod.Var (1, ~1)))
13.586 - (Kodkod.Bits i))
13.587 + (kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1)))
13.588 + (KK.Bits i))
13.589
13.590 -(* kodkod_constrs -> nut -> Kodkod.formula *)
13.591 +(* kodkod_constrs -> nut -> KK.formula *)
13.592 fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
13.593 kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
13.594 - (Kodkod.Rel x)
13.595 + (KK.Rel x)
13.596 | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs)
13.597 (FreeRel (x, _, R, _)) =
13.598 - if is_one_rep R then kk_one (Kodkod.Rel x)
13.599 - else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (Kodkod.Rel x)
13.600 - else Kodkod.True
13.601 + if is_one_rep R then kk_one (KK.Rel x)
13.602 + else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x)
13.603 + else KK.True
13.604 | declarative_axiom_for_plain_rel _ u =
13.605 raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
13.606
13.607 -(* nut NameTable.table -> styp -> Kodkod.rel_expr * rep * int *)
13.608 +(* nut NameTable.table -> styp -> KK.rel_expr * rep * int *)
13.609 fun const_triple rel_table (x as (s, T)) =
13.610 case the_name rel_table (ConstName (s, T, Any)) of
13.611 - FreeRel ((n, j), _, R, _) => (Kodkod.Rel (n, j), R, n)
13.612 + FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)
13.613 | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
13.614
13.615 -(* nut NameTable.table -> styp -> Kodkod.rel_expr *)
13.616 +(* nut NameTable.table -> styp -> KK.rel_expr *)
13.617 fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
13.618
13.619 (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
13.620 @@ -747,7 +743,7 @@
13.621 in
13.622 map_filter (fn (j, T) =>
13.623 if forall (not_equal T o #typ) dtypes then NONE
13.624 - else SOME (kk_project r (map Kodkod.Num [0, j]), T))
13.625 + else SOME (kk_project r (map KK.Num [0, j]), T))
13.626 (index_seq 1 (arity - 1) ~~ tl type_schema)
13.627 end
13.628 (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
13.629 @@ -763,28 +759,28 @@
13.630 SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
13.631 o #const) constrs)
13.632
13.633 -val empty_rel = Kodkod.Product (Kodkod.None, Kodkod.None)
13.634 +val empty_rel = KK.Product (KK.None, KK.None)
13.635
13.636 -(* nfa_table -> typ -> typ -> Kodkod.rel_expr list *)
13.637 +(* nfa_table -> typ -> typ -> KK.rel_expr list *)
13.638 fun direct_path_rel_exprs nfa start final =
13.639 case AList.lookup (op =) nfa final of
13.640 SOME trans => map fst (filter (curry (op =) start o snd) trans)
13.641 | NONE => []
13.642 -(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> Kodkod.rel_expr *)
13.643 +(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *)
13.644 and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final =
13.645 fold kk_union (direct_path_rel_exprs nfa start final)
13.646 - (if start = final then Kodkod.Iden else empty_rel)
13.647 + (if start = final then KK.Iden else empty_rel)
13.648 | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final =
13.649 kk_union (any_path_rel_expr kk nfa qs start final)
13.650 (knot_path_rel_expr kk nfa qs start q final)
13.651 (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ
13.652 - -> Kodkod.rel_expr *)
13.653 + -> KK.rel_expr *)
13.654 and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start
13.655 knot final =
13.656 kk_join (kk_join (any_path_rel_expr kk nfa qs knot final)
13.657 (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot)))
13.658 (any_path_rel_expr kk nfa qs start knot)
13.659 -(* kodkod_constrs -> nfa_table -> typ list -> typ -> Kodkod.rel_expr *)
13.660 +(* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *)
13.661 and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start =
13.662 fold kk_union (direct_path_rel_exprs nfa start start) empty_rel
13.663 | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start =
13.664 @@ -812,12 +808,12 @@
13.665 nfa |> graph_for_nfa |> NfaGraph.strong_conn
13.666 |> map (fn keys => filter (member (op =) keys o fst) nfa)
13.667
13.668 -(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> Kodkod.formula *)
13.669 +(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *)
13.670 fun acyclicity_axiom_for_datatype dtypes kk nfa start =
13.671 #kk_no kk (#kk_intersect kk
13.672 - (loop_path_rel_expr kk nfa (map fst nfa) start) Kodkod.Iden)
13.673 + (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
13.674 (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
13.675 - -> Kodkod.formula list *)
13.676 + -> KK.formula list *)
13.677 fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes =
13.678 map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes
13.679 |> strongly_connected_sub_nfas
13.680 @@ -825,7 +821,7 @@
13.681 nfa)
13.682
13.683 (* extended_context -> int -> kodkod_constrs -> nut NameTable.table
13.684 - -> Kodkod.rel_expr -> constr_spec -> int -> Kodkod.formula *)
13.685 + -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
13.686 fun sel_axiom_for_sel ext_ctxt j0
13.687 (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
13.688 kk_join, ...}) rel_table dom_r
13.689 @@ -840,15 +836,14 @@
13.690 if exclusive then
13.691 kk_n_ary_function kk (Func (Atom z, R2)) r
13.692 else
13.693 - let val r' = kk_join (Kodkod.Var (1, 0)) r in
13.694 - kk_all [Kodkod.DeclOne ((1, 0), Kodkod.AtomSeq z)]
13.695 - (kk_formula_if (kk_subset (Kodkod.Var (1, 0)) dom_r)
13.696 - (kk_n_ary_function kk R2 r')
13.697 - (kk_no r'))
13.698 + let val r' = kk_join (KK.Var (1, 0)) r in
13.699 + kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
13.700 + (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
13.701 + (kk_n_ary_function kk R2 r') (kk_no r'))
13.702 end
13.703 end
13.704 (* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
13.705 - -> constr_spec -> Kodkod.formula list *)
13.706 + -> constr_spec -> KK.formula list *)
13.707 fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
13.708 (constr as {const, delta, epsilon, explicit_max, ...}) =
13.709 let
13.710 @@ -862,9 +857,9 @@
13.711 val ran_r = discr_rel_expr rel_table const
13.712 val max_axiom =
13.713 if honors_explicit_max then
13.714 - Kodkod.True
13.715 + KK.True
13.716 else if is_twos_complement_representable bits (epsilon - delta) then
13.717 - Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max)
13.718 + KK.LE (KK.Cardinality ran_r, KK.Num explicit_max)
13.719 else
13.720 raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
13.721 "\"bits\" value " ^ string_of_int bits ^
13.722 @@ -876,21 +871,20 @@
13.723 end
13.724 end
13.725 (* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
13.726 - -> dtype_spec -> Kodkod.formula list *)
13.727 + -> dtype_spec -> KK.formula list *)
13.728 fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
13.729 ({constrs, ...} : dtype_spec) =
13.730 maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
13.731
13.732 (* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
13.733 - -> Kodkod.formula list *)
13.734 + -> KK.formula list *)
13.735 fun uniqueness_axiom_for_constr ext_ctxt
13.736 ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
13.737 : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
13.738 let
13.739 - (* Kodkod.rel_expr -> Kodkod.formula *)
13.740 + (* KK.rel_expr -> KK.formula *)
13.741 fun conjunct_for_sel r =
13.742 - kk_rel_eq (kk_join (Kodkod.Var (1, 0)) r)
13.743 - (kk_join (Kodkod.Var (1, 1)) r)
13.744 + kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
13.745 val num_sels = num_sels_for_constr_type (snd const)
13.746 val triples = map (const_triple rel_table
13.747 o boxed_nth_sel_for_constr ext_ctxt const)
13.748 @@ -904,13 +898,13 @@
13.749 if num_sels = 0 then
13.750 kk_lone set_r
13.751 else
13.752 - kk_all (map (Kodkod.DeclOne o rpair set_r o pair 1) [0, 1])
13.753 + kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
13.754 (kk_implies
13.755 (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
13.756 - (kk_rel_eq (Kodkod.Var (1, 0)) (Kodkod.Var (1, 1))))
13.757 + (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
13.758 end
13.759 (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
13.760 - -> Kodkod.formula list *)
13.761 + -> KK.formula list *)
13.762 fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table
13.763 ({constrs, ...} : dtype_spec) =
13.764 map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs
13.765 @@ -918,7 +912,7 @@
13.766 (* constr_spec -> int *)
13.767 fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
13.768 (* int -> kodkod_constrs -> nut NameTable.table -> dtype_spec
13.769 - -> Kodkod.formula list *)
13.770 + -> KK.formula list *)
13.771 fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
13.772 rel_table
13.773 ({card, constrs, ...} : dtype_spec) =
13.774 @@ -926,12 +920,12 @@
13.775 [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
13.776 else
13.777 let val rs = map (discr_rel_expr rel_table o #const) constrs in
13.778 - [kk_rel_eq (fold1 kk_union rs) (Kodkod.AtomSeq (card, j0)),
13.779 + [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
13.780 kk_disjoint_sets kk rs]
13.781 end
13.782
13.783 (* extended_context -> int -> int Typtab.table -> kodkod_constrs
13.784 - -> nut NameTable.table -> dtype_spec -> Kodkod.formula list *)
13.785 + -> nut NameTable.table -> dtype_spec -> KK.formula list *)
13.786 fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = []
13.787 | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
13.788 (dtype as {typ, ...}) =
13.789 @@ -942,12 +936,12 @@
13.790 end
13.791
13.792 (* extended_context -> int -> int Typtab.table -> kodkod_constrs
13.793 - -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list *)
13.794 + -> nut NameTable.table -> dtype_spec list -> KK.formula list *)
13.795 fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
13.796 acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
13.797 maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
13.798
13.799 -(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *)
13.800 +(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
13.801 fun kodkod_formula_from_nut bits ofs liberal
13.802 (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
13.803 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
13.804 @@ -959,20 +953,20 @@
13.805 val main_j0 = offset_of_type ofs bool_T
13.806 val bool_j0 = main_j0
13.807 val bool_atom_R = Atom (2, main_j0)
13.808 - val false_atom = Kodkod.Atom bool_j0
13.809 - val true_atom = Kodkod.Atom (bool_j0 + 1)
13.810 + val false_atom = KK.Atom bool_j0
13.811 + val true_atom = KK.Atom (bool_j0 + 1)
13.812
13.813 - (* polarity -> int -> Kodkod.rel_expr -> Kodkod.formula *)
13.814 + (* polarity -> int -> KK.rel_expr -> KK.formula *)
13.815 fun formula_from_opt_atom polar j0 r =
13.816 case polar of
13.817 - Neg => kk_not (kk_rel_eq r (Kodkod.Atom j0))
13.818 - | _ => kk_rel_eq r (Kodkod.Atom (j0 + 1))
13.819 - (* int -> Kodkod.rel_expr -> Kodkod.formula *)
13.820 + Neg => kk_not (kk_rel_eq r (KK.Atom j0))
13.821 + | _ => kk_rel_eq r (KK.Atom (j0 + 1))
13.822 + (* int -> KK.rel_expr -> KK.formula *)
13.823 val formula_from_atom = formula_from_opt_atom Pos
13.824
13.825 - (* Kodkod.formula -> Kodkod.formula -> Kodkod.formula *)
13.826 + (* KK.formula -> KK.formula -> KK.formula *)
13.827 fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2)
13.828 - (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.829 + (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
13.830 val kk_or3 =
13.831 double_rel_rel_let kk
13.832 (fn r1 => fn r2 =>
13.833 @@ -985,27 +979,27 @@
13.834 (kk_intersect r1 r2))
13.835 fun kk_notimplies3 r1 r2 = kk_and3 r1 (kk_not3 r2)
13.836
13.837 - (* int -> Kodkod.rel_expr -> Kodkod.formula list *)
13.838 + (* int -> KK.rel_expr -> KK.formula list *)
13.839 val unpack_formulas =
13.840 map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1
13.841 - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) -> int
13.842 - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.843 + (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr
13.844 + -> KK.rel_expr -> KK.rel_expr *)
13.845 fun kk_vect_set_op connective k r1 r2 =
13.846 fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective)
13.847 (unpack_formulas k r1) (unpack_formulas k r2))
13.848 - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) -> int
13.849 - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula *)
13.850 + (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr
13.851 + -> KK.rel_expr -> KK.formula *)
13.852 fun kk_vect_set_bool_op connective k r1 r2 =
13.853 fold1 kk_and (map2 connective (unpack_formulas k r1)
13.854 (unpack_formulas k r2))
13.855
13.856 - (* nut -> Kodkod.formula *)
13.857 + (* nut -> KK.formula *)
13.858 fun to_f u =
13.859 case rep_of u of
13.860 Formula polar =>
13.861 (case u of
13.862 - Cst (False, _, _) => Kodkod.False
13.863 - | Cst (True, _, _) => Kodkod.True
13.864 + Cst (False, _, _) => KK.False
13.865 + | Cst (True, _, _) => KK.True
13.866 | Op1 (Not, _, _, u1) =>
13.867 kk_not (to_f_with_polarity (flip_polarity polar) u1)
13.868 | Op1 (Finite, _, _, u1) =>
13.869 @@ -1014,9 +1008,9 @@
13.870 Neut => if opt1 then
13.871 raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
13.872 else
13.873 - Kodkod.True
13.874 + KK.True
13.875 | Pos => formula_for_bool (not opt1)
13.876 - | Neg => Kodkod.True
13.877 + | Neg => KK.True
13.878 end
13.879 | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1
13.880 | Op2 (All, _, _, u1, u2) =>
13.881 @@ -1052,7 +1046,7 @@
13.882 else
13.883 let
13.884 (* FIXME: merge with similar code below *)
13.885 - (* bool -> nut -> Kodkod.rel_expr *)
13.886 + (* bool -> nut -> KK.rel_expr *)
13.887 fun set_to_r widen u =
13.888 if widen then
13.889 kk_difference (full_rel_for_rep dom_R)
13.890 @@ -1065,7 +1059,7 @@
13.891 end
13.892 | Op2 (DefEq, _, _, u1, u2) =>
13.893 (case min_rep (rep_of u1) (rep_of u2) of
13.894 - Unit => Kodkod.True
13.895 + Unit => KK.True
13.896 | Formula polar =>
13.897 kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
13.898 | min_R =>
13.899 @@ -1085,7 +1079,7 @@
13.900 end)
13.901 | Op2 (Eq, T, R, u1, u2) =>
13.902 (case min_rep (rep_of u1) (rep_of u2) of
13.903 - Unit => Kodkod.True
13.904 + Unit => KK.True
13.905 | Formula polar =>
13.906 kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
13.907 | min_R =>
13.908 @@ -1114,7 +1108,7 @@
13.909 else
13.910 if is_lone_rep min_R then
13.911 if arity_of_rep min_R = 1 then
13.912 - kk_subset (kk_product r1 r2) Kodkod.Iden
13.913 + kk_subset (kk_product r1 r2) KK.Iden
13.914 else if not both_opt then
13.915 (r1, r2) |> is_opt_rep (rep_of u2) ? swap
13.916 |-> kk_subset
13.917 @@ -1139,8 +1133,8 @@
13.918 val rs2 = unpack_products r2
13.919 in
13.920 if length rs1 = length rs2
13.921 - andalso map Kodkod.arity_of_rel_expr rs1
13.922 - = map Kodkod.arity_of_rel_expr rs2 then
13.923 + andalso map KK.arity_of_rel_expr rs1
13.924 + = map KK.arity_of_rel_expr rs2 then
13.925 fold1 kk_and (map2 kk_subset rs1 rs2)
13.926 else
13.927 kk_subset r1 r2
13.928 @@ -1165,26 +1159,25 @@
13.929 | Op3 (If, _, _, u1, u2, u3) =>
13.930 kk_formula_if (to_f u1) (to_f_with_polarity polar u2)
13.931 (to_f_with_polarity polar u3)
13.932 - | FormulaReg (j, _, _) => Kodkod.FormulaReg j
13.933 + | FormulaReg (j, _, _) => KK.FormulaReg j
13.934 | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
13.935 | Atom (2, j0) => formula_from_atom j0 (to_r u)
13.936 | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])
13.937 - (* polarity -> nut -> Kodkod.formula *)
13.938 + (* polarity -> nut -> KK.formula *)
13.939 and to_f_with_polarity polar u =
13.940 case rep_of u of
13.941 Formula _ => to_f u
13.942 | Atom (2, j0) => formula_from_atom j0 (to_r u)
13.943 | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u)
13.944 | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u])
13.945 - (* nut -> Kodkod.rel_expr *)
13.946 + (* nut -> KK.rel_expr *)
13.947 and to_r u =
13.948 case u of
13.949 Cst (False, _, Atom _) => false_atom
13.950 | Cst (True, _, Atom _) => true_atom
13.951 | Cst (Iden, T, Func (Struct [R1, R2], Formula Neut)) =>
13.952 if R1 = R2 andalso arity_of_rep R1 = 1 then
13.953 - kk_intersect Kodkod.Iden (kk_product (full_rel_for_rep R1)
13.954 - Kodkod.Univ)
13.955 + kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ)
13.956 else
13.957 let
13.958 val schema1 = atom_schema_of_rep R1
13.959 @@ -1200,106 +1193,100 @@
13.960 (kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1)
13.961 (rel_expr_from_rel_expr kk min_R R2 r2))
13.962 end
13.963 - | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => Kodkod.Atom j0
13.964 + | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
13.965 | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
13.966 to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
13.967 | Cst (Num j, T, R) =>
13.968 if is_word_type T then
13.969 - atom_from_int_expr kk T R (Kodkod.Num j)
13.970 + atom_from_int_expr kk T R (KK.Num j)
13.971 else if T = int_T then
13.972 case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
13.973 - ~1 => if is_opt_rep R then Kodkod.None
13.974 + ~1 => if is_opt_rep R then KK.None
13.975 else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
13.976 - | j' => Kodkod.Atom j'
13.977 + | j' => KK.Atom j'
13.978 else
13.979 - if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
13.980 - else if is_opt_rep R then Kodkod.None
13.981 + if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T)
13.982 + else if is_opt_rep R then KK.None
13.983 else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
13.984 | Cst (Unknown, _, R) => empty_rel_for_rep R
13.985 | Cst (Unrep, _, R) => empty_rel_for_rep R
13.986 - | Cst (Suc, T, Func (Atom x, _)) =>
13.987 - if domain_type T <> nat_T then
13.988 - Kodkod.Rel suc_rel
13.989 - else
13.990 - kk_intersect (Kodkod.Rel suc_rel)
13.991 - (kk_product Kodkod.Univ (Kodkod.AtomSeq x))
13.992 - | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => Kodkod.Rel nat_add_rel
13.993 - | Cst (Add, Type ("fun", [@{typ int}, _]), _) => Kodkod.Rel int_add_rel
13.994 + | Cst (Suc, T as @{typ "unsigned_bit word => unsigned_bit word"}, R) =>
13.995 + to_bit_word_unary_op T R (curry KK.Add (KK.Num 1))
13.996 + | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
13.997 + kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
13.998 + | Cst (Suc, _, Func (Atom x, _)) => KK.Rel suc_rel
13.999 + | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel
13.1000 + | Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel
13.1001 | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
13.1002 - to_bit_word_binary_op T R NONE (SOME (curry Kodkod.Add))
13.1003 + to_bit_word_binary_op T R NONE (SOME (curry KK.Add))
13.1004 | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
13.1005 to_bit_word_binary_op T R
13.1006 (SOME (fn i1 => fn i2 => fn i3 =>
13.1007 - kk_implies (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i1, i2)))
13.1008 - (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i2, i3)))))
13.1009 - (SOME (curry Kodkod.Add))
13.1010 + kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2)))
13.1011 + (KK.LE (KK.Num 0, KK.BitXor (i2, i3)))))
13.1012 + (SOME (curry KK.Add))
13.1013 | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) =>
13.1014 - Kodkod.Rel nat_subtract_rel
13.1015 + KK.Rel nat_subtract_rel
13.1016 | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) =>
13.1017 - Kodkod.Rel int_subtract_rel
13.1018 + KK.Rel int_subtract_rel
13.1019 | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
13.1020 to_bit_word_binary_op T R NONE
13.1021 (SOME (fn i1 => fn i2 =>
13.1022 - Kodkod.IntIf (Kodkod.LE (i1, i2), Kodkod.Num 0,
13.1023 - Kodkod.Sub (i1, i2))))
13.1024 + KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2))))
13.1025 | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
13.1026 to_bit_word_binary_op T R
13.1027 (SOME (fn i1 => fn i2 => fn i3 =>
13.1028 - kk_implies (Kodkod.LT (Kodkod.BitXor (i1, i2), Kodkod.Num 0))
13.1029 - (Kodkod.LT (Kodkod.BitXor (i2, i3), Kodkod.Num 0))))
13.1030 - (SOME (curry Kodkod.Sub))
13.1031 + kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0))
13.1032 + (KK.LT (KK.BitXor (i2, i3), KK.Num 0))))
13.1033 + (SOME (curry KK.Sub))
13.1034 | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) =>
13.1035 - Kodkod.Rel nat_multiply_rel
13.1036 + KK.Rel nat_multiply_rel
13.1037 | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) =>
13.1038 - Kodkod.Rel int_multiply_rel
13.1039 + KK.Rel int_multiply_rel
13.1040 | Cst (Multiply,
13.1041 T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) =>
13.1042 to_bit_word_binary_op T R
13.1043 (SOME (fn i1 => fn i2 => fn i3 =>
13.1044 - kk_or (Kodkod.IntEq (i2, Kodkod.Num 0))
13.1045 - (Kodkod.IntEq (Kodkod.Div (i3, i2), i1)
13.1046 + kk_or (KK.IntEq (i2, KK.Num 0))
13.1047 + (KK.IntEq (KK.Div (i3, i2), i1)
13.1048 |> bit_T = @{typ signed_bit}
13.1049 - ? kk_and (Kodkod.LE (Kodkod.Num 0,
13.1050 - foldl1 Kodkod.BitAnd [i1, i2, i3])))))
13.1051 - (SOME (curry Kodkod.Mult))
13.1052 - | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) =>
13.1053 - Kodkod.Rel nat_divide_rel
13.1054 - | Cst (Divide, Type ("fun", [@{typ int}, _]), _) =>
13.1055 - Kodkod.Rel int_divide_rel
13.1056 + ? kk_and (KK.LE (KK.Num 0,
13.1057 + foldl1 KK.BitAnd [i1, i2, i3])))))
13.1058 + (SOME (curry KK.Mult))
13.1059 + | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
13.1060 + | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_divide_rel
13.1061 | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
13.1062 to_bit_word_binary_op T R NONE
13.1063 (SOME (fn i1 => fn i2 =>
13.1064 - Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
13.1065 - Kodkod.Num 0, Kodkod.Div (i1, i2))))
13.1066 + KK.IntIf (KK.IntEq (i2, KK.Num 0),
13.1067 + KK.Num 0, KK.Div (i1, i2))))
13.1068 | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
13.1069 to_bit_word_binary_op T R
13.1070 (SOME (fn i1 => fn i2 => fn i3 =>
13.1071 - Kodkod.LE (Kodkod.Num 0, foldl1 Kodkod.BitAnd [i1, i2, i3])))
13.1072 + KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3])))
13.1073 (SOME (fn i1 => fn i2 =>
13.1074 - Kodkod.IntIf (kk_and (Kodkod.LT (i1, Kodkod.Num 0))
13.1075 - (Kodkod.LT (Kodkod.Num 0, i2)),
13.1076 - Kodkod.Sub (Kodkod.Div (Kodkod.Add (i1, Kodkod.Num 1), i2),
13.1077 - Kodkod.Num 1),
13.1078 - Kodkod.IntIf (kk_and (Kodkod.LT (Kodkod.Num 0, i1))
13.1079 - (Kodkod.LT (i2, Kodkod.Num 0)),
13.1080 - Kodkod.Sub (Kodkod.Div (Kodkod.Sub (i1, Kodkod.Num 1),
13.1081 - i2), Kodkod.Num 1),
13.1082 - Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
13.1083 - Kodkod.Num 0, Kodkod.Div (i1, i2))))))
13.1084 - | Cst (Gcd, _, _) => Kodkod.Rel gcd_rel
13.1085 - | Cst (Lcm, _, _) => Kodkod.Rel lcm_rel
13.1086 - | Cst (Fracs, _, Func (Atom (1, _), _)) => Kodkod.None
13.1087 + KK.IntIf (kk_and (KK.LT (i1, KK.Num 0))
13.1088 + (KK.LT (KK.Num 0, i2)),
13.1089 + KK.Sub (KK.Div (KK.Add (i1, KK.Num 1), i2), KK.Num 1),
13.1090 + KK.IntIf (kk_and (KK.LT (KK.Num 0, i1))
13.1091 + (KK.LT (i2, KK.Num 0)),
13.1092 + KK.Sub (KK.Div (KK.Sub (i1, KK.Num 1), i2), KK.Num 1),
13.1093 + KK.IntIf (KK.IntEq (i2, KK.Num 0),
13.1094 + KK.Num 0, KK.Div (i1, i2))))))
13.1095 + | Cst (Gcd, _, _) => KK.Rel gcd_rel
13.1096 + | Cst (Lcm, _, _) => KK.Rel lcm_rel
13.1097 + | Cst (Fracs, _, Func (Atom (1, _), _)) => KK.None
13.1098 | Cst (Fracs, _, Func (Struct _, _)) =>
13.1099 - kk_project_seq (Kodkod.Rel norm_frac_rel) 2 2
13.1100 - | Cst (NormFrac, _, _) => Kodkod.Rel norm_frac_rel
13.1101 + kk_project_seq (KK.Rel norm_frac_rel) 2 2
13.1102 + | Cst (NormFrac, _, _) => KK.Rel norm_frac_rel
13.1103 | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
13.1104 - Kodkod.Iden
13.1105 + KK.Iden
13.1106 | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
13.1107 Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) =>
13.1108 if nat_j0 = int_j0 then
13.1109 - kk_intersect Kodkod.Iden
13.1110 - (kk_product (Kodkod.AtomSeq (max_int_for_card int_k + 1, nat_j0))
13.1111 - Kodkod.Univ)
13.1112 + kk_intersect KK.Iden
13.1113 + (kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0))
13.1114 + KK.Univ)
13.1115 else
13.1116 raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
13.1117 | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
13.1118 @@ -1312,21 +1299,19 @@
13.1119 val overlap = Int.min (nat_k, abs_card)
13.1120 in
13.1121 if nat_j0 = int_j0 then
13.1122 - kk_union (kk_product (Kodkod.AtomSeq (int_k - abs_card,
13.1123 - int_j0 + abs_card))
13.1124 - (Kodkod.Atom nat_j0))
13.1125 - (kk_intersect Kodkod.Iden
13.1126 - (kk_product (Kodkod.AtomSeq (overlap, int_j0))
13.1127 - Kodkod.Univ))
13.1128 + kk_union (kk_product (KK.AtomSeq (int_k - abs_card,
13.1129 + int_j0 + abs_card))
13.1130 + (KK.Atom nat_j0))
13.1131 + (kk_intersect KK.Iden
13.1132 + (kk_product (KK.AtomSeq (overlap, int_j0)) KK.Univ))
13.1133 else
13.1134 raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
13.1135 end
13.1136 | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
13.1137 to_bit_word_unary_op T R
13.1138 - (fn i => Kodkod.IntIf (Kodkod.LE (i, Kodkod.Num 0),
13.1139 - Kodkod.Num 0, i))
13.1140 + (fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i))
13.1141 | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
13.1142 - | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None
13.1143 + | Op1 (Finite, _, Opt (Atom _), _) => KK.None
13.1144 | Op1 (Converse, T, R, u1) =>
13.1145 let
13.1146 val (b_T, a_T) = HOLogic.dest_prodT (domain_type T)
13.1147 @@ -1346,9 +1331,9 @@
13.1148 val body_arity = arity_of_rep body_R
13.1149 in
13.1150 kk_project (to_rep (Func (Struct [a_R, b_R], body_R)) u1)
13.1151 - (map Kodkod.Num (index_seq a_arity b_arity @
13.1152 - index_seq 0 a_arity @
13.1153 - index_seq ab_arity body_arity))
13.1154 + (map KK.Num (index_seq a_arity b_arity @
13.1155 + index_seq 0 a_arity @
13.1156 + index_seq ab_arity body_arity))
13.1157 |> rel_expr_from_rel_expr kk R (Func (Struct [b_R, a_R], body_R))
13.1158 end
13.1159 | Op1 (Closure, _, R, u1) =>
13.1160 @@ -1410,13 +1395,13 @@
13.1161 | Op2 (Exist, T, Opt _, u1, u2) =>
13.1162 let val rs1 = untuple to_decl u1 in
13.1163 if not (is_opt_rep (rep_of u2)) then
13.1164 - kk_rel_if (kk_exist rs1 (to_f u2)) true_atom Kodkod.None
13.1165 + kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None
13.1166 else
13.1167 let val r2 = to_r u2 in
13.1168 kk_union (kk_rel_if (kk_exist rs1 (kk_rel_eq r2 true_atom))
13.1169 - true_atom Kodkod.None)
13.1170 + true_atom KK.None)
13.1171 (kk_rel_if (kk_all rs1 (kk_rel_eq r2 false_atom))
13.1172 - false_atom Kodkod.None)
13.1173 + false_atom KK.None)
13.1174 end
13.1175 end
13.1176 | Op2 (Or, _, _, u1, u2) =>
13.1177 @@ -1437,10 +1422,10 @@
13.1178 kk_rel_if
13.1179 (fold kk_and (map_filter (fn (u, r) =>
13.1180 if is_opt_rep (rep_of u) then SOME (kk_some r)
13.1181 - else NONE) [(u1, r1), (u2, r2)]) Kodkod.True)
13.1182 - (atom_from_formula kk bool_j0 (Kodkod.LT (pairself
13.1183 + else NONE) [(u1, r1), (u2, r2)]) KK.True)
13.1184 + (atom_from_formula kk bool_j0 (KK.LT (pairself
13.1185 (int_expr_from_atom kk (type_of u1)) (r1, r2))))
13.1186 - Kodkod.None)
13.1187 + KK.None)
13.1188 (to_r u1) (to_r u2))
13.1189 | Op2 (The, T, R, u1, u2) =>
13.1190 if is_opt_rep R then
13.1191 @@ -1485,8 +1470,8 @@
13.1192 if f1 = f2 then
13.1193 atom_from_formula kk j0 f1
13.1194 else
13.1195 - kk_union (kk_rel_if f1 true_atom Kodkod.None)
13.1196 - (kk_rel_if f2 Kodkod.None false_atom)
13.1197 + kk_union (kk_rel_if f1 true_atom KK.None)
13.1198 + (kk_rel_if f2 KK.None false_atom)
13.1199 end
13.1200 | Op2 (Union, _, R, u1, u2) =>
13.1201 to_set_op kk_or kk_or3 kk_union kk_union kk_intersect false R u1 u2
13.1202 @@ -1518,7 +1503,7 @@
13.1203 | Opt (Atom (2, _)) =>
13.1204 let
13.1205 (* FIXME: merge with similar code above *)
13.1206 - (* rep -> rep -> nut -> Kodkod.rel_expr *)
13.1207 + (* rep -> rep -> nut -> KK.rel_expr *)
13.1208 fun must R1 R2 u =
13.1209 kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom
13.1210 fun may R1 R2 u =
13.1211 @@ -1553,9 +1538,9 @@
13.1212 (to_rep (Func (b_R, Formula Neut)) u2)
13.1213 | Opt (Atom (2, _)) =>
13.1214 let
13.1215 - (* Kodkod.rel_expr -> rep -> nut -> Kodkod.rel_expr *)
13.1216 + (* KK.rel_expr -> rep -> nut -> KK.rel_expr *)
13.1217 fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r
13.1218 - (* Kodkod.rel_expr -> Kodkod.rel_expr *)
13.1219 + (* KK.rel_expr -> KK.rel_expr *)
13.1220 fun do_term r =
13.1221 kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
13.1222 in kk_union (do_term true_atom) (do_term false_atom) end
13.1223 @@ -1567,7 +1552,7 @@
13.1224 (Func (R11, R12), Func (R21, Formula Neut)) =>
13.1225 if R21 = R11 andalso is_lone_rep R12 then
13.1226 let
13.1227 - (* Kodkod.rel_expr -> Kodkod.rel_expr *)
13.1228 + (* KK.rel_expr -> KK.rel_expr *)
13.1229 fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1)
13.1230 val core_r = big_join (to_r u2)
13.1231 val core_R = Func (R12, Formula Neut)
13.1232 @@ -1593,9 +1578,9 @@
13.1233 | Op2 (Apply, @{typ nat}, _,
13.1234 Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
13.1235 if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
13.1236 - Kodkod.Atom (offset_of_type ofs nat_T)
13.1237 + KK.Atom (offset_of_type ofs nat_T)
13.1238 else
13.1239 - fold kk_join (map to_integer [u1, u2]) (Kodkod.Rel nat_subtract_rel)
13.1240 + fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel)
13.1241 | Op2 (Apply, _, R, u1, u2) =>
13.1242 if is_Cst Unrep u2 andalso is_set_type (type_of u1)
13.1243 andalso is_FreeName u1 then
13.1244 @@ -1603,7 +1588,7 @@
13.1245 else
13.1246 to_apply R u1 u2
13.1247 | Op2 (Lambda, T, R as Opt (Atom (1, j0)), u1, u2) =>
13.1248 - to_guard [u1, u2] R (Kodkod.Atom j0)
13.1249 + to_guard [u1, u2] R (KK.Atom j0)
13.1250 | Op2 (Lambda, T, Func (_, Formula Neut), u1, u2) =>
13.1251 kk_comprehension (untuple to_decl u1) (to_f u2)
13.1252 | Op2 (Lambda, T, Func (_, R2), u1, u2) =>
13.1253 @@ -1639,10 +1624,9 @@
13.1254 | Vect (k, R) => to_product (replicate k R) us
13.1255 | Atom (1, j0) =>
13.1256 (case filter (not_equal Unit o rep_of) us of
13.1257 - [] => Kodkod.Atom j0
13.1258 - | us' =>
13.1259 - kk_rel_if (kk_some (fold1 kk_product (map to_r us')))
13.1260 - (Kodkod.Atom j0) Kodkod.None)
13.1261 + [] => KK.Atom j0
13.1262 + | us' => kk_rel_if (kk_some (fold1 kk_product (map to_r us')))
13.1263 + (KK.Atom j0) KK.None)
13.1264 | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
13.1265 | Construct ([u'], _, _, []) => to_r u'
13.1266 | Construct (_ :: sel_us, T, R, arg_us) =>
13.1267 @@ -1660,47 +1644,46 @@
13.1268 else
13.1269 kk_comprehension
13.1270 (decls_for_atom_schema ~1 (atom_schema_of_rep R1))
13.1271 - (kk_rel_eq (kk_join (Kodkod.Var (1, ~1)) sel_r)
13.1272 - arg_r)
13.1273 + (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r)
13.1274 end) sel_us arg_us
13.1275 in fold1 kk_intersect set_rs end
13.1276 - | BoundRel (x, _, _, _) => Kodkod.Var x
13.1277 - | FreeRel (x, _, _, _) => Kodkod.Rel x
13.1278 - | RelReg (j, _, R) => Kodkod.RelReg (arity_of_rep R, j)
13.1279 + | BoundRel (x, _, _, _) => KK.Var x
13.1280 + | FreeRel (x, _, _, _) => KK.Rel x
13.1281 + | RelReg (j, _, R) => KK.RelReg (arity_of_rep R, j)
13.1282 | u => raise NUT ("Nitpick_Kodkod.to_r", [u])
13.1283 - (* nut -> Kodkod.decl *)
13.1284 + (* nut -> KK.decl *)
13.1285 and to_decl (BoundRel (x, _, R, _)) =
13.1286 - Kodkod.DeclOne (x, Kodkod.AtomSeq (the_single (atom_schema_of_rep R)))
13.1287 + KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R)))
13.1288 | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
13.1289 - (* nut -> Kodkod.expr_assign *)
13.1290 + (* nut -> KK.expr_assign *)
13.1291 and to_expr_assign (FormulaReg (j, _, R)) u =
13.1292 - Kodkod.AssignFormulaReg (j, to_f u)
13.1293 + KK.AssignFormulaReg (j, to_f u)
13.1294 | to_expr_assign (RelReg (j, _, R)) u =
13.1295 - Kodkod.AssignRelReg ((arity_of_rep R, j), to_r u)
13.1296 + KK.AssignRelReg ((arity_of_rep R, j), to_r u)
13.1297 | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
13.1298 - (* int * int -> nut -> Kodkod.rel_expr *)
13.1299 + (* int * int -> nut -> KK.rel_expr *)
13.1300 and to_atom (x as (k, j0)) u =
13.1301 case rep_of u of
13.1302 Formula _ => atom_from_formula kk j0 (to_f u)
13.1303 - | Unit => if k = 1 then Kodkod.Atom j0
13.1304 + | Unit => if k = 1 then KK.Atom j0
13.1305 else raise NUT ("Nitpick_Kodkod.to_atom", [u])
13.1306 | R => atom_from_rel_expr kk x R (to_r u)
13.1307 - (* rep list -> nut -> Kodkod.rel_expr *)
13.1308 + (* rep list -> nut -> KK.rel_expr *)
13.1309 and to_struct Rs u =
13.1310 case rep_of u of
13.1311 Unit => full_rel_for_rep (Struct Rs)
13.1312 | R' => struct_from_rel_expr kk Rs R' (to_r u)
13.1313 - (* int -> rep -> nut -> Kodkod.rel_expr *)
13.1314 + (* int -> rep -> nut -> KK.rel_expr *)
13.1315 and to_vect k R u =
13.1316 case rep_of u of
13.1317 Unit => full_rel_for_rep (Vect (k, R))
13.1318 | R' => vect_from_rel_expr kk k R R' (to_r u)
13.1319 - (* rep -> rep -> nut -> Kodkod.rel_expr *)
13.1320 + (* rep -> rep -> nut -> KK.rel_expr *)
13.1321 and to_func R1 R2 u =
13.1322 case rep_of u of
13.1323 Unit => full_rel_for_rep (Func (R1, R2))
13.1324 | R' => rel_expr_to_func kk R1 R2 R' (to_r u)
13.1325 - (* rep -> nut -> Kodkod.rel_expr *)
13.1326 + (* rep -> nut -> KK.rel_expr *)
13.1327 and to_opt R u =
13.1328 let val old_R = rep_of u in
13.1329 if is_opt_rep old_R then
13.1330 @@ -1708,16 +1691,16 @@
13.1331 else
13.1332 to_rep R u
13.1333 end
13.1334 - (* rep -> nut -> Kodkod.rel_expr *)
13.1335 + (* rep -> nut -> KK.rel_expr *)
13.1336 and to_rep (Atom x) u = to_atom x u
13.1337 | to_rep (Struct Rs) u = to_struct Rs u
13.1338 | to_rep (Vect (k, R)) u = to_vect k R u
13.1339 | to_rep (Func (R1, R2)) u = to_func R1 R2 u
13.1340 | to_rep (Opt R) u = to_opt R u
13.1341 | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R])
13.1342 - (* nut -> Kodkod.rel_expr *)
13.1343 + (* nut -> KK.rel_expr *)
13.1344 and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u
13.1345 - (* nut list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.1346 + (* nut list -> rep -> KK.rel_expr -> KK.rel_expr *)
13.1347 and to_guard guard_us R r =
13.1348 let
13.1349 val unpacked_rs = unpack_joins r
13.1350 @@ -1737,16 +1720,16 @@
13.1351 else
13.1352 kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
13.1353 end
13.1354 - (* rep -> rep -> Kodkod.rel_expr -> int -> Kodkod.rel_expr *)
13.1355 + (* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *)
13.1356 and to_project new_R old_R r j0 =
13.1357 rel_expr_from_rel_expr kk new_R old_R
13.1358 (kk_project_seq r j0 (arity_of_rep old_R))
13.1359 - (* rep list -> nut list -> Kodkod.rel_expr *)
13.1360 + (* rep list -> nut list -> KK.rel_expr *)
13.1361 and to_product Rs us =
13.1362 case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of
13.1363 [] => raise REP ("Nitpick_Kodkod.to_product", Rs)
13.1364 | rs => fold1 kk_product rs
13.1365 - (* int -> typ -> rep -> nut -> Kodkod.rel_expr *)
13.1366 + (* int -> typ -> rep -> nut -> KK.rel_expr *)
13.1367 and to_nth_pair_sel n res_T res_R u =
13.1368 case u of
13.1369 Tuple (_, _, us) => to_rep res_R (nth us n)
13.1370 @@ -1774,9 +1757,9 @@
13.1371 (to_rep res_R (Cst (Unity, res_T, Unit)))
13.1372 | arity => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
13.1373 end
13.1374 - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula)
13.1375 - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) -> nut -> nut
13.1376 - -> Kodkod.formula *)
13.1377 + (* (KK.formula -> KK.formula -> KK.formula)
13.1378 + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> nut -> nut
13.1379 + -> KK.formula *)
13.1380 and to_set_bool_op connective set_oper u1 u2 =
13.1381 let
13.1382 val min_R = min_rep (rep_of u1) (rep_of u2)
13.1383 @@ -1792,12 +1775,12 @@
13.1384 (kk_join r2 true_atom)
13.1385 | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
13.1386 end
13.1387 - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula)
13.1388 - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
13.1389 - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula)
13.1390 - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula)
13.1391 - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) -> bool -> rep
13.1392 - -> nut -> nut -> Kodkod.rel_expr *)
13.1393 + (* (KK.formula -> KK.formula -> KK.formula)
13.1394 + -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr)
13.1395 + -> (KK.rel_expr -> KK.rel_expr -> KK.formula)
13.1396 + -> (KK.rel_expr -> KK.rel_expr -> KK.formula)
13.1397 + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> bool -> rep -> nut
13.1398 + -> nut -> KK.rel_expr *)
13.1399 and to_set_op connective connective3 set_oper true_set_oper false_set_oper
13.1400 neg_second R u1 u2 =
13.1401 let
13.1402 @@ -1829,51 +1812,47 @@
13.1403 r1 r2
13.1404 | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
13.1405 end
13.1406 - (* typ -> rep -> (Kodkod.int_expr -> Kodkod.int_expr) -> Kodkod.rel_expr *)
13.1407 + (* typ -> rep -> (KK.int_expr -> KK.int_expr) -> KK.rel_expr *)
13.1408 and to_bit_word_unary_op T R oper =
13.1409 let
13.1410 val Ts = strip_type T ||> single |> op @
13.1411 - (* int -> Kodkod.int_expr *)
13.1412 - fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
13.1413 + (* int -> KK.int_expr *)
13.1414 + fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))
13.1415 in
13.1416 kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
13.1417 - (Kodkod.FormulaLet
13.1418 - (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 1),
13.1419 - Kodkod.IntEq (Kodkod.IntReg 1, oper (Kodkod.IntReg 0))))
13.1420 + (KK.FormulaLet
13.1421 + (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 1),
13.1422 + KK.IntEq (KK.IntReg 1, oper (KK.IntReg 0))))
13.1423 end
13.1424 - (* typ -> rep
13.1425 - -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr -> bool) option
13.1426 - -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr) option
13.1427 - -> Kodkod.rel_expr *)
13.1428 + (* typ -> rep -> (KK.int_expr -> KK.int_expr -> KK.int_expr -> bool) option
13.1429 + -> (KK.int_expr -> KK.int_expr -> KK.int_expr) option -> KK.rel_expr *)
13.1430 and to_bit_word_binary_op T R opt_guard opt_oper =
13.1431 let
13.1432 val Ts = strip_type T ||> single |> op @
13.1433 - (* int -> Kodkod.int_expr *)
13.1434 - fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
13.1435 + (* int -> KK.int_expr *)
13.1436 + fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))
13.1437 in
13.1438 kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
13.1439 - (Kodkod.FormulaLet
13.1440 - (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 2),
13.1441 + (KK.FormulaLet
13.1442 + (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 2),
13.1443 fold1 kk_and
13.1444 ((case opt_guard of
13.1445 NONE => []
13.1446 | SOME guard =>
13.1447 - [guard (Kodkod.IntReg 0) (Kodkod.IntReg 1)
13.1448 - (Kodkod.IntReg 2)]) @
13.1449 + [guard (KK.IntReg 0) (KK.IntReg 1) (KK.IntReg 2)]) @
13.1450 (case opt_oper of
13.1451 NONE => []
13.1452 | SOME oper =>
13.1453 - [Kodkod.IntEq (Kodkod.IntReg 2,
13.1454 - oper (Kodkod.IntReg 0) (Kodkod.IntReg 1))]))))
13.1455 + [KK.IntEq (KK.IntReg 2,
13.1456 + oper (KK.IntReg 0) (KK.IntReg 1))]))))
13.1457 end
13.1458 - (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *)
13.1459 + (* rep -> rep -> KK.rel_expr -> nut -> KK.rel_expr *)
13.1460 and to_apply res_R func_u arg_u =
13.1461 case unopt_rep (rep_of func_u) of
13.1462 Unit =>
13.1463 let val j0 = offset_of_type ofs (type_of func_u) in
13.1464 to_guard [arg_u] res_R
13.1465 - (rel_expr_from_rel_expr kk res_R (Atom (1, j0))
13.1466 - (Kodkod.Atom j0))
13.1467 + (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0))
13.1468 end
13.1469 | Atom (1, j0) =>
13.1470 to_guard [arg_u] res_R
13.1471 @@ -1902,7 +1881,7 @@
13.1472 (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
13.1473 |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
13.1474 | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])
13.1475 - (* int -> rep -> rep -> Kodkod.rel_expr -> nut *)
13.1476 + (* int -> rep -> rep -> KK.rel_expr -> nut *)
13.1477 and to_apply_vect k R' res_R func_r arg_u =
13.1478 let
13.1479 val arg_R = one_rep ofs (type_of arg_u) (unopt_rep (rep_of arg_u))
13.1480 @@ -1912,11 +1891,10 @@
13.1481 kk_case_switch kk arg_R res_R (to_opt arg_R arg_u)
13.1482 (all_singletons_for_rep arg_R) vect_rs
13.1483 end
13.1484 - (* bool -> nut -> Kodkod.formula *)
13.1485 + (* bool -> nut -> KK.formula *)
13.1486 and to_could_be_unrep neg u =
13.1487 - if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u)
13.1488 - else Kodkod.False
13.1489 - (* nut -> Kodkod.rel_expr -> Kodkod.rel_expr *)
13.1490 + if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u) else KK.False
13.1491 + (* nut -> KK.rel_expr -> KK.rel_expr *)
13.1492 and to_compare_with_unrep u r =
13.1493 if is_opt_rep (rep_of u) then
13.1494 kk_rel_if (kk_some (to_r u)) r (empty_rel_for_rep (rep_of u))
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Dec 17 15:22:27 2009 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Dec 18 12:00:29 2009 +0100
14.3 @@ -40,6 +40,8 @@
14.4 open Nitpick_Rep
14.5 open Nitpick_Nut
14.6
14.7 +structure KK = Kodkod
14.8 +
14.9 type params = {
14.10 show_skolems: bool,
14.11 show_datatypes: bool,
14.12 @@ -71,19 +73,22 @@
14.13 else
14.14 Const (atom_name "" T j, T)
14.15
14.16 +(* term -> real *)
14.17 +fun extract_real_number (Const (@{const_name HOL.divide}, _) $ t1 $ t2) =
14.18 + real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
14.19 + | extract_real_number t = real (snd (HOLogic.dest_number t))
14.20 (* term * term -> order *)
14.21 fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
14.22 - | nice_term_ord (t1, t2) =
14.23 - int_ord (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
14.24 + | nice_term_ord tp = Real.compare (pairself extract_real_number tp)
14.25 handle TERM ("dest_number", _) =>
14.26 - case (t1, t2) of
14.27 + case tp of
14.28 (t11 $ t12, t21 $ t22) =>
14.29 (case nice_term_ord (t11, t21) of
14.30 EQUAL => nice_term_ord (t12, t22)
14.31 | ord => ord)
14.32 - | _ => TermOrd.term_ord (t1, t2)
14.33 + | _ => TermOrd.fast_term_ord tp
14.34
14.35 -(* nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list *)
14.36 +(* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
14.37 fun tuple_list_for_name rel_table bounds name =
14.38 the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
14.39
14.40 @@ -240,8 +245,8 @@
14.41 | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
14.42
14.43 (* string * string * string * string -> scope -> nut list -> nut list
14.44 - -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> typ -> typ
14.45 - -> rep -> int list list -> term *)
14.46 + -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
14.47 + -> int list list -> term *)
14.48 fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
14.49 ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
14.50 : scope) sel_names rel_table bounds =
14.51 @@ -324,7 +329,7 @@
14.52 | _ => t
14.53 (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
14.54 fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
14.55 - ts1 ~~ ts2 |> T1 = @{typ bisim_iterator} ? rev
14.56 + ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
14.57 |> make_plain_fun (maybe_opt andalso not for_auto) T1 T2
14.58 |> unbit_and_unbox_term
14.59 |> typecast_fun (unbit_and_unbox_type T')
14.60 @@ -506,7 +511,7 @@
14.61 oooo term_for_rep []
14.62 end
14.63
14.64 -(* scope -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> nut
14.65 +(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
14.66 -> term *)
14.67 fun term_for_name scope sel_names rel_table bounds name =
14.68 let val T = type_of name in
14.69 @@ -563,7 +568,7 @@
14.70 end
14.71
14.72 (* params -> scope -> (term option * int list) list -> styp list -> nut list
14.73 - -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
14.74 + -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
14.75 -> Pretty.T * bool *)
14.76 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
14.77 ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
14.78 @@ -704,7 +709,7 @@
14.79 end
14.80
14.81 (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
14.82 - -> Kodkod.raw_bound list -> term -> bool option *)
14.83 + -> KK.raw_bound list -> term -> bool option *)
14.84 fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, ...})
14.85 auto_timeout free_names sel_names rel_table bounds prop =
14.86 let
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Dec 17 15:22:27 2009 +0100
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Dec 18 12:00:29 2009 +0100
15.3 @@ -130,6 +130,8 @@
15.4 open Nitpick_Peephole
15.5 open Nitpick_Rep
15.6
15.7 +structure KK = Kodkod
15.8 +
15.9 datatype cst =
15.10 Unity |
15.11 False |
15.12 @@ -196,8 +198,8 @@
15.13 BoundName of int * typ * rep * string |
15.14 FreeName of string * typ * rep |
15.15 ConstName of string * typ * rep |
15.16 - BoundRel of Kodkod.n_ary_index * typ * rep * string |
15.17 - FreeRel of Kodkod.n_ary_index * typ * rep * string |
15.18 + BoundRel of KK.n_ary_index * typ * rep * string |
15.19 + FreeRel of KK.n_ary_index * typ * rep * string |
15.20 RelReg of int * typ * rep |
15.21 FormulaReg of int * typ * rep
15.22
15.23 @@ -439,7 +441,7 @@
15.24 case NameTable.lookup table name of
15.25 SOME u => u
15.26 | NONE => raise NUT ("Nitpick_Nut.the_name", [name])
15.27 -(* nut NameTable.table -> nut -> Kodkod.n_ary_index *)
15.28 +(* nut NameTable.table -> nut -> KK.n_ary_index *)
15.29 fun the_rel table name =
15.30 case the_name table name of
15.31 FreeRel (x, _, _, _) => x
15.32 @@ -915,10 +917,8 @@
15.33 | Cst (True, T, _) => Cst (True, T, Formula Neut)
15.34 | Cst (Num j, T, _) =>
15.35 if is_word_type T then
15.36 - if is_twos_complement_representable bits j then
15.37 - Cst (Num j, T, best_non_opt_set_rep_for_type scope T)
15.38 - else
15.39 - Cst (Unrep, T, best_opt_set_rep_for_type scope T)
15.40 + Cst (if is_twos_complement_representable bits j then Num j
15.41 + else Unrep, T, best_opt_set_rep_for_type scope T)
15.42 else
15.43 (case spec_of_type scope T of
15.44 (1, j0) => if j = 0 then Cst (Unity, T, Unit)
15.45 @@ -1239,8 +1239,8 @@
15.46 |> optimize_unit
15.47 in aux table def Pos end
15.48
15.49 -(* int -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list
15.50 - -> int * Kodkod.n_ary_index list *)
15.51 +(* int -> KK.n_ary_index list -> KK.n_ary_index list
15.52 + -> int * KK.n_ary_index list *)
15.53 fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys)
15.54 | fresh_n_ary_index n ((m, j) :: xs) ys =
15.55 if m = n then (j, ys @ ((m, j + 1) :: xs))
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Thu Dec 17 15:22:27 2009 +0100
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Dec 18 12:00:29 2009 +0100
16.3 @@ -266,7 +266,7 @@
16.4
16.5 (* bool -> int *)
16.6 val from_bool = atom_for_bool main_j0
16.7 - (* int -> Kodkod.rel_expr *)
16.8 + (* int -> rel_expr *)
16.9 fun from_nat n = Atom (n + main_j0)
16.10 val from_int = Atom o atom_for_int (int_card, main_j0)
16.11 (* int -> int *)
16.12 @@ -347,7 +347,7 @@
16.13 (* rel_expr -> formula *)
16.14 fun s_no None = True
16.15 | s_no (Product (r1, r2)) = s_or (s_no r1) (s_no r2)
16.16 - | s_no (Intersect (Closure (Kodkod.Rel x), Kodkod.Iden)) = Acyclic x
16.17 + | s_no (Intersect (Closure (Rel x), Iden)) = Acyclic x
16.18 | s_no r = if is_one_rel_expr r then False else No r
16.19 fun s_lone None = True
16.20 | s_lone r = if is_one_rel_expr r then True else Lone r
16.21 @@ -409,8 +409,8 @@
16.22 s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)
16.23 else
16.24 RelEq (r1, r2)
16.25 - | (_, Kodkod.None) => s_no r1
16.26 - | (Kodkod.None, _) => s_no r2
16.27 + | (_, None) => s_no r1
16.28 + | (None, _) => s_no r2
16.29 | _ => RelEq (r1, r2)
16.30 fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2)
16.31 | s_subset (Atom j) (AtomSeq (k, j0)) =
17.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Dec 17 15:22:27 2009 +0100
17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Dec 18 12:00:29 2009 +0100
17.3 @@ -249,6 +249,10 @@
17.4 [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
17.5 else if T = @{typ signed_bit} then
17.6 [(Card T, map (Integer.add 1 o Integer.min max_bits o Integer.max 1) bitss)]
17.7 + else if T = @{typ "unsigned_bit word"} then
17.8 + [(Card T, lookup_type_ints_assign thy cards_assigns nat_T)]
17.9 + else if T = @{typ "signed_bit word"} then
17.10 + [(Card T, lookup_type_ints_assign thy cards_assigns int_T)]
17.11 else if T = @{typ bisim_iterator} then
17.12 [(Card T, map (Integer.add 1 o Integer.max 0) bisim_depths)]
17.13 else if is_fp_iterator_type T then
17.14 @@ -316,32 +320,20 @@
17.15 [] => false
17.16 | xs =>
17.17 let
17.18 - val exact_cards =
17.19 - map (Integer.prod
17.20 - o map (bounded_exact_card_of_type ext_ctxt k 0 card_assigns)
17.21 + val dom_cards =
17.22 + map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns)
17.23 o binder_types o snd) xs
17.24 val maxes = map (constr_max max_assigns) xs
17.25 (* int -> int -> int *)
17.26 - fun effective_max 0 ~1 = k
17.27 - | effective_max 0 max = max
17.28 - | effective_max card ~1 = card
17.29 + fun effective_max card ~1 = card
17.30 | effective_max card max = Int.min (card, max)
17.31 - val max = map2 effective_max exact_cards maxes |> Integer.sum
17.32 - (* unit -> int *)
17.33 - fun doms_card () =
17.34 - xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns)
17.35 - o binder_types o snd)
17.36 - |> Integer.sum
17.37 - in
17.38 - max < k
17.39 - orelse (forall (not_equal 0) exact_cards andalso doms_card () < k)
17.40 - end
17.41 - handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
17.42 -
17.43 -(* extended_context -> scope_desc -> bool *)
17.44 -fun is_surely_inconsistent_scope_description ext_ctxt
17.45 - (desc as (card_assigns, _)) =
17.46 - exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_assigns
17.47 + val max = map2 effective_max dom_cards maxes |> Integer.sum
17.48 + in max < k end
17.49 +(* extended_context -> (typ * int) list -> (typ * int) list
17.50 + -> (styp * int) list -> bool *)
17.51 +fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns =
17.52 + exists (is_surely_inconsistent_card_assign ext_ctxt
17.53 + (seen @ rest, max_assigns)) seen
17.54
17.55 (* extended_context -> scope_desc -> (typ * int) list option *)
17.56 fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
17.57 @@ -349,15 +341,15 @@
17.58 (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
17.59 fun aux seen [] = SOME seen
17.60 | aux seen ((T, 0) :: _) = NONE
17.61 - | aux seen ((T, k) :: assigns) =
17.62 - (if is_surely_inconsistent_scope_description ext_ctxt
17.63 - ((T, k) :: seen, max_assigns) then
17.64 + | aux seen ((T, k) :: rest) =
17.65 + (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen)
17.66 + rest max_assigns then
17.67 raise SAME ()
17.68 else
17.69 - case aux ((T, k) :: seen) assigns of
17.70 + case aux ((T, k) :: seen) rest of
17.71 SOME assigns => SOME assigns
17.72 | NONE => raise SAME ())
17.73 - handle SAME () => aux seen ((T, k - 1) :: assigns)
17.74 + handle SAME () => aux seen ((T, k - 1) :: rest)
17.75 in aux [] (rev card_assigns) end
17.76
17.77 (* theory -> (typ * int) list -> typ * int -> typ * int *)