58 |
58 |
59 ML {* print_depth 50 *} |
59 ML {* print_depth 50 *} |
60 |
60 |
61 ML {* |
61 ML {* |
62 fun get_cnstrs dts = |
62 fun get_cnstrs dts = |
63 map (fn (_, _, _, constrs) => constrs) dts |
63 map snd dts |
64 |
64 |
65 fun get_typed_cnstrs dts = |
65 fun get_typed_cnstrs dts = |
66 flat (map (fn (_, bn, _, constrs) => |
66 flat (map (fn ((bn, _, _), constrs) => |
67 (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) |
67 (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) |
68 |
68 |
69 fun get_cnstr_strs dts = |
69 fun get_cnstr_strs dts = |
70 map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) |
70 map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) |
71 |
71 |
92 fun raw_dts ty_ss dts = |
92 fun raw_dts ty_ss dts = |
93 let |
93 let |
94 fun raw_dts_aux1 (bind, tys, _) = |
94 fun raw_dts_aux1 (bind, tys, _) = |
95 (raw_bind bind, map (replace_typ ty_ss) tys, NoSyn) |
95 (raw_bind bind, map (replace_typ ty_ss) tys, NoSyn) |
96 |
96 |
97 fun raw_dts_aux2 (ty_args, bind, _, constrs) = |
97 fun raw_dts_aux2 ((bind, ty_args, _), constrs) = |
98 (ty_args, raw_bind bind, NoSyn, map raw_dts_aux1 constrs) |
98 ((raw_bind bind, ty_args, NoSyn), map raw_dts_aux1 constrs) |
99 in |
99 in |
100 map raw_dts_aux2 dts |
100 map raw_dts_aux2 dts |
101 end |
101 end |
102 |
102 |
103 fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) |
103 fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) |
144 fun define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy = |
144 fun define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy = |
145 let |
145 let |
146 val thy = Local_Theory.exit_global lthy |
146 val thy = Local_Theory.exit_global lthy |
147 val thy_name = Context.theory_name thy |
147 val thy_name = Context.theory_name thy |
148 |
148 |
149 val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts |
149 val dt_names = map (fn ((s, _, _), _) => Binding.name_of s) dts |
150 val dt_full_names = map (Long_Name.qualify thy_name) dt_names |
150 val dt_full_names = map (Long_Name.qualify thy_name) dt_names |
151 val dt_full_names' = add_raws dt_full_names |
151 val dt_full_names' = add_raws dt_full_names |
152 val dts_env = dt_full_names ~~ dt_full_names' |
152 val dts_env = dt_full_names ~~ dt_full_names' |
153 |
153 |
154 val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names |
154 val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names |
331 Local_Theory.note ((Binding.empty, [rsp_attr]), |
331 Local_Theory.note ((Binding.empty, [rsp_attr]), |
332 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
332 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
333 alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 |
333 alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 |
334 |
334 |
335 val _ = trace_msg (K "Defining the quotient types...") |
335 val _ = trace_msg (K "Defining the quotient types...") |
336 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
336 val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts |
337 |
337 |
338 val (qty_infos, lthy7) = |
338 val (qty_infos, lthy7) = |
339 let |
339 let |
340 val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result |
340 val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result |
341 in |
341 in |
525 *} |
525 *} |
526 |
526 |
527 |
527 |
528 section {* Preparing and parsing of the specification *} |
528 section {* Preparing and parsing of the specification *} |
529 |
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 |
530 ML {* |
561 ML {* |
531 (* generates the parsed datatypes and |
562 (* generates the parsed datatypes and |
532 declares the constructors |
563 declares the constructors |
533 *) |
564 *) |
534 fun prepare_dts dt_strs thy = |
565 fun prepare_dts dt_strs thy = |
535 let |
566 let |
536 fun inter_fs_sort thy (a, S) = |
567 val ctxt = Proof_Context.init_global thy |
537 (a, Type.inter_sort (Sign.tsig_of thy) (@{sort fs}, S)) |
568 |> fold (fn ((_, args, _), _) => fold (fn (a, _) => |
538 |
569 Variable.declare_typ (TFree (a, dummyS))) args) dt_strs |
539 fun mk_type tname sorts (cname, cargs, mx) = |
570 |
540 let |
571 val dts = check_specs ctxt (map (parse_spec ctxt) dt_strs) |
541 val full_tname = Sign.full_name thy tname |
|
542 val ty = Type (full_tname, map (TFree o inter_fs_sort thy) sorts) |
|
543 in |
|
544 (cname, cargs ---> ty, mx) |
|
545 end |
|
546 |
|
547 fun prep_constr (cname, cargs, mx, _) (constrs, sorts) = |
|
548 let |
|
549 val (cargs', sorts') = |
|
550 fold_map (Datatype.read_typ thy) (map snd cargs) sorts |
|
551 |>> map (map_type_tfree (TFree o inter_fs_sort thy)) |
|
552 in |
|
553 (constrs @ [(cname, cargs', mx)], sorts') |
|
554 end |
|
555 |
572 |
556 fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) = |
573 fun mk_constr_trms ((tname, tvs, _), constrs) = |
557 let |
574 let |
558 |
575 val full_tname = Sign.full_name thy tname |
559 val (constrs', sorts') = |
576 val ty = Type (full_tname, map TFree tvs) |
560 fold prep_constr constrs ([], sorts) |
577 in |
561 |
578 map (fn (c, tys, mx) => (c, tys ---> ty, mx)) constrs |
562 val constr_trms' = |
579 end |
563 map (mk_type tname (rev sorts')) constrs' |
580 |
564 in |
581 val constr_trms = flat (map mk_constr_trms dts) |
565 (constr_trms @ constr_trms', dts @ [(tvs, tname, mx, constrs')], sorts') |
|
566 end |
|
567 |
|
568 val (constr_trms, dts, sorts) = fold prep_dts dt_strs ([], [], []); |
|
569 in |
582 in |
570 thy |
583 thy |
571 |> Sign.add_consts_i constr_trms |
584 |> Sign.add_consts_i constr_trms |
572 |> pair dts |
585 |> pair dts |
573 end |
586 end |
679 |
692 |
680 ML {* |
693 ML {* |
681 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
694 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
682 let |
695 let |
683 val pre_typs = |
696 val pre_typs = |
684 map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs |
697 map (fn ((tname, tvs, mx), _) => (tname, length tvs, mx)) dt_strs |
685 |
698 |
686 (* this theory is used just for parsing *) |
699 (* this theory is used just for parsing *) |
687 val thy = Proof_Context.theory_of lthy |
700 val thy = Proof_Context.theory_of lthy |
688 val tmp_thy = Theory.copy thy |
701 val tmp_thy = Theory.copy thy |
689 |
702 |
705 local |
718 local |
706 structure P = Parse; |
719 structure P = Parse; |
707 structure S = Scan |
720 structure S = Scan |
708 |
721 |
709 fun triple ((x, y), z) = (x, y, z) |
722 fun triple ((x, y), z) = (x, y, z) |
|
723 fun triple2 ((x, y), z) = (y, x, z) |
710 fun tuple1 ((x, y, z), u) = (x, y, z, u) |
724 fun tuple1 ((x, y, z), u) = (x, y, z, u) |
711 fun tuple2 (((x, y), z), u) = (x, y, u, z) |
725 fun tuple2 (((x, y), z), u) = (x, y, u, z) |
712 fun tuple3 ((x, y), (z, u)) = (x, y, z, u) |
726 fun tuple3 ((x, y), (z, u)) = (x, y, z, u) |
713 in |
727 in |
714 |
728 |