OpenCores
URL https://opencores.org/ocsvn/openrisc/openrisc/trunk

Subversion Repositories openrisc

[/] [openrisc/] [trunk/] [gnu-dev/] [or1k-gcc/] [gcc/] [ada/] [a-cfhama.ads] - Blame information for rev 706

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 706 jeremybenn
------------------------------------------------------------------------------
2
--                                                                          --
3
--                         GNAT LIBRARY COMPONENTS                          --
4
--                                                                          --
5
--    A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ M A P S     --
6
--                                                                          --
7
--                                 S p e c                                  --
8
--                                                                          --
9
--          Copyright (C) 2004-2011, Free Software Foundation, Inc.         --
10
--                                                                          --
11
-- This specification is derived from the Ada Reference Manual for use with --
12
-- GNAT. The copyright notice above, and the license provisions that follow --
13
-- apply solely to the  contents of the part following the private keyword. --
14
--                                                                          --
15
-- GNAT is free software;  you can  redistribute it  and/or modify it under --
16
-- terms of the  GNU General Public License as published  by the Free Soft- --
17
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
18
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
19
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
20
-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
21
--                                                                          --
22
-- As a special exception under Section 7 of GPL version 3, you are granted --
23
-- additional permissions described in the GCC Runtime Library Exception,   --
24
-- version 3.1, as published by the Free Software Foundation.               --
25
--                                                                          --
26
-- You should have received a copy of the GNU General Public License and    --
27
-- a copy of the GCC Runtime Library Exception along with this program;     --
28
-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
29
-- <http://www.gnu.org/licenses/>.                                          --
30
------------------------------------------------------------------------------
31
 
32
--  This spec is derived from package Ada.Containers.Bounded_Hashed_Maps in the
33
--  Ada 2012 RM. The modifications are to facilitate formal proofs by making it
34
--  easier to express properties.
35
 
36
--  The modifications are:
37
 
