524 end |
524 end |
525 *} |
525 *} |
526 |
526 |
527 |
527 |
528 section {* Preparing and parsing of the specification *} |
528 section {* Preparing and parsing of the specification *} |
|
529 |
|
530 ML {* |
|
531 (* adds the default sort @{sort fs} to nominal specifications *) |
|
532 |
|
533 fun augment_sort thy S = Sign.inter_sort thy (@{sort fs}, S) |
|
534 |
|
535 fun augment_sort_typ thy = |
|
536 map_type_tfree (fn (s, S) => TFree (s, augment_sort thy S)) |
|
537 *} |
|
538 |
529 ML {* |
539 ML {* |
530 (* generates the parsed datatypes and |
540 (* generates the parsed datatypes and declares the constructors *) |
531 declares the constructors |
|
532 *) |
|
533 |
541 |
534 fun prepare_dts dt_strs thy = |
542 fun prepare_dts dt_strs thy = |
535 let |
543 let |
536 fun prep_spec ((tname, tvs, mx), constrs) = |
544 fun prep_spec ((tname, tvs, mx), constrs) = |
537 ((tname, tvs, mx), |
545 ((tname, tvs, mx), constrs |> map (fn (c, atys, mx', _) => (c, map snd atys, mx'))) |
538 constrs |> map (fn (c, Ts, mx', _) => (c, map snd Ts, mx'))) |
|
539 |
|
540 fun mk_constr_trms ((tname, tvs, _), constrs) = |
|
541 let |
|
542 val full_tname = Sign.full_name thy tname |
|
543 val ty = Type (full_tname, map TFree tvs) |
|
544 in |
|
545 map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs |
|
546 end |
|
547 |
546 |
548 val (dts, spec_ctxt) = |
547 val (dts, spec_ctxt) = |
549 Datatype.read_specs (map prep_spec dt_strs) thy |
548 Datatype.read_specs (map prep_spec dt_strs) thy |
550 |
549 |
551 val constr_trms = flat (map mk_constr_trms dts) |
550 fun augment ((tname, tvs, mx), constrs) = |
552 |
551 ((tname, map (apsnd (augment_sort thy)) tvs, mx), |
|
552 constrs |> map (fn (c, tys, mx') => (c, map (augment_sort_typ thy) tys, mx'))) |
|
553 |
|
554 val dts' = map augment dts |
|
555 |
|
556 fun mk_constr_trms ((tname, tvs, _), constrs) = |
|
557 let |
|
558 val ty = Type (Sign.full_name thy tname, map TFree tvs) |
|
559 in |
|
560 map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs |
|
561 end |
|
562 |
|
563 val constr_trms = flat (map mk_constr_trms dts') |
|
564 |
|
565 (* FIXME: local version *) |
553 (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *) |
566 (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *) |
|
567 |
554 val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt) |
568 val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt) |
555 |
569 in |
556 in |
570 (dts', thy') |
557 (dts, thy') |
571 end |
558 end |
572 *} |
559 *} |
573 |
560 |
574 ML {* |
561 ML {* |
575 (* parsing the binding function specifications and *) |
562 (* parsing the binding function specification and *) |
576 (* declaring the function constants *) |
563 (* declaring the functions in the local theory *) |
|
564 fun prepare_bn_funs bn_fun_strs bn_eq_strs thy = |
577 fun prepare_bn_funs bn_fun_strs bn_eq_strs thy = |
565 let |
578 let |
566 val lthy = Named_Target.theory_init thy |
579 val lthy = Named_Target.theory_init thy |
567 |
580 |
568 val ((bn_funs, bn_eqs), lthy') = |
581 val ((bn_funs, bn_eqs), lthy') = |
667 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
680 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
668 let |
681 let |
669 (* this theory is used just for parsing *) |
682 (* this theory is used just for parsing *) |
670 val thy = Proof_Context.theory_of lthy |
683 val thy = Proof_Context.theory_of lthy |
671 |
684 |
672 val (((dts, (bn_funs, bn_eqs)), bclauses), thy') = |
685 val (((dts, (bn_funs, bn_eqs)), bclauses), _) = |
673 thy |
686 thy |
674 |> prepare_dts dt_strs |
687 |> prepare_dts dt_strs |
675 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
688 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
676 ||>> prepare_bclauses dt_strs |
689 ||>> prepare_bclauses dt_strs |
677 |
690 |