src/Pure/sign.ML
changeset 4256 e768c42069bb
parent 4249 34b7aafdc1bc
child 4261 e20b9fd85811
     1.1 --- a/src/Pure/sign.ML	Thu Nov 20 15:07:19 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 20 15:28:48 1997 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4  sig
     1.5    type sg
     1.6    type sg_ref
     1.7 +  type data
     1.8    val rep_sg: sg ->
     1.9     {self: sg_ref,
    1.10      tsig: Type.type_sig,
    1.11 @@ -26,7 +27,7 @@
    1.12      syn: Syntax.syntax,
    1.13      path: string list,
    1.14      spaces: (string * NameSpace.T) list,
    1.15 -    data: Data.T}
    1.16 +    data: data}
    1.17    val name_of: sg -> string
    1.18    val stamp_names_of: sg -> string list
    1.19    val tsig_of: sg -> Type.type_sig
    1.20 @@ -115,8 +116,9 @@
    1.21    val add_path: string -> sg -> sg
    1.22    val add_space: string * string list -> sg -> sg
    1.23    val add_name: string -> sg -> sg
    1.24 +  val data_kinds: data -> string list
    1.25    val init_data: string * (object * (object -> object) *
    1.26 -    (object * object -> object) * (object -> unit)) -> sg -> sg
    1.27 +    (object * object -> object) * (sg -> object -> unit)) -> sg -> sg
    1.28    val get_data: sg -> string -> object
    1.29    val put_data: string * object -> sg -> sg
    1.30    val print_data: sg -> string -> unit
    1.31 @@ -134,6 +136,8 @@
    1.32  
    1.33  (** datatype sg **)
    1.34  
    1.35 +(* types sg, data, sg_ref *)
    1.36 +
    1.37  datatype sg =
    1.38    Sg of
    1.39     {id: string ref,                             (*id*)
    1.40 @@ -144,9 +148,16 @@
    1.41      syn: Syntax.syntax,                         (*syntax for parsing and printing*)
    1.42      path: string list,                          (*current name space entry prefix*)
    1.43      spaces: (string * NameSpace.T) list,        (*name spaces for consts, types etc.*)
    1.44 -    data: Data.T}                               (*additional data*)
    1.45 +    data: data}                                 (*anytype data*)
    1.46 +and data =
    1.47 +  Data of
    1.48 +    (object *                             	(*value*)
    1.49 +     ((object -> object) *                	(*prepare extend method*)
    1.50 +      (object * object -> object) *       	(*merge and prepare extend method*)
    1.51 +      (sg -> object -> unit)))                 	(*print method*)
    1.52 +    Symtab.table
    1.53  and sg_ref =
    1.54 -  SgRef of sg ref option;
    1.55 +  SgRef of sg ref option
    1.56  
    1.57  (*make signature*)
    1.58  fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) =
    1.59 @@ -154,7 +165,7 @@
    1.60      syn = syn, path = path, spaces = spaces, data = data});
    1.61  
    1.62  
    1.63 -(* basic components *)
    1.64 +(* basic operations *)
    1.65  
    1.66  fun rep_sg (Sg (_, args)) = args;
    1.67  
    1.68 @@ -174,15 +185,6 @@
    1.69  val nonempty_sort = Type.nonempty_sort o tsig_of;
    1.70  
    1.71  
    1.72 -(* data *)
    1.73 -
    1.74 -fun access_data f sg k = f (#data (rep_sg sg)) k
    1.75 -  handle ERROR => error ("of theory " ^ str_of_sg sg);
    1.76 -
    1.77 -val get_data = access_data Data.get;
    1.78 -val print_data = access_data Data.print;
    1.79 -
    1.80 -
    1.81  (* id and self *)
    1.82  
    1.83  fun check_stale (sg as Sg ({id, ...},
    1.84 @@ -242,7 +244,77 @@
    1.85    | is_draft _ = false;
    1.86  
    1.87  
    1.88 -(* build signature *)
    1.89 +
    1.90 +(** signature data **)
    1.91 +
    1.92 +(* errors *)
    1.93 +
    1.94 +fun of_theory sg = " of theory " ^ str_of_sg sg;
    1.95 +
    1.96 +fun err_method name kind =
    1.97 +  error ("Error while invoking " ^ quote kind ^ " method " ^ name);
    1.98 +
    1.99 +fun err_dup_init sg kind =
   1.100 +  error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
   1.101 +
   1.102 +fun err_uninit sg kind =
   1.103 +  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
   1.104 +
   1.105 +
   1.106 +(* prepare data *)
   1.107 +
   1.108 +val empty_data = Data Symtab.null;
   1.109 +
   1.110 +fun merge_data (Data tab1, Data tab2) =
   1.111 +  let
   1.112 +    val data1 = Symtab.dest tab1;
   1.113 +    val data2 = Symtab.dest tab2;
   1.114 +    val all_data = data1 @ data2;
   1.115 +    val kinds = distinct (map fst all_data);
   1.116 +
   1.117 +   fun entry data kind =
   1.118 +     (case assoc (data, kind) of
   1.119 +       None => []
   1.120 +     | Some x => [(kind, x)]);
   1.121 +
   1.122 +    fun merge_entries [(kind, (e, mths as (ext, _, _)))] =
   1.123 +          (kind, (ext e handle _ => err_method "prep_ext" kind, mths))
   1.124 +      | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] =
   1.125 +          (kind, (mrg (e1, e2) handle _ => err_method "merge" kind, mths))
   1.126 +      | merge_entries _ = sys_error "merge_entries";
   1.127 +
   1.128 +    val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
   1.129 +  in Data (Symtab.make data) end;
   1.130 +
   1.131 +fun prep_ext_data data = merge_data (data, empty_data);
   1.132 +
   1.133 +fun init_data_sg sg (Data tab) kind e ext mrg prt =
   1.134 +  Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab))
   1.135 +    handle Symtab.DUPLICATE _ => err_dup_init sg kind;
   1.136 +
   1.137 +
   1.138 +(* access data *)
   1.139 +
   1.140 +fun data_kinds (Data tab) = map fst (Symtab.dest tab);
   1.141 +
   1.142 +fun lookup_data sg tab kind =
   1.143 +  (case Symtab.lookup (tab, kind) of
   1.144 +    Some x => x
   1.145 +  | None => err_uninit sg kind);
   1.146 +
   1.147 +fun get_data (sg as Sg (_, {data = Data tab, ...})) kind =
   1.148 +  fst (lookup_data sg tab kind);
   1.149 +
   1.150 +fun print_data (sg as Sg (_, {data = Data tab, ...})) kind =
   1.151 +  let val (e, (_, _, prt)) = lookup_data sg tab kind
   1.152 +  in prt sg e handle _ => err_method ("print" ^ of_theory sg) kind end;
   1.153 +
   1.154 +fun put_data_sg sg (Data tab) kind e =
   1.155 +  Data (Symtab.update ((kind, (e, snd (lookup_data sg tab kind))), tab));
   1.156 +
   1.157 +
   1.158 +
   1.159 +(** build signatures **)
   1.160  
   1.161  fun ext_stamps stamps (id as ref name) =
   1.162    let val stmps = (case stamps of ref "#" :: ss => ss | ss => ss) in
   1.163 @@ -269,7 +341,7 @@
   1.164      val _ = check_stale sg;
   1.165      val (self', data') =
   1.166        if is_draft sg andalso keep then (self, data)
   1.167 -      else (SgRef (Some (ref sg)), Data.prep_ext data);
   1.168 +      else (SgRef (Some (ref sg)), prep_ext_data data);
   1.169    in
   1.170      create_sign self' stamps name
   1.171        (extfun (syn, tsig, const_tab, (path, spaces), data') decls)
   1.172 @@ -747,11 +819,11 @@
   1.173  
   1.174  (* signature data *)
   1.175  
   1.176 -fun ext_init_data (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) =
   1.177 -  (syn, tsig, ctab, names, Data.init data kind e ext mrg prt);
   1.178 +fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) =
   1.179 +  (syn, tsig, ctab, names, init_data_sg sg data kind e ext mrg prt);
   1.180  
   1.181 -fun ext_put_data (syn, tsig, ctab, names, data) (kind, e) =
   1.182 -  (syn, tsig, ctab, names, Data.put data kind e);
   1.183 +fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, e) =
   1.184 +  (syn, tsig, ctab, names, put_data_sg sg data kind e);
   1.185  
   1.186  
   1.187  (* the external interfaces *)
   1.188 @@ -780,8 +852,8 @@
   1.189  val add_trrules_i    = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
   1.190  val add_path         = extend_sign true ext_path "#";
   1.191  val add_space        = extend_sign true ext_space "#";
   1.192 -val init_data        = extend_sign true ext_init_data "#";
   1.193 -val put_data         = extend_sign true ext_put_data "#";
   1.194 +fun init_data arg sg = extend_sign true (ext_init_data sg) "#" arg sg;
   1.195 +fun put_data arg sg  = extend_sign true (ext_put_data sg) "#" arg sg;
   1.196  fun add_name name sg = extend_sign true K name () sg;
   1.197  fun prep_ext sg      = extend_sign false K "#" () sg;
   1.198  
   1.199 @@ -846,7 +918,7 @@
   1.200            ListPair.map NameSpace.merge
   1.201              (map (space_of spaces1) kinds, map (space_of spaces2) kinds);
   1.202  
   1.203 -      val data = Data.merge (data1, data2);
   1.204 +      val data = merge_data (data1, data2);
   1.205  
   1.206        val sign = make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps);
   1.207      in
   1.208 @@ -863,11 +935,11 @@
   1.209  (** partial Pure signature **)
   1.210  
   1.211  val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
   1.212 -  Symtab.null, Syntax.pure_syn, [], [], Data.empty, []);
   1.213 +  Symtab.null, Syntax.pure_syn, [], [], empty_data, []);
   1.214  
   1.215  val pre_pure =
   1.216    create_sign (SgRef (Some (ref dummy_sg))) [] "#"
   1.217 -    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), Data.empty);
   1.218 +    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), empty_data);
   1.219  
   1.220  
   1.221  end;