<div dir="ltr">Hi Lars!<br><div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jul 23, 2014 at 1:26 PM, Lars Hupel <span dir="ltr"><<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I'm currently trying to familiarize myself with CakeML. My current goal<br>
is to generate ASTs inside Isabelle/HOL, and then continue to prove<br>
certain properties wrt to the big step semantics.<br></blockquote><div><br></div><div>I guess you have a copy of the big step semantics inside Isabelle then?<br>In which case you would also have a copy of the AST inside Isabelle.<br>

</div><div>(If not, you could presumably get both by using Lem to generate Isabelle proof documents from the CakeML semantics in Lem.)<br></div><div><br></div><div>When you say "generate ASTs", what would be the input to the procedure for generating an AST?<br>

<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

What I'm struggling with at the moment are some fine points of how<br>
certain terms should be represented as ASTs. For that, I wanted to play<br>
a bit with the online Compiler Explorer. In the "AST" tab, it doesn't<br>
really print an AST, but rather a pretty-printed version of the input.<br></blockquote><div><br></div><div>That's right, the Compiler Explorer does some substantial pretty-printing of the ASTs.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">


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

<br></div><div>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.<br>

<br></div><div>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).<br></div><div><br></div><div>Cheers,<br>Ramana<br></div></div></div>

</div></div>