% 
% @(#)real_Array.m	1.3  7/13/87
%
export Array to "Builtins"

const Array == 
  immutable object Array
    export of
    function of [ElementType : AbstractType] -> [result : NAT]
      where
	NAT ==	immutable type NAT
		  operation empty -> [NA]
		  operation literal [RIS] -> [NA]
		  operation create[Integer] -> [NA]
		  function getSignature -> [Signature]
		end NAT
	RIS ==  type i_RIS
		  function getElement [Integer] -> [ElementType]
		  function upperbound -> [Integer]
		  function lowerbound -> [Integer]
		end i_RIS
	NA ==	type NA
		  function  getElement [Integer] -> [ElementType]
		    % get the element indexed by index, failing if index 
		    % out of range.
		  operation setElement [Integer, ElementType]
		    % set the element, failing if index out of range
		  function  upperbound -> [Integer]
		    % return the highest valid index, ub.
		  function  lowerbound -> [Integer]
		    % return the lowest valid index, lb.
		  function  getSlice [Integer, Integer] -> [NA]
		    % return a new array, a, with lower bound lb, and 
		    % upper bound ub, such that for lb <= i <= ub:
		    %     self.getElement[i] == a.getElement[i]
		    % fail if lb or ub is out of range.
		  operation setSlice [Integer, Integer, RIS]
		    % set the elements indexed by i for lb <= i <= ub, so 
		    % that for each such i:
		    %     self.getElement[i] == a.getElement[i]
		    % fail if lb or ub is out of range.
		  operation slideTo [Integer]
		    % change the valid indicies for self.  Assuming 
		    % the old indicies ranged from lb to ub, the new 
		    % indicies will range from i to i + ub - lb
		  operation addUpper [ElementType]
		    % extend the set of valid indicies, changing ub to 
		    % ub + 1, and setting the element indexed by the new
		    % ub to be e.
		  operation removeUpper -> [ElementType]
		    % return the element indexed by ub, after contracting 
		    % the set of valid indicies to lb <= i <= ub - 1.
		  operation addLower [ElementType]
		    % extend the set of valid indicies, changing lb to 
		    % lb - 1, and setting
		    % the element indexed by the new lb to be e.
		  operation removeLower -> [ElementType]
		    % return the element indexed by lb, after contracting 
		    % the set of valid indicies to lb + 1 <= i <= ub.
		  function  empty -> [Boolean]
		    % -> true if lb == ub + 1, which is true initially,
		    % since initially lb = 1, and ub = 0.
		  operation catenate [a : RIS] -> [r : NA]
		    % extend the range of valid indicies from lb .. ub to 
		    % lb .. ub + a.length.  Set these new elements to refer
		    % to the elements of a so that for a.lb <= i <= a.ub, 
		    % where oub is the old value of self.ub:
		    %     a.getElement[i] == self.getElement[oub + i - 1]
		end NA
	ElementType *> type T end T
      end where

      result <- 
	immutable object aNAT
	  export empty, create, getSignature, literal

	  const ve == Vector.of[ElementType]

	  function getSignature -> [result : Signature]
	    result <- NA
	  end getSignature

	  operation create[length : Integer] -> [result : NA]
	    result <-
	      object aNA
		export getElement, setElement, upperbound, lowerbound, getSlice, setSlice,
		       slideTo, addUpper, removeUpper, addLower,
		       removeLower, empty, catenate

		monitor
		  var lwb, upb, firstIndex, lastIndex : Integer
		  var currentSize, maxSize : Integer
		  attached var vec: ve
		  
		  function  getElement [i : Integer] -> [r : ElementType]
		    var index : Integer
		    assert i >= lwb
		    assert i <= upb
		    index <- (i - lwb) + firstIndex
		    if index >= maxSize then
		      index <- index - maxSize
		    end if
		    r <- vec(index)
		  end getElement

		  operation setElement [i : Integer, r : ElementType]
		    var index : Integer
		    assert i >= lwb
		    assert i <= upb
		    index <- (i - lwb) + firstIndex
		    if index >= maxSize then
		      index <- index - maxSize
		    end if
		    vec(index) := r
		  end setElement

		  function  upperbound -> [r : Integer]
		    r <- upb
		  end upperbound

		  function  lowerbound -> [r : Integer]
		    r <- lwb
		  end lowerbound

		  % return a new Array, a, with lower bound lwb, and 
		  % upper bound upb, such that for lwb <= i <= upb:
		  %     self.getElement[i] == a.getElement[i]
		  % fail if lwb or upb is out of range.
		  function  getSlice [i1 : Integer, l : Integer] -> [r : NA]
		    var index : Integer
		    var i : Integer <- 0
		    assert l >= 0
		    assert i1 >= lwb
		    assert i1+l-1 <= upb
		    r <- aNAT.create[l]
		    r.slideTo[i1]
		    index <- (i1 - lwb) + firstIndex
		    if index >= maxSize then
		      index <- index - maxSize
		    end if
		    loop
		      exit when i >= l
		      r(i1 + i) := vec(index)
		      i <- i + 1
		      index <- index + 1
		      if index >= maxSize then
			index <- index - maxSize
		      end if
		    end loop
		  end getSlice

		  % set the elements indexed by i for lwb <= i <= upb, so 
		  % that for each such i:
		  %     self.getElement[i] == a.getElement[i]
		  % fail if lwb or upb is out of range.
		  operation setSlice [i1 : Integer, l : Integer, s : RIS]
		    var index : Integer
		    var i : Integer <- 0
		    assert l >= 0
		    assert i1 >= lwb
		    assert i1 + l <= upb
		    assert i1 >= s.lowerbound
		    assert i1 + l <= s.upperbound
		    index <- (i1 - lwb) + firstIndex
		    if index >= maxSize then
		      index <- index - maxSize
		    end if
		    loop
		      exit when i >= l
		      vec(index) := s(i1 + i)
		      i <- i + 1
		      index <- index + 1
		      if index >= maxSize then
			index <- index - maxSize
		      end if
		    end loop
		  end setSlice

		  % change the valid indicies for self.  Assuming 
		  % the old indicies ranged from lwb to upb, the new 
		  % indicies will range from i to i + upb - lwb
		  operation slideTo [i : Integer]
		    var difference : Integer <- lwb - i
		    lwb <- lwb - difference
		    upb <- upb - difference
		  end slideTo

		  % extend the set of valid indicies, changing upb to 
		  % upb + 1, and setting the element indexed by the new
		  % upb to be e.
		  operation addUpper [e : ElementType]
		    var index : Integer
		    if currentSize = maxSize then
		      var nvec : ve
		      const nMaxSize : Integer == maxSize * 2
		      var oldIndex : Integer <- firstIndex
		      var newIndex : Integer <- 0
		      nvec <- ve.create[nMaxSize]
		      loop
			exit when newIndex >= maxSize
			nvec(newIndex) := vec(oldIndex)
			newIndex <- newIndex + 1
			oldIndex <- oldIndex + 1
			if oldIndex >= maxSize then
			  oldIndex <- oldIndex - maxSize
			end if
		      end loop
		      firstIndex <- 0
		      lastIndex <- maxSize - 1
		      maxSize <- nMaxSize
		      vec <- nvec
		    end if
		    index <- lastIndex + 1
		    if index >= maxSize then
		      index <- index - maxSize
		    end if
		    vec(index) := e
		    lastIndex <- index
		    currentSize <- currentSize + 1
		    upb <- upb + 1
		  end addUpper

		  % return the element indexed by upb, after contracting 
		  % the set of valid indicies to lwb <= i <= upb - 1.
		  operation removeUpper -> [r : ElementType]
		    assert currentSize > 0
		    r <- vec(lastIndex)
		    currentSize <- currentSize - 1
		    upb <- upb - 1
		    if currentSize = 0 then
		      firstIndex <- 0
		      lastIndex <- ~1
		    else
		      lastIndex <- lastIndex - 1
		      if lastIndex < 0 then
			lastIndex <- lastIndex + maxSize
		      end if
		    end if
		  end removeUpper

		  % extend the set of valid indicies, changing lwb to 
		  % lwb - 1, and setting
		  % the element indexed by the new lwb to be e.
		  operation addLower [e : ElementType]
		    var index : Integer
		    if currentSize = maxSize then
		      var nvec : ve
		      const nMaxSize : Integer == maxSize * 2
		      var oldIndex : Integer <- firstIndex
		      var newIndex : Integer <- 0
		      nvec <- ve.create[nMaxSize]
		      loop
			exit when newIndex >= maxSize
			nvec(newIndex) := vec(oldIndex)
			newIndex <- newIndex + 1
			oldIndex <- oldIndex + 1
			if oldIndex >= maxSize then
			  oldIndex <- oldIndex - maxSize
			end if
		      end loop
		      firstIndex <- 0
		      lastIndex <- maxSize - 1
		      maxSize <- nMaxSize
		      vec <- nvec
		    end if
		    index <- firstIndex - 1
		    if index < 0 then
		      index <- index + maxSize
		    end if
		    vec(index) := e
		    firstIndex <- index
		    currentSize <- currentSize + 1
		    lwb <- lwb - 1
		  end addLower

		  % return the element indexed by lwb, after contracting 
		  % the set of valid indicies to lwb + 1 <= i <= upb.
		  operation removeLower -> [r : ElementType]
		    assert currentSize > 0
		    r <- vec(firstIndex)
		    currentSize <- currentSize - 1
		    lwb <- lwb + 1
		    if currentSize = 0 then
		      firstIndex <- 0
		      lastIndex <- ~1
		    else 
		      firstIndex <- firstIndex + 1
		      if firstIndex >= maxSize then
			firstIndex <- firstIndex - maxSize
		      end if
		    end if
		  end removeLower

		  % -> true if the array is empty
		  function  empty -> [r : Boolean]
		    r <- currentSize = 0
		  end empty

		  % return a new array the result of catenating the 
		  % elements of a to self
		  operation catenate [a : RIS] -> [catenateResult : NA]
		    var index, limit, newsize : Integer
		    var i : Integer <- 0
		    newsize <- currentSize+a.upperbound-a.lowerbound+1
		    catenateResult <- aNAT.create[newsize]
		    catenateResult.slideTo[lwb]
		    index <- firstIndex
		    loop
		      exit when i >= currentSize
		      catenateResult.addUpper[vec(index)]
		      i <- i + 1
		      index <- index + 1
		      if index >= maxSize then
			index <- index - maxSize
		      end if
		    end loop
		    i <- a.lowerbound
		    limit <- a.upperbound
		    loop
		      exit when i > limit
		      catenateResult.addUpper[a(i)]
		      i <- i + 1
		    end loop
		  end catenate

		  initially
		    lwb <- 0
		    firstIndex <- 0
		    if length < 0 then
		      upb <- ~1
		      lastIndex <- ~1
		      maxSize <- ~length
		      currentSize <- 0
		    elseif length = 0 then
		      upb <- ~1
		      lastIndex <- ~1
		      maxSize <- 10
		      currentSize <- 0
		    else
		      upb <- length - 1
		      lastIndex <- length - 1
		      maxSize <- length
		      currentSize <- length
		    end if
		    vec <- ve.create[maxSize]
		  end initially
		end monitor
	      end aNA
	  end create
	  operation empty -> [result : NA]
	    result <- aNAT.create[0]
	  end empty
	  operation literal [v : RIS] -> [literalResult : NA]
	    var i : Integer <- v.lowerbound
	    const limit : Integer == v.upperbound
	    literalResult <- aNAT.create[~(limit - i + 1)]
	    loop
	      exit when i > limit
	      literalResult.addUpper[v(i)]
	      i <- i + 1
	    end loop
	  end literal
	end aNAT
    end of
  end Array
