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

Scott Owens S.A.Owens at kent.ac.uk
Mon Nov 28 23:11:26 UTC 2016


Sorry, decimal, not octal.

Scott

> On 2016/11/28, at 23:02, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> 
> That’s what I thought at first, but then Michael’s comment doesn’t really apply to it. There’s always the SML character literal octal notation #”\080” if we want to identify strings and word8 vectors...
> 
> Scott
> 
>> On 2016/11/28, at 22: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
>> 
> 
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers



More information about the Developers mailing list