[CakeML] Low-level Compiler Explorer

[Lars Hupel]

Hi Ramana,

thanks for the quick reply!

> 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.)

Right, exactly. I used Lem to generate Isabelle theories from the
"semantics" folder in the "vml" repository. I made some preliminary
experiments and was already able to prove some trivial lemmas for
evaluation of arithmetic expressions with no toplevel definitions involved.

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

Currently, I'm writing them by hand in order to get a better feel for
the CakeML formalization (hence my original mail to this list). My
long-term goal is to write a compiler from Isabelle code equations to
CakeML ASTs (via a deeply-embedded term rewriting fragment of HOL as an
intermediate step).

(This is obviously inspired from the ICFP'12 paper by Myreen and Owens.)

> 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.)

Yes, I'd appreciate that.

I'm already in the process of trying to build a repository snapshot of
HOL4 with Poly/ML, but so far am struggling with some linker issues.
I'll report back if I can't get it to work.

Cheers
Lars