author  blanchet 
Fri, 18 Mar 2011 12:05:23 +0100  
changeset 41996  1d7735ae4273 
parent 41995  03c2d29ec790 
child 41997  33b7d118e9dc 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_kodkod.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Kodkod problem generator part of Kodkod. 

6 
*) 

7 

8 
signature NITPICK_KODKOD = 

9 
sig 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34982
diff
changeset

10 
type hol_context = Nitpick_HOL.hol_context 
38126  11 
type datatype_spec = Nitpick_Scope.datatype_spec 
33232
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 

15 
structure NameTable : TABLE 

16 

17 
val univ_card : 

18 
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

19 
val check_bits : int > Kodkod.formula > unit 
38182  20 
val check_arity : string > int > int > unit 
33192  21 
val kk_tuple : bool > int > int list > Kodkod.tuple 
22 
val tuple_set_from_atom_schema : (int * int) list > Kodkod.tuple_set 

23 
val sequential_int_bounds : int > Kodkod.int_bound list 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

24 
val pow_of_two_int_bounds : int > int > Kodkod.int_bound list 
38126  25 
val bounds_and_axioms_for_built_in_rels_in_formulas : 
39345  26 
bool > int > int > int > int > Kodkod.formula list 
38126  27 
> Kodkod.bound list * Kodkod.formula list 
33192  28 
val bound_for_plain_rel : Proof.context > bool > nut > Kodkod.bound 
29 
val bound_for_sel_rel : 

41995  30 
Proof.context > bool > (typ * (nut * int) list option) list 
31 
> datatype_spec list > nut > Kodkod.bound 

33192  32 
val merge_bounds : Kodkod.bound list > Kodkod.bound list 
41802  33 
val kodkod_formula_from_nut : 
34 
int Typtab.table > kodkod_constrs > nut > Kodkod.formula 

41995  35 
val needed_values_for_datatype : 
36 
nut list > int Typtab.table > datatype_spec > (nut * int) list option 

33192  37 
val declarative_axiom_for_plain_rel : kodkod_constrs > nut > Kodkod.formula 
38 
val declarative_axioms_for_datatypes : 

41995  39 
hol_context > bool > nut list > (typ * (nut * int) list option) list 
40 
> int > int > int Typtab.table > kodkod_constrs > nut NameTable.table 

41 
> datatype_spec list > Kodkod.formula list 

33192  42 
end; 
43 

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

44 
structure Nitpick_Kodkod : NITPICK_KODKOD = 
33192  45 
struct 
46 

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

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

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

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

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

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

52 
open Nitpick_Nut 
33192  53 

34126  54 
structure KK = Kodkod 
55 

38126  56 
fun pull x xs = x :: filter_out (curry (op =) x) xs 
33192  57 

38196  58 
fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...} 
59 
: datatype_spec) = true 

60 
 is_datatype_acyclic _ = false 

33192  61 

34126  62 
fun flip_nums n = index_seq 1 n @ [0] > map KK.Num 
33192  63 

64 
fun univ_card nat_card int_card main_j0 bounds formula = 

65 
let 

66 
fun rel_expr_func r k = 

67 
Int.max (k, case r of 

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

33192  70 
 _ => 0) 
71 
fun tuple_func t k = 

72 
case t of 

34126  73 
KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k 
33192  74 
 _ => k 
75 
fun tuple_set_func ts k = 

34126  76 
Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k'  _ => 0) 
33192  77 
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, 
78 
int_expr_func = K I} 

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

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

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

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

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

85 
let 
34126  86 
fun int_expr_func (KK.Num k) () = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

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

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

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

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

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

94 
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

95 
int_expr_func = int_expr_func} 
34126  96 
in KK.fold_formula expr_F formula () end 
33192  97 

38182  98 
fun check_arity guilty_party univ_card n = 
34126  99 
if n > KK.max_arity univ_card then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

100 
raise TOO_LARGE ("Nitpick_Kodkod.check_arity", 
38182  101 
"arity " ^ string_of_int n ^ 
102 
(if guilty_party = "" then 

103 
"" 

104 
else 

105 
" of Kodkod relation associated with " ^ 

41045
2a41709f34c1
use heuristic to determine whether to keep or drop an existing "let"  and drop all higherorder lets
blanchet
parents:
39898
diff
changeset

106 
quote (original_name guilty_party)) ^ 
38182  107 
" too large for universe of cardinality " ^ 
108 
string_of_int univ_card) 

33192  109 
else 
110 
() 

111 

112 
fun kk_tuple debug univ_card js = 

113 
if debug then 

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

33192  118 

34126  119 
val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq 
33192  120 
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep 
121 

34126  122 
val single_atom = KK.TupleSet o single o KK.Tuple o single 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

123 
fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))] 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

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

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

126 
fun aux 0 _ _ = [] 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

127 
 aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])] 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

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

131 
in aux (bits + 1) 1 j0 end 
33192  132 

38126  133 
fun built_in_rels_in_formulas formulas = 
33192  134 
let 
39345  135 
fun rel_expr_func (KK.Rel (x as (_, j))) = 
38126  136 
(j < 0 andalso x <> unsigned_bit_word_sel_rel andalso 
137 
x <> signed_bit_word_sel_rel) 

138 
? insert (op =) x 

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

139 
 rel_expr_func _ = I 
33192  140 
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, 
141 
int_expr_func = K I} 

38126  142 
in fold (KK.fold_formula expr_F) formulas [] end 
33192  143 

144 
val max_table_size = 65536 

145 

146 
fun check_table_size k = 

147 
if k > max_table_size then 

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

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

149 
"precomputed table too large (" ^ string_of_int k ^ ")") 
33192  150 
else 
151 
() 

152 

153 
fun tabulate_func1 debug univ_card (k, j0) f = 

154 
(check_table_size k; 

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

156 
if j2 >= 0 then 

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

158 
else 

159 
NONE 

160 
end) (index_seq 0 k)) 

161 
fun tabulate_op2 debug univ_card (k, j0) res_j0 f = 

162 
(check_table_size (k * k); 

163 
map_filter (fn j => let 

164 
val j1 = j div k 

165 
val j2 = j  j1 * k 

166 
val j3 = f (j1, j2) 

167 
in 

168 
if j3 >= 0 then 

169 
SOME (kk_tuple debug univ_card 

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

171 
else 

172 
NONE 

173 
end) (index_seq 0 (k * k))) 

174 
fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f = 

175 
(check_table_size (k * k); 

176 
map_filter (fn j => let 

177 
val j1 = j div k 

178 
val j2 = j  j1 * k 

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

180 
in 

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

182 
SOME (kk_tuple debug univ_card 

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

184 
j4 + res_j0]) 

185 
else 

186 
NONE 

187 
end) (index_seq 0 (k * k))) 

