33192

1 
(* Title: HOL/Nitpick/Tools/nitpick_kodkod.ML


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


10 
type extended_context = NitpickHOL.extended_context


11 
type dtype_spec = NitpickScope.dtype_spec


12 
type kodkod_constrs = NitpickPeephole.kodkod_constrs


13 
type nut = NitpickNut.nut


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


22 
val check_arity : int > int > unit


23 
val kk_tuple : bool > int > int list > Kodkod.tuple


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


25 
val sequential_int_bounds : int > Kodkod.int_bound list


26 
val bounds_for_built_in_rels_in_formula :


27 
bool > int > int > int > int > Kodkod.formula > Kodkod.bound list


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


29 
val bound_for_sel_rel :


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


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


32 
val declarative_axiom_for_plain_rel : kodkod_constrs > nut > Kodkod.formula


33 
val declarative_axioms_for_datatypes :


34 
extended_context > int Typtab.table > kodkod_constrs


35 
> nut NameTable.table > dtype_spec list > Kodkod.formula list


36 
val kodkod_formula_from_nut :


37 
int Typtab.table > bool > kodkod_constrs > nut > Kodkod.formula


38 
end;


39 


40 
structure NitpickKodkod : NITPICK_KODKOD =


41 
struct


42 


43 
open NitpickUtil


44 
open NitpickHOL


45 
open NitpickScope


46 
open NitpickPeephole


47 
open NitpickRep


48 
open NitpickNut


49 


50 
type nfa_transition = Kodkod.rel_expr * typ


51 
type nfa_entry = typ * nfa_transition list


52 
type nfa_table = nfa_entry list


53 


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


55 


56 
(* int > Kodkod.int_expr list *)


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


58 


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


60 
fun univ_card nat_card int_card main_j0 bounds formula =


61 
let


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


63 
fun rel_expr_func r k =


64 
Int.max (k, case r of


65 
Kodkod.Atom j => j + 1


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


67 
 _ => 0)


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


69 
fun tuple_func t k =


70 
case t of


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


72 
 _ => k


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


74 
fun tuple_set_func ts k =


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


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


77 
int_expr_func = K I}


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


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


80 
> Kodkod.fold_formula expr_F formula


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


82 


83 
(* Proof.context > bool > string > typ > rep > string *)


84 
fun bound_comment ctxt debug nick T R =


85 
short_const_name nick ^


86 
(if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)


87 
else "") ^ " : " ^ string_for_rep R


88 


89 
(* int > int > unit *)


90 
fun check_arity univ_card n =


91 
if n > Kodkod.max_arity univ_card then


