[CakeML-dev] translating i2w

[Yong Kiam]

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>
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> 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
> > 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/20161201/693766f5/attachment.html>