Improvements of new memory.

* Make types more C-ish, by disallowing arrays, structs and unions of size 0.
* Remove sizes for arrays values.
* Only require the size of base types to be positive, we can prove it for
  other types.
* Nicer notations for C-types.
* Start on implementing unary/binary operations and casts.