Celestin Apprentice 5/Apprentice-Release5.iso/Environments/SmallEiffel 0.3.3/SmallEiffel PPC/lib_std/array.e

Text File | 1996-06-13 | 7.9 KB | 410 lines | [TEXT/EDIT]

-- Part of SmallEiffel -- Read DISCLAIMER file -- Copyright (C)
-- Dominique COLNET and Suzanne COLLIN -- [e-mail]
--
class ARRAY[E]
--
-- General purpose arrays.
--

inherit
   COLLECTION[E]
      redefine eval_read_attribute, eval_write_attribute
      end;

creation make

feature {NONE}

   storage: POINTER;
     -- Internal access to storage location.

feature

   capacity: INTEGER;
     -- Internal storage capacity in number of item.

   lower: INTEGER;
     -- Lower index bound.

   upper: INTEGER;
     -- Upper index bound.

feature -- Creation and Modification :

   make(minindex, maxindex: INTEGER) is
     -- Make array with range [minindex .. maxindex].
     -- When maxindex = minindex - 1, the array is empty.
      require
     minindex -1 <= maxindex
      do
     if storage.is_not_void then
        free_pointer(storage);
     end;
     lower := minindex;
     upper := maxindex;
     capacity := maxindex - minindex + 1;
     if capacity > 0 then
        if capacity < 16 then capacity := 16 end;
        storage := malloc(capacity);
        clear_all;
     end;
      ensure
     lower = minindex;
     upper = maxindex;
     all_cleared;
      end;

feature -- Modification :

   resize(minindex, maxindex: INTEGER) is
     -- Resize the array. No elements will be lost in the
     -- intersection of [old lower .. old upper] and
     -- [minindex .. maxindex].
     -- New positions are initialized with appropriate
     -- default values.
      require
     minindex <= maxindex
      local
     other: like Current;
     i, up: INTEGER;
      do
     from
        !!other.make(minindex,maxindex);
        i := lower.max(other.lower);
        up := upper.min(other.upper);
     until
        i > up
     loop
        other.put(item(i),i);
        i := i + 1;
     end;
     if storage.is_not_void then
        free_pointer(storage);
     end;
     standard_copy(other);
     other.free_array;
      end;

feature -- No modification :

   item, infix "@" (index: INTEGER): E is
      external "CSE"
      end;

feature -- Modification :

   put(element: E; index: INTEGER) is
      external "CSE"
      end;

   force(element: E; index: INTEGER) is
     -- Put `element' at position `index'.
     -- Resize array, if `index' is not
     -- inside current bounds.
      do
     if upper < index then
        resize(lower,index);
     elseif index < lower then
        resize(index,upper);
     end;
     put(element,index);
      ensure
     valid_index(index);
     item(index) = element;
      end;

   clear is
     -- Empty the array, discard all items.
      do
     upper := lower - 1;
      ensure
     empty;
      end;

   copy(other: like Current) is
     -- Copy `other' onto Current.
      local
     i: INTEGER;
      do
     upper := lower - 1;
     if capacity = 0 then
        make(other.lower,other.upper);
     else
        resize(other.lower,other.upper);
     end;
     from
        i := lower;
     until
        i > upper
     loop
        put(other.item(i),i);
        i := i + 1;
     end;
      end;

   remove(index: INTEGER) is
     -- Remove one element at position `index'. Followings
     -- elements (after `index') are moved one position left.
      require
     valid_index(index);
      local
     i: INTEGER;
      do
     from
        i := index;
     until
        i + 1 > upper
     loop
        put(item(i + 1),i);
        i := i + 1;
     end;
     upper := upper - 1;
      ensure
     count + 1 = old count;
     upper + 1 = old upper;
      end;

   remove_last is
      require
     not empty;
      do
     upper := upper - 1;
      ensure
     count + 1 = old count;
     lower = old lower
      end;

   remove_first is
      require
     not empty;
      local
     i: INTEGER;
      do
     from
        i := lower;
     until
        i = upper
     loop
        put(item(i+1),i);
        i := i + 1;
     end;
     lower := lower + 1;
      ensure
     count + 1 = old count;
     upper = old upper;
      end;

