# HG changeset patch
# User blanchet
# Date 1411566400 -7200
# Node ID 73df5884edcfa883a4e9133c7b61c45eb073fcae
# Parent  0b94858325a50b9f7dc5d19e45422d1268545920
allow homogeneous nesting for SMT (co)datatypes

diff -r 0b94858325a5 -r 73df5884edcf src/HOL/Tools/SMT/smt_datatypes.ML
--- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:25 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:40 2014 +0200
@@ -79,12 +79,21 @@
           val Xs = map #X mutual_fp_sugars
           val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
 
-          (* FIXME: allow nested recursion to same FP kind *)
-          fun is_nested_co_recursive (T as Type _) = BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs T
-            | is_nested_co_recursive _ = false
+          (* Datatypes nested through datatypes and codatatypes nested through codatatypes are
+             allowed. So are mutually (co)recursive (co)datatypes. *)
+          fun is_same_fp s =
+            (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
+              SOME {fp = fp', ...} => fp' = fp
+            | NONE => false)
+          fun is_homogenously_nested_co_recursive (Type (s, Ts)) =
+              forall (if is_same_fp s then is_homogenously_nested_co_recursive
+                else not o BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs) Ts
+            | is_homogenously_nested_co_recursive _ = true
         in
-          if exists (exists (exists is_nested_co_recursive)) ctrXs_Tsss then maybe_typedef ()
-          else get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp)
+          if forall (forall (forall is_homogenously_nested_co_recursive)) ctrXs_Tsss then
+            get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp)
+          else
+            maybe_typedef ()
         end
       else
         ([], ctxt)