# HG changeset patch # User wenzelm # Date 897049773 -7200 # Node ID 28fe46a570d7e219b0231f967314f649f26ea9d4 # Parent 670b0d4fb9a9cdb2f324d1e57319843cbdcc02dc improved data: secure version using Object.T and Object.kind; diff -r 670b0d4fb9a9 -r 28fe46a570d7 src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Jun 05 14:28:08 1998 +0200 +++ b/src/Pure/sign.ML Fri Jun 05 14:29:33 1998 +0200 @@ -122,11 +122,11 @@ val add_space: string * string list -> sg -> sg val add_name: string -> sg -> sg val data_kinds: data -> string list - val init_data: string * (object * (object -> object) * - (object * object -> object) * (sg -> object -> unit)) -> sg -> sg - val get_data: sg -> string -> object - val put_data: string * object -> sg -> sg - val print_data: sg -> string -> unit + val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * + (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg + val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a + val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg + val print_data: Object.kind -> sg -> unit val merge_refs: sg_ref * sg_ref -> sg_ref val merge: sg * sg -> sg val prep_ext: sg -> sg @@ -157,13 +157,14 @@ data: data} (*anytype data*) and data = Data of - (object * (*value*) - ((object -> object) * (*prepare extend method*) - (object * object -> object) * (*merge and prepare extend method*) - (sg -> object -> unit))) (*print method*) + (Object.kind * (*kind (for authorization)*) + (Object.T * (*value*) + ((Object.T -> Object.T) * (*prepare extend method*) + (Object.T * Object.T -> Object.T) * (*merge and prepare extend method*) + (sg -> Object.T -> unit)))) (*print method*) Symtab.table and sg_ref = - SgRef of sg ref option + SgRef of sg ref option; (*make signature*) fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) = @@ -266,6 +267,9 @@ fun of_theory sg = "\nof theory " ^ str_of_sg sg; +fun err_inconsistent kinds = + error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " data"); + fun err_method name kind = error ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method"); @@ -275,6 +279,9 @@ fun err_uninit sg kind = error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg); +fun err_access sg kind = + error ("Unauthorized access to " ^ quote kind ^ " data" ^ of_theory sg); + (* prepare data *) @@ -282,30 +289,36 @@ fun merge_data (Data tab1, Data tab2) = let - val data1 = Symtab.dest tab1; - val data2 = Symtab.dest tab2; + val data1 = map snd (Symtab.dest tab1); + val data2 = map snd (Symtab.dest tab2); val all_data = data1 @ data2; - val kinds = distinct (map fst all_data); + val kinds = gen_distinct Object.eq_kind (map fst all_data); fun entry data kind = - (case assoc (data, kind) of + (case gen_assoc Object.eq_kind (data, kind) of None => [] | Some x => [(kind, x)]); fun merge_entries [(kind, (e, mths as (ext, _, _)))] = - (kind, (ext e handle _ => err_method "prep_ext" kind, mths)) + (kind, (ext e handle _ => err_method "prep_ext" (Object.name_of_kind kind), mths)) | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] = - (kind, (mrg (e1, e2) handle _ => err_method "merge" kind, mths)) + (kind, (mrg (e1, e2) handle _ => err_method "merge" (Object.name_of_kind kind), mths)) | merge_entries _ = sys_error "merge_entries"; val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds; - in Data (Symtab.make data) end; + val data_idx = map (fn (k, x) => (Object.name_of_kind k, (k, x))) data; + in + Data (Symtab.make data_idx) + handle Symtab.DUPS dups => err_inconsistent dups + end; fun prep_ext_data data = merge_data (data, empty_data); fun init_data_sg sg (Data tab) kind e ext mrg prt = - Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab)) - handle Symtab.DUP _ => err_dup_init sg kind; + let val name = Object.name_of_kind kind in + Data (Symtab.update_new ((name, (kind, (e, (ext, mrg, prt)))), tab)) + handle Symtab.DUP _ => err_dup_init sg name + end; (* access data *) @@ -313,19 +326,25 @@ fun data_kinds (Data tab) = map fst (Symtab.dest tab); fun lookup_data sg tab kind = - (case Symtab.lookup (tab, kind) of - Some x => x - | None => err_uninit sg kind); - -fun get_data (sg as Sg (_, {data = Data tab, ...})) kind = - fst (lookup_data sg tab kind); + let val name = Object.name_of_kind kind in + (case Symtab.lookup (tab, name) of + Some (k, x) => + if Object.eq_kind (kind, k) then x + else err_access sg name + | None => err_uninit sg name) + end; -fun print_data (sg as Sg (_, {data = Data tab, ...})) kind = +fun get_data kind f (sg as Sg (_, {data = Data tab, ...})) = + let val x = fst (lookup_data sg tab kind) + in f x handle Match => Object.kind_error kind end; + +fun print_data kind (sg as Sg (_, {data = Data tab, ...})) = let val (e, (_, _, prt)) = lookup_data sg tab kind - in prt sg e handle _ => err_method ("print" ^ of_theory sg) kind end; + in prt sg e handle _ => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) end; -fun put_data_sg sg (Data tab) kind e = - Data (Symtab.update ((kind, (e, snd (lookup_data sg tab kind))), tab)); +fun put_data_sg sg (Data tab) kind f x = + Data (Symtab.update ((Object.name_of_kind kind, + (kind, (f x, snd (lookup_data sg tab kind)))), tab)); @@ -889,41 +908,41 @@ fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) = (syn, tsig, ctab, names, init_data_sg sg data kind e ext mrg prt); -fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, e) = - (syn, tsig, ctab, names, put_data_sg sg data kind e); +fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) = + (syn, tsig, ctab, names, put_data_sg sg data kind f x); (* the external interfaces *) -val add_classes = extend_sign true (ext_classes true) "#"; -val add_classes_i = extend_sign true (ext_classes false) "#"; -val add_classrel = extend_sign true (ext_classrel true) "#"; -val add_classrel_i = extend_sign true (ext_classrel false) "#"; -val add_defsort = extend_sign true (ext_defsort true) "#"; -val add_defsort_i = extend_sign true (ext_defsort false) "#"; -val add_types = extend_sign true ext_types "#"; -val add_nonterminals = extend_sign true ext_nonterminals "#"; -val add_tyabbrs = extend_sign true ext_tyabbrs "#"; -val add_tyabbrs_i = extend_sign true ext_tyabbrs_i "#"; -val add_arities = extend_sign true (ext_arities true) "#"; -val add_arities_i = extend_sign true (ext_arities false) "#"; -val add_consts = extend_sign true ext_consts "#"; -val add_consts_i = extend_sign true ext_consts_i "#"; -val add_syntax = extend_sign true ext_syntax "#"; -val add_syntax_i = extend_sign true ext_syntax_i "#"; -val add_modesyntax = extend_sign true ext_modesyntax "#"; -val add_modesyntax_i = extend_sign true ext_modesyntax_i "#"; -val add_trfuns = extend_sign true (ext_syn Syntax.extend_trfuns) "#"; -val add_trfunsT = extend_sign true (ext_syn Syntax.extend_trfunsT) "#"; -val add_tokentrfuns = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#"; -val add_trrules = extend_sign true ext_trrules "#"; -val add_trrules_i = extend_sign true (ext_syn Syntax.extend_trrules_i) "#"; -val add_path = extend_sign true ext_path "#"; -val add_space = extend_sign true ext_space "#"; -fun init_data arg sg = extend_sign true (ext_init_data sg) "#" arg sg; -fun put_data arg sg = extend_sign true (ext_put_data sg) "#" arg sg; -fun add_name name sg = extend_sign true K name () sg; -fun prep_ext sg = extend_sign false K "#" () sg; +val add_classes = extend_sign true (ext_classes true) "#"; +val add_classes_i = extend_sign true (ext_classes false) "#"; +val add_classrel = extend_sign true (ext_classrel true) "#"; +val add_classrel_i = extend_sign true (ext_classrel false) "#"; +val add_defsort = extend_sign true (ext_defsort true) "#"; +val add_defsort_i = extend_sign true (ext_defsort false) "#"; +val add_types = extend_sign true ext_types "#"; +val add_nonterminals = extend_sign true ext_nonterminals "#"; +val add_tyabbrs = extend_sign true ext_tyabbrs "#"; +val add_tyabbrs_i = extend_sign true ext_tyabbrs_i "#"; +val add_arities = extend_sign true (ext_arities true) "#"; +val add_arities_i = extend_sign true (ext_arities false) "#"; +val add_consts = extend_sign true ext_consts "#"; +val add_consts_i = extend_sign true ext_consts_i "#"; +val add_syntax = extend_sign true ext_syntax "#"; +val add_syntax_i = extend_sign true ext_syntax_i "#"; +val add_modesyntax = extend_sign true ext_modesyntax "#"; +val add_modesyntax_i = extend_sign true ext_modesyntax_i "#"; +val add_trfuns = extend_sign true (ext_syn Syntax.extend_trfuns) "#"; +val add_trfunsT = extend_sign true (ext_syn Syntax.extend_trfunsT) "#"; +val add_tokentrfuns = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#"; +val add_trrules = extend_sign true ext_trrules "#"; +val add_trrules_i = extend_sign true (ext_syn Syntax.extend_trrules_i) "#"; +val add_path = extend_sign true ext_path "#"; +val add_space = extend_sign true ext_space "#"; +fun init_data arg sg = extend_sign true (ext_init_data sg) "#" arg sg; +fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg; +fun add_name name sg = extend_sign true K name () sg; +fun prep_ext sg = extend_sign false K "#" () sg;