92 
raise LIMIT ("NitpickKodkod.check_arity",


93 
"arity " ^ string_of_int n ^ " too large for universe of \


94 
\cardinality " ^ string_of_int univ_card)


95 
else


96 
()


97 


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


99 
fun kk_tuple debug univ_card js =


100 
if debug then


101 
Kodkod.Tuple js


102 
else


103 
Kodkod.TupleIndex (length js,


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


105 


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


107 
val tuple_set_from_atom_schema =


108 
foldl1 Kodkod.TupleProduct o map Kodkod.TupleAtomSeq


109 
(* rep > Kodkod.tuple_set *)


110 
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep


111 


112 
(* int > Kodkod.int_bound list *)


113 
fun sequential_int_bounds n =


114 
[(NONE, map (Kodkod.TupleSet o single o Kodkod.Tuple o single)


115 
(index_seq 0 n))]


116 


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


118 
fun built_in_rels_in_formula formula =


119 
let


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


121 
fun rel_expr_func (Kodkod.Rel (n, j)) rels =


122 
(case AList.lookup (op =) (#rels initial_pool) n of


123 
SOME k => (j < k ? insert (op =) (n, j)) rels


124 
 NONE => rels)


125 
 rel_expr_func _ rels = rels


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


127 
int_expr_func = K I}


128 
in Kodkod.fold_formula expr_F formula [] end


129 


130 
val max_table_size = 65536


131 


132 
(* int > unit *)


133 
fun check_table_size k =


134 
if k > max_table_size then


135 
raise LIMIT ("NitpickKodkod.check_table_size",


136 
"precomputed table too large (" ^ string_of_int k ^ ")")


137 
else


138 
()


139 


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


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


142 
(check_table_size k;


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


144 
if j2 >= 0 then


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


146 
else


147 
NONE


148 
end) (index_seq 0 k))


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


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


151 
(check_table_size (k * k);


152 
map_filter (fn j => let


153 
val j1 = j div k


154 
val j2 = j  j1 * k


155 
val j3 = f (j1, j2)


156 
in


157 
if j3 >= 0 then


158 
SOME (kk_tuple debug univ_card


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


160 
else


161 
NONE


162 
end) (index_seq 0 (k * k)))


163 
(* bool > int > int * int > int > (int * int > int * int)


164 
> Kodkod.tuple list *)


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


166 
(check_table_size (k * k);


167 
map_filter (fn j => let


168 
val j1 = j div k


169 
val j2 = j  j1 * k


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


171 
in


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


173 
SOME (kk_tuple debug univ_card


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


175 
j4 + res_j0])


176 
else


177 
NONE


178 
end) (index_seq 0 (k * k)))


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


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


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


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


183 
tabulate_op2 debug univ_card (k, j0) j0


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


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


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


187 
tabulate_op2_2 debug univ_card (k, j0) j0


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


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


190 


191 
(* int * int > int *)


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


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


194 
fun isa_gcd (m, 0) = m


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


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


197 
val isa_zgcd = isa_gcd o pairself abs


198 
(* int * int > int * int *)


199 
fun isa_norm_frac (m, n) =


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


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


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


203 


204 
(* bool > int > int > int > int > int * int


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


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


207 
(check_arity univ_card n;


208 
if Kodkod.Rel x = not3_rel then


209 
("not3", tabulate_func1 debug univ_card (2, j0) (curry (op ) 1))


210 
else if Kodkod.Rel x = suc_rel then


211 
("suc", tabulate_func1 debug univ_card (univ_card  j0  1, j0)


212 
(Integer.add 1))


213 
else if Kodkod.Rel x = nat_add_rel then


214 
("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +))


215 
else if Kodkod.Rel x = int_add_rel then


216 
("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +))


217 
else if Kodkod.Rel x = nat_subtract_rel then


218 
("nat_subtract",


219 
tabulate_op2 debug univ_card (nat_card, j0) j0 (op nat_minus))


220 
else if Kodkod.Rel x = int_subtract_rel then


221 
("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op ))


222 
else if Kodkod.Rel x = nat_multiply_rel then


223 
("nat_multiply", tabulate_nat_op2 debug univ_card (nat_card, j0) (op * ))


224 
else if Kodkod.Rel x = int_multiply_rel then


225 
("int_multiply", tabulate_int_op2 debug univ_card (int_card, j0) (op * ))


226 
else if Kodkod.Rel x = nat_divide_rel then


227 
("nat_divide", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_div)


228 
else if Kodkod.Rel x = int_divide_rel then


229 
("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div)


230 
else if Kodkod.Rel x = nat_modulo_rel then


231 
("nat_modulo", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_mod)


232 
else if Kodkod.Rel x = int_modulo_rel then


233 
("int_modulo", tabulate_int_op2 debug univ_card (int_card, j0) isa_mod)


234 
else if Kodkod.Rel x = nat_less_rel then


235 
("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0)


236 
(int_for_bool o op <))


237 
else if Kodkod.Rel x = int_less_rel then


238 
("int_less", tabulate_int_op2 debug univ_card (int_card, j0)


239 
(int_for_bool o op <))


240 
else if Kodkod.Rel x = gcd_rel then


241 
("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd)


242 
else if Kodkod.Rel x = lcm_rel then


243 
("lcm", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_lcm)


244 
else if Kodkod.Rel x = norm_frac_rel then


245 
("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0)


246 
isa_norm_frac)


247 
else


248 
raise ARG ("NitpickKodkod.tabulate_built_in_rel", "unknown relation"))


249 


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


251 
> Kodkod.bound *)


252 
fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x =


253 
let


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


255 
j0 x


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


257 


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


259 
fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 =


260 
map (bound_for_built_in_rel debug univ_card nat_card int_card j0)


261 
o built_in_rels_in_formula


262 


263 
(* Proof.context > bool > nut > Kodkod.bound *)


264 
fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =


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


266 
if nick = @{const_name bisim_iterator_max} then


267 
case R of


268 
Atom (k, j0) => [Kodkod.TupleSet [Kodkod.Tuple [k  1 + j0]]]


269 
 _ => raise NUT ("NitpickKodkod.bound_for_plain_rel", [u])


270 
else


271 
[Kodkod.TupleSet [], upper_bound_for_rep R])


272 
 bound_for_plain_rel _ _ u =


273 
raise NUT ("NitpickKodkod.bound_for_plain_rel", [u])


274 


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


276 
fun bound_for_sel_rel ctxt debug dtypes


277 
(FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),


278 
nick)) =


279 
let


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


281 
constr_spec dtypes (original_name nick, T1)


282 
in


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


284 
if explicit_max = 0 then


285 
[Kodkod.TupleSet []]


286 
else


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


288 
if R2 = Formula Neut then


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


290 
else


291 
[Kodkod.TupleSet [],


292 
Kodkod.TupleProduct (ts, upper_bound_for_rep R2)]


293 
end)


294 
end


295 
 bound_for_sel_rel _ _ _ u =


296 
raise NUT ("NitpickKodkod.bound_for_sel_rel", [u])


297 


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


299 
fun merge_bounds bs =


300 
let


301 
(* Kodkod.bound > int *)


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


303 
(* Kodkod.bound list > Kodkod.bound > Kodkod.bound list


304 
> Kodkod.bound list *)


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


306 
 add_bound ds b (c :: cs) =


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


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


309 
else


310 
add_bound (c :: ds) b cs


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


312 


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


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


315 


316 
(* int list > Kodkod.rel_expr *)


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


318 
(* rep > Kodkod.rel_expr list *)


319 
fun all_singletons_for_rep R =


320 
if is_lone_rep R then


321 
all_combinations_for_rep R > map singleton_from_combination


322 
else


323 
raise REP ("NitpickKodkod.all_singletons_for_rep", [R])


324 


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


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


327 
unpack_products r1 @ unpack_products r2


328 
 unpack_products r = [r]


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


330 
 unpack_joins r = [r]


331 


332 
(* rep > Kodkod.rel_expr *)


333 
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep


334 
fun full_rel_for_rep R =


335 
case atom_schema_of_rep R of


336 
[] => raise REP ("NitpickKodkod.full_rel_for_rep", [R])


337 
 schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema)


338 


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


340 
fun decls_for_atom_schema j0 schema =


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


342 
(index_seq j0 (length schema)) schema


343 


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


345 


346 
(* FIXME: clean up *)


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


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


349 
R r =


350 
let val body_R = body_rep R in


351 
if is_lone_rep body_R then


352 
let


353 
val binder_schema = atom_schema_of_reps (binder_reps R)


354 
val body_schema = atom_schema_of_rep body_R


355 
val one = is_one_rep body_R


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


357 
in


358 
if opt_x <> NONE andalso length binder_schema = 1


359 
andalso length body_schema = 1 then


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


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


362 
Kodkod.AtomSeq (hd body_schema))


363 
else


364 
let


365 
val decls = decls_for_atom_schema ~1 binder_schema


366 
val vars = unary_var_seq ~1 (length binder_schema)


367 
val kk_xone = if one then kk_one else kk_lone


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


369 
end


370 
else


371 
Kodkod.True


372 
end


373 
fun kk_n_ary_function kk R (r as Kodkod.Rel _) =


374 
(* FIXME: weird test *)


375 
if not (is_opt_rep R) then


376 
if r = suc_rel then


377 
Kodkod.False