188 
fun tabulate_nat_op2 debug univ_card (k, j0) f = 

189 
tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f) 

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

191 
tabulate_op2 debug univ_card (k, j0) j0 

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

193 
fun tabulate_int_op2_2 debug univ_card (k, j0) f = 

194 
tabulate_op2_2 debug univ_card (k, j0) j0 

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

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

197 

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

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

200 
fun isa_gcd (m, 0) = m 

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

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

203 
val isa_zgcd = isa_gcd o pairself abs 

204 
fun isa_norm_frac (m, n) = 

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

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

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

208 

39345  209 
fun tabulate_built_in_rel debug univ_card nat_card int_card j0 
38124  210 
(x as (n, _)) = 
38182  211 
(check_arity "" univ_card n; 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

212 
if x = not3_rel then 
33192  213 
("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

214 
else if x = suc_rel then 
38126  215 
("suc", tabulate_func1 debug univ_card (univ_card  j0  1, j0) 
216 
(Integer.add 1)) 

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

217 
else if x = nat_add_rel then 
33192  218 
("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

219 
else if x = int_add_rel then 
33192  220 
("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

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

223 
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

224 
else if x = int_subtract_rel then 
33192  225 
("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

226 
else if x = nat_multiply_rel then 
33192  227 
("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

228 
else if x = int_multiply_rel then 
33192  229 
("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

230 
else if x = nat_divide_rel then 
33192  231 
("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

232 
else if x = int_divide_rel then 
33192  233 
("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

234 
else if x = nat_less_rel then 
33192  235 
("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35312
diff
changeset

236 
(int_from_bool o op <)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

237 
else if x = int_less_rel then 
33192  238 
("int_less", tabulate_int_op2 debug univ_card (int_card, j0) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35312
diff
changeset

239 
(int_from_bool o op <)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

240 
else if x = gcd_rel then 
33192  241 
("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

242 
else if x = lcm_rel then 
33192  243 
("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

244 
else if x = norm_frac_rel then 
33192  245 
("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0) 
246 
isa_norm_frac) 

247 
else 

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

248 
raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation")) 
33192  249 

39345  250 
fun bound_for_built_in_rel debug univ_card nat_card int_card main_j0 
38126  251 
(x as (n, j)) = 
252 
if n = 2 andalso j <= suc_rels_base then 

253 
let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in 

254 
([(x, "suc")], 

255 
if tabulate then 

256 
[KK.TupleSet (tabulate_func1 debug univ_card (k  1, j0) 

257 
(Integer.add 1))] 

258 
else 

259 
[KK.TupleSet [], tuple_set_from_atom_schema [y, y]]) 

260 
end 

261 
else 

262 
let 

39345  263 
val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card 
264 
main_j0 x 

38126  265 
in ([(x, nick)], [KK.TupleSet ts]) end 
33192  266 

38126  267 
fun axiom_for_built_in_rel (x as (n, j)) = 
268 
if n = 2 andalso j <= suc_rels_base then 

269 
let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in 

38160  270 
if tabulate then 
38126  271 
NONE 
38160  272 
else if k < 2 then 
273 
SOME (KK.No (KK.Rel x)) 

38126  274 
else 
275 
SOME (KK.TotalOrdering (x, KK.AtomSeq y, KK.Atom j0, KK.Atom (j0 + 1))) 

276 
end 

277 
else 

278 
NONE 

39345  279 
fun bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card nat_card 
38126  280 
int_card main_j0 formulas = 
281 
let val rels = built_in_rels_in_formulas formulas in 

39345  282 
(map (bound_for_built_in_rel debug univ_card nat_card int_card main_j0) 
38126  283 
rels, 
284 
map_filter axiom_for_built_in_rel rels) 

39316
b6c4385ab400
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents:
38212
diff
changeset

285 
end 
33192  286 

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

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

288 
short_name nick ^ 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

289 
(if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

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

291 

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 

41995  303 
fun bound_for_sel_rel ctxt debug need_vals dtypes 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

304 
(FreeRel (x, T as Type (@{type_name fun}, [T1, T2]), 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

305 
R as Func (Atom (_, j0), R2), nick)) = 
33192  306 
let 
41995  307 
val constr_s = original_name nick 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

308 
val {delta, epsilon, exclusive, explicit_max, ...} = 
41995  309 
constr_spec dtypes (constr_s, T1) 
310 
val dtype as {card, ...} = datatype_spec dtypes T1 > the 

311 
val need_vals = 

312 
AList.lookup (op =) need_vals T1 > the_default NONE > these 

33192  313 
in 
314 
([(x, bound_comment ctxt debug nick T R)], 

41995  315 
let 
316 
val complete_need_vals = (length need_vals = card) 

317 
val (my_need_vals, other_need_vals) = 

318 
need_vals 

319 
> List.partition 

320 
(fn (Construct (sel_us, _, _, _), _) => 

321 
exists (fn FreeRel (x', _, _, _) => x = x' 

322 
 _ => false) sel_us 

323 
 _ => false) 

41996  324 
fun upper_bound_ts () = 
325 
if complete_need_vals then 

326 
my_need_vals > map (KK.Tuple o single o snd) > KK.TupleSet 

327 
else if not (null other_need_vals) then 

328 
index_seq (delta + j0) (epsilon  delta) 

329 
> filter_out (member (op = o apsnd snd) other_need_vals) 

330 
> map (KK.Tuple o single) > KK.TupleSet 

331 
else 

332 
KK.TupleAtomSeq (epsilon  delta, delta + j0) 

41995  333 
in 
334 
if explicit_max = 0 orelse 

41996  335 
(complete_need_vals andalso null my_need_vals) (* ### needed? *) then 
41995  336 
[KK.TupleSet []] 
337 
else 

33192  338 
if R2 = Formula Neut then 
41996  339 
[upper_bound_ts ()] > not exclusive ? cons (KK.TupleSet []) 
33192  340 
else 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

341 
[KK.TupleSet [], 
35178  342 
if T1 = T2 andalso epsilon > delta andalso 
41995  343 
is_datatype_acyclic dtype then 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

344 
index_seq delta (epsilon  delta) 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

345 
> map (fn j => 
38126  346 
KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]], 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

347 
KK.TupleAtomSeq (j, j0))) 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

348 
> foldl1 KK.TupleUnion 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

349 
else 
41996  350 
KK.TupleProduct (upper_bound_ts (), upper_bound_for_rep R2)] 
33192  351 
end) 
352 
end 

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

354 
raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u]) 
33192  355 

356 
fun merge_bounds bs = 

357 
let 

358 
fun arity (zs, _) = fst (fst (hd zs)) 

359 
fun add_bound ds b [] = List.revAppend (ds, [b]) 

360 
 add_bound ds b (c :: cs) = 

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

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

363 
else 

364 
add_bound (c :: ds) b cs 

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

366 

34126  367 
fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n) 
33192  368 

34126  369 
val singleton_from_combination = foldl1 KK.Product o map KK.Atom 
33192  370 
fun all_singletons_for_rep R = 
371 
if is_lone_rep R then 

372 
all_combinations_for_rep R > map singleton_from_combination 

373 
else 

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

374 
raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R]) 
33192  375 

34126  376 
fun unpack_products (KK.Product (r1, r2)) = 
33192  377 
unpack_products r1 @ unpack_products r2 
378 
 unpack_products r = [r] 

34126  379 
fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2 
33192  380 
 unpack_joins r = [r] 
381 

382 
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep 

383 
fun full_rel_for_rep R = 

384 
case atom_schema_of_rep R of 

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

385 
[] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R]) 
34126  386 
 schema => foldl1 KK.Product (map KK.AtomSeq schema) 
33192  387 

388 
fun decls_for_atom_schema j0 schema = 

34126  389 
map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x)) 
33192  390 
(index_seq j0 (length schema)) schema 
391 

392 
fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs) 

393 
R r = 

394 
let val body_R = body_rep R in 

395 
if is_lone_rep body_R then 

396 
let 

397 
val binder_schema = atom_schema_of_reps (binder_reps R) 

398 
val body_schema = atom_schema_of_rep body_R 

399 
val one = is_one_rep body_R 

34126  400 
val opt_x = case r of KK.Rel x => SOME x  _ => NONE 
33192  401 
in 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

402 
if opt_x <> NONE andalso length binder_schema = 1 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

403 
length body_schema = 1 then 
34126  404 
(if one then KK.Function else KK.Functional) 
405 
(the opt_x, KK.AtomSeq (hd binder_schema), 

406 
KK.AtomSeq (hd body_schema)) 

33192  407 
else 
408 
let 

409 
val decls = decls_for_atom_schema ~1 binder_schema 

410 
val vars = unary_var_seq ~1 (length binder_schema) 

411 
val kk_xone = if one then kk_one else kk_lone 

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

413 
end 

414 
else 

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

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

421 
else if x = nat_add_rel then 
33192  422 
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

423 
else if x = nat_multiply_rel then 
33192  424 
formula_for_bool (card_of_rep (body_rep R) <= 2) 
425 
else 

426 
d_n_ary_function kk R r 

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

427 
else if x = nat_subtract_rel then 
34126  428 
KK.True 
33192  429 
else 
430 
d_n_ary_function kk R r 

431 
 kk_n_ary_function kk R r = d_n_ary_function kk R r 

432 

34126  433 
fun kk_disjoint_sets _ [] = KK.True 
33192  434 
 kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs) 
435 
(r :: rs) = 

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

437 

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

438 
fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r = 
33192  439 
if inline_rel_expr r then 
440 
f r 

441 
else 

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

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

445 
val single_rel_rel_let = basic_rel_rel_let 0 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

447 
single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

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

450 
(fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2 
33192  451 

452 
fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f = 

34126  453 
kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0) 
33192  454 
fun rel_expr_from_formula kk R f = 
455 
case unopt_rep R of 

456 
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

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

459 
fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity 

460 
num_chunks r = 

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

462 
chunk_arity) 

463 

464 
fun kk_n_fold_join 

465 
(kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1 

466 
res_R r1 r2 = 

467 
case arity_of_rep R1 of 

468 
1 => kk_join r1 r2 

469 
 arity1 => 

38164  470 
let val unpacked_rs1 = unpack_products r1 in 
33192  471 
if one andalso length unpacked_rs1 = arity1 then 
472 
fold kk_join unpacked_rs1 r2 

38164  473 
else if one andalso inline_rel_expr r1 then 
474 
fold kk_join (unpack_vect_in_chunks kk 1 arity1 r1) r2 

33192  475 
else 
476 
kk_project_seq 

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

478 
arity1 (arity_of_rep res_R) 

479 
end 

480 

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

482 
if rs1 = rs2 then r 

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

484 

485 
val lone_rep_fallback_max_card = 4096 

486 
val some_j0 = 0 

487 

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 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

493 
if is_lone_rep old_R andalso is_lone_rep new_R andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

494 
card = card_of_rep new_R then 
33192  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 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

504 
and atom_from_rel_expr kk x old_R r = 
33192  505 
case old_R of 
506 
Func (R1, R2) => 

507 
let 

508 
val dom_card = card_of_rep R1 

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

510 
in 

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

512 
(vect_from_rel_expr kk dom_card R2' old_R r) 

513 
end 

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

514 
 Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R]) 
33192  515 
 _ => lone_rep_fallback kk (Atom x) old_R r 
516 
and struct_from_rel_expr kk Rs old_R r = 

517 
case old_R of 

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

519 
 Struct Rs' => 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

520 
if Rs' = Rs then 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

521 
r 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

522 
else if map card_of_rep Rs' = map card_of_rep Rs then 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

523 
let 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

524 
val old_arities = map arity_of_rep Rs' 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

525 
val old_offsets = offset_list old_arities 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

526 
val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

527 
in 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

528 
fold1 (#kk_product kk) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

529 
(map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

530 
end 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

531 
else 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

532 
lone_rep_fallback kk (Struct Rs) old_R r 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

533 
 _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R]) 
33192  534 
and vect_from_rel_expr kk k R old_R r = 
535 
case old_R of 

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

537 
 Vect (k', R') => 

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

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

540 
 Func (R1, Formula Neut) => 

541 
if k = card_of_rep R1 then 

542 
fold1 (#kk_product kk) 

543 
(map (fn arg_r => 

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

545 
(all_singletons_for_rep R1)) 

546 
else 

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

547 
raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
33192  548 
 Func (R1, R2) => 
549 
fold1 (#kk_product kk) 

550 
(map (fn arg_r => 

551 
rel_expr_from_rel_expr kk R R2 

552 
(kk_n_fold_join kk true R1 R2 arg_r r)) 

553 
(all_singletons_for_rep R1)) 

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

554 
 _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
33192  555 
and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r = 
556 
let 

557 
val dom_card = card_of_rep R1 

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

559 
in 

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

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

562 
end 

563 
 func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r = 

564 
(case old_R of 

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

566 
let 

567 
val args_rs = all_singletons_for_rep R1 

568 
val vals_rs = unpack_vect_in_chunks kk 1 k r 

569 
fun empty_or_singleton_set_for arg_r val_r = 

34126  570 
#kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r) 
33192  571 
in 
572 
fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs) 

573 
end 

574 
 Func (R1', Formula Neut) => 

575 
if R1 = R1' then 

576 
r 

577 
else 

578 
let 

579 
val schema = atom_schema_of_rep R1 

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

581 
> 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

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

584 
#kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) 
33192  585 
end 
586 
 Func (R1', Atom (2, j0)) => 

587 
func_from_no_opt_rel_expr kk R1 (Formula Neut) 

34126  588 
(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

589 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  590 
[old_R, Func (R1, Formula Neut)])) 
591 
 func_from_no_opt_rel_expr kk R1 R2 old_R r = 

592 
case old_R of 

593 
Vect (k, R) => 

594 
let 

595 
val args_rs = all_singletons_for_rep R1 

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

597 
> map (rel_expr_from_rel_expr kk R2 R) 

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

599 
 Func (R1', Formula Neut) => 

600 
(case R2 of 

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

602 
let val schema = atom_schema_of_rep R1 in 

603 
if length schema = 1 then 

34126  604 
#kk_override kk (#kk_product kk (KK.AtomSeq (hd schema)) 
605 
(KK.Atom j0)) 

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

33192  607 
else 
608 
let 

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

610 
> rel_expr_from_rel_expr kk R1' R1 

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

614 
#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

615 
(#kk_subset kk r2 r3) 
33192  616 
end 
617 
end 

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

618 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  619 
[old_R, Func (R1, R2)])) 
620 
 Func (R1', R2') => 

621 
if R1 = R1' andalso R2 = R2' then 

622 
r 

623 
else 

624 
let 

625 
val dom_schema = atom_schema_of_rep R1 

626 
val ran_schema = atom_schema_of_rep R2 

627 
val dom_prod = fold1 (#kk_product kk) 

628 
(unary_var_seq ~1 (length dom_schema)) 

629 
> rel_expr_from_rel_expr kk R1' R1 

630 
val ran_prod = fold1 (#kk_product kk) 

631 
(unary_var_seq (~(length dom_schema)  1) 

632 
(length ran_schema)) 

633 
> rel_expr_from_rel_expr kk R2' R2 

634 
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

635 
val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk 
33192  636 
in 
637 
#kk_comprehension kk (decls_for_atom_schema ~1 

638 
(dom_schema @ ran_schema)) 

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

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

641 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  642 
[old_R, Func (R1, R2)]) 
643 
and rel_expr_from_rel_expr kk new_R old_R r = 

644 
let 

645 
val unopt_old_R = unopt_rep old_R 

646 
val unopt_new_R = unopt_rep new_R 

647 
in 

648 
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

649 
raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R]) 
33192  650 
else if unopt_new_R = unopt_old_R then 
651 
r 

652 
else 

653 
(case unopt_new_R of 

654 
Atom x => atom_from_rel_expr kk x 

655 
 Struct Rs => struct_from_rel_expr kk Rs 

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

657 
 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

658 
 _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", 
33192  659 
[old_R, new_R])) 
660 
unopt_old_R r 

661 
end 

662 
and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2)) 

