author  blanchet 
Wed, 17 Feb 2010 20:46:50 +0100  
changeset 35190  ce653cc27a94 
parent 35185  9b8f351cced6 
child 35220  2bcdae5f4fdb 
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 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

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

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

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

16 
type nfa_table = nfa_entry list 

17 

18 
structure NameTable : TABLE 

19 

20 
val univ_card : 

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

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

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

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

26 
val sequential_int_bounds : int > Kodkod.int_bound list 

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

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

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

31 
val bound_for_sel_rel : 

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

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

34 
val declarative_axiom_for_plain_rel : kodkod_constrs > nut > Kodkod.formula 

35 
val declarative_axioms_for_datatypes : 

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

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

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35179
diff
changeset

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

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

42 
structure Nitpick_Kodkod : NITPICK_KODKOD = 
33192  43 
struct 
44 

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

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

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

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

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

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

50 
open Nitpick_Nut 
33192  51 

34126  52 
structure KK = Kodkod 
53 

54 
type nfa_transition = KK.rel_expr * typ 

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

57 

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

59 

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

33192  62 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

103 
(* int > int > unit *) 

104 
fun check_arity univ_card n = 

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

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

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

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

111 

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

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

33192  119 

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

122 
(* rep > KK.tuple_set *) 

33192  123 
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep 
124 

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

127 
(* int > KK.int_bound list *) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

157 
val max_table_size = 65536 

158 

159 
(* int > unit *) 

160 
fun check_table_size k = 

161 
if k > max_table_size then 

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

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

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

166 

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

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

171 
if j2 >= 0 then 

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

173 
else 

174 
NONE 

175 
end) (index_seq 0 k)) 

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

179 
map_filter (fn j => let 

180 
val j1 = j div k 

181 
val j2 = j  j1 * k 

182 
val j3 = f (j1, j2) 

183 
in 

184 
if j3 >= 0 then 

185 
SOME (kk_tuple debug univ_card 

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

187 
else 

188 
NONE 

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

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

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

194 
map_filter (fn j => let 

195 
val j1 = j div k 

196 
val j2 = j  j1 * k 

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

198 
in 

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

200 
SOME (kk_tuple debug univ_card 

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

202 
j4 + res_j0]) 

203 
else 

204 
NONE 

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

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

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

210 
tabulate_op2 debug univ_card (k, j0) j0 

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

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

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

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

217 

218 
(* int * int > int *) 

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

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

221 
fun isa_gcd (m, 0) = m 

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

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

224 
val isa_zgcd = isa_gcd o pairself abs 

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

226 
fun isa_norm_frac (m, n) = 

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

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

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

230 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

270 
else 

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

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

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

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

277 
j0 x 

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

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

283 
o built_in_rels_in_formula 

284 

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

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

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

287 
short_name nick ^ 
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

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

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

290 

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

294 
if nick = @{const_name bisim_iterator_max} then 

295 
case R of 

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

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

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

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

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

306 
nick)) = 

307 
let 

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

309 
constr_spec dtypes (original_name nick, T1) 

310 
in 

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

312 
if explicit_max = 0 then 

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

319 
[KK.TupleSet [], 
35178  320 
if T1 = T2 andalso epsilon > delta andalso 
35179
4b198af5beb5
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents:
35178
diff
changeset

321 
(datatype_spec dtypes T1 > the > pairf #co #standard) 
4b198af5beb5
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents:
35178
diff
changeset

322 
= (false, true) then 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

323 
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

324 
> map (fn j => 
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 (KK.TupleSet [Kodkod.Tuple [j + j0]], 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

326 
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

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

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

329 
KK.TupleProduct (ts, upper_bound_for_rep R2)] 
33192  330 
end) 
331 
end 

332 
 bound_for_sel_rel _ _ _ u = 

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

333 
raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u]) 
33192  334 

34126  335 
(* KK.bound list > KK.bound list *) 
33192  336 
fun merge_bounds bs = 
337 
let 

34126  338 
(* KK.bound > int *) 
33192  339 
fun arity (zs, _) = fst (fst (hd zs)) 
34126  340 
(* KK.bound list > KK.bound > KK.bound list > KK.bound list *) 
33192  341 
fun add_bound ds b [] = List.revAppend (ds, [b]) 
342 
 add_bound ds b (c :: cs) = 

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

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

