Changes between Version 66 and Version 67 of IR

Timestamp:

11/25/15 21:55:04 (10 years ago)

Author:

siegel

Comment:

--

IR

@@ -17 +17 @@
 * angular brackets are used to delimit tuples or sequences
 * square brackets are used to delimit parameters in types
+* unlike C, there is no "array-pointer pun".   If an array `a` needs to be converted to a pointer, you must use \addr(\asub(a, 0))`.
+* there are no automatic conversions.  All conversions must be by explicit casts or other functions.   Operations such as numeric addition (`\add`) require that both operands have the exact same type.
+
 
 Example:
@@ -89 +92 @@
  * IEEE754 floating point numbers
 * `HerbrandReal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
-* `Tuple[<T0, T1, ...>]`: a tuple type, the Cartesian product of T0, T1, ...
+* `Tuple[<T0, T1, ...>]`: a tuple type, the Cartesian product of `T0`, `T1`, ...
  * **What about bit-widths?**
-* `Union[<T0, T1, ...>]`: union type, the disjoint union of T0, T1, ...
+* `Union[<T0, T1, ...>]`: union type, the disjoint union of `T0`, `T1`, ...
 * `Array[T]` : arrays of any length whose elements belong to T
 * `Function[<T0,T1,...>,T]` : functions consuming T0,T1,... and returning T.  T can be `void` to indicate nothing is returned.
@@ -170 +173 @@
 * `"abc"` : string literals: value of type `Array[Char, n+1]`, where n is the length of the string (the last element is the character `\0`)
 Ranges and Domains
-* `\range(e1,e2,e3)` : value of type `Range` consisting of the integers e1, e1+e3, e1+2*e3, ... that are less than or equal to e2.
-* `\domain(<r1,...,rn>)` : value of type `Domain[n]`, the ordered Cartesian product of the n ranges (dictionary order)
+* `\range(e1,e2,e3)` : value of type `Range`.  If `e3` is positive, the integers e1, e1+e3, e1+2*e3, ... that are less than or equal to `e2`.  If `e3` is negative, the integers e1, e1+e3, e1+2*e3, ... that are greater than or equal to `e2`.  Exception if `e3` is 0.
+* `\domain(<r1,...,rn>)` : value of type `Domain[n]`, the Cartesian product of the n ranges, with dictionary order
 * `\hasnext(dom, <i,j,…>)`: an expression of boolean type, testing if the domain `dom` contains any element after `<i,j,...>`
 Arrays
@@ -179 +182 @@
 * `\seq_add(a,e)` : array obtained by adding element e to the end of the array.  Original array a is not modified.
 * `\seq_append(a1,a2)` : array obtained by concatenating two arrays.  Original array not modified.
-* `\seq_remove(a,i)` : array obtained by removing element at position i from a.  Original array a not modified.  **WHAT HAPPENS TO REFERENCES INTO A**
+* `\seq_remove(a,i)` : array obtained by removing element at position i from a.  Original array a not modified.
 * `\bit_and(e1, e2)`, `\bit_or(e1, e2)`, `\bit_xor(e1, e2)`, `\bit_comp(e1)` : bit-wise operations: arguments are arrays of booleans of equal length.
 Tuples
 * `\tuple(S,<e0,e1,...>)` : value of tuple type `S` (tuple literal)
 * `\tsel(e1,i)` : tuple selection of component i of e1.  i must be a literal natural number.
+Unions
+* `\union_inj(U,i,x)` : `x` is in `Ti`, result is in the union type `U`
+* `\union_sel(U,i,y)` : `y` is in `U`, result is in `Ti` (or exception if `y` is not in image of injection from `Ti`)
+* `\union_test(U,i,y)` : `y` is in `U`; determines if `y` is in the image under injection of `Ti`.  Returns a Boolean.
 Pointers and Memory
 * `NULL` : value of type `void*`
@@ -211 +218 @@
 * `e0(e1,...,en)` : a function invocation where `e` must evaluate to either an abstract or pure system function
 
-Notes
-* unlike C, there is no "array-pointer pun".   If an array `a` needs to be converted to a pointer, you must use \addr(\asub(a, 0))`.
-
 == The Primitive Statements ==