author  blanchet 
Wed, 04 Aug 2010 22:47:52 +0200  
changeset 38194  a9877c14550f 
parent 38193  44d635ce6da4 
child 38195  a8cef06e0480 
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 : 
26 
bool > int Typtab.table > int > int > int > int > Kodkod.formula list 

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 : 

38126  30 
Proof.context > bool > datatype_spec list > nut > Kodkod.bound 
33192  31 
val merge_bounds : Kodkod.bound list > Kodkod.bound list 
32 
val declarative_axiom_for_plain_rel : kodkod_constrs > nut > Kodkod.formula 

33 
val declarative_axioms_for_datatypes : 

38126  34 
hol_context > bool > int > int > int Typtab.table > kodkod_constrs 
35 
> nut NameTable.table > datatype_spec list > Kodkod.formula list 

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

37 
int Typtab.table > kodkod_constrs > nut > Kodkod.formula 
33192  38 
end; 
39 

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

40 
structure Nitpick_Kodkod : NITPICK_KODKOD = 
33192  41 
struct 
42 

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

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

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

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

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

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

48 
open Nitpick_Nut 
33192  49 

34126  50 
structure KK = Kodkod 
51 

38126  52 
structure NfaGraph = Typ_Graph 
53 

54 
fun pull x xs = x :: filter_out (curry (op =) x) xs 

33192  55 

38126  56 
fun is_datatype_good_and_old ({co = false, standard = true, deep = true, ...} 
57 
: datatype_spec) = true 

58 
 is_datatype_good_and_old _ = false 

33192  59 

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

62 
fun univ_card nat_card int_card main_j0 bounds formula = 

63 
let 

64 
fun rel_expr_func r k = 

65 
Int.max (k, case r of 

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

33192  68 
 _ => 0) 
69 
fun tuple_func t k = 

70 
case t of 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

92 
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

93 
int_expr_func = int_expr_func} 
34126  94 
in KK.fold_formula expr_F formula () end 
33192  95 

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

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

101 
"" 

102 
else 

103 
" of Kodkod relation associated with " ^ 

104 
quote guilty_party) ^ 

105 
" too large for universe of cardinality " ^ 

106 
string_of_int univ_card) 

33192  107 
else 
108 
() 

109 

110 
fun kk_tuple debug univ_card js = 

111 
if debug then 

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

33192  116 

34126  117 
val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq 
33192  118 
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep 
119 

34126  120 
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

121 
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

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

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

124 
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

125 
 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

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

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

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

129 
in aux (bits + 1) 1 j0 end 
33192  130 

38126  131 
fun built_in_rels_in_formulas formulas = 
33192  132 
let 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

133 
fun rel_expr_func (KK.Rel (x as (n, j))) = 
38126  134 
(j < 0 andalso x <> unsigned_bit_word_sel_rel andalso 
135 
x <> signed_bit_word_sel_rel) 

136 
? insert (op =) x 

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

137 
 rel_expr_func _ = I 
33192  138 
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, 
139 
int_expr_func = K I} 

38126  140 
in fold (KK.fold_formula expr_F) formulas [] end 
33192  141 

142 
val max_table_size = 65536 

143 

144 
fun check_table_size k = 

145 
if k > max_table_size then 

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

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

147 
"precomputed table too large (" ^ string_of_int k ^ ")") 
33192  148 
else 
149 
() 

150 

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

152 
(check_table_size k; 

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

154 
if j2 >= 0 then 

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

156 
else 

157 
NONE 

158 
end) (index_seq 0 k)) 

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

160 
(check_table_size (k * k); 

161 
map_filter (fn j => let 

162 
val j1 = j div k 

163 
val j2 = j  j1 * k 

164 
val j3 = f (j1, j2) 

165 
in 

166 
if j3 >= 0 then 

167 
SOME (kk_tuple debug univ_card 

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

169 
else 

170 
NONE 

171 
end) (index_seq 0 (k * k))) 

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

173 
(check_table_size (k * k); 

174 
map_filter (fn j => let 

175 
val j1 = j div k 

176 
val j2 = j  j1 * k 

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

178 
in 

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

180 
SOME (kk_tuple debug univ_card 

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

182 
j4 + res_j0]) 

183 
else 

184 
NONE 

185 
end) (index_seq 0 (k * k))) 

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

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

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

189 
tabulate_op2 debug univ_card (k, j0) j0 

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

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

192 
tabulate_op2_2 debug univ_card (k, j0) j0 

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

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

195 

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

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

198 
fun isa_gcd (m, 0) = m 

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

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

201 
val isa_zgcd = isa_gcd o pairself abs 

202 
fun isa_norm_frac (m, n) = 

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

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

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

206 

38124  207 
fun tabulate_built_in_rel debug ofs univ_card nat_card int_card j0 
208 
(x as (n, _)) = 

