Changes between Version 24 and Version 25 of IR

Timestamp:

11/22/15 20:32:54 (10 years ago)

Author:

siegel

Comment:

--

IR

@@ -54 +54 @@
 ==  Types ==
 
-**Do you need dependent types?**  I.e., can parameters to some of the types be arbitrary expressions, or do they have to be constants?
-
-**Do you need typedefs?**
-
-Question about types.  In the following, where in the state is the length of the array field stored?
-
-{{{
-#include <stdio.h>
-int n=10;
-int main() {
-  struct S {int a[n];};
-  struct S x1;
-  n=20;
-  struct S x2;
-  printf("%ld, %ld\n", sizeof(x1), sizeof(x2));
-  x2.a[10]=1; // error caught by CIVL
-  fflush(stdout);
-}
-}}}
-
-
+The types are:
+
+* `$dytype` : dynamic type: a value of this type represents a "dynamic type", a type which is created at runtime.  For example when the type name `int[n]` is evaluated, the result is a value of type `$dytype`.
 * `$bool` : boolean type, values are `$true` and `$false`
 * `$proc` : process type
@@ -102 +84 @@
 * `union(T1,...,Tn)` : similar to struct
 * `T[]` : array-of-T
-* **do we need the complete array type `T[e]`, which is a dependent type?**
 * Function<S1,...,Sn;T>
  * function consuming S1,...,Sn and returning T.  T can be void.  The actual notation is the horrible C notation.
@@ -108 +89 @@
  * `T*` : pointer-to-T, subtype of above
 
-When are two types equal?
-
-What are two types compatible?
-
-== Type names ==
-
-**Do we need another syntactic category for code that specifies a dynamic type**, for example
-* `int[n*m+3]`.
-
-This can be used in `sizeof`, ...
-
-**Do we need to clearly distinguish dynamic type names and static type names?**
+Type names:
+
+A type name is a syntactic element that names a type, together with possibly more information that makes the type "complete".  All of the names listed above are type names, such as `int[]`, but so is `int[n*m]`.
+
+The expression `$dytypeof(typeName)` takes a type name and returns a value of type `$dytype` representing that type.
+
+The expression `$init_val(d)` takes a `$dytype` value `d` and returns the initial value for an object of type `d`.
+
+Example:
+{{{
+// type definitions
+struct S { int a[];}
+
+// variable decls
+int n;
+$dytype _S;
+struct S x1;
+struct S x2;
+
+// statements (leaving out the chooses and whens for brevity)
+n=10;
+_S=$dytypeof(struct S { int a[n]; };
+x1=$init_val(_S);
+n=20;
+x2=$init_val(_S);
+}}}
+
+is semantically equivalent to the C code
+
+{{{
+int n = 10;
+struct S { int a[n]; };
+struct S x1;
+n=20;
+struct S x2;
+}}}
 
 
@@ -150 +155 @@
 
 == Expressions ==
+
+In the following list of expressions, `e`, `e0`, `e1`, etc., are expressions.  `T` is a type name.
 
 * literals
@@ -165 +172 @@
  * `NULL` : value of type `void*`
 * variables
-* `$defined(e1)`
+* `$dytypeof(T)` : an expression of type `$dytype`
+* `$init_val(e)`, where `e1` is an expression of type `$dytype`
+* `$defined(e)`
 * `e1+e2` : addition
 * `e1-e2` : subtraction
@@ -185 +194 @@
 * `$forall`, `$exists`
 * `e1.i`, some natural number i (tuple read)
-* `$initial_value(T; e1,...,en)`
- * e1,...,en are expressions of integer type
- * the type of this expression is T[e1]...[en]
- * array value with base type `T` and lengths e1,...,en
- * **do we need this for more types?**  E.g., structs of arrays of structs of arrays of ...?
-* `$typeof(...)`: what is this for?
 * `sizeof(T)` : T is a type name?
 * `e1&e2`, `e1|e2`, `e1^e2`, `~e1` : bit-wise operations: arguments are arrays of booleans