[CakeML-dev] Basis library strings

[Ramana Kumar]

On 26 Mar 2017 23:40, "Scott Owens" <S.A.Owens at kent.ac.uk> wrote:

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.


I would bet that at least one of string_lt or String.compare are used in
the Candle kernel. I'm all for you reworking things as long as you also fix
Candle if necessary.


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.


Currently I think nobody is working on it. The status is that various
modules and functions within them are defined and verified but there's
certainly more work to be done in cleaning some things up and adding more
functionality. It makes sense for some of that work to be done on an as
needed basis and it would be great to have your help.


Scott
_______________________________________________
Developers mailing list
Developers at cakeml.org
https://lists.cakeml.org/listinfo/developers
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170327/aa7b43b9/attachment.html>