improving term postprocessing for counterexample presentation in quickcheck

--- a/src/HOL/Tools/smallvalue_generators.ML	Fri Mar 11 08:12:55 2011 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Mar 11 08:12:58 2011 +0100
@@ -306,12 +306,11 @@
   case try dest_fun_upd t of
     NONE =>
       (case t of
-        (Abs (_, _, Const (@{const_name HOL.undefined}, _))) => []
+        Abs (_, _, _) => ([], t) 
       | _ => raise TERM ("dest_plain_fun", [t]))
-  | SOME (t0, (t1, t2)) => (t1, t2) :: dest_plain_fun t0
+  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_plain_fun t0)
 
-fun make_plain_fun T1 T2 tps =
-  fold_rev (mk_fun_upd T1 T2) tps (absdummy (T1, Const ("_", T2)))
+fun make_plain_fun T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
 
 fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
   | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
@@ -320,23 +319,48 @@
       $ t1 $ (make_set T1 tps)
   | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
 
+fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
+  | make_coset T tps = 
+    let
+      val U = T --> @{typ bool}
+      fun invert @{const False} = @{const True}
+        | invert @{const True} = @{const False}
+    in
+      Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
+        $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
+    end
+
 fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
   | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   
 fun post_process_term t =
-  case fastype_of t of
-    Type (@{type_name fun}, [T1, T2]) =>
-      (case try dest_plain_fun t of
-        SOME tps =>
-          tps
-          |> map (pairself post_process_term)
-          |> (case T2 of
-            @{typ bool} => rev #> make_set T1
-          | Type (@{type_name option}, _) => make_map T1 T2
-          | _ => make_plain_fun T1 T2)
-      | NONE => t)
-  | _ => t
+  let
+    (*val _ = tracing ("post_process:" ^ Syntax.string_of_term ctxt t)*)
+    fun map_Abs f t =
+      case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
+    fun process_args t = case strip_comb t of
+      (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
+  in
+    case fastype_of t of
+      Type (@{type_name fun}, [T1, T2]) =>
+        (case try dest_plain_fun t of
+          SOME (tps, t) =>
+            (map (pairself post_process_term) tps, map_Abs post_process_term t)
+            |> (case T2 of
+              @{typ bool} => 
+                (case t of
+                   Abs(_, _, @{const True}) => fst #> rev #> make_set T1
+                 | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
+                 | _ => raise TERM ("post_process_term", [t]))
+            | Type (@{type_name option}, _) =>
+                (case t of
+                  Abs(_, _, Const(@{const_name None}, _)) => fst #> (make_map T1 T2)
+                | _ => make_plain_fun T1 T2) 
+            | _ => make_plain_fun T1 T2)
+        | NONE => raise TERM ("post_process_term", [t]))
+    | _ => process_args t
+  end
 
 (** generator compiliation **)