Changes between Version 1 and Version 2 of PIL


Ignore:
Timestamp:
10/02/24 21:27:50 (20 months ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • PIL

    v1 v2  
    6161- `($set<T>)$empty`   // empty set of type T
    6262- `$pure _Bool $set_in(T x, $set<T> s);`  // is x an element of s?
    63 
    64   $pure $set<T> $set_with($set<T> s, T x); // s U {x}
    65   $pure $set<T> $set_without($set<T> s, T x); // s - {x}
    66   $pure $set<T> $set_union($set<T> s1, $set<T> s2); // s1 U s2
    67   $pure $set<T> $set_difference($set<T> s1, $set<T> s2); // s1-s2
    68   $pure $set_intersection($set<T> s1, $set<T> s2); // s1 \cap s2
    69   $pure T[] $set_elements($set<T> s);
    70   $pure _Bool $set_isSubsetOf($set<T> s1, $set<T> s2);
    71   $pure $set<U> $set_map($set<T> s, $fun<T,U> f);
    72 
    73 
    74   Mutation functions:
    75   _Bool $set_add($set<T> * this, T x);
    76   _Bool $set_remove($set<T> * this, T x);
    77   void $set_addAll($set<T> * this, $set<T> that);
    78   void $set_removeAll($set<T> * this, $set<T> that);
    79   void $set_keepOnly($set<T> * this, $set<T> that);
    80 
    81   Sequences (arrays)
    82   =========
    83   Expressions:
    84   a1 == a2
    85   a[i]
    86   (T[]){ x1, ... }
     63- `$pure $set<T> $set_with($set<T> s, T x);` // s U {x}
     64- `$pure $set<T> $set_without($set<T> s, T x);` // s - {x}
     65- `$pure $set<T> $set_union($set<T> s1, $set<T> s2);` // s1 U s2
     66- `$pure $set<T> $set_difference($set<T> s1, $set<T> s2);` // s1-s2
     67- `$pure $set_intersection($set<T> s1, $set<T> s2);` // s1 \cap s2
     68- `$pure T[] $set_elements($set<T> s);`
     69- `$pure _Bool $set_isSubsetOf($set<T> s1, $set<T> s2);`
     70- `$pure $set<U> $set_map($set<T> s, $fun<T,U> f);`
     71
     72Mutating procedures:
     73- ` _Bool $set_add($set<T> * this, T x);`
     74- ` _Bool $set_remove($set<T> * this, T x);`
     75- `void $set_addAll($set<T> * this, $set<T> that);`
     76- `void $set_removeAll($set<T> * this, $set<T> that);`
     77- `void $set_keepOnly($set<T> * this, $set<T> that);`
     78
     79==  Sequences (arrays)
     80
     81Non-mutating expressions:
     82- `a1 == a2`
     83- `a[i]`
     84- `(T[]){ x1, ... }`
     85
     86Logic functions:
     87- `$pure T[] $seq_fun($int len, $fun<$int,T> f);`
     88- `$pure T[] $seq_uniform($int n, T val);`
     89- `$pure $int $length(T[] a);` // length of a
     90- `$pure T[] $seq_write(T[] a, int i, T x);`  // a[i:=x]
     91- `$pure T[] $seq_subseq(T[] a, int i, int n);`  // a[i..i+n-1]
     92- `$pure T[] $seq_without(T[] a, int i);` // a with position i removed
     93- `$pure T[] $seq_with(T[] a, int i, T x);`
     94- `$pure T[] $seq_concat(T[] a1, T[] a2);`
     95- `$pure U[] $seq_map(T[] a, $fun<T,U> f);`
     96- `$pure T[] $seq_filter(T[] a, $fun<T,_Bool> f);`
     97- `$pure U $seq_foldl(T[] a, $fun<$tuple<T,U>,U> f, U init);`
     98- `$pure U $seq_foldr(T[] a, $fun<$tuple<T,U>,U> f, U init); `
     99
     100Mutating expressions:
     101- `a[i]=x;`
     102
     103Mutating procedures:
     104- `T $seq_remove(T[] * this, int i);`
     105- `void $seq_insert(T[] * this, int i, T x);`
     106- `void $seq_append(T[] * this, T[] that);`
     107
     108==  Maps
     109
     110Non-mutating expressions:
     111- `m1 == m2`
     112- `($map<K,V>)$empty`
     113- `$pure V $map_get($map<K,V> K key);`
     114- `$pure _Bool $map_containsKey($map<K,V> map, K key);`
     115- `$pure _Bool $map_containsValue($map<K,V> map, V val);`
     116- `$pure $map<K,V> $map_with($map<K,V> map, K key, V val);`
     117- `$pure $map<K,V> $map_without($map<K,V> map, K key);`
     118- `$pure $set<K> $map_keys($map<K,V> map);`
     119- `$pure $set<$tuple<K,V>> $map_entries($map<K,V> map);`
     120
     121Mutating procedures:
     122- `V $map_put($map<K,V> * this, K key, V val);`
     123- `V $map_remove($map<K,V> * this, K key);`
     124- `void $map_removeAll($map<K,V> * this, $set<K> keys);`
     125- `void $map_addAll($map<K,V> * this, $map<K,V> that);`
     126
     127== Functions
     128
     129There are two kinds of functions in PIL:
     1301. (Imperative) procedures
     1311. Logic functions
     132
     133=== Procedures
     134
     135Like 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, exactly like C's function type, e.g.,
     136{{{
     137       typedef int(int) i2i;
     138}}}
     139defines `i2i` to be the type "procedure consuming int and returning int".  Most commonly, pointers to procedure types will be used, e.g.,
     140{{{
     141       typedef int(int)* i2ip;
     142}}}
     143defines the type "pointer to procedure from int to int".  As in C, a pointer to a procedure can be used in a procedure call.
     144
     145A procedure definition can be templated:
     146{{{     
     147       <T1,T2,...> <procedure def>
     148}}}   
     149This defines one procedure for each assignment of types to the Ti.
     150     
     151=== Logic functions
     152
     153Typically specified by a $lambda expression. These are first-class objects in PIL: they can be assigned to variables, 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<T1,...,Tn;U>` (functions from `T1` x ... x `Tn` to `U`).  They are side-effect-free.  An application of a logic function `f(x1,...,xn)` is an 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.
    87154 
    88   Built-in logic functions:
    89   $pure T[] $seq_fun($int len, $fun<$int,T> f);
    90   $pure T[] $seq_uniform($int n, T val);
    91   $pure $int $length(T[] a); // length of a
    92   $pure T[] $seq_write(T[] a, int i, T x);  // a[i:=x]
    93   $pure T[] $seq_subseq(T[] a, int i, int n);  // a[i..i+n-1]
    94   $pure T[] $seq_without(T[] a, int i); // a with position i removed
    95   $pure T[] $seq_with(T[] a, int i, T x);
    96   $pure T[] $seq_concat(T[] a1, T[] a2);
    97   $pure U[] $seq_map(T[] a, $fun<T,U> f);
    98   $pure T[] $seq_filter(T[] a, $fun<T,_Bool> f);
    99   $pure U $seq_foldl(T[] a, $fun<$tuple<T,U>,U> f, U init);
    100   $pure U $seq_foldr(T[] a, $fun<$tuple<T,U>,U> f, U init);
    101 
    102   Mutating operations:
    103   a[i]=x;
    104 
    105   Mutating Procedures:
    106   T $seq_remove(T[] * this, int i);
    107   void $seq_insert(T[] * this, int i, T x);
    108   void $seq_append(T[] * this, T[] that);
    109 
    110   Maps
    111   ====
    112   Non-mutation:
    113   m1 == m2
    114   ($map<K,V>)$empty
    115   $pure V $map_get($map<K,V> K key);
    116   $pure _Bool $map_containsKey($map<K,V> map, K key);
    117   $pure _Bool $map_containsValue($map<K,V> map, V val);
    118   $pure $map<K,V> $map_with($map<K,V> map, K key, V val);
    119   $pure $map<K,V> $map_without($map<K,V> map, K key);
    120   $pure $set<K> $map_keys($map<K,V> map);
    121   $pure $set<$tuple<K,V>> $map_entries($map<K,V> map);
    122 
    123   Mutation:
    124   V $map_put($map<K,V> * this, K key, V val);
    125   V $map_remove($map<K,V> * this, K key);
    126   void $map_removeAll($map<K,V> * this, $set<K> keys);
    127   void $map_addAll($map<K,V> * this, $map<K,V> that);
    128 
    129   Functions
    130   =========
    131   There are two kinds of functions in PIL:
    132  
    133   1. (Imperative) procedures, like in C.  These can be nested.
    134      Obviously they can have side-effects, be nondeterministic, and
    135      the behavior can depend on non-local state.  A procedure call
    136      f(x1,...,xn) is an expression that can be used anywhere an
    137      expression with side-effects is allowed.  Imperative procedures
    138      are not values and cannot be assigned to anything.  However, as
    139      in C, a pointer to a procedure is a first-class value that can be
    140      assigned, used as an argument, returned, etc.   There is a
    141      procedure type, exactly like C's function type, e.g.,
    142 
    143        typedef int(int) i2i;
    144 
    145      defines i2i to be the type "procedure consuming int and returning
    146      int".  Most commonly, pointers to procedure types will be used,
    147      e.g.,
    148 
    149        typedef int(int)* i2ip;
    150 
    151      defines the type "pointer to procedure from int to int".  As in
    152      C, a pointer to a procedure can be used in a procedure call.
    153 
    154      A procedure definition can be templated:
    155      
    156        <T1,T2,...> <procedure def>
    157        
    158      This defines one procedure for each assignment of types to
    159      the Ti.
    160      
    161   2. Logic functions.  Typically specified by a $lambda expression.
    162      These are first-class objects in PIL: they can be assigned to
    163      variables, passed as an argument in a function call (including a
    164      procedure call), and can be returned by a function.  Each has a
    165      type of the form $fun<T1,...,Tn;U> (functions from T1 x...x Tn to
    166      U).  They are side-effect-free.  An application of a logic
    167      function f(x1,...,xn) is an expression that can be used anywhere
    168      an expression is allowed.  A logic function is not necessarily
    169      pure, i.e., the value of an application may depend on any part of
    170      the state, not just the arguments.
    171  
    172   Lambda expressions: have the form
    173 
     155=== Lambda expressions
     156
     157These have the form
     158{{{
    174159  $lambda (T1 x1, ..., Tn xn) {U1 v1=init1; ... Um vm=initm; expr}
    175 
    176   where the Ti and Uj are types, the xi and vj are variables,
    177   and expr is an expression in which the only variables that can
    178   occur free are the x1,..., xn, v1,..., vm.  The initializer
    179   expressions initj are expressions using any variables in scope.
    180   The expression has type $fun<T1,...,Tn; V>, where V is the type
    181   of expr.
    182 
    183   Semantics: the lambda expression is evaluated to yield a *closure*:
    184   an ordered pair consisting of a dyscope and an expression.  The
    185   dyscope has variables v1, ..., vm, initialized by evaluating init1,
    186   ..., initm.  The dyscope has no parent scope, it is associated only
    187   with the closure.  The expression is expr.  The dyscope is destroyed
    188   whenever it becomes unreachable, i.e., whenever no part of the state
    189   is assigned the closure.
    190 
    191   A logic function application f(e1,...,en) is evaluated by first
    192   evaluating the arguments ei, then assigning the ei to the xi and
    193   evaluating expr in the closure dyscope.  Note that since expr
    194   has no side effects, the values of the xi are constant.
    195   [Note: a possible change is to allow side-effects in logic
    196   functions.]
    197 
    198 Heaps
    199 =====
    200 
    201   There is a single heap for dynamic allocation.  The following
    202   built-in procedures are provided:
    203  
    204   T* $new<T>(): creates an object A of type T in heap and returns &A.
    205 
    206   T* $alloc<T>(int n): creates an array A of length n of T in heap and
    207   returns &A[0].
    208 
    209   [Question: how to model C's malloc?   Must be able to execute it
    210   without knowing T.]
    211 
    212   void $free<T>(T* p): frees the object referred to by p, the
    213   pointer returned by an earlier call to $new or $alloc.
    214 
    215 
    216 Questions
    217   how to deal with "undefined" values?
    218  
    219   can there be nondeterministic expressions, i.e., expressions that
    220   evaluate to a set of values instead of one value?
    221 
    222   how to implement C's malloc?
     160}}}
     161where the `Ti` and `Uj` are types, the `xi` and `vj` are variables, and `expr` is an expression in which the only variables that can occur free are the `x1`,..., `xn`, `v1`,..., `vm`.  The initializer expressions `initj` are expressions using any variables in scope.  The expression has type `$fun<T1,...,Tn; V>`, where `V` is the type of `expr`.
     162
     163==== Semantics
     164
     165The 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.
     166
     167A 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.]
     168
     169== Heaps
     170
     171There is a single heap for dynamic allocation.  The following built-in procedures are provided:
     172
     173- `T* $new<T>()`: creates an object `A` of type `T` in heap and returns `&A`.
     174- `T* $alloc<T>(int n)`: creates an array `A` of length `n` of `T` in heap and returns `&A[0]`.
     175- `void $free<T>(T* p)`: frees the object referred to by `p`, the pointer returned by an earlier call to `$new` or `$alloc`.
     176
     177
     178== Questions
     179
     180* how to deal with "undefined" values?
     181* can there be nondeterministic expressions, i.e., expressions that evaluate to a set of values instead of one value?
     182* how to implement C's malloc?
     183
     184Ideas on malloc:
    223185
    224186Union of all types occurring in program:
     187{{{
    225188typedef union {
    226189  T1 t1;
    … …  
    228191  ...
    229192} BigUnion;
    230 
     193}}}
    231194
    232195A call to malloc returns a memory block:
    … …  
    236199    - offset (int)
    237200    - size (int)
    238     - value (type BigUnion)
     201    - value (type `BigUnion`)