author  blanchet 
Thu, 17 Dec 2009 15:22:11 +0100  
changeset 34124  c4628a1dcf75 
parent 34121  5e831d805118 
child 34126  8a2c5d7aff51 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_kodkod.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2008, 2009 

4 

5 
Kodkod problem generator part of Kodkod. 

6 
*) 

7 

8 
signature NITPICK_KODKOD = 

9 
sig 

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

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

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

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

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

16 
type nfa_table = nfa_entry list 

17 

18 
structure NameTable : TABLE 

19 

20 
val univ_card : 

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

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

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

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

26 
val sequential_int_bounds : int > Kodkod.int_bound list 

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

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

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

31 
val bound_for_sel_rel : 

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

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

34 
val declarative_axiom_for_plain_rel : kodkod_constrs > nut > Kodkod.formula 

35 
val declarative_axioms_for_datatypes : 

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

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

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

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

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

42 
structure Nitpick_Kodkod : NITPICK_KODKOD = 
33192  43 
struct 
44 

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

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

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

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

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

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

50 
open Nitpick_Nut 
33192  51 

52 
type nfa_transition = Kodkod.rel_expr * typ 

53 
type nfa_entry = typ * nfa_transition list 

54 
type nfa_table = nfa_entry list 

55 

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

57 

58 
(* int > Kodkod.int_expr list *) 

59 
fun flip_nums n = index_seq 1 n @ [0] > map Kodkod.Num 

60 

61 
(* int > int > int > Kodkod.bound list > Kodkod.formula > int *) 

62 
fun univ_card nat_card int_card main_j0 bounds formula = 

63 
let 

64 
(* Kodkod.rel_expr > int > int *) 

65 
fun rel_expr_func r k = 

66 
Int.max (k, case r of 

67 
Kodkod.Atom j => j + 1 

68 
 Kodkod.AtomSeq (k', j0) => j0 + k' 

69 
 _ => 0) 

70 
(* Kodkod.tuple > int > int *) 

71 
fun tuple_func t k = 

72 
case t of 

73 
Kodkod.Tuple js => fold Integer.max (map (Integer.add 1) js) k 

74 
 _ => k 

75 
(* Kodkod.tuple_set > int > int *) 

76 
fun tuple_set_func ts k = 

77 
Int.max (k, case ts of Kodkod.TupleAtomSeq (k', j0) => j0 + k'  _ => 0) 

78 
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, 

79 
int_expr_func = K I} 

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

81 
val card = fold (Kodkod.fold_bound expr_F tuple_F) bounds 1 

82 
> Kodkod.fold_formula expr_F formula 

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

84 

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

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

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

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

88 
(* Kodkod.int_expr > unit > unit *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

89 
fun int_expr_func (Kodkod.Num k) () = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

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

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

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

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

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

97 
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

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

99 
in Kodkod.fold_formula expr_F formula () end 
33192  100 

101 
(* int > int > unit *) 

102 
fun check_arity univ_card n = 

103 
if n > Kodkod.max_arity univ_card then 

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

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

105 
"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

106 
\cardinality " ^ string_of_int univ_card) 
33192  107 
else 
108 
() 

109 

110 
(* bool > int > int list > Kodkod.tuple *) 

111 
fun kk_tuple debug univ_card js = 

112 
if debug then 

113 
Kodkod.Tuple js 

114 
else 

115 
Kodkod.TupleIndex (length js, 

116 
fold (fn j => fn accum => accum * univ_card + j) js 0) 

117 

118 
(* (int * int) list > Kodkod.tuple_set *) 

119 
val tuple_set_from_atom_schema = 

120 
foldl1 Kodkod.TupleProduct o map Kodkod.TupleAtomSeq 

121 
(* rep > Kodkod.tuple_set *) 

122 
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep 

123 

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

124 
(* int > Kodkod.tuple_set *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

125 
val single_atom = Kodkod.TupleSet o single o Kodkod.Tuple o single 
33192  126 
(* int > Kodkod.int_bound list *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

127 
fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))] 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

128 
(* int > int > Kodkod.int_bound list *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

129 
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

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

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

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

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

134 
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

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

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

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

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

140 
(* Kodkod.formula > Kodkod.n_ary_index list *) 

141 
fun built_in_rels_in_formula formula = 

142 
let 

143 
(* Kodkod.rel_expr > Kodkod.n_ary_index list > Kodkod.n_ary_index list *) 

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

144 
fun rel_expr_func (r as Kodkod.Rel (x as (n, j))) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

145 
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

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

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

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

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

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

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

154 
in Kodkod.fold_formula expr_F formula [] end 

155 

156 
val max_table_size = 65536 

157 

158 
(* int > unit *) 

159 
fun check_table_size k = 

160 
if k > max_table_size then 

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

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

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

165 

166 
(* bool > int > int * int > (int > int) > Kodkod.tuple list *) 

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

168 
(check_table_size k; 

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

170 
if j2 >= 0 then 

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

172 
else 

173 
NONE 

174 
end) (index_seq 0 k)) 

175 
(* bool > int > int * int > int > (int * int > int) > Kodkod.tuple list *) 

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

177 
(check_table_size (k * k); 

178 
map_filter (fn j => let 

179 
val j1 = j div k 

180 
val j2 = j  j1 * k 

181 
val j3 = f (j1, j2) 

182 
in 

183 
if j3 >= 0 then 

184 
SOME (kk_tuple debug univ_card 

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

186 
else 

187 
NONE 

188 
end) (index_seq 0 (k * k))) 

189 
(* bool > int > int * int > int > (int * int > int * int) 

190 
> Kodkod.tuple list *) 

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

192 
(check_table_size (k * k); 

193 
map_filter (fn j => let 

194 
val j1 = j div k 

195 
val j2 = j  j1 * k 

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

197 
in 

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

199 
SOME (kk_tuple debug univ_card 

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

201 
j4 + res_j0]) 

202 
else 

203 
NONE 

204 
end) (index_seq 0 (k * k))) 

205 
(* bool > int > int * int > (int * int > int) > Kodkod.tuple list *) 

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

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

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

209 
tabulate_op2 debug univ_card (k, j0) j0 

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

211 
(* bool > int > int * int > (int * int > int * int) > Kodkod.tuple list *) 

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

213 
tabulate_op2_2 debug univ_card (k, j0) j0 

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

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

216 

217 
(* int * int > int *) 

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

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

220 
fun isa_gcd (m, 0) = m 

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

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

223 
val isa_zgcd = isa_gcd o pairself abs 

224 
(* int * int > int * int *) 

225 
fun isa_norm_frac (m, n) = 

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

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

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

229 

230 
(* bool > int > int > int > int > int * int 

231 
> string * bool * Kodkod.tuple list *) 

232 
fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) = 

