# HG changeset patch # User wenzelm # Date 880036128 -3600 # Node ID e768c42069bb33041e0767ce22facead6689d45b # Parent 63ab0616900bd58c1aec205be7049cd7aa56658a removed data.ML (made part of sign.ML); diff -r 63ab0616900b -r e768c42069bb src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Nov 20 15:07:19 1997 +0100 +++ b/src/Pure/IsaMakefile Thu Nov 20 15:28:48 1997 +0100 @@ -17,7 +17,7 @@ Syntax/type_ext.ML Thy/ROOT.ML Thy/browser_info.ML Thy/file.ML \ Thy/path.ML Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML \ Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML \ - axclass.ML basis.ML data.ML deriv.ML display.ML drule.ML envir.ML \ + axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \ goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \ pattern.ML pure_thy.ML search.ML section_utils.ML sequence.ML sign.ML \ sorts.ML symtab.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \ diff -r 63ab0616900b -r e768c42069bb src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Nov 20 15:07:19 1997 +0100 +++ b/src/Pure/ROOT.ML Thu Nov 20 15:28:48 1997 +0100 @@ -26,7 +26,6 @@ use "sorts.ML"; use "type_infer.ML"; use "type.ML"; -use "data.ML"; use "sign.ML"; use "sequence.ML"; use "envir.ML"; diff -r 63ab0616900b -r e768c42069bb src/Pure/data.ML --- a/src/Pure/data.ML Thu Nov 20 15:07:19 1997 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,104 +0,0 @@ -(* Title: Pure/data.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -Arbitrarily typed data. Fools the ML type system via exception -constructors. -*) - -type object = exn; - -signature DATA = -sig - type T - val empty: T - val merge: T * T -> T - val prep_ext: T -> T - val kinds: T -> string list - val init: T -> string -> object -> - (object -> object) -> (object * object -> object) -> (object -> unit) -> T - val get: T -> string -> object - val put: T -> string -> object -> T - val print: T -> string -> unit -end; - - -structure Data: DATA = -struct - - -(* datatype T *) - -datatype T = Data of - (object * (*value*) - ((object -> object) * (*prepare extend method*) - (object * object -> object) * (*merge and prepare extend method*) - (object -> unit))) (*print method*) - Symtab.table; - -val empty = Data Symtab.null; - -fun kinds (Data tab) = map fst (Symtab.dest tab); - - -(* errors *) - -fun err_method name kind = - error ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method"); - -fun err_dup_init kind = - error ("Duplicate initialization of " ^ quote kind ^ " data"); - -fun err_uninit kind = - error ("Tried to access uninitialized " ^ quote kind ^ " data"); - - -(* prepare data *) - -fun merge (Data tab1, Data tab2) = - let - val data1 = Symtab.dest tab1; - val data2 = Symtab.dest tab2; - val all_data = data1 @ data2; - val kinds = distinct (map fst all_data); - - fun entry data kind = - (case assoc (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)) - | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] = - (kind, (mrg (e1, e2) handle _ => err_method "merge" 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; - - -fun prep_ext data = merge (data, empty); - -fun init (Data tab) kind e ext mrg prt = - Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab)) - handle Symtab.DUPLICATE _ => err_dup_init kind; - - -(* access data *) - -fun lookup tab kind = - (case Symtab.lookup (tab, kind) of - Some x => x - | None => err_uninit kind); - -fun get (Data tab) kind = fst (lookup tab kind); - -fun put (Data tab) kind e = - Data (Symtab.update ((kind, (e, snd (lookup tab kind))), tab)); - -fun print (Data tab) kind = - let val (e, (_, _, prt)) = lookup tab kind - in prt e handle _ => err_method "print" kind end; - - -end; diff -r 63ab0616900b -r e768c42069bb src/Pure/display.ML --- a/src/Pure/display.ML Thu Nov 20 15:07:19 1997 +0100 +++ b/src/Pure/display.ML Thu Nov 20 15:28:48 1997 +0100 @@ -153,7 +153,7 @@ val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab)); in Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg)); - Pretty.writeln (Pretty.strs ("data:" :: Data.kinds data)); + Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data)); Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]); Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces')); Pretty.writeln (pretty_classes classes); diff -r 63ab0616900b -r e768c42069bb src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Nov 20 15:07:19 1997 +0100 +++ b/src/Pure/sign.ML Thu Nov 20 15:28:48 1997 +0100 @@ -19,6 +19,7 @@ sig type sg type sg_ref + type data val rep_sg: sg -> {self: sg_ref, tsig: Type.type_sig, @@ -26,7 +27,7 @@ syn: Syntax.syntax, path: string list, spaces: (string * NameSpace.T) list, - data: Data.T} + data: data} val name_of: sg -> string val stamp_names_of: sg -> string list val tsig_of: sg -> Type.type_sig @@ -115,8 +116,9 @@ val add_path: string -> sg -> sg 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) * (object -> unit)) -> sg -> sg + (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 @@ -134,6 +136,8 @@ (** datatype sg **) +(* types sg, data, sg_ref *) + datatype sg = Sg of {id: string ref, (*id*) @@ -144,9 +148,16 @@ syn: Syntax.syntax, (*syntax for parsing and printing*) path: string list, (*current name space entry prefix*) spaces: (string * NameSpace.T) list, (*name spaces for consts, types etc.*) - data: Data.T} (*additional data*) + 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*) + 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) = @@ -154,7 +165,7 @@ syn = syn, path = path, spaces = spaces, data = data}); -(* basic components *) +(* basic operations *) fun rep_sg (Sg (_, args)) = args; @@ -174,15 +185,6 @@ val nonempty_sort = Type.nonempty_sort o tsig_of; -(* data *) - -fun access_data f sg k = f (#data (rep_sg sg)) k - handle ERROR => error ("of theory " ^ str_of_sg sg); - -val get_data = access_data Data.get; -val print_data = access_data Data.print; - - (* id and self *) fun check_stale (sg as Sg ({id, ...}, @@ -242,7 +244,77 @@ | is_draft _ = false; -(* build signature *) + +(** signature data **) + +(* errors *) + +fun of_theory sg = " of theory " ^ str_of_sg sg; + +fun err_method name kind = + error ("Error while invoking " ^ quote kind ^ " method " ^ name); + +fun err_dup_init sg kind = + error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg); + +fun err_uninit sg kind = + error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg); + + +(* prepare data *) + +val empty_data = Data Symtab.null; + +fun merge_data (Data tab1, Data tab2) = + let + val data1 = Symtab.dest tab1; + val data2 = Symtab.dest tab2; + val all_data = data1 @ data2; + val kinds = distinct (map fst all_data); + + fun entry data kind = + (case assoc (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)) + | merge_entries [(kind, (e1, mths as (_, mrg, _))), (_, (e2, _))] = + (kind, (mrg (e1, e2) handle _ => err_method "merge" 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; + +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.DUPLICATE _ => err_dup_init sg kind; + + +(* access data *) + +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); + +fun print_data (sg as Sg (_, {data = Data tab, ...})) kind = + let val (e, (_, _, prt)) = lookup_data sg tab kind + in prt sg e handle _ => err_method ("print" ^ of_theory sg) kind end; + +fun put_data_sg sg (Data tab) kind e = + Data (Symtab.update ((kind, (e, snd (lookup_data sg tab kind))), tab)); + + + +(** build signatures **) fun ext_stamps stamps (id as ref name) = let val stmps = (case stamps of ref "#" :: ss => ss | ss => ss) in @@ -269,7 +341,7 @@ val _ = check_stale sg; val (self', data') = if is_draft sg andalso keep then (self, data) - else (SgRef (Some (ref sg)), Data.prep_ext data); + else (SgRef (Some (ref sg)), prep_ext_data data); in create_sign self' stamps name (extfun (syn, tsig, const_tab, (path, spaces), data') decls) @@ -747,11 +819,11 @@ (* signature data *) -fun ext_init_data (syn, tsig, ctab, names, data) (kind, (e, ext, mrg, prt)) = - (syn, tsig, ctab, names, Data.init data kind e ext mrg prt); +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 (syn, tsig, ctab, names, data) (kind, e) = - (syn, tsig, ctab, names, Data.put data kind e); +fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, e) = + (syn, tsig, ctab, names, put_data_sg sg data kind e); (* the external interfaces *) @@ -780,8 +852,8 @@ 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 "#"; -val init_data = extend_sign true ext_init_data "#"; -val put_data = extend_sign true ext_put_data "#"; +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; @@ -846,7 +918,7 @@ ListPair.map NameSpace.merge (map (space_of spaces1) kinds, map (space_of spaces2) kinds); - val data = Data.merge (data1, data2); + val data = merge_data (data1, data2); val sign = make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps); in @@ -863,11 +935,11 @@ (** partial Pure signature **) val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0, - Symtab.null, Syntax.pure_syn, [], [], Data.empty, []); + Symtab.null, Syntax.pure_syn, [], [], empty_data, []); val pre_pure = create_sign (SgRef (Some (ref dummy_sg))) [] "#" - (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), Data.empty); + (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), empty_data); end;