[CakeML-dev] strings

[Ramana Kumar]

Hi Magnus et al,

I am struggling with some aspects of the design of the new string
representation (as packed byte arrays, rather than the current blocks
with 1 char per word). The plan I am following (on the strings branch)
is that closLang has a new ByteVector value, and these are compiled to
ByteArray in BVL.

In particular, I want to ask about equality. As discussed, we must be
able to distinguish ByteArrays that are compared by pointer from
ByteArrays that must be compared by contents. The question is: Do I
need to modify data_to_word's equality stub code to follow every
RefPtr to check something in the header word indicating whether it's a
compare-by-contents reference, or should I put that information into
the pointer itself?

If it should be visible in the pointer itself (without following it),
then I think I'll need some help figuring out what the pointer
representation actually is and where things can be encoded in it. For
example, could there be some way to use ptr_bits for these
compare-by-contents ByteArrays that won't get them confused with
Blocks?

If we are using the pointer, then I think it's RefPtr that should get
an extra flag, not ByteArray, in BVL.

If we are not using the pointer, then I'd love to know if there are
any hints or comments for deciphering what Equal_code in data_to_word
is doing. (Surely there must be a better approach than painstakingly
reading the code/proof..? Wasn't there any pseudocode at some point?)

Cheers,
Ramana