345 
else 

346 
add_bound (c :: ds) b cs 

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

348 

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

33192  351 

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

354 
(* rep > KK.rel_expr list *) 

33192  355 
fun all_singletons_for_rep R = 
356 
if is_lone_rep R then 

357 
all_combinations_for_rep R > map singleton_from_combination 

358 
else 

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

359 
raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R]) 
33192  360 

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

33192  363 
unpack_products r1 @ unpack_products r2 
364 
 unpack_products r = [r] 

34126  365 
fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2 
33192  366 
 unpack_joins r = [r] 
367 

34126  368 
(* rep > KK.rel_expr *) 
33192  369 
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep 
370 
fun full_rel_for_rep R = 

371 
case atom_schema_of_rep R of 

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

372 
[] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R]) 
34126  373 
 schema => foldl1 KK.Product (map KK.AtomSeq schema) 
33192  374 

34126  375 
(* int > int list > KK.decl list *) 
33192  376 
fun decls_for_atom_schema j0 schema = 
34126  377 
map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x)) 
33192  378 
(index_seq j0 (length schema)) schema 
379 

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

381 

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

385 
let val body_R = body_rep R in 

386 
if is_lone_rep body_R then 

387 
let 

388 
val binder_schema = atom_schema_of_reps (binder_reps R) 

389 
val body_schema = atom_schema_of_rep body_R 

390 
val one = is_one_rep body_R 

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

393 
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

394 
length body_schema = 1 then 
34126  395 
(if one then KK.Function else KK.Functional) 
396 
(the opt_x, KK.AtomSeq (hd binder_schema), 

397 
KK.AtomSeq (hd body_schema)) 

33192  398 
else 
399 
let 

400 
val decls = decls_for_atom_schema ~1 binder_schema 

401 
val vars = unary_var_seq ~1 (length binder_schema) 

402 
val kk_xone = if one then kk_one else kk_lone 

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

404 
end 

405 
else 

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

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

412 
else if x = nat_add_rel then 
33192  413 
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

414 
else if x = nat_multiply_rel then 
33192  415 
formula_for_bool (card_of_rep (body_rep R) <= 2) 
416 
else 

417 
d_n_ary_function kk R r 

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

418 
else if x = nat_subtract_rel then 
34126  419 
KK.True 
33192  420 
else 
421 
d_n_ary_function kk R r 

422 
 kk_n_ary_function kk R r = d_n_ary_function kk R r 

423 

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

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

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

429 

34126  430 
(* int > kodkod_constrs > (KK.rel_expr > KK.rel_expr) > KK.rel_expr 
431 
> KK.rel_expr *) 

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

432 
fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r = 
33192  433 
if inline_rel_expr r then 
434 
f r 

435 
else 

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

33192  438 
end 
34126  439 
(* kodkod_constrs > (KK.rel_expr > KK.rel_expr) > KK.rel_expr 
440 
> KK.rel_expr *) 

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

441 
val single_rel_rel_let = basic_rel_rel_let 0 
34126  442 
(* kodkod_constrs > (KK.rel_expr > KK.rel_expr > KK.rel_expr) > KK.rel_expr 
443 
> KK.rel_expr > KK.rel_expr *) 

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

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

445 
single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1 
34126  446 
(* kodkod_constrs > (KK.rel_expr > KK.rel_expr > KK.rel_expr > KK.rel_expr) 
447 
> KK.rel_expr > KK.rel_expr > KK.rel_expr > KK.rel_expr *) 

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

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

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 

34126  452 
(* kodkod_constrs > int > KK.formula > KK.rel_expr *) 
33192  453 
fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f = 
34126  454 
kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0) 
455 
(* kodkod_constrs > rep > KK.formula > KK.rel_expr *) 

33192  456 
fun rel_expr_from_formula kk R f = 
457 
case unopt_rep R of 

458 
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

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

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

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

465 
chunk_arity) 

466 

34126  467 
(* kodkod_constrs > bool > rep > rep > KK.rel_expr > KK.rel_expr 
468 
> KK.rel_expr *) 

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

471 
res_R r1 r2 = 

472 
case arity_of_rep R1 of 

473 
1 => kk_join r1 r2 

474 
 arity1 => 

475 
let 