378 
else if r = nat_add_rel then


379 
formula_for_bool (card_of_rep (body_rep R) = 1)


380 
else if r = nat_multiply_rel then


381 
formula_for_bool (card_of_rep (body_rep R) <= 2)


382 
else


383 
d_n_ary_function kk R r


384 
else if r = nat_subtract_rel then


385 
Kodkod.True


386 
else


387 
d_n_ary_function kk R r


388 
 kk_n_ary_function kk R r = d_n_ary_function kk R r


389 


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


391 
fun kk_disjoint_sets _ [] = Kodkod.True


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


393 
(r :: rs) =


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


395 


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


397 
> Kodkod.rel_expr > Kodkod.rel_expr *)


398 
fun basic_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =


399 
if inline_rel_expr r then


400 
f r


401 
else


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


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


404 
end


405 


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


407 
> Kodkod.rel_expr *)


408 
val single_rel_let = basic_rel_let 0


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


410 
> Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr *)


411 
fun double_rel_let kk f r1 r2 =


412 
single_rel_let kk (fn r1 => basic_rel_let 1 kk (f r1) r2) r1


413 
(* kodkod_constrs


414 
> (Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr)


415 
> Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr


416 
> Kodkod.rel_expr *)


417 
fun triple_rel_let kk f r1 r2 r3 =


418 
double_rel_let kk (fn r1 => fn r2 => basic_rel_let 2 kk (f r1 r2) r3) r1 r2


419 


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


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


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


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


424 
fun rel_expr_from_formula kk R f =


425 
case unopt_rep R of


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


427 
 _ => raise REP ("NitpickKodkod.rel_expr_from_formula", [R])


428 


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


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


431 
num_chunks r =


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


433 
chunk_arity)


434 


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


436 
> Kodkod.rel_expr *)


437 
fun kk_n_fold_join


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


439 
res_R r1 r2 =


440 
case arity_of_rep R1 of


441 
1 => kk_join r1 r2


442 
 arity1 =>


443 
let


444 
val unpacked_rs1 =


445 
if inline_rel_expr r1 then unpack_vect_in_chunks kk 1 arity1 r1


446 
else unpack_products r1


447 
in


448 
if one andalso length unpacked_rs1 = arity1 then


449 
fold kk_join unpacked_rs1 r2


450 
else


451 
kk_project_seq


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


453 
arity1 (arity_of_rep res_R)


454 
end


455 


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


457 
> Kodkod.rel_expr list > Kodkod.rel_expr *)


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


459 
if rs1 = rs2 then r


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


461 


462 
val lone_rep_fallback_max_card = 4096


463 
val some_j0 = 0


464 


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


466 
fun lone_rep_fallback kk new_R old_R r =


467 
if old_R = new_R then


468 
r


469 
else


470 
let val card = card_of_rep old_R in


471 
if is_lone_rep old_R andalso is_lone_rep new_R


472 
andalso card = card_of_rep new_R then


473 
if card >= lone_rep_fallback_max_card then


474 
raise LIMIT ("NitpickKodkod.lone_rep_fallback",


475 
"too high cardinality (" ^ string_of_int card ^ ")")


476 
else


477 
kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)


478 
(all_singletons_for_rep new_R)


479 
else


480 
raise REP ("NitpickKodkod.lone_rep_fallback", [old_R, new_R])


481 
end


482 
(* kodkod_constrs > int * int > rep > Kodkod.rel_expr > Kodkod.rel_expr *)


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


484 
case old_R of


485 
Func (R1, R2) =>


486 
let


487 
val dom_card = card_of_rep R1


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


489 
in


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


491 
(vect_from_rel_expr kk dom_card R2' old_R r)


492 
end


493 
 Opt _ => raise REP ("NitpickKodkod.atom_from_rel_expr", [old_R])


494 
 _ => lone_rep_fallback kk (Atom x) old_R r


495 
(* kodkod_constrs > rep list > rep > Kodkod.rel_expr > Kodkod.rel_expr *)


496 
and struct_from_rel_expr kk Rs old_R r =


497 
case old_R of


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


499 
 Struct Rs' =>


500 
let


501 
val Rs = filter (not_equal Unit) Rs


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


503 
in


504 
if Rs' = Rs then


505 
r


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


507 
let


508 
val old_arities = map arity_of_rep Rs'


509 
val old_offsets = offset_list old_arities


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


511 
in


512 
fold1 (#kk_product kk)


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


514 
end


515 
else


516 
lone_rep_fallback kk (Struct Rs) old_R r


517 
end


518 
 _ => raise REP ("NitpickKodkod.struct_from_rel_expr", [old_R])


519 
(* kodkod_constrs > int > rep > rep > Kodkod.rel_expr > Kodkod.rel_expr *)


520 
and vect_from_rel_expr kk k R old_R r =


521 
case old_R of


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


523 
 Vect (k', R') =>


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


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


526 
 Func (R1, Formula Neut) =>


527 
if k = card_of_rep R1 then


528 
fold1 (#kk_product kk)


529 
(map (fn arg_r =>


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


531 
(all_singletons_for_rep R1))


532 
else


533 
raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R])


534 
 Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r


535 
 Func (R1, R2) =>


536 
fold1 (#kk_product kk)


537 
(map (fn arg_r =>


538 
rel_expr_from_rel_expr kk R R2


539 
(kk_n_fold_join kk true R1 R2 arg_r r))


540 
(all_singletons_for_rep R1))


541 
 _ => raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R])


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


543 
and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r =


544 
let


545 
val dom_card = card_of_rep R1


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


547 
in


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


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


550 
end


551 
 func_from_no_opt_rel_expr kk Unit R2 old_R r =


552 
(case old_R of


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


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


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


556 
(case unopt_rep R2 of


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


558 
 _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",


559 
[old_R, Func (Unit, R2)]))


560 
 Func (R1', R2') =>


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


562 
(arity_of_rep R2'))


563 
 _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",


564 
[old_R, Func (Unit, R2)]))


