<div dir="ltr">I'll look into adding i2w support to the translator. -- Magnus</div><div class="gmail_extra"><br><div class="gmail_quote">On 2 December 2016 at 07:39, Yong Kiam <span dir="ltr"><<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>You can force the i2w to go through using this if changing the parser to use n2w is not possible:<br><br>val elit_rw = Q.prove(`<br>  (i < 0 ⇒ -n2w (Num (-i)) = -n2w (Num (ABS i))) ∧<br>  (¬(i < 0) ⇒ n2w (Num i) = n2w (Num (ABS i)))`,<br>  rw[]<br>  >-<br>    (simp[Once (GSYM integerTheory.INT_ABS_NEG)]>><br>    `0 ≤ (-i)` by intLib.COOPER_TAC>><br>    metis_tac[integerTheory.INT_<wbr>ABS_EQ_ID])<br>  >><br>    `0 ≤ i` by intLib.COOPER_TAC>><br>    fs[GSYM integerTheory.INT_ABS_EQ_ID]);<br><br>val _ = translate (def_of_const ``ptree_Eliteral`` |> SIMP_RULE std_ss[integer_wordTheory.i2w_<wbr>def,elit_rw,word_2comp_def] |> CONV_RULE wordsLib.WORD_EVAL_CONV)<br><br></div>The i2w becomes something like this:<br><br>(if i < 0 then<br>  n2w<br>    (18446744073709551616 −<br>     if<br>       Num (ABS i) < 18446744073709551616<br>     then<br>       Num (ABS i)<br>     else<br>       Num (ABS i) MOD 18446744073709551616)<br>else n2w (Num (ABS i)))<br><div><br></div><div>(there are special rewrites for Num(ABS i) in the translator)<br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 1, 2016 at 11:55 AM, Yong Kiam <span dir="ltr"><<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Changing it to use n2w should work. I don't think I have ran into i2w in translation before though.<br><br></div>Presumably, this is at a fixed word width so you will want to simplify word_2comp away.<br><br></div><div>BTW, are you fixing / have you fixed lexerProg? I could do it.<br><br></div><div>It's probably failing because of ARBs in toNum and num_from_hex_string, see: <a href="https://github.com/CakeML/cakeml/commit/4347e06c12533161d9311e761e4dbcdb1bd93810" target="_blank">https://github.com/CakeML/cake<wbr>ml/commit/4347e06c12533161d931<wbr>1e761e4dbcdb1bd93810</a><br></div></div><div class="m_-5043841523074240052HOEnZb"><div class="m_-5043841523074240052h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 1, 2016 at 6:34 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I don't think you should translate i2w - can you make your code use<br>
n2w instead? The translator should be able to handle n2w.<br>
(I say this because looking at the translator's hol2deep function I<br>
see it has a case for n2w but not for i2w.)<br>
<div class="m_-5043841523074240052m_-5721015065848315656HOEnZb"><div class="m_-5043841523074240052m_-5721015065848315656h5"><br>
On 1 December 2016 at 21:44,  <<a href="mailto:Michael.Norrish@data61.csiro.au" target="_blank">Michael.Norrish@data61.csiro.<wbr>au</a>> wrote:<br>
> 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?<br>
><br>
> Or can I use n2w instead by altering the Word token constructor to take a num instead of an int?<br>
><br>
> Michael<br>
><br>
> ______________________________<wbr>_________________<br>
> Developers mailing list<br>
> <a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div><br>______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
<br></blockquote></div><br></div>