True Arrays

C uses an "array-pointer" pun. This is not a particularly useful feature and leads to a lot of confusion. In C, code such as

void f(double[] x) {…}
double a[10];
…
  f(a);
…

is automatically converted to

void f(double *x) {…}
double a[10];
…
  f(&a[0]);
…

Moreover, in C there is no way to pass an array value as an argument to a function, or return an array value, or assign an array value to a variable of array type, all features we would like to include in CIVL-C.

CIVL-C maintains backwards compatibility with C. To enable the new features above, a new type of declaration of variables of array type is introduced, using double brackets instead of single brackets. Both forms declare the same type (array of T), but variables declared with double brackets will not have the automatic conversions to pointers applied to them. The double-bracket objects can also be passed as parameters in function calls (without conversion), assigned, and returned by functions. For example:

int[[]]  double(int a[[]], int n) {
  int b[[n]];

  for (int i=0; i<n; i++)
    b[i] = 2*a[i];
  return b;
}

void main() {
  int x[[5]], y[[]];

  for (int i=0; i<5; i++)
    x[i] = i;
  y = double(x);
}

is a legal CIVL-C program and at termination y hold the array value {0,2,4,6,8}. Note no pointers are ever used in this program.

Another example:

  $message[[]] append_message($message[[]] queue, $message m);

takes an array of messages and returns an array one longer which is equivalent to the original array with $m$ added. There is no "sharing" between these two arrays.

You can still modify double-bracketed arrays and create references to elements of them, just as with regular arrays:

void f(int a[[]], int n) {
  a[0] = 10;
  
}

Sequence Operations

The following operations are available for arrays:

• int $length(T a[[]])
  • returns the number of elements in this array
• T[[]] $concat(T a[[]], T b[[]])
  • returns the concatenation of two arrays
• T[[]] $add(T a[[]], T x)
  • returns the result of adding the element x to the end of array a
• T[[]] $remove(T a[[]], int i)
  • returns the result of removing the element at index i from the array a (with subsequent elements shifted down)
• T[[]] $subseq(T a[[]], int start, int end)
  • returns the subsequence of a starting at index start and ending at index end-1
• T[[]] $write(T a[[]], int i, T x)
  • returns the sequence obtained by replacing the element of a at index i with x

Other related ideas

• Instead of malloc, introduce an operator $alloc(heap, type) where heap is an expression of type pointer-to-heap and type is a type name. The type of this expression is pointer-to-type. It allocates an object of the given type on the specified heap and returns a pointer to that object.