Section 1.6 and 1.7 of Programming in Cryptol Textbook - Edits

[manleykm]

There are a few errors in sections 1.6: Floating Point Numbers and 1.7: Tuples of the Programming in Cryptol textbook.

The first two, in section 1.6, were just minor typos:

Floating point numbers may be written using either integral or fractioanl literals. In general, literals that cannot be represented exactly are rejected with a type error, with the exception of decimal fractional litrals which are rounded to the nearest even representable numbers.

(emphasis added)

The last error was in Exercise 1.7, of section 1.7.

The textbook says that the answers to the last two problems should be as follows:

However, this results in the error message

Cryptol> ((1, 2), False, (3-1, (4, True))).2.1

Parse error at <interactive>:1:35,
  unexpected: 2.1

Extra parentheses are needed in order to make these projections run without errors.

Cryptol> (((1, 2), False, (3-1, (4, True))).2).1
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of 0th tuple field
(4, True)

and

Cryptol> ((((1, 2), (2, 6, (True, 4)), False).1).2).0
True

respectively.

[weaversa]

Even leaving spaces works. I wonder if this is due to added parsing of floating point numbers?

Cryptol> ((1, 2), False, (3-1, (4, True))).2 .1
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of 0th tuple field
(4, True)

[manleykm]

In section 1.8, I have another instance where Cryptol 2.9.0 gives a different result than what the book states. In exercise 1.14, the book's solution states that

Cryptol> [0 .. 9] @@ []
[]

This is the result from Cryptol 2.8, but in 2.9, the following error occurs:

Cryptol> [0 .. 9] @@ []
Cannot evaluate polymorphic value.
Type: {a, b} (Integral a, Literal 9 b) => [0]b

[weaversa]

Cryptol> []

Cannot evaluate polymorphic value.
Type: {a} [0]a

[yav]

Thanks for pointing these out, I think both of these warrant some changes to Cryptol, so I made separate tickets to track what we decide to do.

[manleykm]

A (potentially?) interesting note:

For records, it works fine to write:
{name = "test", coords = {xCoord = 3:[32], yCoord = 5:[32]}}.coords.xCoord
which gives a result of 3, without needing any extra parentheses or anything.

Meanwhile, ("test", (3, 5)).1.0 needs to be written (("test", (3, 5)).1).0 in order to give the same result.

[yav]

I am going to close this, as we are tracking the issues in #876 and #877