author  blanchet 
Fri, 18 Dec 2009 12:00:29 +0100  
changeset 34126  8a2c5d7aff51 
parent 34124  c4628a1dcf75 
child 34288  cf455b5880e1 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_kodkod.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2008, 2009 

4 

5 
Kodkod problem generator part of Kodkod. 

6 
*) 

7 

8 
signature NITPICK_KODKOD = 

9 
sig 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

10 
type extended_context = Nitpick_HOL.extended_context 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

11 
type dtype_spec = Nitpick_Scope.dtype_spec 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

12 
type kodkod_constrs = Nitpick_Peephole.kodkod_constrs 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

13 
type nut = Nitpick_Nut.nut 
33192  14 
type nfa_transition = Kodkod.rel_expr * typ 
15 
type nfa_entry = typ * nfa_transition list 

16 
type nfa_table = nfa_entry list 

17 

18 
structure NameTable : TABLE 

19 

20 
val univ_card : 

21 
int > int > int > Kodkod.bound list > Kodkod.formula > int 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

22 
val check_bits : int > Kodkod.formula > unit 
33192  23 
val check_arity : int > int > unit 
24 
val kk_tuple : bool > int > int list > Kodkod.tuple 

25 
val tuple_set_from_atom_schema : (int * int) list > Kodkod.tuple_set 

26 
val sequential_int_bounds : int > Kodkod.int_bound list 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

27 
val pow_of_two_int_bounds : int > int > int > Kodkod.int_bound list 
33192  28 
val bounds_for_built_in_rels_in_formula : 
29 
bool > int > int > int > int > Kodkod.formula > Kodkod.bound list 

30 
val bound_for_plain_rel : Proof.context > bool > nut > Kodkod.bound 

31 
val bound_for_sel_rel : 

32 
Proof.context > bool > dtype_spec list > nut > Kodkod.bound 

33 
val merge_bounds : Kodkod.bound list > Kodkod.bound list 

34 
val declarative_axiom_for_plain_rel : kodkod_constrs > nut > Kodkod.formula 

35 
val declarative_axioms_for_datatypes : 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

36 
extended_context > int > int Typtab.table > kodkod_constrs 
33192  37 
> nut NameTable.table > dtype_spec list > Kodkod.formula list 
38 
val kodkod_formula_from_nut : 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

39 
int > int Typtab.table > bool > kodkod_constrs > nut > Kodkod.formula 
33192  40 
end; 
41 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

42 
structure Nitpick_Kodkod : NITPICK_KODKOD = 
33192  43 
struct 
44 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

45 
open Nitpick_Util 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

46 
open Nitpick_HOL 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

47 
open Nitpick_Scope 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

48 
open Nitpick_Peephole 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

49 
open Nitpick_Rep 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

50 
open Nitpick_Nut 
33192  51 

34126  52 
structure KK = Kodkod 
53 

54 
type nfa_transition = KK.rel_expr * typ 

33192  55 
type nfa_entry = typ * nfa_transition list 
56 
type nfa_table = nfa_entry list 

57 

58 
structure NfaGraph = Graph(type key = typ val ord = TermOrd.typ_ord) 

59 

34126  60 
(* int > KK.int_expr list *) 
61 
fun flip_nums n = index_seq 1 n @ [0] > map KK.Num 

33192  62 

34126  63 
(* int > int > int > KK.bound list > KK.formula > int *) 
33192  64 
fun univ_card nat_card int_card main_j0 bounds formula = 
65 
let 

34126  66 
(* KK.rel_expr > int > int *) 
33192  67 
fun rel_expr_func r k = 
68 
Int.max (k, case r of 

34126  69 
KK.Atom j => j + 1 
70 
 KK.AtomSeq (k', j0) => j0 + k' 

33192  71 
 _ => 0) 
34126  72 
(* KK.tuple > int > int *) 
33192  73 
fun tuple_func t k = 
74 
case t of 

34126  75 
KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k 
33192  76 
 _ => k 
34126  77 
(* KK.tuple_set > int > int *) 
33192  78 
fun tuple_set_func ts k = 
34126  79 
Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k'  _ => 0) 
33192  80 
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, 
81 
int_expr_func = K I} 

82 
val tuple_F = {tuple_func = tuple_func, tuple_set_func = tuple_set_func} 

34126  83 
val card = fold (KK.fold_bound expr_F tuple_F) bounds 1 
84 
> KK.fold_formula expr_F formula 

33192  85 
in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end 
86 

34126  87 
(* int > KK.formula > unit *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

88 
fun check_bits bits formula = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

89 
let 
34126  90 
(* KK.int_expr > unit > unit *) 
91 
fun int_expr_func (KK.Num k) () = 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

92 
if is_twos_complement_representable bits k then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

93 
() 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

94 
else 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

95 
raise TOO_SMALL ("Nitpick_Kodkod.check_bits", 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

96 
"\"bits\" value " ^ string_of_int bits ^ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

97 
" too small for problem") 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

98 
 int_expr_func _ () = () 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

99 
val expr_F = {formula_func = K I, rel_expr_func = K I, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

100 
int_expr_func = int_expr_func} 
34126  101 
in KK.fold_formula expr_F formula () end 
33192  102 

103 
(* int > int > unit *) 

104 
fun check_arity univ_card n = 

34126  105 
if n > KK.max_arity univ_card then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

106 
raise TOO_LARGE ("Nitpick_Kodkod.check_arity", 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

107 
"arity " ^ string_of_int n ^ " too large for universe of \ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

108 
\cardinality " ^ string_of_int univ_card) 
33192  109 
else 
110 
() 

111 

34126  112 
(* bool > int > int list > KK.tuple *) 
33192  113 
fun kk_tuple debug univ_card js = 
114 
if debug then 

34126  115 
KK.Tuple js 
33192  116 
else 
34126  117 
KK.TupleIndex (length js, 
118 
fold (fn j => fn accum => accum * univ_card + j) js 0) 

33192  119 

34126  120 
(* (int * int) list > KK.tuple_set *) 
121 
val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq 

122 
(* rep > KK.tuple_set *) 

33192  123 
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep 
124 

34126  125 
(* int > KK.tuple_set *) 
126 
val single_atom = KK.TupleSet o single o KK.Tuple o single 

127 
(* int > KK.int_bound list *) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

128 
fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))] 
34126  129 
(* int > int > KK.int_bound list *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

130 
fun pow_of_two_int_bounds bits j0 univ_card = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

131 
let 
34126  132 
(* int > int > int > KK.int_bound list *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

133 
fun aux 0 _ _ = [] 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

134 
 aux 1 pow_of_two j = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

135 
if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else [] 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

136 
 aux iter pow_of_two j = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

137 
(SOME pow_of_two, [single_atom j]) :: 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

138 
aux (iter  1) (2 * pow_of_two) (j + 1) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

139 
in aux (bits + 1) 1 j0 end 
33192  140 

34126  141 
(* KK.formula > KK.n_ary_index list *) 
33192  142 
fun built_in_rels_in_formula formula = 
143 
let 

34126  144 
(* KK.rel_expr > KK.n_ary_index list > KK.n_ary_index list *) 
145 
fun rel_expr_func (r as KK.Rel (x as (n, j))) = 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

146 
if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

147 
I 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

148 
else 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

149 
(case AList.lookup (op =) (#rels initial_pool) n of 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

150 
SOME k => j < k ? insert (op =) x 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

151 
 NONE => I) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

152 
 rel_expr_func _ = I 
33192  153 
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, 
154 
int_expr_func = K I} 

34126  155 
in KK.fold_formula expr_F formula [] end 
33192  156 

157 
val max_table_size = 65536 

158 

159 
(* int > unit *) 

160 
fun check_table_size k = 

161 
if k > max_table_size then 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

162 
raise TOO_LARGE ("Nitpick_Kodkod.check_table_size", 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

163 
"precomputed table too large (" ^ string_of_int k ^ ")") 
33192  164 
else 
165 
() 

166 

34126  167 
(* bool > int > int * int > (int > int) > KK.tuple list *) 
33192  168 
fun tabulate_func1 debug univ_card (k, j0) f = 
169 
(check_table_size k; 

170 
map_filter (fn j1 => let val j2 = f j1 in 

171 
if j2 >= 0 then 

172 
SOME (kk_tuple debug univ_card [j1 + j0, j2 + j0]) 

173 
else 

174 
NONE 

175 
end) (index_seq 0 k)) 

34126  176 
(* bool > int > int * int > int > (int * int > int) > KK.tuple list *) 
33192  177 
fun tabulate_op2 debug univ_card (k, j0) res_j0 f = 
178 
(check_table_size (k * k); 

179 
map_filter (fn j => let 

180 
val j1 = j div k 

181 
val j2 = j  j1 * k 

182 
val j3 = f (j1, j2) 

183 
in 

184 
if j3 >= 0 then 

185 
SOME (kk_tuple debug univ_card 

186 
[j1 + j0, j2 + j0, j3 + res_j0]) 

187 
else 

188 
NONE 

189 
end) (index_seq 0 (k * k))) 

190 
(* bool > int > int * int > int > (int * int > int * int) 

34126  191 
> KK.tuple list *) 
33192  192 
fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f = 
193 
(check_table_size (k * k); 

194 
map_filter (fn j => let 

195 
val j1 = j div k 

196 
val j2 = j  j1 * k 

197 
val (j3, j4) = f (j1, j2) 

198 
in 

199 
if j3 >= 0 andalso j4 >= 0 then 

200 
SOME (kk_tuple debug univ_card 

201 
[j1 + j0, j2 + j0, j3 + res_j0, 

202 
j4 + res_j0]) 

203 
else 

204 
NONE 

205 
end) (index_seq 0 (k * k))) 

34126  206 
(* bool > int > int * int > (int * int > int) > KK.tuple list *) 
33192  207 
fun tabulate_nat_op2 debug univ_card (k, j0) f = 
208 
tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f) 

209 
fun tabulate_int_op2 debug univ_card (k, j0) f = 

210 
tabulate_op2 debug univ_card (k, j0) j0 

211 
(atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0))) 