663 

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

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

667 
else 

668 
signed_bit_word_sel_rel)) 

669 
val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom 

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

670 
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

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

672 
kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R)) 
34126  673 
(kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1))) 
674 
(KK.Bits i)) 

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

675 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

676 
fun kodkod_formula_from_nut ofs 
33192  677 
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not, 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

678 
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, 
39456  679 
kk_lone, kk_some, kk_rel_let, kk_rel_if, kk_union, 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

680 
kk_difference, kk_intersect, kk_product, kk_join, kk_closure, 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

681 
kk_comprehension, kk_project, kk_project_seq, kk_not3, 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

682 
kk_nat_less, kk_int_less, ...}) u = 
33192  683 
let 
684 
val main_j0 = offset_of_type ofs bool_T 

685 
val bool_j0 = main_j0 

686 
val bool_atom_R = Atom (2, main_j0) 

34126  687 
val false_atom = KK.Atom bool_j0 
688 
val true_atom = KK.Atom (bool_j0 + 1) 

33192  689 
fun formula_from_opt_atom polar j0 r = 
690 
case polar of 

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

33192  693 
val formula_from_atom = formula_from_opt_atom Pos 
694 
val unpack_formulas = 

695 
map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1 

696 
fun kk_vect_set_bool_op connective k r1 r2 = 

