Changes between Version 93 and Version 94 of IR

Timestamp:

11/30/15 08:37:51 (10 years ago)

Author:

siegel

Comment:

--

IR

@@ -105 +105 @@
 * `Enum` types.
  * **different from integers or like C?**
-* `Integer` : the mathematical integers
-* `Int[lo,hi,wrap]`
- * `lo`, `hi` are concrete (?) integers, `wrap` is boolean
- * finite interval of integers `[lo,hi]`.  If `wrap` is true then all operations "wrap", otherwise, any operation resulting in a value outside of the interval results in an exception being thrown.
- * **Do we want to allow `lo` and `hi` to be any values of type `Integer`, which means they are dynamic types, like complete array types?**
-* `HerbrandInt` : Herbrand integers.  Values are unsimplified symbolic expressions.
-* `Real` : the mathematical real numbers
-* `Float[e,f]`, `e`, `f` are concrete integers, each at least 1.  
- * IEEE754 floating point numbers.  This type includes NaNs, negative 0s, infinities, etc.
-* `HerbrandReal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
+* The **numeric types**
+ * The **integral types**
+  * `Integer` : the mathematical integers
+  * `Int[lo,hi,wrap]`
+   * `lo`, `hi` are concrete (?) integers, `wrap` is boolean
+   * finite interval of integers `[lo,hi]`.  If `wrap` is true then all operations "wrap", otherwise, any operation resulting in a value outside of the interval results in an exception being thrown.
+   * **Do we want to allow `lo` and `hi` to be any values of type `Integer`, which means they are dynamic types, like complete array types?**
+ * The **real types**
+  * `Real` : the mathematical real numbers
+  * `Float[e,f]`, `e`, `f` are concrete integers, each at least 1.  
+   * IEEE754 floating point numbers.  This type includes NaNs, negative 0s, infinities, etc.
+ * Herbrand[T], for a non-Herbrand numeric type `T`
+  * the values of this type are (unsimplified) symbolic expressions.  Each numeric operator is treated as an uninterpreted function.  The leaf nodes in an expression are values of type `T`.  Two values are equal iff the two symbolic expressions are identical (using equality in `T` on the leaf nodes).  A value of Herbrand type may therefore be thought of as representing an expression in `T` but where all the numerical operations have been "delayed". 
 * `Tuple[<T0, T1, ...>]`: a tuple type, the Cartesian product of `T0`, `T1`, ...
  * **What about bit-widths?**
@@ -200 +203 @@
 * `abs(e)`: given any numeric expression e, returns the absolute value; result is same type as `e`.
 * `pow(e,n)`: given any numeric expression e and expression `n` of any integral type, returns e to the n-th power.  `n` must evaluate to a nonnegative integer.
-* `herbrand(e)`: given a Real or Float value, returns the value as a `HerbrandReal`.  Given an `Integer` or `Int` value, returns the value as a `HerbrandInt`.
-* `real(e)`: given any numerical value e, returns it as a real number
-* functions for converting floats to reals and back.
-* functions for converting between Ints and Integers -- or is there a subtype relation?  If so, it must respect all operations.
+* `herbrand(e)`: given a numeric value of type `T`, returns the value as type `Herbrand[T]`, a trivial symbolic expression consisting of a single node.
+* `eval(e)` : given a value of type `Herbrand[T]`, returns the value of type `T` obtained by evaluating all the delayed operations
 
 Characters and Strings
@@ -213 +214 @@
 * `hasnext(dom, <i,j,…>)`: an expression of boolean type, testing if the domain `dom` contains any element after `<i,j,...>`
 
-Arrays
+Arrays (which are also Sequences)
 * `array(T,<e0,...,en-1>)`: value of type `Array[T, n]`, a literal array
 * `array(T,n,e)`: value of type `Array[T,n]` in which each of the n elements is `e`
@@ -261 +262 @@
 * `defined(e)` : is `e` defined? `Bool` type
 * `cast(e,T)` : casts `e` to a value of the named type.
- * A cast can only take place when there is no change to the underlying value.  It is only for changing the type.  Example: one can cast from any integral type to another, but there might be an exception if the value is not in the range of the targeted type.  One can cast any `Float` value to a `Real` value, but not the other way.  (To convert from a `Real` to a `Float`, use, e.g., `round`.)  If t1 is a subtype of t2, one can always cast from t1 to t2 (though this is rarely necessary, since an expression of type t1 can be used wherever one of type t2 is expected).
+ * A cast can only take place when there is no change to the underlying value in the concrete semantics.  It is only for changing the type.
+ * One can cast from any integral type to another (as the values in all cases are integers), but there might be an exception if the value is not in the range of the targeted type.
+ * One can cast any `Float` value to a `Real` value, but not the other way.  (To convert from a `Real` to a `Float`, use, e.g., `round`.)  One cannot cast from one `Float` type to another `Float` type (unless the float parameters are exactly the same).  To do this, one could instead use `round`.
+ * If t1 is a subtype of t2, one can always cast from t1 to t2 (though this is rarely necessary, since an expression of type t1 can be used wherever one of type t2 is expected).  One can also cast from t2 to t1, but a runtime exception will be thrown if the value being cast does not already belong to t1.  For example, one might cast from `Domain` to `Domain[n]`, or from `Array[Real]` to `Array[Real, n]`.
+ * One cannot cast between a Herbrand type and any other type.  Instead, use functions `eval` and `herbrand`.
 * `ite(e1,e2,e3)`: if-then-else (conditional) expression, like `e1?e2:e3` in C. 
 * `call(e0,<e1,...,en>)` : a function invocation where `e0` must evaluate to either an abstract or pure system function