⟦e8ee09023⟧

TextFile

generic
    type Elem_Type is private;
    --| Component element type.

    with function Equal (E1, E2 : in Elem_Type) return Boolean is "=";
    --| An equality relation on elem_type.

package Dynarray_Pkg is

    --| Overview:
    --| This package provides the dynamic array (darray) abstract data type.
    --| A darray has completely dynamic bounds, which change during runtime as
    --| elements are added to/removed from the top/bottom. darrays are similar
    --| to deques, differing only in that operations for indexing into the
    --| structure are also provided.  A darray is indexed by integers that
    --| fall within the current bounds.  The component type, elem_type, of a
    --| darray is a generic formal parameter of this package, along with a
    --| function, equal, that is assumed to form an equality relation over
    --| over elem_type.
    --|
    --| The notation, <first, elts>, will be used to denote a darray.
    --| first is the current low bound of the darray.  elts is the sequence
    --| of elements contained in the darray.  For a given darray, d, the
    --| dot selection mechanism is used to refer to these components, e.g.,
    --| d.first and d.elts.  & is used for sequence concatenation, and also
    --| for prepending/postpending a single element to a sequence.  |s| is
    --| the number of elements in a sequence, s, and () is the null sequence.
    --| Standard Ada array indexing notation is adopted for sequences.
    --|
    --| The following is a complete list of operations, written in the order
    --| in which they appear in the spec:
    --|
    --| Constructors:
    --|        create
    --|        array_to_darray
    --|        set_first
    --|        add_low, add_high
    --|        remove_low, remove_high
    --|        store
    --|        copy, copy_deep (generic)
    --|
    --| Query Operations:
    --|        fetch
    --|        low, high
    --|        first, last
    --|        is_empty
    --|        length
    --|        equal
    --|
    --| Iterators:
    --|        make_elements_iter, more, next
    --|
    --| Heap Management:
    --|        destroy
    --|

    --| Notes:
    --| Programmer: Ron Kownacki

    -- Primary Types:

    type Darray is private;  --| The darray abstract data type.

    type Array_Type is array (Integer range <>) of Elem_Type;
    --| darray/array_type conversion operations are provided.


    -- Storage Management Constants and Types:  (see create procedure)

    Default_Predict : constant Positive := 100;

    Default_High : constant Positive := 50;

    Default_Expand : constant Positive := 100;


    -- Exceptions:

    No_More : exception;  --| Raised on incorrect use of an iterator.

    Out_Of_Bounds : exception;  --| Raised on index out of current bounds.

    Uninitialized_Darray : exception;
    --| Raised on use of uninitialized darray by most operations.


    -- Iterators:

    type Elements_Iter is private;  --| Component elements iterator.


    -- Constructors:

    procedure Create (First : in Integer := 1;
                      Predict : in Positive := Default_Predict;
                      High_Percent : in Positive := Default_High;
                      Expand_Percent : in Positive := Default_Expand;
                      D : in out Darray);

    --| Effects:
    --| Sets d to <first, ()>.  If d has previously been initialized,
    --| then a destroy(d) is first performed.  The predict parameter
    --| specifies the initial space allocated.  (predict  = #elements).
    --| The high_percent parameter is the caller's expectation of the
    --| percentage of add_highs, out of total adds, to the darray.  For
    --| example, a caller would specify 100 if it was known that no
    --| add_lows would be performed.  The expand_percent parameter
    --| specifies the amount of additional space, as a percentage of
    --| currently allocated space, that is to be allocated whenever an
    --| expansion becomes necessary.  For example, 100 doubles the
    --| allocated space.

    procedure Array_To_Darray (A : in Array_Type;
                               First : in Integer := 1;
                               Predict : in Positive;
                               High_Percent : in Positive := Default_High;
                               Expand_Percent : in Positive := Default_Expand;
                               D : in out Darray);

    --| Raises: out_of_bounds
    --| Effects:
    --| Sets d to <first, a(a'first..a'last)>.  If d has previously
    --| been initialized, then an implicit destroy(d) is performed.
    --| The high_percent and expand_percent parameters are defined
    --| as for create.  Raises out_of_bounds iff predict < a'length.

    procedure Set_First (D : in out Darray; First : in Integer);

    --| Raises: uninitialized_darray
    --| Effects:
    --| Sets d.first to first.
    --| Raises uninitialized_darray if d has not been initialized.

    procedure Add_Low (D : in out Darray; E : in Elem_Type);

    --| Raises: uninitialized_darray
    --| Effects:
    --| Sets d to <d.first - 1, e & d.elts>.
    --| Raises uninitialized_darray if d has not been initialized.

    procedure Add_High (D : in out Darray; E : in Elem_Type);

    --| Raises: uninitialized_darray
    --| Effects:
    --| Sets d.elts to d.elts & e.
    --| Raises uninitialized_darray if d has not been initialized.

    procedure Remove_Low (D : in out Darray);

    --| Raises: out_of_bounds, uninitialized_darray
    --| Effects:
    --| Sets d to <d.first + 1, d.elts(d.first + 1 .. last(d))>.
    --| Raises out_of_bounds iff is_empty(d).
    --| Raises uninitialized_darray if d has not been initialized.

    procedure Remove_High (D : in out Darray);

    --| Raises: out_of_bounds, uninitialized_darray
    --| Effects:
    --| Sets d.elts to d.elts(d.first..last(d) - 1).
    --| Raises out_of_bounds iff is_empty(d).
    --| Raises uninitialized_darray if d has not been initialized.

    procedure Store (D : in out Darray; I : in Integer; E : in Elem_Type);

    --| Raises: out_of_bounds, uninitialized_darray
    --| Effects:
    --| Replaces d.elts(i) with e.  Raises out_of_bounds iff
    --| either is_empty(d) or i is not in d.first..last(d).
    --| Raises uninitialized_darray if d has not been initialized.

    function Copy (D : in Darray) return Darray;

    --| Raises: uninitialized_darray
    --| Effects:
    --| Returns a copy of d.  Subsequent changes to the structure of d
    --| will not be visible through the application of operations to
    --| the copy of d, and vice versa.  Assignment or parameter passing
    --| without using copy (or copy_deep, described below) will result
    --| in a single darray value being shared among objects.
    --| Raises uninitialized_darray if d has not been initialized.
    --| The assignment operation is used to transfer the values of
    --| the elem_type component objects of d; consequently, changes
    --| in these values may be observable through both darrays if
    --| elem_type is an access type, or contains access type
    --| components.

    generic
        with function Copy (E : in Elem_Type) return Elem_Type;

    function Copy_Deep (D : in Darray) return Darray;

    --| Raises: uninitialized_darray
    --| Effects:
    --| Returns a copy of d.  Subsequent changes to the structure of d
    --| will not be visible through the application of operations to
    --| the copy of d, and vice versa.  Assignment or parameter passing
    --| without using copy_deep or copy will result in a single
    --| darray value being shared among objects.
    --| Raises uninitialized_darray if d has not been initialized.
    --| The transfer of elem_type component objects is accomplished by
    --| using the assignment operation in conjunction with the copy
    --| function.  Consequently, the user can prevent sharing of
    --| elem_type access components.


    -- Query Operations:

    function Fetch (D : in Darray; I : in Integer) return Elem_Type;

    --| Raises: out_of_bounds, uninitialized_darray
    --| Effects:
    --| Returns d.elts(i).  Raises out_of_bounds iff either is_empty(d)
    --| or i is not in d.first..last(d).
    --| Raises uninitialized_darray if d has not been initialized.

    function Low (D : in Darray) return Elem_Type;

    --| Raises: out_of_bounds, uninitialized_darray
    --| Effects:
    --| Returns d.elts(d.first).  Raises out_of_bounds iff is_empty(d).
    --| Raises uninitialized_darray if d has not been initialized.

    function High (D : in Darray) return Elem_Type;

    --| Raises: out_of_bounds, uninitialized_darray
    --| Effects:
    --| Returns d.elts(last(d)).  Raises out_of_bounds iff is_empty(d).
    --| Raises uninitialized_darray if d has not been initialized.

    function First (D : in Darray) return Integer;

    --| Raises: uninitialized_darray
    --| Effects:
    --| Returns d.first.
    --| Raises uninitialized_darray if d has not been initialized.

    function Last (D : in Darray) return Integer;

    --| Raises: uninitialized_darray
    --| Effects:
    --| Returns d.first + |d.elts| - 1.
    --| Raises uninitialized_darray if d has not been initialized.

    function Is_Empty (D : in Darray) return Boolean;

    --| Raises: uninitialized_darray
    --| Effects:
    --| Returns length(d) = 0, or equivalently, last(d) < d.first.
    --| Raises uninitialized_darray if d has not been initialized.

    function Length (D : in Darray) return Natural;

    --| Raises: uninitialized_darray
    --| Effects:
    --| Returns |d.elts|.
    --| Raises uninitialized_darray if d has not been initialized.

    function Equal (D1, D2 : in Darray) return Boolean;

    --| Raises: uninitialized_darray
    --| Effects:
    --| Return (d1.first = d2.first and
    --|         last(d1) = last(d2) and
    --|         for each i in d1.first..last(d1),
    --|             equal(d1.elts(i), d2.elts(i)).
    --| Raises uninitialized_darray if either d1 or d2 has not been
    --| initialized.  Note that (d1 = d2) implies that equal(d1, d2)
    --| will always hold.  "=" is object equality, equal is state
    --| equality.

    function Darray_To_Array (D : in Darray) return Array_Type;

    --| Raises: uninitialized_darray
    --| Effects:
    --| Let bounds_range be d.first..d.first + length(d) - 1.  If
    --| bounds_range is empty, then return an empty array with bounds
    --| of 1..0.  Otherwise, return bounds_range'(d.elts).
    --| Raises uninitialized_darray if d has not been initialized.


    -- Iterators:

    function Make_Elements_Iter (D : in Darray) return Elements_Iter;

    --| Raises: uninitialized_darray
    --| Effects:
    --| Create and return an elements itererator based on d.  This
    --| object can then be used in conjunction with the more function
    --| and the next procedure to iterate over the components of d.
    --| Raises uninitialized_darray if d has not been initialized.

    function More (Iter : in Elements_Iter) return Boolean;

    --| Effects:
    --| Return true iff the elements iterator has not been exhausted.

    procedure Next (Iter : in out Elements_Iter; E : out Elem_Type);

    --| Raises: no_more
    --| Effects:
    --| Let iter be based on the darray, d.  Successive calls of next
    --| will return, in e, successive elements of d.elts.  Each call
    --| updates the state of the elements iterator.  After all elements
    --| have been returned, an invocation of next will raise no_more.
    --| Requires:
    --| d must not be changed between the invocations of
    --| make_elements_iterator(d) and next.


    -- Heap Management:

    procedure Destroy (D : in out Darray);
    --| Effects:
    --| Return space consumed by the darray value associated with object
    --| d to the heap.  (If d is uninitialized, this operation does
    --| nothing.)  If other objects share the same darray value, then
    --| further use of these objects is erroneous.  Components of type
    --| elem_type, if they are access types, are not garbage collected.
    --| It is the user's responsibility to dispose of these objects.
    --| d is left in the uninitialized state.


private

    type Array_Ptr is access Array_Type;

    type Darray_Info is
        record
            First_Idx : Positive;
            Last_Idx : Natural;
            First : Integer;
            High_Percent : Positive;
            Expand_Percent : Positive;
            Arr : Array_Ptr := null;
        end record;

    type Darray is access Darray_Info;

    --| Let r be an instance of the representation type.
    --| Representation Invariants:
    --| 1. r /= null, r.arr /= null (must be initialized to be valid.)
    --| 2. r.arr'first = 1 and
    --|    r.arr'last >= 1
    --| 3. r.first_idx <= r.last_idx or
    --|    r.first_idx = r.last_idx + 1
    --| 4. r.first_idx <= r.last_idx =>
    --|        r.first_idx, r.last_idx in r.arr'range
    --| 5. r.expand_percent, r.high_percent get values at creation time,
    --|    and these never change.
    --|
    --| Abstraction Function:  (denoted by A(r))
    --| if r.last_idx < r.first_idx then
    --|     <r.first, ()>
    --| else
    --|     <r.first, (r.arr(r.first_idx),...,r.arr(r.last_idx))>
    --|
    --| These properties follow:
    --| 1. length(A(r)) = r.last_idx - r.first_idx + 1
    --| 2. last(A(r)) = r.first + r.last_idx - r.first_idx
    --| 3. fetch(A(r), i) =
    --|        if (i - r.first + r.first_idx) in r.first_idx..r.last_idx
    --|            then r.arr(i - r.first + r.first_idx)
    --|            else undefined.  (out_of_bounds)

    type Elements_Iter is
        record
            Last : Integer := 0;
            Current : Integer := 1;
            Arr : Array_Ptr;
        end record;

    --| Let d be the darray that an elements_iter, i, is based on.
    --| Initially, i.current = d.first_idx, i.last = d.last_idx, and
    --| i.arr = d.arr.
    --| more(i) = i.current <= i.last.
    --| next(i) = i.arr(current).  i.current incremented by next.
    --| Note that if an elements_iter object is not initialized, then
    --| more is false.

end Dynarray_Pkg;
DataMuseum.dk

Rational R1000/400 Tapes

⟦e8ee09023⟧ TextFile

Derivation

TextFile
