[CakeML-dev] translating i2w

Michael.Norrish at data61.csiro.au Michael.Norrish at data61.csiro.au
Thu Dec 1 22:49:58 UTC 2016


Thanks for doing this Yong Kiam.  I had fixed the problems without pushing, so I’m sorry I caused duplicate work.

I think I will just change the WordT token to take a num: the value can never be negative (curiously, it seem as if SML requires ~0w3 to not parse/lex properly), and if we wanted to, we’d just lex it into two tokens rather than one.

Michael

From: Yong Kiam <tanyongkiam at gmail.com>
Date: Friday, 2 December 2016 at 03:55
To: Ramana Kumar <Ramana.Kumar at cl.cam.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] translating i2w

Changing it to use n2w should work. I don't think I have ran into i2w in translation before though.
Presumably, this is at a fixed word width so you will want to simplify word_2comp away.
BTW, are you fixing / have you fixed lexerProg? I could do it.
It's probably failing because of ARBs in toNum and num_from_hex_string, see: https://github.com/CakeML/cakeml/commit/4347e06c12533161d9311e761e4dbcdb1bd93810

On Thu, Dec 1, 2016 at 6:34 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk<mailto:Ramana.Kumar at cl.cam.ac.uk>> wrote:
I don't think you should translate i2w - can you make your code use
n2w instead? The translator should be able to handle n2w.
(I say this because looking at the translator's hol2deep function I
see it has a case for n2w but not for i2w.)

On 1 December 2016 at 21:44,  <Michael.Norrish at data61.csiro.au<mailto:Michael.Norrish at data61.csiro.au>> wrote:
> I’m breaking the build on my branch because the parser wants to turn word token integers into word64 values.  I used the i2w constant to do this, but the translator isn’t happy with word_2comp, which is used in this definition. Is there something obvious I should do to fix this?
>
> Or can I use n2w instead by altering the Word token constructor to take a num instead of an int?
>
> Michael
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org<mailto:Developers at cakeml.org>
> https://lists.cakeml.org/listinfo/developers

_______________________________________________
Developers mailing list
Developers at cakeml.org<mailto: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/20161201/7c0ba21d/attachment-0001.html>


More information about the Developers mailing list