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

Scott Owens S.A.Owens at kent.ac.uk
Tue Nov 29 11:08:49 UTC 2016


I still don’t think it’s that weird :) But Ramana’s suggestion is fine too.

Scott

> On 2016/11/29, at 03:32, michael.norrish at data61.csiro.au wrote:
> 
> What you just wrote sounds entirely weird.  In order to cope with word literals, things for which we already have constructors in the AST, we change the semantics of the language, forbidding certain definitional forms? If you’re up to modifying the semantics along these lines, then I suppose that’s possible, but it surely makes that semantics super-ugly. 
> 
> Ramana’s suggestion is better, and as he also said, my claim below is wrong about it being possible to mess it up.  So, for the moment, I’ll target the word64 literal constructor on my branch.
> 
> Michael
> 
> On 29/11/16, 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
> 
> 
> 



More information about the Developers mailing list