| 54 | | Like in C. These can be nested. Obviously they can have side-effects, be nondeterministic, and the behavior can depend on non-local state. A procedure call `f(x1,...,xn)` is an expression that can be used anywhere an expression with side-effects is allowed. Imperative procedures are not values and cannot be assigned to anything. However, as in C, a pointer to a procedure is a first-class value that can be assigned, used as an argument, returned, etc. There is a procedure type, similar to C's function type, e.g., |
| 55 | | {{{ |
| 56 | | typedef int(int) i2i; |
| 57 | | }}} |
| 58 | | defines `i2i` to be the type "procedure consuming int and returning int". Most commonly, pointers to procedure types will be used, e.g., |
| 59 | | {{{ |
| 60 | | typedef int(int)* i2ip; |
| 61 | | }}} |
| 62 | | defines the type "pointer to procedure from int to int". As in C, a pointer to a procedure can be used in a procedure call. 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. |
| | 54 | A procedure is similar to a C function. It consumes some values of a specified type and possibly returns a value of a specified type. Procedure definitions look like C function definitions: |
| | 55 | {{{ |
| | 56 | R f(T1 x1, ..., Tn xn) { stmts } |
| | 57 | }}} |
| | 58 | 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 value. |
| | 59 | |
| | 60 | 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. |
| | 61 | |
| | 62 | 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`. |
| | 63 | |
| | 64 | Procedure calls can have side-effects, be nondeterministic, and the behavior can depend on non-local state; they may access any variable in scope, the statements may dereference pointers, etc. |
| | 65 | |
| | 66 | {{{ |
| | 67 | int f(int x) { return x+1; } // f is a constant of type int(int) |
| | 68 | int callon1( (int)int g ) { |
| | 69 | return g(1); |
| | 70 | } |
| | 71 | ... |
| | 72 | int y = callon1(f); // y is now 2 |
| | 73 | }}} |
| | 74 | |
| | 75 | 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. |
| 72 | | Typically specified by a $lambda expression. These are first-class objects in PIL: one can be assigned to a variable, passed as an argument in a function call (including a procedure call), and can be returned by a function. Each has a type of the form `$fun<U,T1,...,Tn>` (functions from `T1` x ... x `Tn` to `U`). They are side-effect-free. 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. |
| 73 | | |
| | 87 | 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`. |
| | 88 | |
| | 89 | 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. |
| | 90 | |
| | 91 | Despite the apparent similarity with procedures, logic functions and procedures are clearly distinguished and one cannot be converted to another. |
| | 92 | |
| | 93 | A logic function can be defined as follows: |
| | 94 | {{{ |
| | 95 | $logic R f(T1 x1, ..., xn) = expr; |
| | 96 | }}} |
| | 97 | where `expr` is a side-effect-free expression of type `R` and can refer to any variables in scope. |
| | 98 | |
| 90 | | The type of this expression is `R(T1, ..., Tn)`. |
| 91 | | |
| 92 | | Logic function lambda syntax: |
| | 115 | The type of this expression is `R(T1, ..., Tn)`. The resulting value of this is type is a procedure can be called or assigned to a variable, etc., just like any other procedure. |
| | 116 | |
| | 117 | 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. That dyscope 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. |
| | 118 | |
| | 119 | A lambda expression that specifies a logic function has the form |
| 106 | | |
| 107 | | ==== Semantics |
| 108 | | |
| 109 | | FIX THIS: difference between logic and procedural functions... |
| 110 | | |
| 111 | | |
| 112 | | |
| 113 | | The lambda expression is evaluated to yield a *closure*: an ordered pair consisting of a dyscope and an expression. The dyscope has variables `v1`, ..., `vm`, initialized by evaluating `init1`, ..., `initm`. The dyscope has no parent scope, it is associated only with the closure. The expression is `expr`. The dyscope is destroyed whenever it becomes unreachable, i.e., whenever no part of the state is assigned the closure. |
| 114 | | |
| 115 | | A logic function application `f(e1,...,en)` is evaluated by first evaluating the arguments `ei`, then assigning the `ei` to the `xi` and evaluating expr in the closure dyscope. Note that since expr has no side effects, the values of the xi are constant. [Note: a possible change is to allow side-effects in logic functions.] |