38182  209 
(check_arity "" univ_card n; 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

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

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

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

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

221 
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

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

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

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

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

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

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

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

235 
else if x = int_less_rel then 
33192  236 
("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

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

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

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

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

245 
else 

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

246 
raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation")) 
33192  247 

38126  248 
fun bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0 
249 
(x as (n, j)) = 

250 
if n = 2 andalso j <= suc_rels_base then 

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

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

253 
if tabulate then 

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

255 
(Integer.add 1))] 

256 
else 

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

258 
end 

259 
else 

260 
let 

261 
val (nick, ts) = tabulate_built_in_rel debug ofs univ_card nat_card 

262 
int_card main_j0 x 

263 
in ([(x, nick)], [KK.TupleSet ts]) end 

33192  264 

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

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

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

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

274 
end 

275 
else 

276 
NONE 

277 
fun bounds_and_axioms_for_built_in_rels_in_formulas debug ofs univ_card nat_card 

278 
int_card main_j0 formulas = 

279 
let val rels = built_in_rels_in_formulas formulas in 

280 
(map (bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0) 

281 
rels, 

282 
map_filter axiom_for_built_in_rel rels) 

283 
end 

33192  284 

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

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

286 
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

287 
(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

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

289 

33192  290 
fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) = 
291 
([(x, bound_comment ctxt debug nick T R)], 

292 
if nick = @{const_name bisim_iterator_max} then 

293 
case R of 

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

294 
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

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

299 
raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) 
33192  300 

301 
fun bound_for_sel_rel ctxt debug dtypes 

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

302 
(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

303 
R as Func (Atom (_, j0), R2), nick)) = 
33192  304 
let 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

305 
val {delta, epsilon, exclusive, explicit_max, ...} = 
33192  306 
constr_spec dtypes (original_name nick, T1) 
307 
in 

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

309 
if explicit_max = 0 then 

34126  310 
[KK.TupleSet []] 
33192  311 
else 
34126  312 
let val ts = KK.TupleAtomSeq (epsilon  delta, delta + j0) in 
33192  313 
if R2 = Formula Neut then 
34126  314 
[ts] > not exclusive ? cons (KK.TupleSet []) 
33192  315 
else 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

316 
[KK.TupleSet [], 
35178  317 
if T1 = T2 andalso epsilon > delta andalso 
38126  318 
is_datatype_good_and_old (the (datatype_spec dtypes T1)) then 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

319 
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

320 
> map (fn j => 
38126  321 
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

322 
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

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

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

325 
KK.TupleProduct (ts, upper_bound_for_rep R2)] 
33192  326 
end) 
327 
end 

328 
 bound_for_sel_rel _ _ _ u = 

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

329 
raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u]) 
33192  330 

331 
fun merge_bounds bs = 

332 
let 

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

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

335 
 add_bound ds b (c :: cs) = 

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

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

338 
else 

339 
add_bound (c :: ds) b cs 

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

341 

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

34126  344 
val singleton_from_combination = foldl1 KK.Product o map KK.Atom 
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 
fun unpack_products (KK.Product (r1, r2)) = 
33192  352 
unpack_products r1 @ unpack_products r2 
353 
 unpack_products r = [r] 

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

357 
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep 

358 
fun full_rel_for_rep R = 

359 
case atom_schema_of_rep R of 

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

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

363 
fun decls_for_atom_schema j0 schema = 

34126  364 
map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x)) 
33192  365 
(index_seq j0 (length schema)) schema 
366 

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

368 
R r = 

369 
let val body_R = body_rep R in 

370 
if is_lone_rep body_R then 

371 
let 

372 
val binder_schema = atom_schema_of_reps (binder_reps R) 

373 
val body_schema = atom_schema_of_rep body_R 

374 
val one = is_one_rep body_R 

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

377 
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

378 
length body_schema = 1 then 
34126  379 
(if one then KK.Function else KK.Functional) 
380 
(the opt_x, KK.AtomSeq (hd binder_schema), 

381 
KK.AtomSeq (hd body_schema)) 

33192  382 
else 
383 
let 

384 
val decls = decls_for_atom_schema ~1 binder_schema 

385 
val vars = unary_var_seq ~1 (length binder_schema) 

386 
val kk_xone = if one then kk_one else kk_lone 

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

388 
end 

389 
else 

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

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

396 
else if x = nat_add_rel then 
33192  397 
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

398 
else if x = nat_multiply_rel then 
33192  399 
formula_for_bool (card_of_rep (body_rep R) <= 2) 
400 
else 

401 
d_n_ary_function kk R r 

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

402 
else if x = nat_subtract_rel then 
34126  403 
KK.True 
33192  404 
else 
405 
d_n_ary_function kk R r 

406 
 kk_n_ary_function kk R r = d_n_ary_function kk R r 

407 

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

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

412 

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

413 
fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r = 
33192  414 
if inline_rel_expr r then 
415 
f r 

416 
else 

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

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

420 
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

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

422 
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

423 
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

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

