1 (* Title: HOL/Tools/datatype_package.ML |
1 (* Title: HOL/Tools/datatype_package.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer |
3 Author: Stefan Berghofer |
4 Copyright 1998 TU Muenchen |
4 Copyright 1998 TU Muenchen |
5 |
5 |
6 Datatype package for Isabelle/HOL |
6 Datatype package for Isabelle/HOL. |
|
7 |
|
8 TODO: |
|
9 - streamline internal interfaces (!??); |
|
10 - rep_datatype outer syntax ('and' vs. ',' (!?)); |
|
11 - methods: induct, exhaust; |
7 *) |
12 *) |
|
13 |
|
14 signature BASIC_DATATYPE_PACKAGE = |
|
15 sig |
|
16 val mutual_induct_tac : string list -> int -> tactic |
|
17 val induct_tac : string -> int -> tactic |
|
18 val exhaust_tac : string -> int -> tactic |
|
19 end; |
8 |
20 |
9 signature DATATYPE_PACKAGE = |
21 signature DATATYPE_PACKAGE = |
10 sig |
22 sig |
|
23 include BASIC_DATATYPE_PACKAGE |
11 val quiet_mode : bool ref |
24 val quiet_mode : bool ref |
12 val add_datatype : bool -> string list -> (string list * bstring * mixfix * |
25 val add_datatype : bool -> string list -> (string list * bstring * mixfix * |
13 (bstring * string list * mixfix) list) list -> theory -> theory * |
26 (bstring * string list * mixfix) list) list -> theory -> theory * |
14 {distinct : thm list list, |
27 {distinct : thm list list, |
15 inject : thm list list, |
28 inject : thm list list, |
40 case_thms : thm list list, |
53 case_thms : thm list list, |
41 split_thms : (thm * thm) list, |
54 split_thms : (thm * thm) list, |
42 induction : thm, |
55 induction : thm, |
43 size : thm list, |
56 size : thm list, |
44 simps : thm list} |
57 simps : thm list} |
45 val setup: (theory -> theory) list |
|
46 val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table |
58 val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table |
47 val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info |
59 val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info |
48 val datatype_info : theory -> string -> DatatypeAux.datatype_info |
60 val datatype_info : theory -> string -> DatatypeAux.datatype_info |
49 val constrs_of : theory -> string -> term list option |
61 val constrs_of : theory -> string -> term list option |
50 val case_const_of : theory -> string -> term option |
62 val case_const_of : theory -> string -> term option |
51 val mutual_induct_tac : string list -> int -> tactic |
63 val setup: (theory -> theory) list |
52 val induct_tac : string -> int -> tactic |
|
53 val exhaust_tac : string -> int -> tactic |
|
54 end; |
64 end; |
55 |
65 |
56 structure DatatypePackage : DATATYPE_PACKAGE = |
66 structure DatatypePackage : DATATYPE_PACKAGE = |
57 struct |
67 struct |
58 |
68 |
59 open DatatypeAux; |
69 open DatatypeAux; |
60 |
70 |
61 val quiet_mode = quiet_mode; |
71 val quiet_mode = quiet_mode; |
|
72 |
62 |
73 |
63 (* data kind 'HOL/datatypes' *) |
74 (* data kind 'HOL/datatypes' *) |
64 |
75 |
65 structure DatatypesArgs = |
76 structure DatatypesArgs = |
66 struct |
77 struct |
79 structure DatatypesData = TheoryDataFun(DatatypesArgs); |
90 structure DatatypesData = TheoryDataFun(DatatypesArgs); |
80 val get_datatypes_sg = DatatypesData.get_sg; |
91 val get_datatypes_sg = DatatypesData.get_sg; |
81 val get_datatypes = DatatypesData.get; |
92 val get_datatypes = DatatypesData.get; |
82 val put_datatypes = DatatypesData.put; |
93 val put_datatypes = DatatypesData.put; |
83 |
94 |
84 (* setup *) |
|
85 |
|
86 val setup = [DatatypesData.init]; |
|
87 |
95 |
88 (** theory information about datatypes **) |
96 (** theory information about datatypes **) |
89 |
97 |
90 fun datatype_info_sg sg name = |
98 fun datatype_info_sg sg name = |
91 (case Symtab.lookup (get_datatypes_sg sg, name) of |
99 (case Symtab.lookup (get_datatypes_sg sg, name) of |
256 val descr' = flat descr; |
264 val descr' = flat descr; |
257 val recTs = get_rec_types descr' sorts; |
265 val recTs = get_rec_types descr' sorts; |
258 val used = foldr add_typ_tfree_names (recTs, []); |
266 val used = foldr add_typ_tfree_names (recTs, []); |
259 val newTs = take (length (hd descr), recTs); |
267 val newTs = take (length (hd descr), recTs); |
260 |
268 |
261 val _ = message ("Adding axioms for datatype(s) " ^ commas new_type_names); |
269 val _ = message ("Adding axioms for datatype(s) " ^ commas_quote new_type_names); |
262 |
270 |
263 (**** declare new types and constants ****) |
271 (**** declare new types and constants ****) |
264 |
272 |
265 val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr); |
273 val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr); |
266 |
274 |
420 |
428 |
421 (******************* definitional introduction of datatypes *******************) |
429 (******************* definitional introduction of datatypes *******************) |
422 |
430 |
423 fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy = |
431 fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy = |
424 let |
432 let |
425 val _ = message ("Proofs for datatype(s) " ^ commas new_type_names); |
433 val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names); |
426 |
434 |
427 val (thy2, inject, dist_rewrites, induct) = thy |> |
435 val (thy2, inject, dist_rewrites, induct) = thy |> |
428 DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts |
436 DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts |
429 types_syntax constr_syntax; |
437 types_syntax constr_syntax; |
430 |
438 |
631 end; |
639 end; |
632 |
640 |
633 val add_datatype_i = gen_add_datatype cert_typ; |
641 val add_datatype_i = gen_add_datatype cert_typ; |
634 val add_datatype = gen_add_datatype read_typ; |
642 val add_datatype = gen_add_datatype read_typ; |
635 |
643 |
|
644 |
|
645 (** package setup **) |
|
646 |
|
647 (* setup theory *) |
|
648 |
|
649 val setup = [DatatypesData.init]; |
|
650 |
|
651 |
|
652 (* outer syntax *) |
|
653 |
|
654 open OuterParse; |
|
655 |
|
656 val datatype_decl = |
|
657 Scan.option ($$$ "(" |-- name --| $$$ ")") -- type_args -- name -- opt_infix -- |
|
658 ($$$ "=" |-- enum1 "|" (name -- Scan.repeat typ -- opt_mixfix)); |
|
659 |
|
660 fun mk_datatype args = |
|
661 let |
|
662 val names = map (fn ((((None, _), t), _), _) => t | ((((Some t, _), _), _), _) => t) args; |
|
663 val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; |
|
664 in #1 o add_datatype false names specs end; |
|
665 |
|
666 val datatypeP = |
|
667 OuterSyntax.parser false "datatype" "define inductive datatypes" |
|
668 (enum1 "and" datatype_decl >> (Toplevel.theory o mk_datatype)); |
|
669 |
|
670 val _ = OuterSyntax.add_keywords ["distinct", "inject", "induct"]; |
|
671 (* FIXME val _ = OuterSyntax.add_parsers [datatypeP, rep_datatypeP]; *) |
|
672 val _ = OuterSyntax.add_parsers [datatypeP]; |
|
673 |
636 end; |
674 end; |
637 |
675 |
638 val induct_tac = DatatypePackage.induct_tac; |
676 structure BasicDatatypePackage: BASIC_DATATYPE_PACKAGE = DatatypePackage; |
639 val mutual_induct_tac = DatatypePackage.mutual_induct_tac; |
677 open BasicDatatypePackage; |
640 val exhaust_tac = DatatypePackage.exhaust_tac; |
|