122 val add_name: string -> sg -> sg |
122 val add_name: string -> sg -> sg |
123 val data_kinds: data -> string list |
123 val data_kinds: data -> string list |
124 val merge_refs: sg_ref * sg_ref -> sg_ref |
124 val merge_refs: sg_ref * sg_ref -> sg_ref |
125 val merge: sg * sg -> sg |
125 val merge: sg * sg -> sg |
126 val prep_ext: sg -> sg |
126 val prep_ext: sg -> sg |
|
127 val copy: sg -> sg |
127 val nontriv_merge: sg * sg -> sg |
128 val nontriv_merge: sg * sg -> sg |
128 val pre_pure: sg |
129 val pre_pure: sg |
129 val const_of_class: class -> string |
130 val const_of_class: class -> string |
130 val class_of_const: string -> class |
131 val class_of_const: string -> class |
131 end; |
132 end; |
132 |
133 |
133 signature PRIVATE_SIGN = |
134 signature PRIVATE_SIGN = |
134 sig |
135 sig |
135 include SIGN |
136 include SIGN |
136 val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * |
137 val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) * |
137 (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg |
138 (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg |
138 val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a |
139 val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a |
139 val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg |
140 val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg |
140 val print_data: Object.kind -> sg -> unit |
141 val print_data: Object.kind -> sg -> unit |
141 end; |
142 end; |
162 and data = |
163 and data = |
163 Data of |
164 Data of |
164 (Object.kind * (*kind (for authorization)*) |
165 (Object.kind * (*kind (for authorization)*) |
165 (Object.T * (*value*) |
166 (Object.T * (*value*) |
166 ((Object.T -> Object.T) * (*prepare extend method*) |
167 ((Object.T -> Object.T) * (*prepare extend method*) |
|
168 (Object.T -> Object.T) * (*copy method*) |
167 (Object.T * Object.T -> Object.T) * (*merge and prepare extend method*) |
169 (Object.T * Object.T -> Object.T) * (*merge and prepare extend method*) |
168 (sg -> Object.T -> unit)))) (*print method*) |
170 (sg -> Object.T -> unit)))) (*print method*) |
169 Symtab.table |
171 Symtab.table |
170 and sg_ref = |
172 and sg_ref = |
171 SgRef of sg ref option; |
173 SgRef of sg ref option; |
304 fun entry data kind = |
306 fun entry data kind = |
305 (case gen_assoc Object.eq_kind (data, kind) of |
307 (case gen_assoc Object.eq_kind (data, kind) of |
306 None => [] |
308 None => [] |
307 | Some x => [(kind, x)]); |
309 | Some x => [(kind, x)]); |
308 |
310 |
309 fun merge_entries [(kind, (e, mths as (ext, _, _)))] = |
311 fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] = |
310 (kind, (ext e handle _ => err_method "prep_ext" (Object.name_of_kind kind), mths)) |
312 (kind, (ext e handle _ => err_method "prep_ext" (Object.name_of_kind kind), mths)) |
311 | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] = |
313 | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] = |
312 (kind, (mrg (e1, e2) handle _ => err_method "merge" (Object.name_of_kind kind), mths)) |
314 (kind, (mrg (e1, e2) handle _ => err_method "merge" (Object.name_of_kind kind), mths)) |
313 | merge_entries _ = sys_error "merge_entries"; |
315 | merge_entries _ = sys_error "merge_entries"; |
314 |
316 |
315 val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds; |
317 val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds; |
316 val data_idx = map (fn (k, x) => (Object.name_of_kind k, (k, x))) data; |
318 val data_idx = map (fn (k, x) => (Object.name_of_kind k, (k, x))) data; |
319 handle Symtab.DUPS dups => err_inconsistent dups |
321 handle Symtab.DUPS dups => err_inconsistent dups |
320 end; |
322 end; |
321 |
323 |
322 fun prep_ext_data data = merge_data (data, empty_data); |
324 fun prep_ext_data data = merge_data (data, empty_data); |
323 |
325 |
324 fun init_data_sg sg (Data tab) kind e ext mrg prt = |
326 fun init_data_sg sg (Data tab) kind e cp ext mrg prt = |
325 let val name = Object.name_of_kind kind in |
327 let val name = Object.name_of_kind kind in |
326 Data (Symtab.update_new ((name, (kind, (e, (ext, mrg, prt)))), tab)) |
328 Data (Symtab.update_new ((name, (kind, (e, (cp, ext, mrg, prt)))), tab)) |
327 handle Symtab.DUP _ => err_dup_init sg name |
329 handle Symtab.DUP _ => err_dup_init sg name |
328 end; |
330 end; |
329 |
331 |
330 |
332 |
331 (* access data *) |
333 (* access data *) |
344 fun get_data kind f (sg as Sg (_, {data = Data tab, ...})) = |
346 fun get_data kind f (sg as Sg (_, {data = Data tab, ...})) = |
345 let val x = fst (lookup_data sg tab kind) |
347 let val x = fst (lookup_data sg tab kind) |
346 in f x handle Match => Object.kind_error kind end; |
348 in f x handle Match => Object.kind_error kind end; |
347 |
349 |
348 fun print_data kind (sg as Sg (_, {data = Data tab, ...})) = |
350 fun print_data kind (sg as Sg (_, {data = Data tab, ...})) = |
349 let val (e, (_, _, prt)) = lookup_data sg tab kind |
351 let val (e, (_, _, _, prt)) = lookup_data sg tab kind |
350 in prt sg e handle _ => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) end; |
352 in prt sg e handle _ => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) end; |
351 |
353 |
352 fun put_data_sg sg (Data tab) kind f x = |
354 fun put_data_sg sg (Data tab) kind f x = |
353 Data (Symtab.update ((Object.name_of_kind kind, |
355 Data (Symtab.update ((Object.name_of_kind kind, |
354 (kind, (f x, snd (lookup_data sg tab kind)))), tab)); |
356 (kind, (f x, snd (lookup_data sg tab kind)))), tab)); |
901 (syn, tsig, ctab, (path, add_names spaces kind names), data); |
903 (syn, tsig, ctab, (path, add_names spaces kind names), data); |
902 |
904 |
903 |
905 |
904 (* signature data *) |
906 (* signature data *) |
905 |
907 |
906 fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) = |
908 fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) = |
907 (syn, tsig, ctab, names, init_data_sg sg data kind e ext mrg prt); |
909 (syn, tsig, ctab, names, init_data_sg sg data kind e cp ext mrg prt); |
908 |
910 |
909 fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) = |
911 fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) = |
910 (syn, tsig, ctab, names, put_data_sg sg data kind f x); |
912 (syn, tsig, ctab, names, put_data_sg sg data kind f x); |
|
913 |
|
914 |
|
915 fun copy_data (k, (e, mths as (cp, _, _, _))) = |
|
916 (k, (cp e handle _ => err_method "copy" (Object.name_of_kind k), mths)); |
|
917 |
|
918 fun copy (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) = |
|
919 let |
|
920 val _ = check_stale sg; |
|
921 val self' = SgRef (Some (ref sg)); |
|
922 val Data tab = data; |
|
923 val data' = Data (Symtab.map copy_data tab); |
|
924 in create_sign self' stamps "#" (syn, tsig, const_tab, (path, spaces), data') end; |
911 |
925 |
912 |
926 |
913 (* the external interfaces *) |
927 (* the external interfaces *) |
914 |
928 |
915 val add_classes = extend_sign true (ext_classes true) "#"; |
929 val add_classes = extend_sign true (ext_classes true) "#"; |