233 
(check_arity univ_card n; 

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

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

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

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

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

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

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

245 
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

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

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

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

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

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

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

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

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

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

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

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

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

269 
else 

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

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

272 
(* bool > int > int > int > int > int * int > Kodkod.rel_expr 

273 
> Kodkod.bound *) 

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 

278 
in ([(x, nick)], [Kodkod.TupleSet ts]) end 

279 

280 
(* bool > int > int > int > int > Kodkod.formula > Kodkod.bound list *) 

281 
fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 = 

282 
map (bound_for_built_in_rel debug univ_card nat_card int_card j0) 

283 
o built_in_rels_in_formula 

284 

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

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

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

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

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

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

290 

33192  291 
(* Proof.context > bool > nut > Kodkod.bound *) 
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 
299 
[Kodkod.TupleSet [], upper_bound_for_rep R]) 

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 

303 
(* Proof.context > bool > dtype_spec list > nut > Kodkod.bound *) 

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 

313 
[Kodkod.TupleSet []] 

314 
else 

315 
let val ts = Kodkod.TupleAtomSeq (epsilon  delta, delta + j0) in 

316 
if R2 = Formula Neut then 

317 
[ts] > not exclusive ? cons (Kodkod.TupleSet []) 

318 
else 

319 
[Kodkod.TupleSet [], 

320 
Kodkod.TupleProduct (ts, upper_bound_for_rep R2)] 

321 
end) 

322 
end 

323 
 bound_for_sel_rel _ _ _ u = 

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

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

326 
(* Kodkod.bound list > Kodkod.bound list *) 

327 
fun merge_bounds bs = 

328 
let 

329 
(* Kodkod.bound > int *) 

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

331 
(* Kodkod.bound list > Kodkod.bound > Kodkod.bound list 

332 
> Kodkod.bound list *) 

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

334 
 add_bound ds b (c :: cs) = 

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

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

337 
else 

338 
add_bound (c :: ds) b cs 

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

340 

341 
(* int > int > Kodkod.rel_expr list *) 

342 
fun unary_var_seq j0 n = map (curry Kodkod.Var 1) (index_seq j0 n) 

343 

344 
(* int list > Kodkod.rel_expr *) 

345 
val singleton_from_combination = foldl1 Kodkod.Product o map Kodkod.Atom 

346 
(* rep > Kodkod.rel_expr list *) 

347 
fun all_singletons_for_rep R = 

348 
if is_lone_rep R then 

349 
all_combinations_for_rep R > map singleton_from_combination 

350 
else 

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

351 
raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R]) 
33192  352 

353 
(* Kodkod.rel_expr > Kodkod.rel_expr list *) 

354 
fun unpack_products (Kodkod.Product (r1, r2)) = 

355 
unpack_products r1 @ unpack_products r2 

356 
 unpack_products r = [r] 

357 
fun unpack_joins (Kodkod.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2 

358 
 unpack_joins r = [r] 

359 

360 
(* rep > Kodkod.rel_expr *) 

361 
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep 

362 
fun full_rel_for_rep R = 

363 
case atom_schema_of_rep R of 

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

364 
[] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R]) 
33192  365 
 schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema) 
366 

367 
(* int > int list > Kodkod.decl list *) 

368 
fun decls_for_atom_schema j0 schema = 

369 
map2 (fn j => fn x => Kodkod.DeclOne ((1, j), Kodkod.AtomSeq x)) 

370 
(index_seq j0 (length schema)) schema 

371 

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

373 

374 
(* kodkod_constrs > rep > Kodkod.rel_expr > Kodkod.formula *) 

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

376 
R r = 

377 
let val body_R = body_rep R in 

378 
if is_lone_rep body_R then 

379 
let 

380 
val binder_schema = atom_schema_of_reps (binder_reps R) 

381 
val body_schema = atom_schema_of_rep body_R 

382 
val one = is_one_rep body_R 

383 
val opt_x = case r of Kodkod.Rel x => SOME x  _ => NONE 

384 
in 

385 
if opt_x <> NONE andalso length binder_schema = 1 

386 
andalso length body_schema = 1 then 

387 
(if one then Kodkod.Function else Kodkod.Functional) 

388 
(the opt_x, Kodkod.AtomSeq (hd binder_schema), 

389 
Kodkod.AtomSeq (hd body_schema)) 

390 
else 

391 
let 

392 
val decls = decls_for_atom_schema ~1 binder_schema 

393 
val vars = unary_var_seq ~1 (length binder_schema) 

394 
val kk_xone = if one then kk_one else kk_lone 

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

396 
end 

397 
else 

398 
Kodkod.True 

399 
end 

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

400 
fun kk_n_ary_function kk R (r as Kodkod.Rel x) = 
33192  401 
if not (is_opt_rep R) then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

402 
if x = suc_rel then 
33192  403 
Kodkod.False 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

404 
else if x = nat_add_rel then 
33192  405 
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

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

409 
d_n_ary_function kk R r 

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

410 
else if x = nat_subtract_rel then 
33192  411 
Kodkod.True 
412 
else 

413 
d_n_ary_function kk R r 

