src/HOL/Tools/Nitpick/nitpick_peephole.ML
changeset 35280 54ab4921f826
parent 34982 7b8c366e34a2
child 35284 9edc2bd6d2bd
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Feb 22 10:28:49 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Feb 22 11:57:33 2010 +0100
     1.3 @@ -261,14 +261,10 @@
     1.4  (* bool -> int -> int -> int -> kodkod_constrs *)
     1.5  fun kodkod_constrs optim nat_card int_card main_j0 =
     1.6    let
     1.7 -    val false_atom = Atom main_j0
     1.8 -    val true_atom = Atom (main_j0 + 1)
     1.9 -
    1.10      (* bool -> int *)
    1.11      val from_bool = atom_for_bool main_j0
    1.12      (* int -> rel_expr *)
    1.13      fun from_nat n = Atom (n + main_j0)
    1.14 -    val from_int = Atom o atom_for_int (int_card, main_j0)
    1.15      (* int -> int *)
    1.16      fun to_nat j = j - main_j0
    1.17      val to_int = int_for_atom (int_card, main_j0)
    1.18 @@ -415,7 +411,7 @@
    1.19      fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2)
    1.20        | s_subset (Atom j) (AtomSeq (k, j0)) =
    1.21          formula_for_bool (j >= j0 andalso j < j0 + k)
    1.22 -      | s_subset (r1 as Union (r11, r12)) r2 =
    1.23 +      | s_subset (Union (r11, r12)) r2 =
    1.24          s_and (s_subset r11 r2) (s_subset r12 r2)
    1.25        | s_subset r1 (r2 as Union (r21, r22)) =
    1.26          if is_one_rel_expr r1 then
    1.27 @@ -516,7 +512,7 @@
    1.28        | s_join (r1 as RelIf (f, r11, r12)) r2 =
    1.29          if inline_rel_expr r2 then s_rel_if f (s_join r11 r2) (s_join r12 r2)
    1.30          else Join (r1, r2)
    1.31 -      | s_join (r1 as Atom j1) (r2 as Rel (x as (2, j2))) =
    1.32 +      | s_join (r1 as Atom j1) (r2 as Rel (x as (2, _))) =
    1.33          if x = suc_rel then
    1.34            let val n = to_nat j1 + 1 in
    1.35              if n < nat_card then from_nat n else None
    1.36 @@ -528,7 +524,7 @@
    1.37            s_project (s_join r21 r1) is
    1.38          else
    1.39            Join (r1, r2)
    1.40 -      | s_join r1 (Join (r21, r22 as Rel (x as (3, j22)))) =
    1.41 +      | s_join r1 (Join (r21, r22 as Rel (x as (3, _)))) =
    1.42          ((if x = nat_add_rel then
    1.43              case (r21, r1) of
    1.44                (Atom j1, Atom j2) =>
    1.45 @@ -613,7 +609,6 @@
    1.46        in aux (arity_of_rel_expr r) r end
    1.47  
    1.48      (* rel_expr -> rel_expr -> rel_expr *)
    1.49 -    fun s_nat_subtract r1 r2 = fold s_join [r1, r2] (Rel nat_subtract_rel)
    1.50      fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2)
    1.51        | s_nat_less r1 r2 = fold s_join [r1, r2] (Rel nat_less_rel)
    1.52      fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2)
    1.53 @@ -624,7 +619,6 @@
    1.54      (* rel_expr -> rel_expr *)
    1.55      fun d_not3 r = Join (r, Rel not3_rel)
    1.56      (* rel_expr -> rel_expr -> rel_expr *)
    1.57 -    fun d_nat_subtract r1 r2 = List.foldl Join (Rel nat_subtract_rel) [r1, r2]
    1.58      fun d_nat_less r1 r2 = List.foldl Join (Rel nat_less_rel) [r1, r2]
    1.59      fun d_int_less r1 r2 = List.foldl Join (Rel int_less_rel) [r1, r2]
    1.60    in