425 
(fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2 
33192  426 

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

34126  428 
kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0) 
33192  429 
fun rel_expr_from_formula kk R f = 
430 
case unopt_rep R of 

431 
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

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

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

435 
num_chunks r = 

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

437 
chunk_arity) 

438 

439 
fun kk_n_fold_join 

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

441 
res_R r1 r2 = 

442 
case arity_of_rep R1 of 

443 
1 => kk_join r1 r2 

444 
 arity1 => 

38164  445 
let val unpacked_rs1 = unpack_products r1 in 
33192  446 
if one andalso length unpacked_rs1 = arity1 then 
447 
fold kk_join unpacked_rs1 r2 

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

33192  450 
else 
451 
kk_project_seq 

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

453 
arity1 (arity_of_rep res_R) 

454 
end 

455 

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

457 
if rs1 = rs2 then r 

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

459 

460 
val lone_rep_fallback_max_card = 4096 

461 
val some_j0 = 0 

462 

463 
fun lone_rep_fallback kk new_R old_R r = 

464 
if old_R = new_R then 

465 
r 

466 
else 

467 
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

468 
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

469 
card = card_of_rep new_R then 
33192  470 
if card >= lone_rep_fallback_max_card then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

472 
"too high cardinality (" ^ string_of_int card ^ ")") 
33192  473 
else 
474 
kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R) 

475 
(all_singletons_for_rep new_R) 

476 
else 

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

477 
raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R]) 
33192  478 
end 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

479 
and atom_from_rel_expr kk x old_R r = 
33192  480 
case old_R of 
481 
Func (R1, R2) => 

482 
let 

483 
val dom_card = card_of_rep R1 

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

485 
in 

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

487 
(vect_from_rel_expr kk dom_card R2' old_R r) 

488 
end 

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

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

492 
case old_R of 

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

494 
 Struct Rs' => 

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

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

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

497 
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

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

499 
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

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

501 
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

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

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

504 
(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

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

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

507 
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

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

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

512 
 Vect (k', R') => 

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

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

515 
 Func (R1, Formula Neut) => 

516 
if k = card_of_rep R1 then 

517 
fold1 (#kk_product kk) 

518 
(map (fn arg_r => 

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

520 
(all_singletons_for_rep R1)) 

521 
else 

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

522 
raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
33192  523 
 Func (R1, R2) => 
524 
fold1 (#kk_product kk) 

525 
(map (fn arg_r => 

526 
rel_expr_from_rel_expr kk R R2 

527 
(kk_n_fold_join kk true R1 R2 arg_r r)) 

528 
(all_singletons_for_rep R1)) 

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

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

532 
val dom_card = card_of_rep R1 

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

534 
in 

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

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

537 
end 

538 
 func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r = 

539 
(case old_R of 

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

541 
let 

542 
val args_rs = all_singletons_for_rep R1 

543 
val vals_rs = unpack_vect_in_chunks kk 1 k r 

544 
fun empty_or_singleton_set_for arg_r val_r = 

34126  545 
#kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r) 
33192  546 
in 
547 
fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs) 

548 
end 

549 
 Func (R1', Formula Neut) => 

550 
if R1 = R1' then 

551 
r 

552 
else 

553 
let 

554 
val schema = atom_schema_of_rep R1 

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

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

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

559 
#kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) 
33192  560 
end 
561 
 Func (R1', Atom (2, j0)) => 

562 
func_from_no_opt_rel_expr kk R1 (Formula Neut) 

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

564 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  565 
[old_R, Func (R1, Formula Neut)])) 
566 
 func_from_no_opt_rel_expr kk R1 R2 old_R r = 

567 
case old_R of 

568 
Vect (k, R) => 

569 
let 

570 
val args_rs = all_singletons_for_rep R1 

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

572 
> map (rel_expr_from_rel_expr kk R2 R) 

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

574 
 Func (R1', Formula Neut) => 

575 
(case R2 of 

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

577 
let val schema = atom_schema_of_rep R1 in 

578 
if length schema = 1 then 

34126  579 
#kk_override kk (#kk_product kk (KK.AtomSeq (hd schema)) 
580 
(KK.Atom j0)) 

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

33192  582 
else 
583 
let 

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

585 
> rel_expr_from_rel_expr kk R1' R1 

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

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

590 
(#kk_subset kk r2 r3) 
33192  591 
end 
592 
end 

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

593 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  594 
[old_R, Func (R1, R2)])) 
595 
 Func (R1', R2') => 

596 
if R1 = R1' andalso R2 = R2' then 

597 
r 

598 
else 

599 
let 

600 
val dom_schema = atom_schema_of_rep R1 

601 
val ran_schema = atom_schema_of_rep R2 

602 
val dom_prod = fold1 (#kk_product kk) 

603 
(unary_var_seq ~1 (length dom_schema)) 

604 
> rel_expr_from_rel_expr kk R1' R1 

605 
val ran_prod = fold1 (#kk_product kk) 

606 
(unary_var_seq (~(length dom_schema)  1) 

607 
(length ran_schema)) 

608 
> rel_expr_from_rel_expr kk R2' R2 

609 
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

610 
val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk 
33192  611 
in 
612 
#kk_comprehension kk (decls_for_atom_schema ~1 

613 
(dom_schema @ ran_schema)) 

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

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

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

619 
let 

620 
val unopt_old_R = unopt_rep old_R 

621 
val unopt_new_R = unopt_rep new_R 

622 
in 

623 
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

624 
raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R]) 
33192  625 
else if unopt_new_R = unopt_old_R then 
626 
r 

627 
else 

628 
(case unopt_new_R of 

629 
Atom x => atom_from_rel_expr kk x 

630 
 Struct Rs => struct_from_rel_expr kk Rs 

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

632 
 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

633 
 _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", 
33192  634 
[old_R, new_R])) 
635 
unopt_old_R r 

636 
end 

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

638 

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

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

642 
else 

643 
signed_bit_word_sel_rel)) 

644 
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

645 
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

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

647 
kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R)) 
34126  648 
(kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1))) 
649 
(KK.Bits i)) 

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

