Changes between Version 15 and Version 16 of PIL

Timestamp:

10/06/24 09:14:29 (19 months ago)

Author:

siegel

Comment:

--

PIL

@@ -16 +16 @@
 1. Program order:
  1. A program is a set of variable, function, and type definitions.
- 1. The order is totally irrelevant.
+ 1. The order is totally irrelevant. [NOTE: except for initializers?]
  1. A variable can be used anywhere it is in scope.
  1. A function can be called anywhere it is in scope.
@@ -50 +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 there is no tag and the fields do not have names.
+- `$tuple<T1,...>` : 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;`
 
@@ -56 +56 @@
 
 There are two kinds of functions in PIL:
-1. Imperative functions = "procedures".  A procedure has a type of the form `R(T1,...,Tn)` where `R` is the return type and the `Ti` are the input types.
+1. Procedural functions = "procedures".  A procedure has a type of the form `R(T1,...,Tn)` where `R` is the return type and the `Ti` are the input types.
 1. Logic functions.  One of these has a type of the form `$fun<R,T1,...,Tn>`.
 
@@ -96 +96 @@
 A logic function can be defined as follows:
 {{{
-  $logic R f(T1 x1, ..., xn) = expr;
+  $logic R f(T1 x1, ..., Tn xn) = expr;
 }}}
 where `expr` is a side-effect-free expression of type `R` and can refer to any variables in scope.
@@ -121 +121 @@
 A lambda expression that specifies a procedure closure has the form:
 {{{
-  $lambda [U1 v1=init1; ... Um vm=initm;] R (T1 x1, ..., Tn xn) { S1; ... }
+  $lambda [U1 v1=init1; ... Um vm=initm;] R (T1 x1, ..., Tn xn) { stmts }
 }}}
 where
@@ -132 +132 @@
 * the only variables that can occur free in the block are the `xi` and `vj`.
 
-The type of this expression is `R(T1, ..., Tn)`.   The resulting value of this is type is a procedure which can be called or assigned to a variable, etc., just like any other procedure value.
+The type of this expression is `R(T1, ..., Tn)`.   The resulting value is a procedure which can be called or assigned to a variable, etc., just like any other procedure value.
 
 Note that the definition can only use the specified variables.  Evaluating this expression yields a closure, which is a pair consisting of a dyscope and the body of the procedure.   The dyscope has variables `vj`, which are initialized by evaluating the `initj` when the lambda expression is evaluated.  The body of the procedure may read and write to the `vj`.  That dyscope has no parent and will live as long as the procedure is around.  Hence a function may return a closure and that closure may still be called at any time, anywhere in the program, regardless of whether the original lambda expression is in scope.
@@ -208 +208 @@
 Expressions:
 - `a1 == a2`
- * the two arrays have the same type and length and corresponding elements are equal
+ * the two sequences have the same type and length and corresponding elements are equal
 - `a[i]`
- * the `i`-th element of `a`
+ * the `i`-th element of `a`. Here `a` is an expression of type `T[]` and `i` is an expression of type `$int`.
 - `a[i:=x]`
- * the sequence which is the same as `a`, exception in position `i`, where it has value `x`
+ * the sequence which is the same as `a`, except in position `i`, where it has value `x`.  Here `a` is an expression of type `T[]`, `i` is an expression of type `$int`, and `x` is an expression of type `T`
 - `(T[]){ expr1, ... }`
+ * the sequence obtained by evaluating the given expressions, each of which has type `T`
 
 Logic functions:
 - `$pure $logic T[] $seq_fun($int len, $fun<$int,T> f);`
+ * the sequence of length `len` whose value at position `i` is `f(i)`
 - `$pure $logic T[] $seq_uniform($int n, T val);`
-- `$pure $logic $int $length(T[] a);` // length of a
-- `$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);`
+ * the sequence of length `n` in which every component is `val`
+- `$pure $logic $int $length(T[] a);`
+ * the length of `a`
+- `$pure $logic T[] $seq_subseq(T[] a, int i, int n);`
+ * the sequence of length n,  a[i..i+n-1]
+- $pure $logic T[] $seq_with(T[] a, int i, T x);`
+ * the sequence obtained from `a` by inserting `x` at position `i` and shifting the subsequent elements up
+- `$pure $logic T[] $seq_without(T[] a, int i);`
+ * the sequence obtained from `a` by deleting the element in position `i` and shifting subsequent elements down
 - `$pure $logic T[] $seq_concat(T[] a1, T[] a2);`
+ * the sequence obtained by concatenating the two given ones
 - `$pure $logic U[] $seq_map(T[] a, $fun<T,U> f);`
+ * the sequence obtained by applying `f` to every element of `a`
 - `$pure $logic T[] $seq_filter(T[] a, $fun<T,$bool> f);`
+ * the sequence obtained from `a` by removing every element for which `f(a[i])` is `$false`
 - `$pure $logic U $seq_foldl(T[] a, $fun<$tuple<T,U>,U> f, U init);`
+ * the sequence b which has the same length as `a`, and where b[0]=f(init, a[0]), b1=f(b[0], a[1]), b2=f(b[1], a[2]), etc.
 - `$pure $logic U $seq_foldr(T[] a, $fun<$tuple<T,U>,U> f, U init);`
+ * the sequence b which has the same length as `a`, and where b[n-1]=f(a[n-1], init), b[n-2]=f(a[n-2], b[n-1]), etc.
 
 Mutating expressions:
 - `a[i]=x;`
+ * assigns value of `x` to `a[i]` and returns value of `x`.   Here `a` has array type, say `T[]`, `x` is an expression of type `T`, and `i` is an expression of type `$int`
 
 Mutating procedures:
@@ -240 +253 @@
 Side-effect-free expressions:
 - `m1 == m2`
+ * the two maps have the same type and the same entries
 - `($map<K,V>)$empty`
+ * the empty map from `K` to `V`
 
 Logic functions: