1 (* Title: HOL/thy_data.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 HOL theory data: datatypes. |
|
6 *) |
|
7 |
|
8 type datatype_info = |
|
9 {case_const: term, |
|
10 case_rewrites: thm list, |
|
11 constructors: term list, |
|
12 induct_tac: string -> int -> tactic, |
|
13 nchotomy: thm, |
|
14 exhaustion: thm, |
|
15 exhaust_tac: string -> int -> tactic, |
|
16 case_cong: thm}; |
|
17 |
|
18 |
|
19 signature THY_DATA = |
|
20 sig |
|
21 val get_datatypes_sg: Sign.sg -> datatype_info Symtab.table |
|
22 val get_datatypes: theory -> datatype_info Symtab.table |
|
23 val put_datatypes: datatype_info Symtab.table -> theory -> theory |
|
24 val setup: (theory -> theory) list |
|
25 end; |
|
26 |
|
27 structure ThyData: THY_DATA = |
|
28 struct |
|
29 |
|
30 |
|
31 (* data kind 'HOL/datatypes' *) |
|
32 |
|
33 structure DatatypesArgs = |
|
34 struct |
|
35 val name = "HOL/datatypes"; |
|
36 type T = datatype_info Symtab.table; |
|
37 |
|
38 val empty = Symtab.empty; |
|
39 val prep_ext = I; |
|
40 val merge: T * T -> T = Symtab.merge (K true); |
|
41 |
|
42 fun print sg tab = |
|
43 Pretty.writeln (Pretty.strs ("datatypes:" :: |
|
44 map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab))); |
|
45 end; |
|
46 |
|
47 structure DatatypesData = TheoryDataFun(DatatypesArgs); |
|
48 val get_datatypes_sg = DatatypesData.get_sg; |
|
49 val get_datatypes = DatatypesData.get; |
|
50 val put_datatypes = DatatypesData.put; |
|
51 |
|
52 |
|
53 (* setup *) |
|
54 |
|
55 val setup = [DatatypesData.init]; |
|
56 |
|
57 |
|
58 end; |
|