697 
fold1 kk_and (map2 connective (unpack_formulas k r1) 

698 
(unpack_formulas k r2)) 

699 
fun to_f u = 

700 
case rep_of u of 

701 
Formula polar => 

702 
(case u of 

34126  703 
Cst (False, _, _) => KK.False 
704 
 Cst (True, _, _) => KK.True 

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

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

706 
kk_not (to_f_with_polarity (flip_polarity polar) u1) 
33192  707 
 Op1 (Finite, _, _, u1) => 
708 
let val opt1 = is_opt_rep (rep_of u1) in 

709 
case polar of 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

710 
Neut => 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

711 
if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

712 
else KK.True 
33192  713 
 Pos => formula_for_bool (not opt1) 
34126  714 
 Neg => KK.True 
33192  715 
end 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

716 
 Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1) 
33192  717 
 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

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

719 
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

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

721 
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

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

723 
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

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

725 
kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
33192  726 
 Op2 (Less, T, Formula polar, u1, u2) => 
727 
formula_from_opt_atom polar bool_j0 

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

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

730 
let 

731 
val dom_T = domain_type (type_of u1) 

732 
val R1 = rep_of u1 

733 
val R2 = rep_of u2 

734 
val (dom_R, ran_R) = 

735 
case min_rep R1 R2 of 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

736 
Func Rp => Rp 
33192  737 
 R => (Atom (card_of_domain_from_rep 2 R, 
738 
offset_of_type ofs dom_T), 

739 
if is_opt_rep R then Opt bool_atom_R else Formula Neut) 