476 
val unpacked_rs1 = 

477 
if inline_rel_expr r1 then unpack_vect_in_chunks kk 1 arity1 r1 

478 
else unpack_products r1 

479 
in 

480 
if one andalso length unpacked_rs1 = arity1 then 

481 
fold kk_join unpacked_rs1 r2 

482 
else 

483 
kk_project_seq 

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

485 
arity1 (arity_of_rep res_R) 

486 
end 

487 

34126  488 
(* kodkod_constrs > rep > rep > KK.rel_expr > KK.rel_expr list 
489 
> KK.rel_expr list > KK.rel_expr *) 

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

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

493 

494 
val lone_rep_fallback_max_card = 4096 

495 
val some_j0 = 0 

496 

34126  497 
(* kodkod_constrs > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  498 
fun lone_rep_fallback kk new_R old_R r = 
499 
if old_R = new_R then 

500 
r 

501 
else 

502 
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

503 
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

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

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

507 
"too high cardinality (" ^ string_of_int card ^ ")") 
33192  508 
else 
509 
kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R) 

510 
(all_singletons_for_rep new_R) 

511 
else 

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

512 
raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R]) 
33192  513 
end 
34126  514 
(* kodkod_constrs > int * int > rep > KK.rel_expr > KK.rel_expr *) 
33192  515 
and atom_from_rel_expr kk (x as (k, j0)) old_R r = 
516 
case old_R of 

517 
Func (R1, R2) => 

518 
let 

519 
val dom_card = card_of_rep R1 

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

521 
in 

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

523 
(vect_from_rel_expr kk dom_card R2' old_R r) 

524 
end 

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

525 
 Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R]) 
33192  526 
 _ => lone_rep_fallback kk (Atom x) old_R r 
34126  527 
(* kodkod_constrs > rep list > rep > KK.rel_expr > KK.rel_expr *) 
33192  528 
and struct_from_rel_expr kk Rs old_R r = 
529 
case old_R of 

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

531 
 Struct Rs' => 

532 
let 

533 
val Rs = filter (not_equal Unit) Rs 

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

535 
in 

536 
if Rs' = Rs then 

537 
r 

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

539 
let 

540 
val old_arities = map arity_of_rep Rs' 

541 
val old_offsets = offset_list old_arities 

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

543 
in 

544 
fold1 (#kk_product kk) 

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

546 
end 

547 
else 

548 
lone_rep_fallback kk (Struct Rs) old_R r 

549 
end 

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

550 
 _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R]) 