565 
 func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r =


566 
(case old_R of


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


568 
let


569 
val args_rs = all_singletons_for_rep R1


570 
val vals_rs = unpack_vect_in_chunks kk 1 k r


571 
(* Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr *)


572 
fun empty_or_singleton_set_for arg_r val_r =


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


574 
in


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


576 
end


577 
 Func (R1', Formula Neut) =>


578 
if R1 = R1' then


579 
r


580 
else


581 
let


582 
val schema = atom_schema_of_rep R1


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


584 
> rel_expr_from_rel_expr kk R1' R1


585 
in


586 
#kk_comprehension kk (decls_for_atom_schema ~1 schema)


587 
(#kk_subset kk r1 r)


588 
end


589 
 Func (Unit, (Atom (2, j0))) =>


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


591 
(full_rel_for_rep R1) (empty_rel_for_rep R1)


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


593 
func_from_no_opt_rel_expr kk R1 (Formula Neut)


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


595 
 _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",


596 
[old_R, Func (R1, Formula Neut)]))


597 
 func_from_no_opt_rel_expr kk R1 R2 old_R r =


598 
case old_R of


599 
Vect (k, R) =>


600 
let


601 
val args_rs = all_singletons_for_rep R1


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


603 
> map (rel_expr_from_rel_expr kk R2 R)


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


605 
 Func (R1', Formula Neut) =>


606 
(case R2 of


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


608 
let val schema = atom_schema_of_rep R1 in


609 
if length schema = 1 then


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


611 
(Kodkod.Atom j0))


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


613 
else


614 
let


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


616 
> rel_expr_from_rel_expr kk R1' R1


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


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


619 
in


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


621 
(#kk_rel_eq kk r2 r3)


622 
end


623 
end


624 
 _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",


625 
[old_R, Func (R1, R2)]))


626 
 Func (Unit, R2') =>


627 
let val j0 = some_j0 in


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


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


630 
end


631 
 Func (R1', R2') =>


632 
if R1 = R1' andalso R2 = R2' then


633 
r


634 
else


635 
let


636 
val dom_schema = atom_schema_of_rep R1


637 
val ran_schema = atom_schema_of_rep R2


638 
val dom_prod = fold1 (#kk_product kk)


639 
(unary_var_seq ~1 (length dom_schema))


640 
> rel_expr_from_rel_expr kk R1' R1


641 
val ran_prod = fold1 (#kk_product kk)


642 
(unary_var_seq (~(length dom_schema)  1)


643 
(length ran_schema))


644 
> rel_expr_from_rel_expr kk R2' R2


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


646 
in


647 
#kk_comprehension kk (decls_for_atom_schema ~1


648 
(dom_schema @ ran_schema))


649 
(#kk_subset kk ran_prod app)


650 
end


651 
 _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",


652 
[old_R, Func (R1, R2)])


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


654 
and rel_expr_from_rel_expr kk new_R old_R r =


655 
let


656 
val unopt_old_R = unopt_rep old_R


657 
val unopt_new_R = unopt_rep new_R


658 
in


659 
if unopt_old_R <> old_R andalso unopt_new_R = new_R then


660 
raise REP ("NitpickKodkod.rel_expr_from_rel_expr", [old_R, new_R])


661 
else if unopt_new_R = unopt_old_R then


662 
r


663 
else


664 
(case unopt_new_R of


665 
Atom x => atom_from_rel_expr kk x


666 
 Struct Rs => struct_from_rel_expr kk Rs


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


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


669 
 _ => raise REP ("NitpickKodkod.rel_expr_from_rel_expr",


670 
[old_R, new_R]))


671 
unopt_old_R r


672 
end


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


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


675 


676 
(* kodkod_constrs > nut > Kodkod.formula *)


677 
fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =


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


679 
(Kodkod.Rel x)


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


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


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


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


684 
else Kodkod.True


685 
 declarative_axiom_for_plain_rel _ u =


686 
raise NUT ("NitpickKodkod.declarative_axiom_for_plain_rel", [u])


687 


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


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


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


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


692 
 _ => raise TERM ("NitpickKodkod.const_triple", [Const x])


693 


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


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


696 


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


698 
> styp > int > nfa_transition list *)


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


700 
rel_table (dtypes : dtype_spec list) constr_x n =


701 
let


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


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


704 
val type_schema = type_schema_of_rep T R


705 
in


706 
map_filter (fn (j, T) =>


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


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


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


710 
end


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


712 
> styp > nfa_transition list *)


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


714 
maps (nfa_transitions_for_sel ext_ctxt kk rel_table dtypes x)


715 
(index_seq 0 (num_sels_for_constr_type T))


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


717 
> dtype_spec > nfa_entry option *)


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


719 
 nfa_entry_for_datatype ext_ctxt kk rel_table dtypes


720 
({typ, constrs, ...} : dtype_spec) =


721 
SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes


722 
o #const) constrs)


723 


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


725 


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


727 
fun direct_path_rel_exprs nfa start final =


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


729 
SOME trans => map fst (filter (equal start o snd) trans)


730 
 NONE => []


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


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


733 
fold kk_union (direct_path_rel_exprs nfa start final)


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


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


736 
kk_union (any_path_rel_expr kk nfa qs start final)


737 
(knot_path_rel_expr kk nfa qs start q final)


738 
(* kodkod_constrs > nfa_table > typ list > typ > typ > typ


739 
> Kodkod.rel_expr *)


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


741 
knot final =


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


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


744 
(any_path_rel_expr kk nfa qs start knot)


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


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


747 
fold kk_union (direct_path_rel_exprs nfa start start) empty_rel


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


749 
if start = q then


750 
kk_closure (loop_path_rel_expr kk nfa qs start)


751 
else


752 
kk_union (loop_path_rel_expr kk nfa qs start)


753 
(knot_path_rel_expr kk nfa qs start q start)


754 


755 
(* nfa_table > unit NfaGraph.T *)


756 
fun graph_for_nfa nfa =


757 
let


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


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


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


761 
fun add_nfa [] = I


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


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


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


765 
new_node q' o new_node q


766 
in add_nfa nfa NfaGraph.empty end


767 


768 
(* nfa_table > nfa_table list *)


769 
fun strongly_connected_sub_nfas nfa =


770 
nfa > graph_for_nfa > NfaGraph.strong_conn


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


772 


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


774 
fun acyclicity_axiom_for_datatype dtypes kk nfa start =


775 
#kk_no kk (#kk_intersect kk


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


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


778 
> Kodkod.formula list *)


