Changes between Version 5 and Version 6 of PIL

Timestamp:

10/04/24 09:47:23 (20 months ago)

Author:

siegel

Comment:

--

PIL

@@ -132 +132 @@
 - `($set<T>)$empty`   // empty set of type T
 - `$logic _Bool $set_in(T x, $set<T> s);`  // is x an element of s?
-- `$pure $set<T> $set_with($set<T> s, T x);` // s U {x}
-- `$pure $set<T> $set_without($set<T> s, T x);` // s - {x}
-- `$pure $set<T> $set_union($set<T> s1, $set<T> s2);` // s1 U s2 
-- `$pure $set<T> $set_difference($set<T> s1, $set<T> s2);` // s1-s2 
-- `$pure $set_intersection($set<T> s1, $set<T> s2);` // s1 \cap s2
-- `$pure T[] $set_elements($set<T> s);`
-- `$pure _Bool $set_isSubsetOf($set<T> s1, $set<T> s2);`
-- `$pure $set<U> $set_map($set<T> s, $fun<T,U> f);`
+- `$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);`
 
 Mutating procedures:
@@ -156 +156 @@
 
 Logic functions:
-- `$pure T[] $seq_fun($int len, $fun<$int,T> f);`
-- `$pure T[] $seq_uniform($int n, T val);`
-- `$pure $int $length(T[] a);` // length of a
-- `$pure T[] $seq_write(T[] a, int i, T x);`  // a[i:=x]
-- `$pure T[] $seq_subseq(T[] a, int i, int n);`  // a[i..i+n-1]
-- `$pure T[] $seq_without(T[] a, int i);` // a with position i removed
-- `$pure T[] $seq_with(T[] a, int i, T x);`
-- `$pure T[] $seq_concat(T[] a1, T[] a2);`
-- `$pure U[] $seq_map(T[] a, $fun<T,U> f);`
-- `$pure T[] $seq_filter(T[] a, $fun<T,_Bool> f);`
-- `$pure U $seq_foldl(T[] a, $fun<$tuple<T,U>,U> f, U init);`
-- `$pure U $seq_foldr(T[] a, $fun<$tuple<T,U>,U> f, U init); `
+- `$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); `
 
 Mutating expressions:
@@ -182 +182 @@
 - `m1 == m2`
 - `($map<K,V>)$empty`
-- `$pure V $map_get($map<K,V> K key);`
-- `$pure _Bool $map_containsKey($map<K,V> map, K key);`
-- `$pure _Bool $map_containsValue($map<K,V> map, V val);`
-- `$pure $map<K,V> $map_with($map<K,V> map, K key, V val);`
-- `$pure $map<K,V> $map_without($map<K,V> map, K key);`
-- `$pure $set<K> $map_keys($map<K,V> map);`
-- `$pure $set<$tuple<K,V>> $map_entries($map<K,V> map);`
+- `$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 $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);`
+- `$logic $set<K> $map_keys($map<K,V> map);`
+- `$logic $set<$tuple<K,V>> $map_entries($map<K,V> map);`
 
 Mutating procedures: