[CakeML-dev] [CakeML-Dev] targeting word literal constructors in AST

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Mon Nov 28 23:02:15 UTC 2016


I think I'd be happy saying that portable code should use the fromInt
functions.

On 29 November 2016 at 10:01, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> (Minor correction, it was ``WordFromInt W8`` rather than ``W8FromInt``.)
>
> Another more straightforward suggestion is concrete syntax directly
> corresponding to the AST literals, e.g.:
> 8w3 -> Word8 0w3
> 64w3 -> Word64 0w3
> The problem here is that it's not SML compatible. However, we could
> additionally have 0w3 mapping to the 64-bit version.
>
> On 29 November 2016 at 09:57, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
>
>> Good point, Michael. I didn't think about the problem of redefining
>> int_to_word or Word8.fromInt - that makes targeting them in the parser seem
>> less appealing to me. (However, note that my suggestion did not involve
>> targeting Word8.fromInt from the parser.)
>>
>> Scott: my suggestion was to parse "0w3" as ``Word64 0w3`` and not have
>> special Word8 literals. To write programs with word8s, you must use
>> Word8.fromInt from the basis library (which maps to the primitive
>> ``W8FromInt``).
>>
>> On 29 November 2016 at 09:41, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>>
>>> I don’t think my suggestion is that weird. The semantics of the language
>>> would change so that int_to_word as a name has a special, explicitly
>>> documented meaning. You could require that any definition of int_to_word
>>> has to have type int -> WordN.t for some N IN {8, 32, 64} or something like
>>> that, to catch the error at a better location. I didn’t really understand
>>> Ramana’s suggestion.
>>>
>>> Scott
>>>
>>> > On 2016/11/28, at 22:24, Michael.Norrish at data61.csiro.au wrote:
>>> >
>>> > The other idea I had, which would at least allow the parser to target
>>> the AST (suggestions below would suggest we drop one or both of the
>>> Word{8,64} constructors), was to have 0w3 go to Word8, and 0W3 go to Word64…
>>> >
>>> > Scott’s suggestion is pretty weird incidentally, it would mean that
>>> inserting
>>> >
>>> >   fun int_to_word x = x
>>> >
>>> > in a program that doesn’t contain that string anywhere could cause it
>>> to fail to typecheck.  I mildly prefer Ramana’s because to get the
>>> comparable problem there, you’d have to insert the slightly more involved
>>> >
>>> >   structure Word8 = struct fun fromInt i = I end;
>>> >
>>> > which would break pieces of code with no textually apparent references
>>> to Word8.
>>> >
>>> > Michael
>>> >
>>> > From: Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
>>> > Date: Monday, 28 November 2016 at 20:29
>>> > To: Scott Owens <S.A.Owens at kent.ac.uk>
>>> > Cc: "Norrish, Michael (Data61, Canberra City)" <
>>> Michael.Norrish at data61.csiro.au>, "developers at cakeml.org" <
>>> developers at cakeml.org>
>>> > Subject: Re: [CakeML-dev] [CakeML-Dev] targeting word literal
>>> constructors in AST
>>> >
>>> > I like Scott's suggestion.
>>> >
>>> > On 28 November 2016 at 20:23, Scott Owens <S.A.Owens at kent.ac.uk>
>>> wrote:
>>> > Or we could have the parser map 0w3 to something like “int_to_word 3”
>>> and leave it in the programmers control, and have the basis start with a
>>> default.
>>> >
>>> > Scott
>>> >
>>> > > On 2016/11/28, at 07:36, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
>>> wrote:
>>> > >
>>> > > I doubt we want to go down that path...
>>> > >
>>> > > Here's a (somewhat random) suggestion: word literals (0w3 etc.) are
>>> mapped to Word64.word, and to get bytes via parser you need to use
>>> Word8.fromInt.
>>> > >
>>> > > On 28 November 2016 at 15:35, <Michael.Norrish at data61.csiro.au>
>>> wrote:
>>> > > Presumably SML allows type inference to figure out the width in the
>>> same way that numeric operations get overload-resolved:
>>> > >
>>> > >
>>> > >
>>> > > (* Poly/ML *)
>>> > >
>>> > > > Word8.+(0w3, 0w4);
>>> > >
>>> > > val it = 0wx7: Word8.word
>>> > >
>>> > > > Word64.+(0w3, 0w4);
>>> > >
>>> > > val it = 0wx7: Word64.word
>>> > >
>>> > >
>>> > >
>>> > > Michael
>>> > >
>>> > >
>>> > >
>>> > > From: Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
>>> > > Date: Monday, 28 November 2016 at 11:46
>>> > > To: "Norrish, Michael (Data61, Canberra City)" <
>>> Michael.Norrish at data61.csiro.au>
>>> > > Cc: "developers at cakeml.org" <developers at cakeml.org>
>>> > > Subject: Re: [CakeML-Dev] targeting word literal constructors in AST
>>> > >
>>> > >
>>> > >
>>> > > SML does not distinguish syntactically. I guess we might have to
>>> invent some syntax...?
>>> > >
>>> > >
>>> > >
>>> > > On 28 November 2016 at 11:03, <Michael.Norrish at data61.csiro.au>
>>> wrote:
>>> > >
>>> > > There are both Word8 and Word64 constructors for word literals in
>>> the AST type. How are the parser or lexer meant to figure out which any
>>> piece of syntax corresponds to?
>>> > >
>>> > > Michael
>>> > >
>>> > > _______________________________________________
>>> > > Developers mailing list
>>> > > Developers at cakeml.org
>>> > > https://lists.cakeml.org/listinfo/developers
>>> > >
>>> > >
>>> > >
>>> > >
>>> > > _______________________________________________
>>> > > Developers mailing list
>>> > > Developers at cakeml.org
>>> > > https://lists.cakeml.org/listinfo/developers
>>> > >
>>> > >
>>> > > _______________________________________________
>>> > > Developers mailing list
>>> > > Developers at cakeml.org
>>> > > https://lists.cakeml.org/listinfo/developers
>>> >
>>> >
>>> > _______________________________________________
>>> > Developers mailing list
>>> > Developers at cakeml.org
>>> > https://lists.cakeml.org/listinfo/developers
>>>
>>> _______________________________________________
>>> 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/20161129/955b7414/attachment-0001.html>


More information about the Developers mailing list