\documentclass[12pt]{article} \usepackage{isolatin1} \input{psfig.sty} \setlength{\oddsidemargin}{0mm} %\setlength{\evensidemargin}{0mm} \setlength{\evensidemargin}{-2mm} \setlength{\topmargin}{-16mm} \setlength{\textheight}{240mm} \setlength{\textwidth}{158mm} %\setlength{\parskip}{2mm} %\setlength{\parindent}{0mm} \input{macros} \newcommand{\begit}{\begin{itemize}} \newcommand{\enit}{\end{itemize}} \newcommand{\HOAS}{higher-order abstract syntax} \newcommand{\newone}{} %%{\newpage} \newcommand{\heading}[1]{\subsection{#1}} \newcommand{\explanation}[1]{{\small #1}} \newcommand{\empha}[1]{{\em #1}} \newcommand{\rarrow}{\; \rightarrow\;} \newcommand{\nocolor}{} %% {\color[rgb]{0,0,0}} \title{{\bf Single-Source Language Definitions and Code Generation as Linearization}} \author{Aarne Ranta \\ Department of Computing Science \\ Chalmers University of Technology and the University of Gothenburg\\ {\tt aarne@cs.chalmers.se}} \begin{document} \maketitle \subsection*{Abstract} {\em This paper presents a compiler for a fragment of the C programming language, with JVM (Java Virtual Machine) as target language. The compiler is implemented in a purely declarative way: its definition consists of an abstract syntax of program structures and two concrete syntaxes matching the abstract syntax: one for C and one for JVM. From these grammar components, the compiler is derived by using the GF (Grammatical Framework) grammat tool: the front-end consists of parsing and semantic checking in accordance to the C grammar, and the back end consists of linearization in accordance to the JVM grammar. The tool provides other functionalities as well, such as decompilation and interactive editing. } \section{Introduction} The experiment reported in this paper was prompted by a challenge posted by Lennart Augustsson to the participants of the workshop on Dependent Types in Programming held at Dagstuhl in September 2004. The challenge was to use dependent types to write a compiler from C to bytecode. This paper does not meet the challenge quite literally, since our compiler is for a different subset of C than Augustsson's specification, and since the bytecode that we generate is JVM instead of his format. But it definitely makes use of dependent types. Augustsson's challenge did not specify \textit{how} dependent types are to be used, and the first of the two points we make in this paper (and its title) reflects our interpretation: we use dependent types, in combination with higher-order abstract syntax (HOAS), to define the grammar of the source language (here, the fragment of C). The grammar constitutes the single, declarative source from which the compiler front end is derived, comprising both parser and type checker. The second point, code generation by linearization, means that the back end is likewise implemented by a grammar of the target language (in this case, a fragment of JVM). This grammar is the declarative source from which the compiler back end is derived. In addition, some simple string processing is needed to make the code conform to Jasmin assembler requirements. The complete code of the compiler is 300 lines. It is presented in the appendices of this paper. \section{The Grammatical Framework} The tool we have used for implementing the compiler is GF, the \empha{Grammatical Framework} \cite{gf-jfp}. GF is similar to a Logical Framework (LF) \cite{harper-honsell} extended with a notation for defining concrete syntax. GF was originally designed to help building multilingual translation systems for natural languages and also between formal and natural languages. The translation model implemented by GF is very simple: \begin{verbatim} parsing linearization ------------> ------------> Language_1 Abstract Syntax Language_2 <------------ <------------ linearization parsing \end{verbatim} An abstract syntax is similar to a \empha{theory}, or a \empha{signature} in a logical framework. A concrete syntax defines, in a declarative way, a translation of abstract syntax trees (well-formed terms) into concrete language structures, and from this definition, one can derive both both linearization and parsing. For example, a (somewhat simplified) translator for addition expressions consists of the abstract syntax rule \begin{verbatim} fun EAdd : (A : Typ) -> Exp A -> Exp A -> Exp A ; \end{verbatim} the C concrete syntax rule \begin{verbatim} lin EAdd _ x y = {s = x.s ++ "+" ++ y.s ; prec = 2} ; \end{verbatim} and the JVM concrete syntax rule \begin{verbatim} lin EAdd t x y = {s = x.s ++ y.s ++ t.s ++ "_add"} ; \end{verbatim} The abstract syntax rule uses a type argument to capture the fact that addition is polymorphic (which is a simplification, because we will restrict the rule to numeric types only) and that both operands have the same type as the value. The C rule shows that the type information is suppressed, and that the expression has precedence level 2 (which is a simplification, since we will also treat associativity). The JVM rule shows how addition is translated to stack machine instructions, where the type of the postfixed addition instruction again has to be made explicit. Our compiler, like any GF translation system, will consist of rules like these. The number of languages related to one abstract syntax in a translation system is of course not limited to two. Sometimes just just one language is involved; GF then works much the same way as any grammar formalism or parser generator. The largest number of languages in an application known to us is 88, and its domain are numeral expressions from 1 to 999,999 \cite{gf-homepage}. From the GF point of view, the goal of the compiler experiment is to investigate if GF is capable of implementing compilers using the ideas of single-source language definition and code generation as linearization. The working hypothesis was that it \textit{is} capable but inconvenient, and that, working out a complete example, we would find out what should be done to extend GF into a compiler construction tool. \subsection{Advantages and disadvantages} Due to the way in which it is built, our compiler has a number of unusual, yet attractive features: \bequ The front end is defined by a grammar of C as its single source. The grammar defines both abstract and concrete syntax, and also semantic well-formedness (types, variable scopes). The back end is implemented by means of a grammar of JVM providing another concrete syntax to the abstract syntax of C. As a result of the way JVM is defined, only semantically well formed JVM programs are generated. The JVM grammar can also be used as a decompiler, which translates JVM code back into C code. The language has an interactive editor that also supports incremental compilation. \enqu The problems that we encountered and their causes will be explained in the relevant sections of this report. To summarize, \bequ The scoping conditions resulting from \HOAS are slightly different from the standard ones of C. Our JVM syntax is slightly different from the specification, and hence needs some postprocessing. Using \HOAS to encode all bindings is sometimes cumbersome. \enqu The first two shortcomings seem to be inevitable with the technique we use. The best we can do with the JVM syntax is to use simple postprocessing, on string level, to obtain valid JVM. The last shortcoming is partly inherent to the problem of binding: to spell out, in any formal notation, what happens in nested binding structures \textit{is} complicated. But it also suggests ways in which GF could be fine-tuned to give better support to compiler construction, which, after all, is not an intended use of GF as it is now. \section{The abstract syntax} An \empha{abstract syntax} in GF consists of \texttt{cat} judgements \[ \mbox{\texttt{cat}} \; C \; \Gamma \] declaring basic types (depending on a context $\Gamma$), and \texttt{fun} judgements \[ \mbox{\texttt{fun}} \; f \; \mbox{\texttt{:}} \; A \] declaring functions $f$ of any type $A$, which can be a basic type or a function type. \empha{Syntax trees} are well-formed terms of basic types, in $\eta$-long normal form. As for notation, each judgement form is recognized by its keyword (\texttt{cat}, \texttt{fun}, etc), and the same keyword governs all judgements until the next keyword is encountered. The abstract syntax that we will present is no doubt closer to C than to JVM. One reason is that what we are building is a \textit{C compiler}, and match with the target language is secondary consideration. Another, more general reason is tha C is a higher-level language and JVM which means, among other things, that C makes more semantic distinctions. In general, the abstract syntax of a translation system must reflect all semantic distinctions that can be made in the languages involved, and then it is a good idea to start with looking at what the most distinctive language needs. \subsection{Statements} Statements in C may involve variables, expressions, and other statements. The following \texttt{cat} judgements of GF define the syntactic categories that are needed to construct statements \begin{verbatim} cat Stm ; Typ ; Exp Typ ; Var Typ ; \end{verbatim} The type \texttt{Typ} is the type of C's datatypes. The type (\texttt{Exp}) of expressions is a dependent type, since it has a nonempty context, indicating that \texttt{Exp} take a \texttt{Typ} as argument. The rules for \texttt{Exp} will thus be rules to construct well-typed expressions of a given type. \texttt{Var}\ is the type of variables, of a given type, that get bound in C's variable declarations. Let us start with the simplest kind of statements: declarations and assignments. The following \texttt{fun} rules define their abstract syntax: \begin{verbatim} fun Decl : (A : Typ) -> (Var A -> Stm) -> Stm ; Assign : (A : Typ) -> Var A -> Exp A -> Stm -> Stm ; \end{verbatim} The \texttt{Decl}\ function captures the rule that a variable must be declared before it can be used or assigned to: its second argument is a \empha{continuation}, which is the sequence of statements that depend on (= may refer to) the declared variable. The \texttt{Assign} function uses dependent types to control that a variable is always assigned a value of proper type. We will treat all statements, except \texttt{return}s, in terms of continuations. A sequence of statements (which always has the type \texttt{Stm}) thus always ends in a \texttt{return}, or, abruptly, in an empty statement, \texttt{End}. Here are rules for some other statement forms: \begin{verbatim} While : Exp TInt -> Stm -> Stm -> Stm ; IfElse : Exp TInt -> Stm -> Stm -> Stm -> Stm ; Block : Stm -> Stm -> Stm ; Return : (A : Typ) -> Exp A -> Stm ; End : Stm ; \end{verbatim} Here is an example of a piece of code and its abstract syntax. \begin{verbatim} int x ; Decl (TNum TInt) (\x -> x = 5 ; Assign (TNum TInt) x (EInt 5) ( return x ; Return (TNum TInt) (EVar (TNum TInt) x))) \end{verbatim} The details of expression and type syntax will be explained in the next section. \subsection{Types and expressions} Our fragment of C has two types: integers and floats. Many operators of C are overloaded so that they can be used for both of these types, as well as for some other numeric types---but not for e.g.\ arrays and structures. We capture this distinction by a notion reminiscent of \empha{type classes}: we introduce a special category of numeric types, and a coercion of numeric types into types in general. \begin{verbatim} cat NumTyp ; fun TInt, TFloat : NumTyp ; TNum : NumTyp -> Typ ; \end{verbatim} Well-typed expressions are built from constants, from variables, and by means of binary operations. \begin{verbatim} EVar : (A : Typ) -> Var A -> Exp A ; EInt : Int -> Exp (TNum TInt) ; EFloat : Int -> Int -> Exp (TNum TFloat) ; ELt : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Exp (TNum TInt) ; EAdd, EMul, ESub : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Ex ; \end{verbatim} Notice that the category \texttt{Var} has no constructors, but its expressions are only created by variable bindings in \HOAS. Notice also that GF has a built-in type \texttt{Int} of integer literals, but floats are constructed by hand. Yet another expression form are function calls. To this end, we need a notion of (user-defined) functions and argument lists. The type of functions depends on an argument type list and a value type. Expression lists are formed to match type lists. \begin{verbatim} cat ListTyp ; Fun ListTyp Typ ; ListExp ListTyp ; fun EAppNil : (V : Typ) -> Fun NilTyp V -> Exp V ; EApp : (AS : ListTyp) -> (V : Typ) -> Fun AS V -> ListExp AS -> Exp V ; NilTyp : ListTyp ; ConsTyp : Typ -> ListTyp -> ListTyp ; OneExp : (A : Typ) -> Exp A -> ListExp (ConsTyp A NilTyp) ; ConsExp : (A : Typ) -> (AS : ListTyp) -> Exp A -> ListExp AS -> ListExp (ConsExp A AS) ; \end{verbatim} The separation between zero-element applications and other applications is a concession to the concrete syntax of C: it in this way that we can control the use of commas so that they appear between arguments (\texttt{(x,y,z)}) but not after the last argument (\texttt{(x,y,z,)}). The compositionality of linearization (Section~\ref{compositionality} below) forbids case analysis on the length of the lists. \subsection{Functions} On the top level, a program is a sequence of functions. Each function may refer to functions defined earlier in the program. The idea to express the binding of function symbols with \HOAS is analogous to the binding of variables in statements, using a continuation. As with variables, the principal way to build function symbols is as bound variables (in addition, there can be some built-in functions, unlike in the case of variables). The continuation of can be recursive, which we express by making the function body into a part of the continuation; the category \texttt{Rec} is the combination of a function body and the subsequent function definitions. \begin{verbatim} cat Program ; Rec ListTyp ; fun Empty : Program ; Funct : (AS : ListTyp) -> (V : Typ) -> (Fun AS V -> Rec AS) -> Program ; FunctNil : (V : Typ) -> Stm -> (Fun NilTyp V -> Program) -> Program ; \end{verbatim} For syntactic reasons similar to function application expressions in the previous section, we have distinguished between empty and non-empty argument lists. The tricky problem with function definitions is that they involve two nested binding constructions: the outer binding of the function symbol and the inner binding of the function parameter lists. For the latter, we could use vectors of variables, in the same way as vectors of expressions are used to give arguments to functions. However, this would lead to the need of cumbersome projection functions when using the parameters in the function body. A more elegant solution is to use \HOAS to build function bodies: \begin{verbatim} RecOne : (A : Typ) -> (Var A -> Stm) -> Program -> Rec (ConsTyp A NilTyp) ; RecCons : (A : Typ) -> (AS : ListTyp) -> (Var A -> Rec AS) -> Program -> Rec (ConsTyp A AS) ; \end{verbatim} The end result is an abstract syntax whose relation to concrete syntax is somewhat remote. Here is an example of the code of a function and its abstract syntax: \begin{verbatim} let int = TNum TInt in int fact (int n) { Funct int int (\fact -> RecOne int (\n -> int f ; Decl int (\f -> f = 1 ; Assign int f (EInt 1) ( while (1 < n) { While (ELt int (EInt 1) (EVar int n)) (Block ( f = n * f ; Assign int f (EMul int (EVar int n) (EVar int f)) ( n = n - 1 ; Assign int n (ESub int (EVar int n) (EInt 1)) } End)) return f ; (Return int (EVar int f))) End))) } ; Empty) \end{verbatim} \subsection{The \texttt{printf} function} To give a valid type to the C function \texttt{printf} is one of the things that can be done with dependent types \cite{cayenne}. We have not defined \texttt{printf} in its full strength, partly because of the difficulties to compile it into JVM. But we use special cases of \texttt{printf} as statements, to be able to print values of different types. \begin{verbatim} Printf : (A : Typ) -> Exp A -> Stm -> Stm ; \end{verbatim} \section{The concrete syntax of C} A concrete syntax, for a given abstract syntax, consists of \texttt{lincat} judgements \[ \mbox{\texttt{lincat}} \; C \; \mbox{\texttt{=}} \; T \] defining the \empha{linearization types} $T$ of each category $C$, and \texttt{lin} judgements \[ \mbox{\texttt{lin}} \; f \; \mbox{\texttt{=}} \; t \] defining the \empha{linearization functions} $t$ of each function $f$ in the abstract syntax. The linearization functions are checked to be well-typed with respect the \texttt{lincat} definitions, and the syntax of GF forces them to be \empha{compositional} in the sense that the linearization of a complex tree is always a function of the linearizations of the subtrees. Schematically, if \[ f \colon A_{1} \rarrow \cdots \rarrow A_{n} \rarrow A \] then \[ \sugmap{f} \colon \sugmap{A_{1}} \rarrow \cdots \rarrow \sugmap{A_{n}} \rarrow \sugmap{A} \] and the linearization algorithm is simply \[ \sugmap{(f \; a_{1} \; \ldots \; a_{n})} \; = \; \sugmap{f} \; \sugmap{a_{1}} \; \ldots \; \sugmap{a_{n}} \] using the \sugmap{} notation for both linearization types, linearization functions, and linearizations of trees. \label{compositionality} Because of compositionality, no case analysis on expressions is possible in linearization rules. The values of linearization therefore have to carry information on how they are used in different situations. Therefore linearization types are generally record types instead of just the string type. The simplest record type that is used in GF is \bece \verb6{s : Str}6 \ence If the linearization type of a category is not explicitly given by a \texttt{lincat} judgement, this type is used by default. With \HOAS, a syntax tree can have variable-bindings in its constituents. The linearization of such a constituent is compositionally defined to be the record linearizing the body extended with fields for each of the variable symbols: \[ \sugmap{\lambda x_{0} \rarrow \cdots \rarrow \lambda x_{n} \rarrow b} \;=\; \sugmap{b} *\!* \{\$_{0} = \sugmap{x_{0}} ; \ldots ; \$_{n} = \sugmap{x_{n}}\} \] Notice that the requirement the variable symbols can also be found because linearizable trees are in $\eta$-long normal form. Also notice that we are here using the \sugmap{} notation in yet another way, to denote the magic operation that converts variable symbols into strings. \subsection{Resource modules} Resource modules define auxiliary notions that can be used in concrete syntax. These notions include \empha{parameter types} defined by \texttt{param} judgements \[ \mbox{\texttt{param}} \; P \; \mbox{\texttt{=}} \; C_{1} \; \Gamma_{1} \; \mid \; \cdots \; \mid \; \; C_{n} \; \Gamma_{n} \] and \empha{operations} defined by \texttt{oper} judgements \[ \mbox{\texttt{oper}} \; f \; \mbox{\texttt{:}} \; T \; \mbox{\texttt{=}} \; t \] These judgements are similar to datatype and function definitions in functional programming, with the restriction that parameter types must be finite and operations may not be recursive. It is due to these restrictions that we can always derive a parsing algorithm from a set of linearization rules. The following string operations are useful in almost all grammars. They are actually included in a GF \texttt{Prelude}, but are here defined from scratch to make the code shown in the Appendices complete. \begin{verbatim} oper SS : Type = {s : Str} ; ss : Str -> SS = \s -> {s = s} ; cc2 : (_,_ : SS) -> SS = \x,y -> ss (x.s ++ y.s) ; paren : Str -> Str = \str -> "(" ++ str ++ ")" ; \end{verbatim} \subsection{Precedence} We want to be able to recognize and generate one and the same expression with or without parentheses, depending on whether its precedence level is lower or higher than expected. For instance, a sum used as an operand of multiplication should be in parentheses. We capture this by defining a parameter type of precedence levels. Four levels are enough for the present fragment of C, so we use the enumeration type of integers from 0 to 4 to define the \empha{inherent precedence level} of an expression \begin{verbatim} oper Prec : PType = Predef.Ints 4 ; PrecExp : Type = {s : Str ; p : Prec} ; \end{verbatim} in a resource module (see Appendix D), and \begin{verbatim} lincat Exp = PrecExp ; \end{verbatim} in the concrete syntax of C itself. To state that an expression has a certain inherent precedence level, we use the operation \begin{verbatim} mkPrec : Prec -> Str -> PrecExp = \p,s -> {s = s ; p = p} ; \end{verbatim} To use an expression of a given inherent level at some expected level, we define a function that says that, if the inherent level is lower than the expected level, parentheses are required. \begin{verbatim} usePrec : PrecExp -> Prec -> Str = \x,p -> ifThenElse (Predef.lessInt x.p p) (paren x.s) x.s ; \end{verbatim} (The code shown in Appendix D is at the moment more cumbersome, due to holes in the support for integer arithmetic in GF.) With the help of \texttt{mkPrec} and \texttt{usePrec}, we can now define the main high-level operations that are used in the concrete syntax itself---constants (highest level), non-associative infixes, and left associative infixes: \begin{verbatim} constant : Str -> PrecExp = mkPrec 4 ; infixN : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y -> mkPrec p (usePrec x (nextPrec p) ++ f ++ usePrec y (nextPrec p)) ; infixL : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y -> mkPrec p (usePrec x p ++ f ++ usePrec y (nextPrec p)) ; \end{verbatim} (The code in Appendix D adds to this an associativity parameter, which is redundant in GF, but which we use to instruct the Happy parser generator.) \subsection{Expressions} With the machinery introduced, the linearization rules of expressions are simple and concise: \begin{verbatim} EVar _ x = constant x.s ; EInt n = constant n.s ; EFloat a b = constant (a.s ++ "." ++ b.s) ; EMul _ = infixL 3 "*" ; EAdd _ = infixL 2 "+" ; ESub _ = infixL 2 "-" ; ELt _ = infixN 1 "<" ; EAppNil val f = constant (f.s ++ paren []) ; EApp args val f exps = constant (f.s ++ paren exps.s) ; \end{verbatim} \subsection{Statements} Statements in C have the simplest linearization type, \verb6{s : Str}6. We use a handful of auxiliary operations to regulate the use of semicolons on a high level. \begin{verbatim} oper continues : Str -> SS -> SS = \s,t -> ss (s ++ ";" ++ t.s) ; continue : Str -> SS -> SS = \s,t -> ss (s ++ t.s) ; statement : Str -> SS = \s -> ss (s ++ ";"); \end{verbatim} As for declarations, which bind variables, we notice the projection \verb6.$06 to refer to the bound variable. \begin{verbatim} lin Decl typ cont = continues (typ.s ++ cont.$0) cont ; Assign _ x exp = continues (x.s ++ "=" ++ exp.s) ; While exp loop = continue ("while" ++ paren exp.s ++ loop.s) ; IfElse exp t f = continue ("if" ++ paren exp.s ++ t.s ++ "else" ++ f.s) ; Block stm = continue ("{" ++ stm.s ++ "}") ; Printf t e = continues ("printf" ++ paren (t.s ++ "," ++ e.s)) ; Return _ exp = statement ("return" ++ exp.s) ; Returnv = statement "return" ; End = ss [] ; \end{verbatim} \subsection{Functions and programs} The category \texttt{Rec} of recursive function bodies with continuations has three components: the function body itself, the parameter list, and the program that follows. We express this by a linearization type that contains three strings: \begin{verbatim} lincat Rec = {s,s2,s3 : Str} ; \end{verbatim} The body construction rules accumulate the parameter list independently of the two other components: \begin{verbatim} lin RecOne typ stm prg = stm ** { s2 = typ.s ++ stm.$0 ; s3 = prg.s } ; RecCons typ _ body prg = { s = body.s ; s2 = typ.s ++ body.$0 ++ "," ++ body.s2 ; s3 = prg.s } ; \end{verbatim} The top-level program construction rules rearrange the three components into a linear structure: \begin{verbatim} FunctNil val stm cont = ss ( val.s ++ cont.$0 ++ paren [] ++ "{" ++ stm.s ++ "}" ++ ";" ++ cont.s) ; Funct args val rec = ss ( val.s ++ rec.$0 ++ paren rec.s2 ++ "{" ++ rec.s ++ "}" ++ ";" ++ rec.s3) ; \end{verbatim} \section{The concrete syntax of JVM} JVM syntax is, linguistically, more straightforward than the syntax of C, and could even be defined by a regular expression. The translation from our abstract syntax to JVM, however, is tricky because variables are replaced by their addresses (relative to the frame pointer), and code generation must therefore maintain a symbol table that permits the lookup of variable addresses. As shown in the code in Appendix C, we have not attempted to do this in linearization, but instead generated code with symbolic addresses. The postprocessor has to resolve the symbolic addresses, which we help by generating \texttt{alloc} pseudoinstructions from declarations (in final JVM, no \texttt{alloc} instructions appear). The following example shows how the three representations (C, pseudo-JVM, JVM) look like for a piece of code. \begin{verbatim} int x ; alloc i x ; x gets address 0 int y ; alloc i y ; y gets address 1 x = 5 ; ldc 5 ldc 5 i _store x istore 0 y = x ; i _load x iload 0 i _store y istore 1 \end{verbatim} A related problem is the generation of fresh labels for jumps. We solve this by maintaining a growing label suffix as a field of the linearization of statements into instructions. The problem remains that the two branches in an \texttt{if-else} statement can use the same labels. Making them unique will have to be added to the post-processing pass. This is always possible, because labels are nested in a disciplined way, and jumps can never go to remote labels. As it turned out laborious to thread the label counter to expressions, we decided to compile comparison \verb6x < y6 expressions into function calls, which are provided by a run-time library. This would no more work for the conjunction \verb6x && y6 and disjunction \verb6x || y6, if we want to keep their semantics lazy, since function calls are strict in their arguments. The JVM syntax used is from the Jasmin assembler \cite{jasmin}, with small deviations which are corrected by the postprocessor. The deviations other than variable addresses have to do with spacing: the normal unlexer of GF puts spaces between constituents, whereas in JVM, type names are integral parts of instruction names. We indicate gluing uniformly by generating an underscores on the side from which the adjacent element is glued. Thus e.g.\ \verb6i _load6 becomes \verb6iload6. \subsection{How to restore code generation by linearization} Since postprocessing is needed, we have not quite achieved the goal of code generation as linearization. If linearization is understood in the sense of GF. In GF, linearization rules must be compositional, and can only depend on parameters from finite parameter sets. Hence it is not possible to encode linearization with updates to and lookups from a symbol table, as is usual in code generation. Compositionality also prevents optimizations during linearization by clever instruction selection, elimination of superfluous labels and jumps, etc. One way to achieve compositional JVM linearization is to alpha-convert abstract syntax syntax trees so that variables are indexed with integers that indicate their depths in the tree. This hack works in the present fragment of C because all variables need same amount of memory (one word), but would break down if we added double-precision floats. Therefore we have used the less pure (from the point of view of code generation as linearization) method of symbolic addresses. It would certainly be possible to generate variable addresses directly in the syntax trees by using dependent types; but this would clutter the abstract syntax in a way that is hard to motivate when we are in the business of describing the syntax of C. The abstract syntax would have to, so to say, anticipate all demands of the compiler's target languages. \subsection{Problems with JVM bytecode verifier} \section{Translation as linearization vs.\ translation by transfer} The kind of problems we encountered in code generation by linearization are familiar from translation systems for natural languages. For instance, to translate the English pronoun \eex{you} to German, you have to choose between \eex{du, ihr, Sie}; for Italian, there are four variants, and so on. All semantic distinctions made in any of the involved languages have to be present in the common abstract syntax. The usual solution to this problem is not a universal abstract syntax, but \empha{transfer}: translation does not just linearize the same syntax trees to different languages, but defines functions that translates the trees of one language into the trees of another. Using transfer in the compiler back end is precisely what traditional compilers do. The transfer function in our case would be a noncompositional function from the abstract syntax of C to a different abstract syntax of JVM. The abstract syntax notation of GF permits definitions of functions, and the GF interpreter can be used for evaluating terms into normal form. Thus one could write \begin{verbatim} fun transStm : Env -> Stm -> EnvInstr ; def transStm env (Decl typ rest) = ... transStm env (Assign typ var exp rest) = ... \end{verbatim} This would be cumbersome in practice, because GF does not have programming-language facilities like built-in lists and tuples, or monads. Of course, the compiler could no longer be inverted into a decompiler, in the way true linearization can be inverted into a parser. \section{Parser generation} \section{How to use the compiler} \section{Related work} The theoretical ideas behind our compiler experiment are familiar from various sources. Single-source language and compiler definitions can be built using attribute grammars \cite{knuth-attr}. Building single-source language definitions with dependent types and higher-order abstract syntax has been studied in various logical frameworks \cite{harper-honsell,magnusson-nordstr,twelf}. The addition of linearization rules to type-theoretical abstract syntax is studied in \cite{semBNF}, which also compares the method with attribute grammars. The idea of using a common abstract syntax for different languages was clearly exposed by Landin \cite{landin}. The view of code generation as linearization is a central aspect of the classic compiler textbook by Aho, Sethi, and Ullman \cite{aho-ullman}. The use of the same grammar both for parsing and linearization is a guiding principle of unification-based linguistic grammar formalisms \cite{pereira-shieber}. Interactive editors derived from grammars have been used in various programming and proof assistants \cite{teitelbaum,metal,magnusson-nordstr}. Even though the different ideas are well-known, they are applied less in practice than in theory. In particular, we have not seen them used together to construct a complete compiler. In our view, putting these ideas together is an attractive approach to compiling, since a compiler written in this way is completely declarative, hence concise, and therefore easy to modify and extend. What is more, if a new language construct is added, the GF type checker verifies that the addition is propagated to all components of the compiler. As the implementation is declarative, it is also self-documenting, since a human-readable grammar defines the syntax and static semantics that is actually used in the implementation. \section{Conclusion} We have managed to compile a representative subset of C to JVM, and growing it does not necessarily pose any new kinds of problems. Using \HOAS and dependent types to describe the abstract syntax of C works fine, and defining the concrete syntax of C on top of this using GF linearization machinery is already possible, even though more support could be desired for things like literals and precedences. The parser generated by GF is not able to parse all source programs, because some cyclic parse rules (of the form $C ::= C$) are generated from our grammar. Recovery from cyclic rules is ongoing work in GF independently of this experiment. For the time being, the interactive editor is the best way to construct C programs using our grammar. The most serious difficulty with using GF as a compiler tool is how to generate machine code by linearization if this depends on a symbol table mapping variables to addresses. Since the compositional linearization model of GF does not support this, we needed postprocessing to get real JVM code from the linearization result. \bibliographystyle{plain} \bibliography{gf-bib} \newpage \subsection*{Appendix A: The abstract syntax} \small \begin{verbatim} abstract Imper = PredefAbs ** { cat Program ; Rec ListTyp ; Typ ; NumTyp ; ListTyp ; Fun ListTyp Typ ; Body ListTyp ; Stm ; Exp Typ ; Var Typ ; ListExp ListTyp ; fun Empty : Program ; Funct : (AS : ListTyp) -> (V : Typ) -> (Fun AS V -> Rec AS) -> Program ; FunctNil : (V : Typ) -> Stm -> (Fun NilTyp V -> Program) -> Program ; RecOne : (A : Typ) -> (Var A -> Stm) -> Program -> Rec (ConsTyp A NilTyp) ; RecCons : (A : Typ) -> (AS : ListTyp) -> (Var A -> Rec AS) -> Program -> Rec (ConsTyp A AS) ; Decl : (A : Typ) -> (Var A -> Stm) -> Stm ; Assign : (A : Typ) -> Var A -> Exp A -> Stm -> Stm ; While : Exp TInt -> Stm -> Stm -> Stm ; IfElse : Exp TInt -> Stm -> Stm -> Stm -> Stm ; Block : Stm -> Stm -> Stm ; Printf : (A : Typ) -> Exp A -> Stm -> Stm ; Return : (A : Typ) -> Exp A -> Stm ; Returnv : Stm ; End : Stm ; EVar : (A : Typ) -> Var A -> Exp A ; EInt : Int -> Exp (TNum TInt) ; EFloat : Int -> Int -> Exp (TNum TFloat) ; ELt : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Exp (TNum TInt) ; EAdd, EMul, ESub : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Ex ; EAppNil : (V : Typ) -> Fun NilTyp V -> Exp V ; EApp : (AS : ListTyp) -> (V : Typ) -> Fun AS V -> ListExp AS -> Exp V ; TNum : NumTyp -> Typ ; TInt, TFloat : NumTyp ; NilTyp : ListTyp ; ConsTyp : Typ -> ListTyp -> ListTyp ; OneExp : (A : Typ) -> Exp A -> ListExp (ConsTyp A NilTyp) ; ConsExp : (A : Typ) -> (AS : ListTyp) -> Exp A -> ListExp AS -> ListExp (ConsTyp A AS) ; } \end{verbatim} \normalsize \newpage \subsection*{Appendix B: The concrete syntax of C} \small \begin{verbatim} concrete ImperC of Imper = open ResImper in { flags lexer=codevars ; unlexer=code ; startcat=Program ; lincat Exp = PrecExp ; Rec = {s,s2,s3 : Str} ; lin Empty = ss [] ; FunctNil val stm cont = ss ( val.s ++ cont.$0 ++ paren [] ++ "{" ++ stm.s ++ "}" ++ ";" ++ cont.s) ; Funct args val rec = ss ( val.s ++ rec.$0 ++ paren rec.s2 ++ "{" ++ rec.s ++ "}" ++ ";" ++ rec.s3) ; RecOne typ stm prg = stm ** { s2 = typ.s ++ stm.$0 ; s3 = prg.s } ; RecCons typ _ body prg = { s = body.s ; s2 = typ.s ++ body.$0 ++ "," ++ body.s2 ; s3 = prg.s } ; Decl typ cont = continues (typ.s ++ cont.$0) cont ; Assign _ x exp = continues (x.s ++ "=" ++ exp.s) ; While exp loop = continue ("while" ++ paren exp.s ++ loop.s) ; IfElse exp t f = continue ("if" ++ paren exp.s ++ t.s ++ "else" ++ f.s) ; Block stm = continue ("{" ++ stm.s ++ "}") ; Printf t e = continues ("printf" ++ paren (t.s ++ "," ++ e.s)) ; Return _ exp = statement ("return" ++ exp.s) ; Returnv = statement "return" ; End = ss [] ; EVar _ x = constant x.s ; EInt n = constant n.s ; EFloat a b = constant (a.s ++ "." ++ b.s) ; EMul _ = infixL 3 "*" ; EAdd _ = infixL 2 "+" ; ESub _ = infixL 2 "-" ; ELt _ = infixN 1 "<" ; EAppNil val f = constant (f.s ++ paren []) ; EApp args val f exps = constant (f.s ++ paren exps.s) ; TNum t = t ; TInt = ss "int" ; TFloat = ss "float" ; NilTyp = ss [] ; ConsTyp = cc2 ; OneExp _ e = e ; ConsExp _ _ e es = ss (e.s ++ "," ++ es.s) ; } \end{verbatim} \normalsize \newpage \subsection*{Appendix C: The concrete syntax of JVM} \small \begin{verbatim} concrete ImperJVM of Imper = open ResImper in { flags lexer=codevars ; unlexer=code ; startcat=Program ; lincat Rec = {s,s2,s3 : Str} ; -- code, storage for locals, continuation Stm = Instr ; lin Empty = ss [] ; FunctNil val stm cont = ss ( ".method" ++ "public" ++ "static" ++ cont.$0 ++ paren [] ++ val.s ++ ";" ++ ".limit" ++ "locals" ++ stm.s2 ++ ";" ++ ".limit" ++ "stack" ++ "1000" ++ ";" ++ stm.s ++ ".end" ++ "method" ++ ";" ++ ";" ++ cont.s ) ; Funct args val rec = ss ( ".method" ++ "public" ++ "static" ++ rec.$0 ++ paren args.s ++ val.s ++ ";" ++ ".limit" ++ "locals" ++ rec.s2 ++ ";" ++ ".limit" ++ "stack" ++ "1000" ++ ";" ++ rec.s ++ ".end" ++ "method" ++ ";" ++ ";" ++ rec.s3 ) ; RecOne typ stm prg = instrb typ.s ( ["alloc"] ++ typ.s ++ stm.$0 ++ stm.s2) {s = stm.s ; s2 = stm.s2 ; s3 = prg.s}; RecCons typ _ body prg = instrb typ.s ( ["alloc"] ++ typ.s ++ body.$0 ++ body.s2) {s = body.s ; s2 = body.s2 ; s3 = prg.s}; Decl typ cont = instrb typ.s ( ["alloc"] ++ typ.s ++ cont.$0 ) cont ; Assign t x exp = instrc (exp.s ++ t.s ++ "_store" ++ x.s) ; While exp loop = let test = "TEST_" ++ loop.s2 ; end = "END_" ++ loop.s2 in instrl ( "label" ++ test ++ ";" ++ exp.s ++ "ifeq" ++ end ++ ";" ++ loop.s ++ "goto" ++ test ++ ";" ++ "label" ++ end ) ; IfElse exp t f = let false = "FALSE_" ++ t.s2 ++ f.s2 ; true = "TRUE_" ++ t.s2 ++ f.s2 in instrl ( exp.s ++ "ifeq" ++ false ++ ";" ++ t.s ++ "goto" ++ true ++ ";" ++ "label" ++ false ++ ";" ++ f.s ++ "label" ++ true ) ; Block stm = instrc stm.s ; Printf t e = instrc (e.s ++ "invokestatic" ++ t.s ++ "runtime/printf" ++ paren (t.s) ++ "v") ; Return t exp = instr (exp.s ++ t.s ++ "_return") ; Returnv = instr "return" ; End = ss [] ** {s2,s3 = []} ; EVar t x = instr (t.s ++ "_load" ++ x.s) ; EInt n = instr ("ldc" ++ n.s) ; EFloat a b = instr ("ldc" ++ a.s ++ "." ++ b.s) ; EAdd = binopt "_add" ; ESub = binopt "_sub" ; EMul = binopt "_mul" ; ELt t = binop ("invokestatic" ++ t.s ++ "runtime/lt" ++ paren (t.s ++ t.s) ++ "i") ; EAppNil val f = instr ( "invokestatic" ++ f.s ++ paren [] ++ val.s ) ; EApp args val f exps = instr ( exps.s ++ "invokestatic" ++ f.s ++ paren args.s ++ val.s ) ; TNum t = t ; TInt = ss "i" ; TFloat = ss "f" ; NilTyp = ss [] ; ConsTyp = cc2 ; OneExp _ e = e ; ConsExp _ _ = cc2 ; } \end{verbatim} \normalsize \newpage \subsection*{Appendix D: Auxiliary operations for concrete syntax} \small \begin{verbatim} resource ResImper = open Predef in { -- precedence param PAssoc = PN | PL | PR ; oper Prec : PType = Predef.Ints 4 ; PrecExp : Type = {s : Str ; p : Prec ; a : PAssoc} ; mkPrec : Prec -> PAssoc -> Str -> PrecExp = \p,a,f -> {s = f ; p = p ; a = a} ; usePrec : PrecExp -> Prec -> Str = \x,p -> case < : Prec * Prec> of { <3,4> | <2,3> | <2,4> => paren x.s ; <1,1> | <1,0> | <0,0> => x.s ; <1,_> | <0,_> => paren x.s ; _ => x.s } ; constant : Str -> PrecExp = mkPrec 4 PN ; infixN : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y -> mkPrec p PN (usePrec x (nextPrec p) ++ f ++ usePrec y (nextPrec p)) ; infixL : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y -> mkPrec p PL (usePrec x p ++ f ++ usePrec y (nextPrec p)) ; infixR : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y -> mkPrec p PR (usePrec x (nextPrec p) ++ f ++ usePrec y p) ; nextPrec : Prec -> Prec = \p -> case

of { 4 => 4 ; n => Predef.plus n 1 } ; -- string operations SS : Type = {s : Str} ; ss : Str -> SS = \s -> {s = s} ; cc2 : (_,_ : SS) -> SS = \x,y -> ss (x.s ++ y.s) ; paren : Str -> Str = \str -> "(" ++ str ++ ")" ; continues : Str -> SS -> SS = \s,t -> ss (s ++ ";" ++ t.s) ; continue : Str -> SS -> SS = \s,t -> ss (s ++ t.s) ; statement : Str -> SS = \s -> ss (s ++ ";"); -- taking cases of list size param Size = Zero | One | More ; oper nextSize : Size -> Size = \n -> case n of { Zero => One ; _ => More } ; separator : Str -> Size -> Str = \t,n -> case n of { Zero => [] ; _ => t } ; -- operations for JVM Instr : Type = {s,s2,s3 : Str} ; -- code, variables, labels instr : Str -> Instr = \s -> statement s ** {s2,s3 = []} ; instrc : Str -> Instr -> Instr = \s,i -> ss (s ++ ";" ++ i.s) ** {s2 = i.s2 ; s3 = i.s3} ; instrl : Str -> Instr -> Instr = \s,i -> ss (s ++ ";" ++ i.s) ** {s2 = i.s2 ; s3 = "L" ++ i.s3} ; instrb : Str -> Str -> Instr -> Instr = \v,s,i -> ss (s ++ ";" ++ i.s) ** {s2 = v ++ i.s2 ; s3 = i.s3} ; binop : Str -> SS -> SS -> SS = \op, x, y -> ss (x.s ++ y.s ++ op ++ ";") ; binopt : Str -> SS -> SS -> SS -> SS = \op, t -> binop (t.s ++ op) ; } \end{verbatim} \normalsize \newpage \subsection*{Appendix E: Translation to real JVM} This program is written in Haskell. Most of the changes concern spacing and could be done line by line; the really substantial change is due to the need to build a symbol table of variables stored relative to the frame pointer and look up variable addresses at each load and store. \small \begin{verbatim} module JVM where mkJVM :: String -> String mkJVM = unlines . reverse . fst . foldl trans ([],([],0)) . lines where trans (code,(env,v)) s = case words s of ".method":f:ns -> ((".method " ++ f ++ concat ns):code,([],0)) "alloc":t:x:_ -> (code, ((x,v):env, v + size t)) ".limit":"locals":ns -> chCode (".limit locals " ++ show (length ns - 1)) t:"_load" :x:_ -> chCode (t ++ "load " ++ look x) t:"_store":x:_ -> chCode (t ++ "store " ++ look x) t:"_return":_ -> chCode (t ++ "return") "goto":ns -> chCode ("goto " ++ concat ns) "ifzero":ns -> chCode ("ifeq " ++ concat ns) _ -> chCode s where chCode c = (c:code,(env,v)) look x = maybe (x ++ show env) show $ lookup x env size t = case t of "d" -> 2 _ -> 1 \end{verbatim} \normalsize \newpage \subsection*{Appendix F: A Syntax Editor screen dump} %Show Fig~\ref{demo} \begin{figure} \centerline{\psfig{figure=demo2.ps}} \caption{ GF editor session where an integer expression is to be given. The left window shows the abstract syntax tree, and the right window the evolving C and JVM core. The focus is shadowed, and the possible refinements are shown in a pop-up window. } \label{demo} \end{figure} \end{document} \begin{verbatim} \end{verbatim}