34126  551 
(* kodkod_constrs > int > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  552 
and vect_from_rel_expr kk k R old_R r = 
553 
case old_R of 

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

555 
 Vect (k', R') => 

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

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

558 
 Func (R1, Formula Neut) => 

559 
if k = card_of_rep R1 then 

560 
fold1 (#kk_product kk) 

561 
(map (fn arg_r => 

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

563 
(all_singletons_for_rep R1)) 

564 
else 

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

565 
raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
33192  566 
 Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r 
567 
 Func (R1, R2) => 

568 
fold1 (#kk_product kk) 

569 
(map (fn arg_r => 

570 
rel_expr_from_rel_expr kk R R2 

571 
(kk_n_fold_join kk true R1 R2 arg_r r)) 

572 
(all_singletons_for_rep R1)) 

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

573 
 _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
34126  574 
(* kodkod_constrs > rep > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  575 
and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r = 
576 
let 

577 
val dom_card = card_of_rep R1 

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

579 
in 

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

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

582 
end 

583 
 func_from_no_opt_rel_expr kk Unit R2 old_R r = 

584 
(case old_R of 

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

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

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

588 
(case unopt_rep R2 of 

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

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

590 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  591 
[old_R, Func (Unit, R2)])) 
592 
 Func (R1', R2') => 

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

594 
(arity_of_rep R2')) 

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

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

598 
(case old_R of 

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

600 
let 

601 
val args_rs = all_singletons_for_rep R1 

602 
val vals_rs = unpack_vect_in_chunks kk 1 k r 

34126  603 
(* KK.rel_expr > KK.rel_expr > KK.rel_expr *) 
33192  604 
fun empty_or_singleton_set_for arg_r val_r = 
34126  605 
#kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r) 
33192  606 
in 
607 
fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs) 

608 
end 

609 
 Func (R1', Formula Neut) => 

610 
if R1 = R1' then 

611 
r 

612 
else 

613 
let 

614 
val schema = atom_schema_of_rep R1 

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

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

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

619 
#kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) 
33192  620 
end 
621 
 Func (Unit, (Atom (2, j0))) => 

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

625 
func_from_no_opt_rel_expr kk R1 (Formula Neut) 

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

627 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  628 
[old_R, Func (R1, Formula Neut)])) 
629 
 func_from_no_opt_rel_expr kk R1 R2 old_R r = 

630 
case old_R of 

631 
Vect (k, R) => 

632 
let 

633 
val args_rs = all_singletons_for_rep R1 

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

635 
> map (rel_expr_from_rel_expr kk R2 R) 

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

637 
 Func (R1', Formula Neut) => 

638 
(case R2 of 

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

640 
let val schema = atom_schema_of_rep R1 in 

641 
if length schema = 1 then 

34126  642 
#kk_override kk (#kk_product kk (KK.AtomSeq (hd schema)) 
643 
(KK.Atom j0)) 

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

33192  645 
else 
646 
let 

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

648 
> rel_expr_from_rel_expr kk R1' R1 

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

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

653 
(#kk_subset kk r2 r3) 
33192  654 
end 
655 
end 

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

656 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  657 
[old_R, Func (R1, R2)])) 
658 
 Func (Unit, R2') => 

659 
let val j0 = some_j0 in 

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

34126  661 
(#kk_product kk (KK.Atom j0) r) 
33192  662 
end 
663 
 Func (R1', R2') => 

664 
if R1 = R1' andalso R2 = R2' then 

665 
r 

666 
else 

667 
let 

668 
val dom_schema = atom_schema_of_rep R1 

669 
val ran_schema = atom_schema_of_rep R2 

670 
val dom_prod = fold1 (#kk_product kk) 

671 
(unary_var_seq ~1 (length dom_schema)) 

672 
> rel_expr_from_rel_expr kk R1' R1 

673 
val ran_prod = fold1 (#kk_product kk) 

674 
(unary_var_seq (~(length dom_schema)  1) 

675 
(length ran_schema)) 

676 
> rel_expr_from_rel_expr kk R2' R2 

677 
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

678 
val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk 
33192  679 
in 
680 
#kk_comprehension kk (decls_for_atom_schema ~1 

681 
(dom_schema @ ran_schema)) 

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

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

684 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  685 
[old_R, Func (R1, R2)]) 
34126  686 
(* kodkod_constrs > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  687 
and rel_expr_from_rel_expr kk new_R old_R r = 
688 
let 

689 
val unopt_old_R = unopt_rep old_R 

690 
val unopt_new_R = unopt_rep new_R 

691 
in 

692 
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

693 
raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R]) 
33192  694 
else if unopt_new_R = unopt_old_R then 
695 
r 

696 
else 

697 
(case unopt_new_R of 

698 
Atom x => atom_from_rel_expr kk x 

699 
 Struct Rs => struct_from_rel_expr kk Rs 

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

701 
 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

702 
 _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", 
33192  703 
[old_R, new_R])) 
704 
unopt_old_R r 

705 
end 

34126  706 
(* kodkod_constrs > rep > rep > rep > KK.rel_expr > KK.rel_expr *) 
33192  707 
and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2)) 
708 

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

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

713 
else 

714 
signed_bit_word_sel_rel)) 

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

716 
val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom 

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

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

718 
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

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

720 
kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R)) 
34126  721 
(kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1))) 
722 
(KK.Bits i)) 

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

723 

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

34126  727 
(KK.Rel x) 
33192  728 
 declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs) 
729 
(FreeRel (x, _, R, _)) = 

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

732 
else KK.True 

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

734 
raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u]) 
33192  735 

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

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

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

34126  742 
(* nut NameTable.table > styp > KK.rel_expr *) 
33192  743 
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr 
744 

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

