The CIVL-IR language.  A program in this language is also known as a "CIVL model".

Properties of the language:

* the language (and grammar) are subsets of CIVL-C
* a CIVL-IR program represents a guarded-transition system explicitly
* as in CIVL-C, there are functions, scopes, and functions can be defined in any scope
* all blocks (including a function body) consist of the following elements, in order:
 * a sequence of variable declarations with no initializers
 * a sequence of function definitions
 * a sequence of labeled `$choose` statements.   Each clause in the choose statement is a `$when` statement with some guard and a primitive statement, followed by a `goto` statement
* an array is declared without any length expression.  When it is initialized it can specify length.

Example:

{{{
$integer f() {
  $real x;
  $real y;
  $float(16,23) z;
 
L1 :
  $choose {
    $when (g1) stmt1; goto L2;
    $when (g2) stmt2; goto L3;
  }

  { // begin new scope
    $real x;

L2 :
    $choose {
      $when (g3) stmt3; goto L4;
      ...
    }
  } // end new scope
...
}
// etc.
}}}

==  Static Types ==

* `$bool` : boolean type, values are `$true` and `$false`
* `$proc` : process type
* `$scope` : scope type
* `$char` : character type.  Alternatively, get rid of this and just use an integer type.
* `$mem` : type representing set of memory units
* `$bundle` : type representing some un-typed chunk of data
* `$heap` : heap type
* `$range` : ordered set of integers
* `$domain` : ordered set of tuples of integers
 * `$domain(n)`, n is an integer at least 1; subtype of above in which all tuples have arity n.
* `enum` types.
 * **different from integers or like C?**
* `$integer` : the mathematical integers
* `$int(lo,hi,wrap)`
 * lo, hi are integers, wrap is boolean
 * finite interval of integers [lo,hi].  If `wrap` is true then all operations "wrap", otherwise, any operation resulting in a value outside of the interval results in an exception being thrown.
* `$hint` : Herbrand integers.  Values are unsimplified symbolic expressions.
* `$real` : the mathematical real numbers
* `$float(e,f)`, e, f are integers, each at least 1
 * IEEE754 floating point numbers
* `$hreal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
* `struct(T1,...,Tn)`
 * structure type with named fields.  Names may not seem necessary but if you want a subset of CIVL-C...
 * What about bit-widths?
* `union(T1,...,Tn)` : similar to struct
* `T[]` : array-of-T
* Function<S1,...,Sn;T>
 * function consuming S1,...,Sn and returning T.  T can be void.  The actual notation is the horrible C notation.
* `void*` : all pointers
 * `T*` : pointer-to-T, subtype of above

When are two types equal?

What are two types compatible?


== Expressions ==

* literals
 * `$true`, `$false` : values of type `$bool`
 * 123, -123, 3.1415, etc. : values of type `$integer`, `$int`, `$real`, `$float`
  * what particular notations for floating values?
 * 'a', 'b', ... UNICODE?
 * `(T[]){e0, e1, ...}` : values of type `T[]`
 * `(S){e0, ...}` : values of type `S` (struct literal)
 * `e1..e2`, `e1..e2#e3` : values of type `$range`
 * `($domain){r1,...,rn}` : value of type `$domain(n)`
 * `"abc"` : string literals: value of type `$char[]`
 * `$root`, `$here` : values of type `$scope`
 * `$self`, `$proc_null` : values of type `$proc`
 * `NULL` : value of type `void*`
* variables
* `$defined(e1)`
* `e1+e2` : addition
* `e1-e2` : subtraction
* `e1*e2` : multiplication
* `e1/e2` : division
* `e1%e2` : modulus
* `e1[e2]` : array index
* `*e` : pointer dereference
* `&e` : address-of
* `!e` : logical not
* `-e` : negative
* `(T)e` : cast expression
 * cast of integer to array-of-boolean, and vice-versa?
* `e1==e2`, `e1!=e2`
* `e1&&e2`, `e1||e2`
* `e1?e2:e3`
* `e1<e2`, `e1<=e2`
* `e0(e1,...,en)` : pure function call?
* `$forall`, `$exists`
* `e1.i`, some natural number i (tuple read)
* `$initial_value(T; e1,...,en)`
 * e1,...,en are expressions of integer type
 * the type of this expression is T[e1]...[en]
 * array value with base type `T` and length e1,...,en
* `$typeof(...)`: what is this for?
* `$sizeof(T)` : T is a type name?
* `e1&e2`, `e1|e2`, `e1^e2`, `~e1` : bit-wise operations: arguments are arrays of booleans


== Statements ==

* Assign
* Call
 * regular function (one with flow graph)
 * system function?
 * abstract function?
 * pure functions?
* Spawn
* Wait
* Wailtall?
* Malloc
* Free
* Noop
* Return
* Atomic_enter
* Atomic_exit
* Parfor_spawn.  is there exit?
* For_dom_enter (for domains).  exit?



== Program Graph ==

== Model ==

== Semantics ==

Semantics issues

* define every possible cast
* define every possible +, etc.
* define every kind of pointer value and casts between pointer types
* casts between pointer and integer types?

=== Values ===



=== Transitions ===



== Libraries ==