779 
fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes =


780 
map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes


781 
> strongly_connected_sub_nfas


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


783 
nfa)


784 


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


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


787 
fun sel_axiom_for_sel ext_ctxt j0


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


789 
kk_join, kk_project, ...}) rel_table dom_r


790 
({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)


791 
n =


792 
let


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


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


795 
val R2 = dest_Func R > snd


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


797 
in


798 
if exclusive then


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


800 
else


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


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


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


804 
(kk_n_ary_function kk R2 r')


805 
(kk_no r'))


806 
end


807 
end


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


809 
> constr_spec > Kodkod.formula list *)


810 
fun sel_axioms_for_constr ext_ctxt j0 kk rel_table


811 
(constr as {const, delta, epsilon, explicit_max, ...}) =


812 
let


813 
val honors_explicit_max =


814 
explicit_max < 0 orelse epsilon  delta <= explicit_max


815 
in


816 
if explicit_max = 0 then


817 
[formula_for_bool honors_explicit_max]


818 
else


819 
let


820 
val ran_r = discr_rel_expr rel_table const


821 
val max_axiom =


822 
if honors_explicit_max then Kodkod.True


823 
else Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max)


824 
in


825 
max_axiom ::


826 
map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr)


827 
(index_seq 0 (num_sels_for_constr_type (snd const)))


828 
end


829 
end


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


831 
> dtype_spec > Kodkod.formula list *)


832 
fun sel_axioms_for_datatype ext_ctxt j0 kk rel_table


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


834 
maps (sel_axioms_for_constr ext_ctxt j0 kk rel_table) constrs


835 


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


837 
> Kodkod.formula list *)


838 
fun uniqueness_axiom_for_constr ext_ctxt


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


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


841 
let


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


843 
fun conjunct_for_sel r =


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


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


846 
val num_sels = num_sels_for_constr_type (snd const)


847 
val triples = map (const_triple rel_table


848 
o boxed_nth_sel_for_constr ext_ctxt const)


849 
(~1 upto num_sels  1)


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


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


852 
 R => raise REP ("NitpickKodkod.uniqueness_axiom_for_constr", [R])


853 
val set_r = triples > hd > #1


854 
in


855 
if num_sels = 0 then


856 
kk_lone set_r


857 
else


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


859 
(kk_implies


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


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


862 
end


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


864 
> Kodkod.formula list *)


865 
fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table


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


867 
map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs


868 


869 
(* constr_spec > int *)


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


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


872 
> Kodkod.formula list *)


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


874 
rel_table


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


876 
if forall #exclusive constrs then


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


878 
else


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


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


881 
kk_disjoint_sets kk rs]


882 
end


883 


884 
(* extended_context > int Typtab.table > kodkod_constrs > nut NameTable.table


885 
> dtype_spec > Kodkod.formula list *)


886 
fun other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =


887 
let val j0 = offset_of_type ofs typ in


888 
sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @


889 
uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @


890 
partition_axioms_for_datatype j0 kk rel_table dtype


891 
end


892 


893 
(* extended_context > int Typtab.table > kodkod_constrs > nut NameTable.table


894 
> dtype_spec list > Kodkod.formula list *)


895 
fun declarative_axioms_for_datatypes ext_ctxt ofs kk rel_table dtypes =


896 
acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @


897 
maps (other_axioms_for_datatype ext_ctxt ofs kk rel_table) dtypes


898 


899 
(* int Typtab.table > bool > kodkod_constrs > nut > Kodkod.formula *)


900 
fun kodkod_formula_from_nut ofs liberal


901 
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,


902 
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,


903 
kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference,


904 
kk_intersect, kk_product, kk_join, kk_closure, kk_comprehension,


905 
kk_project, kk_project_seq, kk_not3, kk_nat_less, kk_int_less,


906 
...}) u =


907 
let


908 
val main_j0 = offset_of_type ofs bool_T


909 
val bool_j0 = main_j0


910 
val bool_atom_R = Atom (2, main_j0)


911 
val false_atom = Kodkod.Atom bool_j0


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


913 


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


915 
fun formula_from_opt_atom polar j0 r =


916 
case polar of


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


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


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


920 
val formula_from_atom = formula_from_opt_atom Pos


921 


922 
(* Kodkod.formula > Kodkod.formula > Kodkod.formula *)


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


924 
(* Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr *)


925 
val kk_or3 =


926 
double_rel_let kk


927 
(fn r1 => fn r2 =>


928 
kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom


929 
(kk_intersect r1 r2))


930 
val kk_and3 =


931 
double_rel_let kk


932 
(fn r1 => fn r2 =>


933 
kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom


934 
(kk_intersect r1 r2))


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


936 


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


938 
val unpack_formulas =


939 
map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1


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


941 
> Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.rel_expr *)


942 
fun kk_vect_set_op connective k r1 r2 =


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


944 
(unpack_formulas k r1) (unpack_formulas k r2))


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


946 
> Kodkod.rel_expr > Kodkod.rel_expr > Kodkod.formula *)


947 
fun kk_vect_set_bool_op connective k r1 r2 =


948 
fold1 kk_and (map2 connective (unpack_formulas k r1)


949 
(unpack_formulas k r2))


950 


951 
(* nut > Kodkod.formula *)


952 
fun to_f u =


953 
case rep_of u of


954 
Formula polar =>


