[CakeML-dev] translating i2w
magnus.myreen at gmail.com
Thu Dec 1 22:30:39 UTC 2016
I'll look into adding i2w support to the translator. -- Magnus
On 2 December 2016 at 07:39, Yong Kiam <tanyongkiam at gmail.com> wrote:
> You can force the i2w to go through using this if changing the parser to
> use n2w is not possible:
> val elit_rw = Q.prove(`
> (i < 0 ⇒ -n2w (Num (-i)) = -n2w (Num (ABS i))) ∧
> (¬(i < 0) ⇒ n2w (Num i) = n2w (Num (ABS i)))`,
> (simp[Once (GSYM integerTheory.INT_ABS_NEG)]>>
> `0 ≤ (-i)` by intLib.COOPER_TAC>>
> `0 ≤ i` by intLib.COOPER_TAC>>
> fs[GSYM integerTheory.INT_ABS_EQ_ID]);
> val _ = translate (def_of_const ``ptree_Eliteral`` |> SIMP_RULE
> std_ss[integer_wordTheory.i2w_def,elit_rw,word_2comp_def] |> CONV_RULE
> The i2w becomes something like this:
> (if i < 0 then
> (18446744073709551616 −
> Num (ABS i) < 18446744073709551616
> Num (ABS i)
> Num (ABS i) MOD 18446744073709551616)
> else n2w (Num (ABS i)))
> (there are special rewrites for Num(ABS i) in the translator)
> On Thu, Dec 1, 2016 at 11:55 AM, Yong Kiam <tanyongkiam at gmail.com> wrote:
>> 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/4347e06c12533161d931
>> On Thu, Dec 1, 2016 at 6:34 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
>>> 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
> Developers mailing list
> Developers at cakeml.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Developers