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 fun parse_spec ctxt ((tname, tvs, mx), constrs) = |
|
532 let |
|
533 val tvs' = map (apsnd (Typedecl.read_constraint ctxt)) tvs |
|
534 val constrs' = constrs |
|
535 |> map (fn (c, Ts, mx', bns) => (c, map ((Syntax.parse_typ ctxt) o snd) Ts, mx')) |
|
536 in |
|
537 ((tname, tvs', mx), constrs') |
|
538 end |
|
539 |
|
540 fun check_specs ctxt specs = |
|
541 let |
|
542 fun prep_spec ((tname, args, mx), constrs) tys = |
|
543 let |
|
544 val (args', tys1) = chop (length args) tys; |
|
545 val (constrs', tys3) = (constrs, tys1) |-> fold_map (fn (cname, cargs, mx') => fn tys2 => |
|
546 let val (cargs', tys3) = chop (length cargs) tys2; |
|
547 in ((cname, cargs', mx'), tys3) end); |
|
548 in |
|
549 (((tname, map dest_TFree args', mx), constrs'), tys3) |
|
550 end |
|
551 |
|
552 val all_tys = |
|
553 specs |> maps (fn ((_, args, _), cs) => map TFree args @ maps #2 cs) |
|
554 |> Syntax.check_typs ctxt; |
|
555 |
|
556 in |
|
557 #1 (fold_map prep_spec specs all_tys) |
|
558 end |
|
559 *} |
|
560 |
|
561 ML {* |
529 ML {* |
562 (* generates the parsed datatypes and |
530 (* generates the parsed datatypes and |
563 declares the constructors |
531 declares the constructors |
564 *) |
532 *) |
|
533 |
565 fun prepare_dts dt_strs thy = |
534 fun prepare_dts dt_strs thy = |
566 let |
535 let |
567 val ctxt = Proof_Context.init_global thy |
536 fun prep_spec ((tname, tvs, mx), constrs) = |
568 |> fold (fn ((_, args, _), _) => fold (fn (a, _) => |
537 ((tname, tvs, mx), |
569 Variable.declare_typ (TFree (a, dummyS))) args) dt_strs |
538 constrs |> map (fn (c, Ts, mx', _) => (c, map snd Ts, mx'))) |
570 |
539 |
571 val dts = check_specs ctxt (map (parse_spec ctxt) dt_strs) |
|
572 |
|
573 fun mk_constr_trms ((tname, tvs, _), constrs) = |
540 fun mk_constr_trms ((tname, tvs, _), constrs) = |
574 let |
541 let |
575 val full_tname = Sign.full_name thy tname |
542 val full_tname = Sign.full_name thy tname |
576 val ty = Type (full_tname, map TFree tvs) |
543 val ty = Type (full_tname, map TFree tvs) |
577 in |
544 in |
578 map (fn (c, tys, mx) => (c, tys ---> ty, mx)) constrs |
545 map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs |
579 end |
546 end |
580 |
547 |
|
548 val (dts, spec_ctxt) = |
|
549 Datatype.read_specs (map prep_spec dt_strs) thy |
|
550 |
581 val constr_trms = flat (map mk_constr_trms dts) |
551 val constr_trms = flat (map mk_constr_trms dts) |
582 in |
552 |
583 thy |
553 (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *) |
584 |> Sign.add_consts_i constr_trms |
554 val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt) |
585 |> pair dts |
555 |
|
556 in |
|
557 (dts, thy') |
586 end |
558 end |
587 *} |
559 *} |
588 |
560 |
589 ML {* |
561 ML {* |
590 (* parsing the binding function specification and *) |
562 (* parsing the binding function specification and *) |
597 Specification.read_spec bn_fun_strs bn_eq_strs lthy |
569 Specification.read_spec bn_fun_strs bn_eq_strs lthy |
598 |
570 |
599 fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) |
571 fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) |
600 |
572 |
601 val bn_funs' = map prep_bn_fun bn_funs |
573 val bn_funs' = map prep_bn_fun bn_funs |
|
574 |
602 in |
575 in |
603 (Local_Theory.exit_global lthy') |
576 (Local_Theory.exit_global lthy') |
604 |> Sign.add_consts_i bn_funs' |
577 |> Sign.add_consts_i bn_funs' |
605 |> pair (bn_funs', bn_eqs) |
578 |> pair (bn_funs', bn_eqs) |
606 end |
579 end |
691 *} |
664 *} |
692 |
665 |
693 ML {* |
666 ML {* |
694 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
667 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
695 let |
668 let |
696 val pre_typs = |
|
697 map (fn ((tname, tvs, mx), _) => (tname, length tvs, mx)) dt_strs |
|
698 |
|
699 (* this theory is used just for parsing *) |
669 (* this theory is used just for parsing *) |
700 val thy = Proof_Context.theory_of lthy |
670 val thy = Proof_Context.theory_of lthy |
701 val tmp_thy = Theory.copy thy |
671 |
702 |
672 val (((dts, (bn_funs, bn_eqs)), bclauses), thy') = |
703 val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = |
673 thy |
704 tmp_thy |
|
705 |> Sign.add_types_global pre_typs |
|
706 |> prepare_dts dt_strs |
674 |> prepare_dts dt_strs |
707 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
675 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
708 ||>> prepare_bclauses dt_strs |
676 ||>> prepare_bclauses dt_strs |
709 |
677 |
710 val bclauses' = complete dt_strs bclauses |
678 val bclauses' = complete dt_strs bclauses |
711 in |
679 in |
712 nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy |
680 nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy |
713 end |
681 end |
714 *} |
682 *} |
715 |
683 |
716 ML {* |
684 ML {* |
717 (* nominal datatype parser *) |
685 (* nominal datatype parser *) |
718 local |
686 local |
719 structure P = Parse; |
687 structure P = Parse; |
720 structure S = Scan |
688 structure S = Scan |
721 |
689 |
722 fun triple ((x, y), z) = (x, y, z) |
690 fun triple1 ((x, y), z) = (x, y, z) |
723 fun triple2 ((x, y), z) = (y, x, z) |
691 fun triple2 ((x, y), z) = (y, x, z) |
724 fun tuple1 ((x, y, z), u) = (x, y, z, u) |
|
725 fun tuple2 (((x, y), z), u) = (x, y, u, z) |
692 fun tuple2 (((x, y), z), u) = (x, y, u, z) |
726 fun tuple3 ((x, y), (z, u)) = (x, y, z, u) |
693 fun tuple3 ((x, y), (z, u)) = (x, y, z, u) |
727 in |
694 in |
728 |
695 |
729 val _ = Keyword.keyword "binds" |
696 val _ = Keyword.keyword "binds" |