740 
val set_R = Func (dom_R, ran_R) 

741 
in 

742 
if not (is_opt_rep ran_R) then 

743 
to_set_bool_op kk_implies kk_subset u1 u2 

744 
else if polar = Neut then 

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

745 
raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u]) 
33192  746 
else 
747 
let 

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

748 
(* FIXME: merge with similar code below *) 
33192  749 
fun set_to_r widen u = 
750 
if widen then 

751 
kk_difference (full_rel_for_rep dom_R) 

752 
(kk_join (to_rep set_R u) false_atom) 

753 
else 

754 
kk_join (to_rep set_R u) true_atom 

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

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

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

758 
end 

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

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

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

761 
Formula polar => 
33192  762 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
763 
 min_R => 

764 
let 

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

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

767 
 args _ = [] 

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

769 
in 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

770 
if null opt_arg_us orelse not (is_Opt min_R) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

771 
is_eval_name u1 then 
33192  772 
fold (kk_or o (kk_no o to_r)) opt_arg_us 
773 
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)) 

774 
else 

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

775 
kk_subset (to_rep min_R u1) (to_rep min_R u2) 
33192  776 
end) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

777 
 Op2 (Eq, _, _, u1, u2) => 
33192  778 
(case min_rep (rep_of u1) (rep_of u2) of 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

779 
Formula polar => 
33192  780 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
781 
 min_R => 

782 
if is_opt_rep min_R then 

783 
if polar = Neut then 

784 
(* continuation of hackish optimization *) 

785 
kk_rel_eq (to_rep min_R u1) (to_rep min_R u2) 

786 
else if is_Cst Unrep u1 then 

787 
to_could_be_unrep (polar = Neg) u2 

788 
else if is_Cst Unrep u2 then 

789 
to_could_be_unrep (polar = Neg) u1 

790 
else 

791 
let 

792 
val r1 = to_rep min_R u1 

793 
val r2 = to_rep min_R u2 

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

795 
in 

796 
(if polar = Pos then 

797 
if not both_opt then 

798 
kk_rel_eq r1 r2 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

799 
else if is_lone_rep min_R andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

800 
arity_of_rep min_R = 1 then 
33192  801 
kk_some (kk_intersect r1 r2) 
802 
else 

803 
raise SAME () 

804 
else 

805 
if is_lone_rep min_R then 

806 
if arity_of_rep min_R = 1 then 

35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

807 
kk_lone (kk_union r1 r2) 
33192  808 
else if not both_opt then 
809 
(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

810 
> kk_subset 
33192  811 
else 
812 
raise SAME () 

813 
else 

814 
raise SAME ()) 

815 
handle SAME () => 

816 
formula_from_opt_atom polar bool_j0 

817 
(to_guard [u1, u2] bool_atom_R 

818 
(rel_expr_from_formula kk bool_atom_R 

819 
(kk_rel_eq r1 r2))) 

820 
end 

821 
else 

822 
let 

823 
val r1 = to_rep min_R u1 

824 
val r2 = to_rep min_R u2 

825 
in 

826 
if is_one_rep min_R then 

827 
let 

828 
val rs1 = unpack_products r1 

829 
val rs2 = unpack_products r2 

830 
in 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

831 
if length rs1 = length rs2 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

832 
map KK.arity_of_rel_expr rs1 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

833 
= map KK.arity_of_rel_expr rs2 then 
33192  834 
fold1 kk_and (map2 kk_subset rs1 rs2) 
835 
else 

836 
kk_subset r1 r2 

837 
end 

838 
else 

839 
kk_rel_eq r1 r2 

840 
end) 

841 
 Op2 (Apply, T, _, u1, u2) => 

842 
(case (polar, rep_of u1) of 

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

844 
 _ => 

845 
to_f_with_polarity polar 

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

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

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

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

850 
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

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

853 
 _ => raise NUT ("Nitpick_Kodkod.to_f", [u])) 
33192  854 
 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

855 
 _ => raise NUT ("Nitpick_Kodkod.to_f", [u]) 
33192  856 
and to_f_with_polarity polar u = 
857 
case rep_of u of 

858 
Formula _ => to_f u 

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

860 
 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

861 
 _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u]) 
33192  862 
and to_r u = 
863 
case u of 

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

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

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

866 
 Cst (Iden, _, Func (Struct [R1, R2], Formula Neut)) => 
33192  867 
if R1 = R2 andalso arity_of_rep R1 = 1 then 
34126  868 
kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ) 
33192  869 
else 
870 
let 

871 
val schema1 = atom_schema_of_rep R1 

872 
val schema2 = atom_schema_of_rep R2 

873 
val arity1 = length schema1 

874 
val arity2 = length schema2 

875 
val r1 = fold1 kk_product (unary_var_seq 0 arity1) 

876 
val r2 = fold1 kk_product (unary_var_seq arity1 arity2) 

877 
val min_R = min_rep R1 R2 

878 
in 

879 
kk_comprehension 

880 
(decls_for_atom_schema 0 (schema1 @ schema2)) 

881 
(kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1) 

882 
(rel_expr_from_rel_expr kk min_R R2 r2)) 

883 
end 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

884 
 Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

885 
 Cst (Iden, T as Type (@{type_name fun}, [T1, _]), R as Func (R1, _)) => 
33192  886 
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

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

888 
if is_word_type T then 
34126  889 
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

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

891 
case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of 
34126  892 
~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

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

895 
else 
34126  896 
if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T) 
897 
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

898 
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) 
33192  899 
 Cst (Unknown, _, R) => empty_rel_for_rep R 
900 
 Cst (Unrep, _, R) => empty_rel_for_rep R 

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

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

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

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

905 
 Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

906 
 Cst (Add, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_add_rel 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

907 
 Cst (Add, Type (_, [@{typ int}, _]), _) => KK.Rel int_add_rel 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

908 
 Cst (Add, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) => 
34126  909 
to_bit_word_binary_op T R NONE (SOME (curry KK.Add)) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

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

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

912 
(SOME (fn i1 => fn i2 => fn i3 => 
34126  913 
kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2))) 
914 
(KK.LE (KK.Num 0, KK.BitXor (i2, i3))))) 

915 
(SOME (curry KK.Add)) 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

916 
 Cst (Subtract, Type (_, [@{typ nat}, _]), _) => 
34126  917 
KK.Rel nat_subtract_rel 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

918 
 Cst (Subtract, Type (_, [@{typ int}, _]), _) => 
34126  919 
KK.Rel int_subtract_rel 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

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

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

922 
(SOME (fn i1 => fn i2 => 
34126  923 
KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2)))) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

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

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

926 
(SOME (fn i1 => fn i2 => fn i3 => 
34126  927 
kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0)) 
928 
(KK.LT (KK.BitXor (i2, i3), KK.Num 0)))) 

929 
(SOME (curry KK.Sub)) 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

930 
 Cst (Multiply, Type (_, [@{typ nat}, _]), _) => 
34126  931 
KK.Rel nat_multiply_rel 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

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

934 
 Cst (Multiply, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

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

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

937 
(SOME (fn i1 => fn i2 => fn i3 => 
34126  938 
kk_or (KK.IntEq (i2, KK.Num 0)) 
939 
(KK.IntEq (KK.Div (i3, i2), i1) 

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

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

943 
(SOME (curry KK.Mult)) 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

944 
 Cst (Divide, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_divide_rel 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

945 
 Cst (Divide, Type (_, [@{typ int}, _]), _) => KK.Rel int_divide_rel 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

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

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

948 
(SOME (fn i1 => fn i2 => 
34126  949 
KK.IntIf (KK.IntEq (i2, KK.Num 0), 
950 
KK.Num 0, KK.Div (i1, i2)))) 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

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

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

953 
(SOME (fn i1 => fn i2 => fn i3 => 
34126  954 
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

955 
(SOME (fn i1 => fn i2 => 
34126  956 
KK.IntIf (kk_and (KK.LT (i1, KK.Num 0)) 
957 
(KK.LT (KK.Num 0, i2)), 

958 
KK.Sub (KK.Div (KK.Add (i1, KK.Num 1), i2), KK.Num 1), 

959 
KK.IntIf (kk_and (KK.LT (KK.Num 0, i1)) 

960 
(KK.LT (i2, KK.Num 0)), 

961 
KK.Sub (KK.Div (KK.Sub (i1, KK.Num 1), i2), KK.Num 1), 

962 
KK.IntIf (KK.IntEq (i2, KK.Num 0), 

963 
KK.Num 0, KK.Div (i1, i2)))))) 

964 
 Cst (Gcd, _, _) => KK.Rel gcd_rel 

965 
 Cst (Lcm, _, _) => KK.Rel lcm_rel 

966 
 Cst (Fracs, _, Func (Atom (1, _), _)) => KK.None 

33192  967 
 Cst (Fracs, _, Func (Struct _, _)) => 
34126  968 
kk_project_seq (KK.Rel norm_frac_rel) 2 2 
969 
 Cst (NormFrac, _, _) => KK.Rel norm_frac_rel 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

970 
 Cst (NatToInt, Type (_, [@{typ nat}, _]), Func (Atom _, Atom _)) => 
34126  971 
KK.Iden 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

972 
 Cst (NatToInt, Type (_, [@{typ nat}, _]), 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

973 
Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) => 
33192  974 
if nat_j0 = int_j0 then 
34126  975 
kk_intersect KK.Iden 
976 
(kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0)) 

977 
KK.Univ) 

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

979 
raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"") 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

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

981 
to_bit_word_unary_op T R I 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

982 
 Cst (IntToNat, Type (_, [@{typ int}, _]), 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

983 
Func (Atom (int_k, int_j0), nat_R)) => 
33192  984 
let 
985 
val abs_card = max_int_for_card int_k + 1 

986 
val (nat_k, nat_j0) = the_single (atom_schema_of_rep nat_R) 

987 
val overlap = Int.min (nat_k, abs_card) 

988 
in 

989 
if nat_j0 = int_j0 then 

34126  990 
kk_union (kk_product (KK.AtomSeq (int_k  abs_card, 
991 
int_j0 + abs_card)) 

992 
(KK.Atom nat_j0)) 

993 
(kk_intersect KK.Iden 

994 
(kk_product (KK.AtomSeq (overlap, int_j0)) KK.Univ)) 

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

996 
raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"") 
33192  997 
end 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

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

999 
to_bit_word_unary_op T R 
34126  1000 
(fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i)) 
33192  1001 
 Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1) 
34126  1002 
 Op1 (Finite, _, Opt (Atom _), _) => KK.None 
33192  1003 
 Op1 (Converse, T, R, u1) => 
1004 
let 

1005 
val (b_T, a_T) = HOLogic.dest_prodT (domain_type T) 

1006 
val (b_R, a_R) = 

1007 
case R of 

1008 
Func (Struct [R1, R2], _) => (R1, R2) 

1009 
 Func (R1, _) => 

1010 
if card_of_rep R1 <> 1 then 

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

1011 
raise REP ("Nitpick_Kodkod.to_r (Converse)", [R]) 
33192  1012 
else 
1013 
pairself (Atom o pair 1 o offset_of_type ofs) (b_T, a_T) 

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

1014 
 _ => raise REP ("Nitpick_Kodkod.to_r (Converse)", [R]) 
33192  1015 
val body_R = body_rep R 
1016 
val a_arity = arity_of_rep a_R 

1017 
val b_arity = arity_of_rep b_R 

1018 
val ab_arity = a_arity + b_arity 

1019 
val body_arity = arity_of_rep body_R 

1020 
in 

1021 
kk_project (to_rep (Func (Struct [a_R, b_R], body_R)) u1) 

34126  1022 
(map KK.Num (index_seq a_arity b_arity @ 
1023 
index_seq 0 a_arity @ 

1024 
index_seq ab_arity body_arity)) 

33192  1025 
> rel_expr_from_rel_expr kk R (Func (Struct [b_R, a_R], body_R)) 
1026 
end 

1027 
 Op1 (Closure, _, R, u1) => 

1028 
if is_opt_rep R then 

1029 
let 

1030 
val T1 = type_of u1 

1031 
val R' = rep_to_binary_rel_rep ofs T1 (unopt_rep (rep_of u1)) 

1032 
val R'' = opt_rep ofs T1 R' 

1033 
in 

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

1034 
single_rel_rel_let kk 
33192  1035 
(fn r => 
1036 
let 

1037 
val true_r = kk_closure (kk_join r true_atom) 

1038 
val full_r = full_rel_for_rep R' 

1039 
val false_r = kk_difference full_r 

1040 
(kk_closure (kk_difference full_r 

1041 
(kk_join r false_atom))) 

1042 
in 

1043 
rel_expr_from_rel_expr kk R R'' 

1044 
(kk_union (kk_product true_r true_atom) 

1045 
(kk_product false_r false_atom)) 

1046 
end) (to_rep R'' u1) 

1047 
end 

1048 
else 

1049 
let val R' = rep_to_binary_rel_rep ofs (type_of u1) (rep_of u1) in 

1050 
rel_expr_from_rel_expr kk R R' (kk_closure (to_rep R' u1)) 

1051 
end 

1052 
 Op1 (SingletonSet, _, Func (R1, Opt _), Cst (Unrep, _, _)) => 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

1053 
kk_product (full_rel_for_rep R1) false_atom 
33192  1054 
 Op1 (SingletonSet, _, R, u1) => 
1055 
(case R of 

1056 
Func (R1, Formula Neut) => to_rep R1 u1 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1057 
 Func (R1, Opt _) => 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1058 
single_rel_rel_let kk 
33192  1059 
(fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R) 
1060 
(rel_expr_to_func kk R1 bool_atom_R 

1061 
(Func (R1, Formula Neut)) r)) 

1062 
(to_opt R1 u1) 

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

1063 
 _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u])) 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

1064 
 Op1 (SafeThe, _, R, u1) => 
33192  1065 
if is_opt_rep R then 
1066 
kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom 

1067 
else 

1068 
to_rep (Func (R, Formula Neut)) u1 

39345  1069 
 Op1 (First, _, R, u1) => to_nth_pair_sel 0 R u1 
1070 
 Op1 (Second, _, R, u1) => to_nth_pair_sel 1 R u1 

33192  1071 
 Op1 (Cast, _, R, u1) => 
1072 
((case rep_of u1 of 

1073 
Formula _ => 

1074 
(case unopt_rep R of 

1075 
Atom (2, j0) => atom_from_formula kk j0 (to_f u1) 

1076 
 _ => raise SAME ()) 

1077 
 _ => raise SAME ()) 

1078 
handle SAME () => rel_expr_from_rel_expr kk R (rep_of u1) (to_r u1)) 

1079 
 Op2 (All, T, R as Opt _, u1, u2) => 

1080 
to_r (Op1 (Not, T, R, 

1081 
Op2 (Exist, T, R, u1, Op1 (Not, T, rep_of u2, u2)))) 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1082 
 Op2 (Exist, _, Opt _, u1, u2) => 
33192  1083 
let val rs1 = untuple to_decl u1 in 
1084 
if not (is_opt_rep (rep_of u2)) then 

34126  1085 
kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None 
33192  1086 
else 
1087 
let val r2 = to_r u2 in 

1088 
kk_union (kk_rel_if (kk_exist rs1 (kk_rel_eq r2 true_atom)) 

34126  1089 
true_atom KK.None) 
33192  1090 
(kk_rel_if (kk_all rs1 (kk_rel_eq r2 false_atom)) 
34126  1091 
false_atom KK.None) 
33192  1092 
end 
1093 
end 

1094 
 Op2 (Or, _, _, u1, u2) => 

1095 
if is_opt_rep (rep_of u1) then kk_rel_if (to_f u2) true_atom (to_r u1) 

1096 
else kk_rel_if (to_f u1) true_atom (to_r u2) 

1097 
 Op2 (And, _, _, u1, u2) => 

1098 
if is_opt_rep (rep_of u1) then kk_rel_if (to_f u2) (to_r u1) false_atom 

1099 
else kk_rel_if (to_f u1) (to_r u2) false_atom 

1100 
 Op2 (Less, _, _, u1, u2) => 

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

1101 
(case type_of u1 of 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1102 
@{typ nat} => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1103 
if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1104 
else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1105 
else kk_nat_less (to_integer u1) (to_integer u2) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1106 
 @{typ int} => kk_int_less (to_integer u1) (to_integer u2) 
36127
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1107 
 _ => 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1108 
let 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1109 
val R1 = Opt (Atom (card_of_rep (rep_of u1), 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1110 
offset_of_type ofs (type_of u1))) 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1111 
in 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1112 
double_rel_rel_let kk 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1113 
(fn r1 => fn r2 => 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1114 
kk_rel_if 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1115 
(fold kk_and (map_filter (fn (u, r) => 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1116 
if is_opt_rep (rep_of u) then SOME (kk_some r) 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1117 
else NONE) [(u1, r1), (u2, r2)]) KK.True) 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1118 
(atom_from_formula kk bool_j0 (KK.LT (pairself 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1119 
(int_expr_from_atom kk (type_of u1)) (r1, r2)))) 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1120 
KK.None) 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1121 
(to_rep R1 u1) (to_rep R1 u2) 
e91292c520be
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
blanchet
parents:
35695
diff
changeset

1122 
end) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1123 
 Op2 (Triad, _, Opt (Atom (2, j0)), u1, u2) => 
33192  1124 
let 
1125 
val f1 = to_f u1 

1126 
val f2 = to_f u2 

1127 
in 

1128 
if f1 = f2 then 

1129 
atom_from_formula kk j0 f1 

1130 
else 

34126  1131 
kk_union (kk_rel_if f1 true_atom KK.None) 
1132 
(kk_rel_if f2 KK.None false_atom) 

33192  1133 
end 
1134 
 Op2 (Composition, _, R, u1, u2) => 

1135 
let 

33863
fb13147a3050
generate arguments of relational composition in the right order in Nitpick
blanchet
parents:
33854
diff
changeset

1136 
val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u1)) 
fb13147a3050
generate arguments of relational composition in the right order in Nitpick
blanchet
parents:
33854
diff
changeset

1137 
val (_, c_T) = HOLogic.dest_prodT (domain_type (type_of u2)) 
fb13147a3050
generate arguments of relational composition in the right order in Nitpick
blanchet
parents:
33854
diff
changeset

1138 
val ab_k = card_of_domain_from_rep 2 (rep_of u1) 
fb13147a3050
generate arguments of relational composition in the right order in Nitpick
blanchet
parents:
33854
diff
changeset

1139 
val bc_k = card_of_domain_from_rep 2 (rep_of u2) 
33192  1140 
val ac_k = card_of_domain_from_rep 2 R 
1141 
val a_k = exact_root 2 (ac_k * ab_k div bc_k) 

1142 
val b_k = exact_root 2 (ab_k * bc_k div ac_k) 

1143 
val c_k = exact_root 2 (bc_k * ac_k div ab_k) 

1144 
val a_R = Atom (a_k, offset_of_type ofs a_T) 

1145 
val b_R = Atom (b_k, offset_of_type ofs b_T) 

