src/Pure/sign.ML
changeset 4998 28fe46a570d7
parent 4961 27f559b54c57
child 5175 2dbef0104bcf
     1.1 --- a/src/Pure/sign.ML	Fri Jun 05 14:28:08 1998 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Jun 05 14:29:33 1998 +0200
     1.3 @@ -122,11 +122,11 @@
     1.4    val add_space: string * string list -> sg -> sg
     1.5    val add_name: string -> sg -> sg
     1.6    val data_kinds: data -> string list
     1.7 -  val init_data: string * (object * (object -> object) *
     1.8 -    (object * object -> object) * (sg -> object -> unit)) -> sg -> sg
     1.9 -  val get_data: sg -> string -> object
    1.10 -  val put_data: string * object -> sg -> sg
    1.11 -  val print_data: sg -> string -> unit
    1.12 +  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) *
    1.13 +    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
    1.14 +  val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
    1.15 +  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
    1.16 +  val print_data: Object.kind -> sg -> unit
    1.17    val merge_refs: sg_ref * sg_ref -> sg_ref
    1.18    val merge: sg * sg -> sg
    1.19    val prep_ext: sg -> sg
    1.20 @@ -157,13 +157,14 @@
    1.21      data: data}                                 (*anytype data*)
    1.22  and data =
    1.23    Data of
    1.24 -    (object *                             	(*value*)
    1.25 -     ((object -> object) *                	(*prepare extend method*)
    1.26 -      (object * object -> object) *       	(*merge and prepare extend method*)
    1.27 -      (sg -> object -> unit)))                 	(*print method*)
    1.28 +    (Object.kind *				(*kind (for authorization)*)
    1.29 +      (Object.T *				(*value*)
    1.30 +        ((Object.T -> Object.T) *               (*prepare extend method*)
    1.31 +          (Object.T * Object.T -> Object.T) *   (*merge and prepare extend method*)
    1.32 +          (sg -> Object.T -> unit))))           (*print method*)
    1.33      Symtab.table
    1.34  and sg_ref =
    1.35 -  SgRef of sg ref option
    1.36 +  SgRef of sg ref option;
    1.37  
    1.38  (*make signature*)
    1.39  fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) =
    1.40 @@ -266,6 +267,9 @@
    1.41  
    1.42  fun of_theory sg = "\nof theory " ^ str_of_sg sg;
    1.43  
    1.44 +fun err_inconsistent kinds =
    1.45 +  error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " data");
    1.46 +
    1.47  fun err_method name kind =
    1.48    error ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method");
    1.49  
    1.50 @@ -275,6 +279,9 @@
    1.51  fun err_uninit sg kind =
    1.52    error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
    1.53  
    1.54 +fun err_access sg kind =
    1.55 +  error ("Unauthorized access to " ^ quote kind ^ " data" ^ of_theory sg);
    1.56 +
    1.57  
    1.58  (* prepare data *)
    1.59  
    1.60 @@ -282,30 +289,36 @@
    1.61  
    1.62  fun merge_data (Data tab1, Data tab2) =
    1.63    let
    1.64 -    val data1 = Symtab.dest tab1;
    1.65 -    val data2 = Symtab.dest tab2;
    1.66 +    val data1 = map snd (Symtab.dest tab1);
    1.67 +    val data2 = map snd (Symtab.dest tab2);
    1.68      val all_data = data1 @ data2;
    1.69 -    val kinds = distinct (map fst all_data);
    1.70 +    val kinds = gen_distinct Object.eq_kind (map fst all_data);
    1.71  
    1.72     fun entry data kind =
    1.73 -     (case assoc (data, kind) of
    1.74 +     (case gen_assoc Object.eq_kind (data, kind) of
    1.75         None => []
    1.76       | Some x => [(kind, x)]);
    1.77  
    1.78      fun merge_entries [(kind, (e, mths as (ext, _, _)))] =
    1.79 -          (kind, (ext e handle _ => err_method "prep_ext" kind, mths))
    1.80 +          (kind, (ext e handle _ => err_method "prep_ext" (Object.name_of_kind kind), mths))
    1.81        | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] =
    1.82 -          (kind, (mrg (e1, e2) handle _ => err_method "merge" kind, mths))
    1.83 +          (kind, (mrg (e1, e2) handle _ => err_method "merge" (Object.name_of_kind kind), mths))
    1.84        | merge_entries _ = sys_error "merge_entries";
    1.85  
    1.86      val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
    1.87 -  in Data (Symtab.make data) end;
    1.88 +    val data_idx = map (fn (k, x) => (Object.name_of_kind k, (k, x))) data;
    1.89 +  in
    1.90 +    Data (Symtab.make data_idx)
    1.91 +      handle Symtab.DUPS dups => err_inconsistent dups
    1.92 +  end;
    1.93  
    1.94  fun prep_ext_data data = merge_data (data, empty_data);
    1.95  
    1.96  fun init_data_sg sg (Data tab) kind e ext mrg prt =
    1.97 -  Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab))
    1.98 -    handle Symtab.DUP _ => err_dup_init sg kind;
    1.99 +  let val name = Object.name_of_kind kind in
   1.100 +    Data (Symtab.update_new ((name, (kind, (e, (ext, mrg, prt)))), tab))
   1.101 +      handle Symtab.DUP _ => err_dup_init sg name
   1.102 +  end;
   1.103  
   1.104  
   1.105  (* access data *)
   1.106 @@ -313,19 +326,25 @@
   1.107  fun data_kinds (Data tab) = map fst (Symtab.dest tab);
   1.108  
   1.109  fun lookup_data sg tab kind =
   1.110 -  (case Symtab.lookup (tab, kind) of
   1.111 -    Some x => x
   1.112 -  | None => err_uninit sg kind);
   1.113 -
   1.114 -fun get_data (sg as Sg (_, {data = Data tab, ...})) kind =
   1.115 -  fst (lookup_data sg tab kind);
   1.116 +  let val name = Object.name_of_kind kind in
   1.117 +    (case Symtab.lookup (tab, name) of
   1.118 +      Some (k, x) =>
   1.119 +        if Object.eq_kind (kind, k) then x
   1.120 +        else err_access sg name
   1.121 +    | None => err_uninit sg name)
   1.122 +  end;
   1.123  
   1.124 -fun print_data (sg as Sg (_, {data = Data tab, ...})) kind =
   1.125 +fun get_data kind f (sg as Sg (_, {data = Data tab, ...})) =
   1.126 +  let val x = fst (lookup_data sg tab kind)
   1.127 +  in f x handle Match => Object.kind_error kind end;
   1.128 +
   1.129 +fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
   1.130    let val (e, (_, _, prt)) = lookup_data sg tab kind
   1.131 -  in prt sg e handle _ => err_method ("print" ^ of_theory sg) kind end;
   1.132 +  in prt sg e handle _ => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) end;
   1.133  
   1.134 -fun put_data_sg sg (Data tab) kind e =
   1.135 -  Data (Symtab.update ((kind, (e, snd (lookup_data sg tab kind))), tab));
   1.136 +fun put_data_sg sg (Data tab) kind f x =
   1.137 +  Data (Symtab.update ((Object.name_of_kind kind,
   1.138 +    (kind, (f x, snd (lookup_data sg tab kind)))), tab));
   1.139  
   1.140  
   1.141  
   1.142 @@ -889,41 +908,41 @@
   1.143  fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) =
   1.144    (syn, tsig, ctab, names, init_data_sg sg data kind e ext mrg prt);
   1.145  
   1.146 -fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, e) =
   1.147 -  (syn, tsig, ctab, names, put_data_sg sg data kind e);
   1.148 +fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) =
   1.149 +  (syn, tsig, ctab, names, put_data_sg sg data kind f x);
   1.150  
   1.151  
   1.152  (* the external interfaces *)
   1.153  
   1.154 -val add_classes      = extend_sign true (ext_classes true) "#";
   1.155 -val add_classes_i    = extend_sign true (ext_classes false) "#";
   1.156 -val add_classrel     = extend_sign true (ext_classrel true) "#";
   1.157 -val add_classrel_i   = extend_sign true (ext_classrel false) "#";
   1.158 -val add_defsort      = extend_sign true (ext_defsort true) "#";
   1.159 -val add_defsort_i    = extend_sign true (ext_defsort false) "#";
   1.160 -val add_types        = extend_sign true ext_types "#";
   1.161 -val add_nonterminals = extend_sign true ext_nonterminals "#";
   1.162 -val add_tyabbrs      = extend_sign true ext_tyabbrs "#";
   1.163 -val add_tyabbrs_i    = extend_sign true ext_tyabbrs_i "#";
   1.164 -val add_arities      = extend_sign true (ext_arities true) "#";
   1.165 -val add_arities_i    = extend_sign true (ext_arities false) "#";
   1.166 -val add_consts       = extend_sign true ext_consts "#";
   1.167 -val add_consts_i     = extend_sign true ext_consts_i "#";
   1.168 -val add_syntax       = extend_sign true ext_syntax "#";
   1.169 -val add_syntax_i     = extend_sign true ext_syntax_i "#";
   1.170 -val add_modesyntax   = extend_sign true ext_modesyntax "#";
   1.171 -val add_modesyntax_i = extend_sign true ext_modesyntax_i "#";
   1.172 -val add_trfuns       = extend_sign true (ext_syn Syntax.extend_trfuns) "#";
   1.173 -val add_trfunsT      = extend_sign true (ext_syn Syntax.extend_trfunsT) "#";
   1.174 -val add_tokentrfuns  = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#";
   1.175 -val add_trrules      = extend_sign true ext_trrules "#";
   1.176 -val add_trrules_i    = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
   1.177 -val add_path         = extend_sign true ext_path "#";
   1.178 -val add_space        = extend_sign true ext_space "#";
   1.179 -fun init_data arg sg = extend_sign true (ext_init_data sg) "#" arg sg;
   1.180 -fun put_data arg sg  = extend_sign true (ext_put_data sg) "#" arg sg;
   1.181 -fun add_name name sg = extend_sign true K name () sg;
   1.182 -fun prep_ext sg      = extend_sign false K "#" () sg;
   1.183 +val add_classes       = extend_sign true (ext_classes true) "#";
   1.184 +val add_classes_i     = extend_sign true (ext_classes false) "#";
   1.185 +val add_classrel      = extend_sign true (ext_classrel true) "#";
   1.186 +val add_classrel_i    = extend_sign true (ext_classrel false) "#";
   1.187 +val add_defsort       = extend_sign true (ext_defsort true) "#";
   1.188 +val add_defsort_i     = extend_sign true (ext_defsort false) "#";
   1.189 +val add_types         = extend_sign true ext_types "#";
   1.190 +val add_nonterminals  = extend_sign true ext_nonterminals "#";
   1.191 +val add_tyabbrs       = extend_sign true ext_tyabbrs "#";
   1.192 +val add_tyabbrs_i     = extend_sign true ext_tyabbrs_i "#";
   1.193 +val add_arities       = extend_sign true (ext_arities true) "#";
   1.194 +val add_arities_i     = extend_sign true (ext_arities false) "#";
   1.195 +val add_consts        = extend_sign true ext_consts "#";
   1.196 +val add_consts_i      = extend_sign true ext_consts_i "#";
   1.197 +val add_syntax        = extend_sign true ext_syntax "#";
   1.198 +val add_syntax_i      = extend_sign true ext_syntax_i "#";
   1.199 +val add_modesyntax    = extend_sign true ext_modesyntax "#";
   1.200 +val add_modesyntax_i  = extend_sign true ext_modesyntax_i "#";
   1.201 +val add_trfuns        = extend_sign true (ext_syn Syntax.extend_trfuns) "#";
   1.202 +val add_trfunsT       = extend_sign true (ext_syn Syntax.extend_trfunsT) "#";
   1.203 +val add_tokentrfuns   = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#";
   1.204 +val add_trrules       = extend_sign true ext_trrules "#";
   1.205 +val add_trrules_i     = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
   1.206 +val add_path          = extend_sign true ext_path "#";
   1.207 +val add_space         = extend_sign true ext_space "#";
   1.208 +fun init_data arg sg  = extend_sign true (ext_init_data sg) "#" arg sg;
   1.209 +fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg;
   1.210 +fun add_name name sg  = extend_sign true K name () sg;
   1.211 +fun prep_ext sg       = extend_sign false K "#" () sg;
   1.212  
   1.213  
   1.214