[CakeML-dev] New string/bytearray operations

[Ramana Kumar]

I've just committed semantics for the primitives for strings/bytearrays,
which you can see here:
https://github.com/CakeML/cakeml/blob/strcat/semantics/semanticPrimitives.lem#L509

I'd really like to get these right before pushing them through, since it's
quite a lot of work.
I have a few concerns currently:

1. It's not obvious that the bounds checking can be done efficiently. The
BoundsCheckByte primitive doesn't work neatly with checking whether an
offset+length pair is correct, so I'd have to do some special casing, e.g.,
when the length = 0. Should we have a different semantics which allows
negative or too long lengths and does something reasonable with them? Or
could there be another efficient operation like BoundsCheckByte for
checking an offset+length?

2. It takes work to add new primitives (update type system, inferencer, all
backend do_app proofs..), and these 4 are reasonably complicated despite
being quite similar to each other. Could we get away with a smaller or
simpler set? E.g., maybe we only really need CopyAw8Aw8 but give it a
flexible semantics taking either bytearrays or strings? I don't know if
that can work though.

If we add similar primitives for polymorphic arrays and vectors, it would
be good to factor out as much commonality as possible in the semantics...
Sadly it looks like a lot of copy-paste-tweaking is inevitable... I'd
rather only add the polymorphic ones after the byte ones are done, just to
avoid too much explosion of work.

On 20 March 2017 at 17:32, Magnus Myreen <magnus.myreen at gmail.com> wrote:

> Sounds good to me. One thing to note: the semantics should read all
> the values before writing them. This is so that we give the obviously
> correct semantics to copying inside the same array. The implementation
> will need to check whether it should do left-to-right or right-to-left
> copying so that the code doesn't accidentally read from what it just
> wrote.
>
> Also, as I pointed out in my other email, I think these memcpy
> primitives should also exist for normal value arrays.
>
> Cheers,
> Magnus
>
> On 20 March 2017 at 06:29, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> > I've been rethinking these primitives after the discussion at the last
> > hangout, and have come up with a different set altogether. Can you see a
> > simpler or more elegant approach to the one described below?
> >
> > Here is the new approach I am considering:
> >
> > 4 copying primitives in the source language going from string/bytearray
> to
> > string/bytearray.
> > The source comes with an offset and a length to copy.
> > If the destination is a string, a new string is created. If the
> destination
> > is a bytearray, it must be provided.
> >
> > Concatenation (of lists of strings/arrays) and conversions between
> (whole)
> > strings and (whole) bytearrays can be implemented in the basis library in
> > terms of these primitives. And the primitives should be efficiently
> > implementable in terms of a byte-based memcpy primitive further down.
> (There
> > will need to be bounds checking in the source-level semantics (i.e.,
> > Subscript exception can be raised), and this will sometimes be
> unfortunate
> > (i.e., when obviously in bounds), but I don't think this is too costly.)
> >
> > On 14 March 2017 at 16:52, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
> >>
> >> Hi all,
> >>
> >> I've started adding string/bytearray conversion and concatenation
> >> primitives (issues 244 and 245). Before getting too deep into updating
> >> the compiler etc., may I request a review of the semantics? Here they
> >> are:
> >>
> >>
> >> https://github.com/CakeML/cakeml/commit/67dd15bbd03f516be618ba72f1d56a
> 2764209263
> >>
> >> I noticed that v_to_char_list might be better as vs_to_char_list, to
> >> be run after v_to_list (rather than duplicating its
> >> list-deconstruction functionality). But I leave such refactoring for
> >> another time.
> >>
> >> Cheers,
> >> Ramana
> >
> >
> >
> > _______________________________________________
> > 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/20170320/848db805/attachment.html>