955 
(case u of


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


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


958 
 Op1 (Not, _, _, u1) => kk_not (to_f u1)


959 
 Op1 (Finite, _, _, u1) =>


960 
let val opt1 = is_opt_rep (rep_of u1) in


961 
case polar of


962 
Neut => if opt1 then


963 
raise NUT ("NitpickKodkod.to_f (Finite)", [u])


964 
else


965 
Kodkod.True


966 
 Pos => formula_for_bool (not opt1)


967 
 Neg => Kodkod.True


968 
end


969 
 Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1


970 
 Op2 (All, _, _, u1, u2) => kk_all (untuple to_decl u1) (to_f u2)


971 
 Op2 (Exist, _, _, u1, u2) => kk_exist (untuple to_decl u1) (to_f u2)


972 
 Op2 (Or, _, _, u1, u2) => kk_or (to_f u1) (to_f u2)


973 
 Op2 (And, _, _, u1, u2) => kk_and (to_f u1) (to_f u2)


974 
 Op2 (Less, T, Formula polar, u1, u2) =>


975 
formula_from_opt_atom polar bool_j0


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


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


978 
let


979 
val dom_T = domain_type (type_of u1)


980 
val R1 = rep_of u1


981 
val R2 = rep_of u2


982 
val (dom_R, ran_R) =


983 
case min_rep R1 R2 of


984 
Func (Unit, R') =>


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


986 
 Func Rp => Rp


987 
 R => (Atom (card_of_domain_from_rep 2 R,


988 
offset_of_type ofs dom_T),


989 
if is_opt_rep R then Opt bool_atom_R else Formula Neut)


990 
val set_R = Func (dom_R, ran_R)


991 
in


992 
if not (is_opt_rep ran_R) then


993 
to_set_bool_op kk_implies kk_subset u1 u2


994 
else if polar = Neut then


995 
raise NUT ("NitpickKodkod.to_f (Subset)", [u])


996 
else


997 
let


998 
(* bool > nut > Kodkod.rel_expr *)


999 
fun set_to_r widen u =


1000 
if widen then


1001 
kk_difference (full_rel_for_rep dom_R)


1002 
(kk_join (to_rep set_R u) false_atom)


1003 
else


1004 
kk_join (to_rep set_R u) true_atom


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


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


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


1008 
end


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


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


1011 
Unit => Kodkod.True


1012 
 Formula polar =>


1013 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)


1014 
 min_R =>


1015 
let


1016 
(* nut > nut list *)


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


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


1019 
 args _ = []


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


1021 
in


1022 
if null opt_arg_us orelse not (is_Opt min_R)


1023 
orelse is_eval_name u1 then


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


1025 
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2))


1026 
else


1027 
kk_no (kk_difference (to_rep min_R u1) (to_rep min_R u2))


1028 
end)


1029 
 Op2 (Eq, T, R, u1, u2) =>


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


1031 
Unit => Kodkod.True


1032 
 Formula polar =>


1033 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)


1034 
 min_R =>


1035 
if is_opt_rep min_R then


1036 
if polar = Neut then


1037 
(* continuation of hackish optimization *)


1038 
kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)


1039 
else if is_Cst Unrep u1 then


1040 
to_could_be_unrep (polar = Neg) u2


1041 
else if is_Cst Unrep u2 then


1042 
to_could_be_unrep (polar = Neg) u1


1043 
else


1044 
let


1045 
val r1 = to_rep min_R u1


1046 
val r2 = to_rep min_R u2


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


1048 
in


1049 
(if polar = Pos then


1050 
if not both_opt then


1051 
kk_rel_eq r1 r2


1052 
else if is_lone_rep min_R


1053 
andalso arity_of_rep min_R = 1 then


1054 
kk_some (kk_intersect r1 r2)


1055 
else


1056 
raise SAME ()


1057 
else


1058 
if is_lone_rep min_R then


1059 
if arity_of_rep min_R = 1 then


1060 
kk_subset (kk_product r1 r2) Kodkod.Iden


1061 
else if not both_opt then


1062 
(r1, r2) > is_opt_rep (rep_of u2) ? swap


1063 
> uncurry kk_difference > kk_no


1064 
else


1065 
raise SAME ()


1066 
else


1067 
raise SAME ())


1068 
handle SAME () =>


1069 
formula_from_opt_atom polar bool_j0


1070 
(to_guard [u1, u2] bool_atom_R


1071 
(rel_expr_from_formula kk bool_atom_R


1072 
(kk_rel_eq r1 r2)))


1073 
end


1074 
else


1075 
let


1076 
val r1 = to_rep min_R u1


1077 
val r2 = to_rep min_R u2


1078 
in


1079 
if is_one_rep min_R then


1080 
let


1081 
val rs1 = unpack_products r1


1082 
val rs2 = unpack_products r2


1083 
in


1084 
if length rs1 = length rs2


1085 
andalso map Kodkod.arity_of_rel_expr rs1


1086 
= map Kodkod.arity_of_rel_expr rs2 then


1087 
fold1 kk_and (map2 kk_subset rs1 rs2)


1088 
else


1089 
kk_subset r1 r2


1090 
end


1091 
else


1092 
kk_rel_eq r1 r2


1093 
end)


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


1095 
(case (polar, rep_of u1) of


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


1097 
 _ =>


1098 
to_f_with_polarity polar


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


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


1101 
kk_formula_let [to_expr_assign u1 u2] (to_f u3)


1102 
 Op3 (If, _, _, u1, u2, u3) =>


1103 
kk_formula_if (to_f u1) (to_f u2) (to_f u3)


1104 
 FormulaReg (j, _, _) => Kodkod.FormulaReg j


1105 
 _ => raise NUT ("NitpickKodkod.to_f", [u]))


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


1107 
 _ => raise NUT ("NitpickKodkod.to_f", [u])


1108 
(* polarity > nut > Kodkod.formula *)


1109 
and to_f_with_polarity polar u =


1110 
case rep_of u of


1111 
Formula _ => to_f u


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


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


1114 
 _ => raise NUT ("NitpickKodkod.to_f_with_polarity", [u])


1115 
(* nut > Kodkod.rel_expr *)


