Changes between Version 6 and Version 7 of DataStructures

Timestamp:

07/04/14 12:06:00 (12 years ago)

Author:

siegel

Comment:

--

DataStructures

@@ -8 +8 @@
 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 ==
+== Immutable Version ==
+
+=== Sequences ===
 
 This is an abstract datatype for an immutable (functional) sequence of elements of the same type.
@@ -64 +66 @@
 
 
-== Sets ==
+=== Sets ===
 
 Should we make it an ordered set, `$oset`?
@@ -110 +112 @@
 
 
-== Maps ==
+=== Maps ===
 
 `$map`
@@ -150 +152 @@
 }}}
 
+== Mutable Version ==
+
+
+=== Sequences ===
+
+This is an abstract datatype for a mutable sequence of elements of the same type.
+
+New type: `$mseq`.  Functions:
+
+{{{
+/* Creates a new mutable sequence allocated in the given
+ * scope's heap.  The type of the elements that this sequence
+ * can hold is specified.  The sequence is initially empty.
+ * A handle to the new sequence is returned.
+ */
+$mseq $mseq_create($scope scope, $type type);
+
+/* Forms a new mutable sequence by copying the data from an 
+ * existing sequence of values.  The parameter ptr points to the
+ * element in the existing sequence of adjacent values in memory.
+ * The number of elements is n, and the type of each element is type.
+ * The new sequence is allocated in the heap of the specified scope.
+ * A handle to the new sequence is returned.
+ */
+$mseq $mseq_create_from_array($scope scope, $type type, void * ptr, int n);
+
+/* Creates a new mutable sequence by copying a subsequence
+ * of data from an existing mutable sequence.  The elements
+ * at indexes start, state+1, ..., stop-1 are copied from the original
+ * to create the new sequence, where they will have indexes 0, 1, ...,
+ * stop-start-1.  The length of the new sequence will be stop-start,
+ * unless stop-start is negative, in which case the length will be 0.
+ */
+$mseq $mseq_create_subseq($scope scope, $mseq original, int start int stop);
+
+/* Destroys the mseq specified by the given handle.
+ * All memory associated with the mseq is deallocated.
+ * The handle then becomes an undefined value.
+ * The sequence does not have to be empty when this is called.
+ */
+void $mseq_destroy($mseq mseq);
+
+/* Returns the type of an element that goes in this seq */
+$type $mseq_get_element_type($mseq mseq);
+
+/* Adds the specified element to the mseq.
+ * A runtime exception is generated if the thing pointed
+ * to by eltptr doesn't have the right type for the mseq.
+ */
+void $mseq_add($mseq mseq, void * eltptr);
+
+/* Removes the element at position index from the mseq
+ * and shifts the subsequence elements down.
+ * If result is not NULL, the value removed is written to the memory
+ * pointed to by result.  If the result is NULL, this is not done.
+ */
+void $mseq_remove($mseq mseq, int index, void * result);
+
+/* Replaces the element at position index with whatever
+ * object is pointed to by ptr. 
+ * If old is not NULL, the old entry at index is copied to the
+ * memory specified by old.  If old is NULL, this is not done.
+ */
+void $mseq_set($mseq mseq, int index, void * ptr, void * old);
+
+/* Returns the length of the mseq (i.e., the number of elements) */
+int $mseq_get_length($mseq mseq);
+
+/* Inserts the specified element at the given index.
+ * Subsequent elements are shifted up.n
+ * The parameter eltptr is a pointer to the element to insert. */
+void $mseq_insert($mseq mseq, int index, void * eltptr);
+
+/* Gets the element at position index and stores it in wherever
+ * ptr points to. */
+void $mseq_get($mseq mseq, int index, void * ptr);
+
+/* Adds all the elements of s2 to s1.  The
+ * elements from s2 are copied and appended to the
+ * end of s1.  The sequence s2 itself is not modified.
+ */
+$mseq $mseq_append($mseq s1, $mseq s2);
+}}}
+
+
+=== Sets ===
+
+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);
+}}}
+