Idea

New data structures are needed in CIVL-C in order to model what happens in OpenMP and other complex APIs. Sequences, sets, and maps, specifically. The purpose of this page is to propose the new interface for these structures.

Typeof

First we need a new expression $typeof. This expression has the syntax $typeof(typename). It is just like sizeof syntactically. It represents any type as a value. The type of the $typeof expression is the type $type. This is also represented in the CIVL model layer as "dynamic type".

Sequences

This is an abstract datatype for an immutable (functional) sequence of elements of the same type.

New type: $seq. Functions:

/* Returns the empty seq whose elements (if it had any)
 * would have the given type.  The type becomes associated
 * with the seq.  */
$seq $seq_empty($type type);

/* Returns the type of an element that goes in this seq */
$type $seq_element_type($seq v);

/* Returns the seq that is like the given one but with one more
 * element added.  A runtime exception is generated if the thing pointed
 * to by eltptr doesn't have the right type for v. */
$seq $seq_add($seq v, void * eltptr);

/* Returns the seq that is like the given one but with the element
 * at position index removed and the subsequent elements shifted down */
$seq $seq_remove($seq v, int index);

/* Returns the seq that is like the given one but with the element
 * at position index replaced with whatever object is pointed to by
 * ptr. */
$seq $seq_set($seq v, int index, void * ptr);

/* Returns the length of the seq (i.e., the number of elements) */
int $seq_length($seq v);

/* Returns the seq that is like the given one but with an element
 * inserted at position i (and the subsequent elements shifted up).
 * The parameter eltptr is a pointer to the element to insert. */
$seq $seq_insert($seq v, int index, void * eltptr);

/* Gets the element at position index and stores it in wherever
 * ptr points to. */
void $seq_get($seq v, int index, void * ptr);

/* Returns the subsequence */
$seq $seq_sub($seq v, int start, int stop);

/* Returns the concatenation of the two sequences */
$seq $seq_concat($seq s1, $seq s2);

Sets

Maps