650 

33192  651 
fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) = 
652 
kk_n_ary_function kk (R > nick = @{const_name List.set} ? unopt_rep) 

34126  653 
(KK.Rel x) 
33192  654 
 declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs) 
655 
(FreeRel (x, _, R, _)) = 

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

658 
else KK.True 

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

660 
raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u]) 
33192  661 

662 
fun const_triple rel_table (x as (s, T)) = 

663 
case the_name rel_table (ConstName (s, T, Any)) of 

34126  664 
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

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

667 
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr 

668 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

669 
fun nfa_transitions_for_sel hol_ctxt binarize 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

670 
({kk_project, ...} : kodkod_constrs) rel_table 
38126  671 
(dtypes : datatype_spec list) constr_x n = 
33192  672 
let 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

673 
val x as (_, T) = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

674 
binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n 
33192  675 
val (r, R, arity) = const_triple rel_table x 
676 
val type_schema = type_schema_of_rep T R 

677 
in 

678 
map_filter (fn (j, T) => 

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

38126  680 
else SOME ((x, kk_project r (map KK.Num [0, j])), T)) 
33192  681 
(index_seq 1 (arity  1) ~~ tl type_schema) 
682 
end 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

683 
fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

684 
(x as (_, T)) = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

685 
maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x) 
33192  686 
(index_seq 0 (num_sels_for_constr_type T)) 
38126  687 
fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

688 
 nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

689 
 nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

690 
 nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

691 
{typ, constrs, ...} = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

692 
SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

693 
dtypes o #const) constrs) 
33192  694 

34126  695 
val empty_rel = KK.Product (KK.None, KK.None) 
33192  696 

35177  697 
fun direct_path_rel_exprs nfa start_T final_T = 
698 
case AList.lookup (op =) nfa final_T of 

38126  699 
SOME trans => map (snd o fst) (filter (curry (op =) start_T o snd) trans) 
33192  700 
 NONE => [] 
35177  701 
and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T 
702 
final_T = 

703 
fold kk_union (direct_path_rel_exprs nfa start_T final_T) 

704 
(if start_T = final_T then KK.Iden else empty_rel) 

705 
 any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T = 

706 
kk_union (any_path_rel_expr kk nfa Ts start_T final_T) 

707 
(knot_path_rel_expr kk nfa Ts start_T T final_T) 

708 
and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts 

709 
start_T knot_T final_T = 

710 
kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T) 

711 
(kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T))) 

712 
(any_path_rel_expr kk nfa Ts start_T knot_T) 

713 
and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T = 

714 
fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel 

715 
 loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts) 

716 
start_T = 

717 
if start_T = T then 

718 
kk_closure (loop_path_rel_expr kk nfa Ts start_T) 

33192  719 
else 
35177  720 
kk_union (loop_path_rel_expr kk nfa Ts start_T) 
721 
(knot_path_rel_expr kk nfa Ts start_T T start_T) 

33192  722 

723 
fun graph_for_nfa nfa = 

724 
let 

35177  725 
fun new_node T = perhaps (try (NfaGraph.new_node (T, ()))) 
33192  726 
fun add_nfa [] = I 
727 
 add_nfa ((_, []) :: nfa) = add_nfa nfa 

35177  728 
 add_nfa ((T, ((_, T') :: transitions)) :: nfa) = 
729 
add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o 

730 
new_node T' o new_node T 

33192  731 
in add_nfa nfa NfaGraph.empty end 
732 

733 
fun strongly_connected_sub_nfas nfa = 

734 
nfa > graph_for_nfa > NfaGraph.strong_conn 

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

736 

38126  737 
fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa 
738 
start_T = 

739 
kk_no (kk_intersect 

740 
(loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T) 

741 
KK.Iden) 

742 
fun acyclicity_axioms_for_datatypes kk nfas = 

743 
maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas 

744 

745 
fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r = 

746 
kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z))) 

747 
fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 = 

748 
kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z)))) 

