| | 256 | Types |
| | 257 | * `new(t)` : new (default) value of `Dytype` t. If `t` has type `Dytype[T]`, then this expression has static type `T`. |
| | 258 | * `typeof(e)` : returns the value of type `Dytype` representing the value type of `e`. If `e` has static type `T` then this expression has static type `Dytype[T]`. |
| | 259 | * `subtype(t1,t2)`: is `t1` a subtype of `t2`? Both args have type `Dytype`. Returns a `Bool` |
| | 260 | * `sizeof_type(t)` : the size of the dynamic type `t`; return an `Integer` |
| | 261 | * `cast(e,t)` : casts `e` to a value of dytype `t`. If `t` has type `Dytype[T]`, this expression has static type `T` and the value will have dynamic type `t`. |
| | 262 | * 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. |
| | 263 | * 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. |
| | 264 | * 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`.) |
| | 265 | * 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`. |
| | 266 | * 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]`. |
| | 267 | * One cannot cast between a Herbrand type and any other type. Instead, use functions `eval` and `herbrand`. |
| | 268 | |
| 263 | | * `cast(e,T)` : casts `e` to a value of the named type. |
| 264 | | * 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. |
| 265 | | * 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. |
| 266 | | * 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`. |
| 267 | | * 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]`. |
| 268 | | * One cannot cast between a Herbrand type and any other type. Instead, use functions `eval` and `herbrand`. |
| 269 | | * `ite(e1,e2,e3)`: if-then-else (conditional) expression, like `e1?e2:e3` in C. |
| | 273 | * `ite(e1,e2,e3)`: if-then-else (conditional) expression, like `e1?e2:e3` in C. `e1` must have `Bool` type. `e2` and `e3` must have the same static types, which is the static type of the result. |
