# HG changeset patch
# User bulwahn
# Date 1292431606 -3600
# Node ID f4d3acf0c4cc0c489d91bb5ac2a724ec464afa50
# Parent  810a885deceece752e3e0f2c56a9fba37f2325e0
adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition

diff -r 810a885decee -r f4d3acf0c4cc src/HOL/Smallcheck.thy
--- a/src/HOL/Smallcheck.thy	Wed Dec 15 17:46:46 2010 +0100
+++ b/src/HOL/Smallcheck.thy	Wed Dec 15 17:46:46 2010 +0100
@@ -281,7 +281,9 @@
 begin
 
 definition
-  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App (Code_Evaluation.term_of (Some :: 'a => 'a option)) (t ())))"
+  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
+    (Code_Evaluation.Const (STR ''Option.option.Some'')
+      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
 
 definition enum_term_of_option :: "'a option itself => unit => term list"
 where
diff -r 810a885decee -r f4d3acf0c4cc src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 15 17:46:46 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 15 17:46:46 2010 +0100
@@ -280,12 +280,7 @@
         $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
   in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
 
-fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
-  | make_set T1 ((t1, @{const False}) :: tps) = make_set T1 tps
-  | make_set T1 ((t1, @{const True}) :: tps) =
-    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
-      $ t1 $ (make_set T1 tps)
-  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
+(** post-processing of function terms **)
 
 fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
   | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
@@ -303,14 +298,34 @@
 
 fun make_plain_fun T1 T2 tps =
   fold_rev (mk_fun_upd T1 T2) tps (absdummy (T1, Const ("_", T2)))
+
+fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
+  | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
+  | make_set T1 ((t1, @{const True}) :: tps) =
+    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
+      $ t1 $ (make_set T1 tps)
+  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
+
+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]) =>
-      dest_plain_fun t |> map (pairself post_process_term) |>
-        (if T2 = @{typ bool} then rev #> make_set T1 else make_plain_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
 
+(** generator compiliation **)
+
 fun compile_generator_expr ctxt t =
   let
     val thy = ProofContext.theory_of ctxt