[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?
Cheers
Lars
More information about the Users
mailing list