1146 
val c_R = Atom (c_k, offset_of_type ofs c_T) 

1147 
val body_R = body_rep R 

1148 
in 

1149 
(case body_R of 

1150 
Formula Neut => 

33863
fb13147a3050
generate arguments of relational composition in the right order in Nitpick
blanchet
parents:
33854
diff
changeset

1151 
kk_join (to_rep (Func (Struct [a_R, b_R], Formula Neut)) u1) 
fb13147a3050
generate arguments of relational composition in the right order in Nitpick
blanchet
parents:
33854
diff
changeset

1152 
(to_rep (Func (Struct [b_R, c_R], Formula Neut)) u2) 
33192  1153 
 Opt (Atom (2, _)) => 
1154 
let 

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

1155 
(* FIXME: merge with similar code above *) 
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

1156 
fun must R1 R2 u = 
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

1157 
kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom 
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

1158 
fun may R1 R2 u = 
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

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

1160 
(full_rel_for_rep (Struct [R1, R2])) 
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

1161 
(kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) 
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

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

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

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

1165 
(kk_product (kk_join (must a_R b_R u1) (must b_R c_R u2)) 
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

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

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

1168 
(full_rel_for_rep (Struct [a_R, c_R])) 
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

1169 
(kk_join (may a_R b_R u1) (may b_R c_R u2))) 
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

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

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

1172 
 _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u])) 
33192  1173 
> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R)) 
1174 
end 

1175 
 Op2 (Apply, @{typ nat}, _, 

1176 
Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) => 

1177 
if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then 

34126  1178 
KK.Atom (offset_of_type ofs nat_T) 
33192  1179 
else 
34126  1180 
fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel) 
35312  1181 
 Op2 (Apply, _, R, u1, u2) => to_apply R u1 u2 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1182 
 Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) => 
34126  1183 
to_guard [u1, u2] R (KK.Atom j0) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1184 
 Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) => 
33192  1185 
kk_comprehension (untuple to_decl u1) (to_f u2) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1186 
 Op2 (Lambda, _, Func (_, R2), u1, u2) => 
33192  1187 
let 
1188 
val dom_decls = untuple to_decl u1 

1189 
val ran_schema = atom_schema_of_rep R2 

1190 
val ran_decls = decls_for_atom_schema ~1 ran_schema 

1191 
val ran_vars = unary_var_seq ~1 (length ran_decls) 

1192 
in 

1193 
kk_comprehension (dom_decls @ ran_decls) 

1194 
(kk_subset (fold1 kk_product ran_vars) 

1195 
(to_rep R2 u2)) 

1196 
end 

1197 
 Op3 (Let, _, R, u1, u2, u3) => 

1198 
kk_rel_let [to_expr_assign u1 u2] (to_rep R u3) 

1199 
 Op3 (If, _, R, u1, u2, u3) => 

1200 
if is_opt_rep (rep_of u1) then 

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

1201 
triple_rel_rel_let kk 
33192  1202 
(fn r1 => fn r2 => fn r3 => 
1203 
let val empty_r = empty_rel_for_rep R in 

1204 
fold1 kk_union 

1205 
[kk_rel_if (kk_rel_eq r1 true_atom) r2 empty_r, 

1206 
kk_rel_if (kk_rel_eq r1 false_atom) r3 empty_r, 

1207 
kk_rel_if (kk_rel_eq r2 r3) 

1208 
(if inline_rel_expr r2 then r2 else r3) empty_r] 

1209 
end) 

1210 
(to_r u1) (to_rep R u2) (to_rep R u3) 

1211 
else 

1212 
kk_rel_if (to_f u1) (to_rep R u2) (to_rep R u3) 

1213 
 Tuple (_, R, us) => 

1214 
(case unopt_rep R of 

1215 
Struct Rs => to_product Rs us 

1216 
 Vect (k, R) => to_product (replicate k R) us 

1217 
 Atom (1, j0) => 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

1218 
kk_rel_if (kk_some (fold1 kk_product (map to_r us))) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

1219 
(KK.Atom j0) KK.None 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1220 
 _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u])) 
33192  1221 
 Construct ([u'], _, _, []) => to_r u' 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1222 
 Construct (discr_u :: sel_us, _, _, arg_us) => 
33192  1223 
let 
1224 
val set_rs = 

1225 
map2 (fn sel_u => fn arg_u => 

1226 
let 

1227 
val (R1, R2) = dest_Func (rep_of sel_u) 

1228 
val sel_r = to_r sel_u 

1229 
val arg_r = to_opt R2 arg_u 

1230 
in 

1231 
if is_one_rep R2 then 

1232 
kk_n_fold_join kk true R2 R1 arg_r 

1233 
(kk_project sel_r (flip_nums (arity_of_rep R2))) 

1234 
else 

34288
cf455b5880e1
reduced arity of Nitpick selectors associated with sets by 1, by using "Formula" instead of "Atom 2"
blanchet
parents:
34126
diff
changeset

1235 
kk_comprehension [KK.DeclOne ((1, ~1), to_r discr_u)] 
34126  1236 
(kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r) 
35695  1237 
> is_opt_rep (rep_of arg_u) ? to_guard [arg_u] R1 
33192  1238 
end) sel_us arg_us 
1239 
in fold1 kk_intersect set_rs end 

34126  1240 
 BoundRel (x, _, _, _) => KK.Var x 
1241 
 FreeRel (x, _, _, _) => KK.Rel x 

1242 
 RelReg (j, _, R) => KK.RelReg (arity_of_rep R, j) 

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

1243 
 u => raise NUT ("Nitpick_Kodkod.to_r", [u]) 
33192  1244 
and to_decl (BoundRel (x, _, R, _)) = 
34126  1245 
KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R))) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1246 
 to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u]) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1247 
and to_expr_assign (FormulaReg (j, _, _)) u = 
34126  1248 
KK.AssignFormulaReg (j, to_f u) 
33192  1249 
 to_expr_assign (RelReg (j, _, R)) u = 
34126  1250 
KK.AssignRelReg ((arity_of_rep R, j), to_r u) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1251 
 to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1]) 
39345  1252 
and to_atom (x as (_, j0)) u = 
33192  1253 
case rep_of u of 
1254 
Formula _ => atom_from_formula kk j0 (to_f u) 

1255 
 R => atom_from_rel_expr kk x R (to_r u) 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

1256 
and to_struct Rs u = struct_from_rel_expr kk Rs (rep_of u) (to_r u) 