52 |
54 |
53 val (unsorted_As, _) = lthy |> mk_TFrees (length var_As); |
55 val (unsorted_As, _) = lthy |> mk_TFrees (length var_As); |
54 val As = map2 (resort_tfree o Type.sort_of_atyp) var_As unsorted_As; |
56 val As = map2 (resort_tfree o Type.sort_of_atyp) var_As unsorted_As; |
55 val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names'; |
57 val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names'; |
56 |
58 |
57 fun add_nested_types_of (T as Type (s, _)) seen = |
59 fun nested_Tindicessss_of parent_Tkks (T as Type (s, _)) kk = |
58 if member (op =) seen T then |
60 (case try lfp_sugar_of s of |
59 seen |
61 SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) => |
60 else if s = @{type_name fun} then |
62 let |
61 (warning "Partial support for recursion through functions -- 'primrec' will fail"; seen) |
63 val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) []; |
62 else |
64 val substT = Term.typ_subst_TVars rho; |
63 (case try lfp_sugar_of s of |
65 val mutual_Ts = map substT mutual_Ts0; |
64 SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) => |
66 val mutual_nn = length mutual_Ts; |
65 let |
67 val mutual_kks = kk upto kk + mutual_nn - 1; |
66 val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) []; |
68 val mutual_Tkks = mutual_Ts ~~ mutual_kks; |
67 val substT = Term.typ_subst_TVars rho; |
|
68 |
69 |
69 val mutual_Ts = map substT mutual_Ts0; |
70 fun Tindices_of_ctr_arg (parent_Tkks as (_, parent_kk) :: _) (U as Type (s, _)) |
|
71 (accum as (Tkssss, kk')) = |
|
72 if s = @{type_name fun} then |
|
73 if exists_subtype_in mutual_Ts U then |
|
74 (warning "Incomplete support for recursion through functions -- \ |
|
75 \'primrec' will fail"; |
|
76 Tindices_of_ctr_arg parent_Tkks (range_type U) accum) |
|
77 else |
|
78 ([], accum) |
|
79 else |
|
80 (case AList.lookup (op =) (parent_Tkks @ mutual_Tkks) U of |
|
81 SOME kk => ([kk], accum) |
|
82 | NONE => |
|
83 if exists_subtype_in mutual_Ts U then |
|
84 ([kk'], nested_Tindicessss_of parent_Tkks U kk' |>> append Tkssss) |
|
85 else |
|
86 ([], accum)) |
|
87 | Tindices_of_ctr_arg _ _ accum = ([], accum); |
70 |
88 |
71 fun add_interesting_subtypes (U as Type (_, Us)) = |
89 fun Tindicesss_of_mutual_type T kk ctr_Tss = |
72 (case filter (exists_subtype_in mutual_Ts) Us of [] => I |
90 fold_map (fold_map (Tindices_of_ctr_arg ((T, kk) :: parent_Tkks))) ctr_Tss |
73 | Us' => insert (op =) U #> fold add_interesting_subtypes Us') |
91 #>> pair T; |
74 | add_interesting_subtypes _ = I; |
|
75 |
92 |
76 val ctrs = maps #ctrs ctr_sugars; |
93 val ctrss = map #ctrs ctr_sugars; |
77 val ctr_Ts = maps (binder_types o substT o fastype_of) ctrs |> distinct (op =); |
94 val ctr_Tsss = map (map (binder_types o substT o fastype_of)) ctrss; |
78 val subTs = fold add_interesting_subtypes ctr_Ts []; |
95 in |
79 in |
96 ([], kk + mutual_nn) |
80 fold add_nested_types_of subTs (seen @ mutual_Ts) |
97 |> fold_map3 Tindicesss_of_mutual_type mutual_Ts mutual_kks ctr_Tsss |
81 end |
98 |> (fn (Tkkssss, (Tkkssss', kk)) => (Tkkssss @ Tkkssss', kk)) |
82 | NONE => error ("Unsupported recursion via type constructor " ^ quote s ^ |
99 end |
83 " not corresponding to new-style datatype (cf. \"datatype_new\")")); |
100 | NONE => error ("Unsupported recursion via type constructor " ^ quote s ^ |
|
101 " not corresponding to new-style datatype (cf. \"datatype_new\")")); |
84 |
102 |
85 val Ts = add_nested_types_of fpT1 []; |
103 fun get_indices (Bound kk) = [kk]; |
|
104 |
|
105 val (Tkkssss, _) = nested_Tindicessss_of [] fpT1 0; |
|
106 val Ts = map fst Tkkssss; |
|
107 val callssss = map (map (map (map Bound)) o snd) Tkkssss; |
|
108 |
86 val b_names = map base_name_of_typ Ts; |
109 val b_names = map base_name_of_typ Ts; |
87 val compat_b_names = map (prefix compatN) b_names; |
110 val compat_b_names = map (prefix compatN) b_names; |
88 val compat_bs = map Binding.name compat_b_names; |
111 val compat_bs = map Binding.name compat_b_names; |
89 val common_name = compatN ^ mk_common_name b_names; |
112 val common_name = compatN ^ mk_common_name b_names; |
90 val nn_fp = length fpTs; |
113 val nn_fp = length fpTs; |
91 val nn = length Ts; |
114 val nn = length Ts; |
92 val get_indices = K []; |
|
93 val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts; |
115 val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts; |
94 val callssss = map (fn fp_sugar0 => indexify_callsss fp_sugar0 []) fp_sugars0; |
|
95 |
116 |
96 val ((fp_sugars, (lfp_sugar_thms, _)), lthy) = |
117 val ((fp_sugars, (lfp_sugar_thms, _)), lthy) = |
97 if nn > nn_fp then |
118 if nn > nn_fp then |
98 mutualize_fp_sugars Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy |
119 mutualize_fp_sugars Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy |
99 else |
120 else |
140 ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); |
161 ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); |
141 |
162 |
142 val notes = |
163 val notes = |
143 [(foldN, fold_thmss, []), |
164 [(foldN, fold_thmss, []), |
144 (inductN, map single induct_thms, induct_attrs), |
165 (inductN, map single induct_thms, induct_attrs), |
145 (recN, rec_thmss, [])] |
166 (recN, rec_thmss, code_nitpicksimp_simp_attrs)] |
146 |> filter_out (null o #2) |
167 |> filter_out (null o #2) |
147 |> maps (fn (thmN, thmss, attrs) => |
168 |> maps (fn (thmN, thmss, attrs) => |
148 if forall null thmss then |
169 if forall null thmss then |
149 [] |
170 [] |
150 else |
171 else |