author | narasche |
Fri, 19 Dec 1997 13:30:21 +0100 | |
changeset 4458 | ad8be126603d |
parent 4329 | 9d99bfdd7441 |
child 4491 | 34a53d0c8e8d |
permissions | -rw-r--r-- |
4082 | 1 |
(* Title: HOL/thy_data.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
4127 | 5 |
HOL theory data: simpset, claset, records, datatypes. |
4082 | 6 |
*) |
7 |
||
4127 | 8 |
(*for records*) |
9 |
type record_info = |
|
4458 | 10 |
{args: (string * sort) list, |
4329 | 11 |
parent: (typ list * string) option, |
4458 | 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 |
|
4127 | 33 |
val hol_data: (string * (object * (object -> object) * |
4259 | 34 |
(object * object -> object) * (Sign.sg -> object -> unit))) list |
4082 | 35 |
end; |
36 |
||
37 |
structure ThyData: THY_DATA = |
|
38 |
struct |
|
39 |
||
40 |
||
4105 | 41 |
(** datatypes **) |
42 |
||
43 |
(* data kind 'datatypes' *) |
|
4082 | 44 |
|
45 |
val datatypesK = "datatypes"; |
|
46 |
exception DatatypeInfo of datatype_info Symtab.table; |
|
47 |
||
4105 | 48 |
local |
49 |
val empty = DatatypeInfo Symtab.null; |
|
50 |
||
51 |
fun prep_ext (x as DatatypeInfo _) = x; |
|
52 |
||
53 |
fun merge (DatatypeInfo tab1, DatatypeInfo tab2) = |
|
54 |
DatatypeInfo (Symtab.merge (K true) (tab1, tab2)); |
|
55 |
||
4259 | 56 |
fun print sg (DatatypeInfo tab) = |
57 |
Pretty.writeln (Pretty.strs ("datatypes:" :: |
|
58 |
map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab))); |
|
4105 | 59 |
in |
60 |
val datatypes_thy_data = (datatypesK, (empty, prep_ext, merge, print)); |
|
4127 | 61 |
end; |
62 |
||
63 |
||
64 |
(* get and put datatypes *) |
|
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
65 |
|
4127 | 66 |
fun get_datatypes_sg sg = |
67 |
(case Sign.get_data sg datatypesK of |
|
68 |
DatatypeInfo tab => tab |
|
69 |
| _ => sys_error "get_datatypes_sg"); |
|
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
70 |
|
4127 | 71 |
val get_datatypes = get_datatypes_sg o sign_of; |
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
72 |
|
4127 | 73 |
fun put_datatypes tab thy = |
74 |
Theory.put_data (datatypesK, DatatypeInfo tab) thy; |
|
75 |
||
4082 | 76 |
|
77 |
||
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
78 |
(** records **) |
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
79 |
|
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
80 |
(* data kind 'records' *) |
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
81 |
|
4127 | 82 |
val recordsK = "records"; |
83 |
exception Records of record_info Symtab.table; |
|
84 |
||
85 |
||
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
86 |
(* methods *) |
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
87 |
|
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
88 |
local |
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
89 |
val empty = Records Symtab.null; |
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
90 |
|
4127 | 91 |
fun prep_ext (x as Records _) = x; |
4120
57c1e7d70960
data kinds 'datatypes', data kinds 'records' added
narasche
parents:
4105
diff
changeset
|
92 |
|
4127 | 93 |
fun merge (Records tab1, Records tab2) = |
94 |
Records (Symtab.merge (K true) (tab1, tab2)); |
|
4105 | 95 |
|
4259 | 96 |
fun print sg (Records tab) = |
4127 | 97 |
let |
4458 | 98 |
fun pretty_parent None = [] |
99 |
| pretty_parent (Some (ts, name)) = |
|
100 |
[Pretty.block ((Sign.pretty_typ sg (Type (name, ts))) :: [Pretty.str (" +")])]; |
|
4329 | 101 |
|
4458 | 102 |
fun pretty_field (c, T) = Pretty.block |
103 |
[Pretty.str (c ^ " :: "), Pretty.brk 1, Pretty.quote (Sign.pretty_typ sg T)]; |
|
4127 | 104 |
|
4458 | 105 |
fun pretty_record (name, {args, parent, fields}) = |
106 |
Pretty.block |
|
107 |
(Pretty.fbreaks |
|
108 |
((Pretty.block |
|
109 |
((Sign.pretty_typ sg (Type (name, map TFree args))) :: |
|
110 |
[Pretty.str " = "])) |
|
111 |
:: pretty_parent parent @ map pretty_field fields)) |
|
4127 | 112 |
in |
113 |
seq (Pretty.writeln o pretty_record) (Symtab.dest tab) |
|
114 |
end; |
|
115 |
in |
|
116 |
val record_thy_data = (recordsK, (empty, prep_ext, merge, print)); |
|
117 |
end; |
|
118 |
||
4082 | 119 |
|
4127 | 120 |
(* get and put records *) |
4082 | 121 |
|
4127 | 122 |
fun get_records thy = |
123 |
(case Theory.get_data thy recordsK of |
|
124 |
Records tab => tab |
|
125 |
| _ => sys_error "get_records"); |
|
126 |
||
127 |
fun put_records tab thy = |
|
128 |
Theory.put_data (recordsK, Records tab) thy; |
|
129 |
||
4082 | 130 |
|
131 |
||
132 |
(** hol_data **) |
|
133 |
||
134 |
val hol_data = |
|
4259 | 135 |
[Simplifier.simpset_thy_data, |
136 |
ClasetThyData.thy_data, |
|
4127 | 137 |
datatypes_thy_data, |
138 |
record_thy_data]; |
|
139 |
||
4082 | 140 |
|
141 |
end; |