745 
(* hol_context > bool > kodkod_constrs > nut NameTable.table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

746 
> dtype_spec list > styp > int > nfa_transition list *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

747 
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

748 
({kk_project, ...} : kodkod_constrs) rel_table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

749 
(dtypes : dtype_spec list) constr_x n = 
33192  750 
let 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

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

752 
binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n 
33192  753 
val (r, R, arity) = const_triple rel_table x 
754 
val type_schema = type_schema_of_rep T R 

755 
in 

756 
map_filter (fn (j, T) => 

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

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

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

761 
(* hol_context > bool > kodkod_constrs > nut NameTable.table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

762 
> dtype_spec list > styp > nfa_transition list *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

763 
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

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

765 
maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x) 
33192  766 
(index_seq 0 (num_sels_for_constr_type T)) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

767 
(* hol_context > bool > kodkod_constrs > nut NameTable.table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

768 
> dtype_spec list > dtype_spec > nfa_entry option *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

769 
fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : dtype_spec) = NONE 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

770 
 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

771 
 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

772 
 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

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

774 
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

775 
dtypes o #const) constrs) 
33192  776 

34126  777 
val empty_rel = KK.Product (KK.None, KK.None) 
33192  778 

34126  779 
(* nfa_table > typ > typ > KK.rel_expr list *) 
35177  780 
fun direct_path_rel_exprs nfa start_T final_T = 
781 
case AList.lookup (op =) nfa final_T of 

782 
SOME trans => map fst (filter (curry (op =) start_T o snd) trans) 

33192  783 
 NONE => [] 
34126  784 
(* kodkod_constrs > nfa_table > typ list > typ > typ > KK.rel_expr *) 
35177  785 
and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T 
786 
final_T = 

787 
fold kk_union (direct_path_rel_exprs nfa start_T final_T) 

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

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

790 
kk_union (any_path_rel_expr kk nfa Ts start_T final_T) 

791 
(knot_path_rel_expr kk nfa Ts start_T T final_T) 

33192  792 
(* kodkod_constrs > nfa_table > typ list > typ > typ > typ 
34126  793 
> KK.rel_expr *) 
35177  794 
and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts 
795 
start_T knot_T final_T = 

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

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

798 
(any_path_rel_expr kk nfa Ts start_T knot_T) 

34126  799 
(* kodkod_constrs > nfa_table > typ list > typ > KK.rel_expr *) 
35177  800 
and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T = 
801 
fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel 

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

803 
start_T = 

804 
if start_T = T then 

805 
kk_closure (loop_path_rel_expr kk nfa Ts start_T) 

33192  806 
else 
35177  807 
kk_union (loop_path_rel_expr kk nfa Ts start_T) 
808 
(knot_path_rel_expr kk nfa Ts start_T T start_T) 

33192  809 

810 
(* nfa_table > unit NfaGraph.T *) 

811 
fun graph_for_nfa nfa = 

812 
let 

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

35177  814 
fun new_node T = perhaps (try (NfaGraph.new_node (T, ()))) 
33192  815 
(* nfa_table > unit NfaGraph.T > unit NfaGraph.T *) 
816 
fun add_nfa [] = I 

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

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

820 
new_node T' o new_node T 

33192  821 
in add_nfa nfa NfaGraph.empty end 
822 

823 
(* nfa_table > nfa_table list *) 

824 
fun strongly_connected_sub_nfas nfa = 

825 
nfa > graph_for_nfa > NfaGraph.strong_conn 

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

827 

35177  828 
(* kodkod_constrs > dtype_spec list > nfa_table > typ > KK.formula *) 
829 
fun acyclicity_axiom_for_datatype kk dtypes nfa start_T = 

33192  830 
#kk_no kk (#kk_intersect kk 
35177  831 
(loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

832 
(* hol_context > bool > kodkod_constrs > nut NameTable.table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

833 
> dtype_spec list > KK.formula list *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

834 
fun acyclicity_axioms_for_datatypes 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

835 
map_filter (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

836 
dtypes 
33192  837 
> strongly_connected_sub_nfas 
35177  838 
> maps (fn nfa => 
839 
map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa) 

33192  840 

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

841 
(* hol_context > bool > int > kodkod_constrs > nut NameTable.table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

842 
> KK.rel_expr > constr_spec > int > KK.formula *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

843 
fun sel_axiom_for_sel hol_ctxt binarize j0 
35178  844 
(kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no, 
33982  845 
kk_join, ...}) rel_table dom_r 
33192  846 
({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec) 
847 
n = 

848 
let 

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

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

850 
binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n 
33192  851 
val (r, R, arity) = const_triple rel_table x 
852 
val R2 = dest_Func R > snd 

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

854 
in 

855 
if exclusive then 

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

857 
else 

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

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

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

33192  862 
end 
863 
end 

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

864 
(* hol_context > bool > int > int > kodkod_constrs > nut NameTable.table 
34126  865 
> constr_spec > KK.formula list *) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

866 
fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table 
33192  867 
(constr as {const, delta, epsilon, explicit_max, ...}) = 
868 
let 

869 
val honors_explicit_max = 

870 
explicit_max < 0 orelse epsilon  delta <= explicit_max 

871 
in 

872 
if explicit_max = 0 then 

873 
[formula_for_bool honors_explicit_max] 

874 
else 

875 
let 

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

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

880 
else if is_twos_complement_representable bits (epsilon  delta) then 
35178  881 
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

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

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

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

885 
" too small for \"max\"") 
33192  886 
in 
887 
max_axiom :: 

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

888 
map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr) 
33192  889 
(index_seq 0 (num_sels_for_constr_type (snd const))) 
890 
end 

891 
end 

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

892 
(* hol_context > bool > int > int > kodkod_constrs > nut NameTable.table 
34126  893 
> dtype_spec > KK.formula list *) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

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

896 
maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs 
33192  897 

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

898 
(* hol_context > bool > kodkod_constrs > nut NameTable.table > constr_spec 
34126  899 
> KK.formula list *) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

900 
fun uniqueness_axiom_for_constr hol_ctxt binarize 
33192  901 
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} 
902 
: kodkod_constrs) rel_table ({const, ...} : constr_spec) = 

903 
let 

34126  904 
(* KK.rel_expr > KK.formula *) 
33192  905 
fun conjunct_for_sel r = 
34126  906 
kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r) 
33192  907 
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

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

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

910 
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

911 
(~1 upto num_sels  1) 
33192  912 
val j0 = case triples > hd > #2 of 
913 
Func (Atom (_, j0), _) => j0 

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

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

915 
[R]) 
33192  916 
val set_r = triples > hd > #1 
917 
in 

