[CakeML] Monadic translation and in-logic compilation

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Thu Jun 28 15:28:58 UTC 2018


Hi Anthony,

Having looked into this a little further, I have an idea for your question
2. I think the usual machinery adds an extra declaration to the program.
See basis_ffiTheory.whole_prog_spec_semantics_prog to see what this
declaration looks like. Essentially, it adds

  val () = hello();

to the end of your program.

You could try adding that yourself manually and see if it helps!
I think it will, because looking at the end of your prog_tm as currently
defined (in the file you sent), I see it ends with

  val hello = fn _ => print "Hello World!\n";

The semantics of making all those declarations, ending with the above, is
indeed to do no I/O and exit successfully.

Cheers,
Ramana

On Thu, 28 Jun 2018 at 15:12, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

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


More information about the Users mailing list