== CIVL IR ==

=== Language principles ===

* CIVL-IR is a subset of CIVL-C.  A CIVL-IR program is a CIVL-C program, and has the same semantics.

=== Grammar ===

{{{
program: typedef* decl* fundef+ ;
typedef:
    enum ID '{' idnetifier-list '}' ';'
  | struct ID '{' decl* '}' ';'
  | union ID '{' decl* '}' ';'
  | 'typedef' type-specifier declarator ';'
  ;
decl: qualifier? type-specifier declarator contract-clause* ';' ;
qualifier: '$input' | '$output' | '$abstract' | '$system' '<' STRING ',' STRING '>' ;
function-definition: '$atomic_f'? type-specifier declarator contract-clause* block ;
block: '{' typedef* decl* function-definition* statement* '}' ;
statement: block | simpleStmt | chooseStmt ;
simpleStmt: label? guard? primitiveStmt gotoStmt? ;
chooseStmt: label? '$choose' '{' simpleStmt* '}' ;
label: ID ':' ;
guard: '$when' '(' expr ')' ;  
gotoStmt: 'goto' ID ;
contract-clause :
    '$assigns' expr ';' 
  | '$requires' expr ';'
  | '$ensures' expr ';'
   ...
INT: ... /* integer constant */
ID: ... /* identifier */
STRING: ... /* string literal in double quotes */
}}}

=== Types ===
{{{
type-specifier:
    ID  /* typedef use */
  | '$int'  /* mathematical integers */
  | '$bool'  /* boolean type ($true and $false, unrelated to integers) */
  | '$char'  /* character type (Unicode characters, unrelated to integers) */
  | '$real'   /* mathematical reals */
  | '$float' '<' INT ',' INT '>'  /* IEEE floating-point numbers e=significand bits, f=exponent bits */
  | '$herbrand' '<' type-name '>'  /* Herbrand type of non-Herbrand numeric type T */
  | '$proc'  /* process type */
  | '$bundle'  /* bundle type for sequence of any type (same as seq<T>?) */
  | '$heap'  /* heap type, for dynamic allocation */
  | '$range'  /* regular sequence of integers */
  | '$domain'  /* tuple of ranges */
  | '$mem'  /* set of memory locations */
  | 'enum' ID  /* enumerated type */
  | 'struct' ID  /* structure type */
  | 'union' ID  /* union type */
  | 'void'   /* use as pointer element-type and return type of a function */
  | '$seq' '<' type-name '>'  /* sequence of T */
  | '$set' '<' type-name '>'  /* set of T */
  | '$map' '<' type-name ',' type-name '>'  /* partial function from T1 to T2 */
  | '$rel' '<' type-list '>'  /* relation: set of n-tuples with specified component types */
  ;
declarator: '*'* ID ('[' ']' | '(' type-list? ')')* ;
type-name: type-specifier '*'* ('[' ']' | '(' type-list? ')')* ;
type-list: type-name (',' type-name)* ;
complete-type-name: type-specifier '*'* ('[' expr ']' | '(' type-list? ')')* ;

}}}

Notes
* Sequences, sets, maps, and relations are immutable.   An assignment using objects of this type creates a new copy of the object, just as with primitive types like `int`.
* The main difference between the array type and the sequence type is that elements of an array are addressable, i.e., one can form a pointer such as `&a[i]`.  This is not possible with sequences, sets, maps, or relations---there is no way to have a pointer to any component of such a type.
* The difference between the function type and map type: a function is really a procedure in the language, so it can modify the state as well as return a value.    This is like the C notion of "function".   A map is a logical partial function: it is defined on some subset of the domain type, it will always "return" the same value on a given input, and reading it cannot modify the state.

Questions
* how to allocate an array
* how to initialize a variable (what are initial values?)
* how to go between sequences and arrays
* can you make types values? (reification)

=== Statements ===

{{{
primitiveStmt:
    ';'  /* noop */
  | lvalue '=' expr ';'  /* assignment */
  | expr '(' arg-list? ')' ';'  /* function call */
  | (lvalue '=')? '$spawn' expr '(' arg-list? ')' ';'  /* process creation */
  | 'return' expr? ';'  /* return from function call */
  | '$parspawn' expr ',' expr ',' expr ';'  /* parallel spawn */
  | (lvalue '=')? '$alloc' expr ',' expr ',' type-name ';'  /* heap allocation */
arg-list: expr (',' expr)* ;  /* actual argument list */

}}}

Notes
* For function calls and spawns, the first expression shall have type pointer-to-function-....  The function pointed to will be the one called or spawned.
* The 3 expressions in a `$parspawn` are (1) pointer to the first element of the process array, an expression of type `$proc*`, (2) an expression of type `$domain`, and (3) an expression of type pointer-to-function-....  The function must have the type that consumes n `$int`s, where n is the dimension of the domain, and returns `void`.   The function is spawned once for each element of the domain.  References to the new processes are stored in the process array.  
* The first expression following `$alloc` has type `$heap*`.  It is a pointer to the heap that will be modified by allocating the new memory.  The second expression has type `$int` and is the number of elements being allocated.    This is followed by the element type.    The function returns a pointer to the first element of an array, similar to C's malloc.    It is deallocated using function`$free`.

Built-in functions:
{{{
void $assert( $bool asserted_expr, ... );  /* assertion with optional error message */
void $assume( $bool expr );  /* assumption */
void $wait( $proc p );  /* wait until p terminates */
void $waitall( $int nprocs, $proc * procs );  /* wait for all procs in list to terminate */
void $free( void * ptr );  /* frees something that was $alloc-ed */

}}}

=== Expressions ===

{{{
  expr:

}}}