918 
if num_sels = 0 then 

919 
kk_lone set_r 

920 
else 

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

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

926 
(* hol_context > bool > kodkod_constrs > nut NameTable.table > dtype_spec 
34126  927 
> KK.formula list *) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

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

930 
map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs 
33192  931 

932 
(* constr_spec > int *) 

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

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

34126  935 
> KK.formula list *) 
33192  936 
fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...}) 
937 
rel_table 

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

939 
if forall #exclusive constrs then 

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

941 
else 

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

34126  943 
[kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)), 
33192  944 
kk_disjoint_sets kk rs] 
945 
end 

946 

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

947 
(* hol_context > bool > int > int Typtab.table > kodkod_constrs 
34126  948 
> nut NameTable.table > dtype_spec > KK.formula list *) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

949 
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

950 
 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

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

952 
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

953 
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

954 
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

955 
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

956 
end 
33192  957 

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

958 
(* hol_context > bool > int > int Typtab.table > kodkod_constrs 
34126  959 
> nut NameTable.table > dtype_spec list > KK.formula list *) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

960 
fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

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

962 
acyclicity_axioms_for_datatypes 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

963 
maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

964 
dtypes 
33192  965 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35179
diff
changeset

966 
(* int > int Typtab.table > kodkod_constrs > nut > KK.formula *) 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35179
diff
changeset

967 
fun kodkod_formula_from_nut bits ofs 
33192  968 
(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

969 
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

970 
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

971 
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

972 
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

973 
kk_nat_less, kk_int_less, ...}) u = 
33192  974 
let 
975 
val main_j0 = offset_of_type ofs bool_T 

976 
val bool_j0 = main_j0 

977 
val bool_atom_R = Atom (2, main_j0) 

34126  978 
val false_atom = KK.Atom bool_j0 
979 
val true_atom = KK.Atom (bool_j0 + 1) 

33192  980 

34126  981 
(* polarity > int > KK.rel_expr > KK.formula *) 
33192  982 
fun formula_from_opt_atom polar j0 r = 
983 
case polar of 

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

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

33192  987 
val formula_from_atom = formula_from_opt_atom Pos 
988 

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

993 
double_rel_rel_let kk 
33192  994 
(fn r1 => fn r2 => 
995 
kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom 

996 
(kk_intersect r1 r2)) 

997 
val kk_and3 = 

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

998 
double_rel_rel_let kk 
33192  999 
(fn r1 => fn r2 => 
1000 
kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom 

1001 
(kk_intersect r1 r2)) 

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

1003 

34126  1004 
(* int > KK.rel_expr > KK.formula list *) 
33192  1005 
val unpack_formulas = 
1006 
map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1 

34126  1007 
(* (KK.formula > KK.formula > KK.formula) > int > KK.rel_expr 
1008 
> KK.rel_expr > KK.rel_expr *) 

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

1011 
(unpack_formulas k r1) (unpack_formulas k r2)) 

34126  1012 
(* (KK.formula > KK.formula > KK.formula) > int > KK.rel_expr 
1013 
> KK.rel_expr > KK.formula *) 

33192  1014 
fun kk_vect_set_bool_op connective k r1 r2 = 
1015 
fold1 kk_and (map2 connective (unpack_formulas k r1) 

1016 
(unpack_formulas k r2)) 

1017 

34126  1018 
(* nut > KK.formula *) 
33192  1019 
fun to_f u = 
1020 
case rep_of u of 

1021 
Formula polar => 

1022 
(case u of 

34126  1023 
Cst (False, _, _) => KK.False 
1024 
 Cst (True, _, _) => KK.True 

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

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

1026 
kk_not (to_f_with_polarity (flip_polarity polar) u1) 
33192  1027 
 Op1 (Finite, _, _, u1) => 
1028 
let val opt1 = is_opt_rep (rep_of u1) in 

1029 
case polar of 

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

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

1031 
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

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

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

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

1039 
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

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

1041 
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

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

1043 
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

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

1045 
kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
33192  1046 
 Op2 (Less, T, Formula polar, u1, u2) => 
1047 
formula_from_opt_atom polar bool_j0 

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

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

1050 
let 

1051 
val dom_T = domain_type (type_of u1) 

1052 
val R1 = rep_of u1 

1053 
val R2 = rep_of u2 

1054 
val (dom_R, ran_R) = 

1055 
case min_rep R1 R2 of 

1056 
Func (Unit, R') => 

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

1058 
 Func Rp => Rp 

1059 
 R => (Atom (card_of_domain_from_rep 2 R, 

1060 
offset_of_type ofs dom_T), 

1061 
if is_opt_rep R then Opt bool_atom_R else Formula Neut) 

1062 
val set_R = Func (dom_R, ran_R) 

1063 
in 

1064 
if not (is_opt_rep ran_R) then 

1065 
to_set_bool_op kk_implies kk_subset u1 u2 

1066 
else if polar = Neut then 

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

1067 
raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u]) 
33192  1068 
else 
1069 
let 

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

1070 
(* FIXME: merge with similar code below *) 
34126  1071 
(* bool > nut > KK.rel_expr *) 
33192  1072 
fun set_to_r widen u = 
1073 
if widen then 

1074 
kk_difference (full_rel_for_rep dom_R) 

1075 
(kk_join (to_rep set_R u) false_atom) 

1076 
else 

1077 
kk_join (to_rep set_R u) true_atom 

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

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

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

1081 
end 

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

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

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

1087 
 min_R => 

1088 
let 

1089 
(* nut > nut list *) 

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

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

1092 
 args _ = [] 

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

1094 
in 

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

1095 
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

1096 
is_eval_name u1 then 
33192  1097 
fold (kk_or o (kk_no o to_r)) opt_arg_us 
1098 
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)) 

1099 
else 

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

1100 
kk_subset (to_rep min_R u1) (to_rep min_R u2) 
33192  1101 
end) 
1102 
 Op2 (Eq, T, R, u1, u2) => 

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

34126  1104 
Unit => KK.True 
33192  1105 
 Formula polar => 
1106 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 

1107 
 min_R => 

1108 
if is_opt_rep min_R then 

1109 
if polar = Neut then 

1110 
(* continuation of hackish optimization *) 

1111 
kk_rel_eq (to_rep min_R u1) (to_rep min_R u2) 

1112 
else if is_Cst Unrep u1 then 

1113 
to_could_be_unrep (polar = Neg) u2 