34126  212 
(* bool > int > int * int > (int * int > int * int) > KK.tuple list *) 
33192  213 
fun tabulate_int_op2_2 debug univ_card (k, j0) f = 
214 
tabulate_op2_2 debug univ_card (k, j0) j0 

215 
(pairself (atom_for_int (k, 0)) o f 

216 
o pairself (int_for_atom (k, 0))) 

217 

218 
(* int * int > int *) 

219 
fun isa_div (m, n) = m div n handle General.Div => 0 

220 
fun isa_mod (m, n) = m mod n handle General.Div => m 

221 
fun isa_gcd (m, 0) = m 

222 
 isa_gcd (m, n) = isa_gcd (n, isa_mod (m, n)) 

223 
fun isa_lcm (m, n) = isa_div (m * n, isa_gcd (m, n)) 

224 
val isa_zgcd = isa_gcd o pairself abs 

225 
(* int * int > int * int *) 

226 
fun isa_norm_frac (m, n) = 

227 
if n < 0 then isa_norm_frac (~m, ~n) 

228 
else if m = 0 orelse n = 0 then (0, 1) 

229 
else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end 

230 

231 
(* bool > int > int > int > int > int * int 

34126  232 
> string * bool * KK.tuple list *) 
33192  233 
fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) = 
234 
(check_arity univ_card n; 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

235 
if x = not3_rel then 
33192  236 
("not3", tabulate_func1 debug univ_card (2, j0) (curry (op ) 1)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

237 
else if x = suc_rel then 
33192  238 
("suc", tabulate_func1 debug univ_card (univ_card  j0  1, j0) 
239 
(Integer.add 1)) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

240 
else if x = nat_add_rel then 
33192  241 
("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

242 
else if x = int_add_rel then 
33192  243 
("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

244 
else if x = nat_subtract_rel then 
33192  245 
("nat_subtract", 
33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33631
diff
changeset

246 
tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

247 
else if x = int_subtract_rel then 
33192  248 
("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op )) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

249 
else if x = nat_multiply_rel then 
33192  250 
("nat_multiply", tabulate_nat_op2 debug univ_card (nat_card, j0) (op * )) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

251 
else if x = int_multiply_rel then 
33192  252 
("int_multiply", tabulate_int_op2 debug univ_card (int_card, j0) (op * )) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

253 
else if x = nat_divide_rel then 
33192  254 
("nat_divide", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_div) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

255 
else if x = int_divide_rel then 
33192  256 
("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

257 
else if x = nat_less_rel then 
33192  258 
("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0) 
259 
(int_for_bool o op <)) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

260 
else if x = int_less_rel then 
33192  261 
("int_less", tabulate_int_op2 debug univ_card (int_card, j0) 
262 
(int_for_bool o op <)) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

263 
else if x = gcd_rel then 
33192  264 
("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

265 
else if x = lcm_rel then 
33192  266 
("lcm", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_lcm) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

267 
else if x = norm_frac_rel then 
33192  268 
("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0) 
269 
isa_norm_frac) 

270 
else 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

271 
raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation")) 
33192  272 

34126  273 
(* bool > int > int > int > int > int * int > KK.rel_expr > KK.bound *) 
33192  274 
fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x = 
275 
let 

276 
val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card 

277 
j0 x 

34126  278 
in ([(x, nick)], [KK.TupleSet ts]) end 
33192  279 

34126  280 
(* bool > int > int > int > int > KK.formula > KK.bound list *) 
33192  281 
fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 = 
282 
map (bound_for_built_in_rel debug univ_card nat_card int_card j0) 

283 
o built_in_rels_in_formula 

284 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

285 
(* Proof.context > bool > string > typ > rep > string *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

286 
fun bound_comment ctxt debug nick T R = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

287 
short_name nick ^ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

288 
(if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

289 
else "") ^ " : " ^ string_for_rep R 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

290 

34126  291 
(* Proof.context > bool > nut > KK.bound *) 
33192  292 
fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) = 
293 
([(x, bound_comment ctxt debug nick T R)], 

294 
if nick = @{const_name bisim_iterator_max} then 

295 
case R of 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

296 
Atom (k, j0) => [single_atom (k  1 + j0)] 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

297 
 _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) 
33192  298 
else 
34126  299 
[KK.TupleSet [], upper_bound_for_rep R]) 
33192  300 
 bound_for_plain_rel _ _ u = 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

301 
raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) 
33192  302 

34126  303 
(* Proof.context > bool > dtype_spec list > nut > KK.bound *) 
33192  304 
fun bound_for_sel_rel ctxt debug dtypes 
305 
(FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2), 

306 
nick)) = 

307 
let 

308 
val constr as {delta, epsilon, exclusive, explicit_max, ...} = 

309 
constr_spec dtypes (original_name nick, T1) 

310 
in 

311 
([(x, bound_comment ctxt debug nick T R)], 

312 
if explicit_max = 0 then 

34126  313 
[KK.TupleSet []] 
33192  314 
else 
34126  315 
let val ts = KK.TupleAtomSeq (epsilon  delta, delta + j0) in 
33192  316 
if R2 = Formula Neut then 
34126  317 
[ts] > not exclusive ? cons (KK.TupleSet []) 
33192  318 
else 
34126  319 
[KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)] 
33192  320 
end) 
321 
end 

322 
 bound_for_sel_rel _ _ _ u = 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

323 
raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u]) 
33192  324 

34126  325 
(* KK.bound list > KK.bound list *) 
33192  326 
fun merge_bounds bs = 
327 
let 

34126  328 
(* KK.bound > int *) 
33192  329 
fun arity (zs, _) = fst (fst (hd zs)) 
34126  330 
(* KK.bound list > KK.bound > KK.bound list > KK.bound list *) 
33192  331 
fun add_bound ds b [] = List.revAppend (ds, [b]) 
332 
 add_bound ds b (c :: cs) = 

333 
if arity b = arity c andalso snd b = snd c then 

334 
List.revAppend (ds, (fst c @ fst b, snd c) :: cs) 

335 
else 

336 
add_bound (c :: ds) b cs 

337 
in fold (add_bound []) bs [] end 

338 

34126  339 
(* int > int > KK.rel_expr list *) 
340 
fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n) 