414 
 kk_n_ary_function kk R r = d_n_ary_function kk R r 

415 

416 
(* kodkod_constrs > Kodkod.rel_expr list > Kodkod.formula *) 

417 
fun kk_disjoint_sets _ [] = Kodkod.True 

418 
 kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs) 

419 
(r :: rs) = 

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

421 

422 
(* int > kodkod_constrs > (Kodkod.rel_expr > Kodkod.rel_expr) 

423 
> Kodkod.rel_expr > Kodkod.rel_expr *) 

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

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

427 
else 

428 
let val x = (Kodkod.arity_of_rel_expr r, j) in 

429 
kk_rel_let [Kodkod.AssignRelReg (x, r)] (f (Kodkod.RelReg x)) 

430 
end 

431 
(* kodkod_constrs > (Kodkod.rel_expr > Kodkod.rel_expr) > Kodkod.rel_expr 

432 
> Kodkod.rel_expr *) 

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

433 
val single_rel_rel_let = basic_rel_rel_let 0 
33192  434 
(* kodkod_constrs > (Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr) 
435 
> Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr *) 

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

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

437 
single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1 
33192  438 
(* kodkod_constrs 
439 
> (Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr) 

440 
> Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr 

441 
> Kodkod.rel_expr *) 

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

442 
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

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

444 
(fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2 
33192  445 

446 
(* kodkod_constrs > int > Kodkod.formula > Kodkod.rel_expr *) 

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

448 
kk_rel_if f (Kodkod.Atom (j0 + 1)) (Kodkod.Atom j0) 

449 
(* kodkod_constrs > rep > Kodkod.formula > Kodkod.rel_expr *) 

450 
fun rel_expr_from_formula kk R f = 

451 
case unopt_rep R of 

452 
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

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

455 
(* kodkod_cotrs > int > int > Kodkod.rel_expr > Kodkod.rel_expr list *) 

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

457 
num_chunks r = 

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

459 
chunk_arity) 

460 

461 
(* kodkod_constrs > bool > rep > rep > Kodkod.rel_expr > Kodkod.rel_expr 

462 
> Kodkod.rel_expr *) 

463 
fun kk_n_fold_join 

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

465 
res_R r1 r2 = 

466 
case arity_of_rep R1 of 

467 
1 => kk_join r1 r2 

468 
 arity1 => 

469 
let 

470 
val unpacked_rs1 = 

471 
if inline_rel_expr r1 then unpack_vect_in_chunks kk 1 arity1 r1 

472 
else unpack_products r1 

473 
in 

474 
if one andalso length unpacked_rs1 = arity1 then 

475 
fold kk_join unpacked_rs1 r2 

476 
else 

477 
kk_project_seq 

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

479 
arity1 (arity_of_rep res_R) 

480 
end 

481 

482 
(* kodkod_constrs > rep > rep > Kodkod.rel_expr > Kodkod.rel_expr list 

483 
> Kodkod.rel_expr list > Kodkod.rel_expr *) 

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

485 
if rs1 = rs2 then r 

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

487 

488 
val lone_rep_fallback_max_card = 4096 

489 
val some_j0 = 0 

490 

491 
(* kodkod_constrs > rep > rep > Kodkod.rel_expr > Kodkod.rel_expr *) 

492 
fun lone_rep_fallback kk new_R old_R r = 

493 
if old_R = new_R then 

494 
r 

495 
else 

496 
let val card = card_of_rep old_R in 

497 
if is_lone_rep old_R andalso is_lone_rep new_R 

498 
andalso card = card_of_rep new_R then 

499 
if card >= lone_rep_fallback_max_card then 

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

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

501 
"too high cardinality (" ^ string_of_int card ^ ")") 
33192  502 
else 
503 
kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R) 

504 
(all_singletons_for_rep new_R) 

505 
else 

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

506 
raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R]) 
33192  507 
end 
508 
(* kodkod_constrs > int * int > rep > Kodkod.rel_expr > Kodkod.rel_expr *) 

509 
and atom_from_rel_expr kk (x as (k, j0)) old_R r = 

510 
case old_R of 

511 
Func (R1, R2) => 

512 
let 

513 
val dom_card = card_of_rep R1 

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

515 
in 

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

517 
(vect_from_rel_expr kk dom_card R2' old_R r) 

518 
end 

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

519 
 Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R]) 
33192  520 
 _ => lone_rep_fallback kk (Atom x) old_R r 
521 
(* kodkod_constrs > rep list > rep > Kodkod.rel_expr > Kodkod.rel_expr *) 

522 
and struct_from_rel_expr kk Rs old_R r = 

523 
case old_R of 

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

525 
 Struct Rs' => 

526 
let 

527 
val Rs = filter (not_equal Unit) Rs 

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

529 
in 

530 
if Rs' = Rs then 

531 
r 

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

533 
let 

534 
val old_arities = map arity_of_rep Rs' 

535 
val old_offsets = offset_list old_arities 

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

537 
in 

538 
fold1 (#kk_product kk) 

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

540 
end 

541 
else 

542 
lone_rep_fallback kk (Struct Rs) old_R r 

543 
end 

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

544 
 _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R]) 
33192  545 
(* kodkod_constrs > int > rep > rep > Kodkod.rel_expr > Kodkod.rel_expr *) 
546 
and vect_from_rel_expr kk k R old_R r = 

547 
case old_R of 

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

549 
 Vect (k', R') => 

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

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

552 
 Func (R1, Formula Neut) => 

553 
if k = card_of_rep R1 then 

