wneuper/isa: src/HOL/Tools/Nitpick/nitpick

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

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2008, 2009, 2010

     5 Kodkod problem generator part of Kodkod.

     6 *)

     8 signature NITPICK_KODKOD =

     9 sig

    10   type hol_context = Nitpick_HOL.hol_context

    11   type dtype_spec = Nitpick_Scope.dtype_spec

    12   type kodkod_constrs = Nitpick_Peephole.kodkod_constrs

    13   type nut = Nitpick_Nut.nut

    14   type nfa_transition = Kodkod.rel_expr * typ

    15   type nfa_entry = typ * nfa_transition list

    16   type nfa_table = nfa_entry list

    18   structure NameTable : TABLE

    20   val univ_card :

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

    22   val check_bits : int -> Kodkod.formula -> unit

    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

    27   val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list

    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 :

    36     hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs

    37     -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list

    38   val kodkod_formula_from_nut :

    39     int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula

    40 end;

    42 structure Nitpick_Kodkod : NITPICK_KODKOD =

    43 struct

    45 open Nitpick_Util

    46 open Nitpick_HOL

    47 open Nitpick_Scope

    48 open Nitpick_Peephole

    49 open Nitpick_Rep

    50 open Nitpick_Nut

    52 structure KK = Kodkod

    54 type nfa_transition = KK.rel_expr * typ

    55 type nfa_entry = typ * nfa_transition list

    56 type nfa_table = nfa_entry list

    58 structure NfaGraph = Typ_Graph

    60 (* int -> KK.int_expr list *)

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

    63 (* int -> int -> int -> KK.bound list -> KK.formula -> int *)

    64 fun univ_card nat_card int_card main_j0 bounds formula =

    65   let

    66     (* KK.rel_expr -> int -> int *)

    67     fun rel_expr_func r k =

    68       Int.max (k, case r of

    69                     KK.Atom j => j + 1

    70                   | KK.AtomSeq (k', j0) => j0 + k'

    71                   | _ => 0)

    72     (* KK.tuple -> int -> int *)

    73     fun tuple_func t k =

    74       case t of

    75         KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k

    76       | _ => k

    77     (* KK.tuple_set -> int -> int *)

    78     fun tuple_set_func ts k =

    79       Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k' | _ => 0)

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

    81                   int_expr_func = K I}

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

    83     val card = fold (KK.fold_bound expr_F tuple_F) bounds 1

    84                |> KK.fold_formula expr_F formula

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

    87 (* int -> KK.formula -> unit *)

    88 fun check_bits bits formula =

    89   let

    90     (* KK.int_expr -> unit -> unit *)

    91     fun int_expr_func (KK.Num k) () =

    92         if is_twos_complement_representable bits k then

    93           ()

    94         else

    95           raise TOO_SMALL ("Nitpick_Kodkod.check_bits",

    96                            "\"bits\" value " ^ string_of_int bits ^

    97                            " too small for problem")

    98       | int_expr_func _ () = ()

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

   100                   int_expr_func = int_expr_func}

   101   in KK.fold_formula expr_F formula () end

   103 (* int -> int -> unit *)

   104 fun check_arity univ_card n =

   105   if n > KK.max_arity univ_card then

   106     raise TOO_LARGE ("Nitpick_Kodkod.check_arity",

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

   108                      \cardinality " ^ string_of_int univ_card)

   109   else

   110     ()

   112 (* bool -> int -> int list -> KK.tuple *)

   113 fun kk_tuple debug univ_card js =

   114   if debug then

   115     KK.Tuple js

   116   else

   117     KK.TupleIndex (length js,

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

   120 (* (int * int) list -> KK.tuple_set *)

   121 val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq

   122 (* rep -> KK.tuple_set *)

   123 val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep

   125 (* int -> KK.tuple_set *)

   126 val single_atom = KK.TupleSet o single o KK.Tuple o single

   127 (* int -> KK.int_bound list *)

   128 fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]

   129 (* int -> int -> KK.int_bound list *)

   130 fun pow_of_two_int_bounds bits j0 =

   131   let

   132     (* int -> int -> int -> KK.int_bound list *)

   133     fun aux 0  _ _ = []

   134       | aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])]

   135       | aux iter pow_of_two j =

   136         (SOME pow_of_two, [single_atom j]) ::

   137         aux (iter - 1) (2 * pow_of_two) (j + 1)

   138   in aux (bits + 1) 1 j0 end

   140 (* KK.formula -> KK.n_ary_index list *)

   141 fun built_in_rels_in_formula formula =

   142   let

   143     (* KK.rel_expr -> KK.n_ary_index list -> KK.n_ary_index list *)

   144     fun rel_expr_func (KK.Rel (x as (n, j))) =

   145         if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then

   146           I

   147         else

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

   149              SOME k => j < k ? insert (op =) x

   150            | NONE => I)

   151       | rel_expr_func _ = I

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

   153                   int_expr_func = K I}

   154   in KK.fold_formula expr_F formula [] end

   156 val max_table_size = 65536

   158 (* int -> unit *)

   159 fun check_table_size k =

   160   if k > max_table_size then

   161     raise TOO_LARGE ("Nitpick_Kodkod.check_table_size",

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

   163   else

   164     ()

   166 (* bool -> int -> int * int -> (int -> int) -> KK.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) -> KK.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    -> KK.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) -> KK.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) -> KK.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)))

   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

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

   231    -> string * bool * KK.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;

   234    if x = not3_rel then

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

   236    else if x = suc_rel then

   237      ("suc", tabulate_func1 debug univ_card (univ_card - j0 - 1, j0)

   238                             (Integer.add 1))

   239    else if x = nat_add_rel then

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

   241    else if x = int_add_rel then

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

   243    else if x = nat_subtract_rel then

   244      ("nat_subtract",

   245       tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus))

   246    else if x = int_subtract_rel then

   247      ("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op -))

   248    else if x = nat_multiply_rel then

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

   250    else if x = int_multiply_rel then

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

   252    else if x = nat_divide_rel then

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

   254    else if x = int_divide_rel then

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

   256    else if x = nat_less_rel then

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

   258                                    (int_from_bool o op <))

   259    else if x = int_less_rel then

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

   261                                    (int_from_bool o op <))

   262    else if x = gcd_rel then

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

   264    else if x = lcm_rel then

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

   266    else if x = norm_frac_rel then

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

   268                                       isa_norm_frac)

   269    else

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

   272 (* bool -> int -> int -> int -> int -> int * int -> KK.rel_expr -> KK.bound *)

   273 fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x =

   274   let

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

   276                                            j0 x

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

   279 (* bool -> int -> int -> int -> int -> KK.formula -> KK.bound list *)

   280 fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 =

   281   map (bound_for_built_in_rel debug univ_card nat_card int_card j0)

   282   o built_in_rels_in_formula

   284 (* Proof.context -> bool -> string -> typ -> rep -> string *)

   285 fun bound_comment ctxt debug nick T R =

   286   short_name nick ^

   287   (if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^

   288   " : " ^ string_for_rep R

   290 (* Proof.context -> bool -> nut -> KK.bound *)

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

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

   293      if nick = @{const_name bisim_iterator_max} then

   294        case R of

   295          Atom (k, j0) => [single_atom (k - 1 + j0)]

   296        | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])

   297      else

   298        [KK.TupleSet [], upper_bound_for_rep R])

   299   | bound_for_plain_rel _ _ u =

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

   302 (* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *)

   303 fun bound_for_sel_rel ctxt debug dtypes

   304         (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),

   305                   R as Func (Atom (_, j0), R2), nick)) =

   306     let

   307       val {delta, epsilon, exclusive, explicit_max, ...} =

   308         constr_spec dtypes (original_name nick, T1)

   309     in

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

   311        if explicit_max = 0 then

   312          [KK.TupleSet []]

   313        else

   314          let val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) in

   315            if R2 = Formula Neut then

   316              [ts] |> not exclusive ? cons (KK.TupleSet [])

   317            else

   318              [KK.TupleSet [],

   319               if T1 = T2 andalso epsilon > delta andalso

   320                  (datatype_spec dtypes T1 |> the |> pairf #co #standard)

   321                  = (false, true) then

   322                 index_seq delta (epsilon - delta)

   323                 |> map (fn j =>

   324                            KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],

   325                                             KK.TupleAtomSeq (j, j0)))

   326                 |> foldl1 KK.TupleUnion

   327               else

   328                 KK.TupleProduct (ts, upper_bound_for_rep R2)]

   329          end)

   330     end

   331   | bound_for_sel_rel _ _ _ u =

   332     raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])

   334 (* KK.bound list -> KK.bound list *)

   335 fun merge_bounds bs =

   336   let

   337     (* KK.bound -> int *)

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

   339     (* KK.bound list -> KK.bound -> KK.bound list -> KK.bound list *)

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

   341       | add_bound ds b (c :: cs) =

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

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

   344         else

   345           add_bound (c :: ds) b cs

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

   348 (* int -> int -> KK.rel_expr list *)

   349 fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n)

   351 (* int list -> KK.rel_expr *)

   352 val singleton_from_combination = foldl1 KK.Product o map KK.Atom

   353 (* rep -> KK.rel_expr list *)

   354 fun all_singletons_for_rep R =

   355   if is_lone_rep R then

   356     all_combinations_for_rep R |> map singleton_from_combination

   357   else

   358     raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R])

   360 (* KK.rel_expr -> KK.rel_expr list *)

   361 fun unpack_products (KK.Product (r1, r2)) =

   362     unpack_products r1 @ unpack_products r2

   363   | unpack_products r = [r]

   364 fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2

   365   | unpack_joins r = [r]

   367 (* rep -> KK.rel_expr *)

   368 val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep

   369 fun full_rel_for_rep R =

   370   case atom_schema_of_rep R of

   371     [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])

   372   | schema => foldl1 KK.Product (map KK.AtomSeq schema)

   374 (* int -> int list -> KK.decl list *)

   375 fun decls_for_atom_schema j0 schema =

   376   map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x))

   377        (index_seq j0 (length schema)) schema

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

   381 (* kodkod_constrs -> rep -> KK.rel_expr -> KK.formula *)

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

   383                      R r =

   384   let val body_R = body_rep R in

   385     if is_lone_rep body_R then

   386       let

   387         val binder_schema = atom_schema_of_reps (binder_reps R)

   388         val body_schema = atom_schema_of_rep body_R

   389         val one = is_one_rep body_R

   390         val opt_x = case r of KK.Rel x => SOME x | _ => NONE

   391       in

   392         if opt_x <> NONE andalso length binder_schema = 1 andalso

   393            length body_schema = 1 then

   394           (if one then KK.Function else KK.Functional)

   395               (the opt_x, KK.AtomSeq (hd binder_schema),

   396                KK.AtomSeq (hd body_schema))

   397         else

   398           let

   399             val decls = decls_for_atom_schema ~1 binder_schema

   400             val vars = unary_var_seq ~1 (length binder_schema)

   401             val kk_xone = if one then kk_one else kk_lone

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

   403       end

   404     else

   405       KK.True

   406   end

   407 fun kk_n_ary_function kk R (r as KK.Rel x) =

   408     if not (is_opt_rep R) then

   409       if x = suc_rel then

   410         KK.False

   411       else if x = nat_add_rel then

   412         formula_for_bool (card_of_rep (body_rep R) = 1)

   413       else if x = nat_multiply_rel then

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

   415       else

   416         d_n_ary_function kk R r

   417     else if x = nat_subtract_rel then

   418       KK.True

   419     else

   420       d_n_ary_function kk R r

   421   | kk_n_ary_function kk R r = d_n_ary_function kk R r

   423 (* kodkod_constrs -> KK.rel_expr list -> KK.formula *)

   424 fun kk_disjoint_sets _ [] = KK.True

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

   426                      (r :: rs) =

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

   429 (* int -> kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr

   430    -> KK.rel_expr *)

   431 fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =

   432   if inline_rel_expr r then

   433     f r

   434   else

   435     let val x = (KK.arity_of_rel_expr r, j) in

   436       kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x))

   437     end

   438 (* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr

   439    -> KK.rel_expr *)

   440 val single_rel_rel_let = basic_rel_rel_let 0

   441 (* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr) -> KK.rel_expr

   442    -> KK.rel_expr -> KK.rel_expr *)

   443 fun double_rel_rel_let kk f r1 r2 =

   444   single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1

   445 (* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr)

   446    -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)

   447 fun triple_rel_rel_let kk f r1 r2 r3 =

   448   double_rel_rel_let kk

   449       (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2

   451 (* kodkod_constrs -> int -> KK.formula -> KK.rel_expr *)

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

   453   kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0)

   454 (* kodkod_constrs -> rep -> KK.formula -> KK.rel_expr *)

   455 fun rel_expr_from_formula kk R f =

   456   case unopt_rep R of

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

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

   460 (* kodkod_cotrs -> int -> int -> KK.rel_expr -> KK.rel_expr list *)

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

   462                           num_chunks r =

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

   464                                                     chunk_arity)

   466 (* kodkod_constrs -> bool -> rep -> rep -> KK.rel_expr -> KK.rel_expr

   467    -> KK.rel_expr *)

   468 fun kk_n_fold_join

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

   470         res_R r1 r2 =

   471   case arity_of_rep R1 of

   472     1 => kk_join r1 r2

   473   | arity1 =>

   474     let

   475       val unpacked_rs1 =

   476         if inline_rel_expr r1 then unpack_vect_in_chunks kk 1 arity1 r1

   477         else unpack_products r1

   478     in

   479       if one andalso length unpacked_rs1 = arity1 then

   480         fold kk_join unpacked_rs1 r2

   481       else

   482         kk_project_seq

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

   484             arity1 (arity_of_rep res_R)

   485     end

   487 (* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr list

   488    -> KK.rel_expr list -> KK.rel_expr *)

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

   490   if rs1 = rs2 then r

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

   493 val lone_rep_fallback_max_card = 4096

   494 val some_j0 = 0

   496 (* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)

   497 fun lone_rep_fallback kk new_R old_R r =

   498   if old_R = new_R then

   499     r

   500   else

   501     let val card = card_of_rep old_R in

   502       if is_lone_rep old_R andalso is_lone_rep new_R andalso

   503          card = card_of_rep new_R then

   504         if card >= lone_rep_fallback_max_card then

   505           raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback",

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

   507         else

   508           kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)

   509                          (all_singletons_for_rep new_R)

   510       else

   511         raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])

   512     end

   513 (* kodkod_constrs -> int * int -> rep -> KK.rel_expr -> KK.rel_expr *)

   514 and atom_from_rel_expr kk x old_R r =

   515   case old_R of

   516     Func (R1, R2) =>

   517     let

   518       val dom_card = card_of_rep R1

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

   520     in

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

   522                          (vect_from_rel_expr kk dom_card R2' old_R r)

   523     end

   524   | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R])

   525   | _ => lone_rep_fallback kk (Atom x) old_R r

   526 (* kodkod_constrs -> rep list -> rep -> KK.rel_expr -> KK.rel_expr *)

   527 and struct_from_rel_expr kk Rs old_R r =

   528   case old_R of

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

   530   | Struct Rs' =>

   531     let

   532       val Rs = filter (not_equal Unit) Rs

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

   534     in

   535       if Rs' = Rs then

   536         r

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

   538         let

   539           val old_arities = map arity_of_rep Rs'

   540           val old_offsets = offset_list old_arities

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

   542         in

   543           fold1 (#kk_product kk)

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

   545         end

   546       else

   547         lone_rep_fallback kk (Struct Rs) old_R r

   548     end

   549   | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])

   550 (* kodkod_constrs -> int -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)

   551 and vect_from_rel_expr kk k R old_R r =

   552   case old_R of

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

   554   | Vect (k', R') =>

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

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

   557   | Func (R1, Formula Neut) =>

   558     if k = card_of_rep R1 then

   559       fold1 (#kk_product kk)

   560             (map (fn arg_r =>

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

   562                  (all_singletons_for_rep R1))

   563     else

   564       raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])

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

   566   | Func (R1, R2) =>

   567     fold1 (#kk_product kk)

   568           (map (fn arg_r =>

   569                    rel_expr_from_rel_expr kk R R2

   570                                          (kk_n_fold_join kk true R1 R2 arg_r r))

   571                (all_singletons_for_rep R1))

   572   | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])

   573 (* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)

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

   575     let

   576       val dom_card = card_of_rep R1

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

   578     in

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

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

   581     end

   582   | func_from_no_opt_rel_expr kk Unit R2 old_R r =

   583     (case old_R of

   584        Vect (_, R') => rel_expr_from_rel_expr kk R2 R' r

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

   586      | Func (Atom (1, _), Formula Neut) =>

   587        (case unopt_rep R2 of

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

   589         | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",

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

   591      | Func (R1', R2') =>

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

   593                               (arity_of_rep R2'))

   594      | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",

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

   596   | func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r =

   597     (case old_R of

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

   599        let

   600          val args_rs = all_singletons_for_rep R1

   601          val vals_rs = unpack_vect_in_chunks kk 1 k r

   602          (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)

   603          fun empty_or_singleton_set_for arg_r val_r =

   604            #kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r)

   605        in

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

   607        end

   608      | Func (R1', Formula Neut) =>

   609        if R1 = R1' then

   610          r

   611        else

   612          let

   613            val schema = atom_schema_of_rep R1

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

   615                     |> rel_expr_from_rel_expr kk R1' R1

   616            val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk

   617          in

   618            #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)

   619          end

   620      | Func (Unit, (Atom (2, j0))) =>

   621        #kk_rel_if kk (#kk_rel_eq kk r (KK.Atom (j0 + 1)))

   622                   (full_rel_for_rep R1) (empty_rel_for_rep R1)

   623      | Func (R1', Atom (2, j0)) =>

   624        func_from_no_opt_rel_expr kk R1 (Formula Neut)

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

   626      | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",

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

   628   | func_from_no_opt_rel_expr kk R1 R2 old_R r =

   629     case old_R of

   630       Vect (k, R) =>

   631       let

   632         val args_rs = all_singletons_for_rep R1

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

   634                       |> map (rel_expr_from_rel_expr kk R2 R)

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

   636     | Func (R1', Formula Neut) =>

   637       (case R2 of

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

   639          let val schema = atom_schema_of_rep R1 in

   640            if length schema = 1 then

   641              #kk_override kk (#kk_product kk (KK.AtomSeq (hd schema))

   642                                              (KK.Atom j0))

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

   644            else

   645              let

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

   647                         |> rel_expr_from_rel_expr kk R1' R1

   648                val r2 = KK.Var (1, ~(length schema) - 1)

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

   650              in

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

   652                                  (#kk_subset kk r2 r3)

   653              end

   654            end

   655          | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",

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

   657     | Func (Unit, R2') =>

   658       let val j0 = some_j0 in

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

   660                                   (#kk_product kk (KK.Atom j0) r)

   661       end

   662     | Func (R1', R2') =>

   663       if R1 = R1' andalso R2 = R2' then

   664         r

   665       else

   666         let

   667           val dom_schema = atom_schema_of_rep R1

   668           val ran_schema = atom_schema_of_rep R2

   669           val dom_prod = fold1 (#kk_product kk)

   670                                (unary_var_seq ~1 (length dom_schema))

   671                          |> rel_expr_from_rel_expr kk R1' R1

   672           val ran_prod = fold1 (#kk_product kk)

   673                                (unary_var_seq (~(length dom_schema) - 1)

   674                                               (length ran_schema))

   675                          |> rel_expr_from_rel_expr kk R2' R2

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

   677           val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk

   678         in

   679           #kk_comprehension kk (decls_for_atom_schema ~1

   680                                                       (dom_schema @ ran_schema))

   681                                (kk_xeq ran_prod app)

   682         end

   683     | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",

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

   685 (* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)

   686 and rel_expr_from_rel_expr kk new_R old_R r =

   687   let

   688     val unopt_old_R = unopt_rep old_R

   689     val unopt_new_R = unopt_rep new_R

   690   in

   691     if unopt_old_R <> old_R andalso unopt_new_R = new_R then

   692       raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R])

   693     else if unopt_new_R = unopt_old_R then

   694       r

   695     else

   696       (case unopt_new_R of

   697          Atom x => atom_from_rel_expr kk x

   698        | Struct Rs => struct_from_rel_expr kk Rs

   699        | Vect (k, R') => vect_from_rel_expr kk k R'

   700        | Func (R1, R2) => func_from_no_opt_rel_expr kk R1 R2

   701        | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr",

   702                          [old_R, new_R]))

   703           unopt_old_R r

   704   end

   705 (* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)

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

   708 (* kodkod_constrs -> typ -> KK.rel_expr -> KK.rel_expr *)

   709 fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r =

   710   kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then

   711                        unsigned_bit_word_sel_rel

   712                      else

   713                        signed_bit_word_sel_rel))

   714 (* kodkod_constrs -> typ -> KK.rel_expr -> KK.int_expr *)

   715 val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom

   716 (* kodkod_constrs -> typ -> rep -> KK.int_expr -> KK.rel_expr *)

   717 fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}

   718                         : kodkod_constrs) T R i =

   719   kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))

   720                    (kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1)))

   721                               (KK.Bits i))

   723 (* kodkod_constrs -> nut -> KK.formula *)

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

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

   726                       (KK.Rel x)

   727   | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs)

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

   729     if is_one_rep R then kk_one (KK.Rel x)

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

   731     else KK.True

   732   | declarative_axiom_for_plain_rel _ u =

   733     raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])

   735 (* nut NameTable.table -> styp -> KK.rel_expr * rep * int *)

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

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

   738     FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)

   739   | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])

   741 (* nut NameTable.table -> styp -> KK.rel_expr *)

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

   744 (* hol_context -> bool -> kodkod_constrs -> nut NameTable.table

   745    -> dtype_spec list -> styp -> int -> nfa_transition list *)

   746 fun nfa_transitions_for_sel hol_ctxt binarize

   747                             ({kk_project, ...} : kodkod_constrs) rel_table

   748                             (dtypes : dtype_spec list) constr_x n =

   749   let

   750     val x as (_, T) =

   751       binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n

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

   753     val type_schema = type_schema_of_rep T R

   754   in

   755     map_filter (fn (j, T) =>

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

   757                    else SOME (kk_project r (map KK.Num [0, j]), T))

   758                (index_seq 1 (arity - 1) ~~ tl type_schema)

   759   end

   760 (* hol_context -> bool -> kodkod_constrs -> nut NameTable.table

   761    -> dtype_spec list -> styp -> nfa_transition list *)

   762 fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes

   763                                (x as (_, T)) =

   764   maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)

   765        (index_seq 0 (num_sels_for_constr_type T))

   766 (* hol_context -> bool -> kodkod_constrs -> nut NameTable.table

   767    -> dtype_spec list -> dtype_spec -> nfa_entry option *)

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

   769   | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE

   770   | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE

   771   | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes

   772                            {typ, constrs, ...} =

   773     SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table

   774                                                 dtypes o #const) constrs)

   776 val empty_rel = KK.Product (KK.None, KK.None)

   778 (* nfa_table -> typ -> typ -> KK.rel_expr list *)

   779 fun direct_path_rel_exprs nfa start_T final_T =

   780   case AList.lookup (op =) nfa final_T of

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

   782   | NONE => []

   783 (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *)

   784 and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T

   785                       final_T =

   786     fold kk_union (direct_path_rel_exprs nfa start_T final_T)

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

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

   789     kk_union (any_path_rel_expr kk nfa Ts start_T final_T)

   790              (knot_path_rel_expr kk nfa Ts start_T T final_T)

   791 (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ

   792    -> KK.rel_expr *)

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

   794                        start_T knot_T final_T =

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

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

   797           (any_path_rel_expr kk nfa Ts start_T knot_T)

   798 (* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *)

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

   800     fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel

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

   802                        start_T =

   803     if start_T = T then

   804       kk_closure (loop_path_rel_expr kk nfa Ts start_T)

   805     else

   806       kk_union (loop_path_rel_expr kk nfa Ts start_T)

   807                (knot_path_rel_expr kk nfa Ts start_T T start_T)

   809 (* nfa_table -> unit NfaGraph.T *)

   810 fun graph_for_nfa nfa =

   811   let

   812     (* typ -> unit NfaGraph.T -> unit NfaGraph.T *)

   813     fun new_node T = perhaps (try (NfaGraph.new_node (T, ())))

   814     (* nfa_table -> unit NfaGraph.T -> unit NfaGraph.T *)

   815     fun add_nfa [] = I

   816       | add_nfa ((_, []) :: nfa) = add_nfa nfa

   817       | add_nfa ((T, ((_, T') :: transitions)) :: nfa) =

   818         add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o

   819         new_node T' o new_node T

   820   in add_nfa nfa NfaGraph.empty end

   822 (* nfa_table -> nfa_table list *)

   823 fun strongly_connected_sub_nfas nfa =

   824   nfa |> graph_for_nfa |> NfaGraph.strong_conn

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

   827 (* kodkod_constrs -> nfa_table -> typ -> KK.formula *)

   828 fun acyclicity_axiom_for_datatype kk nfa start_T =

   829   #kk_no kk (#kk_intersect kk

   830                  (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)

   831 (* hol_context -> bool -> kodkod_constrs -> nut NameTable.table

   832    -> dtype_spec list -> KK.formula list *)

   833 fun acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes =

   834   map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)

   835              dtypes

   836   |> strongly_connected_sub_nfas

   837   |> maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa)

   839 (* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table

   840    -> KK.rel_expr -> constr_spec -> int -> KK.formula *)

   841 fun sel_axiom_for_sel hol_ctxt binarize j0

   842         (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})

   843         rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)

   844         n =

   845   let

   846     val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n

   847     val (r, R, _) = const_triple rel_table x

   848     val R2 = dest_Func R |> snd

   849     val z = (epsilon - delta, delta + j0)

   850   in

   851     if exclusive then

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

   853     else

   854       let val r' = kk_join (KK.Var (1, 0)) r in

   855         kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]

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

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

   858       end

   859   end

   860 (* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table

   861    -> constr_spec -> KK.formula list *)

   862 fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table

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

   864   let

   865     val honors_explicit_max =

   866       explicit_max < 0 orelse epsilon - delta <= explicit_max

   867   in

   868     if explicit_max = 0 then

   869       [formula_for_bool honors_explicit_max]

   870     else

   871       let

   872         val dom_r = discr_rel_expr rel_table const

   873         val max_axiom =

   874           if honors_explicit_max then

   875             KK.True

   876           else if is_twos_complement_representable bits (epsilon - delta) then

   877             KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)

   878           else

   879             raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",

   880                              "\"bits\" value " ^ string_of_int bits ^

   881                              " too small for \"max\"")

   882       in

   883         max_axiom ::

   884         map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)

   885             (index_seq 0 (num_sels_for_constr_type (snd const)))

   886       end

   887   end

   888 (* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table

   889    -> dtype_spec -> KK.formula list *)

   890 fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table

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

   892   maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs

   894 (* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> constr_spec

   895    -> KK.formula list *)

   896 fun uniqueness_axiom_for_constr hol_ctxt binarize

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

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

   899   let

   900     (* KK.rel_expr -> KK.formula *)

   901     fun conjunct_for_sel r =

   902       kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)

   903     val num_sels = num_sels_for_constr_type (snd const)

   904     val triples =

   905       map (const_triple rel_table

   906            o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)

   907           (~1 upto num_sels - 1)

   908     val set_r = triples |> hd |> #1

   909   in

   910     if num_sels = 0 then

   911       kk_lone set_r

   912     else

   913       kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])

   914              (kk_implies

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

   916                   (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))

   917   end

   918 (* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> dtype_spec

   919    -> KK.formula list *)

   920 fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table

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

   922   map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs

   924 (* constr_spec -> int *)

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

   926 (* int -> kodkod_constrs -> nut NameTable.table -> dtype_spec

   927    -> KK.formula list *)

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

   929                                   rel_table

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

   931   if forall #exclusive constrs then

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

   933   else

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

   935       [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),

   936        kk_disjoint_sets kk rs]

   937     end

   939 (* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs

   940    -> nut NameTable.table -> dtype_spec -> KK.formula list *)

   941 fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []

   942   | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table

   943                               (dtype as {typ, ...}) =

   944     let val j0 = offset_of_type ofs typ in

   945       sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @

   946       uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @

   947       partition_axioms_for_datatype j0 kk rel_table dtype

   948     end

   950 (* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs

   951    -> nut NameTable.table -> dtype_spec list -> KK.formula list *)

   952 fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table

   953                                      dtypes =

   954   acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes @

   955   maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)

   956        dtypes

   958 (* int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)

   959 fun kodkod_formula_from_nut ofs

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

   961                 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,

   962                 kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,

   963                 kk_difference, kk_intersect, kk_product, kk_join, kk_closure,

   964                 kk_comprehension, kk_project, kk_project_seq, kk_not3,

   965                 kk_nat_less, kk_int_less, ...}) u =

   966   let

   967     val main_j0 = offset_of_type ofs bool_T

   968     val bool_j0 = main_j0

   969     val bool_atom_R = Atom (2, main_j0)

   970     val false_atom = KK.Atom bool_j0

   971     val true_atom = KK.Atom (bool_j0 + 1)

   973     (* polarity -> int -> KK.rel_expr -> KK.formula *)

   974     fun formula_from_opt_atom polar j0 r =

   975       case polar of

   976         Neg => kk_not (kk_rel_eq r (KK.Atom j0))

   977       | _ => kk_rel_eq r (KK.Atom (j0 + 1))

   978     (* int -> KK.rel_expr -> KK.formula *)

   979     val formula_from_atom = formula_from_opt_atom Pos

   981     (* KK.formula -> KK.formula -> KK.formula *)

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

   983     (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)

   984     val kk_or3 =

   985       double_rel_rel_let kk

   986           (fn r1 => fn r2 =>

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

   988                         (kk_intersect r1 r2))

   989     val kk_and3 =

   990       double_rel_rel_let kk

   991           (fn r1 => fn r2 =>

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

   993                         (kk_intersect r1 r2))

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

   996     (* int -> KK.rel_expr -> KK.formula list *)

   997     val unpack_formulas =

   998       map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1

   999     (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr

  1000        -> KK.rel_expr -> KK.rel_expr *)

  1001     fun kk_vect_set_op connective k r1 r2 =

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

  1003                              (unpack_formulas k r1) (unpack_formulas k r2))

  1004     (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr

  1005        -> KK.rel_expr -> KK.formula *)

  1006     fun kk_vect_set_bool_op connective k r1 r2 =

  1007       fold1 kk_and (map2 connective (unpack_formulas k r1)

  1008                          (unpack_formulas k r2))

  1010     (* nut -> KK.formula *)

  1011     fun to_f u =

  1012       case rep_of u of

  1013         Formula polar =>

  1014         (case u of

  1015            Cst (False, _, _) => KK.False

  1016          | Cst (True, _, _) => KK.True

  1017          | Op1 (Not, _, _, u1) =>

  1018            kk_not (to_f_with_polarity (flip_polarity polar) u1)

  1019          | Op1 (Finite, _, _, u1) =>

  1020            let val opt1 = is_opt_rep (rep_of u1) in

  1021              case polar of

  1022                Neut =>

  1023                if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])

  1024                else KK.True

  1025              | Pos => formula_for_bool (not opt1)

  1026              | Neg => KK.True

  1027            end

  1028          | Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1)

  1029          | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1

  1030          | Op2 (All, _, _, u1, u2) =>

  1031            kk_all (untuple to_decl u1) (to_f_with_polarity polar u2)

  1032          | Op2 (Exist, _, _, u1, u2) =>

  1033            kk_exist (untuple to_decl u1) (to_f_with_polarity polar u2)

  1034          | Op2 (Or, _, _, u1, u2) =>

  1035            kk_or (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)

  1036          | Op2 (And, _, _, u1, u2) =>

  1037            kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)

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

  1039            formula_from_opt_atom polar bool_j0

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

  1041          | Op2 (Subset, _, _, u1, u2) =>

  1042            let

  1043              val dom_T = domain_type (type_of u1)

  1044              val R1 = rep_of u1

  1045              val R2 = rep_of u2

  1046              val (dom_R, ran_R) =

  1047                case min_rep R1 R2 of

  1048                  Func (Unit, R') =>

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

  1050                | Func Rp => Rp

  1051                | R => (Atom (card_of_domain_from_rep 2 R,

  1052                              offset_of_type ofs dom_T),

  1053                        if is_opt_rep R then Opt bool_atom_R else Formula Neut)

  1054              val set_R = Func (dom_R, ran_R)

  1055            in

  1056              if not (is_opt_rep ran_R) then

  1057                to_set_bool_op kk_implies kk_subset u1 u2

  1058              else if polar = Neut then

  1059                raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u])

  1060              else

  1061                let

  1062                  (* FIXME: merge with similar code below *)

  1063                  (* bool -> nut -> KK.rel_expr *)

  1064                  fun set_to_r widen u =

  1065                    if widen then

  1066                      kk_difference (full_rel_for_rep dom_R)

  1067                                    (kk_join (to_rep set_R u) false_atom)

  1068                    else

  1069                      kk_join (to_rep set_R u) true_atom

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

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

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

  1073            end

  1074          | Op2 (DefEq, _, _, u1, u2) =>

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

  1076               Unit => KK.True

  1077             | Formula polar =>

  1078               kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)

  1079             | min_R =>

  1080               let

  1081                 (* nut -> nut list *)

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

  1083                   | args (Tuple (_, _, us)) = us

  1084                   | args _ = []

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

  1086               in

  1087                 if null opt_arg_us orelse not (is_Opt min_R) orelse

  1088                    is_eval_name u1 then

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

  1090                        (kk_rel_eq (to_rep min_R u1) (to_rep min_R u2))

  1091                 else

  1092                   kk_subset (to_rep min_R u1) (to_rep min_R u2)

  1093               end)

  1094          | Op2 (Eq, _, _, u1, u2) =>

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

  1096               Unit => KK.True

  1097             | Formula polar =>

  1098               kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)

  1099             | min_R =>

  1100               if is_opt_rep min_R then

  1101                 if polar = Neut then

  1102                   (* continuation of hackish optimization *)

  1103                   kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)

  1104                 else if is_Cst Unrep u1 then

  1105                   to_could_be_unrep (polar = Neg) u2

  1106                 else if is_Cst Unrep u2 then

  1107                   to_could_be_unrep (polar = Neg) u1

  1108                 else

  1109                   let

  1110                     val r1 = to_rep min_R u1

  1111                     val r2 = to_rep min_R u2

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

  1113                   in

  1114                     (if polar = Pos then

  1115                        if not both_opt then

  1116                          kk_rel_eq r1 r2

  1117                        else if is_lone_rep min_R andalso

  1118                                arity_of_rep min_R = 1 then

  1119                          kk_some (kk_intersect r1 r2)

  1120                        else

  1121                          raise SAME ()

  1122                      else

  1123                        if is_lone_rep min_R then

  1124                          if arity_of_rep min_R = 1 then

  1125                            kk_lone (kk_union r1 r2)

  1126                          else if not both_opt then

  1127                            (r1, r2) |> is_opt_rep (rep_of u2) ? swap

  1128                                     |-> kk_subset

  1129                          else

  1130                            raise SAME ()

  1131                        else

  1132                          raise SAME ())

  1133                     handle SAME () =>

  1134                            formula_from_opt_atom polar bool_j0

  1135                                (to_guard [u1, u2] bool_atom_R

  1136                                          (rel_expr_from_formula kk bool_atom_R

  1137                                                             (kk_rel_eq r1 r2)))

  1138                   end

  1139               else

  1140                 let

  1141                   val r1 = to_rep min_R u1

  1142                   val r2 = to_rep min_R u2

  1143                 in

  1144                   if is_one_rep min_R then

  1145                     let

  1146                       val rs1 = unpack_products r1

  1147                       val rs2 = unpack_products r2

  1148                     in

  1149                       if length rs1 = length rs2 andalso

  1150                          map KK.arity_of_rel_expr rs1

  1151                          = map KK.arity_of_rel_expr rs2 then

  1152                         fold1 kk_and (map2 kk_subset rs1 rs2)

  1153                       else

  1154                         kk_subset r1 r2

  1155                     end

  1156                   else

  1157                     kk_rel_eq r1 r2

  1158                 end)

  1159          | Op2 (The, T, _, u1, u2) =>

  1160            to_f_with_polarity polar

  1161                               (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2))

  1162          | Op2 (Eps, T, _, u1, u2) =>

  1163            to_f_with_polarity polar

  1164                               (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2))

  1165          | Op2 (Apply, T, _, u1, u2) =>

  1166            (case (polar, rep_of u1) of

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

  1168             | _ =>

  1169               to_f_with_polarity polar

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

  1171          | Op3 (Let, _, _, u1, u2, u3) =>

  1172            kk_formula_let [to_expr_assign u1 u2] (to_f_with_polarity polar u3)

  1173          | Op3 (If, _, _, u1, u2, u3) =>

  1174            kk_formula_if (to_f u1) (to_f_with_polarity polar u2)

  1175                          (to_f_with_polarity polar u3)

  1176          | FormulaReg (j, _, _) => KK.FormulaReg j

  1177          | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))

  1178       | Atom (2, j0) => formula_from_atom j0 (to_r u)

  1179       | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])

  1180     (* polarity -> nut -> KK.formula *)

  1181     and to_f_with_polarity polar u =

  1182       case rep_of u of

  1183         Formula _ => to_f u

  1184       | Atom (2, j0) => formula_from_atom j0 (to_r u)

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

  1186       | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u])

  1187     (* nut -> KK.rel_expr *)

  1188     and to_r u =

  1189       case u of

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

  1191       | Cst (True, _, Atom _) => true_atom

  1192       | Cst (Iden, _, Func (Struct [R1, R2], Formula Neut)) =>

  1193         if R1 = R2 andalso arity_of_rep R1 = 1 then

  1194           kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ)

  1195         else

  1196           let

  1197             val schema1 = atom_schema_of_rep R1

  1198             val schema2 = atom_schema_of_rep R2

  1199             val arity1 = length schema1

  1200             val arity2 = length schema2

  1201             val r1 = fold1 kk_product (unary_var_seq 0 arity1)

  1202             val r2 = fold1 kk_product (unary_var_seq arity1 arity2)

  1203             val min_R = min_rep R1 R2

  1204           in

  1205             kk_comprehension

  1206                 (decls_for_atom_schema 0 (schema1 @ schema2))

  1207                 (kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1)

  1208                            (rel_expr_from_rel_expr kk min_R R2 r2))

  1209           end

  1210       | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0

  1211       | Cst (Iden, T as Type (@{type_name fun}, [T1, _]), R as Func (R1, _)) =>

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

  1213       | Cst (Num j, T, R) =>

  1214         if is_word_type T then

  1215           atom_from_int_expr kk T R (KK.Num j)

  1216         else if T = int_T then

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

  1218             ~1 => if is_opt_rep R then KK.None

  1219                   else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])

  1220           | j' => KK.Atom j'

  1221         else

  1222           if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T)

  1223           else if is_opt_rep R then KK.None

  1224           else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])

  1225       | Cst (Unknown, _, R) => empty_rel_for_rep R

  1226       | Cst (Unrep, _, R) => empty_rel_for_rep R

  1227       | Cst (Suc, T as @{typ "unsigned_bit word => unsigned_bit word"}, R) =>

  1228         to_bit_word_unary_op T R (curry KK.Add (KK.Num 1))

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

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

  1231       | Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel

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

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

  1234       | Cst (Add, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>

  1235         to_bit_word_binary_op T R NONE (SOME (curry KK.Add))

  1236       | Cst (Add, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>

  1237         to_bit_word_binary_op T R

  1238             (SOME (fn i1 => fn i2 => fn i3 =>

  1239                  kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2)))

  1240                             (KK.LE (KK.Num 0, KK.BitXor (i2, i3)))))

  1241             (SOME (curry KK.Add))

  1242       | Cst (Subtract, Type (_, [@{typ nat}, _]), _) =>

  1243         KK.Rel nat_subtract_rel

  1244       | Cst (Subtract, Type (_, [@{typ int}, _]), _) =>

  1245         KK.Rel int_subtract_rel

  1246       | Cst (Subtract, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>

  1247         to_bit_word_binary_op T R NONE

  1248             (SOME (fn i1 => fn i2 =>

  1249                       KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2))))

  1250       | Cst (Subtract, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>

  1251         to_bit_word_binary_op T R

  1252             (SOME (fn i1 => fn i2 => fn i3 =>

  1253                  kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0))

  1254                             (KK.LT (KK.BitXor (i2, i3), KK.Num 0))))

  1255             (SOME (curry KK.Sub))

  1256       | Cst (Multiply, Type (_, [@{typ nat}, _]), _) =>

  1257         KK.Rel nat_multiply_rel

  1258       | Cst (Multiply, Type (_, [@{typ int}, _]), _) =>

  1259         KK.Rel int_multiply_rel

  1260       | Cst (Multiply,

  1261              T as Type (_, [Type (@{type_name word}, [bit_T]), _]), R) =>

  1262         to_bit_word_binary_op T R

  1263             (SOME (fn i1 => fn i2 => fn i3 =>

  1264                 kk_or (KK.IntEq (i2, KK.Num 0))

  1265                       (KK.IntEq (KK.Div (i3, i2), i1)

  1266                        |> bit_T = @{typ signed_bit}

  1267                           ? kk_and (KK.LE (KK.Num 0,

  1268                                            foldl1 KK.BitAnd [i1, i2, i3])))))

  1269             (SOME (curry KK.Mult))

  1270       | Cst (Divide, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_divide_rel

  1271       | Cst (Divide, Type (_, [@{typ int}, _]), _) => KK.Rel int_divide_rel

  1272       | Cst (Divide, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>

  1273         to_bit_word_binary_op T R NONE

  1274             (SOME (fn i1 => fn i2 =>

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

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

  1277       | Cst (Divide, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>

  1278         to_bit_word_binary_op T R

  1279             (SOME (fn i1 => fn i2 => fn i3 =>

  1280                       KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3])))

  1281             (SOME (fn i1 => fn i2 =>

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

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

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

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

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

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

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

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

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

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

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

  1293       | Cst (Fracs, _, Func (Struct _, _)) =>

  1294         kk_project_seq (KK.Rel norm_frac_rel) 2 2

  1295       | Cst (NormFrac, _, _) => KK.Rel norm_frac_rel

  1296       | Cst (NatToInt, Type (_, [@{typ nat}, _]), Func (Atom _, Atom _)) =>

  1297         KK.Iden

  1298       | Cst (NatToInt, Type (_, [@{typ nat}, _]),

  1299              Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) =>

  1300         if nat_j0 = int_j0 then

  1301           kk_intersect KK.Iden

  1302               (kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0))

  1303                           KK.Univ)

  1304         else

  1305           raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")

  1306       | Cst (NatToInt, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>

  1307         to_bit_word_unary_op T R I

  1308       | Cst (IntToNat, Type (_, [@{typ int}, _]),

  1309              Func (Atom (int_k, int_j0), nat_R)) =>

  1310         let

  1311           val abs_card = max_int_for_card int_k + 1

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

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

  1314         in

  1315           if nat_j0 = int_j0 then

  1316             kk_union (kk_product (KK.AtomSeq (int_k - abs_card,

  1317                                               int_j0 + abs_card))

  1318                                  (KK.Atom nat_j0))

  1319                      (kk_intersect KK.Iden

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

  1321           else

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

  1323         end

  1324       | Cst (IntToNat, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>

  1325         to_bit_word_unary_op T R

  1326             (fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i))

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

  1328       | Op1 (Finite, _, Opt (Atom _), _) => KK.None

  1329       | Op1 (Converse, T, R, u1) =>

  1330         let

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

  1332           val (b_R, a_R) =

  1333             case R of

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

  1335             | Func (R1, _) =>

  1336               if card_of_rep R1 <> 1 then

  1337                 raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])

  1338               else

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

  1340             | _ => raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])

  1341           val body_R = body_rep R

  1342           val a_arity = arity_of_rep a_R

  1343           val b_arity = arity_of_rep b_R

  1344           val ab_arity = a_arity + b_arity

  1345           val body_arity = arity_of_rep body_R

  1346         in

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

  1348                      (map KK.Num (index_seq a_arity b_arity @

  1349                                   index_seq 0 a_arity @

  1350                                   index_seq ab_arity body_arity))

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

  1352         end

  1353       | Op1 (Closure, _, R, u1) =>

  1354         if is_opt_rep R then

  1355           let

  1356             val T1 = type_of u1

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

  1358             val R'' = opt_rep ofs T1 R'

  1359           in

  1360             single_rel_rel_let kk

  1361                 (fn r =>

  1362                     let

  1363                       val true_r = kk_closure (kk_join r true_atom)

  1364                       val full_r = full_rel_for_rep R'

  1365                       val false_r = kk_difference full_r

  1366                                         (kk_closure (kk_difference full_r

  1367                                                         (kk_join r false_atom)))

  1368                     in

  1369                       rel_expr_from_rel_expr kk R R''

  1370                           (kk_union (kk_product true_r true_atom)

  1371                                     (kk_product false_r false_atom))

  1372                     end) (to_rep R'' u1)

  1373           end

  1374         else

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

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

  1377           end

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

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

  1380       | Op1 (SingletonSet, _, R, u1) =>

  1381         (case R of

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

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

  1384          | Func (R1, Opt _) =>

  1385            single_rel_rel_let kk

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

  1387                             (rel_expr_to_func kk R1 bool_atom_R

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

  1389                (to_opt R1 u1)

  1390          | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u]))

  1391       | Op1 (SafeThe, _, R, u1) =>

  1392         if is_opt_rep R then

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

  1394         else

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

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

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

  1398       | Op1 (Cast, _, R, u1) =>

  1399         ((case rep_of u1 of

  1400             Formula _ =>

  1401             (case unopt_rep R of

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

  1403              | _ => raise SAME ())

  1404           | _ => raise SAME ())

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

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

  1407         to_r (Op1 (Not, T, R,

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

  1409       | Op2 (Exist, _, Opt _, u1, u2) =>

  1410         let val rs1 = untuple to_decl u1 in

  1411           if not (is_opt_rep (rep_of u2)) then

  1412             kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None

  1413           else

  1414             let val r2 = to_r u2 in

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

  1416                                   true_atom KK.None)

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

  1418                                   false_atom KK.None)

  1419             end

  1420         end

  1421       | Op2 (Or, _, _, u1, u2) =>

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

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

  1424       | Op2 (And, _, _, u1, u2) =>

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

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

  1427       | Op2 (Less, _, _, u1, u2) =>

  1428         (case type_of u1 of

  1429            @{typ nat} =>

  1430            if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom

  1431            else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom

  1432            else kk_nat_less (to_integer u1) (to_integer u2)

  1433          | @{typ int} => kk_int_less (to_integer u1) (to_integer u2)

  1434          | _ => double_rel_rel_let kk

  1435                     (fn r1 => fn r2 =>

  1436                         kk_rel_if

  1437                             (fold kk_and (map_filter (fn (u, r) =>

  1438                                  if is_opt_rep (rep_of u) then SOME (kk_some r)

  1439                                  else NONE) [(u1, r1), (u2, r2)]) KK.True)

  1440                             (atom_from_formula kk bool_j0 (KK.LT (pairself

  1441                                 (int_expr_from_atom kk (type_of u1)) (r1, r2))))

  1442                             KK.None)

  1443                     (to_r u1) (to_r u2))

  1444       | Op2 (The, _, R, u1, u2) =>

  1445         if is_opt_rep R then

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

  1447             kk_rel_if (kk_one (kk_join r1 true_atom)) (kk_join r1 true_atom)

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

  1449                                         (kk_subset (full_rel_for_rep R)

  1450                                                    (kk_join r1 false_atom)))

  1451                                  (to_rep R u2) (empty_rel_for_rep R))

  1452           end

  1453         else

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

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

  1456           end

  1457       | Op2 (Eps, _, R, u1, u2) =>

  1458         if is_opt_rep (rep_of u1) then

  1459           let

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

  1461             val r2 = to_rep R u2

  1462           in

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

  1464                                 (kk_join r1 true_atom) (empty_rel_for_rep R))

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

  1466                                        (kk_subset (full_rel_for_rep R)

  1467                                                   (kk_join r1 false_atom)))

  1468                                 r2 (empty_rel_for_rep R))

  1469           end

  1470         else

  1471           let

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

  1473             val r2 = to_rep R u2

  1474           in

  1475             kk_union (kk_rel_if (kk_one r1) r1 (empty_rel_for_rep R))

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

  1477                                 r2 (empty_rel_for_rep R))

  1478           end

  1479       | Op2 (Triad, _, Opt (Atom (2, j0)), u1, u2) =>

  1480         let

  1481           val f1 = to_f u1

  1482           val f2 = to_f u2

  1483         in

  1484           if f1 = f2 then

  1485             atom_from_formula kk j0 f1

  1486           else

  1487             kk_union (kk_rel_if f1 true_atom KK.None)

  1488                      (kk_rel_if f2 KK.None false_atom)

  1489         end

  1490       | Op2 (Union, _, R, u1, u2) =>

  1491         to_set_op kk_or kk_or3 kk_union kk_union kk_intersect false R u1 u2

  1492       | Op2 (SetDifference, _, R, u1, u2) =>

  1493         to_set_op kk_notimplies kk_notimplies3 kk_difference kk_intersect

  1494                   kk_union true R u1 u2

  1495       | Op2 (Intersect, _, R, u1, u2) =>

  1496         to_set_op kk_and kk_and3 kk_intersect kk_intersect kk_union false R

  1497                   u1 u2

  1498       | Op2 (Composition, _, R, u1, u2) =>

  1499         let

  1500           val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u1))

  1501           val (_, c_T) = HOLogic.dest_prodT (domain_type (type_of u2))

  1502           val ab_k = card_of_domain_from_rep 2 (rep_of u1)

  1503           val bc_k = card_of_domain_from_rep 2 (rep_of u2)

  1504           val ac_k = card_of_domain_from_rep 2 R

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

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

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

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

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

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

  1511           val body_R = body_rep R

  1512         in

  1513           (case body_R of

  1514              Formula Neut =>

  1515              kk_join (to_rep (Func (Struct [a_R, b_R], Formula Neut)) u1)

  1516                      (to_rep (Func (Struct [b_R, c_R], Formula Neut)) u2)

  1517            | Opt (Atom (2, _)) =>

  1518              let

  1519                (* FIXME: merge with similar code above *)

  1520                (* rep -> rep -> nut -> KK.rel_expr *)

  1521                fun must R1 R2 u =

  1522                  kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom

  1523                fun may R1 R2 u =

  1524                  kk_difference

  1525                      (full_rel_for_rep (Struct [R1, R2]))

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

  1527                               false_atom)

  1528              in

  1529                kk_union

  1530                    (kk_product (kk_join (must a_R b_R u1) (must b_R c_R u2))

  1531                                true_atom)

  1532                    (kk_product (kk_difference

  1533                                    (full_rel_for_rep (Struct [a_R, c_R]))

  1534                                    (kk_join (may a_R b_R u1) (may b_R c_R u2)))

  1535                                false_atom)

  1536              end

  1537            | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))

  1538           |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))

  1539         end

  1540       | Op2 (Product, T, R, u1, u2) =>

  1541         let

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

  1543           val a_k = card_of_domain_from_rep 2 (rep_of u1)

  1544           val b_k = card_of_domain_from_rep 2 (rep_of u2)

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

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

  1547           val body_R = body_rep R

  1548         in

  1549           (case body_R of

  1550              Formula Neut =>

  1551              kk_product (to_rep (Func (a_R, Formula Neut)) u1)

  1552                         (to_rep (Func (b_R, Formula Neut)) u2)

  1553            | Opt (Atom (2, _)) =>

  1554              let

  1555                (* KK.rel_expr -> rep -> nut -> KK.rel_expr *)

  1556                fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r

  1557                (* KK.rel_expr -> KK.rel_expr *)

  1558                fun do_term r =

  1559                  kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r

  1560              in kk_union (do_term true_atom) (do_term false_atom) end

  1561            | _ => raise NUT ("Nitpick_Kodkod.to_r (Product)", [u]))

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

  1563         end

  1564       | Op2 (Image, T, R, u1, u2) =>

  1565         (case (rep_of u1, rep_of u2) of

  1566            (Func (R11, R12), Func (R21, Formula Neut)) =>

  1567            if R21 = R11 andalso is_lone_rep R12 then

  1568              let

  1569                (* KK.rel_expr -> KK.rel_expr *)

  1570                fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1)

  1571                val core_r = big_join (to_r u2)

  1572                val core_R = Func (R12, Formula Neut)

  1573              in

  1574                if is_opt_rep R12 then

  1575                  let

  1576                    val schema = atom_schema_of_rep R21

  1577                    val decls = decls_for_atom_schema ~1 schema

  1578                    val vars = unary_var_seq ~1 (length decls)

  1579                    val f = kk_some (big_join (fold1 kk_product vars))

  1580                  in

  1581                    kk_rel_if (kk_all decls f)

  1582                              (rel_expr_from_rel_expr kk R core_R core_r)

  1583                              (rel_expr_from_rel_expr kk R (opt_rep ofs T core_R)

  1584                                               (kk_product core_r true_atom))

  1585                  end

  1586                else

  1587                  rel_expr_from_rel_expr kk R core_R core_r

  1588              end

  1589            else

  1590              raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])

  1591          | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]))

  1592       | Op2 (Apply, @{typ nat}, _,

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

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

  1595           KK.Atom (offset_of_type ofs nat_T)

  1596         else

  1597           fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel)

  1598       | Op2 (Apply, _, R, u1, u2) => to_apply R u1 u2

  1599       | Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) =>

  1600         to_guard [u1, u2] R (KK.Atom j0)

  1601       | Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) =>

  1602         kk_comprehension (untuple to_decl u1) (to_f u2)

  1603       | Op2 (Lambda, _, Func (_, R2), u1, u2) =>

  1604         let

  1605           val dom_decls = untuple to_decl u1

  1606           val ran_schema = atom_schema_of_rep R2

  1607           val ran_decls = decls_for_atom_schema ~1 ran_schema

  1608           val ran_vars = unary_var_seq ~1 (length ran_decls)

  1609         in

  1610           kk_comprehension (dom_decls @ ran_decls)

  1611                            (kk_subset (fold1 kk_product ran_vars)

  1612                                       (to_rep R2 u2))

  1613         end

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

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

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

  1617         if is_opt_rep (rep_of u1) then

  1618           triple_rel_rel_let kk

  1619               (fn r1 => fn r2 => fn r3 =>

  1620                   let val empty_r = empty_rel_for_rep R in

  1621                     fold1 kk_union

  1622                           [kk_rel_if (kk_rel_eq r1 true_atom) r2 empty_r,

  1623                            kk_rel_if (kk_rel_eq r1 false_atom) r3 empty_r,

  1624                            kk_rel_if (kk_rel_eq r2 r3)

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

  1626                   end)

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

  1628         else

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

  1630       | Tuple (_, R, us) =>

  1631         (case unopt_rep R of

  1632            Struct Rs => to_product Rs us

  1633          | Vect (k, R) => to_product (replicate k R) us

  1634          | Atom (1, j0) =>

  1635            (case filter (not_equal Unit o rep_of) us of

  1636               [] => KK.Atom j0

  1637             | us' => kk_rel_if (kk_some (fold1 kk_product (map to_r us')))

  1638                                (KK.Atom j0) KK.None)

  1639          | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))

  1640       | Construct ([u'], _, _, []) => to_r u'

  1641       | Construct (discr_u :: sel_us, _, _, arg_us) =>

  1642         let

  1643           val set_rs =

  1644             map2 (fn sel_u => fn arg_u =>

  1645                      let

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

  1647                        val sel_r = to_r sel_u

  1648                        val arg_r = to_opt R2 arg_u

  1649                      in

  1650                        if is_one_rep R2 then

  1651                          kk_n_fold_join kk true R2 R1 arg_r

  1652                               (kk_project sel_r (flip_nums (arity_of_rep R2)))

  1653                        else

  1654                          kk_comprehension [KK.DeclOne ((1, ~1), to_r discr_u)]

  1655                              (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r)

  1656                          |> is_opt_rep (rep_of arg_u) ? to_guard [arg_u] R1

  1657                      end) sel_us arg_us

  1658         in fold1 kk_intersect set_rs end

  1659       | BoundRel (x, _, _, _) => KK.Var x

  1660       | FreeRel (x, _, _, _) => KK.Rel x

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

  1662       | u => raise NUT ("Nitpick_Kodkod.to_r", [u])

  1663     (* nut -> KK.decl *)

  1664     and to_decl (BoundRel (x, _, R, _)) =

  1665         KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R)))

  1666       | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])

  1667     (* nut -> KK.expr_assign *)

  1668     and to_expr_assign (FormulaReg (j, _, _)) u =

  1669         KK.AssignFormulaReg (j, to_f u)

  1670       | to_expr_assign (RelReg (j, _, R)) u =

  1671         KK.AssignRelReg ((arity_of_rep R, j), to_r u)

  1672       | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])

  1673     (* int * int -> nut -> KK.rel_expr *)

  1674     and to_atom (x as (k, j0)) u =

  1675       case rep_of u of

  1676         Formula _ => atom_from_formula kk j0 (to_f u)

  1677       | Unit => if k = 1 then KK.Atom j0

  1678                 else raise NUT ("Nitpick_Kodkod.to_atom", [u])

  1679       | R => atom_from_rel_expr kk x R (to_r u)

  1680     (* rep list -> nut -> KK.rel_expr *)

  1681     and to_struct Rs u =

  1682       case rep_of u of

  1683         Unit => full_rel_for_rep (Struct Rs)

  1684       | R' => struct_from_rel_expr kk Rs R' (to_r u)

  1685     (* int -> rep -> nut -> KK.rel_expr *)

  1686     and to_vect k R u =

  1687       case rep_of u of

  1688         Unit => full_rel_for_rep (Vect (k, R))

  1689       | R' => vect_from_rel_expr kk k R R' (to_r u)

  1690     (* rep -> rep -> nut -> KK.rel_expr *)

  1691     and to_func R1 R2 u =

  1692       case rep_of u of

  1693         Unit => full_rel_for_rep (Func (R1, R2))

  1694       | R' => rel_expr_to_func kk R1 R2 R' (to_r u)

  1695     (* rep -> nut -> KK.rel_expr *)

  1696     and to_opt R u =

  1697       let val old_R = rep_of u in

  1698         if is_opt_rep old_R then

  1699           rel_expr_from_rel_expr kk (Opt R) old_R (to_r u)

  1700         else

  1701           to_rep R u

  1702       end

  1703     (* rep -> nut -> KK.rel_expr *)

  1704     and to_rep (Atom x) u = to_atom x u

  1705       | to_rep (Struct Rs) u = to_struct Rs u

  1706       | to_rep (Vect (k, R)) u = to_vect k R u

  1707       | to_rep (Func (R1, R2)) u = to_func R1 R2 u

  1708       | to_rep (Opt R) u = to_opt R u

  1709       | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R])

  1710     (* nut -> KK.rel_expr *)

  1711     and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u

  1712     (* nut list -> rep -> KK.rel_expr -> KK.rel_expr *)

  1713     and to_guard guard_us R r =

  1714       let

  1715         val unpacked_rs = unpack_joins r

  1716         val plain_guard_rs =

  1717           map to_r (filter (is_Opt o rep_of) guard_us)

  1718           |> filter_out (member (op =) unpacked_rs)

  1719         val func_guard_us =

  1720           filter ((is_Func andf is_opt_rep) o rep_of) guard_us

  1721         val func_guard_rs = map to_r func_guard_us

  1722         val guard_fs =

  1723           map kk_no plain_guard_rs @

  1724           map2 (kk_not oo kk_n_ary_function kk)

  1725                (map (unopt_rep o rep_of) func_guard_us) func_guard_rs

  1726       in

  1727         if null guard_fs then r

  1728         else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r

  1729       end

  1730     (* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *)

  1731     and to_project new_R old_R r j0 =

  1732       rel_expr_from_rel_expr kk new_R old_R

  1733                              (kk_project_seq r j0 (arity_of_rep old_R))

  1734     (* rep list -> nut list -> KK.rel_expr *)

  1735     and to_product Rs us =

  1736       case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of

  1737         [] => raise REP ("Nitpick_Kodkod.to_product", Rs)

  1738       | rs => fold1 kk_product rs

  1739     (* int -> typ -> rep -> nut -> KK.rel_expr *)

  1740     and to_nth_pair_sel n res_T res_R u =

  1741       case u of

  1742         Tuple (_, _, us) => to_rep res_R (nth us n)

  1743       | _ => let

  1744                val R = rep_of u

  1745                val (a_T, b_T) = HOLogic.dest_prodT (type_of u)

  1746                val Rs =

  1747                  case unopt_rep R of

  1748                    Struct (Rs as [_, _]) => Rs

  1749                  | _ =>

  1750                    let

  1751                      val res_card = card_of_rep res_R

  1752                      val other_card = card_of_rep R div res_card

  1753                      val (a_card, b_card) = (res_card, other_card)

  1754                                             |> n = 1 ? swap

  1755                    in

  1756                      [Atom (a_card, offset_of_type ofs a_T),

  1757                       Atom (b_card, offset_of_type ofs b_T)]

  1758                    end

  1759                val nth_R = nth Rs n

  1760                val j0 = if n = 0 then 0 else arity_of_rep (hd Rs)

  1761              in

  1762                case arity_of_rep nth_R of

  1763                  0 => to_guard [u] res_R

  1764                                (to_rep res_R (Cst (Unity, res_T, Unit)))

  1765                | _ => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0

  1766              end

  1767     (* (KK.formula -> KK.formula -> KK.formula)

  1768        -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> nut -> nut

  1769        -> KK.formula *)

  1770     and to_set_bool_op connective set_oper u1 u2 =

  1771       let

  1772         val min_R = min_rep (rep_of u1) (rep_of u2)

  1773         val r1 = to_rep min_R u1

  1774         val r2 = to_rep min_R u2

  1775       in

  1776         case min_R of

  1777           Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2

  1778         | Func (_, Formula Neut) => set_oper r1 r2

  1779         | Func (Unit, Atom (2, j0)) =>

  1780           connective (formula_from_atom j0 r1) (formula_from_atom j0 r2)

  1781         | Func (_, Atom _) => set_oper (kk_join r1 true_atom)

  1782                                        (kk_join r2 true_atom)

  1783         | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])

  1784       end

  1785     (* (KK.formula -> KK.formula -> KK.formula)

  1786        -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr)

  1787        -> (KK.rel_expr -> KK.rel_expr -> KK.formula)

  1788        -> (KK.rel_expr -> KK.rel_expr -> KK.formula)

  1789        -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> bool -> rep -> nut

  1790        -> nut -> KK.rel_expr *)

  1791     and to_set_op connective connective3 set_oper true_set_oper false_set_oper

  1792                   neg_second R u1 u2 =

  1793       let

  1794         val min_R = min_rep (rep_of u1) (rep_of u2)

  1795         val r1 = to_rep min_R u1

  1796         val r2 = to_rep min_R u2

  1797         val unopt_R = unopt_rep R

  1798       in

  1799         rel_expr_from_rel_expr kk unopt_R (unopt_rep min_R)

  1800             (case min_R of

  1801                Opt (Vect (k, Atom _)) => kk_vect_set_op connective k r1 r2

  1802              | Vect (k, Atom _) => kk_vect_set_op connective k r1 r2

  1803              | Func (_, Formula Neut) => set_oper r1 r2

  1804              | Func (Unit, _) => connective3 r1 r2

  1805              | Func _ =>

  1806                double_rel_rel_let kk

  1807                    (fn r1 => fn r2 =>

  1808                        kk_union

  1809                            (kk_product

  1810                                 (true_set_oper (kk_join r1 true_atom)

  1811                                      (kk_join r2 (atom_for_bool bool_j0

  1812                                                              (not neg_second))))

  1813                                 true_atom)

  1814                            (kk_product

  1815                                 (false_set_oper (kk_join r1 false_atom)

  1816                                      (kk_join r2 (atom_for_bool bool_j0

  1817                                                                 neg_second)))

  1818                                 false_atom))

  1819                    r1 r2

  1820              | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))

  1821       end

  1822     (* typ -> rep -> (KK.int_expr -> KK.int_expr) -> KK.rel_expr *)

  1823     and to_bit_word_unary_op T R oper =

  1824       let

  1825         val Ts = strip_type T ||> single |> op @

  1826         (* int -> KK.int_expr *)

  1827         fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))

  1828       in

  1829         kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))

  1830             (KK.FormulaLet

  1831                  (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 1),

  1832                   KK.IntEq (KK.IntReg 1, oper (KK.IntReg 0))))

  1833       end

  1834     (* typ -> rep -> (KK.int_expr -> KK.int_expr -> KK.int_expr -> bool) option

  1835        -> (KK.int_expr -> KK.int_expr -> KK.int_expr) option -> KK.rel_expr *)

  1836     and to_bit_word_binary_op T R opt_guard opt_oper =

  1837       let

  1838         val Ts = strip_type T ||> single |> op @

  1839         (* int -> KK.int_expr *)

  1840         fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))

  1841       in

  1842         kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))

  1843             (KK.FormulaLet

  1844                  (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 2),

  1845                   fold1 kk_and

  1846                         ((case opt_guard of

  1847                             NONE => []

  1848                           | SOME guard =>

  1849                             [guard (KK.IntReg 0) (KK.IntReg 1) (KK.IntReg 2)]) @

  1850                          (case opt_oper of

  1851                             NONE => []

  1852                           | SOME oper =>

  1853                             [KK.IntEq (KK.IntReg 2,

  1854                                        oper (KK.IntReg 0) (KK.IntReg 1))]))))

  1855       end

  1856     (* rep -> rep -> KK.rel_expr -> nut -> KK.rel_expr *)

  1857     and to_apply res_R func_u arg_u =

  1858       case unopt_rep (rep_of func_u) of

  1859         Unit =>

  1860         let val j0 = offset_of_type ofs (type_of func_u) in

  1861           to_guard [arg_u] res_R

  1862                    (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0))

  1863         end

  1864       | Atom (1, j0) =>

  1865         to_guard [arg_u] res_R

  1866                  (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u))

  1867       | Atom (k, _) =>

  1868         let

  1869           val dom_card = card_of_rep (rep_of arg_u)

  1870           val ran_R = Atom (exact_root dom_card k,

  1871                             offset_of_type ofs (range_type (type_of func_u)))

  1872         in

  1873           to_apply_vect dom_card ran_R res_R (to_vect dom_card ran_R func_u)

  1874                         arg_u

  1875         end

  1876       | Vect (1, R') =>

  1877         to_guard [arg_u] res_R

  1878                  (rel_expr_from_rel_expr kk res_R R' (to_r func_u))

  1879       | Vect (k, R') => to_apply_vect k R' res_R (to_r func_u) arg_u

  1880       | Func (R, Formula Neut) =>

  1881         to_guard [arg_u] res_R (rel_expr_from_formula kk res_R

  1882                                     (kk_subset (to_opt R arg_u) (to_r func_u)))

  1883       | Func (Unit, R2) =>

  1884         to_guard [arg_u] res_R

  1885                  (rel_expr_from_rel_expr kk res_R R2 (to_r func_u))

  1886       | Func (R1, R2) =>

  1887         rel_expr_from_rel_expr kk res_R R2

  1888             (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))

  1889         |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R

  1890       | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])

  1891     (* int -> rep -> rep -> KK.rel_expr -> nut *)

  1892     and to_apply_vect k R' res_R func_r arg_u =

  1893       let

  1894         val arg_R = one_rep ofs (type_of arg_u) (unopt_rep (rep_of arg_u))

  1895         val vect_r = vect_from_rel_expr kk k res_R (Vect (k, R')) func_r

  1896         val vect_rs = unpack_vect_in_chunks kk (arity_of_rep res_R) k vect_r

  1897       in

  1898         kk_case_switch kk arg_R res_R (to_opt arg_R arg_u)

  1899                        (all_singletons_for_rep arg_R) vect_rs

  1900       end

  1901     (* bool -> nut -> KK.formula *)

  1902     and to_could_be_unrep neg u =

  1903       if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u) else KK.False

  1904     (* nut -> KK.rel_expr -> KK.rel_expr *)

  1905     and to_compare_with_unrep u r =

  1906       if is_opt_rep (rep_of u) then

  1907         kk_rel_if (kk_some (to_r u)) r (empty_rel_for_rep (rep_of u))

  1908       else

  1909         r

  1910   in to_f_with_polarity Pos u end

  1912 end;

author	blanchet
	Wed, 10 Mar 2010 14:21:01 +0100
changeset 35695	80b2c22f8f00
parent 35666	ed2c3830d881
child 36127	e91292c520be
permissions	-rw-r--r--