# HG changeset patch
# User blanchet
# Date 1300446323 -3600
# Node ID 1d7735ae42737d184d11876010a34891e9e730c3
# Parent  03c2d29ec790fdac5694a0279715023013c8955f
more optimizations of bounds for "need"

diff -r 03c2d29ec790 -r 1d7735ae4273 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 11:43:28 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 12:05:23 2011 +0100
@@ -313,7 +313,6 @@
     in
       ([(x, bound_comment ctxt debug nick T R)],
        let
-         val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0)
          val complete_need_vals = (length need_vals = card)
          val (my_need_vals, other_need_vals) =
            need_vals
@@ -322,13 +321,22 @@
                       exists (fn FreeRel (x', _, _, _) => x = x'
                                | _ => false) sel_us
                     | _ => false)
+         fun upper_bound_ts () =
+           if complete_need_vals then
+             my_need_vals |> map (KK.Tuple o single o snd) |> KK.TupleSet
+           else if not (null other_need_vals) then
+             index_seq (delta + j0) (epsilon - delta)
+             |> filter_out (member (op = o apsnd snd) other_need_vals)
+             |> map (KK.Tuple o single) |> KK.TupleSet
+           else
+             KK.TupleAtomSeq (epsilon - delta, delta + j0)
        in
          if explicit_max = 0 orelse
-            (complete_need_vals andalso null my_need_vals) then
+            (complete_need_vals andalso null my_need_vals) (* ### needed? *) then
            [KK.TupleSet []]
          else
            if R2 = Formula Neut then
-             [ts] |> not exclusive ? cons (KK.TupleSet [])
+             [upper_bound_ts ()] |> not exclusive ? cons (KK.TupleSet [])
            else
              [KK.TupleSet [],
               if T1 = T2 andalso epsilon > delta andalso
@@ -339,7 +347,7 @@
                                             KK.TupleAtomSeq (j, j0)))
                 |> foldl1 KK.TupleUnion
               else
-                KK.TupleProduct (ts, upper_bound_for_rep R2)]
+                KK.TupleProduct (upper_bound_ts (), upper_bound_for_rep R2)]
          end)
     end
   | bound_for_sel_rel _ _ _ _ u =
@@ -1525,7 +1533,9 @@
                  else
                    accum)
         | aux _ = I
-    in SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map snd end
+    in
+      SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd)
+    end
 
 fun needed_value_axioms_for_datatype _ _ NONE = [KK.False]
   | needed_value_axioms_for_datatype ofs kk (SOME fixed) =