Variable width char

[brianhuffman]

This PR removes the constraint that character literals (and strings) have type [8]; instead, they are treated exactly like decimal literals, and have a polymorphic type. See #863.

[jpziegler]

Consider making the built-in Char type variable-size.

cryptol/lib/Cryptol.cry

Line 63 in eed0bde

type Char = [8]

I'm guessing this might break a few more things, though.

[jpziegler]

Or we could leave Char defined as [8] and just let people redefine it if they want wider characters.

[jpziegler]

Printing strings is only working for monomorphic 8-bit strings.

Cryptol> :s ascii=on
Cryptol> "abc"
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'rep' of 'Cryptol::number'
[97, 98, 99]
Cryptol> "abc":[3][8]
"abc"
Cryptol> "abc":[3][16]
[0x0061, 0x0062, 0x0063]

[weaversa]

‘Char’ is pretty reminiscent of the C type, which is (mostly) just 8-bits. I suggest it stays 8-bits.

[brianhuffman]

As for string printing, we'll have to decide what we want. When :ascii=on, do you think it's desirable to print all values of type [n]Integer as strings? Maybe just [n][8], [n][7], [n][16], and [n][32], and no other types? Or should we have a heuristic that checks to see whether a list of numbers contains only printable unicode codepoints, and print it as a string only if it is? Maybe some combination of these rules?

Or maybe we could have a few different settings for the :ascii flag besides just on and off? I could imagine setting :ascii = 8 to make cryptol print lists of [8] as strings, and :ascii = 7 to print lists of [7] as strings, etc.

[jpziegler]

I like that last idea.

I suppose if we're going to support printing of bit-sizes greater than 8, we probably shouldn't call this ascii. Perhaps :utf? Or :char? Could keep :ascii around as-is and have :utf=8 do the same thing (and even set :ascii=on as a side effect.)

We could allow users to set :utf=any if they have multiple different types of strings.

Maybe:

Cryptol> :utf=off
Cryptol> :utf=8
Cryptol> :utf=32
Cryptol> :utf=64
Error! :utf must be an integer less than or equal to 32, off, or any.
Cryptol> :utf=any

[yav]

Just to be clear, this does not implement variables width characters (e.g., as in UTF-8) but rather overloaded characters, correct? If so, I think using utf in the settings would be confusing.

I don't have an opinion on what we should do here, but if we merge this version we should remember to update the book also, as it likely has examples involving characters.

[brianhuffman]

I think :set char or :set char-width would be a better name than :set utf for configuring the pretty printing of string values.

[jpziegler]

Here's the Gold-Bug example that @WeeknightMVP and I were playing with. Loads fine with this PR.

[robdockins]

Have we achieved consensus on what to do about this? I got the impression we had decided this generalization was broadly something we wanted to do, and the only remaining questions were about the UI aspects of controlling the pretty-printing. Is that correct?