[CakeML] Monadic translation and in-logic compilation

Magnus Myreen magnus.myreen at gmail.com
Thu Jun 28 05:04:05 UTC 2018


Hi Anthony,

Good to hear from you!

I suggest you look at the examples in cakeml/examples e.g. the hello
example and how the program term is constructed there. I suspect you can do
something very similar in your setting. Translator proved certificate
theorems can be automatically turned into characteristic formulae (CF)
style app theorems which I believe the hello example proved. Once you have
such a theorem you can follow the work flow of the hello example.

(Sorry for not being more informative. I don’t have my laptop with me at
present.)

Cheers,
Magnus


On Thu, 28 Jun 2018 at 00:26, Anthony Fox <Anthony.Fox at arm.com> wrote:

> The directory
>
>
>
>    cakeml/translator/monadic/examples
>
>
>
> provides some examples of translating monadic functions to CakeML. I would
> like to compile these in the logic and then run them, but I haven’t had
> much luck.  I’ve attached the hello world script that I came up with
> (command line and exception features will be needed eventually, which is
> why they’re included).
>
>
>
> The compile succeeds and produces a hello.S file. I then compile this with:
>
>
>
> $ cc -o hello ${CAKEML}/basis/basis_ffi.c hello.S
>
>
>
> Running the hello program produces no output and no error is reported. Can
> someone explain why this isn’t working? I suspect the problem might be in
> how I’m defining the program (val prog_tm = …)? I’m not sure what should be
> happening between translation and compilation.
>
>
>
> Thanks,
>
> Anthony
>
>
>
>
> IMPORTANT NOTICE: The contents of this email and any attachments are
> confidential and may also be privileged. If you are not the intended
> recipient, please notify the sender immediately and do not disclose the
> contents to any other person, use it for any purpose, or store or copy the
> information in any medium. Thank you.
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20180628/b5c6c2d4/attachment-0001.html>


More information about the Users mailing list