# HG changeset patch # User wenzelm # Date 897314336 -7200 # Node ID 4486d53a6438bab653e6d1ae93af8195a19b00d5 # Parent cf4e3b487caf915d0e1533b72e8a6f36e2cc772f use type-safe theory data interface; diff -r cf4e3b487caf -r 4486d53a6438 src/Pure/attribute.ML --- a/src/Pure/attribute.ML Mon Jun 08 15:57:50 1998 +0200 +++ b/src/Pure/attribute.ML Mon Jun 08 15:58:56 1998 +0200 @@ -103,48 +103,42 @@ (** theory data **) -(* data kind 'attributes' *) +(* data kind 'Pure/attributes' *) -local - val attributesK = Object.kind "Pure/attributes"; - - exception Attributes of +structure AttributesDataArgs = +struct + val name = "Pure/attributes"; + type T = {space: NameSpace.T, attrs: ((((string list -> theory attribute) * (string list -> local_theory attribute)) * string) * stamp) Symtab.table}; - - val empty = Attributes {space = NameSpace.empty, attrs = Symtab.empty}; - - fun prep_ext (x as Attributes _) = x; + val empty = {space = NameSpace.empty, attrs = Symtab.empty}; + val prep_ext = I; - fun merge (Attributes {space = space1, attrs = attrs1}, - Attributes {space = space2, attrs = attrs2}) = - Attributes { - space = NameSpace.merge (space1, space2), + fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) = + {space = NameSpace.merge (space1, space2), attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups => error ("Attempt to merge different versions of attributes " ^ commas_quote dups)}; fun pretty_attr (name, ((_, comment), _)) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; - fun print _ (Attributes {space, attrs}) = + fun print _ ({space, attrs}) = (Pretty.writeln (Display.pretty_name_space ("attribute name space", space)); Pretty.writeln (Pretty.big_list "attributes:" (map pretty_attr (Symtab.dest attrs)))); -in - val init_attributes = Theory.init_data attributesK (empty, prep_ext, merge, print); - val print_attributes = Theory.print_data attributesK; - val get_attributes = Theory.get_data attributesK (fn Attributes x => x); - val put_attributes = Theory.put_data attributesK Attributes; end; +structure AttributesData = TheoryDataFun(AttributesDataArgs); +val print_attributes = AttributesData.print; + (* get global / local attributes *) fun gen_attr which thy = let - val {space, attrs} = get_attributes thy; + val {space, attrs} = AttributesData.get thy; val intern = NameSpace.intern space; fun attr (raw_name, args) x_th = @@ -165,19 +159,19 @@ val new_attrs = map (fn (name, f, g, comment) => (full name, (((f, g), comment), stamp ()))) raw_attrs; - val {space, attrs} = get_attributes thy; + val {space, attrs} = AttributesData.get thy; val space' = NameSpace.extend (space, map fst new_attrs); val attrs' = Symtab.extend (attrs, new_attrs) handle Symtab.DUPS dups => error ("Duplicate declaration of attributes(s) " ^ commas_quote dups); in - thy |> put_attributes {space = space', attrs = attrs'} + thy |> AttributesData.put {space = space', attrs = attrs'} end; (* setup *) (* FIXME add_attributes: lemma etc. *) val setup = - [init_attributes]; + [AttributesData.init]; end; diff -r cf4e3b487caf -r 4486d53a6438 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Jun 08 15:57:50 1998 +0200 +++ b/src/Pure/pure_thy.ML Mon Jun 08 15:58:56 1998 +0200 @@ -56,20 +56,23 @@ (** data kind 'Pure/theorems' **) -local - val theoremsK = Object.kind "Pure/theorems"; +structure TheoremsDataArgs = +struct + val name = "Pure/theorems"; - exception Theorems of - {space: NameSpace.T, - thms_tab: tthm list Symtab.table, - const_idx: int * (int * tthm) list Symtab.table} ref; - + type T = + {space: NameSpace.T, + thms_tab: tthm list Symtab.table, + const_idx: int * (int * tthm) list Symtab.table} ref; fun mk_empty _ = - Theorems (ref {space = NameSpace.empty, - thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)}); + ref {space = NameSpace.empty, thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)} : T; - fun print sg (Theorems (ref {space, thms_tab, const_idx = _})) = + val empty = mk_empty (); + val prep_ext = mk_empty; + val merge = mk_empty; + + fun print sg (ref {space, thms_tab, const_idx = _}) = let val prt_thm = Attribute.pretty_tthm o apfst (Thm.transfer_sg sg); fun prt_thms (name, [th]) = @@ -83,16 +86,16 @@ Pretty.writeln (Display.pretty_name_space ("theorem name space", space)); Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss)) end; -in - val init_theorems = Theory.init_data theoremsK (mk_empty (), mk_empty, mk_empty, print); - val print_theorems = Theory.print_data theoremsK; - val get_theorems_sg = Sign.get_data theoremsK (fn Theorems r => r); - val get_theorems = get_theorems_sg o Theory.sign_of; end; +structure TheoremsData = TheoryDataFun(TheoremsDataArgs); +val get_theorems_sg = TheoremsData.get_sg; +val get_theorems = TheoremsData.get; + (* print theory *) +val print_theorems = TheoremsData.print; fun print_theory thy = (Display.print_theory thy; print_theorems thy); @@ -208,7 +211,7 @@ warning ("Replaced old copy of theorems " ^ quote name); fun warn_same name = - warning ("Theorem database already contains a copy of " ^ quote name); + warning ("Theorem database already contains a copy of " ^ quote name); fun enter_tthmx sg app_name (bname, tthmx) = let @@ -287,22 +290,23 @@ (** theory management **) -(* data kind 'Pure/theory' *) +(* data kind 'Pure/theory_management' *) -local - val theoryK = Object.kind "Pure/theory"; - exception Theory of {name: string, generation: int}; +structure TheoryManagementDataArgs = +struct + val name = "Pure/theory_management"; + type T = {name: string, generation: int}; - val empty = Theory {name = "", generation = 0}; - fun prep_ext (x as Theory _) = x; + val empty = {name = "", generation = 0}; + val prep_ext = I; fun merge _ = empty; - fun print _ (Theory _) = (); -in - val init_theory = Theory.init_data theoryK (empty, prep_ext, merge, print); - val get_info = Theory.get_data theoryK (fn Theory info => info); - val put_info = Theory.put_data theoryK Theory; + fun print _ _ = (); end; +structure TheoryManagementData = TheoryDataFun(TheoryManagementDataArgs); +val get_info = TheoryManagementData.get; +val put_info = TheoryManagementData.put; + (* get / put name *) @@ -341,7 +345,7 @@ val copy_thy = thy |> Theory.prep_ext - |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int generation) (* FIXME !!?? *) + |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int generation) (* FIXME !!?? *) |> put_info {name = name, generation = generation + 1}; in (transform_error f thy, false, None) handle exn => @@ -378,7 +382,7 @@ val proto_pure = Theory.pre_pure - |> Theory.apply (Attribute.setup @ [init_theorems, init_theory]) + |> Theory.apply (Attribute.setup @ [TheoremsData.init, TheoryManagementData.init]) |> put_name "ProtoPure" |> global_path |> Theory.add_types