Changes between Version 69 and Version 70 of IR2

Timestamp:

05/04/21 13:17:37 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -77 +77 @@
 === Notes ===
 
+* A typedef can be used to define parameterized types.  The type parameters are listed between angular brackets preceding the typedef.   When the identifier is later used, it must be used with angular brackets and actual type names to replace the type parameters.
 * A declaration declares a variable to have either an object type or a function type.   (An object type is any type that is not a function type.)
+* The optional type-param-list in a declaration may be applied to declaration of function type only.   It declares a "generic" function.  When the function is called (or spawned), the call must include the angular brackets with a list of type names that replace the type parameters used in the declaration or definition of the function.
 * A variable of function type represents either an abstract or a system function.   The declaration of such a variable must use either the qualifier `$abstract_f` or `$system_f`.  Moreover, those two qualifiers can only be used in a declaration of function type.
 * An abstract function represents a new uninterpreted pure function.
@@ -89 +91 @@
 * The `expr` in a guard must have type `$bool`.
 
-{{{
-  int a[];
-  void main() {
-    a = (int[10])$lambda(int i; $undefined);
-    a = $new(int[10]); // 
-    ... initialized a somehow ...
-   $assume($defined(a, 0, 10)); // ?
-
-}}}
 
 == Contracts ==
@@ -122 +115 @@
 {{{
 type-specifier:
-    ID  /* typedef use or type parameter */
+    ID ('<' type-list '>')?  /* type parameter or (possibly parameterized) typedef use */
   | '$int'  /* mathematical integers */
   | '$bool'  /* boolean type ($true and $false, unrelated to integers) */