33192  341 

34126  342 
(* int list > KK.rel_expr *) 
343 
val singleton_from_combination = foldl1 KK.Product o map KK.Atom 

344 
(* rep > KK.rel_expr list *) 

33192  345 
fun all_singletons_for_rep R = 
346 
if is_lone_rep R then 

347 
all_combinations_for_rep R > map singleton_from_combination 

348 
else 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

349 
raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R]) 
33192  350 

34126  351 
(* KK.rel_expr > KK.rel_expr list *) 
352 
fun unpack_products (KK.Product (r1, r2)) = 

33192  353 
unpack_products r1 @ unpack_products r2 
354 
 unpack_products r = [r] 

34126  355 
fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2 
33192  356 
 unpack_joins r = [r] 
357 

34126  358 
(* rep > KK.rel_expr *) 
33192  359 
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep 
360 
fun full_rel_for_rep R = 

361 
case atom_schema_of_rep R of 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

362 
[] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R]) 
34126  363 
 schema => foldl1 KK.Product (map KK.AtomSeq schema) 
33192  364 

34126  365 
(* int > int list > KK.decl list *) 
33192  366 
fun decls_for_atom_schema j0 schema = 
34126  367 
map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x)) 
33192  368 
(index_seq j0 (length schema)) schema 
369 

370 
(* The type constraint below is a workaround for a Poly/ML bug. *) 

371 

34126  372 
(* kodkod_constrs > rep > KK.rel_expr > KK.formula *) 
33192  373 
fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs) 
374 
R r = 

375 
let val body_R = body_rep R in 

376 
if is_lone_rep body_R then 

377 
let 

378 
val binder_schema = atom_schema_of_reps (binder_reps R) 

379 
val body_schema = atom_schema_of_rep body_R 

380 
val one = is_one_rep body_R 

34126  381 
val opt_x = case r of KK.Rel x => SOME x  _ => NONE 
33192  382 
in 
383 
if opt_x <> NONE andalso length binder_schema = 1 

384 
andalso length body_schema = 1 then 

34126  385 
(if one then KK.Function else KK.Functional) 
386 
(the opt_x, KK.AtomSeq (hd binder_schema), 

387 
KK.AtomSeq (hd body_schema)) 

33192  388 
else 
389 
let 

390 
val decls = decls_for_atom_schema ~1 binder_schema 

391 
val vars = unary_var_seq ~1 (length binder_schema) 

392 
val kk_xone = if one then kk_one else kk_lone 

393 
in kk_all decls (kk_xone (fold kk_join vars r)) end 

394 
end 

395 
else 

34126  396 
KK.True 
33192  397 
end 
34126  398 
fun kk_n_ary_function kk R (r as KK.Rel x) = 
33192  399 
if not (is_opt_rep R) then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

400 
if x = suc_rel then 
34126  401 
KK.False 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

402 
else if x = nat_add_rel then 
33192  403 
formula_for_bool (card_of_rep (body_rep R) = 1) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

404 
else if x = nat_multiply_rel then 
33192  405 
formula_for_bool (card_of_rep (body_rep R) <= 2) 
406 
else 

407 
d_n_ary_function kk R r 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

408 
else if x = nat_subtract_rel then 
34126  409 
KK.True 
33192  410 
else 
411 
d_n_ary_function kk R r 

412 
 kk_n_ary_function kk R r = d_n_ary_function kk R r 

413 

34126  414 
(* kodkod_constrs > KK.rel_expr list > KK.formula *) 
415 
fun kk_disjoint_sets _ [] = KK.True 

33192  416 
 kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs) 
417 
(r :: rs) = 

418 
fold (kk_and o kk_no o kk_intersect r) rs (kk_disjoint_sets kk rs) 

419 

34126  420 
(* int > kodkod_constrs > (KK.rel_expr > KK.rel_expr) > KK.rel_expr 
421 
> KK.rel_expr *) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

422 
fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r = 
33192  423 
if inline_rel_expr r then 
424 
f r 

425 
else 

34126  426 
let val x = (KK.arity_of_rel_expr r, j) in 
427 
kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x)) 

33192  428 
end 
34126  429 
(* kodkod_constrs > (KK.rel_expr > KK.rel_expr) > KK.rel_expr 
430 
> KK.rel_expr *) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

431 
val single_rel_rel_let = basic_rel_rel_let 0 
34126  432 
(* kodkod_constrs > (KK.rel_expr > KK.rel_expr > KK.rel_expr) > KK.rel_expr 
433 
> KK.rel_expr > KK.rel_expr *) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

434 
fun double_rel_rel_let kk f r1 r2 = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

435 
single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1 
34126  436 
(* kodkod_constrs > (KK.rel_expr > KK.rel_expr > KK.rel_expr > KK.rel_expr) 
437 
> KK.rel_expr > KK.rel_expr > KK.rel_expr > KK.rel_expr *) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

438 
fun tripl_rel_rel_let kk f r1 r2 r3 = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

439 
double_rel_rel_let kk 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

440 
(fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2 
33192  441 

34126  442 
(* kodkod_constrs > int > KK.formula > KK.rel_expr *) 
33192  443 
fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f = 
34126  444 
kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0) 
445 
(* kodkod_constrs > rep > KK.formula > KK.rel_expr *) 

33192  446 
fun rel_expr_from_formula kk R f = 
447 
case unopt_rep R of 

448 
Atom (2, j0) => atom_from_formula kk j0 f 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

449 
 _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R]) 
33192  450 

34126  451 
(* kodkod_cotrs > int > int > KK.rel_expr > KK.rel_expr list *) 
33192  452 
fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity 
453 
num_chunks r = 

454 
List.tabulate (num_chunks, fn j => kk_project_seq r (j * chunk_arity) 

455 
chunk_arity) 

456 

34126  457 
(* kodkod_constrs > bool > rep > rep > KK.rel_expr > KK.rel_expr 
458 
> KK.rel_expr *) 

33192  459 
fun kk_n_fold_join 
460 
(kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1 

461 
res_R r1 r2 = 

462 
case arity_of_rep R1 of 

463 
1 => kk_join r1 r2 

464 
 arity1 => 

465 
let 

466 
val unpacked_rs1 = 

467 
if inline_rel_expr r1 then unpack_vect_in_chunks kk 1 arity1 r1 

468 
else unpack_products r1 

469 
in 

470 
if one andalso length unpacked_rs1 = arity1 then 

471 
fold kk_join unpacked_rs1 r2 

472 
else 

473 
kk_project_seq 

474 
(kk_intersect (kk_product r1 (full_rel_for_rep res_R)) r2) 

475 
arity1 (arity_of_rep res_R) 

476 
end 

477 

34126  478 
(* kodkod_constrs > rep > rep > KK.rel_expr > KK.rel_expr list 
479 
> KK.rel_expr list > KK.rel_expr *) 

33192  480 
fun kk_case_switch (kk as {kk_union, kk_product, ...}) R1 R2 r rs1 rs2 = 
481 
if rs1 = rs2 then r 

482 
else kk_n_fold_join kk true R1 R2 r (fold1 kk_union (map2 kk_product rs1 rs2)) 

483 

484 
val lone_rep_fallback_max_card = 4096 

485 
val some_j0 = 0 

486 

34126  487 
(* kodkod_constrs > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  488 
fun lone_rep_fallback kk new_R old_R r = 
489 
if old_R = new_R then 

490 
r 

491 
else 

492 
let val card = card_of_rep old_R in 

493 
if is_lone_rep old_R andalso is_lone_rep new_R 

494 
andalso card = card_of_rep new_R then 

495 
if card >= lone_rep_fallback_max_card then 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

496 
raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback", 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

497 
"too high cardinality (" ^ string_of_int card ^ ")") 
33192  498 
else 
499 
kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R) 

