# HG changeset patch
# User berghofe
# Date 1102694057 -3600
# Node ID 5260ac75e07c55a6c66a8d75644b77cf26a8023f
# Parent  0a36ccb79481794d338f9d55a654a39f1cad467f
Fixed bug in mk_gen_of_def that could cause non-termination of the generator
for datatypes with nested recursion (such as trie).

diff -r 0a36ccb79481 -r 5260ac75e07c src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Fri Dec 10 16:50:20 2004 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Dec 10 16:54:17 2004 +0100
@@ -114,11 +114,12 @@
             fun mk_delay p = Pretty.block
               [Pretty.str "fn () =>", Pretty.brk 1, p];
 
-            fun mk_constr s (cname, dts) =
+            fun mk_constr s b (cname, dts) =
               let
-                val Ts = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
-                val gs = map (fn T => mk_app false (mk_gen sg false rtnames s T)
-                  [Pretty.str "j"]) Ts;
+                val gs = map (fn dt => mk_app false (mk_gen sg false rtnames s
+                    (DatatypeAux.typ_of_dtyp descr sorts dt))
+                  [Pretty.str (if b andalso DatatypeAux.is_rec_type dt then "0"
+                     else "j")]) dts;
                 val id = mk_const_id sg cname
               in case gs of
                   _ :: _ :: _ => Pretty.block
@@ -126,11 +127,11 @@
                 | _ => mk_app false (Pretty.str id) (map parens gs)
               end;
 
-            fun mk_choice [c] = mk_constr "(i-1)" c
+            fun mk_choice [c] = mk_constr "(i-1)" false c
               | mk_choice cs = Pretty.block [Pretty.str "one_of",
                   Pretty.brk 1, Pretty.blk (1, Pretty.str "[" ::
                   flat (separate [Pretty.str ",", Pretty.fbrk]
-                    (map (single o mk_delay o mk_constr "(i-1)") cs)) @
+                    (map (single o mk_delay o mk_constr "(i-1)" false) cs)) @
                   [Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"];
 
             val gs = map (Pretty.str o suffix "G" o strip_tname) tvs;
@@ -154,7 +155,7 @@
                  [Pretty.block [Pretty.str "(case", Pretty.brk 1,
                    Pretty.str "i", Pretty.brk 1, Pretty.str "of",
                    Pretty.brk 1, Pretty.str "0 =>", Pretty.brk 1,
-                   mk_constr "0" (cname, the (assoc (cs, cname))),
+                   mk_constr "0" true (cname, the (assoc (cs, cname))),
                    Pretty.brk 1, Pretty.str "| _ =>", Pretty.brk 1,
                    mk_choice cs1, Pretty.str ")"]]
                else [mk_choice cs2])) ::