[CakeML-dev] translating i2w

[Magnus Myreen]

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)))`,
>   rw[]
>   >-
>     (simp[Once (GSYM integerTheory.INT_ABS_NEG)]>>
>     `0 ≤ (-i)` by intLib.COOPER_TAC>>
>     metis_tac[integerTheory.INT_ABS_EQ_ID])
>   >>
>     `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
> wordsLib.WORD_EVAL_CONV)
>
> The i2w becomes something like this:
>
> (if i < 0 then
>   n2w
>     (18446744073709551616 −
>      if
>        Num (ABS i) < 18446744073709551616
>      then
>        Num (ABS i)
>      else
>        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
>> 1e761e4dbcdb1bd93810
>>
>> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161202/6740ef71/attachment.html>