500 
(all_singletons_for_rep new_R) 

501 
else 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

502 
raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R]) 
33192  503 
end 
34126  504 
(* kodkod_constrs > int * int > rep > KK.rel_expr > KK.rel_expr *) 
33192  505 
and atom_from_rel_expr kk (x as (k, j0)) old_R r = 
506 
case old_R of 

507 
Func (R1, R2) => 

508 
let 

509 
val dom_card = card_of_rep R1 

510 
val R2' = case R2 of Atom _ => R2  _ => Atom (card_of_rep R2, some_j0) 

511 
in 

512 
atom_from_rel_expr kk x (Vect (dom_card, R2')) 

513 
(vect_from_rel_expr kk dom_card R2' old_R r) 

514 
end 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

515 
 Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R]) 
33192  516 
 _ => lone_rep_fallback kk (Atom x) old_R r 
34126  517 
(* kodkod_constrs > rep list > rep > KK.rel_expr > KK.rel_expr *) 
33192  518 
and struct_from_rel_expr kk Rs old_R r = 
519 
case old_R of 

520 
Atom _ => lone_rep_fallback kk (Struct Rs) old_R r 

521 
 Struct Rs' => 

522 
let 

523 
val Rs = filter (not_equal Unit) Rs 

524 
val Rs' = filter (not_equal Unit) Rs' 

525 
in 

526 
if Rs' = Rs then 

527 
r 

528 
else if map card_of_rep Rs' = map card_of_rep Rs then 

529 
let 

530 
val old_arities = map arity_of_rep Rs' 

531 
val old_offsets = offset_list old_arities 

532 
val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities 

533 
in 

534 
fold1 (#kk_product kk) 

535 
(map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs) 

536 
end 

537 
else 

538 
lone_rep_fallback kk (Struct Rs) old_R r 

539 
end 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

540 
 _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R]) 
34126  541 
(* kodkod_constrs > int > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  542 
and vect_from_rel_expr kk k R old_R r = 
543 
case old_R of 

544 
Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r 

545 
 Vect (k', R') => 

546 
if k = k' andalso R = R' then r 

547 
else lone_rep_fallback kk (Vect (k, R)) old_R r 

548 
 Func (R1, Formula Neut) => 

549 
if k = card_of_rep R1 then 

550 
fold1 (#kk_product kk) 

551 
(map (fn arg_r => 

552 
rel_expr_from_formula kk R (#kk_subset kk arg_r r)) 

553 
(all_singletons_for_rep R1)) 

554 
else 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

555 
raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
33192  556 
 Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r 
557 
 Func (R1, R2) => 

558 
fold1 (#kk_product kk) 

559 
(map (fn arg_r => 

560 
rel_expr_from_rel_expr kk R R2 

561 
(kk_n_fold_join kk true R1 R2 arg_r r)) 

562 
(all_singletons_for_rep R1)) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

563 
 _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
34126  564 
(* kodkod_constrs > rep > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  565 
and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r = 
566 
let 

567 
val dom_card = card_of_rep R1 

568 
val R2' = case R2 of Atom _ => R2  _ => Atom (card_of_rep R2, some_j0) 

569 
in 

570 
func_from_no_opt_rel_expr kk R1 R2 (Vect (dom_card, R2')) 

571 
(vect_from_rel_expr kk dom_card R2' (Atom x) r) 

572 
end 

573 
 func_from_no_opt_rel_expr kk Unit R2 old_R r = 

574 
(case old_R of 

575 
Vect (k, R') => rel_expr_from_rel_expr kk R2 R' r 

576 
 Func (Unit, R2') => rel_expr_from_rel_expr kk R2 R2' r 

577 
 Func (Atom (1, _), Formula Neut) => 

578 
(case unopt_rep R2 of 

579 
Atom (2, j0) => atom_from_formula kk j0 (#kk_some kk r) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

580 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  581 
[old_R, Func (Unit, R2)])) 
582 
 Func (R1', R2') => 

583 
rel_expr_from_rel_expr kk R2 R2' (#kk_project_seq kk r (arity_of_rep R1') 

584 
(arity_of_rep R2')) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

585 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  586 
[old_R, Func (Unit, R2)])) 
587 
 func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r = 

588 
(case old_R of 

589 
Vect (k, Atom (2, j0)) => 

590 
let 

591 
val args_rs = all_singletons_for_rep R1 

592 
val vals_rs = unpack_vect_in_chunks kk 1 k r 

34126  593 
(* KK.rel_expr > KK.rel_expr > KK.rel_expr *) 
33192  594 
fun empty_or_singleton_set_for arg_r val_r = 
34126  595 
#kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r) 
33192  596 
in 
597 
fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs) 

598 
end 

599 
 Func (R1', Formula Neut) => 

600 
if R1 = R1' then 

601 
r 

602 
else 

603 
let 

604 
val schema = atom_schema_of_rep R1 

605 
val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema)) 

606 
> rel_expr_from_rel_expr kk R1' R1 

33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

607 
val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk 
33192  608 
in 
33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

609 
#kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) 
33192  610 
end 
611 
 Func (Unit, (Atom (2, j0))) => 

34126  612 
#kk_rel_if kk (#kk_rel_eq kk r (KK.Atom (j0 + 1))) 
33192  613 
(full_rel_for_rep R1) (empty_rel_for_rep R1) 
614 
 Func (R1', Atom (2, j0)) => 

615 
func_from_no_opt_rel_expr kk R1 (Formula Neut) 

34126  616 
(Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1))) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

617 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  618 
[old_R, Func (R1, Formula Neut)])) 
619 
 func_from_no_opt_rel_expr kk R1 R2 old_R r = 

620 
case old_R of 

621 
Vect (k, R) => 

622 
let 

623 
val args_rs = all_singletons_for_rep R1 

624 
val vals_rs = unpack_vect_in_chunks kk (arity_of_rep R) k r 

625 
> map (rel_expr_from_rel_expr kk R2 R) 

626 
in fold1 (#kk_union kk) (map2 (#kk_product kk) args_rs vals_rs) end 

627 
 Func (R1', Formula Neut) => 

628 
(case R2 of 

629 
Atom (x as (2, j0)) => 

630 
let val schema = atom_schema_of_rep R1 in 

631 
if length schema = 1 then 

34126  632 
#kk_override kk (#kk_product kk (KK.AtomSeq (hd schema)) 
633 
(KK.Atom j0)) 

634 
(#kk_product kk r (KK.Atom (j0 + 1))) 

33192  635 
else 
636 
let 

637 
val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema)) 

638 
> rel_expr_from_rel_expr kk R1' R1 

34126  639 
val r2 = KK.Var (1, ~(length schema)  1) 
33192  640 
val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r) 
641 
in 

642 
#kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x])) 

33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

643 
(#kk_subset kk r2 r3) 
33192  644 
end 
645 
end 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

646 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  647 
[old_R, Func (R1, R2)])) 
648 
 Func (Unit, R2') => 

649 
let val j0 = some_j0 in 

650 
func_from_no_opt_rel_expr kk R1 R2 (Func (Atom (1, j0), R2')) 

34126  651 
(#kk_product kk (KK.Atom j0) r) 
33192  652 
end 
653 
 Func (R1', R2') => 

654 
if R1 = R1' andalso R2 = R2' then 

655 
r 

656 
else 

657 
let 

658 
val dom_schema = atom_schema_of_rep R1 

659 
val ran_schema = atom_schema_of_rep R2 

660 
val dom_prod = fold1 (#kk_product kk) 

661 
(unary_var_seq ~1 (length dom_schema)) 

662 
> rel_expr_from_rel_expr kk R1' R1 

663 
val ran_prod = fold1 (#kk_product kk) 

664 
(unary_var_seq (~(length dom_schema)  1) 

665 
(length ran_schema)) 

666 
> rel_expr_from_rel_expr kk R2' R2 

667 
val app = kk_n_fold_join kk true R1' R2' dom_prod r 

33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

668 
val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk 
33192  669 
in 
670 
#kk_comprehension kk (decls_for_atom_schema ~1 

671 
(dom_schema @ ran_schema)) 

33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

672 
(kk_xeq ran_prod app) 
33192  673 
end 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

674 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  675 
[old_R, Func (R1, R2)]) 
34126  676 
(* kodkod_constrs > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  677 
and rel_expr_from_rel_expr kk new_R old_R r = 
678 
let 

679 
val unopt_old_R = unopt_rep old_R 

680 
val unopt_new_R = unopt_rep new_R 

681 
in 

682 
if unopt_old_R <> old_R andalso unopt_new_R = new_R then 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

683 
raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R]) 
33192  684 
else if unopt_new_R = unopt_old_R then 
685 
r 

686 
else 

687 
(case unopt_new_R of 

688 
Atom x => atom_from_rel_expr kk x 

689 
 Struct Rs => struct_from_rel_expr kk Rs 

690 
 Vect (k, R') => vect_from_rel_expr kk k R' 

691 
 Func (R1, R2) => func_from_no_opt_rel_expr kk R1 R2 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

692 
 _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", 
33192  693 
[old_R, new_R])) 
694 
unopt_old_R r 

695 
end 

34126  696 
(* kodkod_constrs > rep > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  697 
and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2)) 
698 

34126  699 
(* kodkod_constrs > typ > KK.rel_expr > KK.rel_expr *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

700 
fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r = 
34126  701 
kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then 
702 
unsigned_bit_word_sel_rel 

703 
else 

704 
signed_bit_word_sel_rel)) 

705 
(* kodkod_constrs > typ > KK.rel_expr > KK.int_expr *) 

706 
val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom 

707 
(* kodkod_constrs > typ > rep > KK.int_expr > KK.rel_expr *) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

708 
fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...} 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

709 
: kodkod_constrs) T R i = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

710 
kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R)) 
34126  711 
(kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1))) 
712 
(KK.Bits i)) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

