<div dir="ltr"><div><div><div><div><div><div>I've just committed semantics for the primitives for strings/bytearrays, which you can see here:<br><a href="https://github.com/CakeML/cakeml/blob/strcat/semantics/semanticPrimitives.lem#L509">https://github.com/CakeML/cakeml/blob/strcat/semantics/semanticPrimitives.lem#L509</a><br><br></div>I'd really like to get these right before pushing them through, since it's quite a lot of work.<br></div>I have a few concerns currently:<br></div><br>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?<br></div><br></div>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.<br><br></div>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.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 20 March 2017 at 17:32, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Sounds good to me. One thing to note: the semantics should read all<br>
the values before writing them. This is so that we give the obviously<br>
correct semantics to copying inside the same array. The implementation<br>
will need to check whether it should do left-to-right or right-to-left<br>
copying so that the code doesn't accidentally read from what it just<br>
wrote.<br>
<br>
Also, as I pointed out in my other email, I think these memcpy<br>
primitives should also exist for normal value arrays.<br>
<br>
Cheers,<br>
Magnus<br>
<div><div class="h5"><br>
On 20 March 2017 at 06:29, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>
> I've been rethinking these primitives after the discussion at the last<br>
> hangout, and have come up with a different set altogether. Can you see a<br>
> simpler or more elegant approach to the one described below?<br>
><br>
> Here is the new approach I am considering:<br>
><br>
> 4 copying primitives in the source language going from string/bytearray to<br>
> string/bytearray.<br>
> The source comes with an offset and a length to copy.<br>
> If the destination is a string, a new string is created. If the destination<br>
> is a bytearray, it must be provided.<br>
><br>
> Concatenation (of lists of strings/arrays) and conversions between (whole)<br>
> strings and (whole) bytearrays can be implemented in the basis library in<br>
> terms of these primitives. And the primitives should be efficiently<br>
> implementable in terms of a byte-based memcpy primitive further down. (There<br>
> will need to be bounds checking in the source-level semantics (i.e.,<br>
> Subscript exception can be raised), and this will sometimes be unfortunate<br>
> (i.e., when obviously in bounds), but I don't think this is too costly.)<br>
><br>
> On 14 March 2017 at 16:52, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>
>><br>
>> Hi all,<br>
>><br>
>> I've started adding string/bytearray conversion and concatenation<br>
>> primitives (issues 244 and 245). Before getting too deep into updating<br>
>> the compiler etc., may I request a review of the semantics? Here they<br>
>> are:<br>
>><br>
>><br>
>> <a href="https://github.com/CakeML/cakeml/commit/67dd15bbd03f516be618ba72f1d56a2764209263" rel="noreferrer" target="_blank">https://github.com/CakeML/<wbr>cakeml/commit/<wbr>67dd15bbd03f516be618ba72f1d56a<wbr>2764209263</a><br>
>><br>
>> I noticed that v_to_char_list might be better as vs_to_char_list, to<br>
>> be run after v_to_list (rather than duplicating its<br>
>> list-deconstruction functionality). But I leave such refactoring for<br>
>> another time.<br>
>><br>
>> Cheers,<br>
>> Ramana<br>
><br>
><br>
><br>
</div></div>> ______________________________<wbr>_________________<br>
> Developers mailing list<br>
> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
><br>
</blockquote></div><br></div>