equal
deleted
inserted
replaced
39 (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- |
39 (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- |
40 (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple |
40 (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple |
41 |
41 |
42 (* binding function parser *) |
42 (* binding function parser *) |
43 val bnfun_parser = |
43 val bnfun_parser = |
44 S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) |
44 S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], []) |
45 |
45 |
46 (* main parser *) |
46 (* main parser *) |
47 val main_parser = |
47 val main_parser = |
48 (P.and_list1 dt_parser) -- bnfun_parser >> triple2 |
48 P.and_list1 dt_parser -- bnfun_parser >> triple2 |
49 |
49 |
50 end |
50 end |
51 *} |
51 *} |
52 |
52 |
53 ML {* |
53 ML {* |
91 val conf = Datatype.default_config |
91 val conf = Datatype.default_config |
92 in |
92 in |
93 Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts) |
93 Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts) |
94 end |
94 end |
95 *} |
95 *} |
|
96 |
|
97 |
|
98 text {* Infrastructure for adding "_raw" to types and terms *} |
96 |
99 |
97 ML {* |
100 ML {* |
98 fun add_raw s = s ^ "_raw" |
101 fun add_raw s = s ^ "_raw" |
99 fun add_raws ss = map add_raw ss |
102 fun add_raws ss = map add_raw ss |
100 fun raw_bind bn = Binding.suffix_name "_raw" bn |
103 fun raw_bind bn = Binding.suffix_name "_raw" bn |
252 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
255 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
253 |
256 |
254 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
257 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
255 |
258 |
256 val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) |
259 val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) |
257 |
|
258 in |
260 in |
259 lthy |
261 lthy |
260 |> add_datatype_wrapper raw_dt_names raw_dts |
262 |> add_datatype_wrapper raw_dt_names raw_dts |
261 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
263 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
262 ||>> pair raw_bclauses |
264 ||>> pair raw_bclauses |
422 |
424 |
423 ML {* |
425 ML {* |
424 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
426 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
425 let |
427 let |
426 fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) |
428 fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) |
427 |
|
428 val lthy0 = |
429 val lthy0 = |
429 Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy |
430 Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy |
430 val (dts, lthy1) = |
431 val (dts, lthy1) = prepare_dts dt_strs lthy0 |
431 prepare_dts dt_strs lthy0 |
432 val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 |
432 val ((bn_funs, bn_eqs), lthy2) = |
|
433 prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 |
|
434 val bclauses = prepare_bclauses dt_strs lthy2 |
433 val bclauses = prepare_bclauses dt_strs lthy2 |
435 val bclauses' = complete dt_strs bclauses |
434 val bclauses' = complete dt_strs bclauses |
436 in |
435 in |
437 nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd |
436 nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd |
438 end |
437 end |
493 |
492 |
494 typ exp_raw |
493 typ exp_raw |
495 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
494 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
496 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
495 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
497 |
496 |
498 text {* |
497 |
499 Why does it take so long to define the nominal |
498 |
500 datatype? Is it the function definitions? |
499 end |
501 |
500 |
502 *} |
501 |
503 |
502 |
504 |
|
505 end |
|
506 |
|
507 |
|
508 |
|