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