[CakeML-dev] Basis library strings

[Scott Owens]

I’m looking at the String.compare function and wanting to add a String.< function, for mlstrings.

It appears that string_lt is defined in terms of string_lt for HOL strings at the end of the file, and some stuff is proved about it. However, the definition won’t lead to good code (if it is even translatable at all). It also doesn’t look like these theorems are used anywhere. Furthermore, it doesn’t like anything is proved about String.compare, other than side conditions for the translator.

Is all of the above true? If so, then I’d like get rid of the existing string_lt and instead define it in terms of compare, and try to prove some theorems about them.

At a higher level, I’m not sure who is working on the basis library, what its status is, and what future plans there are for it. I’m starting to need to use bits of it somewhat seriously, and finding that it isn’t really ready for that.

Scott