| 69 | | * `$bool` : boolean type, values are `$true` and `$false` |
| 70 | | * `$proc` : process type |
| 71 | | * `$scope` : scope type |
| 72 | | * `$char` : character type. Alternatively, get rid of this and just use an integer type. |
| 73 | | * `$bundle` : type representing some un-typed chunk of data |
| 74 | | * `$heap` : heap type |
| 75 | | * `$range` : ordered set of integers |
| 76 | | * `$domain` : ordered set of tuples of integers |
| 77 | | * `$domain(n)`, n is an integer at least 1; subtype of `$domain` in which all tuples have arity n. |
| 78 | | * `enum` types. |
| | 69 | * `\Bool` : boolean type, values are `$true` and `$false` |
| | 70 | * `\Proc` : process type |
| | 71 | * `\Scope` : scope type |
| | 72 | * `\Char` : character type. Alternatively, get rid of this and just use an integer type. |
| | 73 | * `\Bundle` : type representing some un-typed chunk of data |
| | 74 | * `\Heap` : heap type |
| | 75 | * `\Range` : ordered set of integers |
| | 76 | * `\Domain` : ordered set of tuples of integers |
| | 77 | * `\Domain(n)`, n is an integer at least 1; subtype of `$domain` in which all tuples have arity n. |
| | 78 | * `\Enum` types. |
| 80 | | * `$integer` : the mathematical integers |
| 81 | | * `$int(lo,hi,wrap)` |
| 82 | | * lo, hi are integers, wrap is boolean |
| 83 | | * 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. |
| | 80 | * `\Integer` : the mathematical integers |
| | 81 | * `\Int(lo,hi,wrap)` |
| | 82 | * `lo`, `hi` are integers, `wrap` is boolean |
| | 83 | * 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. |
| 85 | | * `$hint` : Herbrand integers. Values are unsimplified symbolic expressions. |
| 86 | | * `$real` : the mathematical real numbers |
| 87 | | * `$float(e,f)`, e, f are integers, each at least 1. **Same question for e and f as for lo and hi.** |
| | 85 | * `\Hint` : Herbrand integers. Values are unsimplified symbolic expressions. |
| | 86 | * `\Real` : the mathematical real numbers |
| | 87 | * `\Float(e,f)`, e, f are integers, each at least 1. **Same question for e and f as for lo and hi.** |
| 95 | | * `union`: similar to structs |
| 96 | | * `T[]` : array-of-T |
| 97 | | * Function<S1,...,Sn;T> |
| 98 | | * function consuming S1,...,Sn and returning T. T can be void. The actual notation is the horrible C notation. |
| 99 | | * `$mem` : type representing a memory set. May be thought of as a set of pointers. |
| 100 | | * `void*` : all pointers, a subtype of `$mem` |
| 101 | | * `T*` : pointer-to-T, subtype of `void*` |
| | 95 | * `\Union`: similar to structs |
| | 96 | * `\Array(T)` : array-of-T |
| | 97 | * `\Function(S1,...,Sn;T)` |
| | 98 | * function consuming `S1,...,Sn` and returning `T`. `T` can be void. The actual notation is the horrible C notation. |
| | 99 | * `\Mem` : type representing a memory set. May be thought of as a set of pointers. |
| | 100 | * `\Pointer(\Void)` : all pointers, a subtype of `\Mem` |
| | 101 | * `\Pointer(T)` : pointer-to-T, subtype of `\Pointer(\Void)` |
| 150 | | * `$true`, `$false` : values of type `$bool` |
| 151 | | * 123, -123, 3.1415, etc. : values of type `$integer`, `$int`, `$real`, `$float` |
| | 150 | * `$true`, `$false` : values of type `\Bool` |
| | 151 | * 123, -123, 3.1415, etc. : values of type `\Integer`, `\Int`, `\Real`, `\Float` |
| 154 | | * `(T[]){e0, e1, ...}` : values of type `T[]` |
| 155 | | * `(S){e0, ...}` : values of type `S` (struct literal) |
| 156 | | * `e1..e2`, `e1..e2#e3` : values of type `$range` |
| | 154 | * `\cast(\Array(T), {e0, e1, ...})` : values of type `\Array(T)` |
| | 155 | * `\cast(S, {e0, ...})` : values of type `S` (struct literal) |
| | 156 | * `e1..e2`, `e1..e2#e3` : values of type `\Range` |
| 163 | | * `$sizeof(T)` : the size of the named type |
| 164 | | * `$sizeof(e)` : the size of the value of expression `e` |
| 165 | | * `$initval(T)` : initial value of the named type |
| 166 | | * `$defined(e)` : is `e` defined? Type is `$bool` |
| 167 | | * `$has_next(dom, i, j, k, …)`: an expression of boolean type, testing if the domain `dom` contains any element after `(i, j, k, ...)` |
| 168 | | * `e1+e2` : addition. One of the following must hold: |
| | 163 | * `\sizeof(T)` : the size of the named type |
| | 164 | * `\sizeof(e)` : the size of the value of expression `e` |
| | 165 | * `\initval(T)` : initial value of the named type |
| | 166 | * `\defined(e)` : is `e` defined? Type is `$bool` |
| | 167 | * `\has_next(dom, i, j, k, …)`: an expression of boolean type, testing if the domain `dom` contains any element after `(i, j, k, ...)` |
| | 168 | * `\add(e1, e2)` : numeric addition. |
| 170 | | * `e1` has pointer type and `e2` has an integer type. (Alternatively, we could define a separate function `$pointer_add(p,n)`.) |
| 171 | | * `e1-e2` : subtraction |
| 172 | | * `e1*e2` : multiplication |
| 173 | | * `e1/e2` : division |
| | 170 | * `\padd(e1, e2)`: pointer addition. |
| | 171 | * `e1` has pointer type and `e2` has an integer type. |
| | 172 | * `\subtract(e1, e2)` : subtraction |
| | 173 | * `\multiply(e1, e2)` : multiplication |
| | 174 | * `\divide(e1, e2)` : division |
| 175 | | * `e1%e2` : modulus |
| 176 | | * `e1[e2]` : array subscript expression. Note that `e1` must have array type, not pointer type. (This is different from C.) If `e1` has pointer type, use `*(e1+e2)` instead. |
| 177 | | * `*e` : pointer dereference |
| 178 | | * `&e` : address-of |
| 179 | | * `!e` : logical not |
| 180 | | * `-e` : negative |
| 181 | | * (T)e : casts `e` to a value of the named type |
| | 176 | * `\mod(e1, e2)` : modulus |
| | 177 | * `\array_subscript(e1, e2)` : array subscript expression. Note that `e1` must have array type, not pointer type. (This is different from C.) If `e1` has pointer type, use `\deref(\padd(e1, e2))` instead. |
| | 178 | * `\deref(e)` : pointer dereference |
| | 179 | * `\address_of(e)` : address-of |
| | 180 | * `\not(e)` : logical not |
| | 181 | * `\neg(e)` : negative |
| | 182 | * `\cast(T, e)` : casts `e` to a value of the named type |
| 184 | | * `e1==e2`, `e1!=e2` |
| 185 | | * `e1&&e2`, `e1||e2` |
| 186 | | * `e1?e2:e3` |
| 187 | | * `e1<e2`, `e1<=e2` |
| | 185 | * `\eq(e1, e2)`, `\neq(e1, e2)`: equality/inequality test |
| | 186 | * `\and(e1, e2)`, `\or(e1, e2)`: logical and/or operation |
| | 187 | * `\cond(e1, e2, e3)`: conditional expression, equivalent to `e1?e2:e3` in C. |
| | 188 | * `\lt(e1, e2)`, `\lte(e1, e2)`: less than/less than or equal to |