554 
fold1 (#kk_product kk) 

555 
(map (fn arg_r => 

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

557 
(all_singletons_for_rep R1)) 

558 
else 

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

559 
raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
33192  560 
 Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r 
561 
 Func (R1, R2) => 

562 
fold1 (#kk_product kk) 

563 
(map (fn arg_r => 

564 
rel_expr_from_rel_expr kk R R2 

565 
(kk_n_fold_join kk true R1 R2 arg_r r)) 

566 
(all_singletons_for_rep R1)) 

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

567 
 _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
33192  568 
(* kodkod_constrs > rep > rep > rep > Kodkod.rel_expr > Kodkod.rel_expr *) 
569 
and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r = 

570 
let 

571 
val dom_card = card_of_rep R1 

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

573 
in 

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

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

576 
end 

577 
 func_from_no_opt_rel_expr kk Unit R2 old_R r = 

578 
(case old_R of 

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

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

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

582 
(case unopt_rep R2 of 

583 
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

584 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  585 
[old_R, Func (Unit, R2)])) 
586 
 Func (R1', R2') => 

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

588 
(arity_of_rep R2')) 

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

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

592 
(case old_R of 

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

594 
let 

595 
val args_rs = all_singletons_for_rep R1 

596 
val vals_rs = unpack_vect_in_chunks kk 1 k r 

597 
(* Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr *) 

598 
fun empty_or_singleton_set_for arg_r val_r = 

599 
#kk_join kk val_r (#kk_product kk (Kodkod.Atom (j0 + 1)) arg_r) 

600 
in 

601 
fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs) 

602 
end 

603 
 Func (R1', Formula Neut) => 

604 
if R1 = R1' then 

605 
r 

606 
else 

607 
let 

608 
val schema = atom_schema_of_rep R1 

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

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

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

613 
#kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) 
33192  614 
end 
615 
 Func (Unit, (Atom (2, j0))) => 

616 
#kk_rel_if kk (#kk_rel_eq kk r (Kodkod.Atom (j0 + 1))) 

617 
(full_rel_for_rep R1) (empty_rel_for_rep R1) 

618 
 Func (R1', Atom (2, j0)) => 

619 
func_from_no_opt_rel_expr kk R1 (Formula Neut) 

620 
(Func (R1', Formula Neut)) (#kk_join kk r (Kodkod.Atom (j0 + 1))) 

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

621 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  622 
[old_R, Func (R1, Formula Neut)])) 
623 
 func_from_no_opt_rel_expr kk R1 R2 old_R r = 

624 
case old_R of 

625 
Vect (k, R) => 

626 
let 

627 
val args_rs = all_singletons_for_rep R1 

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

629 
> map (rel_expr_from_rel_expr kk R2 R) 

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

631 
 Func (R1', Formula Neut) => 

632 
(case R2 of 

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

634 
let val schema = atom_schema_of_rep R1 in 

635 
if length schema = 1 then 

636 
#kk_override kk (#kk_product kk (Kodkod.AtomSeq (hd schema)) 

637 
(Kodkod.Atom j0)) 

638 
(#kk_product kk r (Kodkod.Atom (j0 + 1))) 

639 
else 

640 
let 

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

642 
> rel_expr_from_rel_expr kk R1' R1 

643 
val r2 = Kodkod.Var (1, ~(length schema)  1) 

644 
val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r) 

645 
in 

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

647 
(#kk_subset kk r2 r3) 
33192  648 
end 
649 
end 

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

650 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  651 
[old_R, Func (R1, R2)])) 
652 
 Func (Unit, R2') => 

653 
let val j0 = some_j0 in 

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

655 
(#kk_product kk (Kodkod.Atom j0) r) 

656 
end 

657 
 Func (R1', R2') => 

658 
if R1 = R1' andalso R2 = R2' then 

659 
r 

660 
else 

661 
let 

662 
val dom_schema = atom_schema_of_rep R1 

663 
val ran_schema = atom_schema_of_rep R2 

664 
val dom_prod = fold1 (#kk_product kk) 

665 
(unary_var_seq ~1 (length dom_schema)) 

666 
> rel_expr_from_rel_expr kk R1' R1 

667 
val ran_prod = fold1 (#kk_product kk) 

668 
(unary_var_seq (~(length dom_schema)  1) 

669 
(length ran_schema)) 

670 
> rel_expr_from_rel_expr kk R2' R2 

671 
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

672 
val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk 
33192  673 
in 
674 
#kk_comprehension kk (decls_for_atom_schema ~1 

675 
(dom_schema @ ran_schema)) 

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

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

678 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  679 
[old_R, Func (R1, R2)]) 
680 
(* kodkod_constrs > rep > rep > Kodkod.rel_expr > Kodkod.rel_expr *) 

681 
and rel_expr_from_rel_expr kk new_R old_R r = 

682 
let 

683 
val unopt_old_R = unopt_rep old_R 

684 
val unopt_new_R = unopt_rep new_R 

685 
in 

686 
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

687 
raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R]) 
33192  688 
else if unopt_new_R = unopt_old_R then 
689 
r 

690 
else 

691 
(case unopt_new_R of 

692 
Atom x => atom_from_rel_expr kk x 

693 
 Struct Rs => struct_from_rel_expr kk Rs 

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

695 
 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

696 
 _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", 
33192  697 
[old_R, new_R])) 
698 
unopt_old_R r 

699 
end 

700 
(* kodkod_constrs > rep > rep > rep > Kodkod.rel_expr > Kodkod.rel_expr *) 

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

702 

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

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

704 
fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

705 
kk_join r (Kodkod.Rel (if T = @{typ "unsigned_bit word"} then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

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

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

710 
val int_expr_from_atom = Kodkod.SetSum ooo bit_set_from_atom 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

711 
(* kodkod_constrs > typ > rep > Kodkod.int_expr > Kodkod.rel_expr *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

712 
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

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

714 
kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

715 
(kk_rel_eq (bit_set_from_atom kk T (Kodkod.Var (1, ~1))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

716 
(Kodkod.Bits i)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

717 

33192  718 
(* kodkod_constrs > nut > Kodkod.formula *) 
719 
fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) = 

720 
kk_n_ary_function kk (R > nick = @{const_name List.set} ? unopt_rep) 

721 
(Kodkod.Rel x) 

722 
 declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs) 

723 
(FreeRel (x, _, R, _)) = 

724 
if is_one_rep R then kk_one (Kodkod.Rel x) 

725 
else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (Kodkod.Rel x) 

726 
else Kodkod.True 

727 
 declarative_axiom_for_plain_rel _ u = 

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

728 
raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u]) 
33192  729 

730 
(* nut NameTable.table > styp > Kodkod.rel_expr * rep * int *) 

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

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

733 
FreeRel ((n, j), _, R, _) => (Kodkod.Rel (n, j), R, n) 

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

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

736 
(* nut NameTable.table > styp > Kodkod.rel_expr *) 

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

738 

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

740 
> styp > int > nfa_transition list *) 

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

742 
rel_table (dtypes : dtype_spec list) constr_x n = 

743 
let 

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

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

746 
val type_schema = type_schema_of_rep T R 

747 
in 

748 
map_filter (fn (j, T) => 

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

750 
else SOME (kk_project r (map Kodkod.Num [0, j]), T)) 

751 
(index_seq 1 (arity  1) ~~ tl type_schema) 

752 
end 

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

754 
> styp > nfa_transition list *) 

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

756 
maps (nfa_transitions_for_sel ext_ctxt kk rel_table dtypes x) 

757 
(index_seq 0 (num_sels_for_constr_type T)) 

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

759 
> dtype_spec > nfa_entry option *) 

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

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

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

762 
 nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} = 
33192  763 
SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes 
764 
o #const) constrs) 

765 

766 
val empty_rel = Kodkod.Product (Kodkod.None, Kodkod.None) 

767 

768 
(* nfa_table > typ > typ > Kodkod.rel_expr list *) 

769 
fun direct_path_rel_exprs nfa start final = 

770 
case AList.lookup (op =) nfa final of 

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

771 
SOME trans => map fst (filter (curry (op =) start o snd) trans) 
33192  772 
 NONE => [] 
773 
(* kodkod_constrs > nfa_table > typ list > typ > typ > Kodkod.rel_expr *) 

774 
and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final = 

775 
fold kk_union (direct_path_rel_exprs nfa start final) 

776 
(if start = final then Kodkod.Iden else empty_rel) 

777 
 any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final = 

778 
kk_union (any_path_rel_expr kk nfa qs start final) 

779 
(knot_path_rel_expr kk nfa qs start q final) 

780 
(* kodkod_constrs > nfa_table > typ list > typ > typ > typ 

781 
> Kodkod.rel_expr *) 

782 
and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start 

783 
knot final = 

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

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

786 
(any_path_rel_expr kk nfa qs start knot) 

787 
(* kodkod_constrs > nfa_table > typ list > typ > Kodkod.rel_expr *) 

788 
and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start = 

789 
fold kk_union (direct_path_rel_exprs nfa start start) empty_rel 

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

791 
if start = q then 

792 
kk_closure (loop_path_rel_expr kk nfa qs start) 

793 
else 

794 
kk_union (loop_path_rel_expr kk nfa qs start) 

795 
(knot_path_rel_expr kk nfa qs start q start) 

796 

797 
(* nfa_table > unit NfaGraph.T *) 

798 
fun graph_for_nfa nfa = 

799 
let 

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

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

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

803 
fun add_nfa [] = I 

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

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

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

807 
new_node q' o new_node q 

808 
in add_nfa nfa NfaGraph.empty end 

809 

810 
(* nfa_table > nfa_table list *) 

811 
fun strongly_connected_sub_nfas nfa = 

812 
nfa > graph_for_nfa > NfaGraph.strong_conn 

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

814 

815 
(* dtype_spec list > kodkod_constrs > nfa_table > typ > Kodkod.formula *) 

816 
fun acyclicity_axiom_for_datatype dtypes kk nfa start = 

817 
#kk_no kk (#kk_intersect kk 

818 
(loop_path_rel_expr kk nfa (map fst nfa) start) Kodkod.Iden) 

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

820 
> Kodkod.formula list *) 

821 
fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes = 

822 
map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes 

823 
> strongly_connected_sub_nfas 

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

825 
nfa) 

826 

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

828 
> Kodkod.rel_expr > constr_spec > int > Kodkod.formula *) 

829 
fun sel_axiom_for_sel ext_ctxt j0 

830 
(kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no, 

33982  831 
kk_join, ...}) rel_table dom_r 
33192  832 
({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec) 
833 
n = 

834 
let 

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

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

837 
val R2 = dest_Func R > snd 

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

839 
in 

840 
if exclusive then 

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

842 
else 

843 
let val r' = kk_join (Kodkod.Var (1, 0)) r in 

844 
kk_all [Kodkod.DeclOne ((1, 0), Kodkod.AtomSeq z)] 

845 
(kk_formula_if (kk_subset (Kodkod.Var (1, 0)) dom_r) 

846 
(kk_n_ary_function kk R2 r') 

847 
(kk_no r')) 

848 
end 

849 
end 

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

850 
(* extended_context > int > int > kodkod_constrs > nut NameTable.table 
33192  851 
> constr_spec > Kodkod.formula list *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

852 
fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table 
33192  853 
(constr as {const, delta, epsilon, explicit_max, ...}) = 
854 
let 

855 
val honors_explicit_max = 

856 
explicit_max < 0 orelse epsilon  delta <= explicit_max 

857 
in 

858 
if explicit_max = 0 then 

859 
[formula_for_bool honors_explicit_max] 

860 
else 

861 
let 

862 
val ran_r = discr_rel_expr rel_table const 

863 
val max_axiom = 

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

864 
if honors_explicit_max then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

865 
Kodkod.True 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

866 
else if is_twos_complement_representable bits (epsilon  delta) then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

867 
Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

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

871 
" too small for \"max\"") 
33192  872 
in 
873 
max_axiom :: 

874 
map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr) 

875 
(index_seq 0 (num_sels_for_constr_type (snd const))) 

876 
end 

877 
end 

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

878 
(* extended_context > int > int > kodkod_constrs > nut NameTable.table 
33192  879 
> dtype_spec > Kodkod.formula list *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

882 
maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs 
33192  883 

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

885 
> Kodkod.formula list *) 

886 
fun uniqueness_axiom_for_constr ext_ctxt 

887 
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} 

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

889 
let 

890 
(* Kodkod.rel_expr > Kodkod.formula *) 

891 
fun conjunct_for_sel r = 

892 
kk_rel_eq (kk_join (Kodkod.Var (1, 0)) r) 

893 
(kk_join (Kodkod.Var (1, 1)) r) 

894 
val num_sels = num_sels_for_constr_type (snd const) 

895 
val triples = map (const_triple rel_table 

896 
o boxed_nth_sel_for_constr ext_ctxt const) 

897 
(~1 upto num_sels  1) 

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

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

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

900 
 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

901 
[R]) 
33192  902 
val set_r = triples > hd > #1 
903 
in 

904 
if num_sels = 0 then 

905 
kk_lone set_r 

906 
else 

907 
kk_all (map (Kodkod.DeclOne o rpair set_r o pair 1) [0, 1]) 

908 
(kk_implies 

909 
(fold1 kk_and (map (conjunct_for_sel o #1) (tl triples))) 

910 
(kk_rel_eq (Kodkod.Var (1, 0)) (Kodkod.Var (1, 1)))) 

911 
end 

912 
(* extended_context > kodkod_constrs > nut NameTable.table > dtype_spec 

913 
> Kodkod.formula list *) 

914 
fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table 

915 
({constrs, ...} : dtype_spec) = 

916 
map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs 

917 

918 
(* constr_spec > int *) 

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

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

921 
> Kodkod.formula list *) 

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

923 
rel_table 

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

925 
if forall #exclusive constrs then 

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

927 
else 

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

929 
[kk_rel_eq (fold1 kk_union rs) (Kodkod.AtomSeq (card, j0)), 

930 
kk_disjoint_sets kk rs] 

931 
end 

932 

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

933 
(* extended_context > int > int Typtab.table > kodkod_constrs 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

934 
> nut NameTable.table > dtype_spec > Kodkod.formula list *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

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

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

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

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

941 
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

942 
end 
33192  943 

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

944 
(* extended_context > int > int Typtab.table > kodkod_constrs 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

945 
> nut NameTable.table > dtype_spec list > Kodkod.formula list *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

948 
maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes 
33192  949 

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

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

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

954 
kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference, 

955 
kk_intersect, kk_product, kk_join, kk_closure, kk_comprehension, 

956 
kk_project, kk_project_seq, kk_not3, kk_nat_less, kk_int_less, 

957 
...}) u = 

958 
let 

959 
val main_j0 = offset_of_type ofs bool_T 

960 
val bool_j0 = main_j0 

961 
val bool_atom_R = Atom (2, main_j0) 

962 
val false_atom = Kodkod.Atom bool_j0 

963 
val true_atom = Kodkod.Atom (bool_j0 + 1) 

964 

965 
(* polarity > int > Kodkod.rel_expr > Kodkod.formula *) 

966 
fun formula_from_opt_atom polar j0 r = 

967 
case polar of 

968 
Neg => kk_not (kk_rel_eq r (Kodkod.Atom j0)) 

969 
 _ => kk_rel_eq r (Kodkod.Atom (j0 + 1)) 

970 
(* int > Kodkod.rel_expr > Kodkod.formula *) 

971 
val formula_from_atom = formula_from_opt_atom Pos 

972 

973 
(* Kodkod.formula > Kodkod.formula > Kodkod.formula *) 

974 
fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2) 

975 
(* Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr *) 

976 
val kk_or3 = 

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

977 
double_rel_rel_let kk 
33192  978 
(fn r1 => fn r2 => 
979 
kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom 

980 
(kk_intersect r1 r2)) 

981 
val kk_and3 = 

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

982 
double_rel_rel_let kk 
33192  983 
(fn r1 => fn r2 => 
984 
kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom 

985 
(kk_intersect r1 r2)) 

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

987 

988 
(* int > Kodkod.rel_expr > Kodkod.formula list *) 

989 
val unpack_formulas = 

990 
map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1 

991 
(* (Kodkod.formula > Kodkod.formula > Kodkod.formula) > int 

992 
> Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr *) 

993 
fun kk_vect_set_op connective k r1 r2 = 

994 
fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective) 

995 
(unpack_formulas k r1) (unpack_formulas k r2)) 

996 
(* (Kodkod.formula > Kodkod.formula > Kodkod.formula) > int 

997 
> Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.formula *) 

998 
fun kk_vect_set_bool_op connective k r1 r2 = 

999 
fold1 kk_and (map2 connective (unpack_formulas k r1) 

1000 
(unpack_formulas k r2)) 

1001 

1002 
(* nut > Kodkod.formula *) 

1003 
fun to_f u = 

1004 
case rep_of u of 

1005 
Formula polar => 

1006 
(case u of 

1007 
Cst (False, _, _) => Kodkod.False 

1008 
 Cst (True, _, _) => Kodkod.True 

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

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

1010 
kk_not (to_f_with_polarity (flip_polarity polar) u1) 
33192  1011 
 Op1 (Finite, _, _, u1) => 
1012 
let val opt1 = is_opt_rep (rep_of u1) in 

1013 
case polar of 

1014 
Neut => if opt1 then 

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

1015 
raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) 
33192  1016 
else 
1017 
Kodkod.True 

1018 
 Pos => formula_for_bool (not opt1) 

1019 
 Neg => Kodkod.True 

1020 
end 

1021 
 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

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

1023 
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

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

1025 
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

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

1027 
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

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

1029 
kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
33192  1030 
 Op2 (Less, T, Formula polar, u1, u2) => 
1031 
formula_from_opt_atom polar bool_j0 

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

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

1034 
let 

1035 
val dom_T = domain_type (type_of u1) 

1036 
val R1 = rep_of u1 