713 

34126  714 
(* kodkod_constrs > nut > KK.formula *) 
33192  715 
fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) = 
716 
kk_n_ary_function kk (R > nick = @{const_name List.set} ? unopt_rep) 

34126  717 
(KK.Rel x) 
33192  718 
 declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs) 
719 
(FreeRel (x, _, R, _)) = 

34126  720 
if is_one_rep R then kk_one (KK.Rel x) 
721 
else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x) 

722 
else KK.True 

33192  723 
 declarative_axiom_for_plain_rel _ u = 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

724 
raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u]) 
33192  725 

34126  726 
(* nut NameTable.table > styp > KK.rel_expr * rep * int *) 
33192  727 
fun const_triple rel_table (x as (s, T)) = 
728 
case the_name rel_table (ConstName (s, T, Any)) of 

34126  729 
FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

730 
 _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x]) 
33192  731 

34126  732 
(* nut NameTable.table > styp > KK.rel_expr *) 
33192  733 
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr 
734 

735 
(* extended_context > kodkod_constrs > nut NameTable.table > dtype_spec list 

736 
> styp > int > nfa_transition list *) 

737 
fun nfa_transitions_for_sel ext_ctxt ({kk_project, ...} : kodkod_constrs) 

738 
rel_table (dtypes : dtype_spec list) constr_x n = 

739 
let 

740 
val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt constr_x n 

741 
val (r, R, arity) = const_triple rel_table x 

742 
val type_schema = type_schema_of_rep T R 

743 
in 

744 
map_filter (fn (j, T) => 

745 
if forall (not_equal T o #typ) dtypes then NONE 

34126  746 
else SOME (kk_project r (map KK.Num [0, j]), T)) 
33192  747 
(index_seq 1 (arity  1) ~~ tl type_schema) 
748 
end 

749 
(* extended_context > kodkod_constrs > nut NameTable.table > dtype_spec list 

750 
> styp > nfa_transition list *) 

751 
fun nfa_transitions_for_constr ext_ctxt kk rel_table dtypes (x as (_, T)) = 

752 
maps (nfa_transitions_for_sel ext_ctxt kk rel_table dtypes x) 

753 
(index_seq 0 (num_sels_for_constr_type T)) 

754 
(* extended_context > kodkod_constrs > nut NameTable.table > dtype_spec list 

755 
> dtype_spec > nfa_entry option *) 

756 
fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE 

33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

757 
 nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

758 
 nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} = 
33192  759 
SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes 
760 
o #const) constrs) 

761 

34126  762 
val empty_rel = KK.Product (KK.None, KK.None) 
33192  763 

34126  764 
(* nfa_table > typ > typ > KK.rel_expr list *) 
33192  765 
fun direct_path_rel_exprs nfa start final = 
766 
case AList.lookup (op =) nfa final of 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

767 
SOME trans => map fst (filter (curry (op =) start o snd) trans) 
33192  768 
 NONE => [] 
34126  769 
(* kodkod_constrs > nfa_table > typ list > typ > typ > KK.rel_expr *) 
33192  770 
and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final = 
771 
fold kk_union (direct_path_rel_exprs nfa start final) 

34126  772 
(if start = final then KK.Iden else empty_rel) 
33192  773 
 any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final = 
774 
kk_union (any_path_rel_expr kk nfa qs start final) 

775 
(knot_path_rel_expr kk nfa qs start q final) 

776 
(* kodkod_constrs > nfa_table > typ list > typ > typ > typ 

34126  777 
> KK.rel_expr *) 
33192  778 
and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start 
779 
knot final = 

780 
kk_join (kk_join (any_path_rel_expr kk nfa qs knot final) 

781 
(kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot))) 

782 
(any_path_rel_expr kk nfa qs start knot) 

34126  783 
(* kodkod_constrs > nfa_table > typ list > typ > KK.rel_expr *) 
33192  784 
and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start = 
785 
fold kk_union (direct_path_rel_exprs nfa start start) empty_rel 

786 
 loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start = 

787 
if start = q then 

788 
kk_closure (loop_path_rel_expr kk nfa qs start) 

789 
else 

790 
kk_union (loop_path_rel_expr kk nfa qs start) 

791 
(knot_path_rel_expr kk nfa qs start q start) 

792 

793 
(* nfa_table > unit NfaGraph.T *) 

794 
fun graph_for_nfa nfa = 

795 
let 

796 
(* typ > unit NfaGraph.T > unit NfaGraph.T *) 

797 
fun new_node q = perhaps (try (NfaGraph.new_node (q, ()))) 

798 
(* nfa_table > unit NfaGraph.T > unit NfaGraph.T *) 

799 
fun add_nfa [] = I 

800 
 add_nfa ((_, []) :: nfa) = add_nfa nfa 

