# HG changeset patch
# User haftmann
# Date 1244877385 -7200
# Node ID b72c11302b3977c3826a18da818a0a84ad36e290
# Parent  b30570327b760c98a9477f8ef9d9c0747cb02fd0
quickcheck generators for datatypes with functions

diff -r b30570327b76 -r b72c11302b39 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Sat Jun 13 09:16:24 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Jun 13 09:16:25 2009 +0200
@@ -254,8 +254,6 @@
 
 (* constructing random instances on datatypes *)
 
-exception Datatype_Fun; (*FIXME*)
-
 fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
   let
     val mk_const = curry (Sign.mk_const thy);
@@ -274,19 +272,20 @@
     val random_auxT = sizeT o random_resultT;
     val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
       random_auxsN rTs;
-
     fun mk_random_call T = (NONE, (HOLogic.mk_random T j, T));
     fun mk_random_aux_call fTs (k, _) (tyco, Ts) =
       let
-        val _ = if null fTs then () else raise Datatype_Fun; (*FIXME*)
-        val random = nth random_auxs k;
+        val T = Type (tyco, Ts);
+        fun mk_random_fun_lift [] t = t
+          | mk_random_fun_lift (fT :: fTs) t =
+              mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
+                mk_random_fun_lift fTs t;
+        val t = mk_random_fun_lift fTs (nth random_auxs k $ i1 $ j);
         val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
           |> the_default 0;
-      in (SOME size, (random $ i1 $ j, Type (tyco, Ts))) end;
-
+      in (SOME size, (t, fTs ---> T)) end;
     val tss = DatatypeAux.interpret_construction descr vs
       { atyp = mk_random_call, dtyp = mk_random_aux_call };
-
     fun mk_consexpr simpleT (c, xs) =
       let
         val (ks, simple_tTs) = split_list xs;
@@ -347,35 +346,39 @@
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;
 
+fun perhaps_constrain thy insts raw_vs =
+  let
+    fun meet_random (T, sort) = Sorts.meet_sort (Sign.classes_of thy) 
+      (Logic.varifyT T, sort);
+    val vtab = Vartab.empty
+      |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
+      |> fold meet_random insts;
+  in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
+  end handle CLASS_ERROR => NONE;
+
 fun ensure_random_datatype raw_tycos thy =
   let
     val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy;
     val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
       DatatypePackage.the_datatype_descr thy raw_tycos;
-    val aTs = (flat o maps snd o maps snd) (DatatypeAux.interpret_construction descr raw_vs
-      { atyp = single, dtyp = K o K });
-    fun meet_random T = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT T, @{sort random});
-    val vtab = (Vartab.empty
-      |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
-      |> fold meet_random aTs
-      |> SOME) handle CLASS_ERROR => NONE;
-    val vconstrain = case vtab of SOME vtab => (fn (v, _) =>
-          (v, (the o Vartab.lookup vtab) (v, 0)))
-      | NONE => I;
-    val vs = map vconstrain raw_vs;
-    val constrain = map_atyps (fn TFree v => TFree (vconstrain v));
+    val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
+      (DatatypeAux.interpret_construction descr raw_vs { atyp = single, dtyp = (K o K o K) [] });
+    val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
+      (DatatypeAux.interpret_construction descr raw_vs { atyp = K [], dtyp = K o K });
     val has_inst = exists (fn tyco =>
       can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
-  in if is_some vtab andalso not has_inst then
-    (mk_random_datatype descr vs tycos (names, auxnames)
-      ((pairself o map) constrain raw_TUs) thy
-    (*FIXME ephemeral handles*)
-    handle Datatype_Fun => thy
-         | e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
-         | e as TYPE (msg, _, _) =>  (tracing msg; raise e)
-         | e as ERROR msg =>  (tracing msg; raise e))
-  else thy end;
+  in if has_inst then thy
+    else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
+     of SOME constrain => (mk_random_datatype descr
+          (map constrain raw_vs) tycos (names, auxnames)
+            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
+            (*FIXME ephemeral handles*)
+          handle e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
+               | e as TYPE (msg, _, _) => (tracing msg; raise e)
+               | e as ERROR msg => (tracing msg; raise e))
+      | NONE => thy
+  end;
 
 
 (** setup **)