removed data.ML (made part of sign.ML);
authorwenzelm
Thu Nov 20 15:28:48 1997 +0100 (1997-11-20)
changeset 4256e768c42069bb
parent 4255 63ab0616900b
child 4257 1663f9056045
removed data.ML (made part of sign.ML);
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/data.ML
src/Pure/display.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/IsaMakefile	Thu Nov 20 15:07:19 1997 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Thu Nov 20 15:28:48 1997 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  	Syntax/type_ext.ML Thy/ROOT.ML Thy/browser_info.ML Thy/file.ML \
     1.5  	Thy/path.ML Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML \
     1.6  	Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML \
     1.7 -	axclass.ML basis.ML data.ML deriv.ML display.ML drule.ML envir.ML \
     1.8 +	axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \
     1.9  	goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \
    1.10  	pattern.ML pure_thy.ML search.ML section_utils.ML sequence.ML sign.ML \
    1.11  	sorts.ML symtab.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
     2.1 --- a/src/Pure/ROOT.ML	Thu Nov 20 15:07:19 1997 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Thu Nov 20 15:28:48 1997 +0100
     2.3 @@ -26,7 +26,6 @@
     2.4  use "sorts.ML";
     2.5  use "type_infer.ML";
     2.6  use "type.ML";
     2.7 -use "data.ML";
     2.8  use "sign.ML";
     2.9  use "sequence.ML";
    2.10  use "envir.ML";
     3.1 --- a/src/Pure/data.ML	Thu Nov 20 15:07:19 1997 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,104 +0,0 @@
     3.4 -(*  Title:      Pure/data.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Markus Wenzel, TU Muenchen
     3.7 -
     3.8 -Arbitrarily typed data.  Fools the ML type system via exception
     3.9 -constructors.
    3.10 -*)
    3.11 -
    3.12 -type object = exn;
    3.13 -
    3.14 -signature DATA =
    3.15 -sig
    3.16 -  type T
    3.17 -  val empty: T
    3.18 -  val merge: T * T -> T
    3.19 -  val prep_ext: T -> T
    3.20 -  val kinds: T -> string list
    3.21 -  val init: T -> string -> object ->
    3.22 -    (object -> object) -> (object * object -> object) -> (object -> unit) -> T
    3.23 -  val get: T -> string -> object
    3.24 -  val put: T -> string -> object -> T
    3.25 -  val print: T -> string -> unit
    3.26 -end;
    3.27 -
    3.28 -
    3.29 -structure Data: DATA =
    3.30 -struct
    3.31 -
    3.32 -
    3.33 -(* datatype T *)
    3.34 -
    3.35 -datatype T = Data of
    3.36 -  (object *                             (*value*)
    3.37 -   ((object -> object) *                (*prepare extend method*)
    3.38 -    (object * object -> object) *       (*merge and prepare extend method*)
    3.39 -    (object -> unit)))                  (*print method*)
    3.40 -  Symtab.table;
    3.41 -
    3.42 -val empty = Data Symtab.null;
    3.43 -
    3.44 -fun kinds (Data tab) = map fst (Symtab.dest tab);
    3.45 -
    3.46 -
    3.47 -(* errors *)
    3.48 -
    3.49 -fun err_method name kind =
    3.50 -  error ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method");
    3.51 -
    3.52 -fun err_dup_init kind =
    3.53 -  error ("Duplicate initialization of " ^ quote kind ^ " data");
    3.54 -
    3.55 -fun err_uninit kind =
    3.56 -  error ("Tried to access uninitialized " ^ quote kind ^ " data");
    3.57 -
    3.58 -
    3.59 -(* prepare data *)
    3.60 -
    3.61 -fun merge (Data tab1, Data tab2) =
    3.62 -  let
    3.63 -    val data1 = Symtab.dest tab1;
    3.64 -    val data2 = Symtab.dest tab2;
    3.65 -    val all_data = data1 @ data2;
    3.66 -    val kinds = distinct (map fst all_data);
    3.67 -
    3.68 -   fun entry data kind =
    3.69 -     (case assoc (data, kind) of
    3.70 -       None => []
    3.71 -     | Some x => [(kind, x)]);
    3.72 -
    3.73 -    fun merge_entries [(kind, (e, mths as (ext, _, _)))] =
    3.74 -          (kind, (ext e handle _ => err_method "prep_ext" kind, mths))
    3.75 -      | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] =
    3.76 -          (kind, (mrg (e1, e2) handle _ => err_method "merge" kind, mths))
    3.77 -      | merge_entries _ = sys_error "merge_entries";
    3.78 -
    3.79 -    val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
    3.80 -  in Data (Symtab.make data) end;
    3.81 -
    3.82 -
    3.83 -fun prep_ext data = merge (data, empty);
    3.84 -
    3.85 -fun init (Data tab) kind e ext mrg prt =
    3.86 -  Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab))
    3.87 -    handle Symtab.DUPLICATE _ => err_dup_init kind;
    3.88 -
    3.89 -
    3.90 -(* access data *)
    3.91 -
    3.92 -fun lookup tab kind =
    3.93 -  (case Symtab.lookup (tab, kind) of
    3.94 -    Some x => x
    3.95 -  | None => err_uninit kind);
    3.96 -
    3.97 -fun get (Data tab) kind = fst (lookup tab kind);
    3.98 -
    3.99 -fun put (Data tab) kind e =
   3.100 -  Data (Symtab.update ((kind, (e, snd (lookup tab kind))), tab));
   3.101 -
   3.102 -fun print (Data tab) kind =
   3.103 -  let val (e, (_, _, prt)) = lookup tab kind
   3.104 -  in prt e handle _ => err_method "print" kind end;
   3.105 -
   3.106 -
   3.107 -end;
     4.1 --- a/src/Pure/display.ML	Thu Nov 20 15:07:19 1997 +0100
     4.2 +++ b/src/Pure/display.ML	Thu Nov 20 15:28:48 1997 +0100
     4.3 @@ -153,7 +153,7 @@
     4.4      val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab));
     4.5    in
     4.6      Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg));
     4.7 -    Pretty.writeln (Pretty.strs ("data:" :: Data.kinds data));
     4.8 +    Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data));
     4.9      Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
    4.10      Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces'));
    4.11      Pretty.writeln (pretty_classes classes);
     5.1 --- a/src/Pure/sign.ML	Thu Nov 20 15:07:19 1997 +0100
     5.2 +++ b/src/Pure/sign.ML	Thu Nov 20 15:28:48 1997 +0100
     5.3 @@ -19,6 +19,7 @@
     5.4  sig
     5.5    type sg
     5.6    type sg_ref
     5.7 +  type data
     5.8    val rep_sg: sg ->
     5.9     {self: sg_ref,
    5.10      tsig: Type.type_sig,
    5.11 @@ -26,7 +27,7 @@
    5.12      syn: Syntax.syntax,
    5.13      path: string list,
    5.14      spaces: (string * NameSpace.T) list,
    5.15 -    data: Data.T}
    5.16 +    data: data}
    5.17    val name_of: sg -> string
    5.18    val stamp_names_of: sg -> string list
    5.19    val tsig_of: sg -> Type.type_sig
    5.20 @@ -115,8 +116,9 @@
    5.21    val add_path: string -> sg -> sg
    5.22    val add_space: string * string list -> sg -> sg
    5.23    val add_name: string -> sg -> sg
    5.24 +  val data_kinds: data -> string list
    5.25    val init_data: string * (object * (object -> object) *
    5.26 -    (object * object -> object) * (object -> unit)) -> sg -> sg
    5.27 +    (object * object -> object) * (sg -> object -> unit)) -> sg -> sg
    5.28    val get_data: sg -> string -> object
    5.29    val put_data: string * object -> sg -> sg
    5.30    val print_data: sg -> string -> unit
    5.31 @@ -134,6 +136,8 @@
    5.32  
    5.33  (** datatype sg **)
    5.34  
    5.35 +(* types sg, data, sg_ref *)
    5.36 +
    5.37  datatype sg =
    5.38    Sg of
    5.39     {id: string ref,                             (*id*)
    5.40 @@ -144,9 +148,16 @@
    5.41      syn: Syntax.syntax,                         (*syntax for parsing and printing*)
    5.42      path: string list,                          (*current name space entry prefix*)
    5.43      spaces: (string * NameSpace.T) list,        (*name spaces for consts, types etc.*)
    5.44 -    data: Data.T}                               (*additional data*)
    5.45 +    data: data}                                 (*anytype data*)
    5.46 +and data =
    5.47 +  Data of
    5.48 +    (object *                             	(*value*)
    5.49 +     ((object -> object) *                	(*prepare extend method*)
    5.50 +      (object * object -> object) *       	(*merge and prepare extend method*)
    5.51 +      (sg -> object -> unit)))                 	(*print method*)
    5.52 +    Symtab.table
    5.53  and sg_ref =
    5.54 -  SgRef of sg ref option;
    5.55 +  SgRef of sg ref option
    5.56  
    5.57  (*make signature*)
    5.58  fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) =
    5.59 @@ -154,7 +165,7 @@
    5.60      syn = syn, path = path, spaces = spaces, data = data});
    5.61  
    5.62  
    5.63 -(* basic components *)
    5.64 +(* basic operations *)
    5.65  
    5.66  fun rep_sg (Sg (_, args)) = args;
    5.67  
    5.68 @@ -174,15 +185,6 @@
    5.69  val nonempty_sort = Type.nonempty_sort o tsig_of;
    5.70  
    5.71  
    5.72 -(* data *)
    5.73 -
    5.74 -fun access_data f sg k = f (#data (rep_sg sg)) k
    5.75 -  handle ERROR => error ("of theory " ^ str_of_sg sg);
    5.76 -
    5.77 -val get_data = access_data Data.get;
    5.78 -val print_data = access_data Data.print;
    5.79 -
    5.80 -
    5.81  (* id and self *)
    5.82  
    5.83  fun check_stale (sg as Sg ({id, ...},
    5.84 @@ -242,7 +244,77 @@
    5.85    | is_draft _ = false;
    5.86  
    5.87  
    5.88 -(* build signature *)
    5.89 +
    5.90 +(** signature data **)
    5.91 +
    5.92 +(* errors *)
    5.93 +
    5.94 +fun of_theory sg = " of theory " ^ str_of_sg sg;
    5.95 +
    5.96 +fun err_method name kind =
    5.97 +  error ("Error while invoking " ^ quote kind ^ " method " ^ name);
    5.98 +
    5.99 +fun err_dup_init sg kind =
   5.100 +  error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
   5.101 +
   5.102 +fun err_uninit sg kind =
   5.103 +  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
   5.104 +
   5.105 +
   5.106 +(* prepare data *)
   5.107 +
   5.108 +val empty_data = Data Symtab.null;
   5.109 +
   5.110 +fun merge_data (Data tab1, Data tab2) =
   5.111 +  let
   5.112 +    val data1 = Symtab.dest tab1;
   5.113 +    val data2 = Symtab.dest tab2;
   5.114 +    val all_data = data1 @ data2;
   5.115 +    val kinds = distinct (map fst all_data);
   5.116 +
   5.117 +   fun entry data kind =
   5.118 +     (case assoc (data, kind) of
   5.119 +       None => []
   5.120 +     | Some x => [(kind, x)]);
   5.121 +
   5.122 +    fun merge_entries [(kind, (e, mths as (ext, _, _)))] =
   5.123 +          (kind, (ext e handle _ => err_method "prep_ext" kind, mths))
   5.124 +      | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] =
   5.125 +          (kind, (mrg (e1, e2) handle _ => err_method "merge" kind, mths))
   5.126 +      | merge_entries _ = sys_error "merge_entries";
   5.127 +
   5.128 +    val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
   5.129 +  in Data (Symtab.make data) end;
   5.130 +
   5.131 +fun prep_ext_data data = merge_data (data, empty_data);
   5.132 +
   5.133 +fun init_data_sg sg (Data tab) kind e ext mrg prt =
   5.134 +  Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab))
   5.135 +    handle Symtab.DUPLICATE _ => err_dup_init sg kind;
   5.136 +
   5.137 +
   5.138 +(* access data *)
   5.139 +
   5.140 +fun data_kinds (Data tab) = map fst (Symtab.dest tab);
   5.141 +
   5.142 +fun lookup_data sg tab kind =
   5.143 +  (case Symtab.lookup (tab, kind) of
   5.144 +    Some x => x
   5.145 +  | None => err_uninit sg kind);
   5.146 +
   5.147 +fun get_data (sg as Sg (_, {data = Data tab, ...})) kind =
   5.148 +  fst (lookup_data sg tab kind);
   5.149 +
   5.150 +fun print_data (sg as Sg (_, {data = Data tab, ...})) kind =
   5.151 +  let val (e, (_, _, prt)) = lookup_data sg tab kind
   5.152 +  in prt sg e handle _ => err_method ("print" ^ of_theory sg) kind end;
   5.153 +
   5.154 +fun put_data_sg sg (Data tab) kind e =
   5.155 +  Data (Symtab.update ((kind, (e, snd (lookup_data sg tab kind))), tab));
   5.156 +
   5.157 +
   5.158 +
   5.159 +(** build signatures **)
   5.160  
   5.161  fun ext_stamps stamps (id as ref name) =
   5.162    let val stmps = (case stamps of ref "#" :: ss => ss | ss => ss) in
   5.163 @@ -269,7 +341,7 @@
   5.164      val _ = check_stale sg;
   5.165      val (self', data') =
   5.166        if is_draft sg andalso keep then (self, data)
   5.167 -      else (SgRef (Some (ref sg)), Data.prep_ext data);
   5.168 +      else (SgRef (Some (ref sg)), prep_ext_data data);
   5.169    in
   5.170      create_sign self' stamps name
   5.171        (extfun (syn, tsig, const_tab, (path, spaces), data') decls)
   5.172 @@ -747,11 +819,11 @@
   5.173  
   5.174  (* signature data *)
   5.175  
   5.176 -fun ext_init_data (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) =
   5.177 -  (syn, tsig, ctab, names, Data.init data kind e ext mrg prt);
   5.178 +fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) =
   5.179 +  (syn, tsig, ctab, names, init_data_sg sg data kind e ext mrg prt);
   5.180  
   5.181 -fun ext_put_data (syn, tsig, ctab, names, data) (kind, e) =
   5.182 -  (syn, tsig, ctab, names, Data.put data kind e);
   5.183 +fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, e) =
   5.184 +  (syn, tsig, ctab, names, put_data_sg sg data kind e);
   5.185  
   5.186  
   5.187  (* the external interfaces *)
   5.188 @@ -780,8 +852,8 @@
   5.189  val add_trrules_i    = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
   5.190  val add_path         = extend_sign true ext_path "#";
   5.191  val add_space        = extend_sign true ext_space "#";
   5.192 -val init_data        = extend_sign true ext_init_data "#";
   5.193 -val put_data         = extend_sign true ext_put_data "#";
   5.194 +fun init_data arg sg = extend_sign true (ext_init_data sg) "#" arg sg;
   5.195 +fun put_data arg sg  = extend_sign true (ext_put_data sg) "#" arg sg;
   5.196  fun add_name name sg = extend_sign true K name () sg;
   5.197  fun prep_ext sg      = extend_sign false K "#" () sg;
   5.198  
   5.199 @@ -846,7 +918,7 @@
   5.200            ListPair.map NameSpace.merge
   5.201              (map (space_of spaces1) kinds, map (space_of spaces2) kinds);
   5.202  
   5.203 -      val data = Data.merge (data1, data2);
   5.204 +      val data = merge_data (data1, data2);
   5.205  
   5.206        val sign = make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps);
   5.207      in
   5.208 @@ -863,11 +935,11 @@
   5.209  (** partial Pure signature **)
   5.210  
   5.211  val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
   5.212 -  Symtab.null, Syntax.pure_syn, [], [], Data.empty, []);
   5.213 +  Symtab.null, Syntax.pure_syn, [], [], empty_data, []);
   5.214  
   5.215  val pre_pure =
   5.216    create_sign (SgRef (Some (ref dummy_sg))) [] "#"
   5.217 -    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), Data.empty);
   5.218 +    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), empty_data);
   5.219  
   5.220  
   5.221  end;