Changes between Version 65 and Version 66 of IR2

Timestamp:

05/03/21 22:23:51 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -221 +221 @@
   | expr '&&' expr  /* logical and */
   | expr '||' expr  /* logical or */
+  | expr '==>' expr  /* logical implication */
   | expr '==' expr  /* equality */
   | '!' expr  /* logical not */
   | expr '<' expr  /* less than */
   | expr '<=" expr  /* less than or equal to */
-  | expr '[' expr ']'  /* array or map read */
+  | expr '[' expr ']'  /* array access */
   | '(' expr ')'
   | '-' expr  /* negative */
@@ -234 +235 @@
   | '$exists' '(' decl expr? ')' expr  /* existential quantification */
   | expr '?' expr ':' expr  /* if-then-else expression */
+  | '$length' '(' expr ')'  /* length of array */
   ;
 expr-pair-list: expr-pair (',' expr-pair)* ;
@@ -285 +287 @@
 <T> $int $seq_length( $seq<T> a ); // length of a
 <T> T $seq_get( $seq<T> a, $int i ); // get element i of a
-<T> $seq<T> $seq_set( $seq<T> a, $int i, T x ); // seq obtained by replacing element `i` of `a` with `x`
-<T> $seq<T> $seq_subseq( $seq<T> a, $int start, $int stop ); // subsequence from `start` to `stop-1`
-<T> $seq<T> $seq_add( $seq<T> a, T x ); // sequence obtained by adding element `x` to the end of `a`
-<T> $seq<T> $seq_append( $seq<T> a1, $seq<T> a2 ); //  sequence obtained by concatenating `a1` and `a2`
-<T> $seq<T> $seq_remove( $seq<T> a, $int i ); // sequence obtained by removing element at position `i` from `a`
-<T> $seq<T> $seq_insert( $seq<T> a, $int i, T x ); // sequence obtained by inserting element `x` at position `i` in `a`
-<T> void $seq_write( $int n, T * ptr, $seq<T> a );  // write the first `n` elements of `a` to `ptr`, `ptr+1`, ..., `ptr+n-1`.
-<T> $seq<T> $seq_read( $int n, T * ptr ); // form a sequence by reading `ptr`, `ptr+1`, ..., `ptr+n-1`.
+<T> $seq<T> $seq_set( $seq<T> a, $int i, T x ); // seq obtained by replacing element i of a with x
+<T> $seq<T> $seq_subseq( $seq<T> a, $int start, $int stop ); // subsequence from start to stop-1
+<T> $seq<T> $seq_add( $seq<T> a, T x ); // sequence obtained by adding element x to the end of a
+<T> $seq<T> $seq_append( $seq<T> a1, $seq<T> a2 ); //  sequence obtained by concatenating a1 and a2
+<T> $seq<T> $seq_remove( $seq<T> a, $int i ); // sequence obtained by removing element at position i from a
+<T> $seq<T> $seq_insert( $seq<T> a, $int i, T x ); // sequence obtained by inserting element x at position i in a
+<T> void $seq_write( $int n, T * ptr, $seq<T> a );  // write the first n elements of a to ptr, ptr+1, ..., ptr+n-1
+<T> $seq<T> $seq_read( $int n, T * ptr ); // form a sequence by reading ptr, ptr+1, ..., ptr+n-1
 
 }}}