Handle constant integer expressions

[tchajed]

Go has an (unusual) feature of infinite-precision computation of constant integer expressions, which are formally considered untyped in the language. Goose does not support untyped constants (which would be modeled as having type Z), but it ought to support constant expressions correctly.

For example, (1 << 64 - 1) is a valid way of computing the largest uint64. This is currently translated to #1 << #64 - #1, which does the computation using u64; this happens to produce the right answer, but recently mit-plv/coqutil@2d7d3f9 changed this. We could work around this particular issue (since coqutil exposes customizing the shift behavior) but the principled fix is to translate to #(1 << 64 - 1) and do the computation in Z (with an overload for << to mean left-shift on mathematical integers). For other expressions there may be no way to define the operations on u64 so that the results are correct.

The translator needs to recognize constant expressions with a recursive pass to implement this, and then translate the constants and operations specially within, since the AST does not have a special node for constant expressions. An alternative might be to look for sub-expressions of type "untyped integer," which the type checker does expose sometimes, but for example I think in var x uint64 = 1 << 64 - 1 the type of 1 << 64 - 1 will be uint64.