[CakeML] Low-level Compiler Explorer

Lars Hupel hupel at in.tum.de
Wed Jul 23 12:26:02 UTC 2014

Dear list,

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.

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


More information about the Users mailing list