Changes between Version 10 and Version 11 of PIL

Timestamp:

10/05/24 14:45:32 (19 months ago)

Author:

siegel

Comment:

--

PIL

@@ -6 +6 @@
 1. PIL programs can be easily translated to PFG.
 1. PIL must also have a totally well-defined semantics and syntax.
+1. Every operation should have a well-defined outcome, even division by zero or an illegal pointer dereference.  However, when analyzing a PIL program, a user can specify exactly which of these operations should be considered erroneous and reported.   A reasonable default might be to make all of them erroneous.
 1. PIL programs can have nested funtion definitions.
 1. PIL programs can use preprocessor directives like in C
-1. There are no automatic conversions.  All must be done by explicit casts.
-1. `$input`/`$output` variables in global scope (like CIVL-C)
-1. Identifiers are like in C, e.g.,  `x`, `f10`, ...
-1. Keywords, functions, etc. not in C start with `$` (like CIVL-C) 
-1. Libraries: similar to C, `#include <stdlib.h>`, but these name PIL libraries and there are additional PIL libraries
+1. There are no automatic conversions.  There is no "array-pointer pun".  All conversions must be done by explicit casts or other expressions.  To convert an array `a` to a pointer to element 0 of `a`, write `&a[0]`.
+1. PIL supports `$input`/`$output` variables in global scope (like CIVL-C)
+1. PIL identifiers are the same as C's, e.g., `x`, `f10`, ...
+1. Keywords, built-in or library functions, constants, and types not in C start with `$` (like CIVL-C) 
+1. PIL supports libraries: similar to C, `#include <stdlib.h>`, but these name PIL libraries and there are additional standard PIL libraries not in the C standard library
+1. Program order:
+ 1. A program is a set of variable, function, and type definitions.
+ 1. The order is totally irrelevant.
+ 1. A variable can be used anywhere it is in scope.
+ 1. A function can be called anywhere it is in scope.
 1. PIL programs can be divided into multiple files (translation units)
- 1.  One TU can refer to a variable, function, type, in another TU.
- 1. the variable just needs to be declared somewhere in the TU
- 1. the function just needs a prototype somewhere in the TU
- 1. the use of "static" in a variable decl or function def makes it private to that TU (so two can have same name)
- 1. no need for "extern"
- 1. at most one of the TUs declaring the variable can have an initializer
- 1. at most one of the TUs can have a definition for a function
-1. Program order:
- 1. a program is a sequence of variable, function, and type definitions.
- 1. the order is totally irrelevant.
- 1. a variable can be used anywhere it is in scope
- 1. a function can be called anywhere it is in scope
+ 1. One TU can refer to a variable, function, or type, in another TU.
+ 1. The variable just needs to be declared somewhere in the TU.
+ 1. The function just needs a prototype somewhere in the TU.
+ 1. The use of `static` in a variable declaration or function definition makes it private to that TU (so two can have same name), as in C.
+ 1. There is no need for `extern` so this is not in PIL.
+ 1. At most one of the TUs declaring the variable can have an initializer.
+ 1. At most one of the TUs can have a definition for a function.
 
 == Types
-- '''type names''' are used for all declarations (no C declarators).  Examples:
- * `$int[]`: array of integer
- * `$int*`: pointer to integer
- * `$int*[]`: array of pointer to integer
- * `$int[]*`: pointer to array of integer
- * `$int*[]($real)`: function from Real to array of pointer to integer
+- '''type names''' are used for all declarations.  There are no C declarators.  Examples:
+ * `$int[] a`: declares `a` to be an array of integer
+ * `$int* p`: pointer to integer
+ * `$int*[] b`: array of pointer to integer
+ * `$int[]* q`: pointer to array of integer
+ * `$int*[]($real) f`: function from Real to array of pointer to integer
 - basic types: 
-- what are the limits of these types?  to be decided
-- `$int`, `$real` (mathematical types)
-- `struct`: as in C
-- `union`: as in C
-- `T[]`: sequence of `T`.  Note: no "T[n]".  sequences can be assigned, returned, passed as arguments, etc.  
-- `$set<T>` : finite set of `T`, ops to add, contains, remove, size, ...
-- `$map<T1,T2>` : finite map from `T1` to `T2`, ops to put, get, containsKey, ...
-- `$fun<T1,T2>` :  "logic functions":  deterministic, total, side-effect free functions from `T1` to `T2`
-- `$tuple<T,...>` : tuples of specified type (similar to struct)
-- `$rel<T,...>` : relations of specified type (set of tuples)
+ * `$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). 
+ * `$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`
- -   what can be pointed to: var, array element, struct element, union member,  ...
-- Type definitions: `typedef typename ID;`
+- `struct TAG { T1 f1; ... Tn fn; }`: a C struct
+- `union`: similar
+- `T[]`: sequence of `T`.  Note: there is no "T[n]".  Sequences are first-class values: they can be assigned, returned, passed as arguments, etc.  
+- `R(T1, ..., Tn)`: the type of a procedure which consumes values in `T1`, ..., `Tn` and returns a value in `R`.   This is basically C's function type.
+- `$fun<T1,T2>` :  "logic functions":  deterministic, total, side-effect free functions from `T1` to `T2`.  Note however the function may depend on the state (i.e., the state should be considered a hidden input).   A `$pure` function is a function that does not depend on the state.
+- `$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.
+- Type definitions have the form: `typedef typename ID;`
 
 == Functions
 
 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. 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. Logic functions.  One of these has a type of the form `$fun<R,T1,...,Tn>`.
 
@@ -63 +66 @@
 defines a procedure named `f` which consumes inputs of types `T1`, ..., `Tn` and returns a value of type `R`.    `R` can be `void` if the procedure does not return a value.
 