801 
 add_nfa ((q, ((_, q') :: transitions)) :: nfa) = 

802 
add_nfa ((q, transitions) :: nfa) o NfaGraph.add_edge (q, q') o 

803 
new_node q' o new_node q 

804 
in add_nfa nfa NfaGraph.empty end 

805 

806 
(* nfa_table > nfa_table list *) 

807 
fun strongly_connected_sub_nfas nfa = 

808 
nfa > graph_for_nfa > NfaGraph.strong_conn 

809 
> map (fn keys => filter (member (op =) keys o fst) nfa) 

810 

34126  811 
(* dtype_spec list > kodkod_constrs > nfa_table > typ > KK.formula *) 
33192  812 
fun acyclicity_axiom_for_datatype dtypes kk nfa start = 
813 
#kk_no kk (#kk_intersect kk 

34126  814 
(loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden) 
33192  815 
(* extended_context > kodkod_constrs > nut NameTable.table > dtype_spec list 
34126  816 
> KK.formula list *) 
33192  817 
fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes = 
818 
map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes 

819 
> strongly_connected_sub_nfas 

820 
> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst) 

821 
nfa) 

822 

823 
(* extended_context > int > kodkod_constrs > nut NameTable.table 

34126  824 
> KK.rel_expr > constr_spec > int > KK.formula *) 
33192  825 
fun sel_axiom_for_sel ext_ctxt j0 
826 
(kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no, 

33982  827 
kk_join, ...}) rel_table dom_r 
33192  828 
({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec) 
829 
n = 

830 
let 

831 
val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt const n 

832 
val (r, R, arity) = const_triple rel_table x 

833 
val R2 = dest_Func R > snd 

834 
val z = (epsilon  delta, delta + j0) 

835 
in 

836 
if exclusive then 

837 
kk_n_ary_function kk (Func (Atom z, R2)) r 

838 
else 

34126  839 
let val r' = kk_join (KK.Var (1, 0)) r in 
840 
kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)] 

841 
(kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r) 

842 
(kk_n_ary_function kk R2 r') (kk_no r')) 

33192  843 
end 
844 
end 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

845 
(* extended_context > int > int > kodkod_constrs > nut NameTable.table 
34126  846 
> constr_spec > KK.formula list *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

847 
fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table 
33192  848 
(constr as {const, delta, epsilon, explicit_max, ...}) = 
849 
let 

850 
val honors_explicit_max = 

851 
explicit_max < 0 orelse epsilon  delta <= explicit_max 

852 
in 

853 
if explicit_max = 0 then 

854 
[formula_for_bool honors_explicit_max] 

855 
else 

856 
let 

857 
val ran_r = discr_rel_expr rel_table const 

858 
val max_axiom = 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

859 
if honors_explicit_max then 
34126  860 
KK.True 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

861 
else if is_twos_complement_representable bits (epsilon  delta) then 
34126  862 
KK.LE (KK.Cardinality ran_r, KK.Num explicit_max) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

863 
else 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

864 
raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr", 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

865 
"\"bits\" value " ^ string_of_int bits ^ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

866 
" too small for \"max\"") 
33192  867 
in 
868 
max_axiom :: 

869 
map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr) 

870 
(index_seq 0 (num_sels_for_constr_type (snd const))) 

871 
end 

872 
end 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

873 
(* extended_context > int > int > kodkod_constrs > nut NameTable.table 
34126  874 
> dtype_spec > KK.formula list *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

875 
fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table 
33192  876 
({constrs, ...} : dtype_spec) = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

877 
maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs 
33192  878 

879 
(* extended_context > kodkod_constrs > nut NameTable.table > constr_spec 

34126  880 
> KK.formula list *) 
33192  881 
fun uniqueness_axiom_for_constr ext_ctxt 
882 
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} 

883 
: kodkod_constrs) rel_table ({const, ...} : constr_spec) = 

884 
let 

34126  885 
(* KK.rel_expr > KK.formula *) 
33192  886 
fun conjunct_for_sel r = 
34126  887 
kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r) 
33192  888 
val num_sels = num_sels_for_constr_type (snd const) 
889 
val triples = map (const_triple rel_table 

890 
o boxed_nth_sel_for_constr ext_ctxt const) 

891 
(~1 upto num_sels  1) 

892 
val j0 = case triples > hd > #2 of 

893 
Func (Atom (_, j0), _) => j0 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

894 
 R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr", 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

895 
[R]) 
33192  896 
val set_r = triples > hd > #1 
897 
in 

898 
if num_sels = 0 then 

899 
kk_lone set_r 

900 
else 

34126  901 
kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1]) 
33192  902 
(kk_implies 
903 
(fold1 kk_and (map (conjunct_for_sel o #1) (tl triples))) 

34126  904 
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1)))) 
33192  905 
end 
906 
(* extended_context > kodkod_constrs > nut NameTable.table > dtype_spec 

34126  907 
> KK.formula list *) 
33192  908 
fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table 
909 
({constrs, ...} : dtype_spec) = 

910 
map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs 

911 

912 
(* constr_spec > int *) 

913 
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon  delta 

914 
(* int > kodkod_constrs > nut NameTable.table > dtype_spec 

34126  915 
> KK.formula list *) 
33192  916 
fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...}) 
917 
rel_table 

918 
({card, constrs, ...} : dtype_spec) = 

919 
if forall #exclusive constrs then 

920 
[Integer.sum (map effective_constr_max constrs) = card > formula_for_bool] 

921 
else 

922 
let val rs = map (discr_rel_expr rel_table o #const) constrs in 

34126  923 
[kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)), 
33192  924 
kk_disjoint_sets kk rs] 
925 
end 

926 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

927 
(* extended_context > int > int Typtab.table > kodkod_constrs 
34126  928 
> nut NameTable.table > dtype_spec > KK.formula list *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

929 
fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = [] 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

930 
 other_axioms_for_datatype ext_ctxt bits ofs kk rel_table 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

931 
(dtype as {typ, ...}) = 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

932 
let val j0 = offset_of_type ofs typ in 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

933 
sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @ 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

934 
uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @ 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

935 
partition_axioms_for_datatype j0 kk rel_table dtype 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

936 
end 
33192  937 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

938 
(* extended_context > int > int Typtab.table > kodkod_constrs 
34126  939 
> nut NameTable.table > dtype_spec list > KK.formula list *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

940 
fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes = 
33192  941 
acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @ 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

942 
maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes 
33192  943 

34126  944 
(* int > int Typtab.table > bool > kodkod_constrs > nut > KK.formula *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

945 
fun kodkod_formula_from_nut bits ofs liberal 
33192  946 
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not, 
947 
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one, 

948 
kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference, 

949 
kk_intersect, kk_product, kk_join, kk_closure, kk_comprehension, 

950 
kk_project, kk_project_seq, kk_not3, kk_nat_less, kk_int_less, 

951 
...}) u = 

952 
let 

953 
val main_j0 = offset_of_type ofs bool_T 

954 
val bool_j0 = main_j0 

955 
val bool_atom_R = Atom (2, main_j0) 

34126  956 
val false_atom = KK.Atom bool_j0 
957 
val true_atom = KK.Atom (bool_j0 + 1) 

33192  958 

34126  959 
(* polarity > int > KK.rel_expr > KK.formula *) 
33192  960 
fun formula_from_opt_atom polar j0 r = 
961 
case polar of 

34126  962 
Neg => kk_not (kk_rel_eq r (KK.Atom j0)) 
963 
 _ => kk_rel_eq r (KK.Atom (j0 + 1)) 

964 
(* int > KK.rel_expr > KK.formula *) 

33192  965 
val formula_from_atom = formula_from_opt_atom Pos 
966 

34126  967 
(* KK.formula > KK.formula > KK.formula *) 
33192  968 
fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2) 
34126  969 
(* KK.rel_expr > KK.rel_expr > KK.rel_expr *) 
33192  970 
val kk_or3 = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

971 
double_rel_rel_let kk 
33192  972 
(fn r1 => fn r2 => 
973 
kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom 

974 
(kk_intersect r1 r2)) 

975 
val kk_and3 = 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

976 
double_rel_rel_let kk 
33192  977 
(fn r1 => fn r2 => 
978 
kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom 

979 
(kk_intersect r1 r2)) 

980 
fun kk_notimplies3 r1 r2 = kk_and3 r1 (kk_not3 r2) 

981 

34126  982 
(* int > KK.rel_expr > KK.formula list *) 
33192  983 
val unpack_formulas = 
984 
map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1 

34126  985 
(* (KK.formula > KK.formula > KK.formula) > int > KK.rel_expr 
986 
> KK.rel_expr > KK.rel_expr *) 

33192  987 
fun kk_vect_set_op connective k r1 r2 = 
988 
fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective) 

989 
(unpack_formulas k r1) (unpack_formulas k r2)) 

34126  990 
(* (KK.formula > KK.formula > KK.formula) > int > KK.rel_expr 
991 
> KK.rel_expr > KK.formula *) 

33192  992 
fun kk_vect_set_bool_op connective k r1 r2 = 
993 
fold1 kk_and (map2 connective (unpack_formulas k r1) 

994 
(unpack_formulas k r2)) 

995 

34126  996 
(* nut > KK.formula *) 
33192  997 
fun to_f u = 
998 
case rep_of u of 

999 
Formula polar => 

1000 
(case u of 

34126  1001 
Cst (False, _, _) => KK.False 
1002 
 Cst (True, _, _) => KK.True 

33854
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1003 
 Op1 (Not, _, _, u1) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1004 
kk_not (to_f_with_polarity (flip_polarity polar) u1) 
33192  1005 
 Op1 (Finite, _, _, u1) => 
1006 
let val opt1 = is_opt_rep (rep_of u1) in 

1007 
case polar of 

1008 
Neut => if opt1 then 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1009 
raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) 
33192  1010 
else 
34126  1011 
KK.True 
33192  1012 
 Pos => formula_for_bool (not opt1) 
34126  1013 
 Neg => KK.True 
33192  1014 
end 
1015 
 Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1 

33854
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1016 
 Op2 (All, _, _, u1, u2) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1017 
kk_all (untuple to_decl u1) (to_f_with_polarity polar u2) 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1018 
 Op2 (Exist, _, _, u1, u2) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1019 
kk_exist (untuple to_decl u1) (to_f_with_polarity polar u2) 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1020 
 Op2 (Or, _, _, u1, u2) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1021 
kk_or (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1022 
 Op2 (And, _, _, u1, u2) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1023 
kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
33192  1024 
 Op2 (Less, T, Formula polar, u1, u2) => 
1025 
formula_from_opt_atom polar bool_j0 

1026 
(to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2))) 

1027 
 Op2 (Subset, _, _, u1, u2) => 

1028 
let 

1029 
val dom_T = domain_type (type_of u1) 

1030 
val R1 = rep_of u1 

1031 
val R2 = rep_of u2 

1032 
val (dom_R, ran_R) = 

1033 
case min_rep R1 R2 of 

1034 
Func (Unit, R') => 

1035 
(Atom (1, offset_of_type ofs dom_T), R') 

1036 
 Func Rp => Rp 

1037 
 R => (Atom (card_of_domain_from_rep 2 R, 

1038 
offset_of_type ofs dom_T), 

1039 
if is_opt_rep R then Opt bool_atom_R else Formula Neut) 

1040 
val set_R = Func (dom_R, ran_R) 

1041 
in 

1042 
if not (is_opt_rep ran_R) then 

1043 
to_set_bool_op kk_implies kk_subset u1 u2 

1044 
else if polar = Neut then 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1045 
raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u]) 
33192  1046 
else 
1047 
let 

33886
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

1048 
(* FIXME: merge with similar code below *) 
34126  1049 
(* bool > nut > KK.rel_expr *) 
33192  1050 
fun set_to_r widen u = 
1051 
if widen then 

1052 
kk_difference (full_rel_for_rep dom_R) 

1053 
(kk_join (to_rep set_R u) false_atom) 

1054 
else 

1055 
kk_join (to_rep set_R u) true_atom 

1056 
val widen1 = (polar = Pos andalso is_opt_rep R1) 

1057 
val widen2 = (polar = Neg andalso is_opt_rep R2) 

1058 
in kk_subset (set_to_r widen1 u1) (set_to_r widen2 u2) end 

1059 
end 

1060 
 Op2 (DefEq, _, _, u1, u2) => 

1061 
(case min_rep (rep_of u1) (rep_of u2) of 

34126  1062 
Unit => KK.True 
33192  1063 
 Formula polar => 
1064 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 

1065 
 min_R => 

1066 
let 

1067 
(* nut > nut list *) 

1068 
fun args (Op2 (Apply, _, _, u1, u2)) = u2 :: args u1 

1069 
 args (Tuple (_, _, us)) = us 

1070 
 args _ = [] 

1071 
val opt_arg_us = filter (is_opt_rep o rep_of) (args u1) 

1072 
in 

1073 
if null opt_arg_us orelse not (is_Opt min_R) 

1074 
orelse is_eval_name u1 then 

1075 
fold (kk_or o (kk_no o to_r)) opt_arg_us 

1076 
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)) 

1077 
else 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

1078 
kk_subset (to_rep min_R u1) (to_rep min_R u2) 
33192  1079 
end) 
1080 
 Op2 (Eq, T, R, u1, u2) => 

1081 
(case min_rep (rep_of u1) (rep_of u2) of 

34126  1082 
Unit => KK.True 
33192  1083 
 Formula polar => 
1084 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 

1085 
 min_R => 

1086 
if is_opt_rep min_R then 

1087 
if polar = Neut then 

1088 
(* continuation of hackish optimization *) 

1089 
kk_rel_eq (to_rep min_R u1) (to_rep min_R u2) 

1090 
else if is_Cst Unrep u1 then 

1091 
to_could_be_unrep (polar = Neg) u2 

1092 
else if is_Cst Unrep u2 then 

1093 
to_could_be_unrep (polar = Neg) u1 

1094 
else 

1095 
let 

1096 
val r1 = to_rep min_R u1 

1097 
val r2 = to_rep min_R u2 

1098 
val both_opt = forall (is_opt_rep o rep_of) [u1, u2] 

1099 
in 

1100 
(if polar = Pos then 

1101 
if not both_opt then 

1102 
kk_rel_eq r1 r2 

1103 
else if is_lone_rep min_R 

1104 
andalso arity_of_rep min_R = 1 then 

1105 
kk_some (kk_intersect r1 r2) 

1106 
else 

1107 
raise SAME () 

1108 
else 

1109 
if is_lone_rep min_R then 

1110 
if arity_of_rep min_R = 1 then 

34126  1111 
kk_subset (kk_product r1 r2) KK.Iden 
33192  1112 
else if not both_opt then 
1113 
(r1, r2) > is_opt_rep (rep_of u2) ? swap 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

1114 
> kk_subset 
33192  1115 
else 
1116 
raise SAME () 

1117 
else 

1118 
raise SAME ()) 

1119 
handle SAME () => 

1120 
formula_from_opt_atom polar bool_j0 

1121 
(to_guard [u1, u2] bool_atom_R 

1122 
(rel_expr_from_formula kk bool_atom_R 

1123 
(kk_rel_eq r1 r2))) 

1124 
end 

1125 
else 

1126 
let 

1127 
val r1 = to_rep min_R u1 

1128 
val r2 = to_rep min_R u2 

1129 
in 

1130 
if is_one_rep min_R then 

1131 
let 

1132 
val rs1 = unpack_products r1 

1133 
val rs2 = unpack_products r2 

1134 
in 

1135 
if length rs1 = length rs2 

34126  1136 
andalso map KK.arity_of_rel_expr rs1 
1137 
= map KK.arity_of_rel_expr rs2 then 

33192  1138 
fold1 kk_and (map2 kk_subset rs1 rs2) 
1139 
else 

1140 
kk_subset r1 r2 

1141 
end 

1142 
else 

1143 
kk_rel_eq r1 r2 

1144 
end) 

33744
e82531ebf5f3
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
blanchet
parents:
33705
diff
changeset

1145 
 Op2 (The, T, _, u1, u2) => 
e82531ebf5f3
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
blanchet
parents:
33705
diff
changeset

1146 
to_f_with_polarity polar 
e82531ebf5f3
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
blanchet
parents:
33705
diff
changeset

1147 
(Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2)) 
e82531ebf5f3
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
blanchet
parents:
33705
diff
changeset

1148 
 Op2 (Eps, T, _, u1, u2) => 
e82531ebf5f3
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
blanchet
parents:
33705
diff
changeset

1149 
to_f_with_polarity polar 
e82531ebf5f3
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
blanchet
parents:
33705
diff
changeset

1150 
(Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2)) 
33192  1151 
 Op2 (Apply, T, _, u1, u2) => 
1152 
(case (polar, rep_of u1) of 

1153 
(Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1) 

1154 
 _ => 

1155 
to_f_with_polarity polar 

1156 
(Op2 (Apply, T, Opt (Atom (2, offset_of_type ofs T)), u1, u2))) 

1157 
 Op3 (Let, _, _, u1, u2, u3) => 

33854
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1158 
kk_formula_let [to_expr_assign u1 u2] (to_f_with_polarity polar u3) 
33192  1159 
 Op3 (If, _, _, u1, u2, u3) => 
33854
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1160 
kk_formula_if (to_f u1) (to_f_with_polarity polar u2) 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1161 
(to_f_with_polarity polar u3) 
34126  1162 
 FormulaReg (j, _, _) => KK.FormulaReg j 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1163 
 _ => raise NUT ("Nitpick_Kodkod.to_f", [u])) 
33192  1164 
 Atom (2, j0) => formula_from_atom j0 (to_r u) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1165 
 _ => raise NUT ("Nitpick_Kodkod.to_f", [u]) 
34126  1166 
(* polarity > nut > KK.formula *) 
33192  1167 
and to_f_with_polarity polar u = 
1168 
case rep_of u of 

1169 
Formula _ => to_f u 

1170 
 Atom (2, j0) => formula_from_atom j0 (to_r u) 

1171 
 Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1172 
 _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u]) 
34126  1173 
(* nut > KK.rel_expr *) 
33192  1174 
and to_r u = 
1175 
case u of 

1176 
Cst (False, _, Atom _) => false_atom 

1177 
 Cst (True, _, Atom _) => true_atom 

1178 
 Cst (Iden, T, Func (Struct [R1, R2], Formula Neut)) => 

1179 
if R1 = R2 andalso arity_of_rep R1 = 1 then 

34126  1180 
kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ) 
33192  1181 
else 
1182 
let 

1183 
val schema1 = atom_schema_of_rep R1 

1184 
val schema2 = atom_schema_of_rep R2 

1185 
val arity1 = length schema1 

1186 
val arity2 = length schema2 

1187 
val r1 = fold1 kk_product (unary_var_seq 0 arity1) 

1188 
val r2 = fold1 kk_product (unary_var_seq arity1 arity2) 

1189 
val min_R = min_rep R1 R2 

1190 
in 

1191 
kk_comprehension 

1192 
(decls_for_atom_schema 0 (schema1 @ schema2)) 

1193 
(kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1) 

1194 
(rel_expr_from_rel_expr kk min_R R2 r2)) 

1195 
end 

34126  1196 
 Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0 
33192  1197 
 Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) => 
1198 
to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut))) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1199 
 Cst (Num j, T, R) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1200 
if is_word_type T then 
34126  1201 
atom_from_int_expr kk T R (KK.Num j) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1202 
else if T = int_T then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1203 
case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of 
34126  1204 
~1 => if is_opt_rep R then KK.None 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1205 
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) 
34126  1206 
 j' => KK.Atom j' 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1207 
else 
34126  1208 
if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T) 
1209 
else if is_opt_rep R then KK.None 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1210 
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) 
33192  1211 
 Cst (Unknown, _, R) => empty_rel_for_rep R 
1212 
 Cst (Unrep, _, R) => empty_rel_for_rep R 

34126  1213 
 Cst (Suc, T as @{typ "unsigned_bit word => unsigned_bit word"}, R) => 
1214 
to_bit_word_unary_op T R (curry KK.Add (KK.Num 1)) 

1215 
 Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) => 

1216 
kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x)) 

1217 
 Cst (Suc, _, Func (Atom x, _)) => KK.Rel suc_rel 

1218 
 Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel 

1219 
 Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1220 
 Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => 
34126  1221 
to_bit_word_binary_op T R NONE (SOME (curry KK.Add)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1222 
 Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1223 
to_bit_word_binary_op T R 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1224 
(SOME (fn i1 => fn i2 => fn i3 => 
34126  1225 
kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2))) 
1226 
(KK.LE (KK.Num 0, KK.BitXor (i2, i3))))) 

1227 
(SOME (curry KK.Add)) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1228 
 Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) => 
34126  1229 
KK.Rel nat_subtract_rel 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1230 
 Cst (Subtract, Type ("fun", [@{typ int}, _]), _) => 
34126  1231 
KK.Rel int_subtract_rel 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1232 
 Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1233 
to_bit_word_binary_op T R NONE 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1234 
(SOME (fn i1 => fn i2 => 
34126  1235 
KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2)))) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1236 
 Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1237 
to_bit_word_binary_op T R 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1238 
(SOME (fn i1 => fn i2 => fn i3 => 
34126  1239 
kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0)) 
1240 
(KK.LT (KK.BitXor (i2, i3), KK.Num 0)))) 

1241 
(SOME (curry KK.Sub)) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1242 
 Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) => 
34126  1243 
KK.Rel nat_multiply_rel 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1244 
 Cst (Multiply, Type ("fun", [@{typ int}, _]), _) => 
34126  1245 
KK.Rel int_multiply_rel 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1246 
 Cst (Multiply, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1247 
T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1248 
to_bit_word_binary_op T R 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1249 
(SOME (fn i1 => fn i2 => fn i3 => 
34126  1250 
kk_or (KK.IntEq (i2, KK.Num 0)) 
1251 
(KK.IntEq (KK.Div (i3, i2), i1) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1252 
> bit_T = @{typ signed_bit} 
34126  1253 
? kk_and (KK.LE (KK.Num 0, 
1254 
foldl1 KK.BitAnd [i1, i2, i3]))))) 

1255 
(SOME (curry KK.Mult)) 

1256 
 Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_divide_rel 

1257 
 Cst (Divide, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_divide_rel 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1258 
 Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1259 
to_bit_word_binary_op T R NONE 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1260 
(SOME (fn i1 => fn i2 => 
34126  1261 
KK.IntIf (KK.IntEq (i2, KK.Num 0), 
1262 
KK.Num 0, KK.Div (i1, i2)))) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1263 
 Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1264 
to_bit_word_binary_op T R 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1265 
(SOME (fn i1 => fn i2 => fn i3 => 
34126  1266 
KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3]))) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1267 
(SOME (fn i1 => fn i2 => 
34126  1268 
KK.IntIf (kk_and (KK.LT (i1, KK.Num 0)) 
1269 
(KK.LT (KK.Num 0, i2)), 
