src/HOL/Tools/Nitpick/nitpick_peephole.ML
changeset 55889 6bfbec3dff62
parent 45398 7dbb7b044a11
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Mar 03 22:33:22 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -128,14 +128,18 @@
     1.4  fun formula_for_bool b = if b then True else False
     1.5  
     1.6  fun atom_for_nat (k, j0) n = if n < 0 orelse n >= k then ~1 else n + j0
     1.7 +
     1.8  fun min_int_for_card k = ~k div 2 + 1
     1.9  fun max_int_for_card k = k div 2
    1.10 +
    1.11  fun int_for_atom (k, j0) j =
    1.12    let val j = j - j0 in if j <= max_int_for_card k then j else j - k end
    1.13 +
    1.14  fun atom_for_int (k, j0) n =
    1.15    if n < min_int_for_card k orelse n > max_int_for_card k then ~1
    1.16    else if n < 0 then n + k + j0
    1.17    else n + j0
    1.18 +
    1.19  fun is_twos_complement_representable bits n =
    1.20    let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
    1.21  
    1.22 @@ -147,6 +151,7 @@
    1.23                       "too large cardinality (" ^ string_of_int n ^ ")")
    1.24    else
    1.25      (max_squeeze_card + 1) * m + n
    1.26 +
    1.27  fun unsqueeze p = (p div (max_squeeze_card + 1), p mod (max_squeeze_card + 1))
    1.28  
    1.29  fun boolify (j, b) = 2 * j + (if b then 0 else 1)
    1.30 @@ -154,6 +159,7 @@
    1.31  
    1.32  fun suc_rel_for_atom_seq (x, tabulate) =
    1.33    (2, suc_rels_base - boolify (squeeze x, tabulate))
    1.34 +
    1.35  fun atom_seq_for_suc_rel (_, j) = unboolify (~ j + suc_rels_base) |>> unsqueeze
    1.36  
    1.37  fun is_none_product (Product (r1, r2)) =
    1.38 @@ -206,8 +212,10 @@
    1.39  
    1.40  fun is_Num (Num _) = true
    1.41    | is_Num _ = false
    1.42 +
    1.43  fun dest_Num (Num k) = k
    1.44    | dest_Num _ = raise ARG ("Nitpick_Peephole.dest_Num", "not \"Num\"")
    1.45 +
    1.46  fun num_seq j0 n = map Num (index_seq j0 n)
    1.47  
    1.48  fun occurs_in_union r (Union (r1, r2)) =