78 val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars; |
78 val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars; |
79 val all_infos = Datatype_Data.get_all thy; |
79 val all_infos = Datatype_Data.get_all thy; |
80 val (orig_descr' :: nested_descrs, _) = |
80 val (orig_descr' :: nested_descrs, _) = |
81 Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp; |
81 Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp; |
82 |
82 |
|
83 fun cliquify_descr [] = [] |
|
84 | cliquify_descr [entry] = [[entry]] |
|
85 | cliquify_descr (full_descr as (_, (T_name1, _, _)) :: _) = |
|
86 let |
|
87 val nn = |
|
88 if member (op =) fpT_names T_name1 then |
|
89 nn_fp |
|
90 else |
|
91 (case Symtab.lookup all_infos T_name1 of |
|
92 SOME {descr, ...} => |
|
93 length (filter_out (fn (_, (_, Us, _)) => exists Datatype_Aux.is_rec_type Us) descr) |
|
94 | NONE => raise Fail "unknown old-style datatype"); |
|
95 in |
|
96 chop nn full_descr ||> cliquify_descr |> op :: |
|
97 end; |
|
98 |
83 (* put nested types before the types that nest them, as needed for N2M *) |
99 (* put nested types before the types that nest them, as needed for N2M *) |
84 val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs); |
100 val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs); |
85 val (cliques, descr) = |
101 val (cliques, descr) = |
86 split_list (flat (map_index (fn (i, descr) => map (pair i) descr) descrs)); |
102 split_list (flat (map_index (fn (i, descr) => map (pair i) descr) |
|
103 (maps cliquify_descr descrs))); |
87 |
104 |
88 val dest_dtyp = Datatype_Aux.typ_of_dtyp descr; |
105 val dest_dtyp = Datatype_Aux.typ_of_dtyp descr; |
89 |
106 |
90 val Ts = Datatype_Aux.get_rec_types descr; |
107 val Ts = Datatype_Aux.get_rec_types descr; |
91 val nn = length Ts; |
108 val nn = length Ts; |