On 19/09/2016 21:54, Makarius wrote:
On 16/09/16 14:24, David Matthews wrote:
The representation of strings has been simplified. Previously, single
character strings were represented by the character itself as a tagged
value. This was largely a relic of SML 90 which didn't have a separate
char type. That has been removed and all strings are now represented as
a vector of bytes. This speeds up string operations since the code no
longer has to consider the special case.
It should be actually easy for Isabelle/ML to cope with the new
representation of Poly/ML, using a table of pre-allocated singleton
strings. I have done something similar for the Isabelle/Scala version of
Symbol.explode, since the JVM is based on legacy UTF-16 widestring
representation.
I can do the same for the Isabelle/ML library, but there might be a
general benefit if basis/String.sml would do it uniformly in
charAsstring and thus in String.str etc.
Instead of creating a new singleton string each time, it would refer to
a vector of 256 pre-allocated values.
That seems a very good idea. I've implemented it.
Regards,
David
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
