# HG changeset patch
# User bulwahn
# Date 1299853273 -3600
# Node ID d786a8a3dc47ee5b186c7d055394c7d05b85f011
# Parent  db9cfca3408566c00de197648eea3cc651459a56
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common

diff -r db9cfca34085 -r d786a8a3dc47 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Quickcheck.thy	Fri Mar 11 15:21:13 2011 +0100
@@ -134,12 +134,12 @@
 
 subsection {* Code setup *}
 
-code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
+code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
   -- {* With enough criminal energy this can be abused to derive @{prop False};
   for this reason we use a distinguished target @{text Quickcheck}
   not spoiling the regular trusted code generation *}
 
-code_reserved Quickcheck Quickcheck_Generators
+code_reserved Quickcheck Random_Generators
 
 no_notation fcomp (infixl "\<circ>>" 60)
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
diff -r db9cfca34085 -r d786a8a3dc47 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -291,75 +291,6 @@
         $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
   in Abs ("d", @{typ code_numeral}, fold_rev mk_exhaustive_closure bounds check) end
 
-(** 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])
-
-fun mk_fun_upd T1 T2 (t1, t2) t = 
-  Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
-
-fun dest_fun_upds t =
-  case try dest_fun_upd t of
-    NONE =>
-      (case t of
-        Abs (_, _, _) => ([], t) 
-      | _ => raise TERM ("dest_fun_upds", [t]))
-  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
-
-fun make_fun_upds 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
-  | 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_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 =
-  let
-    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_fun_upds 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
-                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
-                 | _ => raise TERM ("post_process_term", [t]))
-            | Type (@{type_name option}, _) =>
-                (case t of
-                  Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
-                | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
-                | _ => make_fun_upds T1 T2) 
-            | _ => make_fun_upds T1 T2)
-        | NONE => process_args t)
-    | _ => process_args t
-  end
-
 (** generator compiliation **)
 
 fun compile_generator_expr ctxt t =
@@ -373,7 +304,8 @@
       thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
   in
     fn size => rpair NONE (compile size |> 
-      (if Config.get ctxt quickcheck_pretty then Option.map (map post_process_term) else I))
+      (if Config.get ctxt quickcheck_pretty then
+        Option.map (map Quickcheck_Common.post_process_term) else I))
   end;
 
 fun compile_generator_exprs ctxt ts =
@@ -388,7 +320,8 @@
       thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
       (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') [];
   in
-    map (fn compile => fn size => compile size |> Option.map (map post_process_term)) compiles
+    map (fn compile => fn size => compile size
+      |> Option.map (map Quickcheck_Common.post_process_term)) compiles
   end;
   
   
diff -r db9cfca34085 -r d786a8a3dc47 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -13,11 +13,14 @@
     sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
       string list * string list -> typ list * typ list -> theory -> theory)
     -> Datatype.config -> string list -> theory -> theory
+  val post_process_term : term -> term
 end;
 
 structure Quickcheck_Common : QUICKCHECK_COMMON =
 struct
 
+(** ensuring sort constraints **)
+
 fun perhaps_constrain thy insts raw_vs =
   let
     fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) 
@@ -50,5 +53,75 @@
             ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
       | NONE => thy
   end;
+  
+(** 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])
+
+fun mk_fun_upd T1 T2 (t1, t2) t = 
+  Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
+
+fun dest_fun_upds t =
+  case try dest_fun_upd t of
+    NONE =>
+      (case t of
+        Abs (_, _, _) => ([], t) 
+      | _ => raise TERM ("dest_fun_upds", [t]))
+  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
+
+fun make_fun_upds 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
+  | 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_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 =
+  let
+    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_fun_upds 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
+                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
+                 | _ => raise TERM ("post_process_term", [t]))
+            | Type (@{type_name option}, _) =>
+                (case t of
+                  Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
+                | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
+                | _ => make_fun_upds T1 T2) 
+            | _ => make_fun_upds T1 T2)
+        | NONE => process_args t)
+    | _ => process_args t
+  end
+  
 
 end;