----------------------------------------------------------------------------- -- -- libwww-ada95 : A World Wide Web client library for Ada95 -- -- U T I L . H A S H E D _ M A P P I N G -- -- S p e c -- -- Copyright (C) 1997-1998 Regents of the University of California -- -- libwww-ada95 is free software; you can redistribute it and/or modify it -- under the terms of the GNU General Public License as published by the Free -- Software Foundation, with or without the single exception listed below; -- either version 2, or (at your option) any later version. libwww-ada95 is -- distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; -- without even the implied warranty of MERCHANTABILITY or FITNESS FOR A -- PARTICULAR PURPOSE. See the GNU General Public License for more details. -- You should have received a copy of the GNU General Public License -- distributed with libwww-ada95; see the file COPYING. If not, write to the -- Free Software Foundation, 59 Temple Place - Suite 330, Boston, MA -- 02111-1307, USA. -- -- As a special exception, if other files instantiate generics from this -- library, or you link this library with other files to produce an -- executable, this library does not by itself cause the resulting -- executable to be covered by the GNU General Public License. This -- exception does not however invalidate any other reasons why the -- executable file might be covered by the GNU General Public License. -- -- Created in 1997 by Ron Kownacki and Kari Nies ----------------------------------------------------------------------------- -- -- This package provides a mapping from one arbitrary type, key_type, to -- another arbitrary type, value_type. These types are generic formals -- to the package, along with an equality relation on key_type, an -- integer subtype that determines the number of hash buckets, and a -- hashing function on key_type that maps to that integer subtype. -- -- For the purpose of specifying the operations in this package, we will -- view a mapping as a set of bindings, or key/value pairs. This allows -- the use of set notation in description. -- -- The following is a complete list of operations, written in the order -- in which they appear in the spec. -- -- Constructors: -- Create -- Bind -- Unbind -- Copy -- Query Operations: -- Is_Empty -- Size -- Is_Bound -- Fetch -- Iterators: -- Make_Keys_Iter, More, Next -- Make_Values_Iter, More, Next -- Make_Bindings_Iter, More, Next -- Heap Management: -- Destroy -- ----------------------------------------------------------------------------- with Util.LLists; -- Lists used in implementation. (private) pragma Elaborate (Util.LLists); generic type Key_Type is private; -- | Domain type of the mapping. with function Equal (K1, K2 : Key_Type) return boolean is "="; -- | equal is required to form an equality relation on Key_Type. type Bucket_Range is (<>); -- | Defines the number of hash buckets, one for each member of -- | bucket_range. with function Hash (K : Key_Type) return Bucket_Range; -- | Required property: Equal (E1, E2) => Hash (E1) = Hash (E2). -- | Best results if hash produces a uniform distribution -- | over Bucket_Range. type Value_Type is private; -- | Target type of the mapping. package Util.Hashed_Mapping is type Mapping is private; -- | The hashed mapping abstract data type. -- Exceptions: No_More : exception; -- | Raised on incorrect use of an iterator. Uninitialized_Mapping : exception; -- | Raised on use of an unitialized mapping by most operations. Already_Bound : exception; -- | Raised on attempt to rebind a key that is currently bound. Not_Bound : exception; -- | Raised when a key that is expected to be bound is unbound. -- Iterators: type Keys_Iter is private; -- | Bound keys in arbitrary order. type Values_Iter is private; -- | Bound values in arbitrary order. type Bindings_Iter is private; -- | Key,value pairs in arbitrary order -- Constructors: function Create return Mapping; -- | Effects: -- | Return {}. procedure Bind (Map : in out Mapping; Key : in Key_Type; Value : in Value_Type); -- | Raises: Already_Bound, Uninitialized_Mapping -- | Effects: -- | Insert the binding, , into Map. Raises -- | Already_Bound iff a pair, , where Equal (key, k'), -- | is in map. -- | Raises Uninitialized_Mapping iff map has not been initialized. procedure Unbind (Map : in out Mapping; Key : in Key_Type); -- | Raises: not_bound, Uninitialized_Mapping -- | Effects: -- | If , where equal (key, k), is in map, then removes -- | from map. Raises not_bound if no such pair exists. -- | Raises Uninitialized_Mapping iff map has not been initialized. function Copy (Map : Mapping) return Mapping; -- | Raises: Uninitialized_Mapping -- | Effects: -- | Returns a copy of map. Subsequent changes to map will not be -- | visible through applying operations to the copy of map. -- | Assignment or parameter passing without copying will result -- | in a single mapping value being shared among mapping objects. -- | Raises Uninitialized_Mapping iff map has not been initialized. -- | The assignment operation is used to transfer the values of the -- | key_type and value_type type components of map; consequently, -- | changes in the values of these types may be observable through -- | both mappings if these are access types, or if they contain -- | components of an access type. -- Query Operations: function Is_Empty (Map : Mapping) return boolean; -- | Raises: Uninitialized_Mapping -- | Effects: -- | Return map = {}. -- | Raises Uninitialized_Mapping iff map has not been initialized. function Size (Map : Mapping) return natural; -- | Raises: Uninitialized_Mapping -- | Effects: -- | Return |map|, the number of bindings in map. -- | Raises Uninitialized_Mapping iff map has not been initialized. function Is_Bound (Map : Mapping; Key : Key_Type) return boolean; -- | Raises: Uninitialized_Mapping -- | Return true iff Equal (Key, K) for some in map. -- | Raises Uninitialized_Mapping iff map has not been initialized. function Fetch (Map : Mapping; Key : Key_Type) return Value_Type; -- | Raises: Not_bound, Uninitialized_Mapping -- | If , where Equal (Key, K), is in Map, then return v. -- | Raises Not_Bound if no such exists. -- | Raises Uninitialized_Mapping iff map has not been initialized. -- Iterators: function Make_Keys_Iter (Map : Mapping) return Keys_Iter; -- | Raises: Uninitialized_Mapping -- | Effects: -- | Create and return a keys iterator based on map. This object -- | can then be used in conjunction with the more function and the -- | next procedure to iterate over all keys that are bound in map. -- | Raises Uninitialized_Mapping iff map has not been initialized. function More (Iter : Keys_Iter) return boolean; -- | Effects: -- | Return true iff the keys iterator has not been exhausted. procedure Next (Iter : in out Keys_Iter; Key : out Key_Type); -- | Raises: No_More -- | Effects: -- | Let Iter be based on the mapping, map. Successive calls of Next -- | will return the bound keys of map in some arbitrary order. -- | After all bound keys have been returned, then the procedure will -- | raise No_More. -- | Requires: -- | Map must not be changed between the invocations of -- | Make_Keys_Iterator (Map) and Next. function Make_Values_Iter (Map : Mapping) return Values_Iter; -- | Raises: Uninitialized_Mapping -- | Effects: -- | Create and return a values iterator based on Map. This object -- | can then be used in conjunction with the more function and the -- | next procedure to iterate over all values that are bound to keys -- | in Map. -- | Raises Uninitialized_Mapping iff Map has not been initialized. function More (Iter : Values_Iter) return boolean; -- | Effects: -- | Return true iff the values iterator has not been exhausted. procedure Next (Iter : in out Values_Iter; Val : out Value_Type); -- | Raises: No_More -- | Effects: -- | Let Iter be based on the mapping, map. Successive calls of Next -- | will return the bound values of map in some arbitrary order. -- | After all bound values have been returned, then the procedure -- | will raise No_More. -- | Requires: -- | Map must not be changed between the invocations of -- | Make_Values_Iterator (Map) and Next. function Make_Bindings_Iter (Map : Mapping) return Bindings_Iter; -- | Raises: Uninitialized_Mapping -- | Effects: -- | Create and return a bindings iterator based on map. This object -- | can then be used in conjunction with the more function and the -- | next procedure to iterate over all key/value pairs in map. -- | Raises Uninitialized_Mapping iff map has not been initialized. function More (Iter : Bindings_Iter) return boolean; -- | Effects: -- | Return true iff the bindings iterator has not been exhausted. procedure Next (Iter : in out Bindings_Iter; Key : out Key_Type; Val : out Value_Type); -- | Raises: No_More -- | Effects: -- | Let iter be based on the mapping, map. Successive calls of next -- | will return the key/value pairs of map in some arbitrary order. -- | After all such pairs have been returned, then the procedure will -- | raise No_More. -- | Requires: -- | Map must not be changed between the invocations of -- | Make_Bindings_Iterator (Map) and Next. -- Heap management: procedure Destroy (M : in out Mapping); -- | Effects: -- | Return space consumed by mapping value associated with object -- | M to the heap. (If M is uninitialized, this operation does -- | nothing.) If other objects share the same mapping value, the -- | further use of these objects is erroneous. Components of type -- | value_type, if they are access types, are not garbage collected. -- | It is the user's responsibility to dispose of these objects. -- | M is left in the uninitialized state. private type Component is record Key : Key_Type; Val : Value_Type; end record; function Equal (C1, C2 : Component) return boolean; -- | Effects: Return true iff Equal (C1.Key, C2.Key). package Bucket_Pkg is new Util.LLists (Component, Equal); use Bucket_Pkg; type Bucket_Array is array (Bucket_Range) of Bucket_Pkg.List; type Mapping_Rec is record Size : natural; Buckets : Bucket_Array; end record; type Mapping is access Mapping_Rec; -- | Representation Invariants: -- | 1. r /= null. (This would be the uninitialized case) -- | 2. If for some i, a component, c, is in bucket r.buckets (i), -- | then hash (c.key) = i. -- | 3. If a component, c1, is in bucket, r.buckets (i), then there is -- | no other c2 in r.buckets (i) such that equal (c1, c2). -- | (Enforce one binding to a given key at any time.) -- | 4. r.size equals the total number of components in buckets -- | r.buckets (bucket_range'first) through -- | r.buckets (bucket_range'last). -- | -- | Abstraction Function: -- | A (r) is the set consisting of all key, value pairs that appear as -- | components in buckets r.buckets (bucket_range'first) through -- | r.buckets (bucket_range'last). type General_Iter is record Map : Mapping; Current : Bucket_Range; Position : List_Iterator; end record; -- | For a given General_Iter, i, the Make, More and Next operations -- | have the following effects: -- | Make: Sets map field to the given mapping, sets i.current to the -- | lowest idx of a nonempty bucket, and sets i.position to the head -- | of that bucket. -- | More: Returns not empty (i.position). -- | Next: key, val fields of first component of i.position. -- | Advances i.position to next component in bucket, if it exists. -- | Otherwise, increments i.current until a nonempty bucket, and sets -- | i.position to this bucket. When this fails, sets i.position to an -- | empty bucket. type Keys_Iter is new General_Iter; type Values_Iter is new General_Iter; type Bindings_Iter is new General_Iter; end Util.Hashed_Mapping;