[CakeML] Users Digest, Vol 28, Issue 3

[Milad Ketabii]

Hi There!

Already I came up with a solution ofr the ELECT_Auxiliary_dec problem.
However, I would be very much thankful if someone let me know about the
TRANSFER_Auxiliary (screenshot Encoding_FOUR.png).

It would also be great if someone had an explanation as why the let binding
in the ELECT_Auxiliary_dec is the criminal (I personally have no idea).

thanks,
Milad

On Mon, Dec 10, 2018 at 8:30 PM <users-request at cakeml.org> wrote:

> Send Users mailing list submissions to
>         users at cakeml.org
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         https://lists.cakeml.org/listinfo/users
> or, via email, send a message with subject or body 'help' to
>         users-request at cakeml.org
>
> You can reach the person managing the list at
>         users-owner at cakeml.org
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Users digest..."
>
>
> Today's Topics:
>
>    1.  New problems in Translation again! (Milad Ketabii)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Mon, 10 Dec 2018 19:19:51 +1100
> From: Milad Ketabii <ketabii.math at gmail.com>
> To: users at cakeml.org
> Subject: [CakeML] New problems in Translation again!
> Message-ID:
>         <
> CAFLPSnwUkppTZP_Pn3paU_Db2tfyb5mUYwj17VBjvaC-RG6XWA at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Hi everyone
>
> Attached are three screen shots that show the encoding of what i want to
> translate from HOL4 to CakeML and the error that I get.
>
> As the error shows, ELECT_Auxiliary_dec is not translatable (the
> Translation.png file). The screenshot (Encoding Two.png)
>  shows the definition of the ELECT_Auxiliary_dec.
> Once i rewrite the ELECT_Auxiliary into another function (screenshot
> EncodingThree,png) the translation goes OK. How can I fix the problem with
> ELECT_Auxiliary_dec so that it becomes translatable. I do not want to
> compute some functions several times so the let binding is important.
>
> The file Encoding_Four,png shows more or less the same problem with another
> definition; once I include it in a pattern match environment, the
> translation goes through. How can I get it translated as it is in the
> screenshot (or with some modifications).
>
> thanks for your hints,
>
> Milad
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <
> https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment.html
> >
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: Translation.png
> Type: image/png
> Size: 194030 bytes
> Desc: not available
> URL: <
> https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment.png
> >
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: Encoding_ScreenOne.png
> Type: image/png
> Size: 200838 bytes
> Desc: not available
> URL: <
> https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0001.png
> >
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: Encoding_ScreenTwo.png
> Type: image/png
> Size: 174523 bytes
> Desc: not available
> URL: <
> https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0002.png
> >
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: Encoding_ScreenThree.png
> Type: image/png
> Size: 159649 bytes
> Desc: not available
> URL: <
> https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0003.png
> >
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: Encoding_Four.png
> Type: image/png
> Size: 94083 bytes
> Desc: not available
> URL: <
> https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0004.png
> >
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>
>
> ------------------------------
>
> End of Users Digest, Vol 28, Issue 3
> ************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181210/99799147/attachment.html>