749 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

750 
fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) = 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

751 
(delta, (epsilon, (num_binder_types T, s))) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

752 
val constr_ord = 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

753 
prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord)) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

754 
o pairself constr_quadruple 
38126  755 

756 
fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...}, 

757 
{card = card2, self_rec = self_rec2, constrs = constr2, ...}) 

758 
: datatype_spec * datatype_spec) = 

759 
prod_ord int_ord (prod_ord bool_ord int_ord) 

760 
((card1, (self_rec1, length constr1)), 

761 
(card2, (self_rec2, length constr2))) 

762 

763 
(* We must absolutely tabulate "suc" for all datatypes whose selector bounds 

764 
break cycles; otherwise, we may end up with two incompatible symmetry 

765 
breaking orders, leading to spurious models. *) 

766 
fun should_tabulate_suc_for_type dtypes T = 

38127  767 
is_asymmetric_nondatatype T orelse 
38126  768 
case datatype_spec dtypes T of 
769 
SOME {self_rec, ...} => self_rec 

770 
 NONE => false 

771 

772 
fun lex_order_rel_expr (kk as {kk_implies, kk_and, kk_subset, kk_join, ...}) 

773 
dtypes sel_quadruples = 

774 
case sel_quadruples of 

775 
[] => KK.True 

776 
 ((r, Func (Atom _, Atom x), 2), (_, Type (_, [_, T]))) :: sel_quadruples' => 

777 
let val z = (x, should_tabulate_suc_for_type dtypes T) in 

778 
if null sel_quadruples' then 

779 
gt kk z (kk_join (KK.Var (1, 1)) r) (kk_join (KK.Var (1, 0)) r) 

780 
else 

781 
kk_and (kk_subset (kk_join (KK.Var (1, 1)) r) 

782 
(all_ge kk z (kk_join (KK.Var (1, 0)) r))) 