1037 
val R2 = rep_of u2 

1038 
val (dom_R, ran_R) = 

1039 
case min_rep R1 R2 of 

1040 
Func (Unit, R') => 

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

1042 
 Func Rp => Rp 

1043 
 R => (Atom (card_of_domain_from_rep 2 R, 

1044 
offset_of_type ofs dom_T), 

1045 
if is_opt_rep R then Opt bool_atom_R else Formula Neut) 

1046 
val set_R = Func (dom_R, ran_R) 

1047 
in 

1048 
if not (is_opt_rep ran_R) then 

1049 
to_set_bool_op kk_implies kk_subset u1 u2 

1050 
else if polar = Neut then 

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

1051 
raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u]) 
33192  1052 
else 
1053 
let 

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

1054 
(* FIXME: merge with similar code below *) 
33192  1055 
(* bool > nut > Kodkod.rel_expr *) 
1056 
fun set_to_r widen u = 

1057 
if widen then 

1058 
kk_difference (full_rel_for_rep dom_R) 

1059 
(kk_join (to_rep set_R u) false_atom) 

1060 
else 

1061 
kk_join (to_rep set_R u) true_atom 

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

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

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

1065 
end 

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

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

1068 
Unit => Kodkod.True 

1069 
 Formula polar => 

1070 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 

1071 
 min_R => 

1072 
let 

1073 
(* nut > nut list *) 

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

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

1076 
 args _ = [] 

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

1078 
in 

1079 
if null opt_arg_us orelse not (is_Opt min_R) 

1080 
orelse is_eval_name u1 then 

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

1082 
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)) 

1083 
else 

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

1084 
kk_subset (to_rep min_R u1) (to_rep min_R u2) 
33192  1085 
end) 
1086 
 Op2 (Eq, T, R, u1, u2) => 

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

1088 
Unit => Kodkod.True 

1089 
 Formula polar => 

1090 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 

1091 
 min_R => 

1092 
if is_opt_rep min_R then 

1093 
if polar = Neut then 

1094 
(* continuation of hackish optimization *) 

1095 
kk_rel_eq (to_rep min_R u1) (to_rep min_R u2) 

1096 
else if is_Cst Unrep u1 then 

1097 
to_could_be_unrep (polar = Neg) u2 

1098 
else if is_Cst Unrep u2 then 

1099 
to_could_be_unrep (polar = Neg) u1 

1100 
else 

1101 
let 

1102 
val r1 = to_rep min_R u1 

1103 
val r2 = to_rep min_R u2 

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

1105 
in 

1106 
(if polar = Pos then 

1107 
if not both_opt then 

1108 
kk_rel_eq r1 r2 

1109 
else if is_lone_rep min_R 

1110 
andalso arity_of_rep min_R = 1 then 

1111 
kk_some (kk_intersect r1 r2) 

1112 
else 

1113 
raise SAME () 

1114 
else 

1115 
if is_lone_rep min_R then 

1116 
if arity_of_rep min_R = 1 then 

1117 
kk_subset (kk_product r1 r2) Kodkod.Iden 

1118 
else if not both_opt then 

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

1120 
> kk_subset 
33192  1121 
else 
1122 
raise SAME () 

1123 
else 

1124 
raise SAME ()) 

1125 
handle SAME () => 

1126 
formula_from_opt_atom polar bool_j0 

1127 
(to_guard [u1, u2] bool_atom_R 

1128 
(rel_expr_from_formula kk bool_atom_R 

1129 
(kk_rel_eq r1 r2))) 

1130 
end 

1131 
else 

1132 
let 

1133 
val r1 = to_rep min_R u1 

1134 
val r2 = to_rep min_R u2 

1135 
in 

1136 
if is_one_rep min_R then 

1137 
let 

1138 
val rs1 = unpack_products r1 

1139 
val rs2 = unpack_products r2 

1140 
in 

1141 
if length rs1 = length rs2 

1142 
andalso map Kodkod.arity_of_rel_expr rs1 

1143 
= map Kodkod.arity_of_rel_expr rs2 then 

1144 
fold1 kk_and (map2 kk_subset rs1 rs2) 

1145 
else 

1146 
kk_subset r1 r2 

1147 
end 

1148 
else 

1149 
kk_rel_eq r1 r2 

1150 
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

1151 
 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

1152 
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

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

1154 
 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

1155 
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

1156 
(Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2)) 
33192  1157 
 Op2 (Apply, T, _, u1, u2) => 
1158 
(case (polar, rep_of u1) of 

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

1160 
 _ => 

1161 
to_f_with_polarity polar 

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

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

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

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

1166 
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

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

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

1171 
 _ => raise NUT ("Nitpick_Kodkod.to_f", [u]) 
33192  1172 
(* polarity > nut > Kodkod.formula *) 
1173 
and to_f_with_polarity polar u = 

1174 
case rep_of u of 

1175 
Formula _ => to_f u 

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

1177 
 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

1178 
 _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u]) 
33192  1179 
(* nut > Kodkod.rel_expr *) 
1180 
and to_r u = 

1181 
case u of 

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

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

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

1185 
if R1 = R2 andalso arity_of_rep R1 = 1 then 

1186 
kk_intersect Kodkod.Iden (kk_product (full_rel_for_rep R1) 

1187 
Kodkod.Univ) 

1188 
else 

1189 
let 

1190 
val schema1 = atom_schema_of_rep R1 

1191 
val schema2 = atom_schema_of_rep R2 

1192 
val arity1 = length schema1 

1193 
val arity2 = length schema2 

1194 
val r1 = fold1 kk_product (unary_var_seq 0 arity1) 

1195 
val r2 = fold1 kk_product (unary_var_seq arity1 arity2) 

1196 
val min_R = min_rep R1 R2 

1197 
in 

1198 
kk_comprehension 

1199 
(decls_for_atom_schema 0 (schema1 @ schema2)) 

1200 
(kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1) 

