85 |
87 |
86 datatype data = Data of |
88 datatype data = Data of |
87 {is_body: bool, (*inner body mode*) |
89 {is_body: bool, (*inner body mode*) |
88 names: Name.context, (*type/term variable names*) |
90 names: Name.context, (*type/term variable names*) |
89 consts: string Symtab.table, (*consts within the local scope*) |
91 consts: string Symtab.table, (*consts within the local scope*) |
|
92 bounds: int * ((string * typ) * string) list, (*next index, internal name, type, external name*) |
90 fixes: fixes, (*term fixes -- global name space, intern ~> extern*) |
93 fixes: fixes, (*term fixes -- global name space, intern ~> extern*) |
91 binds: (typ * term) Vartab.table, (*term bindings*) |
94 binds: (typ * term) Vartab.table, (*term bindings*) |
92 type_occs: string list Symtab.table, (*type variables -- possibly within term variables*) |
95 type_occs: string list Symtab.table, (*type variables -- possibly within term variables*) |
93 maxidx: int, (*maximum var index*) |
96 maxidx: int, (*maximum var index*) |
94 sorts: sort Ord_List.T, (*declared sort occurrences*) |
97 sorts: sort Ord_List.T, (*declared sort occurrences*) |
95 constraints: |
98 constraints: |
96 typ Vartab.table * (*type constraints*) |
99 typ Vartab.table * (*type constraints*) |
97 sort Vartab.table}; (*default sorts*) |
100 sort Vartab.table}; (*default sorts*) |
98 |
101 |
99 fun make_data (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) = |
102 fun make_data |
100 Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds, |
103 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) = |
101 type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; |
104 Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes, |
|
105 binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; |
102 |
106 |
103 structure Data = Proof_Data |
107 structure Data = Proof_Data |
104 ( |
108 ( |
105 type T = data; |
109 type T = data; |
106 fun init _ = |
110 fun init _ = |
107 make_data (false, Name.context, Symtab.empty, empty_fixes, Vartab.empty, |
111 make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, |
108 Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); |
112 Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); |
109 ); |
113 ); |
110 |
114 |
111 fun map_data f = |
115 fun map_data f = |
112 Data.map (fn Data {is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints} => |
116 Data.map (fn |
113 make_data (f (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints))); |
117 Data {is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} => |
|
118 make_data |
|
119 (f (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints))); |
114 |
120 |
115 fun map_names f = |
121 fun map_names f = |
116 map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => |
122 map_data (fn |
117 (is_body, f names, consts, fixes, binds, type_occs, maxidx, sorts, constraints)); |
123 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
|
124 (is_body, f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); |
118 |
125 |
119 fun map_consts f = |
126 fun map_consts f = |
120 map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => |
127 map_data (fn |
121 (is_body, names, f consts, fixes, binds, type_occs, maxidx, sorts, constraints)); |
128 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
|
129 (is_body, names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); |
|
130 |
|
131 fun map_bounds f = |
|
132 map_data (fn |
|
133 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
|
134 (is_body, names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); |
122 |
135 |
123 fun map_fixes f = |
136 fun map_fixes f = |
124 map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => |
137 map_data (fn |
125 (is_body, names, consts, f fixes, binds, type_occs, maxidx, sorts, constraints)); |
138 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
|
139 (is_body, names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints)); |
126 |
140 |
127 fun map_binds f = |
141 fun map_binds f = |
128 map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => |
142 map_data (fn |
129 (is_body, names, consts, fixes, f binds, type_occs, maxidx, sorts, constraints)); |
143 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
|
144 (is_body, names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints)); |
130 |
145 |
131 fun map_type_occs f = |
146 fun map_type_occs f = |
132 map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => |
147 map_data (fn |
133 (is_body, names, consts, fixes, binds, f type_occs, maxidx, sorts, constraints)); |
148 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
|
149 (is_body, names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints)); |
134 |
150 |
135 fun map_maxidx f = |
151 fun map_maxidx f = |
136 map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => |
152 map_data (fn |
137 (is_body, names, consts, fixes, binds, type_occs, f maxidx, sorts, constraints)); |
153 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
|
154 (is_body, names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints)); |
138 |
155 |
139 fun map_sorts f = |
156 fun map_sorts f = |
140 map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => |
157 map_data (fn |
141 (is_body, names, consts, fixes, binds, type_occs, maxidx, f sorts, constraints)); |
158 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
|
159 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints)); |
142 |
160 |
143 fun map_constraints f = |
161 fun map_constraints f = |
144 map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => |
162 map_data (fn |
145 (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, f constraints)); |
163 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
|
164 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints)); |
146 |
165 |
147 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); |
166 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); |
148 |
167 |
149 val is_body = #is_body o rep_data; |
168 val is_body = #is_body o rep_data; |
150 |
169 |
151 fun set_body b = |
170 fun set_body b = |
152 map_data (fn (_, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => |
171 map_data (fn (_, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => |
153 (b, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints)); |
172 (b, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); |
154 |
173 |
155 fun restore_body ctxt = set_body (is_body ctxt); |
174 fun restore_body ctxt = set_body (is_body ctxt); |
156 |
175 |
157 val names_of = #names o rep_data; |
176 val names_of = #names o rep_data; |
158 val fixes_of = #fixes o rep_data; |
177 val fixes_of = #fixes o rep_data; |