equal
deleted
inserted
replaced
54 val dummy = rec_hds |> forall (fn t => is_Const t orelse |
54 val dummy = rec_hds |> forall (fn t => is_Const t orelse |
55 error ("Datatype set not previously declared as constant: " ^ |
55 error ("Datatype set not previously declared as constant: " ^ |
56 Syntax.string_of_term_global \<^theory>\<open>IFOL\<close> t)); |
56 Syntax.string_of_term_global \<^theory>\<open>IFOL\<close> t)); |
57 val rec_names = (*nat doesn't have to be added*) |
57 val rec_names = (*nat doesn't have to be added*) |
58 \<^const_name>\<open>nat\<close> :: map (#1 o dest_Const) rec_hds |
58 \<^const_name>\<open>nat\<close> :: map (#1 o dest_Const) rec_hds |
59 val u = if co then \<^const>\<open>QUniv.quniv\<close> else \<^const>\<open>Univ.univ\<close> |
59 val u = if co then \<^Const>\<open>QUniv.quniv\<close> else \<^Const>\<open>Univ.univ\<close> |
60 val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) |
60 val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) |
61 (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t |
61 (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t |
62 | _ => I)) con_ty_lists []; |
62 | _ => I)) con_ty_lists []; |
63 in u $ Ind_Syntax.union_params (hd rec_tms, cs) end; |
63 in u $ Ind_Syntax.union_params (hd rec_tms, cs) end; |
64 |
64 |
86 val case_varname = "f"; (*name for case variables*) |
86 val case_varname = "f"; (*name for case variables*) |
87 |
87 |
88 (** Define the constructors **) |
88 (** Define the constructors **) |
89 |
89 |
90 (*The empty tuple is 0*) |
90 (*The empty tuple is 0*) |
91 fun mk_tuple [] = \<^const>\<open>zero\<close> |
91 fun mk_tuple [] = \<^Const>\<open>zero\<close> |
92 | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; |
92 | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; |
93 |
93 |
94 fun mk_inject n k u = Balanced_Tree.access |
94 fun mk_inject n k u = Balanced_Tree.access |
95 {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k; |
95 {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k; |
96 |
96 |
160 |
160 |
161 (** Generating function variables for the recursor definition |
161 (** Generating function variables for the recursor definition |
162 Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
162 Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
163 |
163 |
164 (*a recursive call for x is the application rec`x *) |
164 (*a recursive call for x is the application rec`x *) |
165 val rec_call = \<^const>\<open>apply\<close> $ Free ("rec", \<^typ>\<open>i\<close>); |
165 val rec_call = \<^Const>\<open>apply\<close> $ Free ("rec", \<^typ>\<open>i\<close>); |
166 |
166 |
167 (*look back down the "case args" (which have been reversed) to |
167 (*look back down the "case args" (which have been reversed) to |
168 determine the de Bruijn index*) |
168 determine the de Bruijn index*) |
169 fun make_rec_call ([], _) arg = error |
169 fun make_rec_call ([], _) arg = error |
170 "Internal error in datatype (variable name mismatch)" |
170 "Internal error in datatype (variable name mismatch)" |
229 val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists); |
229 val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists); |
230 |
230 |
231 val recursor_def = |
231 val recursor_def = |
232 Misc_Legacy.mk_defpair |
232 Misc_Legacy.mk_defpair |
233 (recursor_tm, |
233 (recursor_tm, |
234 \<^const>\<open>Univ.Vrecursor\<close> $ |
234 \<^Const>\<open>Univ.Vrecursor\<close> $ |
235 absfree ("rec", \<^typ>\<open>i\<close>) (list_comb (case_const, recursor_cases))); |
235 absfree ("rec", \<^typ>\<open>i\<close>) (list_comb (case_const, recursor_cases))); |
236 |
236 |
237 (* Build the new theory *) |
237 (* Build the new theory *) |
238 |
238 |
239 val need_recursor = (not coind andalso recursor_typ <> case_typ); |
239 val need_recursor = (not coind andalso recursor_typ <> case_typ); |