1116 
and to_r u =


1117 
case u of


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


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


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


1121 
if R1 = R2 andalso arity_of_rep R1 = 1 then


1122 
kk_intersect Kodkod.Iden (kk_product (full_rel_for_rep R1)


1123 
Kodkod.Univ)


1124 
else


1125 
let


1126 
val schema1 = atom_schema_of_rep R1


1127 
val schema2 = atom_schema_of_rep R2


1128 
val arity1 = length schema1


1129 
val arity2 = length schema2


1130 
val r1 = fold1 kk_product (unary_var_seq 0 arity1)


1131 
val r2 = fold1 kk_product (unary_var_seq arity1 arity2)


1132 
val min_R = min_rep R1 R2


1133 
in


1134 
kk_comprehension


1135 
(decls_for_atom_schema 0 (schema1 @ schema2))


1136 
(kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1)


1137 
(rel_expr_from_rel_expr kk min_R R2 r2))


1138 
end


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


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


1141 
to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))


1142 
 Cst (Num j, @{typ int}, R) =>


1143 
(case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of


1144 
~1 => if is_opt_rep R then Kodkod.None


1145 
else raise NUT ("NitpickKodkod.to_r (Num)", [u])


1146 
 j' => Kodkod.Atom j')


1147 
 Cst (Num j, T, R) =>


1148 
if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)


1149 
else if is_opt_rep R then Kodkod.None


1150 
else raise NUT ("NitpickKodkod.to_r", [u])


1151 
 Cst (Unknown, _, R) => empty_rel_for_rep R


1152 
 Cst (Unrep, _, R) => empty_rel_for_rep R


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


1154 
if domain_type T <> nat_T then suc_rel


1155 
else kk_intersect suc_rel (kk_product Kodkod.Univ (Kodkod.AtomSeq x))


1156 
 Cst (Add, Type ("fun", [@{typ nat}, _]), _) => nat_add_rel


1157 
 Cst (Add, Type ("fun", [@{typ int}, _]), _) => int_add_rel


1158 
 Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) => nat_subtract_rel


1159 
 Cst (Subtract, Type ("fun", [@{typ int}, _]), _) => int_subtract_rel


1160 
 Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) => nat_multiply_rel


1161 
 Cst (Multiply, Type ("fun", [@{typ int}, _]), _) => int_multiply_rel


1162 
 Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => nat_divide_rel


1163 
 Cst (Divide, Type ("fun", [@{typ int}, _]), _) => int_divide_rel


1164 
 Cst (Modulo, Type ("fun", [@{typ nat}, _]), _) => nat_modulo_rel


1165 
 Cst (Modulo, Type ("fun", [@{typ int}, _]), _) => int_modulo_rel


1166 
 Cst (Gcd, _, _) => gcd_rel


1167 
 Cst (Lcm, _, _) => lcm_rel


1168 
 Cst (Fracs, _, Func (Atom (1, _), _)) => Kodkod.None


1169 
 Cst (Fracs, _, Func (Struct _, _)) =>


1170 
kk_project_seq norm_frac_rel 2 2


1171 
 Cst (NormFrac, _, _) => norm_frac_rel


1172 
 Cst (NatToInt, _, Func (Atom _, Atom _)) => Kodkod.Iden


1173 
 Cst (NatToInt, _,


1174 
Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) =>


1175 
if nat_j0 = int_j0 then


1176 
kk_intersect Kodkod.Iden


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


1178 
Kodkod.Univ)


1179 
else


1180 
raise BAD ("NitpickKodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")


1181 
 Cst (IntToNat, _, Func (Atom (int_k, int_j0), nat_R)) =>


1182 
let


1183 
val abs_card = max_int_for_card int_k + 1


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


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


1186 
in


1187 
if nat_j0 = int_j0 then


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


1189 
int_j0 + abs_card))


1190 
(Kodkod.Atom nat_j0))


1191 
(kk_intersect Kodkod.Iden


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


1193 
Kodkod.Univ))


1194 
else


1195 
raise BAD ("NitpickKodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")


1196 
end


1197 
 Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)


1198 
 Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None


1199 
 Op1 (Converse, T, R, u1) =>


1200 
let


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


1202 
val (b_R, a_R) =


1203 
case R of


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


1205 
 Func (R1, _) =>


1206 
if card_of_rep R1 <> 1 then


1207 
raise REP ("NitpickKodkod.to_r (Converse)", [R])


1208 
else


1209 
pairself (Atom o pair 1 o offset_of_type ofs) (b_T, a_T)


1210 
 _ => raise REP ("NitpickKodkod.to_r (Converse)", [R])


1211 
val body_R = body_rep R


1212 
val a_arity = arity_of_rep a_R


1213 
val b_arity = arity_of_rep b_R


1214 
val ab_arity = a_arity + b_arity


1215 
val body_arity = arity_of_rep body_R


1216 
in


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


1218 
(map Kodkod.Num (index_seq a_arity b_arity @


1219 
index_seq 0 a_arity @


1220 
index_seq ab_arity body_arity))


1221 
> rel_expr_from_rel_expr kk R (Func (Struct [b_R, a_R], body_R))


1222 
end


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


1224 
if is_opt_rep R then


1225 
let


1226 
val T1 = type_of u1


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


1228 
val R'' = opt_rep ofs T1 R'


1229 
in


1230 
single_rel_let kk


1231 
(fn r =>


1232 
let


1233 
val true_r = kk_closure (kk_join r true_atom)


1234 
val full_r = full_rel_for_rep R'


1235 
val false_r = kk_difference full_r


1236 
(kk_closure (kk_difference full_r


1237 
(kk_join r false_atom)))


1238 
in


1239 
rel_expr_from_rel_expr kk R R''


1240 
(kk_union (kk_product true_r true_atom)


1241 
(kk_product false_r false_atom))


1242 
end) (to_rep R'' u1)


1243 
end


1244 
else


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


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


1247 
end


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


1249 
(if R1 = Unit then I else kk_product (full_rel_for_rep R1)) false_atom


