equal
deleted
inserted
replaced
11 val indexify_names: string list -> string list |
11 val indexify_names: string list -> string list |
12 val make_tnames: typ list -> string list |
12 val make_tnames: typ list -> string list |
13 val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list |
13 val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list |
14 val make_ind : DatatypeAux.descr list -> (string * sort) list -> term |
14 val make_ind : DatatypeAux.descr list -> (string * sort) list -> term |
15 val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list |
15 val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list |
|
16 val make_primrec_Ts : DatatypeAux.descr list -> (string * sort) list -> |
|
17 string list -> typ list * typ list |
16 val make_primrecs : string list -> DatatypeAux.descr list -> |
18 val make_primrecs : string list -> DatatypeAux.descr list -> |
17 (string * sort) list -> theory -> term list |
19 (string * sort) list -> theory -> term list |
18 val make_cases : string list -> DatatypeAux.descr list -> |
20 val make_cases : string list -> DatatypeAux.descr list -> |
19 (string * sort) list -> theory -> term list list |
21 (string * sort) list -> theory -> term list list |
20 val make_distincts : string list -> DatatypeAux.descr list -> |
22 val make_distincts : string list -> DatatypeAux.descr list -> |
150 ((hd descr) ~~ take (length (hd descr), get_rec_types descr' sorts)) |
152 ((hd descr) ~~ take (length (hd descr), get_rec_types descr' sorts)) |
151 end; |
153 end; |
152 |
154 |
153 (*************** characteristic equations for primrec combinator **************) |
155 (*************** characteristic equations for primrec combinator **************) |
154 |
156 |
155 fun make_primrecs new_type_names descr sorts thy = |
157 fun make_primrec_Ts descr sorts used = |
156 let |
158 let |
157 val sign = Theory.sign_of thy; |
159 val descr' = flat descr; |
158 |
|
159 val descr' = flat descr; |
|
160 val recTs = get_rec_types descr' sorts; |
|
161 val used = foldr add_typ_tfree_names (recTs, []); |
|
162 |
160 |
163 val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~ |
161 val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~ |
164 replicate (length descr') HOLogic.typeS); |
162 replicate (length descr') HOLogic.typeS); |
165 |
163 |
166 val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) => |
164 val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) => |
173 binder_types T ---> nth_elem (body_index dt, rec_result_Ts); |
171 binder_types T ---> nth_elem (body_index dt, rec_result_Ts); |
174 |
172 |
175 val argTs = Ts @ map mk_argT recs |
173 val argTs = Ts @ map mk_argT recs |
176 in argTs ---> nth_elem (i, rec_result_Ts) |
174 in argTs ---> nth_elem (i, rec_result_Ts) |
177 end) constrs) descr'); |
175 end) constrs) descr'); |
|
176 |
|
177 in (rec_result_Ts, reccomb_fn_Ts) end; |
|
178 |
|
179 fun make_primrecs new_type_names descr sorts thy = |
|
180 let |
|
181 val sign = Theory.sign_of thy; |
|
182 |
|
183 val descr' = flat descr; |
|
184 val recTs = get_rec_types descr' sorts; |
|
185 val used = foldr add_typ_tfree_names (recTs, []); |
|
186 |
|
187 val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used; |
178 |
188 |
179 val rec_fns = map (uncurry (mk_Free "f")) |
189 val rec_fns = map (uncurry (mk_Free "f")) |
180 (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts))); |
190 (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts))); |
181 |
191 |
182 val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec"; |
192 val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec"; |