169
170
171
172
173
174
175
176
177
178
179
180
181
182
|
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
+
+
+
|
function Iterate (Container : in Constant_Map)
return Map_Iterator_Interfaces.Reversible_Iterator'Class;
function Iterate (Container : in Constant_Map; Start : in Cursor)
return Map_Iterator_Interfaces.Reversible_Iterator'Class;
function Iterate (Container : in Constant_Map; First, Last : in Cursor)
return Map_Iterator_Interfaces.Reversible_Iterator'Class;
type Constant_Reference_Type
(Element : not null access constant Element_Type) is private
with Implicit_Dereference => Element;
function Constant_Reference
(Container : aliased in Constant_Map;
|
338
339
340
341
342
343
344
345
346
347
348
349
350
351
|
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
|
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
|
with Pre => Position.Is_Empty
or else Backend_Refs."=" (Position.Backend, Object.Backend);
overriding function Previous
(Object : Iterator;
Position : Cursor) return Cursor
is (Previous (Position))
with Pre => Position.Is_Empty
or else Backend_Refs."=" (Position.Backend, Object.Backend);
type Range_Iterator is new Map_Iterator_Interfaces.Reversible_Iterator
with record
Backend : Backend_Refs.Immutable_Reference;
First_Position : Cursor;
Last_Position : Cursor;
end record;
-- with Dynamic_Predicate => not Range_Iterator.Backend.Is_Empty
-- and then Has_Element (Range_Iterator.First_Position)
-- and then Has_Element (Range_Iterator.Last_Position)
-- and then not Range_Iterator.First_Position
-- > Range_Iterator.Last_Position;
overriding function First (Object : Range_Iterator) return Cursor;
overriding function Last (Object : Range_Iterator) return Cursor;
overriding function Next
(Object : Range_Iterator;
Position : Cursor) return Cursor
with Pre => Position.Is_Empty
or else Backend_Refs."=" (Position.Backend, Object.Backend);
overriding function Previous
(Object : Range_Iterator;
Position : Cursor) return Cursor
with Pre => Position.Is_Empty
or else Backend_Refs."=" (Position.Backend, Object.Backend);
No_Element : constant Cursor := (Is_Empty => True);
end Natools.Constant_Indefinite_Ordered_Maps;
|