[CakeML-dev] translating i2w

Yong Kiam tanyongkiam at gmail.com
Thu Dec 1 23:32:00 UTC 2016


Oh oops sorry, I must have been confused. I guess we might have been
talking about the stuff at the bottom of lexer_impl, e.g. lex_impl_all

On Thu, Dec 1, 2016 at 6:19 PM, <Michael.Norrish at data61.csiro.au> wrote:

> Really?  I don’t understand quite how the lexerProg assembles the lexer
> implementation, but it looks as if it translates lexer_fun, which calls
> next_token, and next_token calls next_sym.  It’s next_sym that has problems
> with sideconditions, and if you look at how next_token is translated, you
> can see how the call to next_sym is replaced by a call to next_sym_alt (by
> rewriting with the equivalence theorem).
>
>
>
> And git history disagrees with you about having touched lexer_impl btw J
>
>
>
> Michael
>
>
>
> *From: *Yong Kiam <tanyongkiam at gmail.com>
> *Date: *Friday, 2 December 2016 at 10:00
> *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] translating i2w
>
>
>
> Hi Michael,
>
> One thing that came up when a few of us were looking through the bootstrap
> just now was the difference between lexer_fun and lexer_impl. The
> translation currently just translates lexer_fun and doesn't seem to be
> touching lexer_impl at all. Is it still needed or is it meant to be
> faster/nicer?
>
> Also, I didn't update lexer_impl when I fixed the translation.
>
>
>
> On Thu, Dec 1, 2016 at 5:49 PM, <Michael.Norrish at data61.csiro.au> wrote:
>
> 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>
> 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
>
>
>
>
> _______________________________________________
> 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/c13d1a8a/attachment.html>


More information about the Developers mailing list