Changes between Version 118 and Version 119 of IR2

Timestamp:

06/04/21 09:21:17 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -253 +253 @@
   | expr type-args? '(' expression-list? ')'  /* application of abstract function (and perhaps other functions?) */
   | '$typeof' '(' type-name ')'  /* value type named by the extended type name */
-  | '$fresh' '(' expr ')'  /* returns a new arbitrary value of the given type */
-  | '$new' '(' expr ')'  /* returns a new arbitrary and undefined value of the given complete type */
+  | '$fresh' '(' (expr | type-name) ')'  /* returns a new arbitrary value of the given type */
+  | '$new' '(' (expr | type-name) ')'  /* returns a new arbitrary and undefined value of the given complete type */
   | '$forall' '(' decl expr? ')' expr  /* universal quantification */
   | '$exists' '(' decl expr? ')' expr  /* existential quantification */
@@ -293 +293 @@
   * A pointer becomes defined when assigned the result of an `$alloc`.   Each element in the newly allocated object is undefined.
   * Example: to determine whether it is safe to read `*(p+i)`, assert `$summable(p, i) && $valid(p+i) && $defined(*(p+i))`.  You must check (1) you can sum `p` and `i`, (2) `p+i` points to an object of the base type, so dereference is safe, and (3) the object is defined (has been assigned a value).  If you aren't sure `p` and `i` have been defined, you can add `$defined(p) && $defined(i)` to the assertion.   It may be more efficient to use temporary variables and break this up into multiple assertions.
-  * `$fresh` and `$new` consume an argument of type `$type<T>` and return a value of type `T`.  For `$new`, the argument must specify a complete type.  Fresh accepts any type name.
+  * `$fresh` and `$new` consume an argument expression of type `$type<T>` and return a value of type `T`.  For `$new`, the argument must specify a complete type.  `$fresh` accepts any extended type.   `$new(T)`, where `T` is a type-name, is syntactic sugar for `$new($typeof(T))`; ditto for `$fresh(T)`.
 
 Example: C code
@@ -299 +299 @@
 typedef T mat[n][m];
 mat a;
-
 }}}
 might be translated
@@ -306 +305 @@
 $type<mat> _type_mat = $typeof(T[n][m]);
 mat a = $new(_type_mat);
-
 }}}