1114 
else if is_Cst Unrep u2 then 

1115 
to_could_be_unrep (polar = Neg) u1 

1116 
else 

1117 
let 

1118 
val r1 = to_rep min_R u1 

1119 
val r2 = to_rep min_R u2 

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

1121 
in 

1122 
(if polar = Pos then 

1123 
if not both_opt then 

1124 
kk_rel_eq r1 r2 

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

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

1126 
arity_of_rep min_R = 1 then 
33192  1127 
kk_some (kk_intersect r1 r2) 
1128 
else 

1129 
raise SAME () 

1130 
else 

1131 
if is_lone_rep min_R then 

1132 
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

1133 
kk_lone (kk_union r1 r2) 
33192  1134 
else if not both_opt then 
1135 
(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

1136 
> kk_subset 
33192  1137 
else 
1138 
raise SAME () 

1139 
else 

1140 
raise SAME ()) 

1141 
handle SAME () => 

1142 
formula_from_opt_atom polar bool_j0 

1143 
(to_guard [u1, u2] bool_atom_R 

1144 
(rel_expr_from_formula kk bool_atom_R 

1145 
(kk_rel_eq r1 r2))) 

1146 
end 

1147 
else 

1148 
let 

1149 
val r1 = to_rep min_R u1 

1150 
val r2 = to_rep min_R u2 

1151 
in 

1152 
if is_one_rep min_R then 

1153 
let 

1154 
val rs1 = unpack_products r1 

1155 
val rs2 = unpack_products r2 

1156 
in 

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

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

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

1159 
= map KK.arity_of_rel_expr rs2 then 
33192  1160 
fold1 kk_and (map2 kk_subset rs1 rs2) 
1161 
else 

1162 
kk_subset r1 r2 

1163 
end 

1164 
else 

1165 
kk_rel_eq r1 r2 

1166 
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

1167 
 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

1168 
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

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

1170 
 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

1171 
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

1172 
(Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2)) 
33192  1173 
 Op2 (Apply, T, _, u1, u2) => 
1174 
(case (polar, rep_of u1) of 

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

1176 
 _ => 

1177 
to_f_with_polarity polar 

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

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

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

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

1182 
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

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

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

1187 
 _ => raise NUT ("Nitpick_Kodkod.to_f", [u]) 
34126  1188 
(* polarity > nut > KK.formula *) 
33192  1189 
and to_f_with_polarity polar u = 
1190 
case rep_of u of 

1191 
Formula _ => to_f u 

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

1193 
 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

1194 
 _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u]) 
34126  1195 
(* nut > KK.rel_expr *) 
33192  1196 
and to_r u = 
1197 
case u of 

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

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

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

1201 
if R1 = R2 andalso arity_of_rep R1 = 1 then 

34126  1202 
kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ) 
33192  1203 
else 
1204 
let 

1205 
val schema1 = atom_schema_of_rep R1 

1206 
val schema2 = atom_schema_of_rep R2 

1207 
val arity1 = length schema1 

1208 
val arity2 = length schema2 

1209 
val r1 = fold1 kk_product (unary_var_seq 0 arity1) 

1210 
val r2 = fold1 kk_product (unary_var_seq arity1 arity2) 

1211 
val min_R = min_rep R1 R2 

1212 
in 

1213 
kk_comprehension 

1214 
(decls_for_atom_schema 0 (schema1 @ schema2)) 

1215 
(kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1) 

1216 
(rel_expr_from_rel_expr kk min_R R2 r2)) 

1217 
end 

34126  1218 
 Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0 
33192  1219 
 Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) => 
1220 
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

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

1222 
if is_word_type T then 
34126  1223 
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

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

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

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

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

1232 
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) 
33192  1233 
 Cst (Unknown, _, R) => empty_rel_for_rep R 
1234 
 Cst (Unrep, _, R) => empty_rel_for_rep R 

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

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

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

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

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

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

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

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

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

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

1246 
(SOME (fn i1 => fn i2 => fn i3 => 
34126  1247 
kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2))) 
1248 
(KK.LE (KK.Num 0, KK.BitXor (i2, i3))))) 

1249 
(SOME (curry KK.Add)) 

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

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

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

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

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

1256 
(SOME (fn i1 => fn i2 => 
34126  1257 
KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2)))) 