783 
(kk_implies (kk_subset (kk_join (KK.Var (1, 1)) r) 

784 
(kk_join (KK.Var (1, 0)) r)) 

785 
(lex_order_rel_expr kk dtypes sel_quadruples')) 

786 
end 

787 
(* Skip constructors components that aren't atoms, since we cannot compare 

788 
these easily. *) 

789 
 _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples' 

790 

38193  791 
fun is_nil_like_constr_type dtypes T = 
792 
case datatype_spec dtypes T of 

793 
SOME {constrs, ...} => 

794 
(case filter_out (is_self_recursive_constr_type o snd o #const) constrs of 

795 
[{const = (_, T'), ...}] => T = T' 

796 
 _ => false) 

797 
 NONE => false 

38126  798 

799 
fun sym_break_axioms_for_constr_pair hol_ctxt binarize 

800 
(kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset, 

801 
kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

802 
(constr_ord, 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

803 
({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...}, 
38191  804 
{const = const2 as (_, T2), delta = delta2, epsilon = epsilon2, ...}) 
805 
: constr_spec * constr_spec) = 

38126  806 
let 
807 
val dataT = body_type T1 

808 
val nfa = nfas > find_first (exists (curry (op =) dataT o fst)) > these 

809 
val rec_Ts = nfa > map fst 

810 
fun rec_and_nonrec_sels (x as (_, T)) = 

811 
index_seq 0 (num_sels_for_constr_type T) 

812 
> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x) 

813 
> List.partition (member (op =) rec_Ts o range_type o snd) 

814 
val sel_xs1 = rec_and_nonrec_sels const1 > op @ 

815 
in 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

816 
if constr_ord = EQUAL andalso null sel_xs1 then 
38126  817 
[] 
818 
else 

819 
let 

820 
val z = 

821 
(case #2 (const_triple rel_table (discr_for_constr const1)) of 

822 
Func (Atom x, Formula _) => x 

823 
 R => raise REP ("Nitpick_Kodkod.sym_break_axioms_for_constr_pair", 

824 
[R]), should_tabulate_suc_for_type dtypes dataT) 

825 
val (rec_sel_xs2, nonrec_sel_xs2) = rec_and_nonrec_sels const2 

826 
val sel_xs2 = rec_sel_xs2 @ nonrec_sel_xs2 

827 
fun sel_quadruples2 () = sel_xs2 > map (`(const_triple rel_table)) 

828 
(* If the two constructors are the same, we drop the first selector 

829 
because that one is always checked by the lexicographic order. 

830 
We sometimes also filter out direct subterms, because those are 

831 
already handled by the acyclicity breaking in the bound 

832 
declarations. *) 

833 
fun filter_out_sels no_direct sel_xs = 

834 
apsnd (filter_out 

835 
(fn ((x, _), T) => 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

836 
(constr_ord = EQUAL andalso x = hd sel_xs) orelse 
38126  837 
(T = dataT andalso 
838 
(no_direct orelse not (member (op =) sel_xs x))))) 

38193  839 
(* FIXME: why the last disjunct above? *) 
38126  840 
fun subterms_r no_direct sel_xs j = 
841 
loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa) 

842 
(filter_out (curry (op =) dataT) (map fst nfa)) dataT 

843 
> kk_join (KK.Var (1, j)) 

844 
in 

845 
[kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1), 

846 
KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)] 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

847 
(kk_implies 
38126  848 
(if delta2 >= epsilon1 then KK.True 
38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

849 
else if delta1 >= epsilon2  1 then KK.False 
38126  850 
else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0))) 
851 
(kk_or 

38193  852 
(if is_nil_like_constr_type dtypes T1 then 
38126  853 
KK.True 
854 
else 

855 
kk_some (kk_intersect (subterms_r false sel_xs2 1) 

856 
(all_ge kk z (KK.Var (1, 0))))) 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

857 
(case constr_ord of 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

858 
EQUAL => 
38126  859 
kk_and 
860 
(lex_order_rel_expr kk dtypes (sel_quadruples2 ())) 

861 
(if length rec_sel_xs2 > 1 then 

862 
kk_all [KK.DeclOne ((1, 2), 

863 
subterms_r true sel_xs1 0)] 

864 
(gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))) 

865 
else 

866 
KK.True) 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

867 
 LESS => 
38126  868 
kk_all [KK.DeclOne ((1, 2), 
869 
subterms_r false sel_xs1 0)] 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

870 
(gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

871 
 GREATER => KK.False)))] 
38126  872 
end 
873 
end 

874 

875 
fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes 

876 
({constrs, ...} : datatype_spec) = 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

877 
let 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

878 
val constrs = sort constr_ord constrs 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

879 
val constr_pairs = all_distinct_unordered_pairs_of constrs 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

880 
in 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

881 
map (pair EQUAL) (constrs ~~ constrs) @ 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

882 
map (pair LESS) constr_pairs @ 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

883 
map (pair GREATER) (map swap constr_pairs) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

884 
> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

885 
nfas dtypes) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

886 
end 
38126  887 

888 
val min_sym_break_card = 7 

889 

890 
fun sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk 

891 
rel_table nfas dtypes = 

892 
if datatype_sym_break = 0 then 

893 
[] 

894 
else 

895 
maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas 

896 
dtypes) 

897 
(dtypes > filter is_datatype_good_and_old 

898 
> filter (fn {constrs = [_], ...} => false 

38127  899 
 {card, constrs, ...} => 
900 
card >= min_sym_break_card andalso 

901 
forall (forall (not o is_higher_order_type) 

902 
o binder_types o snd o #const) constrs) 

38126  903 
> (fn dtypes' => 
904 
dtypes' 

905 
> length dtypes' > datatype_sym_break 

906 
? (sort (rev_order o datatype_ord) 

907 
#> take datatype_sym_break))) 

33192  908 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

909 
fun sel_axiom_for_sel hol_ctxt binarize j0 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

910 
(kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...}) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

911 
rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec) 
33192  912 
n = 
913 
let 

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

914 
val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

915 
val (r, R, _) = const_triple rel_table x 
33192  916 
val R2 = dest_Func R > snd 
917 
val z = (epsilon  delta, delta + j0) 

918 
in 

919 
if exclusive then 

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

921 
else 

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

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

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

33192  926 
end 
927 
end 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

928 
fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table 
33192  929 
(constr as {const, delta, epsilon, explicit_max, ...}) = 
930 
let 

931 
val honors_explicit_max = 

932 
explicit_max < 0 orelse epsilon  delta <= explicit_max 

933 
in 

934 
if explicit_max = 0 then 

935 
[formula_for_bool honors_explicit_max] 

936 
else 

937 
let 

35178  938 
val dom_r = discr_rel_expr rel_table const 
33192  939 
val max_axiom = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

940 
if honors_explicit_max then 
34126  941 
KK.True 
38121
a9d96531c2ee
gracefully handle the case where no integers occur in the formula and the "max" option is used
blanchet
parents:
37476
diff
changeset

942 
else if bits = 0 orelse 
a9d96531c2ee
gracefully handle the case where no integers occur in the formula and the "max" option is used
blanchet
parents:
37476
diff
changeset

943 
is_twos_complement_representable bits (epsilon  delta) then 
35178  944 
KK.LE (KK.Cardinality dom_r, KK.Num explicit_max) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

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

948 
" too small for \"max\"") 
33192  949 
in 
950 
max_axiom :: 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

951 
map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr) 
33192  952 
(index_seq 0 (num_sels_for_constr_type (snd const))) 
953 
end 

954 
end 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

955 
fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table 
38126  956 
({constrs, ...} : datatype_spec) = 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

957 
maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs 
33192  958 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

959 
fun uniqueness_axiom_for_constr hol_ctxt binarize 
33192  960 
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} 
961 
: kodkod_constrs) rel_table ({const, ...} : constr_spec) = 

962 
let 

963 
fun conjunct_for_sel r = 

34126  964 
kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r) 
33192  965 
val num_sels = num_sels_for_constr_type (snd const) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

966 
val triples = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

967 
map (const_triple rel_table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

968 
o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

969 
(~1 upto num_sels  1) 
33192  970 
val set_r = triples > hd > #1 
971 
in 

972 
if num_sels = 0 then 

973 
kk_lone set_r 

974 
else 

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

34126  978 
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1)))) 
33192  979 
end 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

980 
fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table 
38126  981 
({constrs, ...} : datatype_spec) = 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

982 
map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs 
33192  983 

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

985 
fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...}) 

986 
rel_table 

38126  987 
({card, constrs, ...} : datatype_spec) = 
33192  988 
if forall #exclusive constrs then 
989 
[Integer.sum (map effective_constr_max constrs) = card > formula_for_bool] 

990 
else 

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

34126  992 
[kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)), 
33192  993 
kk_disjoint_sets kk rs] 
994 
end 

995 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

996 
fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = [] 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

997 
 other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

998 
(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

999 
let val j0 = offset_of_type ofs typ in 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

1000 
sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @ 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

1001 
uniqueness_axioms_for_datatype hol_ctxt binarize 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

1002 
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

1003 
end 
33192  1004 

38126  1005 
fun declarative_axioms_for_datatypes hol_ctxt binarize datatype_sym_break bits 
1006 
ofs kk rel_table dtypes = 

1007 
let 

1008 
val nfas = 

1009 
dtypes > map_filter (nfa_entry_for_datatype hol_ctxt binarize kk 

1010 
rel_table dtypes) 

1011 
> strongly_connected_sub_nfas 

1012 
in 

1013 
acyclicity_axioms_for_datatypes kk nfas @ 

1014 
sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk 

1015 
rel_table nfas dtypes @ 

1016 
maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table) 

1017 
dtypes 

1018 
end 

33192  1019 

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

1020 
fun kodkod_formula_from_nut ofs 
33192  1021 
(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

1022 
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

1023 
kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union, 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

1024 
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

1025 
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

1026 
kk_nat_less, kk_int_less, ...}) u = 
33192  1027 
let 
1028 
val main_j0 = offset_of_type ofs bool_T 

1029 
val bool_j0 = main_j0 

1030 
val bool_atom_R = Atom (2, main_j0) 

34126  1031 
val false_atom = KK.Atom bool_j0 
1032 
val true_atom = KK.Atom (bool_j0 + 1) 

33192  1033 

1034 
fun formula_from_opt_atom polar j0 r = 

1035 
case polar of 

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

33192  1038 
val formula_from_atom = formula_from_opt_atom Pos 
1039 

1040 
val unpack_formulas = 

1041 
map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1 

1042 
fun kk_vect_set_bool_op connective k r1 r2 = 

1043 
fold1 kk_and (map2 connective (unpack_formulas k r1) 

1044 
(unpack_formulas k r2)) 

1045 

1046 
fun to_f u = 

1047 
case rep_of u of 

1048 
Formula polar => 

1049 
(case u of 

34126  1050 
Cst (False, _, _) => KK.False 
1051 
 Cst (True, _, _) => KK.True 

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

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

1053 
kk_not (to_f_with_polarity (flip_polarity polar) u1) 
33192  1054 
 Op1 (Finite, _, _, u1) => 
1055 
let val opt1 = is_opt_rep (rep_of u1) in 

1056 
case polar of 

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

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

1058 
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

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

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

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

1066 
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

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

1068 
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

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

1070 
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

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

1072 
kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
33192  1073 
 Op2 (Less, T, Formula polar, u1, u2) => 
1074 
formula_from_opt_atom polar bool_j0 

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

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

1077 
let 

1078 
val dom_T = domain_type (type_of u1) 

1079 
val R1 = rep_of u1 

1080 
val R2 = rep_of u2 

1081 
val (dom_R, ran_R) = 

1082 
case min_rep R1 R2 of 

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

1083 
Func Rp => Rp 
33192  1084 
 R => (Atom (card_of_domain_from_rep 2 R, 
1085 
offset_of_type ofs dom_T), 

1086 
if is_opt_rep R then Opt bool_atom_R else Formula Neut) 

1087 
val set_R = Func (dom_R, ran_R) 

1088 
in 

1089 
if not (is_opt_rep ran_R) then 

1090 
to_set_bool_op kk_implies kk_subset u1 u2 

1091 
else if polar = Neut then 

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

1092 
raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u]) 
33192  1093 
else 
1094 
let 

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

1095 
(* FIXME: merge with similar code below *) 
33192  1096 
fun set_to_r widen u = 
1097 
if widen then 

1098 
kk_difference (full_rel_for_rep dom_R) 

1099 
(kk_join (to_rep set_R u) false_atom) 

1100 
else 

1101 
kk_join (to_rep set_R u) true_atom 

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

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

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

1105 
end 

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

1107 
(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

1108 
Formula polar => 
33192  1109 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
1110 
 min_R => 

1111 
let 

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

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

1114 
 args _ = [] 

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

1116 
in 

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

1117 
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

1118 
is_eval_name u1 then 
33192  1119 
fold (kk_or o (kk_no o to_r)) opt_arg_us 
1120 
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)) 

1121 
else 

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

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

1124 
 Op2 (Eq, _, _, u1, u2) => 
33192  1125 
(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

1126 
Formula polar => 
33192  1127 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
1128 
 min_R => 

1129 
if is_opt_rep min_R then 

1130 
if polar = Neut then 

1131 
(* continuation of hackish optimization *) 

1132 
kk_rel_eq (to_rep min_R u1) (to_rep min_R u2) 

1133 
else if is_Cst Unrep u1 then 

1134 
to_could_be_unrep (polar = Neg) u2 

1135 
else if is_Cst Unrep u2 then 

1136 
to_could_be_unrep (polar = Neg) u1 

1137 
else 

1138 
let 

1139 
val r1 = to_rep min_R u1 

1140 
val r2 = to_rep min_R u2 

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

1142 
in 

1143 
(if polar = Pos then 

1144 
if not both_opt then 

1145 
kk_rel_eq r1 r2 

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

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

1147 
arity_of_rep min_R = 1 then 
33192  1148 
kk_some (kk_intersect r1 r2) 
1149 
else 

1150 
raise SAME () 

1151 
else 

1152 
if is_lone_rep min_R then 

1153 
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

1154 
kk_lone (kk_union r1 r2) 
33192  1155 
else if not both_opt then 
1156 
(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

1157 
> kk_subset 
33192  1158 
else 
1159 
raise SAME () 

1160 
else 

1161 
raise SAME ()) 

1162 
handle SAME () => 

1163 
formula_from_opt_atom polar bool_j0 

1164 
(to_guard [u1, u2] bool_atom_R 

1165 
(rel_expr_from_formula kk bool_atom_R 

1166 
(kk_rel_eq r1 r2))) 

1167 
end 

1168 
else 

1169 
let 

1170 
val r1 = to_rep min_R u1 

1171 
val r2 = to_rep min_R u2 

1172 
in 

1173 
if is_one_rep min_R then 

1174 
let 

1175 
val rs1 = unpack_products r1 

1176 
val rs2 = unpack_products r2 

1177 
in 

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

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

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

1180 
= map KK.arity_of_rel_expr rs2 then 
33192  1181 
fold1 kk_and (map2 kk_subset rs1 rs2) 
1182 
else 

1183 
kk_subset r1 r2 

1184 
end 

1185 
else 

1186 
kk_rel_eq r1 r2 

1187 
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

1188 
 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

1189 
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

1190 
(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

1191 
 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

1192 
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

1193 
(Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2)) 
33192  1194 
 Op2 (Apply, T, _, u1, u2) => 
1195 
(case (polar, rep_of u1) of 

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

1197 
 _ => 

1198 
to_f_with_polarity polar 

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

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

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

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

1203 
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

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

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

1208 
 _ => raise NUT ("Nitpick_Kodkod.to_f", [u]) 
33192  1209 
and to_f_with_polarity polar u = 
1210 
case rep_of u of 

1211 
Formula _ => to_f u 

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

1213 
 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

1214 
 _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u]) 
33192  1215 
and to_r u = 
1216 
case u of 

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

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

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

1219 
 Cst (Iden, _, Func (Struct [R1, R2], Formula Neut)) => 
33192  1220 
if R1 = R2 andalso arity_of_rep R1 = 1 then 
34126  1221 
kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ) 
33192  1222 
else 
1223 
let 

1224 
val schema1 = atom_schema_of_rep R1 

1225 
val schema2 = atom_schema_of_rep R2 

1226 
val arity1 = length schema1 

1227 
val arity2 = length schema2 

1228 
val r1 = fold1 kk_product (unary_var_seq 0 arity1) 

1229 
val r2 = fold1 kk_product (unary_var_seq arity1 arity2) 

1230 
val min_R = min_rep R1 R2 

1231 
in 

1232 
kk_comprehension 

1233 
(decls_for_atom_schema 0 (schema1 @ schema2)) 

1234 
(kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1) 

1235 
(rel_expr_from_rel_expr kk min_R R2 r2)) 

1236 
end 

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

1237 
 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

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

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

1241 
if is_word_type T then 
34126  1242 
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

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

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

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

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

1251 
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) 
33192  1252 
 Cst (Unknown, _, R) => empty_rel_for_rep R 
1253 
 Cst (Unrep, _, R) => empty_rel_for_rep R 

34126
8a2c5d7aff51
polished Nitpick's binary integer support etc.;
