Changes between Version 127 and Version 128 of IR2

Timestamp:

06/10/21 13:41:55 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -123 +123 @@
 type-specifier:
     ID type-args?  /* type parameter or (possibly parameterized) typedef use */
-  | '$int' size-spec  /* mathematical integers */
-  | '$bool' size-spec  /* boolean type ($true and $false, unrelated to integers) */
-  | '$char' size-spec  /* character type (Unicode characters, unrelated to integers) */
-  | '$real' size-spec   /* mathematical reals */
-  | '$float' size-spec  /* IEEE floating-point numbers */
+  | '$int' size-spec?  /* mathematical integers */
+  | '$bool' size-spec?  /* boolean type ($true and $false, unrelated to integers) */
+  | '$char' size-spec?  /* character type (Unicode characters, unrelated to integers) */
+  | '$real' size-spec?   /* mathematical reals */
+  | '$float' size-spec?  /* IEEE floating-point numbers */
   | '$herbrand' '<' type-name '>'  /* Herbrand type of non-Herbrand numeric type T */
   | '$proc'  /* process type */
@@ -164 +164 @@
 === Notes ===
 
-* Certain basic types can have a specified size---the number of bytes consumed by an object of that type.  These basic types include '$bool', '$int', '$char', and '$real'.   Two versions of the basic type with different sizes are in fact disjoint types.  The basic type without a specified size has domain the union over all sizes of the size-qualified type.  TODO: require this or option?
+* Certain basic types can have a specified size---the number of bytes consumed by an object of that type.  These basic types include '$bool', '$int', '$char', and '$real'.   Two versions of the basic type with different sizes are in fact disjoint types.  There is also a basic type without a specified size, and this type is distinct from all the sized types.   Certain operations require a sized type (specify these!).  
 * 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.
+  * 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. (Except for the first one?)
   * After initialization, an object of 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.
@@ -343 +343 @@
 === `civlc.cvh` ===
 
-Work in progress.   Refer to existing library.
-
-{{{
-<T1,T2> struct $pair { T1 left; T2 right; };
-<T1,T2> typedef struct $pair<T1,T2> $pair;
-<T> $system T * $alloc($heap * h, T obj);  // add an object to a heap
-$system $free($void * p);  // remove an object from the heap
-$system void $exit();  // terminate process immediately
-$system $bool $terminated($proc p);  // has the process terminated?
-$template <$int s> $system $int<s> $choose_int($int<s> n);  // nondeterministic choice of int in 0..n-1
+Work in progress.   Refer to existing library.   All include`$system<"civl.library", "civlc">`.
+
+{{{
+$template <$typenameT1, $typename T2> struct $pair { T1 left; T2 right; };
+$template <$typenameT1, $typename T2> typedef struct $pair<T1,T2> $pair;
+$template <$typename T> $pure_f $int $sizeof($type<T> type);
+$template <$typename T> T * $alloc($heap * h, T obj);  // add an object to a heap
+$int $choose_int($int n);  // nondeterministic choice of int in 0..n-1
+$free($void * p);  // remove an object from the heap
+void $exit();  // terminate process immediately
+$bool $terminated($proc p);  // has the process terminated?
 
 }}}