38
--    A parameter for the container is added to every function reading the
39
--    contents of a container: Key, Element, Next, Query_Element, Has_Element,
40
--    Iterate, Equivalent_Keys. This change is motivated by the need to have
41
--    cursors which are valid on different containers (typically a container C
42
--    and its previous version C'Old) for expressing properties, which is not
43
--    possible if cursors encapsulate an access to the underlying container.
44
 
45
--    There are four new functions:
46
 
47
--      function Strict_Equal (Left, Right : Map) return Boolean;
48
--      function Overlap (Left, Right : Map) return Boolean;
49
--      function Left  (Container : Map; Position : Cursor) return Map;
50
--      function Right (Container : Map; Position : Cursor) return Map;
51
 
52
--    See detailed specifications for these subprograms
53
 
54
private with Ada.Containers.Hash_Tables;
55
private with Ada.Streams;
56
 
57
generic
58
   type Key_Type is private;
59
   type Element_Type is private;
60
 
61
   with function Hash (Key : Key_Type) return Hash_Type;
62
   with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
63
   with function "=" (Left, Right : Element_Type) return Boolean is <>;
64
 
65
package Ada.Containers.Formal_Hashed_Maps is
66
   pragma Pure;
67
 
68
   type Map (Capacity : Count_Type; Modulus : Hash_Type) is tagged private;
69
   pragma Preelaborable_Initialization (Map);
70
 
71
   type Cursor is private;
72
   pragma Preelaborable_Initialization (Cursor);
73
 
74
   Empty_Map : constant Map;
75
 
76
   No_Element : constant Cursor;
77
 
78
   function "=" (Left, Right : Map) return Boolean;
79
 
80
   function Capacity (Container : Map) return Count_Type;
81
 
82
   procedure Reserve_Capacity
83
     (Container : in out Map;
84
      Capacity  : Count_Type);
85
 
86
   function Length (Container : Map) return Count_Type;
87
 
88
   function Is_Empty (Container : Map) return Boolean;
89
 
90
   --  ??? what does clear do to active elements?
91
   procedure Clear (Container : in out Map);
92
 
93
   procedure Assign (Target : in out Map; Source : Map);
94
 
95
   --  ???
96
   --  capacity=0 means use container.length as cap of tgt
97
   --  modulos=0 means use default_modulous(container.length)
98
   function Copy
99
     (Source   : Map;
100
      Capacity : Count_Type := 0) return Map;
101
 
102
   function Key (Container : Map; Position : Cursor) return Key_Type;
103
 
104
   function Element (Container : Map; Position : Cursor) return Element_Type;
105
 
106
   procedure Replace_Element
107
     (Container : in out Map;
108
      Position  : Cursor;
109
      New_Item  : Element_Type);
110
 
111
   procedure Query_Element
112
     (Container : in out Map;
113
      Position  : Cursor;
114
      Process   : not null access
115
                    procedure (Key : Key_Type; Element : Element_Type));
116
 
117
   procedure Update_Element
118
     (Container : in out Map;
119
      Position  : Cursor;
120
      Process   : not null access
121
                    procedure (Key : Key_Type; Element : in out Element_Type));
122
 
123
   procedure Move (Target : in out Map; Source : in out Map);
124
 
125
   procedure Insert
126
     (Container : in out Map;
127
      Key       : Key_Type;
128
      New_Item  : Element_Type;
129
      Position  : out Cursor;
130
      Inserted  : out Boolean);
131
 
132
   procedure Insert
133
     (Container : in out Map;
134
      Key       : Key_Type;
135
      Position  : out Cursor;
136
      Inserted  : out Boolean);
137
 
138
   procedure Insert
139
     (Container : in out Map;
140
      Key       : Key_Type;
141
      New_Item  : Element_Type);
142
 
143
   procedure Include
144
     (Container : in out Map;
145
      Key       : Key_Type;
146
      New_Item  : Element_Type);
147
 
148
   procedure Replace
149
     (Container : in out Map;
150
      Key       : Key_Type;
151
      New_Item  : Element_Type);
152
 
153
   procedure Exclude (Container : in out Map; Key : Key_Type);
154
 
155
   procedure Delete (Container : in out Map; Key : Key_Type);
156
 
157
   procedure Delete (Container : in out Map; Position : in out Cursor);
158
 
159
   function First (Container : Map) return Cursor;
160
 
161
   function Next (Container : Map; Position : Cursor) return Cursor;
162
 
163
   procedure Next (Container : Map; Position : in out Cursor);
164
 
165
   function Find (Container : Map; Key : Key_Type) return Cursor;
166
 
167
   function Contains (Container : Map; Key : Key_Type) return Boolean;
168
 
169
   function Element (Container : Map; Key : Key_Type) return Element_Type;
170
 
171
   function Has_Element (Container : Map; Position : Cursor) return Boolean;
172
 
173
   function Equivalent_Keys
174
     (Left   : Map;
175
      CLeft  : Cursor;
176
      Right  : Map;
177
      CRight : Cursor) return Boolean;
178
 
179
   function Equivalent_Keys
180
     (Left  : Map;
181
      CLeft : Cursor;
182
      Right : Key_Type) return Boolean;
183
 
184
   function Equivalent_Keys
185
     (Left   : Key_Type;
186
      Right  : Map;
187
      CRight : Cursor) return Boolean;
188
 
189
   procedure Iterate
190
     (Container : Map;
191
      Process   : not null access
192
                    procedure (Container : Map; Position : Cursor));
193
 
194
   function Default_Modulus (Capacity : Count_Type) return Hash_Type;
195
 
196
   function Strict_Equal (Left, Right : Map) return Boolean;
197
   --  Strict_Equal returns True if the containers are physically equal, i.e.
198
   --  they are structurally equal (function "=" returns True) and that they
199
   --  have the same set of cursors.
200
 
201
   function Left  (Container : Map; Position : Cursor) return Map;
202
   function Right (Container : Map; Position : Cursor) return Map;
203
   --  Left returns a container containing all elements preceding Position
204
   --  (excluded) in Container. Right returns a container containing all
205
   --  elements following Position (included) in Container. These two new
206
   --  functions can be used to express invariant properties in loops which
207
   --  iterate over containers. Left returns the part of the container already
208
   --  scanned and Right the part not scanned yet.
209
 
210
   function Overlap (Left, Right : Map) return Boolean;
211
   --  Overlap returns True if the containers have common keys
212
 
213
private
214
   pragma Inline (Length);
215
   pragma Inline (Is_Empty);
216
   pragma Inline (Clear);
217
   pragma Inline (Key);
218
   pragma Inline (Element);
219
   pragma Inline (Contains);
220
   pragma Inline (Capacity);
221
   pragma Inline (Has_Element);
222
   pragma Inline (Equivalent_Keys);
223
   pragma Inline (Next);
224
 
225
   type Node_Type is record
226
      Key         : Key_Type;
227
      Element     : Element_Type;
228
      Next        : Count_Type;
229
      Has_Element : Boolean := False;
230
   end record;
231
 
232
   package HT_Types is new
233
     Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types
234
       (Node_Type);
235
 
236
   type Map (Capacity : Count_Type; Modulus : Hash_Type) is
237
      new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
238
 
239
   use HT_Types;
240
   use Ada.Streams;
241
 
242
   procedure Write
243
     (Stream    : not null access Root_Stream_Type'Class;
244
      Container : Map);
245
 
246
   for Map'Write use Write;
247
 
248
   procedure Read
249
     (Stream    : not null access Root_Stream_Type'Class;
250
      Container : out Map);
251
 
252
   for Map'Read use Read;
253
 
254
   type Map_Access is access all Map;
255
   for Map_Access'Storage_Size use 0;
256
 
257
   type Cursor is record
258
      Node : Count_Type;
259
   end record;
260
 
261
   procedure Read
262
     (Stream : not null access Root_Stream_Type'Class;
263
      Item   : out Cursor);
264
 
265
   for Cursor'Read use Read;
266
 
267
   procedure Write
268
     (Stream : not null access Root_Stream_Type'Class;
269
      Item   : Cursor);
270
 
271
   for Cursor'Write use Write;
272
 
273
   Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
274
 
275
   No_Element : constant Cursor := (Node => 0);
276
 
277
end Ada.Containers.Formal_Hashed_Maps;

powered by: WebSVN 2.1.0

© copyright 1999-2024 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.