Changes between Version 12 and Version 13 of PIL

Timestamp:

10/05/24 15:33:12 (19 months ago)

Author:

siegel

Comment:

--

PIL

@@ -36 +36 @@
  * `$int*[]($real) f`: function from Real to array of pointer to integer
 - basic types: 
+ * `$bool` : the set consisting of `$true` and `$false`
  * `$int`: the set of integers
  * `$real`: the set of Reals
- * `fint[lo,hi]`: set of integers between `lo` and `hi`, inclusive. `lo` and `hi` are constant expressions so are known at compile time.
- * `uint[hi]`: nonnegative integers less than the constant expression`hi`.  Arithmetic is performed modulo `hi` (like C's unsigned integer types). 
+ * `$int<lo,hi>`: set of integers between `lo` and `hi`, inclusive. `lo` and `hi` are constant expressions so are known at compile time.
+ * `$uint<hi>`: nonnegative integers less than the constant expression `hi`.  Arithmetic is performed modulo `hi` (like C's unsigned integer types). 
  * `$float<p,emax>`: the set of IEEE binary floating point numbers with precision `p` and emax `emax`.  These are also constant expressions.
 - `T*`: pointer to `T`
@@ -49 +50 @@
 - `$set<T>` : finite set of `T`
 - `$map<T1,T2>` : finite map from `T1` to `T2`.  A map is a set of ordered pairs `(x,y)` with the property that if `(x,y)` and `(x,z)` are in the map, then `y`=`z`.
-- `$tuple<T,...>` : tuples of specified type.  This is similar to `struct`, but is anonymous and the fields do not have names.
+- `$tuple<T,...>` : tuples of specified type.  This is similar to `struct`, but there is no tag and the fields do not have names.
 - Type definitions have the form: `typedef typename ID;`
 
@@ -157 +158 @@
 - `t.i` : the value of component `i` (a constant integer) of tuple `t`
 - `($tuple<T1,...>){ expr1, ... }` : the literal tuple with the given list of components.
-- `t[i : expr1]` : the tuple which is the same as `t`, except for component `i` (a constant integer), which has value `expr1`
+- `t.[i : expr1]` : the tuple which is the same as `t`, except for component `i` (a constant integer), which has value `expr1`
 
 Mutating expressions:
-- `t[i] = expr` : sets component `i` of tuple `t` to `expr`
+- `t.[i] = expr` : sets component `i` of tuple `t` to `expr`
 
 == Sets
@@ -169 +170 @@
 
 Logic functions:
-- `$pure $logic _Bool $set_contains($set<T> s, T x);` :  // is x an element of s?
-- `$pure $logic $set<T> $set_with($set<T> s, T x);` : // s U {x}
-- `$pure $logic $set<T> $set_without($set<T> s, T x);` : // s - {x}
-- `$pure $logic $set<T> $set_union($set<T> s1, $set<T> s2);` : // s1 U s2 
-- `$pure $logic $set<T> $set_difference($set<T> s1, $set<T> s2);` : // s1-s2 
-- `$pure $logic $set_intersection($set<T> s1, $set<T> s2);` : // s1 \cap s2
-- `$pure $logic T[] $set_elements($set<T> s);` : // returns the set of elements of `s` as an array in some deterministic order
-- `$pure $logic _Bool $set_isSubsetOf($set<T> s1, $set<T> s2);` : is `s1` a subset of `s2`?
-- `$pure $logic $set<U> $set_map($set<T> s, $fun<T,U> f);` : the set { f(x) | x in s}
-- `$pure logic $set<T> $set_comprehension($set<T>, $fun<T,_Bool> p);` : the set { x in s | p(x) }
+- `$pure $logic $bool $set_contains($set<T> s, T x);`
+ * is `x` an element of `s`?
+- `$pure $logic $set<T> $set_with($set<T> s, T x);`
+ * `s` U {`x`}
+- `$pure $logic $set<T> $set_without($set<T> s, T x);`
+ * `s` - {`x`}
+- `$pure $logic $set<T> $set_union($set<T> s1, $set<T> s2);`
+ * `s1` U `s2` 
+- `$pure $logic $set<T> $set_difference($set<T> s1, $set<T> s2);`
+ * `s1`-`s2` 
+- `$pure $logic $set_intersection($set<T> s1, $set<T> s2);`
+ * `s1`  \cap `s2`
+- `$pure $logic T[] $set_elements($set<T> s);`
+ * returns the set of elements of `s` as an array in some deterministic order
+- `$pure $logic $bool $set_isSubsetOf($set<T> s1, $set<T> s2);`
+ * is `s1` a subset of `s2`?
+- `$pure $logic $set<U> $set_map($set<T> s, $fun<T,U> f);`
+ * { `f`(`x`) | `x` in `s`}
+- `$pure logic $set<T> $set_comprehension($set<T>, $fun<T,$bool> p);`
+ * { `x` in `s` | `p`(`x`) }
 
 Mutating procedures:
-- ` _Bool $set_add($set<T> * this, T x);`
-- ` _Bool $set_remove($set<T> * this, T x);`
+- `$bool $set_add($set<T> * this, T x);`
+- `$bool $set_remove($set<T> * this, T x);`
 - `void $set_addAll($set<T> * this, $set<T> that);`
 - `void $set_removeAll($set<T> * this, $set<T> that);`
@@ -189 +200 @@
 ==  Sequences (arrays)
 
-Non-mutating expressions:
+Expressions:
 - `a1 == a2`
 - `a[i]`
-- `(T[]){ x1, ... }`
+- `(T[]){ expr1, ... }`
 
 Logic functions:
-- `$logic T[] $seq_fun($int len, $fun<$int,T> f);`
-- `$logic T[] $seq_uniform($int n, T val);`
-- `$logic $int $length(T[] a);` // length of a
-- `$logic T[] $seq_write(T[] a, int i, T x);`  // a[i:=x]
-- `$logic T[] $seq_subseq(T[] a, int i, int n);`  // a[i..i+n-1]
-- `$logic T[] $seq_without(T[] a, int i);` // a with position i removed
-- `$logic T[] $seq_with(T[] a, int i, T x);`
-- `$logic T[] $seq_concat(T[] a1, T[] a2);`
-- `$logic U[] $seq_map(T[] a, $fun<T,U> f);`
-- `$logic T[] $seq_filter(T[] a, $fun<T,_Bool> f);`
-- `$logic U $seq_foldl(T[] a, $fun<$tuple<T,U>,U> f, U init);`
-- `$logic U $seq_foldr(T[] a, $fun<$tuple<T,U>,U> f, U init); `
+- `$pure $logic T[] $seq_fun($int len, $fun<$int,T> f);`
+- `$pure $logic T[] $seq_uniform($int n, T val);`
+- `$pure $logic $int $length(T[] a);` // length of a
+- `$pure $logic T[] $seq_write(T[] a, int i, T x);`  // a[i:=x]
+- `$pure $logic T[] $seq_subseq(T[] a, int i, int n);`  // a[i..i+n-1]
+- `$pure $logic T[] $seq_without(T[] a, int i);` // a with position i removed
+- `$pure $logic T[] $seq_with(T[] a, int i, T x);`
+- `$pure $logic T[] $seq_concat(T[] a1, T[] a2);`
+- `$pure $logic U[] $seq_map(T[] a, $fun<T,U> f);`
+- `$pure $logic T[] $seq_filter(T[] a, $fun<T,$bool> f);`
+- `$pure $logic U $seq_foldl(T[] a, $fun<$tuple<T,U>,U> f, U init);`
+- `$pure $logic U $seq_foldr(T[] a, $fun<$tuple<T,U>,U> f, U init);`
 
 Mutating expressions:
@@ -222 +233 @@
 - `($map<K,V>)$empty`
 - `$logic V $map_get($map<K,V> K key);`
-- `$logic _Bool $map_containsKey($map<K,V> map, K key);`
-- `$logic _Bool $map_containsValue($map<K,V> map, V val);`
+- `$logic $bool $map_containsKey($map<K,V> map, K key);`
+- `$logic $bool $map_containsValue($map<K,V> map, V val);`
 - `$logic $map<K,V> $map_with($map<K,V> map, K key, V val);`
 - `$logic $map<K,V> $map_without($map<K,V> map, K key);`