1 (* Title: ZF/Tools/datatype_package.ML |
1 (* Title: ZF/Tools/datatype_package.ML |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
3 Copyright 1994 University of Cambridge |
5 |
4 |
6 Datatype/Codatatype Definitions |
5 Datatype/Codatatype Definitions |
7 |
6 |
138 :: cases); |
137 :: cases); |
139 |
138 |
140 (*Treatment of a list of constructors, for one part |
139 (*Treatment of a list of constructors, for one part |
141 Result adds a list of terms, each a function variable with arguments*) |
140 Result adds a list of terms, each a function variable with arguments*) |
142 fun add_case_list (con_ty_list, (opno, case_lists)) = |
141 fun add_case_list (con_ty_list, (opno, case_lists)) = |
143 let val (opno', case_list) = foldr add_case (opno, []) con_ty_list |
142 let val (opno', case_list) = List.foldr add_case (opno, []) con_ty_list |
144 in (opno', case_list :: case_lists) end; |
143 in (opno', case_list :: case_lists) end; |
145 |
144 |
146 (*Treatment of all parts*) |
145 (*Treatment of all parts*) |
147 val (_, case_lists) = foldr add_case_list (1,[]) con_ty_lists; |
146 val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists; |
148 |
147 |
149 (*extract the types of all the variables*) |
148 (*extract the types of all the variables*) |
150 val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"}; |
149 val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"}; |
151 |
150 |
152 val case_base_name = big_rec_base_name ^ "_case"; |
151 val case_base_name = big_rec_base_name ^ "_case"; |
182 val ncase_args = length case_args |
181 val ncase_args = length case_args |
183 val bound_args = map Bound ((ncase_args - 1) downto 0) |
182 val bound_args = map Bound ((ncase_args - 1) downto 0) |
184 val rec_args = map (make_rec_call (rev case_args,0)) |
183 val rec_args = map (make_rec_call (rev case_args,0)) |
185 (List.drop(recursor_args, ncase_args)) |
184 (List.drop(recursor_args, ncase_args)) |
186 in |
185 in |
187 foldr add_abs |
186 List.foldr add_abs |
188 (list_comb (recursor_var, |
187 (list_comb (recursor_var, |
189 bound_args @ rec_args)) case_args |
188 bound_args @ rec_args)) case_args |
190 end |
189 end |
191 |
190 |
192 (*Find each recursive argument and add a recursive call for it*) |
191 (*Find each recursive argument and add a recursive call for it*) |
214 end; |
213 end; |
215 |
214 |
216 val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists); |
215 val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists); |
217 |
216 |
218 (*Treatment of all parts*) |
217 (*Treatment of all parts*) |
219 val (_, recursor_lists) = foldr add_case_list (1,[]) rec_ty_lists; |
218 val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists; |
220 |
219 |
221 (*extract the types of all the variables*) |
220 (*extract the types of all the variables*) |
222 val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"}; |
221 val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"}; |
223 |
222 |
224 val recursor_base_name = big_rec_base_name ^ "_rec"; |
223 val recursor_base_name = big_rec_base_name ^ "_rec"; |