[CakeML] Monadic translation and in-logic compilation

[Ramana Kumar]

Hi Anthony,

I haven't had a chance to run your example to see what's going wrong (i.e.,
your question 2), however, as Magnus suggested, you can automatically
generate a CF style app theorem from the certificate theorem produced by
the monadic translator. So there shouldn't be any involved manual proof
effort for your use case. I think the function to look for is
app_of_Arrow_rule, or maybe mk_app_of_ArrowP (for the monadic translator).

Cheers,
Ramana

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

> Thanks Magnus,
>
>
>
> I had spotted the code under cakeml/examples? What I’d like to know is:
>
>
>
>    1. Do you have to verify a CF style app theorem if you just want to
>    run (via compilation) translated code?
>    2. What is wrong with what I tried, i.e. using the monadic translator
>    with IO calls? Is it missing a top-level call to “hello” or is something
>    else wrong?
>
>
>
> I just want to wrap a simple command line interface around a HOL4 function
> (as an alternative to EVAL). What’s the quickest route for that? The
> command line and function behaviour might be quite complex, but I don’t
> really need to verify it with pre- and post-conditions (it looks like that
> can be quite involved). As far as I can tell, the compile examples under
> cakeml/examples all required a reasonable amount of manual effort.
>
> Cheers,
>
> Anthony
>
>
>
> *From: *Magnus Myreen <magnus.myreen at gmail.com>
> *Date: *Thursday, 28 June 2018 at 06:04
> *To: *Anthony Fox <Anthony.Fox at arm.com>, "users at cakeml.org" <
> users at cakeml.org>
> *Subject: *Re: [CakeML] Monadic translation and in-logic compilation
>
>
>
> 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
>
> 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/37f3c055/attachment-0001.html>