# HG changeset patch
# User bulwahn
# Date 1302273074 -7200
# Node ID 5bf3b9612e434804061e6714cdf718c8e3a386ff
# Parent  eb32a8474a57b72996a46eaddad50ddb07a95c1c
ensuring datatype limitations before the instantiation in quickcheck_exhaustive

diff -r eb32a8474a57 -r 5bf3b9612e43 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
@@ -160,8 +160,8 @@
     val mk_aux_call = gen_mk_aux_call functerms
     val mk_consexpr = gen_mk_consexpr test_function functerms
     fun mk_rhs exprs =
-        @{term "If :: bool => term list option => term list option => term list option"}
-            $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
+      @{term "If :: bool => term list option => term list option => term list option"}
+          $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
   in
     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   end
@@ -296,20 +296,26 @@
       "Creation of exhaustive generators failed because the datatype contains a function type";
     thy)
 
+val contains_recursive_type_under_function_types =
+  exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
+    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false))))
+    
 fun instantiate_bounded_forall_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
-  let
-    val _ = Datatype_Aux.message config "Creating bounded universal quantifiers...";
-    val bounded_forallsN = map (prefix (bounded_forallN ^ "_")) (names @ auxnames);
-  in
-    thy
-    |> Class.instantiation (tycos, vs, @{sort bounded_forall})
-    |> Quickcheck_Common.define_functions
-        (fn functerms => mk_bounded_forall_equations functerms (descr, vs, Ts @ Us), NONE)
-        prfx ["P", "i"] bounded_forallsN (map bounded_forallT (Ts @ Us))
-    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
-  end handle FUNCTION_TYPE =>
+  if not (contains_recursive_type_under_function_types descr) then
+    let
+      val _ = Datatype_Aux.message config "Creating bounded universal quantifiers..."
+      val bounded_forallsN = map (prefix (bounded_forallN ^ "_")) (names @ auxnames)
+    in
+      thy
+      |> Class.instantiation (tycos, vs, @{sort bounded_forall})
+      |> Quickcheck_Common.define_functions
+          (fn functerms => mk_bounded_forall_equations functerms (descr, vs, Ts @ Us), NONE)
+          prfx ["P", "i"] bounded_forallsN (map bounded_forallT (Ts @ Us))
+      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+    end
+  else
     (Datatype_Aux.message config
-      "Creation of bounded universal quantifiers failed because the datatype contains a function type";
+      "Creation of bounded universal quantifiers failed because the datatype is recursive under a function type";
     thy)
     
 (* building and compiling generator expressions *)