Re: imperative-to-functional compiler

Hi N,


On 18/01/2011, at 1:53 PM, nojb <n.oje.bar@gmail.com> wrote:


> Suppose you want to translate an imperative language (e.g. a suitable
> subset of Pascal) into a functional language that does not have
> mutable variables (e.g. ML). Is this possible? What would be the
> algorithms/theory that would be relevant to handle the mutability of
> the variables on the Pascal side? Is SSA relevant?


It's certainly possible, and hugely useful, although a lot harder in practice
than some would have you believe.


In my PhD thesis (http://www.jantar.org/phd/) I present a complete translation
of an unabridged ISO 9899:1989 (AKA "ANSI C", "C89", etc) into a sugared, but
pure version of lambda calculus and show that structuring an entire compiler
around such a translation can make its formal verification all but trivial (my
translation includes a complete formal semantics of C and a semi-formally
verified compiler into Knuth's MMIX binaries.)


An alternative route is to translate into SSA first, which is effectively
purely functional. Depending on your source language, pointers and arrays can,
however, make that approach infeasible, since SSA doesn't deal with them
particularly well. Also, from my experience, generating functional
representation of ALGOL languages directly tends to be easier than going
through SSA first, as it can be made syntax driven, even in presence of
unrestricted goto's.


Hope that helps,
Patryk

Return to the comp.compilers page.
Search the comp.compilers archives again.