Changes between Version 64 and Version 65 of IR2

Timestamp:

05/03/21 10:18:08 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -154 +154 @@
 === Notes ===
 
-* Sequences, sets, maps, and relations are immutable.   An assignment using objects of this type creates a new copy of the object, just as with primitive types like `int`.
-* The main difference between the array type and the sequence type is that elements of an array are addressable, i.e., one can form a pointer such as `&a[i]`.  This is not possible with sequences, sets, maps, or relations---there is no way to have a pointer to any component of such a type.
+* Sequences, sets, maps, relations, and `$mem` objects are immutable.   An assignment using objects of this type creates a new copy of the object, just as with primitive types like `$int`.
+* Arrays are similar to sequences.   The main differences are as follows:
+  * An object (i.e., a variable or component of an object) of array type is initialized once, then will never be assigned to again.   Hence there cannot be a statement of the form `a=...` where `a` has array type.
+  * After initialization, an object or array type can appear only as the first (left) argument to the subscript operator `[]` or as the argument to the `$length` operator.
+  * Arrays are mutable.   As in C, the left hand size of an assignment may have the form `a[i]`, where `a` is an object of array type.  Sequences are immutable.
+  * Elements of an array are addressable, i.e., one can form a pointer such as `&a[i]`.  This is not possible with sequences, sets, maps, or relations---there is no way to have a pointer to any component of such a type.
+  * A function may neither consume nor return an object of array type.  There is no such restriction for sequences.  
 * The difference between the function type and map type: a function is really a procedure in the language, so it can modify the state as well as return a value.    This is like the C notion of "function".   A map is a logical partial function: it is defined on some subset of the domain type, it will always "return" the same value on a given input, and reading it cannot modify the state.
 
@@ -240 +245 @@
 === `civlc.cvh` ===
 
+Work in progress...
+
 * `round(e,t)`: returns value in numerical type `t` that is "closest" to the given value `e`
  * add argument for rounding mode?
@@ -255 +262 @@
  * exceptions may be thrown if evaluating any of the delayed operations results in an exception
 
-
-
 {{{
 
@@ -262 +267 @@
 
 === `mem.cvh` ===
+
+Work in progress...
 
 * `mem_reach(ptr)`, where `ptr` is an expression with a pointer type.
@@ -278 +285 @@
 <T> $int $seq_length( $seq<T> a ); // length of a
 <T> T $seq_get( $seq<T> a, $int i ); // get element i of a
-<T> $seq<T> $seq_set( $seq<T> a, $int i, T x ); // seq obtained by replacing element i of a with x
-<T> $seq<T> $seq_subseq( $seq<T> a, $int start, $int stop ); // subsequence from start to stop-1
-<T> $seq<T> $seq_add( $seq<T> a, T e ); // sequence obtained by adding element e to the end of a
-<T> $seq<T> $seq_append( $seq<T> a1, $seq<T> a2 ); //  sequence obtained by concatenating a1 and a2
-<T> $seq<T> $seq_remove( $seq<T> a, $int i ); // sequence obtained by removing element at position i from a
-<T> $seq<T> $seq_insert( $seq<T> a, $int i, T x ); // sequence obtained by inserting element x at position i in a
+<T> $seq<T> $seq_set( $seq<T> a, $int i, T x ); // seq obtained by replacing element `i` of `a` with `x`
+<T> $seq<T> $seq_subseq( $seq<T> a, $int start, $int stop ); // subsequence from `start` to `stop-1`
+<T> $seq<T> $seq_add( $seq<T> a, T x ); // sequence obtained by adding element `x` to the end of `a`
+<T> $seq<T> $seq_append( $seq<T> a1, $seq<T> a2 ); //  sequence obtained by concatenating `a1` and `a2`
+<T> $seq<T> $seq_remove( $seq<T> a, $int i ); // sequence obtained by removing element at position `i` from `a`
+<T> $seq<T> $seq_insert( $seq<T> a, $int i, T x ); // sequence obtained by inserting element `x` at position `i` in `a`
+<T> void $seq_write( $int n, T * ptr, $seq<T> a );  // write the first `n` elements of `a` to `ptr`, `ptr+1`, ..., `ptr+n-1`.
+<T> $seq<T> $seq_read( $int n, T * ptr ); // form a sequence by reading `ptr`, `ptr+1`, ..., `ptr+n-1`.
 
 }}}