Interaction between fractional literals and projections

[yav]

In #875 points out that \x -> x.2.1 gives a parse error "unexpected 2.1" while previously it used to be two projections.

This is because the projection operator . is currently treated as its own operator, so the tokens for the body of the lambda are x, ., and 2.1`.

One way to fix this would be to say that we don't allow space after the . for a selector, so essentially a selector is its own token, like .2 for example. With this interpretation the tokens would be x, .2 and .2 and we'd get the old behavior.

[robdockins]

Humm... yeah that's annoying. I guess languages like JavaScript handle this by making field projections be identifiers.

I think it would be OK to disallow space after the . for projections. My only concern would be if people want to write long projection chains and put them on separate lines. Maybe it's OK if we allow this sort of thing:

someBigRecord
  .field1
  .field3
  .3.5.2
  .field20

[brianhuffman]

If we're going to reimplement the lexing and parsing rules for tuple projections, we might as well take care of #713 at the same time. Instead of allowing any numeric literal to be used as a tuple projection, we should allow only a list of decimal digits.

[brianhuffman]

Something that might complicate this change a bit is that the record update syntax allows tuple selectors to appear without a preceding dot:

Cryptol> let x = (True, False)
Cryptol> { x | 1 = True }
(True, True)

[yav]

That's a good point. I think we could get this to work with a bit of hackery in the parser though. Alternatively, we could go with the more consistent but uglier version where selectors always have dots at the front...

[brianhuffman]

I should have suggested a nested tuple update like this:

Cryptol> let x = (True, (False, False))
Cryptol> { x | 1.0 = True }
(True, (True, False))

(This works in the current version only if you put a space before or after the dot in 1.0.)

[yav]

This is the hackery I was referring to. A sequence like 1.2.3.4 would be tokenized as FRACTION, SELECTOR, SELECTOR. The hack would be that when we see a FRACTION at the root of a chain of selectors in an update field, we'd interpret it as two selectors instead of a fraction. Certainly a bit of a hack but I think it'd work, if we decided that this is the notation we want.

Let's discuss this in person during the ticket review tomorrow.