1250 
 Op1 (SingletonSet, _, R, u1) =>


1251 
(case R of


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


1253 
 Func (Unit, Opt R) => to_guard [u1] R true_atom


1254 
 Func (R1, R2 as Opt _) =>


1255 
single_rel_let kk


1256 
(fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)


1257 
(rel_expr_to_func kk R1 bool_atom_R


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


1259 
(to_opt R1 u1)


1260 
 _ => raise NUT ("NitpickKodkod.to_r (SingletonSet)", [u]))


1261 
 Op1 (Tha, T, R, u1) =>


1262 
if is_opt_rep R then


1263 
kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom


1264 
else


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


1266 
 Op1 (First, T, R, u1) => to_nth_pair_sel 0 T R u1


1267 
 Op1 (Second, T, R, u1) => to_nth_pair_sel 1 T R u1


1268 
 Op1 (Cast, _, R, u1) =>


1269 
((case rep_of u1 of


1270 
Formula _ =>


1271 
(case unopt_rep R of


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


1273 
 _ => raise SAME ())


1274 
 _ => raise SAME ())


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


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


1277 
to_r (Op1 (Not, T, R,


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


1279 
 Op2 (Exist, T, Opt _, u1, u2) =>


1280 
let val rs1 = untuple to_decl u1 in


1281 
if not (is_opt_rep (rep_of u2)) then


1282 
kk_rel_if (kk_exist rs1 (to_f u2)) true_atom Kodkod.None


1283 
else


1284 
let val r2 = to_r u2 in


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


1286 
true_atom Kodkod.None)


1287 
(kk_rel_if (kk_all rs1 (kk_rel_eq r2 false_atom))


1288 
false_atom Kodkod.None)


1289 
end


1290 
end


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


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


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


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


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


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


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


1298 
if type_of u1 = nat_T then


1299 
if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom


1300 
else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom


1301 
else kk_nat_less (to_integer u1) (to_integer u2)


1302 
else


1303 
kk_int_less (to_integer u1) (to_integer u2)


1304 
 Op2 (The, T, R, u1, u2) =>


1305 
if is_opt_rep R then


1306 
let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in


1307 
kk_rel_if (kk_one (kk_join r1 true_atom)) (kk_join r1 true_atom)


1308 
(kk_rel_if (kk_or (kk_some (kk_join r1 true_atom))


1309 
(kk_subset (full_rel_for_rep R)


1310 
(kk_join r1 false_atom)))


1311 
(to_rep R u2) Kodkod.None)


1312 
end


1313 
else


1314 
let val r1 = to_rep (Func (R, Formula Neut)) u1 in


1315 
kk_rel_if (kk_one r1) r1 (to_rep R u2)


1316 
end


1317 
 Op2 (Eps, T, R, u1, u2) =>


1318 
if is_opt_rep (rep_of u1) then


1319 
let


1320 
val r1 = to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1


1321 
val r2 = to_rep R u2


1322 
in


1323 
kk_union (kk_rel_if (kk_one (kk_join r1 true_atom))


1324 
(kk_join r1 true_atom) Kodkod.None)


1325 
(kk_rel_if (kk_or (kk_subset r2 (kk_join r1 true_atom))


1326 
(kk_subset (full_rel_for_rep R)


1327 
(kk_join r1 false_atom)))


1328 
r2 Kodkod.None)


1329 
end


1330 
else


1331 
let


1332 
val r1 = to_rep (Func (unopt_rep R, Formula Neut)) u1


1333 
val r2 = to_rep R u2


1334 
in


1335 
kk_union (kk_rel_if (kk_one r1) r1 Kodkod.None)


1336 
(kk_rel_if (kk_or (kk_no r1) (kk_subset r2 r1))


1337 
r2 Kodkod.None)


1338 
end


1339 
 Op2 (Triad, T, Opt (Atom (2, j0)), u1, u2) =>


1340 
let


1341 
val f1 = to_f u1


1342 
val f2 = to_f u2


1343 
in


1344 
if f1 = f2 then


1345 
atom_from_formula kk j0 f1


1346 
else


1347 
kk_union (kk_rel_if f1 true_atom Kodkod.None)


1348 
(kk_rel_if f2 Kodkod.None false_atom)


1349 
end


1350 
 Op2 (Union, _, R, u1, u2) =>


1351 
to_set_op kk_or kk_or3 kk_union kk_union kk_intersect false R u1 u2


1352 
 Op2 (SetDifference, _, R, u1, u2) =>


1353 
to_set_op kk_notimplies kk_notimplies3 kk_difference kk_intersect


1354 
kk_union true R u1 u2


1355 
 Op2 (Intersect, _, R, u1, u2) =>


1356 
to_set_op kk_and kk_and3 kk_intersect kk_intersect kk_union false R


1357 
u1 u2


1358 
 Op2 (Composition, _, R, u1, u2) =>


1359 
let


1360 
val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u2))


1361 
val (_, c_T) = HOLogic.dest_prodT (domain_type (type_of u1))


1362 
val ab_k = card_of_domain_from_rep 2 (rep_of u2)


1363 
val bc_k = card_of_domain_from_rep 2 (rep_of u1)


1364 
val ac_k = card_of_domain_from_rep 2 R


1365 
val a_k = exact_root 2 (ac_k * ab_k div bc_k)


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


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


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


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


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


1371 
val body_R = body_rep R


1372 
in


1373 
(case body_R of


1374 
Formula Neut =>


1375 
kk_join (to_rep (Func (Struct [a_R, b_R], Formula Neut)) u2)


1376 
(to_rep (Func (Struct [b_R, c_R], Formula Neut)) u1)


1377 
 Opt (Atom (2, _)) =>


1378 
let


1379 
(* Kodkod.rel_expr > rep > rep > nut > Kodkod.rel_expr *)


1380 
fun do_nut r R1 R2 u =


1381 
kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) r


1382 
(* Kodkod.rel_expr > Kodkod.rel_expr *)
