[CakeML] Low-level Compiler Explorer

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Wed Jul 23 12:40:44 UTC 2014

Hi Lars!

On Wed, Jul 23, 2014 at 1:26 PM, Lars Hupel <hupel at in.tum.de> wrote:

> I'm currently trying to familiarize myself with CakeML. My current goal
> is to generate ASTs inside Isabelle/HOL, and then continue to prove
> certain properties wrt to the big step semantics.

I guess you have a copy of the big step semantics inside Isabelle then?
In which case you would also have a copy of the AST inside Isabelle.
(If not, you could presumably get both by using Lem to generate Isabelle
proof documents from the CakeML semantics in Lem.)

When you say "generate ASTs", what would be the input to the procedure for
generating an AST?

> What I'm struggling with at the moment are some fine points of how
> certain terms should be represented as ASTs. For that, I wanted to play
> a bit with the online Compiler Explorer. In the "AST" tab, it doesn't
> really print an AST, but rather a pretty-printed version of the input.

That's right, the Compiler Explorer does some substantial pretty-printing
of the ASTs.

> However, I'm interested in a more low-level representation. Ideally, I
> want to enter a recursive function and get out something like
>   Dletrec [("foo", "xs", Fun "ys" ...)]
> Is that at all possible?

Yes it is possible. At the moment the numerous ways I can think of getting
such output involve running HOL4. If you are not opposed to that, I can
spell them out. (Also, if it's a one-off thing, you can just send me the
code and I can send back the AST.)

It would also be possible (and quite easy) to create a version of the
Compiler Explorer that does not do as much pretty-printing. (Of course it
will still do _some_ pretty-printing, unless you really want to see raw
simply-typed lambda-calculus terms.) I have CC'ed the Compiler Explorer's
main developer, who might be inspired to create such a version.

However, I suspect we can do better by understanding more precisely what
you're after (e.g. the first questions I wrote in this email).

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140723/87f3b3ec/attachment.html>

More information about the Users mailing list