src/HOL/Tools/Nitpick/nitpick_peephole.ML
changeset 38126 8031d099379a
parent 36390 eee4ee6a5cbe
child 45398 7dbb7b044a11
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Sat Jul 31 22:02:54 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Sun Aug 01 15:51:25 2010 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4    val initial_pool : name_pool
     1.5    val not3_rel : n_ary_index
     1.6    val suc_rel : n_ary_index
     1.7 +  val suc_rels_base : int
     1.8    val unsigned_bit_word_sel_rel : n_ary_index
     1.9    val signed_bit_word_sel_rel : n_ary_index
    1.10    val nat_add_rel : n_ary_index
    1.11 @@ -46,6 +47,8 @@
    1.12    val int_for_atom : int * int -> int -> int
    1.13    val atom_for_int : int * int -> int -> int
    1.14    val is_twos_complement_representable : int -> int -> bool
    1.15 +  val suc_rel_for_atom_seq : (int * int) * bool -> n_ary_index
    1.16 +  val atom_seq_for_suc_rel : n_ary_index -> (int * int) * bool
    1.17    val inline_rel_expr : rel_expr -> bool
    1.18    val empty_n_ary_rel : int -> rel_expr
    1.19    val num_seq : int -> int -> int_expr list
    1.20 @@ -99,30 +102,27 @@
    1.21     formula_reg: int,
    1.22     rel_reg: int}
    1.23  
    1.24 -(* If you add new built-in relations, make sure to increment the counters here
    1.25 -   as well to avoid name clashes (which fortunately would be detected by
    1.26 -   Kodkodi). *)
    1.27 -val initial_pool =
    1.28 -  {rels = [(2, 10), (3, 20), (4, 10)], vars = [], formula_reg = 10,
    1.29 -   rel_reg = 10}
    1.30 +(* FIXME: needed? *)
    1.31 +val initial_pool = {rels = [], vars = [], formula_reg = 10, rel_reg = 10}
    1.32  
    1.33 -val not3_rel = (2, 0)
    1.34 -val suc_rel = (2, 1)
    1.35 -val unsigned_bit_word_sel_rel = (2, 2)
    1.36 -val signed_bit_word_sel_rel = (2, 3)
    1.37 -val nat_add_rel = (3, 0)
    1.38 -val int_add_rel = (3, 1)
    1.39 -val nat_subtract_rel = (3, 2)
    1.40 -val int_subtract_rel = (3, 3)
    1.41 -val nat_multiply_rel = (3, 4)
    1.42 -val int_multiply_rel = (3, 5)
    1.43 -val nat_divide_rel = (3, 6)
    1.44 -val int_divide_rel = (3, 7)
    1.45 -val nat_less_rel = (3, 8)
    1.46 -val int_less_rel = (3, 9)
    1.47 -val gcd_rel = (3, 10)
    1.48 -val lcm_rel = (3, 11)
    1.49 -val norm_frac_rel = (4, 0)
    1.50 +val not3_rel = (2, ~1)
    1.51 +val unsigned_bit_word_sel_rel = (2, ~2)
    1.52 +val signed_bit_word_sel_rel = (2, ~3)
    1.53 +val suc_rel = (2, ~4)
    1.54 +val suc_rels_base = ~5 (* must be the last of the binary series *)
    1.55 +val nat_add_rel = (3, ~1)
    1.56 +val int_add_rel = (3, ~2)
    1.57 +val nat_subtract_rel = (3, ~3)
    1.58 +val int_subtract_rel = (3, ~4)
    1.59 +val nat_multiply_rel = (3, ~5)
    1.60 +val int_multiply_rel = (3, ~6)
    1.61 +val nat_divide_rel = (3, ~7)
    1.62 +val int_divide_rel = (3, ~8)
    1.63 +val nat_less_rel = (3, ~9)
    1.64 +val int_less_rel = (3, ~10)
    1.65 +val gcd_rel = (3, ~11)
    1.66 +val lcm_rel = (3, ~12)
    1.67 +val norm_frac_rel = (4, ~1)
    1.68  
    1.69  fun atom_for_bool j0 = Atom o Integer.add j0 o int_from_bool
    1.70  fun formula_for_bool b = if b then True else False
    1.71 @@ -139,6 +139,23 @@
    1.72  fun is_twos_complement_representable bits n =
    1.73    let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
    1.74  
    1.75 +val max_squeeze_card = 49
    1.76 +
    1.77 +fun squeeze (m, n) =
    1.78 +  if n > max_squeeze_card then
    1.79 +    raise TOO_LARGE ("Nitpick_Peephole.squeeze",
    1.80 +                     "too large cardinality (" ^ string_of_int n ^ ")")
    1.81 +  else
    1.82 +    (max_squeeze_card + 1) * m + n
    1.83 +fun unsqueeze p = (p div (max_squeeze_card + 1), p mod (max_squeeze_card + 1))
    1.84 +
    1.85 +fun boolify (j, b) = 2 * j + (if b then 0 else 1)
    1.86 +fun unboolify j = (j div 2, j mod 2 = 0)
    1.87 +
    1.88 +fun suc_rel_for_atom_seq (x, tabulate) =
    1.89 +  (2, suc_rels_base - boolify (squeeze x, tabulate))
    1.90 +fun atom_seq_for_suc_rel (_, j) = unboolify (~ j + suc_rels_base) |>> unsqueeze
    1.91 +
    1.92  fun is_none_product (Product (r1, r2)) =
    1.93      is_none_product r1 orelse is_none_product r2
    1.94    | is_none_product None = true
    1.95 @@ -245,16 +262,18 @@
    1.96      fun to_nat j = j - main_j0
    1.97      val to_int = int_for_atom (int_card, main_j0)
    1.98  
    1.99 +    val exists_empty_decl = exists (fn DeclOne (_, None) => true | _ => false)
   1.100 +
   1.101      fun s_all _ True = True
   1.102        | s_all _ False = False
   1.103        | s_all [] f = f
   1.104 -      | s_all ds (All (ds', f)) = All (ds @ ds', f)
   1.105 -      | s_all ds f = All (ds, f)
   1.106 +      | s_all ds (All (ds', f)) = s_all (ds @ ds') f
   1.107 +      | s_all ds f = if exists_empty_decl ds then True else All (ds, f)
   1.108      fun s_exist _ True = True
   1.109        | s_exist _ False = False
   1.110        | s_exist [] f = f
   1.111 -      | s_exist ds (Exist (ds', f)) = Exist (ds @ ds', f)
   1.112 -      | s_exist ds f = Exist (ds, f)
   1.113 +      | s_exist ds (Exist (ds', f)) = s_exist (ds @ ds') f
   1.114 +      | s_exist ds f = if exists_empty_decl ds then False else Exist (ds, f)
   1.115  
   1.116      fun s_formula_let _ True = True
   1.117        | s_formula_let _ False = False