1201 
(rel_expr_from_rel_expr kk min_R R2 r2)) 

1202 
end 

1203 
 Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => Kodkod.Atom j0 

1204 
 Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) => 

1205 
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

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

1207 
if is_word_type T then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1208 
atom_from_int_expr kk T R (Kodkod.Num j) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

1212 
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1213 
 j' => Kodkod.Atom j' 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1215 
if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1216 
else if is_opt_rep R then Kodkod.None 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1217 
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) 
33192  1218 
 Cst (Unknown, _, R) => empty_rel_for_rep R 
1219 
 Cst (Unrep, _, R) => empty_rel_for_rep R 

1220 
 Cst (Suc, T, Func (Atom x, _)) => 

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

1221 
if domain_type T <> nat_T then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1222 
Kodkod.Rel suc_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1224 
kk_intersect (Kodkod.Rel suc_rel) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1225 
(kk_product Kodkod.Univ (Kodkod.AtomSeq x)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1226 
 Cst (Add, Type ("fun", [@{typ nat}, _]), _) => Kodkod.Rel nat_add_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1227 
 Cst (Add, Type ("fun", [@{typ int}, _]), _) => Kodkod.Rel int_add_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1229 
to_bit_word_binary_op T R NONE (SOME (curry Kodkod.Add)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1230 
 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

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

1232 
(SOME (fn i1 => fn i2 => fn i3 => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1233 
kk_implies (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i1, i2))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1234 
(Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i2, i3))))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1235 
(SOME (curry Kodkod.Add)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1237 
Kodkod.Rel nat_subtract_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1239 
Kodkod.Rel int_subtract_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1240 
 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

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

1242 
(SOME (fn i1 => fn i2 => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1243 
Kodkod.IntIf (Kodkod.LE (i1, i2), Kodkod.Num 0, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1244 
Kodkod.Sub (i1, i2)))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

1247 
(SOME (fn i1 => fn i2 => fn i3 => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1248 
kk_implies (Kodkod.LT (Kodkod.BitXor (i1, i2), Kodkod.Num 0)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1249 
(Kodkod.LT (Kodkod.BitXor (i2, i3), Kodkod.Num 0)))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1250 
(SOME (curry Kodkod.Sub)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1251 
 Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1252 
Kodkod.Rel nat_multiply_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1253 
 Cst (Multiply, Type ("fun", [@{typ int}, _]), _) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1254 
Kodkod.Rel int_multiply_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

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

1258 
(SOME (fn i1 => fn i2 => fn i3 => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1259 
kk_or (Kodkod.IntEq (i2, Kodkod.Num 0)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1260 
(Kodkod.IntEq (Kodkod.Div (i3, i2), i1) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1262 
? kk_and (Kodkod.LE (Kodkod.Num 0, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1263 
foldl1 Kodkod.BitAnd [i1, i2, i3]))))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1264 
(SOME (curry Kodkod.Mult)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1266 
Kodkod.Rel nat_divide_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1268 
Kodkod.Rel int_divide_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

1271 
(SOME (fn i1 => fn i2 => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1272 
Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1273 
Kodkod.Num 0, Kodkod.Div (i1, i2)))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

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

1276 
(SOME (fn i1 => fn i2 => fn i3 => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1277 
Kodkod.LE (Kodkod.Num 0, foldl1 Kodkod.BitAnd [i1, i2, i3]))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1278 
(SOME (fn i1 => fn i2 => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1279 
Kodkod.IntIf (kk_and (Kodkod.LT (i1, Kodkod.Num 0)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1280 
(Kodkod.LT (Kodkod.Num 0, i2)), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1281 
Kodkod.Sub (Kodkod.Div (Kodkod.Add (i1, Kodkod.Num 1), i2), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1282 
Kodkod.Num 1), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1283 
Kodkod.IntIf (kk_and (Kodkod.LT (Kodkod.Num 0, i1)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1284 
(Kodkod.LT (i2, Kodkod.Num 0)), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1285 
Kodkod.Sub (Kodkod.Div (Kodkod.Sub (i1, Kodkod.Num 1), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1286 
i2), Kodkod.Num 1), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1287 
Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1288 
Kodkod.Num 0, Kodkod.Div (i1, i2)))))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1289 
 Cst (Gcd, _, _) => Kodkod.Rel gcd_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1290 
 Cst (Lcm, _, _) => Kodkod.Rel lcm_rel 
33192  1291 
 Cst (Fracs, _, Func (Atom (1, _), _)) => Kodkod.None 
1292 
 Cst (Fracs, _, Func (Struct _, _)) => 

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

1293 
kk_project_seq (Kodkod.Rel norm_frac_rel) 2 2 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1294 
 Cst (NormFrac, _, _) => Kodkod.Rel norm_frac_rel 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1295 
 Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1296 
Kodkod.Iden 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1297 
 Cst (NatToInt, Type ("fun", [@{typ nat}, _]), 
33192  1298 
Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) => 
1299 
if nat_j0 = int_j0 then 

1300 
kk_intersect Kodkod.Iden 

1301 
(kk_product (Kodkod.AtomSeq (max_int_for_card int_k + 1, nat_j0)) 

1302 
Kodkod.Univ) 

1303 
else 

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

1304 
raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"") 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1306 
to_bit_word_unary_op T R I 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

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

1308 
Func (Atom (int_k, int_j0), nat_R)) => 
33192  1309 
let 
1310 
val abs_card = max_int_for_card int_k + 1 

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

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

1313 
in 

1314 
if nat_j0 = int_j0 then 

1315 
kk_union (kk_product (Kodkod.AtomSeq (int_k  abs_card, 

1316 
int_j0 + abs_card)) 

1317 
(Kodkod.Atom nat_j0)) 

1318 
(kk_intersect Kodkod.Iden 

1319 
(kk_product (Kodkod.AtomSeq (overlap, int_j0)) 

1320 
Kodkod.Univ)) 

1321 
else 

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

1322 
raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"") 