[CakeML-dev] translating i2w

[Yong Kiam]

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/
> 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/0215ae09/attachment.html>