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 sequence formed by reading n consecutive elements
 * from memory.  The parameter ptr points to the first such element,
 * and type is the type of each element.
 */
$seq $seq_from_array($type type, void * ptr, int n);

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

/* 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 the seq. */
$seq $seq_add($seq seq, 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 seq, 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 seq, int index, void * ptr);

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

/* 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 seq, int index, void * eltptr);

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

/* Returns the subsequence consisting of elements at index i, for
 * start<=i<stop. */
$seq $seq_subseq($seq seq, int start, int stop);

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

Sets

Should we make it an ordered set, $oset?

New type: $set. Functions:

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

/* Returns the cardinality of the set */
int $set_get_size($set set);

/* Returns the type of an element that goes in this set */
$type $set_get_element_type($set set);

/* Returns the set 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 s. */
$set $set_add($set set, void * eltptr);

/* Returns the set that is like the given one but with the specified element
 * removed.  If the set does not contain the element the set returned
 * will equal the given one. */
$set $set_remove($set set, void * eltptr);

/* Does the set contain the specified element? */
_Bool $set_contains($set set, void * eltptr);

$set $set_union($set s1, $set s2);

$set $set_intersection($set s1, $set s2);

$set $set_difference($set s1, $set s2);

/* Returns the singleton set consisting of the single element
 * specified by the pointer and the type */
$set $set_single($type type, void * eltptr);

/* Returns a sequence consisting of the elements of the set */
$seq $set_to_seq($set set);

Maps

$map

/* Returns the empty map with the given key type and
 * value type.
 */
$map $map_empty($type keyType, $type valType);

/* Returns the map obtained by starting with the given
 * map, removing the entry with the specified key (if
 * one exists) and then adding the specified key-value
 * pair.  If that key-value pair already exists in the given map,
 * the map returned is identical to the given on.
 */
$map $map_put($map map, void * keyPtr, void * valPtr);

/* If an entry with the specified key exists in the map, it
 * the corresponding value is copied into the region specified
 * by the resultPtr.  Otherwise, a no-op.
 */
void $map_get($map map, void * keyPtr, void * resultPtr);

/* Returns the map obtained by removing an entry
 * with the specified key, if one exists.
 */
$map $map_removeKey($map map, void * keyPtr);

/* Returns the set of keys in the given map. */
$set $map_get_keySet($map map);

/* Returns the set of ordered pairs of the form (key,val).
 * Each ordered pair has a struct type consisting of two fields
 * named key and val.  The type of the key field is the keyType;
 * the type of the val field is the valType.
 */
$set $map_get_entrySet($map map);