145 |
145 |
146 ML {* |
146 ML {* |
147 fun rawify_binds dts_env cnstrs_env bn_fun_env binds = |
147 fun rawify_binds dts_env cnstrs_env bn_fun_env binds = |
148 map (map (map (map (fn (opt_trm, i, j) => |
148 map (map (map (map (fn (opt_trm, i, j) => |
149 (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds |
149 (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds |
|
150 *} |
|
151 |
|
152 ML {* |
|
153 fun prep_bn dt_names eqs lthy = |
|
154 let |
|
155 fun aux eq = |
|
156 let |
|
157 val (lhs, rhs) = eq |
|
158 |> strip_qnt_body "all" |
|
159 |> HOLogic.dest_Trueprop |
|
160 |> HOLogic.dest_eq |
|
161 val (head, [cnstr]) = strip_comb lhs |
|
162 val (_, ty) = dest_Free head |
|
163 val (ty_name, _) = dest_Type (domain_type ty) |
|
164 val dt_index = find_index (fn x => x = ty_name) dt_names |
|
165 val (_, cnstr_args) = strip_comb cnstr |
|
166 val included = map (fn i => length (cnstr_args) - i - 1) (loose_bnos rhs) |
|
167 in |
|
168 (head, dt_index, included) |
|
169 end |
|
170 in |
|
171 map aux eqs |
|
172 end |
150 *} |
173 *} |
151 |
174 |
152 ML {* |
175 ML {* |
153 fun add_primrec_wrapper funs eqs lthy = |
176 fun add_primrec_wrapper funs eqs lthy = |
154 if null funs then (([], []), lthy) |
177 if null funs then (([], []), lthy) |
197 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
220 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
198 |
221 |
199 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
222 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
200 |
223 |
201 val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds |
224 val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds |
|
225 |
|
226 val raw_bns = prep_bn dt_full_names' (map snd raw_bn_eqs) lthy |
|
227 |
|
228 val _ = tracing (cat_lines (map PolyML.makestring raw_bns)) |
202 in |
229 in |
203 lthy |
230 lthy |
204 |> add_datatype_wrapper raw_dt_names raw_dts |
231 |> add_datatype_wrapper raw_dt_names raw_dts |
205 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
232 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
206 ||>> pair raw_binds |
233 ||>> pair raw_binds |
|
234 ||>> pair raw_bns |
207 end |
235 end |
208 *} |
236 *} |
209 |
237 |
210 ML {* add_primrec_wrapper *} |
238 ML {* add_primrec_wrapper *} |
211 |
239 |
228 ML {* |
256 ML {* |
229 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
257 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
230 let |
258 let |
231 val thy = ProofContext.theory_of lthy |
259 val thy = ProofContext.theory_of lthy |
232 val thy_name = Context.theory_name thy |
260 val thy_name = Context.theory_name thy |
233 val (((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), lthy2) = |
261 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
234 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
262 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
235 val bn_funs_decls = []; |
263 val bn_funs_decls = []; |
236 |
264 |
237 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
265 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
238 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
266 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
390 ML {* |
418 ML {* |
391 (* parsing the binding function specification and *) |
419 (* parsing the binding function specification and *) |
392 (* declaring the functions in the local theory *) |
420 (* declaring the functions in the local theory *) |
393 fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy = |
421 fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy = |
394 let |
422 let |
395 fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) |
|
396 |
|
397 val ((bn_funs, bn_eqs), _) = |
423 val ((bn_funs, bn_eqs), _) = |
398 Specification.read_spec bn_fun_strs bn_eq_strs lthy |
424 Specification.read_spec bn_fun_strs bn_eq_strs lthy |
399 |
425 |
|
426 fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) |
400 val bn_funs' = map prep_bn_fun bn_funs |
427 val bn_funs' = map prep_bn_fun bn_funs |
401 in |
428 in |
402 lthy |
429 lthy |
403 |> Local_Theory.theory (Sign.add_consts_i bn_funs') |
430 |> Local_Theory.theory (Sign.add_consts_i bn_funs') |
404 |> pair (bn_funs', bn_eqs) |
431 |> pair (bn_funs', bn_eqs) |
464 ML {* |
491 ML {* |
465 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
492 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
466 let |
493 let |
467 fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) |
494 fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) |
468 |
495 |
469 val ((dts, (bn_fun, bn_eq)), binds) = |
496 val lthy0 = |
470 lthy |
497 Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy |
471 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
498 val (dts, lthy1) = |
472 |> prepare_dts dt_strs |
499 prepare_dts dt_strs lthy0 |
473 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
500 val ((bn_funs, bn_eqs), lthy2) = |
474 ||> prepare_binds dt_strs |
501 prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 |
475 |
502 val binds = prepare_binds dt_strs lthy2 |
476 in |
503 in |
477 nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd |
504 nominal_datatype2 dts bn_funs bn_eqs binds lthy |> snd |
478 end |
505 end |
479 *} |
506 *} |
480 |
507 |
481 |
508 |
482 (* Command Keyword *) |
509 (* Command Keyword *) |