== 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: type-qualifier? type-specifier declarator ';' ;
type-qualifier: '$input' | '$output' ;
type-specifier:
    ID
  | '$int'
  | '$bool'
  | '$char'
  | '$int'
  | '$real'
  | '$float' '<' INT ',' INT '>'
  | '$herbrand' '<' type-name '>'
  | '$proc'
  | '$bundle'
  | '$heap'
  | '$range'
  | '$domain'
  | '$mem'
  | 'enum' ID
  | 'struct' ID
  | 'union' ID
  | 'void'
  | '$seq' '<' type-name '>'
  | '$set' '<' type-name '>'
  | '$map' '<' type-name ',' type-name '>'
  | '$rel' '<' type-list '>'
  ;
declarator: '*'* ID ('[' ']' | '(' type-list? ')')* ;
type-name: type-specifier '*'* ('[' ']' | '(' type-list? ')')* ;
type-list: type-name (',' type-name)* ;
complete-type-name: type-specifier '*'* ('[' expr ']' | '(' type-list? ')')* ;
fundef: type-specifier declarator block ;  
block: '{' typedef* vardecl* fundef* statement* '}' ;
statement: block | simpleStmt | chooseStmt ;
simpleStmt: label? guard? primitiveStmt gotoStmt? ;
chooseStmt: label? '$choose' '{' simpleStmt* '}' ;
label: ID ':' ;
guard: '$when' '(' expr ')' ;  
gotoStmt: 'goto' ID ;
expr:
simpleStmt:
INT /* integer constant */
ID /* identifier */
conclause : 'assigns' expr ';' 
          | 'requires' expr ';'
          | 'ensures' expr ';'
          ...
}}}


=== Types ===
* `$bool` : boolean type ($true and $false, unrelated to integers)
* `$char` : character type (Unicode characters, unrelated to integers)
* `$int` : mathematical integers
* `$real` : mathematical reals
* `$float<e,f>` : IEEE floating-point numbers e=significand bits, f=exponent bits
* `$herbrand<T>` : 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 tag` : enumerated type
* `struct tag` : structured type, can also be used for "tuples"
* `union tag` : union type
* `T[]` : array of T
* `void *` : pointer to anything
* `T *` : pointer to T
* `T(T1, ..., Tn)` : function (aka procedure) consuming T1, ..., Tn and returning T
* `$seq<T>` : sequence of T
* `$set<T>` : set of T
* `$map<T1,T2>` : map from T1 to T2
* `$rel<T1, ..., Tn>` : relation,  set of n-tuples

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)