author | wenzelm |
Sun, 19 Apr 1998 17:01:04 +0200 | |
changeset 4808 | 995bc5bd8319 |
parent 4796 | e70ae8578792 |
child 4876 | 1c502a82bcde |
permissions | -rw-r--r-- |
4082 | 1 |
(* Title: HOL/thy_data.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
4808 | 5 |
HOL theory data: records, datatypes. |
4082 | 6 |
*) |
7 |
||
4127 | 8 |
(*for records*) |
9 |
type record_info = |
|
4572 | 10 |
{args: (string * sort) list, |
11 |
parent: (typ list * string) option, |
|
12 |
fields: (string * typ) list} |
|
4127 | 13 |
|
14 |
(*for datatypes*) |
|
4082 | 15 |
type datatype_info = |
16 |
{case_const: term, |
|
17 |
case_rewrites: thm list, |
|
18 |
constructors: term list, |
|
19 |
induct_tac: string -> int -> tactic, |
|
20 |
nchotomy: thm, |
|
21 |
exhaustion: thm, |
|
22 |
exhaust_tac: string -> int -> tactic, |
|
23 |
case_cong: thm}; |
|
24 |
||
4127 | 25 |
|
4082 | 26 |
signature THY_DATA = |
27 |
sig |
|
4458 | 28 |
val get_records: theory -> record_info Symtab.table |
29 |
val put_records: record_info Symtab.table -> theory -> theory |
|
4105 | 30 |
val get_datatypes_sg: Sign.sg -> datatype_info Symtab.table |
31 |
val get_datatypes: theory -> datatype_info Symtab.table |
|
32 |
val put_datatypes: datatype_info Symtab.table -> theory -> theory |
|
4796 | 33 |
val setup: theory -> theory |
4082 | 34 |
end; |
35 |
||
36 |
structure ThyData: THY_DATA = |
|
37 |
struct |
|
38 |
||
39 |
||
4105 | 40 |
(** datatypes **) |
41 |
||
42 |
(* data kind 'datatypes' *) |
|
4082 | 43 |
|
4784 | 44 |
val datatypesK = "HOL/datatypes"; |
4082 | 45 |
exception DatatypeInfo of datatype_info Symtab.table; |
46 |
||
4105 | 47 |
local |
4491 | 48 |
val empty = DatatypeInfo Symtab.empty; |
4105 | 49 |
|
50 |
fun prep_ext (x as DatatypeInfo _) = x; |
|
51 |
||
52 |
fun merge (DatatypeInfo tab1, DatatypeInfo tab2) = |
|
53 |
DatatypeInfo (Symtab.merge (K true) (tab1, tab2)); |
|
54 |
||
4259 | 55 |
fun print sg (DatatypeInfo tab) = |
56 |
Pretty.writeln (Pretty.strs ("datatypes:" :: |
|
57 |
map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab))); |
|
4105 | 58 |
in |
59 |
val datatypes_thy_data = (datatypesK, (empty, prep_ext, merge, print)); |
|
4127 | 60 |
end; |
61 |
||
62 |
||
63 |
(* get and put datatypes *) |
|
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
64 |
|
4127 | 65 |
fun get_datatypes_sg sg = |
66 |
(case Sign.get_data sg datatypesK of |
|
67 |
DatatypeInfo tab => tab |
|
4796 | 68 |
| _ => type_error datatypesK); |
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
69 |
|
4127 | 70 |
val get_datatypes = get_datatypes_sg o sign_of; |
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
71 |
|
4127 | 72 |
fun put_datatypes tab thy = |
73 |
Theory.put_data (datatypesK, DatatypeInfo tab) thy; |
|
74 |
||
4082 | 75 |
|
76 |
||
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
77 |
(** records **) |
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
78 |
|
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
79 |
(* data kind 'records' *) |
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
80 |
|
4784 | 81 |
val recordsK = "HOL/records"; |
4127 | 82 |
exception Records of record_info Symtab.table; |
83 |
||
84 |
||
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
85 |
(* methods *) |
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
86 |
|
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
87 |
local |
4491 | 88 |
val empty = Records Symtab.empty; |
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
89 |
|
4127 | 90 |
fun prep_ext (x as Records _) = x; |
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
91 |
|
4127 | 92 |
fun merge (Records tab1, Records tab2) = |
93 |
Records (Symtab.merge (K true) (tab1, tab2)); |
|
4105 | 94 |
|
4259 | 95 |
fun print sg (Records tab) = |
4127 | 96 |
let |
4458 | 97 |
fun pretty_parent None = [] |
98 |
| pretty_parent (Some (ts, name)) = |
|
99 |
[Pretty.block ((Sign.pretty_typ sg (Type (name, ts))) :: [Pretty.str (" +")])]; |
|
4329 | 100 |
|
4458 | 101 |
fun pretty_field (c, T) = Pretty.block |
102 |
[Pretty.str (c ^ " :: "), Pretty.brk 1, Pretty.quote (Sign.pretty_typ sg T)]; |
|
4127 | 103 |
|
4458 | 104 |
fun pretty_record (name, {args, parent, fields}) = |
105 |
Pretty.block |
|
106 |
(Pretty.fbreaks |
|
107 |
((Pretty.block |
|
108 |
((Sign.pretty_typ sg (Type (name, map TFree args))) :: |
|
109 |
[Pretty.str " = "])) |
|
110 |
:: pretty_parent parent @ map pretty_field fields)) |
|
4127 | 111 |
in |
112 |
seq (Pretty.writeln o pretty_record) (Symtab.dest tab) |
|
113 |
end; |
|
114 |
in |
|
115 |
val record_thy_data = (recordsK, (empty, prep_ext, merge, print)); |
|
116 |
end; |
|
117 |
||
4082 | 118 |
|
4127 | 119 |
(* get and put records *) |
4082 | 120 |
|
4127 | 121 |
fun get_records thy = |
122 |
(case Theory.get_data thy recordsK of |
|
123 |
Records tab => tab |
|
4796 | 124 |
| _ => type_error recordsK); |
4127 | 125 |
|
126 |
fun put_records tab thy = |
|
127 |
Theory.put_data (recordsK, Records tab) thy; |
|
128 |
||
4082 | 129 |
|
130 |
||
4796 | 131 |
(** theory data setup **) |
4082 | 132 |
|
4796 | 133 |
val setup = Theory.init_data [datatypes_thy_data, record_thy_data]; |
4127 | 134 |
|
4082 | 135 |
|
136 |
end; |