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
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Reply via email to