feature -- Adding Elements :

   add_last(elt: E) is
      do
     if storage = Void then end;
     if capacity < count + 1 then
        if capacity = 0 then
           capacity := 16;
           storage := malloc(capacity);
        else
           capacity := capacity + 16;
           storage := realloc(storage,capacity);
        end;
     end;
     upper := upper + 1;
     put(elt,upper);
      ensure
     last = elt;
     count = 1 + old count
      end;

   add(elt: E) is
      do
     if not has(elt) then
        add_last(elt);
     end;
      ensure
     has(elt);
     count >= old count;
      end;

   fast_add(elt: E) is
      do
     if not fast_has(elt) then
        add_last(elt);
     end;
      ensure
     fast_has(elt);
     count >= old count;
      end;

   insert(element : E; index: INTEGER) is
     -- Insert `element' after position `index'.
     -- Element at position `upper' will be lost!
      require
     inside_bounds: lower - 1 <= index and then index < upper
     -- Note: Insertion is AFTER `index'!
      do
     if index < upper - 1 then
        move(index+1,upper-1,1);
     end;
     put (element, index + 1);
      end;

   sub_array(low, up: INTEGER): ARRAY[E] is
      require
     valid_index(low);
     valid_index(up);
     low <= up
      local
     i: INTEGER;
      do
     from
        !!Result.make(low,up);
        i := low;
     until
        i > up
     loop
        Result.put(item(i),i);
        i := i + 1;
     end;
      ensure
     Result.lower = low;
     Result.upper = up;
      end;

feature -- Other Features :

   put_first(elt: E) is
     -- Put `elt' at the first free place
     -- or `add_last' it no Void places.
      local
     i: INTEGER;
     null: E;
      do
     from
        i := lower;
     until
        i > upper or else item(i) = null
     loop
        i := i + 1;
     end;
     if i > upper then
        add_last(elt);
     else
        put(elt,i);
     end;
      end;

   take_first: E is
     -- Take the first element non Void or not set to
     -- the default value. Then set the corresponding
     -- place to the default value.
      local
     i: INTEGER;
     null: E;
      do
     from
        i := lower;
     until
        i > upper or else Result /= null
     loop
        Result := item(i);
        i := i + 1;
     end;
     if i <= upper then
        put(null,i-1);
     end;
      ensure
     count = old count;
      end;

feature -- Interfacing with C :

   to_external: POINTER is
     -- Gives C access into the internal `storage' of the ARRAY.
     -- Result is pointing the element at index `lower'.
     --
     -- NOTE: do not free/realloc the Result. Resizing of the array
     --       can makes this pointer invalid.
      require
     not empty
      do
     Result := storage;
      ensure
     Result.is_not_void
      end;

feature {NONE}

   malloc(size: INTEGER): POINTER is
      require
     size > 0
      local
     x: like item;
      do
     c_inline_c("R=malloc((size_t)(a1*sizeof(_x)));");
      end;

   realloc(pointer: POINTER; size: INTEGER): POINTER is
      require
     size > 0
      local
     x: like item;
      do
     c_inline_c("R=realloc(a1,((size_t)(a2*sizeof(_x))));");
      end;

   free_pointer(p: POINTER) is
      require
     p.is_not_void
      external "C"
      alias "free"
      end;

feature {ARRAY}

   free_array is
      external "CWC"
      alias "free"
      end;

feature -- To implement eval :

   eval_read_attribute(name: STRING; dest: POINTER) is
      do
     if ("capacity").is_equal(name) then
        eval_virtual_machine.put_integer(dest,capacity);
     elseif ("lower").is_equal(name) then
        eval_virtual_machine.put_integer(dest,lower);
     elseif ("upper").is_equal(name) then
        eval_virtual_machine.put_integer(dest,upper);
     else
        check
           ("storage").is_equal(name)
        end;
        eval_virtual_machine.put_pointer(dest,storage);
     end;
      end;

   eval_write_attribute(name: STRING; source: POINTER) is
      do
     if ("capacity").is_equal(name) then
        capacity := eval_virtual_machine.get_integer(source);
     elseif ("lower").is_equal(name) then
        lower := eval_virtual_machine.get_integer(source);
     elseif ("upper").is_equal(name) then
        upper := eval_virtual_machine.get_integer(source);
     else
        check
           ("storage").is_equal(name)
        end;
        storage := eval_virtual_machine.get_pointer(source);
     end;
      end;

invariant

   capacity >= (upper - lower + 1);

   capacity > 0 implies storage.is_not_void;

end -- ARRAY[E]