src/HOL/Tools/Nitpick/nitpick_peephole.ML
author blanchet
Fri Dec 18 12:00:29 2009 +0100 (2009-12-18)
changeset 34126 8a2c5d7aff51
parent 34124 c4628a1dcf75
child 34936 c4f04bee79f3
permissions -rw-r--r--
polished Nitpick's binary integer support etc.;
etc. = improve inconsistent scope correction + sort values nicely in output
+ handle "mod" using the characterization "x mod y = x - x div y * y"
(instead of explicit code in Nitpick)
+ introduce KK = Kodkod as abbreviation
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_peephole.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009
     4 
     5 Peephole optimizer for Nitpick.
     6 *)
     7 
     8 signature NITPICK_PEEPHOLE =
     9 sig
    10   type n_ary_index = Kodkod.n_ary_index
    11   type formula = Kodkod.formula
    12   type int_expr = Kodkod.int_expr
    13   type rel_expr = Kodkod.rel_expr
    14   type decl = Kodkod.decl
    15   type expr_assign = Kodkod.expr_assign
    16 
    17   type name_pool = {
    18     rels: n_ary_index list,
    19     vars: n_ary_index list,
    20     formula_reg: int,
    21     rel_reg: int}
    22 
    23   val initial_pool : name_pool
    24   val not3_rel : n_ary_index
    25   val suc_rel : n_ary_index
    26   val unsigned_bit_word_sel_rel : n_ary_index
    27   val signed_bit_word_sel_rel : n_ary_index
    28   val nat_add_rel : n_ary_index
    29   val int_add_rel : n_ary_index
    30   val nat_subtract_rel : n_ary_index
    31   val int_subtract_rel : n_ary_index
    32   val nat_multiply_rel : n_ary_index
    33   val int_multiply_rel : n_ary_index
    34   val nat_divide_rel : n_ary_index
    35   val int_divide_rel : n_ary_index
    36   val nat_less_rel : n_ary_index
    37   val int_less_rel : n_ary_index
    38   val gcd_rel : n_ary_index
    39   val lcm_rel : n_ary_index
    40   val norm_frac_rel : n_ary_index
    41   val atom_for_bool : int -> bool -> rel_expr
    42   val formula_for_bool : bool -> formula
    43   val atom_for_nat : int * int -> int -> int
    44   val min_int_for_card : int -> int
    45   val max_int_for_card : int -> int
    46   val int_for_atom : int * int -> int -> int
    47   val atom_for_int : int * int -> int -> int
    48   val is_twos_complement_representable : int -> int -> bool
    49   val inline_rel_expr : rel_expr -> bool
    50   val empty_n_ary_rel : int -> rel_expr
    51   val num_seq : int -> int -> int_expr list
    52   val s_and : formula -> formula -> formula
    53 
    54   type kodkod_constrs = {
    55     kk_all: decl list -> formula -> formula,
    56     kk_exist: decl list -> formula -> formula,
    57     kk_formula_let: expr_assign list -> formula -> formula,
    58     kk_formula_if: formula -> formula -> formula -> formula,
    59     kk_or: formula -> formula -> formula,
    60     kk_not: formula -> formula,
    61     kk_iff: formula -> formula -> formula,
    62     kk_implies: formula -> formula -> formula,
    63     kk_and: formula -> formula -> formula,
    64     kk_subset: rel_expr -> rel_expr -> formula,
    65     kk_rel_eq: rel_expr -> rel_expr -> formula,
    66     kk_no: rel_expr -> formula,
    67     kk_lone: rel_expr -> formula,
    68     kk_one: rel_expr -> formula,
    69     kk_some: rel_expr -> formula,
    70     kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
    71     kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
    72     kk_union: rel_expr -> rel_expr -> rel_expr,
    73     kk_difference: rel_expr -> rel_expr -> rel_expr,
    74     kk_override: rel_expr -> rel_expr -> rel_expr,
    75     kk_intersect: rel_expr -> rel_expr -> rel_expr,
    76     kk_product: rel_expr -> rel_expr -> rel_expr,
    77     kk_join: rel_expr -> rel_expr -> rel_expr,
    78     kk_closure: rel_expr -> rel_expr,
    79     kk_reflexive_closure: rel_expr -> rel_expr,
    80     kk_comprehension: decl list -> formula -> rel_expr,
    81     kk_project: rel_expr -> int_expr list -> rel_expr,
    82     kk_project_seq: rel_expr -> int -> int -> rel_expr,
    83     kk_not3: rel_expr -> rel_expr,
    84     kk_nat_less: rel_expr -> rel_expr -> rel_expr,
    85     kk_int_less: rel_expr -> rel_expr -> rel_expr
    86   }
    87 
    88   val kodkod_constrs : bool -> int -> int -> int -> kodkod_constrs
    89 end;
    90 
    91 structure Nitpick_Peephole : NITPICK_PEEPHOLE =
    92 struct
    93 
    94 open Kodkod
    95 open Nitpick_Util
    96 
    97 type name_pool = {
    98   rels: n_ary_index list,
    99   vars: n_ary_index list,
   100   formula_reg: int,
   101   rel_reg: int}
   102 
   103 (* If you add new built-in relations, make sure to increment the counters here
   104    as well to avoid name clashes (which fortunately would be detected by
   105    Kodkodi). *)
   106 val initial_pool =
   107   {rels = [(2, 10), (3, 20), (4, 10)], vars = [], formula_reg = 10,
   108    rel_reg = 10}
   109 
   110 val not3_rel = (2, 0)
   111 val suc_rel = (2, 1)
   112 val unsigned_bit_word_sel_rel = (2, 2)
   113 val signed_bit_word_sel_rel = (2, 3)
   114 val nat_add_rel = (3, 0)
   115 val int_add_rel = (3, 1)
   116 val nat_subtract_rel = (3, 2)
   117 val int_subtract_rel = (3, 3)
   118 val nat_multiply_rel = (3, 4)
   119 val int_multiply_rel = (3, 5)
   120 val nat_divide_rel = (3, 6)
   121 val int_divide_rel = (3, 7)
   122 val nat_less_rel = (3, 8)
   123 val int_less_rel = (3, 9)
   124 val gcd_rel = (3, 10)
   125 val lcm_rel = (3, 11)
   126 val norm_frac_rel = (4, 0)
   127 
   128 (* int -> bool -> rel_expr *)
   129 fun atom_for_bool j0 = Atom o Integer.add j0 o int_for_bool
   130 (* bool -> formula *)
   131 fun formula_for_bool b = if b then True else False
   132 
   133 (* int * int -> int -> int *)
   134 fun atom_for_nat (k, j0) n = if n < 0 orelse n >= k then ~1 else n + j0
   135 (* int -> int *)
   136 fun min_int_for_card k = ~k div 2 + 1
   137 fun max_int_for_card k = k div 2
   138 (* int * int -> int -> int *)
   139 fun int_for_atom (k, j0) j =
   140   let val j = j - j0 in if j <= max_int_for_card k then j else j - k end
   141 fun atom_for_int (k, j0) n =
   142   if n < min_int_for_card k orelse n > max_int_for_card k then ~1
   143   else if n < 0 then n + k + j0
   144   else n + j0
   145 (* int -> int -> bool *)
   146 fun is_twos_complement_representable bits n =
   147   let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
   148 
   149 (* rel_expr -> bool *)
   150 fun is_none_product (Product (r1, r2)) =
   151     is_none_product r1 orelse is_none_product r2
   152   | is_none_product None = true
   153   | is_none_product _ = false
   154 
   155 (* rel_expr -> bool *)
   156 fun is_one_rel_expr (Atom _) = true
   157   | is_one_rel_expr (AtomSeq (1, _)) = true
   158   | is_one_rel_expr (Var _) = true
   159   | is_one_rel_expr _ = false
   160 
   161 (* rel_expr -> bool *)
   162 fun inline_rel_expr (Product (r1, r2)) =
   163     inline_rel_expr r1 andalso inline_rel_expr r2
   164   | inline_rel_expr Iden = true
   165   | inline_rel_expr Ints = true
   166   | inline_rel_expr None = true
   167   | inline_rel_expr Univ = true
   168   | inline_rel_expr (Atom _) = true
   169   | inline_rel_expr (AtomSeq _) = true
   170   | inline_rel_expr (Rel _) = true
   171   | inline_rel_expr (Var _) = true
   172   | inline_rel_expr (RelReg _) = true
   173   | inline_rel_expr _ = false
   174 
   175 (* rel_expr -> rel_expr -> bool option *)
   176 fun rel_expr_equal None (Atom _) = SOME false
   177   | rel_expr_equal None (AtomSeq (k, _)) = SOME (k = 0)
   178   | rel_expr_equal (Atom _) None = SOME false
   179   | rel_expr_equal (AtomSeq (k, _)) None = SOME (k = 0)
   180   | rel_expr_equal (Atom j1) (Atom j2) = SOME (j1 = j2)
   181   | rel_expr_equal (Atom j) (AtomSeq (k, j0)) = SOME (j = j0 andalso k = 1)
   182   | rel_expr_equal (AtomSeq (k, j0)) (Atom j) = SOME (j = j0 andalso k = 1)
   183   | rel_expr_equal (AtomSeq x1) (AtomSeq x2) = SOME (x1 = x2)
   184   | rel_expr_equal r1 r2 = if r1 = r2 then SOME true else NONE
   185 
   186 (* rel_expr -> rel_expr -> bool option *)
   187 fun rel_expr_intersects (Atom j1) (Atom j2) = SOME (j1 = j2)
   188   | rel_expr_intersects (Atom j) (AtomSeq (k, j0)) = SOME (j < j0 + k)
   189   | rel_expr_intersects (AtomSeq (k, j0)) (Atom j) = SOME (j < j0 + k)
   190   | rel_expr_intersects (AtomSeq (k1, j01)) (AtomSeq (k2, j02)) =
   191     SOME (k1 > 0 andalso k2 > 0 andalso j01 + k1 > j02 andalso j02 + k2 > j01)
   192   | rel_expr_intersects r1 r2 =
   193     if is_none_product r1 orelse is_none_product r2 then SOME false else NONE
   194 
   195 (* int -> rel_expr *)
   196 fun empty_n_ary_rel 0 = raise ARG ("Nitpick_Peephole.empty_n_ary_rel", "0")
   197   | empty_n_ary_rel n = funpow (n - 1) (curry Product None) None
   198 
   199 (* decl -> rel_expr *)
   200 fun decl_one_set (DeclOne (_, r)) = r
   201   | decl_one_set _ =
   202     raise ARG ("Nitpick_Peephole.decl_one_set", "not \"DeclOne\"")
   203 
   204 (* int_expr -> bool *)
   205 fun is_Num (Num _) = true
   206   | is_Num _ = false
   207 (* int_expr -> int *)
   208 fun dest_Num (Num k) = k
   209   | dest_Num _ = raise ARG ("Nitpick_Peephole.dest_Num", "not \"Num\"")
   210 (* int -> int -> int_expr list *)
   211 fun num_seq j0 n = map Num (index_seq j0 n)
   212 
   213 (* rel_expr -> rel_expr -> bool *)
   214 fun occurs_in_union r (Union (r1, r2)) =
   215     occurs_in_union r r1 orelse occurs_in_union r r2
   216   | occurs_in_union r r' = (r = r')
   217 
   218 (* rel_expr -> rel_expr -> rel_expr *)
   219 fun s_and True f2 = f2
   220   | s_and False _ = False
   221   | s_and f1 True = f1
   222   | s_and _ False = False
   223   | s_and f1 f2 = And (f1, f2)
   224 
   225 type kodkod_constrs = {
   226   kk_all: decl list -> formula -> formula,
   227   kk_exist: decl list -> formula -> formula,
   228   kk_formula_let: expr_assign list -> formula -> formula,
   229   kk_formula_if: formula -> formula -> formula -> formula,
   230   kk_or: formula -> formula -> formula,
   231   kk_not: formula -> formula,
   232   kk_iff: formula -> formula -> formula,
   233   kk_implies: formula -> formula -> formula,
   234   kk_and: formula -> formula -> formula,
   235   kk_subset: rel_expr -> rel_expr -> formula,
   236   kk_rel_eq: rel_expr -> rel_expr -> formula,
   237   kk_no: rel_expr -> formula,
   238   kk_lone: rel_expr -> formula,
   239   kk_one: rel_expr -> formula,
   240   kk_some: rel_expr -> formula,
   241   kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
   242   kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
   243   kk_union: rel_expr -> rel_expr -> rel_expr,
   244   kk_difference: rel_expr -> rel_expr -> rel_expr,
   245   kk_override: rel_expr -> rel_expr -> rel_expr,
   246   kk_intersect: rel_expr -> rel_expr -> rel_expr,
   247   kk_product: rel_expr -> rel_expr -> rel_expr,
   248   kk_join: rel_expr -> rel_expr -> rel_expr,
   249   kk_closure: rel_expr -> rel_expr,
   250   kk_reflexive_closure: rel_expr -> rel_expr,
   251   kk_comprehension: decl list -> formula -> rel_expr,
   252   kk_project: rel_expr -> int_expr list -> rel_expr,
   253   kk_project_seq: rel_expr -> int -> int -> rel_expr,
   254   kk_not3: rel_expr -> rel_expr,
   255   kk_nat_less: rel_expr -> rel_expr -> rel_expr,
   256   kk_int_less: rel_expr -> rel_expr -> rel_expr
   257 }
   258 
   259 (* We assume throughout that Kodkod variables have a "one" constraint. This is
   260    always the case if Kodkod's skolemization is disabled. *)
   261 (* bool -> int -> int -> int -> kodkod_constrs *)
   262 fun kodkod_constrs optim nat_card int_card main_j0 =
   263   let
   264     val false_atom = Atom main_j0
   265     val true_atom = Atom (main_j0 + 1)
   266 
   267     (* bool -> int *)
   268     val from_bool = atom_for_bool main_j0
   269     (* int -> rel_expr *)
   270     fun from_nat n = Atom (n + main_j0)
   271     val from_int = Atom o atom_for_int (int_card, main_j0)
   272     (* int -> int *)
   273     fun to_nat j = j - main_j0
   274     val to_int = int_for_atom (int_card, main_j0)
   275 
   276     (* decl list -> formula -> formula *)
   277     fun s_all _ True = True
   278       | s_all _ False = False
   279       | s_all [] f = f
   280       | s_all ds (All (ds', f)) = All (ds @ ds', f)
   281       | s_all ds f = All (ds, f)
   282     fun s_exist _ True = True
   283       | s_exist _ False = False
   284       | s_exist [] f = f
   285       | s_exist ds (Exist (ds', f)) = Exist (ds @ ds', f)
   286       | s_exist ds f = Exist (ds, f)
   287 
   288     (* expr_assign list -> formula -> formula *)
   289     fun s_formula_let _ True = True
   290       | s_formula_let _ False = False
   291       | s_formula_let assigns f = FormulaLet (assigns, f)
   292 
   293     (* formula -> formula *)
   294     fun s_not True = False
   295       | s_not False = True
   296       | s_not (All (ds, f)) = Exist (ds, s_not f)
   297       | s_not (Exist (ds, f)) = All (ds, s_not f)
   298       | s_not (Or (f1, f2)) = And (s_not f1, s_not f2)
   299       | s_not (Implies (f1, f2)) = And (f1, s_not f2)
   300       | s_not (And (f1, f2)) = Or (s_not f1, s_not f2)
   301       | s_not (Not f) = f
   302       | s_not (No r) = Some r
   303       | s_not (Some r) = No r
   304       | s_not f = Not f
   305 
   306     (* formula -> formula -> formula *)
   307     fun s_or True _ = True
   308       | s_or False f2 = f2
   309       | s_or _ True = True
   310       | s_or f1 False = f1
   311       | s_or f1 f2 = if f1 = f2 then f1 else Or (f1, f2)
   312     fun s_iff True f2 = f2
   313       | s_iff False f2 = s_not f2
   314       | s_iff f1 True = f1
   315       | s_iff f1 False = s_not f1
   316       | s_iff f1 f2 = if f1 = f2 then True else Iff (f1, f2)
   317     fun s_implies True f2 = f2
   318       | s_implies False _ = True
   319       | s_implies _ True = True
   320       | s_implies f1 False = s_not f1
   321       | s_implies f1 f2 = if f1 = f2 then True else Implies (f1, f2)
   322 
   323     (* formula -> formula -> formula -> formula *)
   324     fun s_formula_if True f2 _ = f2
   325       | s_formula_if False _ f3 = f3
   326       | s_formula_if f1 True f3 = s_or f1 f3
   327       | s_formula_if f1 False f3 = s_and (s_not f1) f3
   328       | s_formula_if f1 f2 True = s_implies f1 f2
   329       | s_formula_if f1 f2 False = s_and f1 f2
   330       | s_formula_if f f1 f2 = FormulaIf (f, f1, f2)
   331 
   332     (* rel_expr -> int_expr list -> rel_expr *)
   333     fun s_project r is =
   334       (case r of
   335          Project (r1, is') =>
   336          if forall is_Num is then
   337            s_project r1 (map (nth is' o dest_Num) is)
   338          else
   339            raise SAME ()
   340        | _ => raise SAME ())
   341       handle SAME () =>
   342              let val n = length is in
   343                if arity_of_rel_expr r = n andalso is = num_seq 0 n then r
   344                else Project (r, is)
   345              end
   346 
   347     (* rel_expr -> formula *)
   348     fun s_no None = True
   349       | s_no (Product (r1, r2)) = s_or (s_no r1) (s_no r2)
   350       | s_no (Intersect (Closure (Rel x), Iden)) = Acyclic x
   351       | s_no r = if is_one_rel_expr r then False else No r
   352     fun s_lone None = True
   353       | s_lone r = if is_one_rel_expr r then True else Lone r
   354     fun s_one None = False
   355       | s_one r =
   356         if is_one_rel_expr r then
   357           True
   358         else if inline_rel_expr r then
   359           case arity_of_rel_expr r of
   360             1 => One r
   361           | arity => foldl1 And (map (One o s_project r o single o Num)
   362                                      (index_seq 0 arity))
   363         else
   364           One r
   365     fun s_some None = False
   366       | s_some (Atom _) = True
   367       | s_some (Product (r1, r2)) = s_and (s_some r1) (s_some r2)
   368       | s_some r = if is_one_rel_expr r then True else Some r
   369 
   370     (* rel_expr -> rel_expr *)
   371     fun s_not3 (Atom j) = Atom (if j = main_j0 then j + 1 else j - 1)
   372       | s_not3 (r as Join (r1, r2)) =
   373         if r2 = Rel not3_rel then r1 else Join (r, Rel not3_rel)
   374       | s_not3 r = Join (r, Rel not3_rel)
   375 
   376     (* rel_expr -> rel_expr -> formula *)
   377     fun s_rel_eq r1 r2 =
   378       (case (r1, r2) of
   379          (Join (r11, Rel x), _) =>
   380          if x = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME ()
   381        | (_, Join (r21, Rel x)) =>
   382          if x = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME ()
   383        | (RelIf (f, r11, r12), _) =>
   384          if inline_rel_expr r2 then
   385            s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)
   386          else
   387            raise SAME ()
   388        | (_, RelIf (f, r21, r22)) =>
   389          if inline_rel_expr r1 then
   390            s_formula_if f (s_rel_eq r1 r21) (s_rel_eq r1 r22)
   391          else
   392            raise SAME ()
   393        | (RelLet (bs, r1'), Atom _) => s_formula_let bs (s_rel_eq r1' r2)
   394        | (Atom _, RelLet (bs, r2')) => s_formula_let bs (s_rel_eq r1 r2')
   395        | _ => raise SAME ())
   396       handle SAME () =>
   397              case rel_expr_equal r1 r2 of
   398                SOME true => True
   399              | SOME false => False
   400              | NONE =>
   401                case (r1, r2) of
   402                  (_, RelIf (f, r21, r22)) =>
   403                   if inline_rel_expr r1 then
   404                     s_formula_if f (s_rel_eq r1 r21) (s_rel_eq r1 r22)
   405                   else
   406                     RelEq (r1, r2)
   407                | (RelIf (f, r11, r12), _) =>
   408                   if inline_rel_expr r2 then
   409                     s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)
   410                   else
   411                     RelEq (r1, r2)
   412                | (_, None) => s_no r1
   413                | (None, _) => s_no r2
   414                | _ => RelEq (r1, r2)
   415     fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2)
   416       | s_subset (Atom j) (AtomSeq (k, j0)) =
   417         formula_for_bool (j >= j0 andalso j < j0 + k)
   418       | s_subset (r1 as Union (r11, r12)) r2 =
   419         s_and (s_subset r11 r2) (s_subset r12 r2)
   420       | s_subset r1 (r2 as Union (r21, r22)) =
   421         if is_one_rel_expr r1 then
   422           s_or (s_subset r1 r21) (s_subset r1 r22)
   423         else
   424           if s_subset r1 r21 = True orelse s_subset r1 r22 = True
   425              orelse r1 = r2 then
   426             True
   427           else
   428             Subset (r1, r2)
   429       | s_subset r1 r2 =
   430         if r1 = r2 orelse is_none_product r1 then True
   431         else if is_none_product r2 then s_no r1
   432         else if forall is_one_rel_expr [r1, r2] then s_rel_eq r1 r2
   433         else Subset (r1, r2)
   434 
   435     (* expr_assign list -> rel_expr -> rel_expr *)
   436     fun s_rel_let [b as AssignRelReg (x', r')] (r as RelReg x) =
   437         if x = x' then r' else RelLet ([b], r)
   438       | s_rel_let bs r = RelLet (bs, r)
   439 
   440     (* formula -> rel_expr -> rel_expr -> rel_expr *)
   441     fun s_rel_if f r1 r2 =
   442       (case (f, r1, r2) of
   443          (True, _, _) => r1
   444        | (False, _, _) => r2
   445        | (No r1', None, RelIf (One r2', r3', r4')) =>
   446          if r1' = r2' andalso r2' = r3' then s_rel_if (Lone r1') r1' r4'
   447          else raise SAME ()
   448        | _ => raise SAME ())
   449       handle SAME () => if r1 = r2 then r1 else RelIf (f, r1, r2)
   450 
   451     (* rel_expr -> rel_expr -> rel_expr *)
   452     fun s_union r1 (Union (r21, r22)) = s_union (s_union r1 r21) r22
   453       | s_union r1 r2 =
   454         if is_none_product r1 then r2
   455         else if is_none_product r2 then r1
   456         else if r1 = r2 then r1
   457         else if occurs_in_union r2 r1 then r1
   458         else Union (r1, r2)
   459     fun s_difference r1 r2 =
   460       if is_none_product r1 orelse is_none_product r2 then r1
   461       else if r1 = r2 then empty_n_ary_rel (arity_of_rel_expr r1)
   462       else Difference (r1, r2)
   463     fun s_override r1 r2 =
   464       if is_none_product r2 then r1
   465       else if is_none_product r1 then r2
   466       else Override (r1, r2)
   467     fun s_intersect r1 r2 =
   468       case rel_expr_intersects r1 r2 of
   469         SOME true => if r1 = r2 then r1 else Intersect (r1, r2)
   470       | SOME false => empty_n_ary_rel (arity_of_rel_expr r1)
   471       | NONE => if is_none_product r1 then r1
   472                 else if is_none_product r2 then r2
   473                 else Intersect (r1, r2)
   474     fun s_product r1 r2 =
   475       if is_none_product r1 then
   476         Product (r1, empty_n_ary_rel (arity_of_rel_expr r2))
   477       else if is_none_product r2 then
   478         Product (empty_n_ary_rel (arity_of_rel_expr r1), r2)
   479       else
   480         Product (r1, r2)
   481     fun s_join r1 (Product (Product (r211, r212), r22)) =
   482         Product (s_join r1 (Product (r211, r212)), r22)
   483       | s_join (Product (r11, Product (r121, r122))) r2 =
   484         Product (r11, s_join (Product (r121, r122)) r2)
   485       | s_join None r = empty_n_ary_rel (arity_of_rel_expr r - 1)
   486       | s_join r None = empty_n_ary_rel (arity_of_rel_expr r - 1)
   487       | s_join (Product (None, None)) r = empty_n_ary_rel (arity_of_rel_expr r)
   488       | s_join r (Product (None, None)) = empty_n_ary_rel (arity_of_rel_expr r)
   489       | s_join Iden r2 = r2
   490       | s_join r1 Iden = r1
   491       | s_join (Product (r1, r2)) Univ =
   492         if arity_of_rel_expr r2 = 1 then r1
   493         else Product (r1, s_join r2 Univ)
   494       | s_join Univ (Product (r1, r2)) =
   495         if arity_of_rel_expr r1 = 1 then r2
   496         else Product (s_join Univ r1, r2)
   497       | s_join r1 (r2 as Product (r21, r22)) =
   498         if arity_of_rel_expr r1 = 1 then
   499           case rel_expr_intersects r1 r21 of
   500             SOME true => r22
   501           | SOME false => empty_n_ary_rel (arity_of_rel_expr r2 - 1)
   502           | NONE => Join (r1, r2)
   503         else
   504           Join (r1, r2)
   505       | s_join (r1 as Product (r11, r12)) r2 =
   506         if arity_of_rel_expr r2 = 1 then
   507           case rel_expr_intersects r2 r12 of
   508             SOME true => r11
   509           | SOME false => empty_n_ary_rel (arity_of_rel_expr r1 - 1)
   510           | NONE => Join (r1, r2)
   511         else
   512           Join (r1, r2)
   513       | s_join r1 (r2 as RelIf (f, r21, r22)) =
   514         if inline_rel_expr r1 then s_rel_if f (s_join r1 r21) (s_join r1 r22)
   515         else Join (r1, r2)
   516       | s_join (r1 as RelIf (f, r11, r12)) r2 =
   517         if inline_rel_expr r2 then s_rel_if f (s_join r11 r2) (s_join r12 r2)
   518         else Join (r1, r2)
   519       | s_join (r1 as Atom j1) (r2 as Rel (x as (2, j2))) =
   520         if x = suc_rel then
   521           let val n = to_nat j1 + 1 in
   522             if n < nat_card then from_nat n else None
   523           end
   524         else
   525           Join (r1, r2)
   526       | s_join r1 (r2 as Project (r21, Num k :: is)) =
   527         if k = arity_of_rel_expr r21 - 1 andalso arity_of_rel_expr r1 = 1 then
   528           s_project (s_join r21 r1) is
   529         else
   530           Join (r1, r2)
   531       | s_join r1 (Join (r21, r22 as Rel (x as (3, j22)))) =
   532         ((if x = nat_add_rel then
   533             case (r21, r1) of
   534               (Atom j1, Atom j2) =>
   535               let val n = to_nat j1 + to_nat j2 in
   536                 if n < nat_card then from_nat n else None
   537               end
   538             | (Atom j, r) =>
   539               (case to_nat j of
   540                  0 => r
   541                | 1 => s_join r (Rel suc_rel)
   542                | _ => raise SAME ())
   543             | (r, Atom j) =>
   544               (case to_nat j of
   545                  0 => r
   546                | 1 => s_join r (Rel suc_rel)
   547                | _ => raise SAME ())
   548             | _ => raise SAME ()
   549           else if x = nat_subtract_rel then
   550             case (r21, r1) of
   551               (Atom j1, Atom j2) => from_nat (nat_minus (to_nat j1) (to_nat j2))
   552             | _ => raise SAME ()
   553           else if x = nat_multiply_rel then
   554             case (r21, r1) of
   555               (Atom j1, Atom j2) =>
   556               let val n = to_nat j1 * to_nat j2 in
   557                 if n < nat_card then from_nat n else None
   558               end
   559             | (Atom j, r) =>
   560               (case to_nat j of 0 => Atom j | 1 => r | _ => raise SAME ())
   561             | (r, Atom j) =>
   562               (case to_nat j of 0 => Atom j | 1 => r | _ => raise SAME ())
   563             | _ => raise SAME ()
   564           else
   565             raise SAME ())
   566          handle SAME () => List.foldr Join r22 [r1, r21])
   567       | s_join r1 r2 = Join (r1, r2)
   568 
   569     (* rel_expr -> rel_expr *)
   570     fun s_closure Iden = Iden
   571       | s_closure r = if is_none_product r then r else Closure r
   572     fun s_reflexive_closure Iden = Iden
   573       | s_reflexive_closure r =
   574         if is_none_product r then Iden else ReflexiveClosure r
   575 
   576     (* decl list -> formula -> rel_expr *)
   577     fun s_comprehension ds False = empty_n_ary_rel (length ds)
   578       | s_comprehension ds True = fold1 s_product (map decl_one_set ds)
   579       | s_comprehension [d as DeclOne ((1, j1), r)]
   580                         (f as RelEq (Var (1, j2), Atom j)) =
   581         if j1 = j2 andalso rel_expr_intersects (Atom j) r = SOME true then
   582           Atom j
   583         else
   584           Comprehension ([d], f)
   585       | s_comprehension ds f = Comprehension (ds, f)
   586 
   587     (* rel_expr -> int -> int -> rel_expr *)
   588     fun s_project_seq r =
   589       let
   590         (* int -> rel_expr -> int -> int -> rel_expr *)
   591         fun aux arity r j0 n =
   592           if j0 = 0 andalso arity = n then
   593             r
   594           else case r of
   595             RelIf (f, r1, r2) =>
   596             s_rel_if f (aux arity r1 j0 n) (aux arity r2 j0 n)
   597           | Product (r1, r2) =>
   598             let
   599               val arity2 = arity_of_rel_expr r2
   600               val arity1 = arity - arity2
   601               val n1 = Int.min (nat_minus arity1 j0, n)
   602               val n2 = n - n1
   603               (* unit -> rel_expr *)
   604               fun one () = aux arity1 r1 j0 n1
   605               fun two () = aux arity2 r2 (nat_minus j0 arity1) n2
   606             in
   607               case (n1, n2) of
   608                 (0, _) => s_rel_if (s_some r1) (two ()) (empty_n_ary_rel n2)
   609               | (_, 0) => s_rel_if (s_some r2) (one ()) (empty_n_ary_rel n1)
   610               | _ => s_product (one ()) (two ())
   611             end
   612           | _ => s_project r (num_seq j0 n)
   613       in aux (arity_of_rel_expr r) r end
   614 
   615     (* rel_expr -> rel_expr -> rel_expr *)
   616     fun s_nat_subtract r1 r2 = fold s_join [r1, r2] (Rel nat_subtract_rel)
   617     fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2)
   618       | s_nat_less r1 r2 = fold s_join [r1, r2] (Rel nat_less_rel)
   619     fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2)
   620       | s_int_less r1 r2 = fold s_join [r1, r2] (Rel int_less_rel)
   621 
   622     (* rel_expr -> int -> int -> rel_expr *)
   623     fun d_project_seq r j0 n = Project (r, num_seq j0 n)
   624     (* rel_expr -> rel_expr *)
   625     fun d_not3 r = Join (r, Rel not3_rel)
   626     (* rel_expr -> rel_expr -> rel_expr *)
   627     fun d_nat_subtract r1 r2 = List.foldl Join (Rel nat_subtract_rel) [r1, r2]
   628     fun d_nat_less r1 r2 = List.foldl Join (Rel nat_less_rel) [r1, r2]
   629     fun d_int_less r1 r2 = List.foldl Join (Rel int_less_rel) [r1, r2]
   630   in
   631     if optim then
   632       {kk_all = s_all, kk_exist = s_exist, kk_formula_let = s_formula_let,
   633        kk_formula_if = s_formula_if, kk_or = s_or, kk_not = s_not,
   634        kk_iff = s_iff, kk_implies = s_implies, kk_and = s_and,
   635        kk_subset = s_subset, kk_rel_eq = s_rel_eq, kk_no = s_no,
   636        kk_lone = s_lone, kk_one = s_one, kk_some = s_some,
   637        kk_rel_let = s_rel_let, kk_rel_if = s_rel_if, kk_union = s_union,
   638        kk_difference = s_difference, kk_override = s_override,
   639        kk_intersect = s_intersect, kk_product = s_product, kk_join = s_join,
   640        kk_closure = s_closure, kk_reflexive_closure = s_reflexive_closure,
   641        kk_comprehension = s_comprehension, kk_project = s_project,
   642        kk_project_seq = s_project_seq, kk_not3 = s_not3,
   643        kk_nat_less = s_nat_less, kk_int_less = s_int_less}
   644     else
   645       {kk_all = curry All, kk_exist = curry Exist,
   646        kk_formula_let = curry FormulaLet, kk_formula_if = curry3 FormulaIf,
   647        kk_or = curry Or,kk_not = Not, kk_iff = curry Iff, kk_implies = curry
   648        Implies, kk_and = curry And, kk_subset = curry Subset, kk_rel_eq = curry
   649        RelEq, kk_no = No, kk_lone = Lone, kk_one = One, kk_some = Some,
   650        kk_rel_let = curry RelLet, kk_rel_if = curry3 RelIf, kk_union = curry
   651        Union, kk_difference = curry Difference, kk_override = curry Override,
   652        kk_intersect = curry Intersect, kk_product = curry Product,
   653        kk_join = curry Join, kk_closure = Closure,
   654        kk_reflexive_closure = ReflexiveClosure, kk_comprehension = curry
   655        Comprehension, kk_project = curry Project,
   656        kk_project_seq = d_project_seq, kk_not3 = d_not3,
   657        kk_nat_less = d_nat_less, kk_int_less = d_int_less}
   658   end
   659 
   660 end;