allow homogeneous nesting for SMT (co)datatypes
authorblanchet
Wed Sep 24 15:46:40 2014 +0200 (2014-09-24)
changeset 5843073df5884edcf
parent 58429 0b94858325a5
child 58431 751e8517daa7
allow homogeneous nesting for SMT (co)datatypes
src/HOL/Tools/SMT/smt_datatypes.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 24 15:46:40 2014 +0200
     1.3 @@ -79,12 +79,21 @@
     1.4            val Xs = map #X mutual_fp_sugars
     1.5            val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
     1.6  
     1.7 -          (* FIXME: allow nested recursion to same FP kind *)
     1.8 -          fun is_nested_co_recursive (T as Type _) = BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs T
     1.9 -            | is_nested_co_recursive _ = false
    1.10 +          (* Datatypes nested through datatypes and codatatypes nested through codatatypes are
    1.11 +             allowed. So are mutually (co)recursive (co)datatypes. *)
    1.12 +          fun is_same_fp s =
    1.13 +            (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
    1.14 +              SOME {fp = fp', ...} => fp' = fp
    1.15 +            | NONE => false)
    1.16 +          fun is_homogenously_nested_co_recursive (Type (s, Ts)) =
    1.17 +              forall (if is_same_fp s then is_homogenously_nested_co_recursive
    1.18 +                else not o BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs) Ts
    1.19 +            | is_homogenously_nested_co_recursive _ = true
    1.20          in
    1.21 -          if exists (exists (exists is_nested_co_recursive)) ctrXs_Tsss then maybe_typedef ()
    1.22 -          else get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp)
    1.23 +          if forall (forall (forall is_homogenously_nested_co_recursive)) ctrXs_Tsss then
    1.24 +            get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp)
    1.25 +          else
    1.26 +            maybe_typedef ()
    1.27          end
    1.28        else
    1.29          ([], ctxt)