-The definition above defines a '''constant''' `f` of type '''`R(T1, ..., Tn)`'''.   Procedures are first-class values.    One may declare a variable of type `R(T1, ..., Tn)`, a procedure may return a value of that type, a procedure may consume a value of that type, a value of that type may be assigned to a variable, etc.   Hence the procedure type is just like any other type, and procedure definitions define new constants of that type, just as `1` is a constant of type `$int`.   Note this is different from C in that C uses function pointers; PIL dispenses with the need for function pointers.
+The definition above defines a '''constant''' `f` of type '''`R(T1, ..., Tn)`'''.   Procedures are first-class values.    One may declare a variable of type `R(T1, ..., Tn)`, a procedure may return a value of that type, a procedure may consume a value of that type, a value of that type may be assigned to a variable, etc.   Hence the procedure type is just like any other type, and procedure definitions define new constants of that type, just as `1` is a constant of type `$int`.   Note this is different from C in that C uses function pointers; PIL dispenses with the need for function pointers and just uses functions.
 
 A '''procedure call expression'''  has the usual form `g(e1, ..., en)`.  This is an expression that can be used anywhere an expression with side-effects is allowed.  Here, `g` is an expression of functional type, say `R(T1, ..., Tn)`, and `ei` is an expression of type `Ti` (for i=1, ..., n).  The procedure call expression has type `R`.  
@@ -78 +81 @@
 }}}
 
-Procedure definitions can be nested.   It is an error to call a procedure `f` when `f` is not in scope.  (This is similar to Gnu C.)   In other words, if the call takes place in dyscope d, then the definition of `f` must be in d's static scope, or in the parent of d's static scope, or its parent, etc.
+Procedure definitions can be nested.   It is an error to call a procedure `f` when `f` is not in scope.  (This is similar to GNU C.)   In other words, if the call takes place in dyscope d, then the definition of `f` must be in d's static scope, or in the parent of that scope, or its parent, etc.
 
 There is a second way to specify a procedure, using a lambda expression, which is described below.
@@ -84 +87 @@
 === Logic functions
 
-Logic functions are a certain class of functions that have no side-effects, and are deterministic total functions of their arguments and the current state.  A logic function has a type of the form `$fun<R,T1,...,Tn>`, logical functions which consume inputs of type `T1`, ..., `Tn` and return a value of type `R`.  
+Logic functions are a certain class of functions that have no side-effects, and are deterministic total functions of their arguments and the current state.  A logic function has a type of the form `$fun<R,T1,...,Tn>`, which signifies the set of logical functions which consume inputs of type `T1`, ..., `Tn` and return a value of type `R`.  
 
 Logic functions are also first-class objects in PIL.   An application of a logic function `f(x1,... ,xn)` is a side-effect-free expression that can be used anywhere an expression is allowed.  A logic function is not necessarily pure, i.e., the value of an application may depend on any part of the state, not just the arguments.
@@ -103 +106 @@
        <T1,T2> $logic int g($map<T1,T2> f, T1 x) { ... }
 }}}   
-This defines one procedure for each assignment of types to the `Ti`.
+This defines one procedure or logic function for each assignment of types to the `Ti`.
 
 Both kinds of functions can be declared without providing definitions, indicating that the definition can be found in a different translation unit:
@@ -122 +125 @@
 * the `Ti` and `Uj` are types
 * the `xi` and `vj` are variables
+* the `initj` are expressions that can refer to any variables in scope
 * R is a type (the return type), which may be void
 * {S1; ...} is a block (same as in a procedure definition)
@@ -140 +144 @@
 * the `Ti` and `Uj` are types
 * the `xi` and `vj` are variables
+* the `initj` are expressions that can refer to any variables in scope
 * R is a type (the return type), which cannot be void
 * `expr` is a side-effect-free expression of type R 
@@ -146 +151 @@
 The type of this expression is `$fun<R, T1, ..., Tn>`.   As with procedural lambdas, this yields a logic function with a dynamic scope that persists, so can be called anywhere, even after the lambda expression goes out of scope.
 
-In both cases, the initializer expressions `initj` are expressions using any variables in scope.
-
 == Tuples
 
@@ -154 +157 @@
 - `t.i`
 - `($tuple<T1,...>){ x1, ... }`
-- `$logic $tuple<T1,...> $tuple_write($tuple<T1,...> t, $int i, Ti x);`
+- `$pure $logic $tuple<T1,...> $tuple_write($tuple<T1,...> t, $int i, Ti x);`
 
 Mutating expressions:
-- `t.i = x;`
+- `t.i = x`
 
 == Sets
@@ -164 +167 @@
 - `s1 == s2`
 - `($set<T>)$empty`   // empty set of type T
-- `$logic _Bool $set_in(T x, $set<T> s);`  // is x an element of s?
-- `$logic $set<T> $set_with($set<T> s, T x);` // s U {x}
-- `$logic $set<T> $set_without($set<T> s, T x);` // s - {x}
-- `$logic $set<T> $set_union($set<T> s1, $set<T> s2);` // s1 U s2 
-- `$logic $set<T> $set_difference($set<T> s1, $set<T> s2);` // s1-s2 
-- `$logic $set_intersection($set<T> s1, $set<T> s2);` // s1 \cap s2
-- `$logic T[] $set_elements($set<T> s);`
-- `$logic _Bool $set_isSubsetOf($set<T> s1, $set<T> s2);`
-- `$logic $set<U> $set_map($set<T> s, $fun<T,U> f);`
+- `$pure $logic _Bool $set_in(T x, $set<T> s);`  // 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);`
+- `$pure $logic _Bool $set_isSubsetOf($set<T> s1, $set<T> s2);`
+- `$pure $logic $set<U> $set_map($set<T> s, $fun<T,U> f);`
 
 Mutating procedures: